FineStructExact_v3Cert
plain-language theorem explainer
A certificate packing three structural facts used by the exact fine-structure derivation: the domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Anyone citing the v3 alpha inverse band or the inhabited certificate will reference this bundle. It is a pure structure definition; the fields are discharged later by sibling lemmas.
Claim. A certificate consists of three properties: (i) for every nonzero real $r$, the domain cost satisfies $C(r,r)=0$; (ii) for all positive reals $m,e$, one has $C(m,e)\ge 0$; (iii) the canonical threshold $T$ obeys $T>0$.
background
The module targets an exact Recognition Science derivation of the fine-structure constant, with the claimed band $\alpha^{-1}\in(137.030,137.039)$ containing the CODATA value. Status is structural: zero sorry, zero axiom.
Domain cost $C(m,e)$ is the local cost functional on a pair of positive scale parameters (mass-like and energy-like). The diagonal vanishing $C(r,r)=0$ encodes perfect match of the two scales. Nonnegativity mirrors the global J-cost law: recognition cost is never negative. The canonical threshold is the positive cutoff against which the derived inverse-alpha expression is compared.
Upstream, ObserverForcing already proves that every recognition event has nonnegative cost via Jcost_nonneg on a positive state. The present certificate lifts that positivity pattern into the fine-structure domain setting and adds the diagonal identity and threshold positivity needed for the exact v3 argument.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements. Inhabitation is supplied downstream by the noncomputable definition cert, which fills them with the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. The theorem cert_inhabited then packages ⟨cert⟩ as Nonempty FineStructExact_v3Cert.
why it matters
This certificate is the typed interface for the exact fine-structure session. Downstream, cert builds a concrete inhabitant and cert_inhabited records that the type is nonempty, closing the structural half of the v3 derivation.
In the broader RS chain the fine-structure band sits on top of T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$), the golden ratio fixed point $\phi$, and the eight-tick octave. The module doc records the numerical target $\alpha^{-1}\approx 137.036$ inside $(137.030,137.039)$. Bundling diagonal vanishing, cost nonnegativity, and threshold positivity keeps those hypotheses explicit rather than scattered, so later alpha identities can cite a single inhabited certificate instead of three separate lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.