cert
plain-language theorem explainer
Packages three structural facts about the domain cost into a single CMB polarization-ratio certificate: diagonal vanishing, non-negativity on positive arguments, and a strictly positive canonical threshold. Cosmology users cite it when assembling the RS B/E-mode claim. The body is a structure instance that wires three sibling 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 the CMB E/B polarization ratio as a structural consequence of the Recognition Science J-cost. In RS the ratio is written $B/E = r/(8 J(\varphi))$, with $r$ the tensor-to-scalar ratio; at the benchmark $r = 0.017$ one obtains $B/E \approx 1.8%$, so E-modes dominate and B-modes arise only from primordial gravitational waves.
The certificate structure collects three elementary properties of a domain cost built from the J-cost: it vanishes on the diagonal away from zero, stays nonnegative for positive mass/energy-like arguments, and sits above a positive threshold. Upstream, non-negativity of recognition cost is already known: every recognition event has cost $\ge 0$ because $J$ is nonnegative on the positive reals.
Local siblings supply the concrete domain-cost identity, its non-negativity lemma, and positivity of the canonical threshold; this definition merely bundles them.
proof idea
One-line structure instance. The three fields of CMBPolarRatio3Cert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (non-negativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No new calculation occurs; the definition is pure packaging.
why it matters
Gives a single inhabited certificate object for the structural CMB E/B claim of the module (status: structural theorem, zero sorry). Downstream consumers can depend on one name rather than three separate lemmas when stating that the RS formula $B/E = r/(8 J(\varphi))$ is well-posed under the J-cost axioms. It sits in the cosmology layer that imports Constants and Cost, and inherits non-negativity from the ObserverForcing cost theorem. No further used-by edges are recorded yet; the immediate role is to discharge the certificate interface for the polarization-ratio narrative and for cert_inhabited.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.