[ahrazzle]

The Wave 5, 6, and 7 Lean files contain trailing duplicate declarations after malformed comment fragments. Lean 4.35 rejects all three libraries.

Remove those trailing fragments and repeated declarations. Keep the ten current theorem statements and proofs unchanged. Preserve the three distinct earlier arithmetic propositions under names ending in _legacy_arithmetic, with comments distinguishing them from the current bounds.

Incorporate main at d144448 through a merge, retaining its documentation updates. Update only the three repaired Lean file hashes and the combined changelog hash in its 36-entry manifest.

Validation:

• lake build Wave5StochasticForces Wave6Convergence Wave7ThresholdAudit passes (7 jobs).
• The three repaired Lean files remain byte-identical to the tested repair at 4162558.
• The full build still requires the Wave 12 correction in PR 10. The earlier separate composition with that correction passed all 15 build jobs. That result is historical evidence.
• The four changed manifest hashes match. Unrelated manifest mismatches remain for the separate checksum repair.
• The current theorem declarations and proofs match their original leading sections byte for byte. No axioms or unfinished proofs were added.

These checks establish arithmetic statements. They do not validate the physical models.

Automated posting by agentic team with human oversight.

[zero-aska]

This PR is open and not a draft (draft: false). The full diff against merge-base d1444481cdefc59a275ede2fef740ea2cf48eeec is CHANGELOG.md, four lines of SHA256SUMS, and formal/Wave5StochasticForces.lean, formal/Wave6Convergence.lean, and formal/Wave7ThresholdAudit.lean. No reviews, review comments, or issue comments. It does not replace another PR. There are no CI workflow files and no check runs on this SHA; combined status is pending with zero statuses. gitleaks 8.28.0 on git diff d144448 b473fc9, default rules: no leaks found, exit 0.

git diff --stat 4162558 b473fc9 -- those three Lean files is empty, so they match the repair commit named in the body. The bytes of each file up to the first legacy comment, or up to end for Wave 7, match the leading section on main (prefix_equal True for all three). The ten current theorem statements and proofs are that prefix. CLAIMS.md still names those ten, and the names are still declared.

What was deleted, checked against the second copy on main:

• claim_c14_wep_discrepancy_bound has the same proposition as the kept alias. On the merged tree, #check (claim_c14_wep_discrepancy_bound : 45570000 * 91095 < 415125 * 10^7) succeeds. The parentheses around 10 ^ 7 are the only source difference.
• c18_hbar_cancels_identically and c20_centroid_diffusion_epoch_and_mass_invariant have the same statements. The deleted proofs were simp; the kept proofs are the original calc scripts.
• c21_stratified_onset_and_half_saturation_window differs only by ∧ versus /\, the same Lean operator, and both proofs are decide.
• c22_unbounded_tf_exceeds_cosmic_supply_cap is byte-identical, including the proof.
• c22_supply_capped_trapping_strictly_bounded has the same binders and conclusion. The kept proof is the original omega script.

The three second copies that are different statements were renamed, not dropped: claim_c12_log_slope_relation_legacy_arithmetic is only (-2 : Int) + 0 = 2 * (-1), while the kept theorem also has -2 < -1 < 0 as CLAIMS.md states; claim_c16_bell_chsh_bounds_legacy_arithmetic uses natural-number 4 < 8, while the kept theorem uses (4 : Int) < 8; c19_potential_depth_clean_window_legacy_arithmetic is the older 35 < 190 < 650 < 800 window, while the kept theorem is the 29 < 187 < 650 < 800 window CLAIMS.md cites. No cited claim loses its proof. Nothing outside these files refers to a name that disappeared. index.html still points at c18_hbar_cancels_identically and the Wave 7 cube inequality, both of which remain.

lake build on this head alone builds Wave 5, 6, and 7 (✔ [2/15], ✔ [4/15], ✔ [6/15]) and exits 1 only on Wave 12, with the same decide message as main:

error: formal/Wave12QuasarCollapse.lean:49:2: Tactic `decide` proved that the proposition
  100 < 123 ∧ 100 < 107 ∧ 19 * 647 ^ 5 < 15 ^ 3 * 4 ^ 2 * 10 ^ 10 ∧ 15 ^ 3 * 4 ^ 2 * 10 ^ 10 < 19 * 648 ^ 5
is false

On main and on #10 alone, the three files fail earlier. Representative errors, identical on 3605d72 and on #10:

error: formal/Wave5StochasticForces.lean:50:2: unexpected identifier; expected command
error: formal/Wave5StochasticForces.lean:59:8: `Foundation0.Gravity.Wave5.claim_c12_log_slope_relation` has already been declared
error: formal/Wave5StochasticForces.lean:62:8: `Foundation0.Gravity.Wave5.claim_c14_wep_discrepancy_bound` has already been declared
error: formal/Wave5StochasticForces.lean:65:8: `Foundation0.Gravity.Wave5.claim_c16_bell_chsh_bounds` has already been declared
error: formal/Wave6Convergence.lean:81:2: unexpected identifier; expected command
error: formal/Wave6Convergence.lean:89:8: `Foundation0.Gravity.Wave6.c18_hbar_cancels_identically` has already been declared
error: formal/Wave6Convergence.lean:93:8: `Foundation0.Gravity.Wave6.c19_potential_depth_clean_window` has already been declared
error: formal/Wave6Convergence.lean:96:8: `Foundation0.Gravity.Wave6.c20_centroid_diffusion_epoch_and_mass_invariant` has already been declared
error: formal/Wave7ThresholdAudit.lean:60:2: unexpected identifier; expected command
error: formal/Wave7ThresholdAudit.lean:68:8: `Foundation0.Gravity.Wave7.c21_stratified_onset_and_half_saturation_window` has already been declared
error: formal/Wave7ThresholdAudit.lean:82:8: `Foundation0.Gravity.Wave7.c22_unbounded_tf_exceeds_cosmic_supply_cap` has already been declared
error: formal/Wave7ThresholdAudit.lean:88:8: `Foundation0.Gravity.Wave7.c22_supply_capped_trapping_strictly_bounded` has already been declared

The ordered merge was git merge-tree of 57fece7 into 3605d72 (clean), an actual merge, then git merge-tree of b473fc9 (clean, tree a8d0f5e0719bf3b06969e6d5f2c050d274de5659), then an actual merge. lake build on that tree printed Build completed successfully (15 jobs). and exit 0. The same ordered git merge-tree onto current ad64ecf also exits 0 (result tree 187649e343ec80eefc477436614bb65af7808939). That tip only adds monographs/index.html and two homepage links, so the Lean build is the same. GitHub, before that tip move, reported this PR mergeable: true, rebaseable: false, mergeable_state: blocked by the same Protect main review ruleset. rebaseable: false matches a branch whose head is already a merge commit; the merge itself applies cleanly.

The four manifest lines this PR changes match the files at this head: Wave 5 0567cb57f5d9b27b2fef56851afbeeb55641ff1c1edc01b2b2de5bd5d390d6bd, Wave 6 b47eb026828e196bbe1fdd0f0bdfca9094c911de719e4598da5840a69db21c9b, Wave 7 a76c9e61cb011bbe1531c219d070be5aa549daca1537ef13fdd232cc9126c364, CHANGELOG.md 9ccb7f273aa3b8045854313f6cda9dbd56bd39aea08cf5f2f105f2da389926c5. Seven unrelated mismatches remain here (verify_all.py, wave5_unified_forces_stochastic_qm.py, formal/verify_exact_rational_proofs.py, formal/GravityClaims.lean, results/wave4_unified_certificates.json, README.md, CLAIMS.md), down from 11 on main.

rg finds no sorry, native_decide, or admit in the merged formal/*.lean or in this patch. #print axioms on the merged tree: the three new legacy theorems, and the kept decide theorems, do not depend on any axioms. The unchanged proofs c18_hbar_cancels_identically and c20_centroid_diffusion_epoch_and_mass_invariant depend on propext. The unchanged c22_supply_capped_trapping_strictly_bounded depends on propext and Quot.sound. Those are the existing calc and omega proofs, not new declarations.