cert
plain-language theorem explainer
Packages three elementary domain-cost facts into the module-2 certificate for the EM fine-structure band: diagonal vanishing, non-negativity on positive reals, and a strictly positive canonical threshold. Anyone citing the RS Physics Module 2 structural pass (alpha inverse in (137.030, 137.039)) reaches for this bundle. The body is a pure structure constructor wiring three sibling lemmas.
Claim. There is a certificate whose fields assert: (i) for every nonzero real $r$, the domain cost of $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Physics RS Module 2 is the structural certificate layer for the electromagnetic fine-structure constant: it records that $\alpha^{-1}$ lies in the open band $(137.030,137.039)$ with CODATA $137.036$ inside, and is marked RS_PASS with zero sorry and zero axioms.
The certificate type bundles three Prop fields about a real-valued domain cost on pairs of reals and a positive real threshold. Diagonal vanishing says matched nonzero arguments incur zero cost; non-negativity says the cost never goes negative on the positive orthant; threshold positivity is the numerical gate used later in the band argument.
Upstream, non-negativity of recognition cost is already forced in ObserverForcing: "The cost of any recognition event is non-negative," via the J-cost minimum at the identity. The present fields are the module-local specializations of that cost calculus to the domain-cost map used for the alpha band.
proof idea
Pure structure inhabitant. The three fields of the certificate are filled by direct assignment to the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No additional tactic work or rewriting occurs; the definition is the wiring of those three proofs into one named bundle.
why it matters
This is the named inhabitant that discharges the module-2 certificate interface for the EM fine-structure structural theorem. The module doc frames the whole file as the alpha-inverse band claim with CODATA inside and status STRUCTURAL THEOREM. In the broader Recognition chain the band sits among the derived constants (alpha inverse inside (137.030, 137.039)), downstream of J-uniqueness (T5), the self-similar fixed point phi (T6), and the Recognition Composition Law that fixes the cost shape. No further declarations currently depend on this particular name, so its role is to close the module-local certificate rather than to feed a larger proof graph edge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.