cert
plain-language theorem explainer
Packages three elementary properties of the matter-perturbation domain cost into a single certificate: diagonal vanishing, non-negativity for positive mass/energy, and positivity of the canonical threshold. Cosmologists citing the RS CMB anisotropy bound (J(φ)^4 ∼ 2×10^{-4}) use this as the structural witness. The body is a pure structure assembly of three sibling lemmas.
Claim. There exists a certificate recording that the domain cost $C$ satisfies $C(r,r)=0$ for all $r\neq 0$, that $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical threshold $T_*$ is strictly positive.
background
The module develops a structural account of CMB temperature anisotropy from the Recognition Science J-cost. In RS units the leading scale is $J(\varphi)^{D+1}=J(\varphi)^4\approx 1.94\times 10^{-4}$, within an order of magnitude of the observed $\Delta T/T\sim 10^{-5}$.
Domain cost is the local cost functional on mass/energy pairs used to bound matter perturbations. The certificate structure demands three facts: the cost vanishes on the diagonal (equal arguments), stays non-negative for positive inputs, and the canonical threshold against which perturbations are compared is positive. Upstream, non-negativity of recognition-event cost follows from non-negativity of $J$ on positive reals.
proof idea
One-line structure constructor. It fills the three fields of MatterPert4Cert by pointing at the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No new arithmetic is performed.
why it matters
Gives the module a single named witness that the domain-cost side conditions hold, so downstream CMB or matter-power arguments can assume the certificate rather than re-prove diagonal vanishing and positivity. Fits the Plan v7 structural theorem line (0 sorry, 0 axiom) for anisotropy from J-cost. Lands next to the forcing-chain landmarks T5 (J-uniqueness) and T8 ($D=3$), since the quoted scale is $J(\varphi)^{D+1}=J(\varphi)^4$. No downstream consumers are wired yet; the inhabited instance is the immediate sibling use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.