Pith. sign in
module module moderate

IndisputableMonolith.Cosmology.DarkEnergyScaleAffinityDerivation

show as:
view Lean formalization →

Derives the lower admissibility condition for the scale-affine cosmic-Z law: with only the early endpoint a=0 and today a=1 fixed, a normalized ledger fraction cannot pick a nonlinear scale coordinate without extra structure, so endpoint interpolation is forced. Cosmologists working the dark-energy residual cite it when reducing free shape in δw(z). The argument is a chain of no-hidden-coordinate lemmas into a certificate.

claimIf a normalized ledger fraction on the scale factor has no hidden scale coordinate beyond the endpoints $a=0$ and $a=1$, then its induced map is scale-affine: it preserves endpoint interpolation and yields a linear relation in the cosmic $Z$-coordinate, so the dark-energy residual takes the form $\delta w(z)=\delta w_0\cdot Z(z)/Z_{\mathrm{today}}$.

background

The parent setting is the cosmic $Z$ scale law: under the BIT kernel, the dark-energy equation-of-state residual is forced into the shape $\delta w(z)=\delta w_0\cdot Z(z)/Z_{\mathrm{today}}$. That module still leaves a last shape residue: which coordinates on the expansion history are admissible once only the early and late endpoints are fixed.

This module isolates the lower admissibility condition behind that scale-affine $Z$ law. A "no hidden scale coordinate" hypothesis means the normalized ledger fraction is not allowed an extra nonlinear reparameterization of the scale factor beyond the two endpoints $a=0$ (early) and $a=1$ (today). Without that extra structure, the only remaining freedom is endpoint interpolation.

Sibling objects package the hypothesis, the forced identity and linear-$Z$ maps, the canonical kernel and deviation forms, and a derivation certificate that records the implication chain.

proof idea

Not a single theorem: a small derivation stack. The core hypothesis is the no-hidden-scale-coordinate condition. From it the module proves successive strengthenings: the map is scale-affine, then the identity on the normalized interval, then linearity in the cosmic $Z$ coordinate, then the canonical deviation and kernel forms. A canonical instance of the hypothesis is shown to land on the canonical affine map. The stack closes with a certificate object that packages the derivation for downstream cosmology proofs.

why it matters in Recognition Science

Closes the lower half of the dark-energy plan's last shape residue. Upstream, CosmicZScaleLaw already forces $\delta w(z)\propto Z(z)/Z_{\mathrm{today}}$ under the BIT kernel; this module justifies why the coordinate on that residual must stay scale-affine once only $a=0$ and $a=1$ are given. No downstream edges are recorded yet, so the immediate consumers are the certificate and the scale-affine $Z$-law statements in the same cosmology layer. In Recognition terms it is bookkeeping on admissible ledger fractions, not a new forcing step in T0–T8, but it keeps the dark-energy residual free of smuggled nonlinear gauges.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (10)