FineStructureV2Cert
plain-language theorem explainer
Certificate bundling three structural properties used in the RS fine-structure derivation: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Downstream code builds a concrete inhabited instance from sibling lemmas. Pure structure definition with no proof body.
Claim. A fine-structure v2 certificate is a record of three facts: (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
Module Fine_Structure_Derivation_v2 targets the fine-structure constant in Recognition Science: $\alpha^{-1}$ is forced into the open band $(137.030,137.039)$ by the closed form $44\pi\exp(-8\ln\varphi/(44\pi))$, with zero fitted parameters. That band is the strongest single-number check of the framework.
Domain cost is the local cost functional on mass/energy-type arguments appearing in this derivation; the diagonal-vanishing and nonnegativity fields package the same positivity that upstream recognition cost enjoys (ObserverForcing: cost of any recognition event is nonnegative via $J$-cost nonnegativity). Canonical threshold is the positive cutoff against which the derivation compares that cost.
The structure itself carries no dynamics: it only names the three Prop fields later discharged by sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
proof idea
No proof body: this is a structure declaration. The three fields are plain Prop-typed hypotheses (diagonal vanishing of domain cost, nonnegativity on the positive quadrant, positivity of the canonical threshold). Inhabitation is deferred to the sibling definition cert, which fills the fields by those three lemmas, and to cert_inhabited, which wraps ⟨cert⟩.
why it matters
Gives a single named bundle for the structural side-conditions of the v2 fine-structure path, so downstream proofs can depend on one certificate rather than three loose lemmas. Used immediately by cert (the concrete instance) and cert_inhabited (Nonempty). Sits inside the module that claims a machine-checked, zero-parameter derivation of $\alpha^{-1}$ into the RS band $(137.030,137.039)$, the framework's sharpest numerical landmark. Does not itself compute $\alpha$; it only certifies the cost/threshold hygiene the derivation assumes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.