cert
plain-language theorem explainer
Packages the three certificate fields for the RS BAO-scale exactness claim: diagonal domain cost vanishes, domain cost is nonnegative on the positive quadrant, and the canonical threshold is positive. Cosmologists matching the drag scale to a phi-ladder length would cite this bundle. The body is a pure structure constructor wiring three already-proved sibling lemmas.
Claim. There is a certificate recording that (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; and (iii) the canonical threshold is strictly positive.
background
The module treats the baryon acoustic oscillation (BAO) drag scale as an RS length on the phi ladder: Planck reports $r_{\mathrm{drag}}\approx 147.09,\mathrm{Mpc}$, while $\varphi^{14}\cdot 0.174,\mathrm{Mpc}\approx 146.7,\mathrm{Mpc}$ (within $0.3%$). The structural claim is that this match sits inside a cost-minimizing recognition geometry rather than an ad-hoc fit.
Domain cost is the local cost functional on pairs of positive reals used to score scale mismatch; its diagonal vanishing and nonnegativity are the usual J-cost axioms specialized to that domain. The canonical threshold is the positive cutoff against which the BAO residual is judged. Upstream, ObserverForcing already records that every recognition-event cost is nonnegative via $J$-cost nonnegativity.
proof idea
One-line structure inhabitant. The three fields of BAOScaleRS_Exact5Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively; no further tactic work.
why it matters
Gives a single named certificate object for the BAO-scale exactness session (module status: structural theorem, zero sorry, zero axiom). Downstream consumers can take the bundle rather than reassemble the three cost/threshold facts. In the broader RS chain this sits under the phi-ladder mass/length bookkeeping (T6 self-similar fixed point, rung arithmetic) and the nonnegativity of recognition cost from the J-uniqueness forcing (T5). No used-by edges are recorded yet; the natural next step is any theorem that quotes the certificate to close the $0.3%$ BAO residual claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.