FineStruct5Cert
plain-language theorem explainer
A certificate record packaging three structural hypotheses used in the fifth fine-structure derivation: diagonal domain cost vanishes, domain cost is nonnegative on positive mass and energy, and the canonical threshold is positive. Downstream code builds a concrete inhabited instance from the sibling lemmas. Pure structure definition with no proof body.
Claim. A fine-structure certificate is a record asserting: (i) for every nonzero real $r$, the domain cost of $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module FineStructure_Derivation5 is the absolute final session of the RS fine-structure derivation. Status is structural theorem (zero sorry, zero axiom). The target band is $\alpha^{-1}\in(137.030,137.039)$ against CODATA $137.036$, the most precisely tested RS prediction (~0.002% from center).
Domain cost is the local cost functional on mass/energy-type parameters used in this derivation (siblings domainCost, domainCost_at_eq, domainCost_nonneg). Canonical threshold is the positive cutoff against which the derivation compares (siblings canonicalThreshold, canonicalThreshold_pos). Upstream, ObserverForcing records that every recognition event has nonnegative cost via $J$-cost nonnegativity on positive states; the present fields mirror that nonnegativity and zero-on-diagonal pattern at the domain-cost level.
proof idea
No proof body: this is a structure (interface) definition. The three fields are Prop-valued requirements. Downstream cert fills them by assigning the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. cert_inhabited then wraps that instance as Nonempty FineStruct5Cert.
why it matters
Gives a single named bundle for the structural side-conditions of Derivation5 so the module can export one inhabited certificate rather than three loose lemmas. Parents are cert (the concrete filler) and cert_inhabited (nonemptiness). Sits inside the RS fine-structure stack that targets the $\alpha^{-1}$ band $(137.030,137.039)$ against CODATA $137.036$. Does not itself compute $\alpha$; it only packages cost and threshold hygiene that the derivation treats as certified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.