← 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. |
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.