cert
plain-language theorem explainer
Packages three structural facts about the fine-structure domain cost and threshold into a single certificate record: diagonal vanishing, non-negativity for positive mass/energy, and a strictly positive canonical threshold. Anyone citing the v2 alpha derivation will pull this witness rather than the three lemmas separately. The body is a pure structure assembly with no extra proof work.
Claim. There is a certificate asserting: (i) for every nonzero real $r$, the domain cost satisfies $\mathrm{domainCost}(r,r)=0$; (ii) for all positive reals $m,e$, $\mathrm{domainCost}(m,e)\ge 0$; (iii) the canonical threshold is strictly positive.
background
Module Fine_Structure_Derivation_v2 targets the reciprocal fine-structure constant in the RS band $(137.030,137.039)$, via the closed form $44\pi\exp(-8\ln\varphi/(44\pi))$, with zero fitted parameters. The local certificate type collects the cost-theoretic hypotheses that later steps of that derivation rely on.
Domain cost is the recognition cost assigned to a mass/energy pair in this derivation; the certificate demands it vanish on the diagonal (equal arguments) and stay non-negative off it when both arguments are positive. The canonical threshold is the positive cutoff used to gate the fine-structure comparison. Upstream, non-negativity of recognition cost is already forced by the J-cost: any recognition event has cost $\ge 0$ because $J$ is non-negative on positive reals (ObserverForcing.cost_nonneg, via Cost.Jcost_nonneg).
proof idea
One-line structure inhabitant. The three fields of FineStructureV2Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No tactics, no rewriting, no new arithmetic.
why it matters
This is the packaged hypothesis bundle for the v2 fine-structure derivation, the module the authors call the strongest single-number confirmation of RS (alpha band with zero free parameters, structural theorem, zero sorry). It sits downstream of the J-cost non-negativity forced in the ObserverForcing layer and of T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$) in the forcing chain. No used_by edges are recorded yet; the natural consumer is any theorem that needs a FineStructureV2Cert instance (for example the sibling cert_inhabited, or the alpha-interval proof itself). It does not itself close the alpha bound; it only certifies the cost/threshold side conditions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.