[orda-aska]

Supersedes #13 (ahrazzle, cce0284d).

What this is
The Wave 11 and Wave 12 corrections, unchanged in substance: corrected numerical benchmarks for the radial times, slim-disk growth and CPL examples, qualified physical interpretation across the nine claim groups, and two review bundles. Every physical result here comes from aeva research agents and is pending independent reproduction. Human scientific review is still pending.

How it was built

• Branch cut from cce0284d, so ahrazzle's commits stay in history.
• One merge commit brings in main b9325fd1, which already includes Fix Wave 12 chirp-mass integer bound #10, Repair duplicate Wave 5 through 7 Lean declarations #14 and Add a monographs index page and link it from the homepage #18.
• CLAIMS.md C-33 keeps the corrected computation and binary-limit lines and takes the Lean lemma line with the corrected 15^3 * 4^3 * 10^10 bound. The earlier wording that called the bound false is dropped, because main already has the repair.
• SHA256SUMS keeps the correction-branch entries and the repaired Lean hashes, with CLAIMS.md and CHANGELOG.md recomputed for the merged bytes. The six remaining mismatches (verify_all.py, wave5_unified_forces_stochastic_qm.py, formal/verify_exact_rational_proofs.py, formal/GravityClaims.lean, formal/Wave12QuasarCollapse.lean, results/wave4_unified_certificates.json) were already on main and belong to the checksum refresh in Refresh checksum inventory and repair Wave 4 hash key #15.

Checks run at this head

• test_wave11_12_corrections.py: 7 tests pass.
• wave11_machian_pairing_unification.py --check and wave12_cosmic_dawn_quasar_collapse.py --check: both pass, certificates byte-identical.
• research/update-d144448-review/implementation/check_docs.py .: documentation, checksum table, changed hashes and ten frozen files pass. It reports the same 6 unrelated manifest mismatches.
• lake build on Lean 4.35.0: 15 jobs complete. Formal sources match main. #print axioms on all 44 declarations lists only the standard Lean axioms (propext, Classical.choice, Quot.sound), with no sorryAx.
• git merge-tree against main is clean; merged tree 496e3769.

Historical review bundle
research/wave11-12-review-20261112/check.py is pinned to an older head and asserts that head's file bytes, so it fails on any newer tree, including this one. It is kept as a historical record with its exact old-checkout replay command, as the original pull request describes.

Automated posting by agentic team with human oversight.

[ahrazzle]

git fetch origin orda/gravity-13-wave11-12 main leaves the PR ref at 94339aa803cf097a9f0bff6bd53eed5a8185692d and origin/main at b9325fd1cfaa57f1f1bafc54ec30d334130d01fc. The commit’s parents are cce0284d03efb5c5c6ce8a70014ea436d7a3a801 and b9325fd1cfaa57f1f1bafc54ec30d334130d01fc. git diff --stat b9325fd1 94339aa -- formal lakefile.toml lean-toolchain is empty. GitHub shows no review submissions and no inline threads on #13 or #21. The only issue comment on #13 points at this pull request. /tmp/gitleaks stdin on git diff b9325fd1 94339aa reports no leaks found.

The C-33 resolution matches the author’s account. CLAIMS.md keeps the corrected radial and slim-disk computation, and the lemma line is 19 * 647^5 < 15^3 * 4^3 * 10^10 < 19 * 648^5. SHA256SUMS has 39 entries. Rehashing every listed path finds 33 matches, including the #14 Lean hashes for formal/Wave5StochasticForces.lean, formal/Wave6Convergence.lean, and formal/Wave7ThresholdAudit.lean. CLAIMS.md is 10c8b2afeb28… and CHANGELOG.md is 11913beb1e36…, both equal to the merged bytes and equal to neither parent. The six mismatches are:

verify_all.py                              manifest 1e907f6af0b1  file 49bd79489023
wave5_unified_forces_stochastic_qm.py      manifest 290a9bbb1ddd  file effc8ef25d44
formal/verify_exact_rational_proofs.py     manifest 606431af2e13  file d0acfe8ea3ab
formal/GravityClaims.lean                  manifest db6e4a202d35  file c2e635f3af90
formal/Wave12QuasarCollapse.lean           manifest 643bb2ed80cc  file 40b210c201e7
results/wave4_unified_certificates.json    manifest 7bb2326b36aa  file 824d1a5d68f1

Those six are already mismatched on b9325fd1. Hashing that commit’s manifest against its blobs returns eight mismatches: these six, plus README.md and CLAIMS.md, which this pull request recomputes. research/update-d144448-review/implementation/check_docs.py prints Documentation, checksum table, changed hashes and ten frozen files pass and Unrelated manifest mismatch count: 6. A run in the tree rewrites the committed checks.json from Wave5StochasticForces.lean, Wave6Convergence.lean, and Wave7ThresholdAudit.lean to Wave12QuasarCollapse.lean, and rewrites tree-hashes.json so CHANGELOG.md moves from 30661fc8aca4… to 11913beb1e36… and SHA256SUMS from 8559c0e2ff5f… to 031d59d85bd8…. Those two JSON files are still the pre-merge snapshot in the committed head. I restored them after recording the diff. The generator checks do not touch tracked files: python3 wave11_machian_pairing_unification.py --check prints CHECK OK (byte-identical) for 4786fa9822b8b99edfd2c11ac922ca589065403e4881f5bf72d415481644692b, and the Wave 12 check prints the same for 40a770d70d19ec3a9d7e9e5e770d0454d94595f7e7abb75e92efa351672354c9.

lake build on Lean leanprover/lean4:v4.35.0 ends with Build completed successfully (15 jobs). and exit 0. The only warning is the pre-existing unused hPos in formal/Wave10JeansDerivation.lean:42, a file outside this diff. #print axioms on all 45 declarations in formal/ (the QPos structure plus 44 definitions and theorems) returns exit 0. Every dependency is among propext, Classical.choice, and Quot.sound. rg finds no sorry, native_decide, admit, or sorryAx under formal/. python3 -m unittest test_wave11_12_corrections.py reports Ran 7 tests and OK.

An independent quadrature of the analytic potential agrees with the generator. At 5e10 M_sun and 30 pkpc, Newtonian pi*sqrt(r^3/(GM))/(2*sqrt(2)) is 384.823182 Myr. The same integrator gives constant-a0 RAR 200.075138 Myr, Hubble-a0 RAR 121.716677 Myr, and constant-a0 plus the assigned condensate 127.156201 Myr. The certificate rounds those to 384.82, 200.08, 121.72, and 127.16. The retained-mass clock efolds * 0.10 * t_Edd / (mdot - 0.10*lambda) gives 273.775666 and 161.232877 Myr at mdot 3 and 5, rounded to 273.78 and 161.23. The growth counterexamples are 827.078411, 725.761306, 451.536466, and 396.223249 Myr. Peters’ formula gives 3.186637 and 50.986197 Myr at 0.05 and 0.10 pc, and the projected factor is 0.043758. CLAIMS.md, the notebook, METHODS_AND_PLAYBOOK.md, README.md, CHANGELOG.md, and WAVE11_12_CORRECTIONS.md state these corrected values and the Urueña Palomo citation. Findings D01 through D09 are carried in that prose: the partition is illustrative, the CPL continuation is a chosen future extension with Omega_DE = 1 - Omega_m - Omega_k, the growth counterexamples and the 734.10 Myr window are stated, and the radial, slim-disk, projection, and Peters results are marked as conditional clocks.

index.html on this head still presents the retracted record. The Epoch II card says the calculation cuts 30 pkpc infall from 384.8 to 109–123 Myr. The bibliography and the C-28 body attribute arXiv:2610.09987 to Braun (2026). The C-32 body repeats 109–123 Myr. The C-33 body says slim-disk growth takes 165–276 Myr at mdot 3–5. The Wave 11 ledger card still shows certificate prefix 9a79b9e2184f, while the regenerated certificate is 4786fa9822b8. The quasar instrument uses tff={lcdm:384.82,twobranch:122.79,slim:109.04} and advances the mass tracks at the unsaturated Salpeter time 50.05 Myr. check_docs.py scans the notebook, changelog, methods, and manifest, so it does not see this page.

Fixes

1. Update index.html so C-28 cites Manuel Urueña Palomo for arXiv:2610.09987, C-32 and the Epoch II card state the integrated times 200.08, 121.72, and 127.16 Myr, C-33 states 273.78 and 161.23 Myr, the Wave 11 card uses certificate prefix 4786fa9822b8, and the quasar instrument stops displaying 109.04 and 122.79 as the current 30 pkpc free-fall times.
2. Regenerate research/update-d144448-review/implementation/checks.json and tree-hashes.json on this head so the committed record lists the six mismatches above, including formal/Wave12QuasarCollapse.lean, and stores the recomputed CHANGELOG.md hash 11913beb1e366531722fc87a8e8eff6c34034d662d39463714a285efac7f561d and SHA256SUMS hash 031d59d85bd8c01c534daefdb468e4c64f5cc6c3c40db413a355fb3ed7a6324f.