CMBDampingScale_v3Cert
plain-language theorem explainer
Certificate structure bundling three algebraic conditions for the RS CMB damping-scale claim: diagonal vanishing of the domain cost, its non-negativity on positive arguments, and positivity of the canonical threshold. Cosmology code that places the damping multipole between φ^15 and φ^16 cites the inhabited instance. Pure Prop bundle with no proof body.
Claim. A certificate is a triple of properties: (i) for every nonzero real $r$, the domain cost vanishes on the diagonal, $\mathrm{cost}(r,r)=0$; (ii) for all positive reals $m,e$, the domain cost is nonnegative, $\mathrm{cost}(m,e)\ge 0$; (iii) the canonical threshold is strictly positive.
background
Module setting (CMB damping scale v3): the observed Silk-damping multipole sits near $\ell_D\sim 1500$–$2000$. Recognition Science places it on the $\varphi$-ladder between $\varphi^{15}\approx 1364$ and $\varphi^{16}\approx 2207$, so the structural claim is that a positive threshold and a nonnegative recognition cost pin $\ell_D$ inside that band.
The domain cost is the local cost functional on mass/energy-like arguments (built from the J-cost of Recognition Science). Upstream, cost_nonneg records that every recognition event has nonnegative cost via $J$-cost nonnegativity: “The cost of any recognition event is non-negative.” The canonical threshold is the positive cutoff used to mark the damping scale in RS-native units.
This structure does not compute $\ell_D$; it packages the three inequalities the rest of the module needs before asserting the $\varphi^{15}$–$\varphi^{16}$ placement.
proof idea
No proof body: the declaration is a structure (Prop bundle). Inhabitation is discharged downstream by the concrete witness cert, which fills the three fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. Those sibling lemmas are the actual algebraic work; this type only names the interface.
why it matters
Gives the typed interface that cert and cert_inhabited satisfy, so the module can export a zero-sorry structural theorem for the CMB damping scale. Downstream, cert assembles the three field proofs and cert_inhabited shows the certificate type is nonempty.
In the RS forcing picture this sits under the $\varphi$-ladder mass/scale bookkeeping (T6 self-similar fixed point) rather than under T5–T8 uniqueness itself: it constrains where Silk damping lands once $J$-cost nonnegativity and a positive threshold are granted. It does not close open observational questions about the precise $\ell_D$ centroid; it only certifies the algebraic side conditions the v3 writeup treats as structural.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.