← Between physics and mathematics · Castellano

Assumptions → certificate → module → observable

A proof certifies an implication. Physics determines whether the actual fields, backgrounds and action satisfy its hypotheses. An experimental comparison additionally needs a prediction with uncertainties.

Chapter	Established statement	Physical scope
Spectrum and profiles	The interval operator determines normal eigenvalues; the Gram matrix tests independence of chosen functions.	A physical mass needs scale and kinetic normalization. A family count needs the actual field domain.
Universal quantization	Q = αA + βB + δC; δ = γ − α/4 − β/3; α, β, δ ∈ ℤ.	Lean checks coefficient arithmetic. H = S(U(2)×U(3)) and its characteristic-class dictionary must describe the proposed theory.
Spin periods	α, β, 2δ ∈ ℤ.	Closed smooth spin four-manifolds have even square periods by Wu parity, supplied outside Lean. The physical orbifold backgrounds are not classified by this theorem.
Joint U(2) criterion	b₀ ∈ ℤ; b₁ + 2b₀ ∈ 8ℤ. (b₀,b₁)=(1,6): Q=m²+mn+n²=c₁²−c₂.	The total characteristic class is integral; an anomaly-free supergravity spectrum is not constructed.
Parent transfer	ℓ(R₁)=ℓ(R₂)=0; 6ℓ(v)=16−3p−3q−6r ≡ 1 (mod 3).	Conditional on the inherited charged spectrum and the specified ordinary integral Green–Schwarz and parent Chern–Simons responses. Additional sectors or corner terms need a new analysis.
Spin(20) lift audit	tₐ²=−1; Uₐ=−itₐ; Uₐ²=+1.	3,290 exact checks, not Lean. A representation phase is not an ordinary Z₂→Spin(20) lift. A combined action may be possible but must include all fields and interactions, including Ω.
ATLAS and CMS	Observed upper limits already used by the laboratory; independent resonance hypotheses and units.	No map from these quantization coefficients to masses, couplings, widths and cross sections is supplied yet. No agreement, exclusion or new-particle discovery follows for the new examples.
Potential and couplings	H=fH(θ−θH); λn=V⁽ⁿ⁾(θH)/(n! fHⁿ).	Canonical local expansion. Lean checks rational polynomial identities; symbolic differentiation checks the logarithm kernel separately.
Recalibrated cases	Nine archived calculations at θH=0.1 and mH=125.1 GeV.	Nearby local couplings do not establish identical global potentials or insensitivity to arbitrary parameters. Dominant towers; bottom omitted; physical uncertainty unquantified.
Measured CMS spectrum	CMS TOP-20-001: dσ/dm(tt̄), 15 bins, pb/GeV.	13 TeV, 137 fb⁻¹, e/μ+jets, parton level, full phase space. Horizontal bars show bin widths; vertical bars are marginal experimental errors. These are measured cross sections, distinct from resonance upper limits.
Covariance and normalization	ρᵢⱼ=Cᵢⱼ/√(CᵢᵢCⱼⱼ); C=L diag(d)Lᵀ, d>0.	Exact positivity concerns the published decimal matrix. Area normalization uses bin widths and induces one null direction at first order. It does not replace the official normalized covariance.
Evidence and next steps	10 rational Lean identities; 15 exact positive pivots; 3 pointwise logarithm derivative bounds.	Full integral error bounds, global minimum certification and an observed GHU fit remain pending. The approximately 7.4% quartic fit/table discrepancy remains open.
Matched wall profiles	s=1/100; R=1/2; epsilon=1/8; alpha=1/20; Delta C(1/4)>0; Delta C(1/2)>0.	Written continuum proof and independently replayed Sage certificate (228 checks). Only two fixed queries; no new Lean formalization, thin-layer rate or complete GHU fit.

Measured data and the figures

The ATLAS curve contains ten published observed 95% CL limits on σ×BR(tt̄), for the RS KK-gluon benchmark with Γ/M=30%, at 13 TeV and 140 fb⁻¹. CMS contains seventy observed narrow qq-resonance limits on σ×B×A, at 13 TeV and 137 fb⁻¹. The vertical axes are logarithmic and use different ranges. Points are the maintained source values; straight segments only guide the eye. They are not measured new-particle production rates. CERN is the laboratory hosting the LHC, not a third independent dataset.

Neither search reports a significant new-particle signal. Experimental evidence can strengthen the applicability of a physical model satisfying a theorem’s assumptions; it cannot turn a conditional theorem into an unconditional physical claim.