cert
plain-language theorem explainer
Packages three structural facts about the RS domain cost and the canonical threshold into a single CMB damping-scale certificate. Cosmologists citing the v3 claim that the damping multipole sits between φ^15 and φ^16 would point here. The definition is a pure structure assembly: three sibling lemmas are plugged into the certificate fields.
Claim. There is a certificate asserting: (i) the domain cost of any nonzero real against itself vanishes; (ii) for positive mass and energy the domain cost is nonnegative; (iii) the canonical threshold is strictly positive. Together these certify the structural side of the RS CMB damping-scale statement $l_D \sim \varphi^{15}$–$\varphi^{16}$.
background
The module treats the CMB photon-diffusion (Silk) damping scale in Recognition Science units. Observationally $l_D$ lies near 1500–2000. RS places it on the $\varphi$-ladder: $\varphi^{15}\approx 1364$ and $\varphi^{16}\approx 2207$, so the predicted window is $\varphi^{15}$ to $\varphi^{16}$.
Domain cost is the local cost functional on mass/energy pairs used in this cosmology layer; the certificate demands it vanish on the diagonal (equal nonzero arguments) and stay nonnegative for positive inputs. The canonical threshold is the positive cutoff against which the damping scale is compared. Upstream, nonnegativity of recognition cost is the standard $J$-cost fact from ObserverForcing: any recognition event has cost $\ge 0$.
proof idea
Pure structure construction, not a tactic proof. The three fields of CMBDampingScale_v3Cert are filled by the in-module lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No further rewriting or arithmetic is performed.
why it matters
Gives an inhabited, sorry-free certificate that the structural hypotheses of the v3 CMB damping-scale claim hold. The module status line marks this as a structural theorem (0 sorry, 0 axiom) supporting the RS prediction that $l_D$ sits between $\varphi^{15}$ and $\varphi^{16}$, consistent with the observed 1500–2000 multipole band. It sits in the cosmology layer that ties ladder rungs to CMB observables; the golden ratio $\varphi$ is the T6 fixed point of the forcing chain. No downstream consumers are recorded yet; the sibling cert_inhabited is the natural next witness that the type is nonempty.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.