cert
plain-language theorem explainer
Packages three elementary facts about the domain cost and the canonical threshold into a single certificate structure used by the RS fine-structure derivation. Anyone citing the structural side of α⁻¹ ∈ (137.030, 137.039) can point here for the cost axioms. The body is a pure structure assembly: three sibling lemmas fill the three fields.
Claim. There is a certificate recording that (i) the domain cost vanishes on the diagonal: $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) the domain cost is nonnegative for positive mass and charge arguments; and (iii) the canonical threshold is strictly positive.
background
This module derives the fine-structure interval $\alpha^{-1}\in(137.030,137.039)$ from Recognition Science, as a structural theorem with no sorry and no extra axioms. The certificate structure collects the cost-side hypotheses needed for that derivation.
Domain cost is the local cost functional on mass/charge pairs that appears in the fine-structure setup. At equilibrium (equal arguments) it is required to vanish; off the diagonal it must stay nonnegative when both arguments are positive. The canonical threshold is the positive cutoff against which the cost comparison is run.
Upstream, nonnegativity of recognition cost is already forced in ObserverForcing: "The cost of any recognition event is non-negative," via the J-cost minimum at identity. The three field fillers here are the in-module specializations of that idea to domain cost and the threshold.
proof idea
One-line structure construction. The three fields of FineStructure2Cert are filled by the sibling lemmas domainCost_at_equilibrium, domainCost_nonneg, and canonicalThreshold_pos respectively. No additional rewriting or case analysis occurs.
why it matters
Gives a named, reusable witness that the cost and threshold side-conditions of the second fine-structure derivation hold. The module status line frames the whole file as the structural theorem delivering $\alpha^{-1}$ inside the RS band $(137.030,137.039)$, which is the framework landmark for the fine-structure constant in RS-native units.
No downstream consumers are wired yet in the graph (used_by is empty), so this certificate is presently a local packaging step rather than a widely cited lemma. It still closes the cost-axiom interface that any later EM-alpha verification (cf. Verification/EMAlphaCert) would import when it needs the domain-cost hypotheses in one place.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.