cert
plain-language theorem explainer
Packages three elementary facts about the domain cost and the canonical threshold into a single certificate for the exact fine-structure derivation. Anyone citing the v3 alpha band or the structural theorem status of this module will pull this bundle. The definition is a pure structure instance that wires three already-proved sibling lemmas into the certificate fields.
Claim. There is a certificate recording that (i) the domain cost vanishes on the diagonal ($\mathrm{domainCost}(r,r)=0$ for $r\neq 0$), (ii) the domain cost is nonnegative for positive mass and energy arguments, and (iii) the canonical threshold is strictly positive.
background
This module develops an exact structural derivation of the fine-structure constant in Recognition Science units. The target band is $\alpha^{-1}\in(137.030,137.039)$, which contains the CODATA value $137.036$. Status is structural: zero sorry, zero axioms.
The certificate type bundles three properties of the local cost functional domainCost and a positive threshold canonicalThreshold. Domain cost is the RS cost evaluated on a mass/energy pair; on the diagonal it must vanish (perfect match costs nothing), and off-diagonal it must stay nonnegative. Nonnegativity of recognition cost is the global fact that every recognition event has $J$-cost $\ge 0$, specialized here to the domain-cost signature.
The three field lemmas (domainCost_at_eq, domainCost_nonneg, canonicalThreshold_pos) are siblings in the same file; this definition only assembles them.
proof idea
One-line structure instance. Each field of FineStructExact_v3Cert is filled by the corresponding sibling lemma: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and positivity of the threshold by canonicalThreshold_pos. No additional reasoning.
why it matters
Gives a single named inhabitant of the fine-structure certificate so downstream proofs can assume the three cost/threshold facts at once rather than re-importing them. The module frames this as part of the exact $\alpha^{-1}$ band derivation inside RS units ($c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$), with the reported interval $(137.030,137.039)$ containing CODATA. No used_by edges are recorded yet; the natural consumer is any theorem that needs the certified cost axioms before quoting the numerical band. Sits beside cert_inhabited, which witnesses that the certificate type is nonempty.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.