FineStructure2Cert
plain-language theorem explainer
A certificate packing three analytic facts used in the RS fine-structure interval: the domain cost vanishes on the diagonal away from zero, stays non-negative for positive arguments, and the canonical threshold is strictly positive. Anyone citing the α⁻¹ band derivation or the inhabited certificate will point here. It is a pure structure definition; no proof body.
Claim. A certificate consists of three properties: (i) for every real $r \neq 0$, the domain cost at $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost at $(m,e)$ is non-negative; (iii) the canonical threshold is strictly positive.
background
This module targets a structural derivation of the fine-structure inverse in the open interval $(137.030, 137.039)$ from Recognition Science, with zero sorry and zero axioms. The local objects are a real-valued domain cost on pairs of positive scales and a fixed positive canonical threshold that gates the fine-structure construction.
Upstream, recognition costs are already known to be non-negative: ObserverForcing records that every recognition event has cost $\ge 0$, via non-negativity of the $J$-cost on positive states. The domain cost here is the physics-side specialization of that cost language to the mass/energy (or scale/scale) pair used in the fine-structure pass.
The three fields of the certificate are exactly the lemmas proved as siblings in the same module: equilibrium vanishing on the diagonal, non-negativity off equilibrium, and positivity of the threshold.
proof idea
No proof: this is a structure declaration. It packages three Prop-valued fields that a later def cert fills by pointing at domainCost_at_equilibrium, domainCost_nonneg, and canonicalThreshold_pos. Inhabitation is then a one-constructor theorem cert_inhabited.
why it matters
The certificate is the typed interface between the cost calculus and the fine-structure interval claim of the module. Downstream, cert assembles a concrete inhabitant and cert_inhabited records Nonempty FineStructure2Cert, so any later theorem that needs the three analytic side-conditions can take a certificate rather than re-proving them.
In the broader RS chain this sits under the electromagnetic fine-structure derivation (the α⁻¹ band quoted in the module doc, matching the primer interval $(137.030, 137.039)$). It does not itself force φ, the eight-tick octave, or $D=3$; those enter earlier. It only locks the cost-and-threshold hygiene required for the Plan v7 sixty-fourth-pass structural theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.