Pith. sign in
module module moderate

IndisputableMonolith.Cosmology.RS_COS_Structural_003

show as:
view Lean formalization →

Module packaging the structural certificate for RS cosmology claim 003: a nonnegative domain cost built from the RS J-cost, a positive canonical threshold, and an inhabited certificate record tying them together. Cosmologists and auditors of the RS forcing chain cite it when checking that domain-level cost bounds sit above a fixed positive cutoff. The module is mostly definitions plus elementary nonnegativity and positivity lemmas, not a deep existence proof.

claimDefine a domain cost $C$ from the RS cost functional $J$, prove $C \ge 0$ and an evaluation identity, fix a canonical threshold $\theta > 0$, and package an inhabited certificate record asserting these structural facts for cosmology claim RS-COS-Structural-003.

background

Recognition Science measures mismatch with the unique cost $J(x) = (x + x^{-1})/2 - 1$ (equivalently $\cosh(\log x) - 1$), forced at T5 of the unified chain. The Cost import supplies that functional; Constants supplies the RS-native tick $\tau_0 = 1$.

In the cosmology layer, one lifts $J$ to a domain-level cost on cosmological patches or recognition domains. The module introduces that lift (domainCost), records that it is nonnegative, and fixes a positive canonical threshold against which domain costs are compared. The local setting is structural bookkeeping for claim 003, not a full dynamical cosmology derivation.

Upstream material is thin: only the Constants and Cost modules. No deeper forcing-chain lemmas are imported here; the certificate is self-contained once $J$ and the tick unit are available.

proof idea

Definition-first module. domainCost is introduced as a real-valued cost on domains; domainCost_at_eq and domainCost_nonneg are short algebraic or direct inequalities from nonnegativity of $J$. canonicalThreshold is a fixed positive real; canonicalThreshold_pos is the positivity witness. RSCOSStructural003Cert (with cert / cert_inhabited) assembles these facts into an inhabited certificate record. No multi-step tactic proof or external lemma chain beyond Cost/Constants.

why it matters in Recognition Science

Gives the structural certificate object for RS-COS-Structural-003 so downstream cosmology pages can assume a nonnegative domain cost and a positive cutoff without re-proving elementary $J$-facts. Used_by is currently empty in the graph, so this module is a leaf certificate rather than an intermediate lemma feeding a named parent theorem. It sits in the cosmology domain of the RS mirror and supports audit of cost-threshold structure consistent with the J-uniqueness (T5) and RS-native units, without yet closing dynamical claims (expansion history, horizon counts, or mass-ladder cosmology).

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)