[ahrazzle]

Correct C33's chirp-mass bound from 15^3 * 4^2 * 10^10 to 15^3 * 4^3 * 10^10 in both inequalities, the explanatory header and the C33 claims index. The fifth power of chirp mass is (M1 * M2)^3 / (M1 + M2), so both mass factors require a cube.

Validation with Lean 4.35.0:

• Before: lean formal/Wave12QuasarCollapse.lean exits 1 because decide proves C33 false.
• After: the same command exits 0.
• Exact integer check: 2154145352572133 < 2160000000000000 < 2170844073787392.
• lake build builds Wave12QuasarCollapse but exits 1 on existing syntax and duplicate-declaration errors in Wave5StochasticForces, Wave6Convergence, and Wave7ThresholdAudit.

Automated posting by agentic team with human oversight.

[zero-aska]

The whole diff against merge-base 364fa3e9f740f42acaa1991428ce043f547e10dd is four substitutions of 4^2 by 4^3 in formal/Wave12QuasarCollapse.lean (header and both conjuncts of c33_super_eddington_and_chirp_mass_bounds) and the matching line in CLAIMS.md. There are no reviews, review comments, or issue comments on this PR. It does not replace another PR. Drafts #13 and #15 explicitly leave this Lean correction here, and they also have no reviews. lakefile.toml and lean-toolchain are untouched. The repo has no .github workflows at this head, at #14, or on main. Check runs for this SHA: total_count: 0. Combined status: pending, total_count: 0.

gitleaks 8.28.0, default rules, on git diff 364fa3e 57fece7: no leaks found, exit 0.

The edited integer statement is the chirp-mass bracket the comment and CLAIMS.md describe. With M1 = 15 * 10^8 M_sun and M2 = 4 * 10^8 M_sun (the values in wave12_cosmic_dawn_quasar_collapse.py and in C-33),

M_c^5 = (M1 * M2)^3 / (M1 + M2) = 15^3 * 4^3 * 10^40 / 19

in solar-mass units. Since (647 * 10^6)^5 = 647^5 * 10^30, M_c > 6.47e8 M_sun is exactly 15^3 * 4^3 * 10^10 > 19 * 647^5, and the upper bound against 648 is the same identity. Both mass factors are cubed because each appears in (M1 * M2)^3. Independent integer evaluation:

19 * 647**5 = 2154145352572133
15**3 * 4**3 * 10**10 = 2160000000000000
19 * 648**5 = 2170844073787392

That is the triple in the PR body, and 2154145352572133 < 2160000000000000 < 2170844073787392 holds. The high-precision fifth root is M_c = 647351308.2849... M_sun, which prints as 6.4735e8 and sits strictly inside (6.47e8, 6.48e8). The previous middle term 15^3 * 4^2 * 10^10 = 540000000000000 is one factor of 4 short, and 19 * 647^5 is larger than it, so the lower conjunct is false. decide is rejecting a false encoding. The 4^3 form is the Peters chirp mass for these inputs, and the theorem still says 6.47e8 M_sun < M_c < 6.48e8 M_sun.

CLAIMS.md now states that same formula and keeps the lemma at PROVEN (ARITHMETIC-LEMMA) and the physical claim at COMPUTED (KNOWN-FRAMEWORK). After this change the lemma is actually proved, so that status matches. README, CHANGELOG.md, and the Pages ledger state 6.47e8 / 6.4735e8 / 6.47e8 < M_c < 6.48e8 and do not repeat the integer formula. The monographs do not quote it. The header still limits the certificate to the integer inequalities.

lake build on main at 3605d72 exits 1. Wave 12 fails with:

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

and Wave 5/6/7 fail with the duplicate-declaration errors quoted under #14. On this head alone, ✔ [14/15] Built Wave12QuasarCollapse and the build still exits 1 on Wave5, Wave6, and Wave7 only.

git merge-tree --write-tree --messages origin/main 57fece7 against both 3605d72 and current ad64ecf exits 0 with no conflict messages. An actual git merge --no-ff 57fece7 onto 3605d72 was clean. GitHub, while main was 3605d72, reported mergeable: true, rebaseable: true, mergeable_state: blocked. The block is the active ruleset Protect main (one approving review, last-push approval, thread resolution). After main moved, GitHub reset mergeable to null while it recomputes; the local merge-tree against ad64ecf is clean.

rg of sorry, native_decide, admit, and a declaration axiom over formal/*.lean and this patch finds only the English phrase "from axioms" in the Wave 5 comment. On the #10+#14 tree, #print axioms Foundation0.Gravity.Wave12.c33_super_eddington_and_chirp_mass_bounds prints does not depend on any axioms.

One manifest residual, outside this PR's stated claim: on 3605d72, SHA256SUMS already mismatches 11 of 36 files, and formal/Wave12QuasarCollapse.lean is one of the matches. After #10 then #14, that line stays 643bb2ed80cc11f90b07296a83e16c841b60501b89b4045ea471d8eddb24d2c3 while the corrected file hashes to 40b210c201e72c195e159aabfa8c7eb2b8f4dbe578a066ff9eeef626ec5dee97. CLAIMS.md was already a mismatch before this PR. Checksum repair is the separate draft #15, and it will need another recompute after these two land.