cert
plain-language theorem explainer
Packages three elementary J-cost facts into a CMB E-mode polarization certificate: diagonal domain cost vanishes, cost is nonnegative on positive arguments, and the canonical threshold is positive. Cosmology readers cite it as the inhabited witness that the structural side conditions for the E/T ratio story hold. The body is a three-field structure literal wiring preexisting lemmas.
Claim. There is a certificate asserting: (i) for every nonzero real $r$, the domain cost of $(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 E-mode polarization as a structural consequence of the Recognition Science J-cost. Observationally, E-mode power is about 10% of temperature anisotropy; the RS sketch identifies the E/T ratio with $J(\varphi)$ (order 12%), or a nearby algebraic combination of $J(\varphi)$ and $\varphi$, as a consistency check rather than a fitted parameter.
Domain cost is the local cost functional on pairs of positive reals used in this cosmology layer; it inherits nonnegativity from the global recognition cost $J$, whose minimum is at the identity ratio $x=1$. The structure CMBPolar3Cert is the bundle of three side conditions needed before any threshold comparison or ratio claim: vanishing on the diagonal, nonnegativity off-diagonal, and a positive canonical threshold.
Upstream, cost_nonneg in ObserverForcing records that every recognition event has nonnegative cost via Jcost_nonneg at positive state.
proof idea
One-line structure construction. Fill the three fields of the certificate by pointing at the in-module lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No new algebra; the definition is pure packaging.
why it matters
Gives an inhabited witness that the structural hypotheses for the CMB E-mode-from-J-cost story are satisfied, matching the module claim of a structural theorem with zero sorry and zero axiom. It sits under the broader RS forcing picture where $J$ is the unique cost (T5) and $\varphi$ is the self-similar fixed point (T6), so dimensionless polarization ratios are forced rather than fitted. No downstream consumers are recorded yet; the immediate sibling use is inhabitation of the certificate type. The numerical E/T match (~10% vs $J(\varphi)$) remains interpretive commentary in the module doc, not a proved equality inside this definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.