cert
plain-language theorem explainer
Packages three structural facts into a Debye-frequency certificate: domain cost vanishes on the diagonal, is nonnegative for positive mass and energy scales, and the canonical threshold is positive. Anyone citing the φ-ladder Debye construction uses this witness. The body is a pure structure assembly of three already-proved sibling lemmas.
Claim. There exists a Debye-frequency certificate consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for all $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 treats the Debye cutoff as a φ-ladder prediction. Classically $\omega_D=c_s(6\pi^2 n)^{1/3}$; Recognition Science claims the Debye-to-Einstein ratio equals $\varphi^{3/D}$, hence $\varphi$ in three spatial dimensions (forcing step T8). Empirically the ratio sits near $1.7$ for FCC metals, within about $0.1$ of $\varphi$.
The certificate structure records the minimal cost-theoretic hygiene needed for that story: a domain cost that is zero at equilibrium (equal mass and energy scales), nonnegative off-diagonal, and a positive canonical threshold against which the Debye scale is compared. Upstream, nonnegativity of recognition cost is the standard $J$-cost fact that any recognition event has $0\le e.\mathrm{cost}$.
proof idea
One-line structure construction. The three fields of DebyeFreqCert are filled by the sibling lemmas domainCost_at_equilibrium, domainCost_nonneg, and canonicalThreshold_pos. No further tactic work; the definition is pure packaging.
why it matters
Gives an inhabited witness that the Debye φ-ladder module meets its cost-interface obligations (module status: structural theorem, zero sorry). Downstream the same module exposes cert_inhabited; no external used-by edges are recorded yet. Ties the Debye/Einstein ratio claim to the broader forcing chain: T5 $J$-uniqueness, T6 $\varphi$ as self-similar fixed point, and T8 $D=3$, under which the predicted ratio collapses to $\varphi$ itself. Does not close the empirical $\sim\varphi+0.1$ gap; it only certifies the cost scaffolding the prediction sits on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.