Pith. sign in
module module moderate

IndisputableMonolith.Cosmology.DarkEnergyScaleAffinityDerivation

show as:
view Lean formalization →

Module deriving the lower admissibility condition for scale-affine redshift laws in dark energy. With only endpoints a=0 and a=1 fixed, a normalized ledger fraction cannot adopt a nonlinear coordinate without extra structure, so it must preserve endpoint interpolation. Cosmologists citing the BIT-kernel dark-energy plan use this to force linear Z-scaling. The argument proceeds by encoding a no-hidden-scale hypothesis and discharging identity, linearity, and canonical-kernel consequences.

claimIf a normalized ledger fraction on the cosmic scale factor has only the early endpoint $a=0$ and the present endpoint $a=1$ available, and admits no hidden scale coordinate, then it is scale-affine: it preserves endpoint interpolation. Consequently the deviation and kernel are forced into the canonical linear form in the redshift coordinate $Z$, yielding $\delta w(z)=\delta w_0\cdot Z(z)/Z_{\mathrm{today}}$ under the BIT kernel.

background

Recognition Science cosmology treats dark-energy equation-of-state deviations as ledger fractions on the cosmic scale factor $a$. The parent module CosmicZScaleLaw tightens the last shape residue in that plan: under the BIT kernel, CosmicZHistory asserts $\delta w(z)=\delta w_0\cdot Z(z)/Z_{\mathrm{today}}$.

The present module supplies the lower admissibility condition behind that scale-affine $Z$-law. A "no hidden scale coordinate" hypothesis says that, given only the early endpoint $a=0$ and today $a=1$, the normalized fraction cannot introduce an extra nonlinear reparameterization without adding structure beyond the ledger. Endpoint interpolation is therefore forced.

Sibling declarations package this as a certificate: maps from the no-hidden hypothesis to scale-affinity, identity on the coordinate, linear $Z$, and the canonical deviation/kernel forms.

proof idea

The module is theorem-bearing, not a pure definition file. It introduces a NoHiddenScaleCoordinate predicate and a canonical instance, then proves a chain of forcing lemmas: no-hidden implies scale-affine; forces the identity coordinate; forces linear $Z$; forces the canonical deviation and kernel. A final ScaleAffinityDerivationCert bundles the chain for downstream discharge. Proofs are algebraic reductions from the two-endpoint normalization plus the absence of extra scale structure, feeding the BIT-kernel identity already established upstream in CosmicZScaleLaw.

why it matters in Recognition Science

This module closes the admissibility gap under the dark-energy shape plan: without it, the linear $Z$-scaling $\delta w(z)\propto Z(z)$ would rest on an unstated coordinate choice. It sits directly under CosmicZScaleLaw and supplies the lower condition for ScaleAffineZLaw. In the broader RS forcing picture it is a local rigidity statement (two endpoints, no hidden scale), analogous in spirit to the uniqueness steps that fix $J$ and $\varphi$ in the foundation chain, though confined to cosmic ledger fractions. Downstream consumers are certificates and history theorems that quote the canonical kernel; used_by is currently empty at the module edge, so the immediate parent is the imported CosmicZScaleLaw plan.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (10)