IndisputableMonolith.Cosmology.RS_Cosmo_Module_004
Cosmology module 004 packages a domain-level cost functional, its nonnegativity, and a positive canonical threshold into a single inhabited certificate. Cosmologists working in the RS ledger cite it when they need a uniform cost bound on spatial domains before assembling larger expansion or horizon arguments. The module is mostly definitional: it wires Cost and Constants into named lemmas and wraps them as RSCosmo004Cert.
claimOn RS-native units, a domain cost $C(\Omega)\ge 0$ is defined from the $J$-cost, together with a canonical threshold $\theta>0$. The module asserts the package $\mathrm{RSCosmo004Cert}$: nonnegativity of $C$, positivity of $\theta$, and an equality relating the pointwise evaluation of $C$ to the underlying cost data.
background
Recognition Science measures mismatch by the $J$-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by the Recognition Composition Law. The Cost import supplies that functional and its elementary inequalities; Constants supplies the RS time quantum $\tau_0=1$ tick and the golden-ratio ladder used elsewhere in the cosmology stack.
Module 004 lifts the pointwise cost to a domain cost $C(\Omega)$ on spatial regions relevant to cosmological bookkeeping (horizon patches, causal diamonds, or ledger cells). It also fixes a canonical threshold $\theta>0$ against which domain costs are compared when deciding whether a region is "cheap" or "expensive" in the RS sense.
The local setting is pure scaffolding for later cosmology theorems: no FLRW dynamics or observational fits live here, only the cost/threshold interface those results will call.
proof idea
Definition-heavy module, not a single deep proof. domainCost is introduced from the Cost layer; domainCost_at_eq records the evaluation identity; domainCost_nonneg is the nonnegativity lemma inherited from $J\ge 0$. canonicalThreshold and canonicalThreshold_pos pin a strictly positive cutoff. The certificate type RSCosmo004Cert bundles those facts; cert and cert_inhabited exhibit a concrete inhabitant so downstream files can assume the package without re-proving the elementary inequalities.
why it matters in Recognition Science
In the RS cosmology tower, every expansion, horizon, or structure-formation argument eventually needs a uniform lower/upper control on domain mismatch. This module is the named gate for that control: nonnegativity of domain cost and a positive canonical threshold. Downstream used-by edges are empty in the current graph, so the module presently stands as an interface certificate rather than a leaf of a proved parent theorem. It sits downstream of Cost and Constants and upstream of any later cosmology result that must quote a domain-cost bound before invoking eight-tick or $\phi$-ladder structure (T6–T7 landmarks). Closing larger cosmology claims will discharge or consume RSCosmo004Cert rather than re-derive $J\ge 0$ locally.
scope and limits
- Does not derive FLRW equations, scale-factor dynamics, or observational cosmology fits.
- Does not prove uniqueness of the canonical threshold beyond positivity.
- Does not connect domain cost to mass-ladder rungs or $\alpha$ bounds.
- Does not assert any theorem about horizons, dark energy, or CMB observables.
- Does not discharge sorry-free parent cosmology theorems; used_by is currently empty.