cert
plain-language theorem explainer
Packages three verified properties into a single certificate for the recognition energy floor: domain cost vanishes on equal arguments, stays non-negative for positive mass and energy, and the canonical threshold is strictly positive. Anyone citing the recognition quantum E_min = J(φ)·E_coh uses this bundle. The definition is a pure structure assembly of three already-proved sibling lemmas.
Claim. There is a certificate recording that (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; and (iii) the canonical threshold is strictly positive. Together these certify the recognition energy floor $E_{\min}=J(\varphi)\,E_{\mathrm{coh}}$.
background
The module fixes the recognition energy floor: no recognition event costs less than $J(\varphi),E_{\mathrm{coh}}\approx 0.118,E_{\mathrm{coh}}$ per rung. That quantity is the recognition quantum. Domain cost is the local cost functional on mass/energy pairs; the canonical threshold is the positive lower bound tied to $J(\varphi)$.
The certificate structure RecogEnergyFloorCert packages three Prop fields: diagonal vanishing of domain cost, nonnegativity for positive arguments, and positivity of the canonical threshold. Upstream, ObserverForcing already records that every recognition-event cost is nonnegative via $J$-cost nonnegativity. The three sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos discharge the three fields.
proof idea
One-line structure instance. Each field of the certificate is filled by the corresponding sibling lemma: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and threshold positivity by canonicalThreshold_pos. No further tactic work.
why it matters
This is the structural certificate that the recognition energy floor is inhabited and consistent. The module status is STRUCTURAL THEOREM (0 sorry, 0 axiom). It anchors the claim that recognition events cannot undercut $J(\varphi),E_{\mathrm{coh}}$ per rung, tying the $J$-cost minimum (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$) to the self-similar scale $\varphi$ (T6). No downstream consumers are wired yet in the graph; the natural parent is any theorem that quotes the recognition quantum or the energy-floor bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.