Formalization: mechanize C-01 (Coordinate-vs-Gradient BTFR Dichotomy) and C-04 (1 Mpc vs. Bullet Cluster Phase-Space Inversion) in Lean 4

This formalization issue specifies two clean algebraic theorems from CLAIMS.md for Lean 4 mechanization alongside Foundation-0/physics0.

Theorems for Lean 4 Formalization

C-01 (Coordinate-vs-Gradient BTFR Dichotomy):
- Mechanize the power-law scaling lock showing that an isotropic coordinate-space fractal measure $g_{\text{coord}}(r) = \frac{G M_b}{r^2}\left(1 + \frac{r}{\ell_}\right)^{3 - D_f}$ with $D_f = 2$ forces $v_{\text{flat}}^2 = G M_b / \ell_$, locking the Baryonic Tully-Fisher relation exponent to $\beta_{\text{BTFR}} \equiv d\ln M_b / d\ln v_{\text{flat}} = 2$.
- Contrast with local field-gradient scaling $|\nabla\Phi|/a_0$ which yields $\beta_{\text{BTFR}} = 4$.
C-04 (1 Mpc vs. Bullet Cluster Phase-Space Inversion):
- Mechanize the monotonicity of phase-space degeneracy $\mathcal{N}{\text{deg}}(m\psi, Q) \propto m_\psi^{-4} Q$ where $Q \equiv \rho / \sigma_{\text{1D}}^3$.
- Prove the empty-intersection theorem showing that no single thermalized boson mass $m_\psi$ can satisfy $\mathcal{N}{\text{deg}} \ge \zeta(3/2)$ at $1\text{ Mpc}$ ($Q{\text{gal}} \le 1.13 \times 10^{-27}\text{ kg s}^3/\text{m}^6$) while simultaneously melting $\mathcal{N}{\text{deg}} < \zeta(3/2)$ in the Bullet Cluster core ($Q{\text{Bullet}} \ge 1.48 \times 10^{-27}\text{ kg s}^3/\text{m}^6$).

Primary References

CLAIMS.md (C-01 & C-04) in Foundation-0/gravity
Foundation-0/physics0 Lean 4 codebase

Formal verification deliverables completed! Certified with zero-float Python fractions verifier formal/verify_exact_rational_proofs.py and stock Lean 4 formalization formal/GravityClaims.lean.

Rechecked against main at fcef36e. Two corrections would make the formalization boundary clearer:

Reconcile the C-04 SI inputs in this issue. Using the implemented fiducial model in verify_all.py, lines 218–234, I reproduce:
- Q_gal,isothermal = 2.0144848219e-41 kg s^3/m^6
- Q_gal,NFW = 1.6115878575e-42 kg s^3/m^6
- Q_Bullet = 4.0071287828e-41 kg s^3/m^6
The opening specification quotes values near 1e-27 in the same units. In particular, its Bullet lower bound is not satisfied by the code's fiducial value. The modeled ordering still holds: Q_gal,iso/Q_Bullet = 0.50272525, reproducing the mass thresholds 1.9379 / 1.0306 / 2.3015 eV. This discrepancy does not overturn that conditional calculation.

Minimal reproduction from the repository root:
```
import math
import verify_all as v
vf = (v.G * 6e10 * v.M_SUN * v.A0)**0.25
rho_gal = vf**2 / (4*math.pi*v.G*v.MPC**2)
rho_cl = 2*(1e6)**2 / (4*math.pi*v.G*(250*v.KPC)**2)
print(rho_gal/(vf/math.sqrt(2))**3,
      0.08*rho_gal/(vf/math.sqrt(2))**3,
      rho_cl/(1e6)**3)
```
Separate the checked arithmetic from the physical premises. GravityClaims.lean, lines 29–52 encodes integer exponent identities and fixed rational/integer inequalities. For example, C-04 proves inequalities between c04_num_scaled and c04_den_scaled; it does not define the phase-space function and prove its monotonicity or the empty intersection from quantified physical assumptions. The Python interval calculation likewise uses explicitly chosen parameter intervals. These are useful arithmetic checks, but observational validity and the derivation linking the physical model to those expressions remain separate obligations. C-02 also currently quantifies ds : Int, whereas the physical spectral dimension is real-valued.

Suggested next step: correct the issue's SI values and state these premises beside each certificate; then add the symbolic bridge from the modeled quantities to the checked inequalities. I reviewed the Lean statements but did not rerun the Lean compiler.

Follow-up on the new Wave-5 files at 7a5f0131d5fe: the certificate is not yet reproducible from this revision.

The stored canonical digest does not match the committed payload. Applying the same algorithm used by the Wave-4 generator to the Wave-5 JSON gives:
- Stored: 923d85f100f34ef2f320724af5264243d29018f8981c7cfdc537393bc3ed013b
- Recomputed: 0f80341a31dc19ce1ca9351b74ec56c65b437dc19596af42aed61c275dc8b933
Reproduce from this checkout:
```
import hashlib, json
from pathlib import Path

p = Path("results/wave5_forces_stochastic_certificates.json")
report = json.loads(p.read_text())
stored = report.pop("sha256_canonical")
actual = hashlib.sha256(
    json.dumps(report, sort_keys=True, separators=(",", ":")).encode("utf-8")
).hexdigest()
print(stored, actual, stored == actual)  # False
```
Please regenerate the digest from the final serialized numerical values and add a check that fails when the committed payload and digest differ. If Wave-5 intentionally uses another canonicalization, include its implementation and name it in the schema.
The computation and claim definitions are missing from this snapshot. The three-commit change adds only the JSON and formal/Wave5StochasticForces.lean; the full tree has no Wave-5 numerical generator, and CLAIMS.md ends at C-08. Add the C-12–C-17 statements, inputs, units, source references, calculation/seed details, and regeneration command alongside these results. The new Lean statements currently check three fixed numerical propositions. Until the physical quantities and assumptions are connected to them, label them as arithmetic checks rather than formal verification of the full mass-scaling or Bell-CHSH claims.

AI-assisted review: I reproduced the digest mismatch using Python and inspected the pinned repository tree and Lean statements. I did not run Lean or reproduce the Wave-5 physical calculations.

The C-12–C-17 statements are now present in 765db410, resolving that part of the earlier report. The new ledger entries introduce a specific evidence-mapping problem:

C-13, C-15 and C-17 cite a Lean verification that is absent. The complete Wave-5 Lean file contains exactly three declarations: claim_c12_log_slope_relation, claim_c14_wep_discrepancy_bound and claim_c16_bell_chsh_bounds. There is no theorem for the vacuum-gap law, Nelson dynamics/phase winding or disk evolution/quadrupole argument. Please replace the shared “Verified in” sentence with a per-claim mapping to the actual theorem, derivation or reproducible numerical check.
The new PROVEN labels cover conclusions beyond the supplied evidence. C-15 says Wallstrom’s objection is resolved, while the certificate supplies four scalar summaries and no derivation of quantized circulation. C-17 says a small quadrupole contribution proves a particular condensate is required. Ruling out that contribution does not establish uniqueness of the condensate explanation.

Split the entries into cited literature results, conditional numerical estimates and proposed physical interpretations. Retain PROVEN only for a stated proposition with its assumptions and derivation, and label the unsupported physical conclusions CONJECTURE pending that evidence. This also makes it clear which parts a later verifier should test.

AI-assisted source review of the pinned ledger, certificate, full tree and Lean declarations. Lean and the Wave-5 physical calculations were not run.

Rechecked the new Wave-6 material at bfe6d72. Three concrete corrections are needed:

The Wave-6 digest does not match the committed payload. Using the canonicalization in the existing Wave-4 generator, the new JSON gives:
- Stored: 6b905845aaca043a95ab04effa73e19030d4924130a18cc22f80eb117ba105b0
- Recomputed: d353741fd9b915e307aaab94c67fe383d86de53be5797ffdfe2fc0d6ee334b52
```
import hashlib, json
from pathlib import Path
report = json.loads(Path("results/wave6_convergence_certificates.json").read_text())
stored = report.pop("sha256_canonical")
actual = hashlib.sha256(json.dumps(
    report, sort_keys=True, separators=(",", ":")
).encode()).hexdigest()
print(stored, actual, stored == actual)  # False
```
Regenerate the hash from the final payload and commit an executable check. If another canonicalization is intended, supply its implementation. M-05 currently lists hashes but supplies no regression gate.
The new changelog changes existing claim identities. For example, CHANGELOG.md calls C-05 an exact-rational framework, C-12 early-universe/acoustic bounds, and C-16 WEP checks. In the ledger, those IDs mean the hybrid dark sector, flux-phase/spin dichotomy, and Bell-CHSH respectively. Preserve the ledger's IDs and titles, with explicit links, so collaborators do not attach evidence to a different proposition.
C-18–C-20 still need reproducible definitions and calculations. The three-commit change adds two Markdown files and a scalar JSON certificate, with no numerical generator or formal theorem. The full tree has no Wave-6 generator, and the ledger has no C-18–C-20 entries. Add assumptions, input provenance, the derivation of the 8e-6 threshold and 388.1 km/s onset, and one regeneration command. The redshift-specific hbar claim in the changelog also needs per-redshift evidence, rather than the single scalar in the JSON.

AI-assisted review: reproduced the digest mismatch in Python and inspected the pinned tree and documents. I did not reproduce the Wave-6 physical calculations or run Lean.

The C-18–C-20 ledger entries and Wave-6 Lean file are now present at 0311496, resolving their earlier absence. The new ledger's blanket “Verified in” statements need a narrower mapping to what the theorems establish:

C-20's theorem does not establish epoch constancy. c20_centroid_diffusion_epoch_and_mass_invariant is a rearrangement of the same integer product. It contains neither a diffusion coefficient nor a filament count nor an evolution law. As a logical countercheck, specialize hbar = z + 1: the identity remains true at z = 0, 3, 1100, 10^9, although hbar changes. This is an algebraic counterexample to inferring constancy from that theorem, not a physical model. A proof of the ledger's d hbar/dt = 0 needs an explicit derived quantity and assumptions connecting its values across epochs.
C-19's theorem proves only 35 < 190 < 650 < 800, 5*800 < 6000, and 30*190 < 6000. It has no definitions of potential, roton occupation or effective radiation, so it cannot certify the newly listed 388.1 km/s onset, 0.0% contamination or Delta_N_eff = 0.
C-18's theorem is likewise an integer-product identity. It does not define percolation, a Kelvin-mode spectrum or the claimed 8.958 kpc radius.

Please label these declarations as algebraic lemmas, map each numerical claim to its actual computation, and reserve the broader PROVEN label for statements connected to the physical model by explicit assumptions and derivations. The distinction matters now that CLAIMS.md cites this file as verification of the whole claims.

AI-assisted source review. I checked the C-20 substitutions with exact Python integer arithmetic; I did not run Lean or reproduce the physical calculations.

Reviewed the new Wave-7 certificate, Lean file and C-21/C-22 ledger entries at b35d987. There are three specific gaps to fix before treating these entries as verified empirical and physical bounds:

Keep the reported likelihood differences attached to their actual sample. In the certificate, 1030.2 is the 77-system M0–M3 difference: 1126.24 - 96.08 = 1030.16. Likewise, C-22's 153.2 is that same sample's M1–M3 difference: 249.29 - 96.08 = 153.21. The 60-system WL+X-ray+SPARC sample instead gives 1178.13 and 146.24. Its M2–M3 difference is 15.36, which C-21 also quotes. Label the cohort and model pair for each comparison; the mixed 77-system result does not itself establish a rejection specifically for the 8–14 keV weak-lensing subset. Also supply the null distribution/calibration, effective parameter counts and boundary assumptions behind the “>32 sigma” and “>12 sigma” conversions.
The hashes do not identify accessible reproducibility inputs. The new ledger verification lines repeat 973d6f1d…, but the JSON labels this as full_126_system_catalog_sha256, not a certificate digest. The complete pinned tree contains neither that 126-row catalogue, the pre_envelope_sha256 payload, nor a Wave-7 fitting generator. Please provide the actual input artifacts or a retrieval/extraction script, row-level source provenance and uncertainties/covariances, model definitions and one regeneration command for the fits and confidence intervals. Distinguish the catalogue hash from the report hash.
C-22's cross-multiplied lemma needs a domain before it can imply a saturation-ratio bound. Lines 30–42 allow any integer x. For x=-2, s=1, rSat=2, its conclusion is correctly -3 < -2, but dividing by x+s=-1 gives a ratio of 3, exceeding rSat=2. If this is intended to bound 1 + (rSat-1)*x/(x+s), define that quantity over rationals/reals and require x+s > 0 (for example via x >= 0, s > 0). Separately, the lemma accepts any rSat > 1; it does not establish the physical cap 6.39. That cap needs an explicit model assumption or derivation.

AI-assisted source review. I reproduced the arithmetic differences and denominator counterexample in Python. I did not run Lean, reconstruct the observational catalogue or reproduce the physical fits.

The new root lakefile.toml and pinned toolchain provide a build entry point. One concrete regression in 306e1e7 prevents the intended Wave-5 declaration changes from taking effect:

The replacement theorem block is inside a nested comment. Line 1 begins /-/-, opening two Lean block comments. The -/ at line 24 closes only the inner one; the outer one stays open through the proposed namespace and theorem declarations, until the old header closes at line 54.

Consequently:

claim_c14_mass_ratio_bound is not an active declaration, and the intended alias is not installed.
The strengthened C-12 ordering statement and revised C-16 statement are also commented out.
Only the original three declarations at lines 56–67 remain active.

Replace the old file contents with one header and one intended namespace block. Merely changing the first line to /- would expose the stale header text and duplicate theorem names. Then run lake build and an import smoke test that checks Foundation0.Gravity.Wave5.claim_c14_mass_ratio_bound and prints the revised C-12/C-16 theorem types. A build without those declaration checks can miss this particular mistake because the old definitions remain valid.

AI-assisted source review: verified the nested-comment boundaries and remaining active declarations from the pinned file. Lean is not installed in this environment, so I have not run the compiler.

The two latest commits extend the nested-comment regression reported above to Wave 6 and Wave 7. Checked main at b2c93b0ba02ea51875e10369ea48593477b6f029:

Wave 6, introduced by 29b6310: Wave6Convergence.lean lines 1–85 start with /-/-. The terminator at line 24 closes only the inner comment; the replacement declarations remain commented out until line 85. The active C-19 theorem at lines 93–94 still checks 35 < 190 < 650 < 800, 5*800 < 6000, and 30*190 < 6000, rather than the new 29/187/650/800/6852 interval statement. The original C-18/C-20 simp proofs also remain active, including Int.mul_assoc.
Wave 7, introduced by b2c93b0: Wave7ThresholdAudit.lean lines 1–64 have the same opener. The terminator at line 22 closes only the inner comment, so the proposed replacement namespace and proofs are ignored. Only the old declarations beginning at line 66 are active.

Please replace each file with one header and one intended namespace block, rather than inserting another copy at the start. Include all three Wave-5/6/7 files in the repair. After lake build, import the modules and #print Foundation0.Gravity.Wave6.c19_potential_depth_clean_window to verify the corrected constants actually appear in the compiled theorem, alongside the Wave-5 declaration checks above.

AI-assisted source review: verified the comment boundaries and surviving declarations in both pinned files. Lean is unavailable in this environment, so the compiler was not run.

The Wave-5/6/7 certificate revisions through 2b40d4e resolve the previously reported payload-hash mismatches: I recomputed all three sha256_canonical values successfully. Their new distinctions between literature values, algebraic identities, assumptions and fitted results are useful corrections.

Two follow-ups from these revisions, still present at current main e855db6:

Wave 7's new prose comparison disagrees with its own table. The top-level caveat states delta_chi2 = 10.6 for the zero-covariance WL+X-ray+SPARC subset. The M2/M3 rows give 73.3454 - 57.9852 = 15.3602, consistent with their stored 15.36. Their BIC difference is 81.5341 - 70.2682 = 11.2659, so 10.6 is not that comparison either. Generate the prose number from the same cohort/model fields, or identify the separate fit that produced it.
Propagate the revised evidence status to the claim ledger. For example, the new Wave-5 certificate says quantized circulation must be imposed by hand; C-15 still labels Wallstrom's objection resolved and the claim PROVEN. Similarly, Wave 6 now explicitly identifies the potential threshold as chosen, Delta_N_eff as assumed, and C-20 as an algebraic cancellation rather than a WEP/redshift measurement. Update C-19/C-20 accordingly and replace stale certificate digests in the ledger.

Validation boundary: matching hashes establish payload integrity. The pinned tree still supplies no Wave-5/6/7 numerical generators or Wave-7 catalogue, so the commit messages' “byte-identical” regeneration and the physical fits are not independently reproduced here. Those previously reported reproducibility gaps remain open.

AI-assisted review: checked the current tree and issue discussion, recomputed canonical hashes and the numerical differences in Python. I did not run Lean or reproduce the observational fits.

Verified the newly added Wave-5 generator at 102a1ae. This resolves the Wave-5 generator absence noted in my previous comment.

On Python 3.12.14, using source and certificate bytes verified against their Git blob IDs:

$ python3 wave5_unified_forces_stochastic_qm.py --check
CHECK OK (byte-identical): wave5_forces_stochastic_certificates.json sha256_canonical=5abd85ab08e9d951a248184acb77a8fa8e3164efc73bd523186097e9638c0b76

This reproduces the committed calculations, seeded stochastic outputs and full certificate, beyond merely checking its stored hash. Add this command to the documented regression workflow so future changes preserve that guarantee.

The result is computational reproducibility for the specified model and seed; it does not establish the broader physical interpretations in the claim ledger. The earlier Wave-6/7 reproducibility observations are unchanged.

AI-assisted verification: ran the pinned Python generator with --check; did not run Lean or reproduce observational fits.

Verified the newly added Wave-6 generator at 8343b8b. This resolves the Wave-6 generator absence noted in my earlier reproducibility comment.

On Python 3.12.14, with the source and certificate bytes verified against their Git blob IDs:

$ python3 wave6_convergence_unification.py --check
CHECK OK (byte-identical): wave6_convergence_certificates.json sha256_canonical=49996c541b68290c5512a390b5fcc2ebb7f31b99f349fb74409b974e84bae3bf

This reproduces the full committed certificate, including the C-18/C-20 algebraic calculations and C-19 potential calculations. Add this command alongside the Wave-5 check in the documented regression workflow.

The validation boundary remains the one stated in the generator: the potential threshold is chosen, Delta_N_eff is assumed, and the C-20 cancellation is an identity, not an equivalence-principle or redshift measurement. Reproduction does not validate those physical assumptions. This change does not supply the Wave-7 generator/catalogue or alter the previously discussed Lean and claim-ledger issues.

AI-assisted verification: ran the pinned Python generator with --check; did not run Lean or reproduce observational fits.

Verified the new Wave-7 solver/catalogue and Wave-9 audit through b2661b2. On Python 3.12.14, after verifying source and certificate bytes against their Git blob IDs, both commands pass:

python3 wave7_group_cluster_threshold_audit.py --check
CHECK OK (byte-identical): wave7_group_cluster_certificates.json sha256_canonical=4db35ebcfb7b3cfc6b825e0e62c549435fa7ebdf9e31339e2bbb70482fcc08a9
python3 wave9_scale_convergence_audit.py --check
CHECK OK (byte-identical): wave9_scale_convergence_certificates.json sha256_canonical=d9d19847bb7f9abdc294e58988259d8d20da7593ddce05184d1df81825a33a55

The Wave-7 source and embedded catalogue now resolve the earlier missing-generator/catalogue reproducibility gap. This reproduces the calculations on the encoded data and assumptions; I have not independently checked each catalogue value against the cited papers.

Two actionable clarifications exposed by the new source:

C-24 labels a lower bound as a maximum. In audit_c24_aest_quasistatic_bound, the input is named mu_inv_min_Lstar_Mpc, and the implemented relation is r_C = (18 * r_M * (mu^-1)^2)^(1/3), increasing with mu^-1. Substituting a lower bound therefore gives a lower bound on r_C, not implied_cluster_rC_max_Mpc. The Lstar value gives 2.73276 Mpc; if the stronger KiDS-bin-1 bound applies to the same universal parameter, it gives 3.52216 Mpc. Rename the field to a minimum/boundary value and state which constraint applies. The conclusion that the 250 kpc core lies inside that radius is not overturned by this correction.
The 60-row sample is not wholly zero-covariance. build_catalog() assigns cov=2.0 to 26 Angus X-ray rows. The remaining 34 rows have cov=0.0; fit_sample() and the Wave-9 fits call odr_chi2() with cov_on=True. The sample excludes the optical sigma^4 covariance, but retains X-ray covariance. Describe it that way in the caveat and zero_cov_wl_xray_sparc labels, or run an explicitly covariance-disabled sensitivity fit if a zero-covariance result is intended.

The previously reported Wave-7 prose delta_chi2=10.6 discrepancy also remains in the generator, so regeneration alone does not correct it. Please include both new --check commands in the regression workflow.

AI-assisted verification: reproduced both pinned certificates and inspected the sample construction and bound algebra; did not run Lean or independently validate catalogue provenance/observational assumptions.

The documentation revisions through 01530dc address the earlier request to propagate evidence status to the claim ledger: C-15 no longer claims Wallstrom's objection is resolved, C-19 is explicitly a chosen threshold, and C-20 is explicitly an algebraic identity rather than a WEP measurement. The README now documents the Wave-5/6/7/9 --check commands and distinguishes checksums from signatures.

One new runnable-documentation gap: the README says raw digests are recorded in SHA256SUMS and instructs sha256sum -c SHA256SUMS, but that file is absent from the complete tree at this commit (the contents endpoint also returns 404). Commit the manifest with the advertised coverage, or remove/mark that command pending until it exists. The Python canonical-certificate checks remain available independently.

The previously reported Lean declaration and Wave-7 covariance-label issues are not resolved by these documentation-only commits. In particular, the revised ledger describes intended Wave-5/6 theorem statements without a corresponding Lean source change.

AI-assisted source/documentation review against the pinned tree; no new numerical or Lean execution in this follow-up.

Follow-up at 8e9af4bf36faa278de50c7e341ca613f01c55ab7: root SHA256SUMS is now present, resolving the missing-file part of my previous comment, but 8 of its 26 raw-file digests do not match the committed bytes.

I fetched all 26 files pinned to that commit, independently verified each returned byte sequence against its Git blob SHA-1 from the complete recursive tree, and computed SHA-256 locally. Eighteen match; these eight differ (actual SHA-256):

49bd79489023aed0f6d1b325734012a6b6e0bf4b0b20755e83f20e7fd332583c  verify_all.py
effc8ef25d4489d9cf2d6ea0c0af78d7707fb2c246038f191c8cda22e2a8762d  wave5_unified_forces_stochastic_qm.py
d0acfe8ea3ab801f5538999979c3e4f69545b1734b02a998451d4263f69b3ce6  formal/verify_exact_rational_proofs.py
c2e635f3af901aef8b51b529f46d2c16742c06c597a543e8cf518f4eb636f70e  formal/GravityClaims.lean
8702c37822bcc1178d5d5cade50d59929f8550a61a45cb38ebcc3c5e1d48b9f9  formal/Wave5StochasticForces.lean
4474b263b026d97089dcd8cc154b4ec5964212554901e66a63b16f88094a106d  formal/Wave6Convergence.lean
f8b168944f4364fe6eb2b1af64695b224e5dd8f5ba8f086168b08fcc2bce3fd6  formal/Wave7ThresholdAudit.lean
824d1a5d68f16a2383d6afd3397776d3f3ae99361595379eb827fa71d69321ea  results/wave4_unified_certificates.json

Please regenerate the manifest from the actual intended checkout, then require sha256sum -c SHA256SUMS to pass there before describing it as byte-matching. If these hashes reflect intended but unpublished source corrections, publish those corrections first and regenerate afterward. The manifest addition changes no Lean/source/certificate files, so it does not resolve previously identified Lean declaration discrepancies.

This is raw-byte integrity validation, distinct from canonical JSON regression checks or scientific validation. No numerical suite or Lean build rerun in this follow-up; no repository files changed.

Wave-10 independent computational check at 382327163d05c1732bca30deddfb2ac1802b7b96: after validating the generator, certificate and Wave-7 dependency bytes against their Git blob identities, python3 wave10_covariant_jeans_unification.py --check succeeds with full byte identity and canonical digest 7dd4b40172b8fe261c3028f7a6af6e2b5131fb93cd83d10c439e3c5f0c5be3d4. This reproduces the implemented 185.59 km/s scale, clean-60 chi-square 60.2645, and the tabulated redshift forecasts. It is computational reproducibility, not observational confirmation of the Dark-WHIM mechanism or a Lean build check.

Two actionable scope/wording corrections in the new research notebook:

Thread C generalizes the gamma=2 calculation to all monotone polytropes (gamma > 1) driving sound speed toward c at recombination. Under the same density ratio and calibration, c_s(rec)=185 km/s * (2103266)^((gamma-1)/2): gamma=1.01 gives about 198.97 km/s, gamma=1.1 about 383.10 km/s, and gamma=2 about 268299 km/s. Monotonicity establishes higher sound speed, not a relativistic value for every gamma>1. Please restrict the numerical claim to gamma=2 and state separately what linear-structure constraints exclude the other cases. The sampled operator families do not prove a no-go for every homogeneous FLRW sound-speed operator.
The implemented collapse-scale calculation uses an Eisenstein-Hu analytic transfer-function approximation normalized to an externally supplied sigma8=0.8111, an approximate growth integral, delta_c=1.686, a Delta=200 virial convention, and sigma=V200/sqrt(2). It does not compute a full Boltzmann spectrum from A_s. Please describe 185.59 as a reproducible value under these conventions rather than an exact parameter-free Planck prediction. k=0 accurately means no fitted shape parameter in this catalog evaluation, not absence of external inputs/model choices or independent out-of-sample validation. Recommend sensitivity runs over transfer-function treatment, cosmology and collapse/virial conventions before presenting the numerical coincidence or Delta BIC as evidence for the conjectured fluid closure.

The code appropriately labels that nonlinear closure conjectural. Keep this distinction in the notebook's 'breakthrough' discussion, and add the Wave-10 check to regression documentation when updating the existing raw-hash manifest issue. No repository files changed in this review.

Wave-11 check at 1185a438dee8878d7580771b4d412b3860c70061: pinned generator/certificate/config bytes verified against Git blob identities. python3 wave11_machian_pairing_unification.py --check passes byte-for-byte, digest 9a79b9e2184fcc70cb0e6b250615b57c7492af36d0a605f563bafa0ea87942f5.

New build blocker: lakefile.toml line 4 is malformed: the last targets read "Wave10JeansDerivation, "Wave11MachianZeroEnergy"]]. Python 3.12 tomllib rejects it with TOMLDecodeError: Unclosed array (at line 4, column 129). Close the Wave10 string and remove the extra bracket, so the tail is "Wave10JeansDerivation", "Wave11MachianZeroEnergy"], then run a TOML parse gate and lake build. No Lean compiler run was performed here; the invalid configuration is independently reproduced.

Physical scope: the successful generator checks arithmetic under the selected assumptions, not CPT pair creation, observed future recollapse, or a derivation of inertia. The C-29 closed-universe loop adds negative Omega_k while keeping OMEGA_L=1-OMEGA_M, so its expression has E(1)^2=1-|Omega_k| rather than 1. If these are present-day density parameters normalized by the stated H0, use Omega_DE=1-Omega_m-Omega_k for each curved model and test E(1)=1. Far-future CPL extrapolation from the chosen w0=-0.75, wa=-0.85 must also remain explicitly conditional, not a DESI-established future.

Finally C-30's visible_pair_annihilation_completion=1-eta_B is not derived from the baryon-to-photon ratio: eta_B alone does not specify the initial baryon/antibaryon pair abundance or photon entropy evolution. Rename it as an illustrative proxy or supply the required initial-condition/thermal-history derivation before interpreting it as a measured annihilation fraction.

No repository files changed; the existing manifest mismatch remains a separate unresolved issue.

New notebook scope regression at c5809bc17bbb82c2db11f3c7242cd6f896fd6d23: section 4 now calls C-30 an 'exact mathematical mechanism' that 'pair-bifurcates' from u=0 into two sheets. The committed Python code instead selects u=±(1+10^-6) and evaluates their charges/energy densities; it solves no evolution equation, transition amplitude or initial-value problem. The Lean lemmas prove odd charge/even positive density for the stated polynomial, not physical bifurcation or cosmological creation. Please retain the generator's CONJECTURE qualification for that mechanism and explicitly identify the missing dynamical calculation.

Also keep the exact energy expression aligned: for the implemented polynomial, rho_dust = u J(u) - (u²-1)², not exactly u J(u) as the new notebook states. The omitted pressure term is small near the selected branch but nonzero. Label the latter a near-branch approximation if used.

Section 4's statement that 'every zero-energy virial system bifurcates' into a core/envelope is not established by this suite. In the ordinary isolated Newtonian inverse-square equilibrium setting, 2K+U=0 gives E=K+U=-K<0 for a nontrivial bound system; a zero ADM Hamiltonian constraint is a different statement and is not a universal core-collapse theorem. Please separate the constraint, virial equilibrium and conjectured nonlinear evolution rather than treating the analogy as a demonstrated consequence.

The notebook also repeats the annihilation-percentage inference already flagged above; no new calculation resolves it. This is source/documentation consistency review, not a new numerical or physical validation.

Wave-12 arithmetic blocker at ecc4823505fe9bc0303047953e33c65a408210c7: formal/Wave12QuasarCollapse.lean's c33_super_eddington_and_chirp_mass_bounds includes a false lower-bound proposition, so by decide cannot prove it.

Exact independent integer evaluation:

19 * 647^5 = 2154145352572133
15^3 * 4^2 * 10^10 = 540000000000000
19 * 648^5 = 2170844073787392

The first is NOT less than the second. For chirp mass M_c = (M1*M2)^(3/5)/(M1+M2)^(1/5), raising to the fifth power requires both masses cubed. Replace 4^2 with 4^3 in both theorem bounds and the explanatory comment. The corrected middle integer is 2160000000000000, which lies strictly between the stated endpoints; the corresponding mass is approximately 6.47351308e8 M_sun for the supplied central masses.

Please run the Wave12 target and full lake build after correcting it, and retain the existing caveat that this certifies only arithmetic for chosen inputs, not measured mass uncertainty or physical collapse. The earlier malformed TOML has been corrected, but this newly registered default target introduces a distinct build blocker. I checked the exact integer arithmetic with Python; Lean is unavailable in this environment, so I am not reporting a Lean execution.

Wave-12 generator/certificate check at 3b730af5fc5dd0cd9d5cc5d68b61c53ad06911dd: independently ran wave12_cosmic_dawn_quasar_collapse.py --check; the full certificate reproduced byte-identically, canonical SHA-256 f46cc3be82489f450d1a3ce8c583fad15970050f938bd4c8b5510fe704ba48b6. This validates deterministic reproduction of the chosen model calculations, not the observational inputs or the proposed condensate-collapse mechanism. The separate Lean chirp-mass error remains unchanged.

One new numerical-interpretation correction: C-32 substitutes the MOND/RAR acceleration evaluated at the initial radius into the Newtonian point-mass free-fall formula (pi/2)*sqrt(r/(2*g(r))). That coefficient assumes an inverse-square force throughout the trajectory. MOND/RAR is not inverse-square, so the reported 182.27 and 109.04 Myr should be labeled characteristic-time approximations, not integrated MOND free-fall times. For a specified static spherical force law, integrate t = integral_0^r0 dr / sqrt(2*integral_r^r0 g(s) ds); add a Newtonian analytic control and a deep-MOND control. For a true filament, specify geometry and mass profile separately rather than treating the point-mass approximation as a filament solution.

Likewise the final dynamical-friction sentence should remain explicitly conjectural: the code computes a trapping-fraction ansatz, not a condensate density/velocity distribution, friction force, central seed formation, or a time-dependent heating history. Preserve the useful calculated numbers without promoting those absent dynamics to validated results.

New documentation reconciliation at ab3e633 (not a new numerical result): the Wave-12 section just added to RESEARCH_NOTEBOOK_AND_REASONING.md in 990d866 repeats claims that the pending audit corrections explicitly bound. Please include this newly changed file and the new M-10 methods entry in the correction pass, rather than updating only the generator/CLAIMS ledger.

The notebook's 122.79/109.04 Myr modified-gravity infall figures use the already-identified instantaneous-force substitution, not a radial trajectory integral. Link the corrected point-mass calculation in PR13 and keep its geometry limitation; do not call it a feeder-filament collapse simulation.
M_*=8.39e4 M_sun is a nonlinear halo mass from the chosen spectrum approximation, not an inferred black-hole seed mass. Numerical proximity to a heavy-seed scale does not establish a baryon-to-seed conversion mechanism.
The trapping ansatz supplies neither a Chandrasekhar friction calculation nor a binary hardening/stellar-loss-cone history. The new sentence claiming it brings the pair to sub-parsec inspiral and solves the MOND merger-friction deficit exceeds the supplied evidence. Label this a proposed investigation and specify the missing dynamical calculation.
The reported pair excess and a Gaussian halo-tail estimate do not by themselves give the probability of two simultaneously active quasars at this separation; that requires selection, occupation, duty-cycle and merger/pair statistics.

The new checksum table documents the previously reproduced certificates, not independent validation of these physical conclusions. This comment targets the newly published prose so the correction branches do not leave contradictory current documentation behind.

Publication check on new index.html at 65b236d (Stage index.html part 4/4): current main contains only the final 238-line fragment. It starts inside the radiant drawing callback (const ang=...) with no opening HTML/script, DOM, or preceding definitions, and ends with closing script/body/html tags. This is not yet a functioning standalone page. Please assemble all four parts before presenting it as the interactive research ledger, then smoke-test its controls.

The fragment also introduces numerical chart displays that should be explicitly separated from reproduced research: bicEst = 60.26 + 0.00052*(sj-185.59)^2 is a hard-coded surrogate, not a rerun of the Clean-60 likelihood/BIC scan; the quasar panel retains the previously challenged 122.79/109.04 Myr times and uses t0 = 177.62 + 0.55*tff. Label illustrative formulas as such and source empirical curves from the recorded outputs. Reconcile the quasar interpretation with the pending #13 corrections rather than presenting these slider values as validated dynamics.

This check inspected committed source only; it did not deploy or modify the page, and the new commit adds no independent research calculation.

Navigation Menu

Repository navigation

Formalization: mechanize C-01 (Coordinate-vs-Gradient BTFR Dichotomy) and C-04 (1 Mpc vs. Bullet Cluster Phase-Space Inversion) in Lean 4 #2

Theorems for Lean 4 Formalization

Primary References

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Formalization: mechanize C-01 (Coordinate-vs-Gradient BTFR Dichotomy) and C-04 (1 Mpc vs. Bullet Cluster Phase-Space Inversion) in Lean 4 #2

Description

Theorems for Lean 4 Formalization

Primary References

Activity

orda-aska commented on Nov 11, 2026

zero-aska commented on Nov 11, 2026

zero-aska commented on Nov 11, 2026

zero-aska commented on Nov 11, 2026

zero-aska commented on Nov 11, 2026

zero-aska commented on Nov 11, 2026

zero-aska commented on Nov 11, 2026

zero-aska commented on Nov 11, 2026

zero-aska commented on Nov 11, 2026

zero-aska commented on Nov 12, 2026

zero-aska commented on Nov 12, 2026

zero-aska commented on Nov 12, 2026

zero-aska commented on Nov 12, 2026

zero-aska commented on Nov 12, 2026

zero-aska commented on Nov 12, 2026

zero-aska commented on Nov 12, 2026

zero-aska commented on Nov 12, 2026

zero-aska commented on Nov 12, 2026

zero-aska commented on Nov 12, 2026

zero-aska commented on Nov 12, 2026

zero-aska commented on Nov 13, 2026

zero-aska commented on Nov 13, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions