MatterPert4Cert
plain-language theorem explainer
A certificate packing three structural properties used for the J-cost CMB anisotropy story: diagonal domain cost vanishes, domain cost is nonnegative on positive arguments, and the canonical threshold is positive. Cosmology and RS forcing readers cite it as the interface that `cert` inhabits. There is no proof body; it is a pure structure definition.
Claim. A certificate consists of three facts: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module treats CMB temperature anisotropy as a J-cost effect. The stated target scale is $\Delta T/T \sim 10^{-5}$, compared with the RS estimate $J(\varphi)^{D+1}=J(\varphi)^4\approx 1.94\times 10^{-4}$ (order-of-magnitude match). The local objects are a real bivariate domain cost and a fixed positive canonical threshold used as a comparison scale.
Domain cost is required to vanish on the diagonal (equal nonzero arguments) and to stay nonnegative when both arguments are positive. That nonnegativity pattern mirrors the foundation fact that every recognition-event cost is nonnegative, via $J$-cost nonnegativity on positive states.
The certificate is the Prop-bundle that later definitions must satisfy before any numerical anisotropy claim is attached.
proof idea
No proof: this is a structure declaration. The three fields are pure propositions (diagonal vanishing of domain cost, nonnegativity on positive pairs, positivity of the canonical threshold). Inhabitation is deferred to the sibling cert, which fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
In the MatterPert4 pipeline this structure is the typed gate for the CMB/J-cost story. Downstream, cert builds a concrete inhabitant and cert_inhabited records Nonempty of the certificate, so later lemmas can assume the three structural facts without re-proving them.
Framework-wise it sits under the cosmology reading of J-cost after the forcing chain has fixed $\varphi$ and $D=3$ (so the $J(\varphi)^4$ scale is meaningful). It does not itself compute $\Delta T/T$; it only locks the cost and threshold hygiene that any such comparison needs. Status in the module header is structural (zero sorry, zero axiom) at the certificate layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.