cert
plain-language theorem explainer
Packages three structural facts about the Compton domain cost into a single certificate: vanishing on the mass-energy diagonal, nonnegativity for positive arguments, and a strictly positive canonical threshold. Anyone citing the Compton-5 structural layer would use this object as the inhabited witness. The definition is a pure structure assembly of three already-proved sibling lemmas.
Claim. There is a Compton-5 certificate consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for every $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
The module develops a structural account of the Thomson/Compton cross section from the Recognition Science J-cost, aiming at a relation of the schematic form $\sigma_T = J(\varphi)\cdot(8\pi/3),a_0^2,(m_e/m_p)^2$ rather than a numerical fit. Status is structural: zero sorry, zero axioms.
The domain cost is the local cost functional on mass-energy pairs used in this Compton layer. The certificate structure Compton5Cert packages the three elementary properties needed before any cross-section identity is stated: diagonal vanishing (equal arguments cost nothing), nonnegativity on the positive quadrant, and positivity of the canonical threshold that gates the kinematic regime.
Upstream, nonnegativity of recognition cost is already forced in ObserverForcing: every recognition event has cost $\ge 0$ because $J$ itself is nonnegative. The present certificate lifts that discipline to the Compton domain cost and adds the diagonal and threshold facts.
proof idea
One-line structure construction. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No new algebra is performed; the definition only witnesses that those three propositions inhabit the certificate type.
why it matters
Gives an inhabited structural certificate for the Compton-5 layer so downstream statements can assume diagonal vanishing, cost nonnegativity, and a positive threshold without re-proving them. The module frames this as the structural backbone for deriving the Thomson cross section from J-cost (Plan v7, 120th pass), tying into the RS cost calculus whose uniqueness is forced at T5 ($J(x)=(x+x^{-1})/2-1$). No downstream consumers are recorded yet in the graph; the immediate sibling cert_inhabited is the natural next witness that the type is nonempty. Does not itself evaluate $\sigma_T$ or close the numerical match to $6.65\times 10^{-29},\mathrm{m}^2$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.