Prove the existing H4Lagrangian bounds without changing the formulas - #5929
Merged
dmitrii-f-t27 merged 1 commit intoOct 4, 2026
Merged
Conversation
This was referenced Oct 4, 2026
dmitrii-f-t27
marked this pull request as ready for review
October 4, 2026 07:10
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Two existing H4Lagrangian theorem bodies fail against the pinned Mathlib. This proves their original bounds using exponential, pi and square-root inequalities, preserving every formula, definition and theorem statement. The Koide comment now accurately describes the existing relative-error < 1 proposition; this does not establish a one-percent physical prediction.
Fixes #5927. Proof-only child of #3142; its CI permission-policy question remains open.
Validation: pinned Lean 4.31.0 / Mathlib 800238935b9c4b495da5771a0dac0db5549b26ab compiled the complete H4 file locally. Formula and theorem-head bytes were independently compared with the baseline. Both changed theorem axiom reports contain only propext, Classical.choice and Quot.sound, with no added sorry or custom/native axioms. Exact-source Linux CI also reports
Built Trinity.H4Lagrangian (6.8s). Required validate, check-linked-issue and parse-ratchet, plus the Corpus ratchet and GitGuardian, pass.The global Lake job remains red on unchanged TernaryFPGABoot parser/API/proof errors; its generic jitter statement has a verified 1000/1002 counterexample. The other advisory build job remains red. This PR claims the two H4 proofs only, not a green whole library, hardware measurements, or full inference. No ratchet ledger, compiler, generated source or admissions changed.