RecogSpectrum3Cert
plain-language theorem explainer
Certificate structure packing three structural facts for the recognition spectrum built from J-cost on the phi-ladder: vanishing diagonal domain cost, nonnegativity of domain cost on positive arguments, and positivity of the canonical threshold. Spectrum constructions and the inhabited certificate in this module cite it. Pure structure definition with no proof body.
Claim. A recognition-spectrum certificate is a triple of facts: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals 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 builds the recognition spectrum of $H_{RS}$ from the phi-ladder: energy levels $E_n = J(\varphi^n),\hbar_R,\omega_0$ for $n=0,1,2,\ldots$, with ground state $E_0=0$ and first excited level the recognition quantum $E_1=J(\varphi),\hbar_R,\omega_0$. Status is structural (zero sorry, zero axiom).
Domain cost is the local cost functional on pairs of positive reals used to score recognition mismatch; its diagonal vanishing and nonnegativity are the analytic content of the first two fields. The canonical threshold is the positive cutoff that separates the ground state from the first rung of the spectrum.
Upstream, ObserverForcing already records that every recognition-event cost is nonnegative via $J$-cost nonnegativity. The present structure lifts that idea to the domain-cost interface needed by the spectrum construction.
proof idea
No proof: this is a structure declaration. It packages three Prop-valued fields (diagonal vanishing of domain cost, nonnegativity of domain cost on positive arguments, positivity of the canonical threshold). Inhabitation is supplied downstream by the concrete cert record, which fills the fields with the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives the typed interface that the recognition-spectrum development needs before it can talk about discrete levels $E_n=J(\varphi^n),\hbar_R,\omega_0$. Downstream, cert assembles a concrete inhabitant and cert_inhabited records that the type is nonempty, closing the structural side of the module.
In the broader framework this sits under T5 ($J$-uniqueness, $J(x)=(x+x^{-1})/2-1$) and the phi-ladder forced at T6: the spectrum is exactly the image of that ladder under $J$, scaled by the RS units. The certificate isolates the three analytic hypotheses (diagonal zero, nonnegativity, positive threshold) so later spectrum theorems can cite a single object rather than three separate lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.