ElectronCompton3Cert
plain-language theorem explainer
Certificate packing three structural hypotheses used in the electron Compton derivation from J-cost: domain cost vanishes on the diagonal, is nonnegative for positive mass/energy arguments, and the canonical threshold is positive. Downstream code builds a concrete inhabitant and a Nonempty proof from it. Pure structure definition; no proof obligations live here.
Claim. A certificate is a triple of properties: (i) for every nonzero real $r$, the domain cost of the pair $(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
The module derives the electron Compton wavelength on the Recognition Science $\phi$-ladder as a structural theorem (zero sorry, zero axiom). In SI units $\lambda_C = h/(m_e c) \approx 2426,\mathrm{fm}$; relative to the Planck length one has $\lambda_C/\ell_{\mathrm{Pl}} = \phi^k$ with $k = \log(1.5\cdot 10^{20})/\log\phi \approx 97.5$, so $\lambda_C = \phi^{97.5}\ell_{\mathrm{Pl}}$.
Domain cost is the local cost functional comparing a mass-like scale to an energy-like scale; it is the specialization of the RS $J$-cost used in this file. The canonical threshold is the positive cutoff against which that cost is compared when locking the Compton rung.
Upstream, ObserverForcing records that every recognition-event cost is nonnegative via $J$-cost nonnegativity at positive state. The three fields of this certificate are the exact interface those facts must satisfy before the Compton packing lemmas can fire.
proof idea
No proof body: the declaration is a structure whose three fields are propositions. Inhabitation is deferred to the sibling cert, which assigns domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos fieldwise, and to cert_inhabited, which wraps that term in Nonempty.
why it matters
This is the typed interface for the electron-Compton-from-$J$-cost structural package. Downstream, cert supplies a concrete term and cert_inhabited proves the type is nonempty, closing the certificate layer of the module.
In the broader RS chain the Compton ratio sits on the $\phi$-ladder (primer mass formula / rung arithmetic), with the same $J$-cost that T5 forces uniquely via the Recognition Composition Law. The certificate isolates only the cost-and-threshold fragment needed for that rung lock; it does not itself compute $k\approx 97.5$, but it is the hypothesis bundle every later packing step in this file consumes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.