cert
plain-language theorem explainer
Packages three structural facts about the domain cost and the canonical threshold into a single certificate for the recognition spectrum built from J-cost. Anyone working the phi-ladder spectrum of H_RS cites this bundle as the standing hypotheses. The definition is a direct structure instance that wires three already-proved lemmas; no new argument is introduced.
Claim. A certificate asserting: (i) the domain cost vanishes on the diagonal, $C(r,r)=0$ for all $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (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 equal to the recognition quantum $J(\varphi),\hbar_R,\omega_0$. Status is structural (zero sorry, zero axiom).
The domain cost $C$ is the local cost functional on pairs of positive reals used to score recognition events; it is built from the J-cost $J(x)=(x+x^{-1})/2-1$. The canonical threshold is the positive cutoff that separates the ground state from the first rung of the ladder.
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing (cost_nonneg: every recognition event has nonnegative cost, via $J\ge 0$). The three fields of RecogSpectrum3Cert are the minimal package needed to treat the spectrum as a well-posed nonnegative ladder with a positive first step.
proof idea
One-line structure instance. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No tactic proof and no new calculation; pure wiring of prior results into the certificate type.
why it matters
This certificate is the standing hypothesis pack for the structural theorem that the recognition spectrum arises from J-cost on the phi-ladder (module status: 0 sorry, 0 axiom). It records exactly the three properties needed so that $E_n = J(\varphi^n),\hbar_R,\omega_0$ is a nonnegative spectrum with $E_0=0$ and a positive first excitation equal to the recognition quantum.
In the broader forcing chain this sits downstream of T5 (J-uniqueness) and T6 ($\varphi$ as self-similar fixed point): once $J$ and $\varphi$ are forced, the ladder costs and the threshold must satisfy the three listed axioms for the spectrum to be physically admissible. No downstream consumers are recorded yet in the graph; the immediate sibling cert_inhabited witnesses that the certificate type is nonempty.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.