BAOScaleRS_Exact5Cert
plain-language theorem explainer
Certificate structure packaging three structural facts used for the RS BAO-scale exact-5 claim: diagonal domain cost vanishes off zero, domain cost is nonnegative on positive arguments, and the canonical threshold is positive. Cosmology and foundation auditors cite it when discharging the inhabited BAO certificate. Pure definitional packaging of field obligations; no proof body.
Claim. A BAO-scale RS exact-5 certificate is a record of three properties: (1) for every nonzero real $r$, the domain cost of $(r,r)$ is zero; (2) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (3) the canonical threshold is strictly positive.
background
This module treats the baryon acoustic oscillation (BAO) drag scale in Recognition Science units. Planck reports $r_{\mathrm{drag}} \approx 147.09,\mathrm{Mpc}$; the RS estimate is $\phi^{14}\cdot 0.174,\mathrm{Mpc} \approx 146.7,\mathrm{Mpc}$ (within about $0.3%$). The module status is structural: zero sorry, zero axioms.
Domain cost is the local cost functional on pairs of positive reals used to score scale mismatch; its diagonal vanishing and nonnegativity mirror the global J-cost minimum at identity. Upstream, ObserverForcing records that every recognition-event cost is nonnegative via Jcost_nonneg on a positive state. The canonical threshold is the positive cutoff against which the BAO scale comparison is judged.
The structure does not itself compute the megaparsec number; it only bundles the three positivity and identity obligations that any inhabited certificate must supply.
proof idea
No proof: this is a structure declaration. It names three fields whose types are the mathematical obligations (diagonal cost identity, two-sided nonnegativity of domain cost on the positive orthant, and positivity of the canonical threshold). Downstream, cert fills the fields by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos; cert_inhabited then wraps that instance as Nonempty.
why it matters
Gives a single inhabitable type for the BAO-scale RS exact-5 structural certificate. Downstream cert is the concrete noncomputable instance, and cert_inhabited proves the type is nonempty, closing the module's structural claim.
In the broader framework this sits under Foundation cosmology matching: the eight-tick and $\phi$-ladder apparatus (T6/T7) produce the rung power $\phi^{14}$ that lands near the observed BAO scale when multiplied by the $0.174,\mathrm{Mpc}$ yardstick. The certificate isolates the cost-theoretic side conditions (J-style nonnegativity and identity minimum) so the numerical BAO comparison can be stated against a clean structural interface rather than ad-hoc inequalities.
It does not replace the forcing chain (T0–T8) or the Recognition Composition Law; it only packages the local cost facts needed for this BAO exact-5 session.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.