IndisputableMonolith.Cosmology.SoundHorizon5
Module packaging a Recognition-Science sound-horizon certificate at the five-tick scale: a nonnegative domain cost, a positive canonical threshold, and an inhabited certificate record. Cosmologists matching RS early-universe scales to the acoustic horizon would cite it. Content is mostly definitions and elementary positivity/equality lemmas, not a deep derivation.
claimIntroduce a domain cost $C$ on the relevant scale variable, prove $C \ge 0$ and an evaluation identity, fix a canonical threshold $\theta > 0$, and package these into an inhabited sound-horizon certificate $\mathrm{SoundHorizon5Cert}$ at the five-related RS scale.
background
Recognition Science works in RS-native units built from the tick $\tau_0$ and the cost functional $J$ (from the Cost import; $J(x)=(x+x^{-1})/2-1$). Cosmology modules translate those primitives into early-universe length and time scales.
The sound horizon is the comoving distance a sound wave travels before recombination; here the module specializes to a five-related discrete scale (naming and certificate tag), not a full FLRW integral. domainCost is the local cost assigned on that domain; canonicalThreshold is the positive cutoff used to mark the horizon edge.
Constants supplies the RS time quantum and related fixed numbers; Cost supplies the $J$-cost infrastructure against which nonnegativity is checked.
proof idea
Definition-heavy module. domainCost and canonicalThreshold are introduced as defs; domainCost_nonneg and canonicalThreshold_pos are short nonnegativity/positivity lemmas; domainCost_at_eq is an evaluation identity. SoundHorizon5Cert is a structure bundling those pieces, with cert and cert_inhabited witnessing a concrete instance. No long tactic scripts or forcing-chain appeals appear at module scope.
why it matters in Recognition Science
Gives Cosmology a named, checkable five-scale sound-horizon certificate so later BAO/CMB comparison lemmas can cite a single inhabited record rather than ad-hoc inequalities. Sits downstream of Constants and Cost only; the supplied graph shows no further used-by edges yet, so it is a leaf certificate module awaiting consumers in the broader RS cosmology stack (acoustic scale, rung matching, or $\phi$-ladder mass/time conversions). It does not itself close T0–T8 or the RCL identity.
scope and limits
- Does not derive the classical FLRW sound-horizon integral or recombination physics.
- Does not prove numerical equality to observed $r_s$ or BAO scales.
- Does not force $D=3$, $\phi$, or eight-tick structure (those live upstream).
- Does not supply a used-by consumer theorem in the current graph.
- Does not claim a unique threshold beyond the packaged canonical choice.