cert
plain-language theorem explainer
Packages three structural facts about the fine-structure domain cost into a single certificate: the cost vanishes on the diagonal, stays nonnegative for positive mass and energy, and the canonical threshold is positive. Anyone citing the Derivation5 alpha band uses this bundle as the structural witness. The definition is a pure structure constructor wiring three already-proved sibling lemmas.
Claim. There exists a certificate recording that the domain cost $C$ satisfies $C(r,r)=0$ for all $r\neq 0$, that $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical threshold $T$ obeys $T>0$.
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)$, with CODATA central value $137.036$, reported as a $0.002%$ match and the most precisely tested RS prediction.
The certificate structure FineStruct5Cert collects three Prop fields: diagonal vanishing of the domain cost, nonnegativity of that cost for positive arguments, and positivity of the canonical threshold. Domain cost is the local cost functional used to gate the fine-structure matching; the canonical threshold is the positive cutoff against which that cost is compared.
Upstream, nonnegativity of recognition cost is already forced in ObserverForcing: any recognition event has cost $\ge 0$ via the J-cost nonnegativity lemma. The present certificate lifts the analogous statements to the fine-structure domain-cost layer.
proof idea
One-line structure constructor. The three fields are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive mass and energy), and canonicalThreshold_pos (strict positivity of the threshold). No new arithmetic is performed; the definition only assembles those proofs into the certificate record.
why it matters
This certificate is the structural witness required by the Derivation5 fine-structure pipeline. The module claims a structural theorem with RS_PASS confirmed on the alpha band $(137.030,137.039)$ against CODATA $137.036$. In the broader RS forcing chain the fine-structure constant sits downstream of T5 J-uniqueness and the RCL, with $\alpha^{-1}$ predicted inside a narrow window once the domain cost and threshold are certified.
No downstream consumers are recorded in the graph for this particular definition, but the sibling cert_inhabited and the module-level alpha claim depend on having an inhabited certificate of this shape. It closes the structural side of the most precise RS numerical test without introducing axioms or sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.