cert
plain-language theorem explainer
Packages three elementary domain-cost facts into a single CMB acoustic-ratio certificate: the cost vanishes on the diagonal, stays non-negative for positive arguments, and the canonical threshold is positive. Anyone citing the φ-ladder structural account of CMB peak ratios (l₂/l₁≈φ^{2.2}, l₃/l₁≈φ^{2.8}) would reach for this bundle. The body is a pure structure constructor wiring three already-proved lemmas.
Claim. There is a certificate asserting that the domain cost $C$ satisfies $C(r,r)=0$ for every $r\neq 0$, that $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical threshold $T$ obeys $T>0$.
background
The module treats CMB acoustic multipoles $l_1\approx 220$, $l_2\approx 540$, $l_3\approx 800$ as clustering near φ-power ratios: $l_2/l_1\approx 2.45\approx\varphi^{2.2}$ and $l_3/l_1\approx 3.64\approx\varphi^{2.8}$. Status is structural (zero sorry, zero axiom).
The certificate structure packages three cost axioms used by that account. Domain cost is the local cost functional on positive reals (built from the Recognition J-cost). The first field requires vanishing on the diagonal $C(r,r)=0$; the second requires non-negativity for positive arguments; the third requires a strictly positive canonical threshold against which ratios are scored.
Upstream, ObserverForcing already records that every recognition-event cost is non-negative via $J$-cost non-negativity. The in-module lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos specialize that picture to the CMB domain cost and threshold.
proof idea
Pure structure inhabitation. The three fields of the certificate are filled by the three sibling lemmas: diagonal vanishing by the domain-cost identity lemma, non-negativity by the domain-cost non-negativity lemma, and threshold positivity by the canonical-threshold positivity lemma. No extra algebra or tactics.
why it matters
Gives a single named inhabitant of the CMB acoustic-ratio certificate so downstream φ-ladder arguments can assume the cost package by name rather than re-proving the three elementary facts. The module frames this as part of the structural theorem that acoustic peak ratios sit near φ-powers (Plan v7 ninety-second pass). It sits downstream of the J-cost non-negativity fact from ObserverForcing and of T5/T6 forcing of $J$ and $\varphi$, but does not itself derive the numerical multipole ratios. No used-by edges are recorded yet; the immediate sibling cert_inhabited is the natural consumer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.