RSPhysics002Cert
plain-language theorem explainer
Certificate structure bundling three structural axioms for the RS electromagnetic fine-structure module: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Anyone citing the module's inhabited certificate or the alpha-band structural pass uses this bundle. It is a pure structure definition with no proof body; inhabitants fill the three fields from sibling lemmas.
Claim. A certificate is a triple of facts: (i) for every real $r\neq 0$, the domain cost satisfies $C(r,r)=0$; (ii) for all $m>0$ and $e>0$, $C(m,e)\ge 0$; (iii) the canonical threshold $T$ obeys $T>0$.
background
Physics RS Module 2 targets the electromagnetic fine-structure constant: it asserts $\alpha^{-1}$ lies in the open band $(137.030,137.039)$, which contains the CODATA value $137.036$, and records an RS structural pass with no sorry and no axioms.
The domain cost $C(m,e)$ is the module-local cost on positive mass and energy (or more generally nonzero reals). It is the specialization, in this physics layer, of the Recognition Science J-cost. Upstream, ObserverForcing records that every recognition event has nonnegative cost, via Cost.Jcost_nonneg on a positive state. The canonical threshold is the positive cutoff used by the module's structural checks.
This structure does not compute $\alpha$; it only packages the three cost and threshold properties the module treats as the certificate interface.
proof idea
No proof body: the declaration is a structure (data bundle), not a theorem. The three fields are propositions. Downstream, the concrete inhabitant cert fills them by one-line assignment from the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. Nonemptiness is then immediate: cert_inhabited wraps that inhabitant.
why it matters
The structure is the typed interface for Module 2's structural theorem on the fine-structure band. Downstream cert and cert_inhabited show the interface is realized inside the module, so later physics layers can depend on a single Nonempty certificate rather than three scattered lemmas.
In the Recognition framework this sits under the EM constants story: the primer band $\alpha^{-1}\in(137.030,137.039)$ with CODATA inside. The cost fields echo the global nonnegativity and diagonal-minimum pattern of J-cost (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$), specialized to the mass-energy domain used by the alpha argument. It does not itself close the numerical alpha derivation; it only certifies the cost/threshold scaffolding that module claims as RS_PASS.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.