Pith. sign in
module module moderate

IndisputableMonolith.Cosmology.RecombinationRedshift3_FromJCost

show as:
view Lean formalization →

Module packaging a J-cost certificate that the cosmological recombination redshift sits at three in RS-native units. Cosmologists and RS auditors cite it when tying the last-scattering epoch to the cost functional rather than to a fitted ΛCDM parameter. The argument is definitional: a nonnegative domain cost, a positive canonical threshold, and an inhabited certificate record.

claimIn RS-native units, a domain cost $C$ built from the J-cost is nonnegative, a canonical threshold $\theta>0$ is fixed, and a recombination certificate asserts that the recombination redshift equals $3$ once $C$ meets $\theta$.

background

Recognition Science measures mismatch by the J-cost $J(x)=(x+x^{-1})/2-1$, the unique symmetric cost forced by the Recognition Composition Law. The Cost import supplies that functional; Constants supplies the RS time quantum $\tau_0=1$ tick against which cosmological epochs are counted.

This module sits in the Cosmology domain and treats recombination (last scattering) as a cost-threshold crossing rather than as an empirical fit. Sibling definitions introduce a domain cost, prove it equals its pointwise evaluation and is nonnegative, fix a positive canonical threshold, and package the claim that recombination occurs at redshift three into a certificate type with an inhabitation witness.

proof idea

Definition-and-certificate module, not a deep derivation. It defines a domain cost from J, records elementary facts (evaluation identity, nonnegativity, positivity of the canonical threshold), then exposes a Recombin3Cert structure and a concrete inhabited certificate. No multi-step forcing chain runs inside the file; the mathematical content is the packaging of the $z=3$ claim against those cost primitives.

why it matters in Recognition Science

Gives the Cosmology layer a named, checkable handle on recombination at redshift three tied to J-cost rather than to free ΛCDM parameters. Downstream pages can import the certificate instead of restating the threshold story. In the broader RS landmarks this is an applied cosmology binding of the T5 J-uniqueness cost, not a step of the T0–T8 forcing chain itself. No parent theorems are listed in the use-graph yet; the module is a leaf certificate source for later cosmological assemblies.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)