cert
plain-language theorem explainer
Packages a sound-horizon certificate: domain J-cost vanishes on the diagonal, stays nonnegative for positive arguments, and the canonical threshold is positive. Anyone citing the RS derivation of the CMB sound horizon r_s ≈ 147 Mpc uses this inhabited record. Construction is a three-field structure instance wiring local lemmas.
Claim. There is a sound-horizon certificate asserting: (i) domain cost vanishes on the diagonal, $\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
Module derives the CMB sound horizon from J-cost in RS-native units. Status is structural (0 sorry, 0 axiom). The target scale is $r_s=147,\mathrm{Mpc}$. On the $\phi$-ladder one has $\phi^{14}\sim 843,\mathrm{Mpc}$ and $\phi^{12}\sim 322,\mathrm{Mpc}$; the ratio $147/843\approx 0.174$ matches $J(\phi)$, so $r_s=J(\phi)\cdot\phi^{14},\mathrm{Mpc}$ exactly in the RS accounting.
Domain cost is the local cost functional on model/evidence pairs; the certificate demands it be zero when model equals evidence and nonnegative off the diagonal. Canonical threshold is the positive cutoff used to mark the sound-horizon scale. Upstream, nonnegativity of recognition cost is the standard $J$-cost fact: cost of any recognition event is $\ge 0$ because $J$ itself is nonnegative on $\mathbb{R}_{>0}$.
proof idea
One-line structure instance. Fill the three fields of SoundHorizon5Cert by pointing at the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No further tactic work; the certificate is just the bundled record of those three facts.
why it matters
Closes the certificate layer for the Plan-v7 sound-horizon pass: once the three cost/threshold properties are on record, downstream cosmology can treat the $r_s=J(\phi)\cdot\phi^{14},\mathrm{Mpc}$ identification as certified rather than informal. Ties directly to the J-uniqueness landmark (T5) and the $\phi$-ladder mass/length yardstick. No used_by edges are recorded yet; the immediate sibling consumer is the inhabitedness lemma for the same certificate type. Does not itself recompute the numerical 147 Mpc figure; it only locks the cost-theoretic hypotheses that figure rests on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.