Pith. sign in
module module high

IndisputableMonolith.Cosmology.CosmicZScaleLaw

show as:
view Lean formalization →

Defines the cosmological scale factor a(z) and the scale-affine law linking integrated cosmic Z-complexity to expansion. Under that law the normalized Z-ratio equals a(z), so dark-energy equation-of-state deviations fall as 1/(1+z). Cited by the U5 dark-energy reduction that tightens residual freedom in w(z). The forcing is algebraic: affinity plus positivity and normalization of a pin the identity map.

claimIntroduce the scale factor $a(z)$ with $a(0)=1$ and $0<a(z)\le 1$. A scale-affine Z-law is a relation forcing the integrated cosmic Z-complexity $Z(z)$ to transform affinely with $a$. Any such law implies $Z(z)/Z(0)=a(z)$, and therefore the dark-energy deviation satisfies $\delta w(z)=\delta w_0/(1+z)$.

background

Recognition Science cosmology reduces the dark-energy equation of state via the BIT mechanism: $w(z)=-1+\delta w\cdot Z(z)/Z_{\mathrm{today}}$, where $Z(z)$ is the integrated cosmic Z-complexity at redshift $z$ and $Z_{\mathrm{today}}=Z(0)$. That form still leaves how $Z$ tracks the expansion history open; this module closes that gap.

The scale factor $a(z)$ is the usual FLRW expansion variable, normalized so $a(0)=1$ today and constrained to $0<a(z)\le 1$ in the past. A scale-affine Z-law asserts that $Z$ is an affine function of $a$ (or of a fixed function of $a$). The module also records the elementary positivity and bound lemmas needed to turn affinity into an identity.

Upstream, CosmicZHistory supplies the $w(z)$ skeleton and the meaning of $Z(z)$. Constants and Cost supply the RS-native units and J-cost background used elsewhere in the cosmology stack, but the local argument is kinematic rather than cost-theoretic.

proof idea

The module is a short definition-plus-forcing package, not a single deep theorem. It first defines $a(z)$ and proves the normalization $a(0)=1$, positivity, and the bound $a\le 1$. It then packages the scale-affine hypothesis as a named predicate on candidate $Z$-maps.

From that predicate, a sequence of lemmas forces the only admissible normalized map to be the identity: $Z(z)/Z_{\mathrm{today}}=a(z)$. Intermediate steps isolate the linear-in-$Z$ consequence, the vanishing of any constant offset (canonical kernel), and the matching of the canonical deviation. A certificate aggregates the chain for downstream import.

No external analytic machinery is required; the argument is equational once affinity and the boundary conditions on $a$ are granted.

why it matters in Recognition Science

This module is the kinematic hinge of the U5 dark-energy reduction. Downstream, DarkEnergyScaleAffinityDerivation imports it and records the tightened residue: scale-affinity implies $Z(z)/Z_{\mathrm{today}}=a(z)$, which immediately yields $\delta w(z)=\delta w_0/(1+z)$. That is the concrete observational shape left after BIT has fixed the overall $w=-1+\cdots$ skeleton.

Without the identity $Z/Z_{\mathrm{today}}=a$, the redshift dependence of $\delta w$ would remain free. The module therefore converts an abstract affinity hypothesis into a sharp, falsifiable $1/(1+z)$ law. It sits in the cosmology domain of the Recognition stack and does not itself touch the T0–T8 forcing chain, the RCL, or the mass ladder; its role is purely to lock the expansion-history side of dark energy.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (13)