cert
plain-language theorem explainer
Packages three elementary domain-cost and threshold facts into one inhabited CMB peak-position certificate. Cosmologists citing the RS acoustic-peak ladder (ℓ₁≈220, ℓ₂≈540, ℓ₃≈800 and their φ-power ratios) use this object as the formal witness that the cost model is well-posed. The definition is a pure structure instance wiring three preexisting lemmas; no new mathematics is proved.
Claim. There exists 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 treats CMB acoustic-peak multipoles under Recognition Science: observed ratios $\ell_2/\ell_1\approx 2.45\sim\varphi^2$ and $\ell_3/\ell_1\approx 3.64\sim\varphi^{2.8}$ are read as $\varphi$-power spacing on the recognition ladder. Status is structural (zero sorry, zero axiom).
domainCost is the local cost functional on positive reals used to score peak-position mismatches; its diagonal vanishing and nonnegativity are the minimal well-posedness conditions inherited from the global J-cost $J(x)=(x+x^{-1})/2-1$. The upstream fact cost_nonneg records that every recognition event has nonnegative cost via Jcost_nonneg.
canonicalThreshold is the positive cutoff against which domain cost is compared when declaring a multipole an admissible peak. The certificate structure CMBPeakPos_v3Cert simply bundles the three Prop-valued obligations that any such cost model must discharge.
proof idea
One-line structure instance. The three fields of CMBPeakPos_v3Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No tactic proof and no new reduction; the definition is pure packaging.
why it matters
Gives the module a single named witness that the cost side of the CMB peak-position story is inhabited and coherent. Downstream consumers (e.g. cert_inhabited and any later peak-ratio theorems) can quote cert rather than re-assemble the three obligations. In the broader RS chain this sits under the cosmology layer that reads acoustic-peak spacing as $\varphi$-ladder structure, consistent with T6 ($\varphi$ as self-similar fixed point) and the eight-tick octave motif, though the present declaration itself only certifies cost well-posedness, not the numerical peak ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.