SoundHorizon5Cert
plain-language theorem explainer
Certificate structure bundling three analytic conditions for the CMB sound-horizon derivation: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Cosmologists citing the RS identity r_s = J(φ)·φ^14 Mpc (~147 Mpc) reference this bundle. Pure structure definition; no proof body.
Claim. A sound-horizon certificate is a triple of properties: (i) for every nonzero real $r$, the domain cost satisfies $C(r,r)=0$; (ii) for all positive reals $m,e$, one has $C(m,e)\ge 0$; (iii) the canonical threshold $T$ obeys $T>0$.
background
The module derives the CMB sound horizon from J-cost in Recognition Science units. The observed scale is $r_s\approx 147,\mathrm{Mpc}$. On the $\varphi$-ladder one has $\varphi^{14}\sim 843,\mathrm{Mpc}$, and the ratio $147/843\approx 0.174$ matches $J(\varphi)$, where $J(x)=(x+x^{-1})/2-1$ is the unique nonnegative cost forced by the Recognition Composition Law (T5). The claimed identity is therefore $r_s=J(\varphi)\cdot\varphi^{14},\mathrm{Mpc}$.
Domain cost is the local cost functional on positive scale pairs used in that derivation; the canonical threshold is the positive cutoff against which the cost is compared. Upstream, nonnegativity of recognition cost is already established for events (cost_nonneg: any recognition event has nonnegative cost via Jcost_nonneg). The certificate isolates the three real-analytic facts the sound-horizon argument needs from that cost calculus.
proof idea
No proof: this is a structure declaration. Its three fields are Prop-valued requirements (diagonal vanishing of domain cost, nonnegativity on the positive quadrant, positivity of the canonical threshold). Inhabitation is supplied separately by the definition cert, which fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives a single named type for the analytic hypotheses of the Plan-v7 sound-horizon pass, so downstream lemmas can quantify over one certificate rather than three loose assumptions. Immediate consumers are cert (the canonical inhabitant) and cert_inhabited (Nonempty SoundHorizon5Cert). In the broader framework this sits under the J-uniqueness / RCL strand (T5) and the $\varphi$-ladder mass and length bookkeeping: the numerical match $r_s=J(\varphi)\cdot\varphi^{14},\mathrm{Mpc}$ is the cosmological payoff. The module claims structural status (0 sorry, 0 axiom); the certificate is the interface that keeps those claims modular.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.