ScaleAffineZLaw
plain-language theorem explainer
A scale-affine Z-law is a normalized cosmic-Z fraction of the scale factor that preserves convex interpolation from the early endpoint a=0 to today a=1. Cosmologists deriving the forced dark-energy shape δw(z)=δw₀/(1+z) cite this structure as the named ledger-admissibility hypothesis. It is a pure structure definition: two endpoint axioms plus the affine-interpolation field; uniqueness of the identity map is proved downstream.
Claim. A scale-affine Z-law consists of a real map $Z_{\mathrm{frac}}$ on the scale factor together with $Z_{\mathrm{frac}}(0)=0$, $Z_{\mathrm{frac}}(1)=1$, and the ledger-uniformity condition that for every real $a$, $Z_{\mathrm{frac}}((1-a)\cdot 0+a\cdot 1)=(1-a)\,Z_{\mathrm{frac}}(0)+a\,Z_{\mathrm{frac}}(1)$.
background
The module closes the last shape residue in the dark-energy plan. Under the BIT kernel, CosmicZHistory already gives $\delta w(z)=\delta w_0\cdot Z(z)/Z_{\mathrm{today}}$, so the dark-energy shape is exactly the normalized cosmic-Z history. The open question is why that normalized history should equal the scale factor $a(z)=1/(1+z)$.
Scale factor here is the usual FLRW coordinate with $a=0$ at the early zero-complexity endpoint and $a=1$ today. The ledger language comes from the foundation layer: a ledger is a double-entry collection of recognition events, and the identity event sits at the J-cost minimum. The scale-affine condition is the statement that equal scale-factor fractions carry equal recognition-ledger fractions along the cosmic interval, with no intermediate coordinate selected before a new physical input is supplied.
Formally the affinity field is convex interpolation between the two endpoints. It is an admissibility law, not a curve fit.
proof idea
No proof body: this is a structure definition. Four fields package the admissibility class. Zfrac is the normalized Z-fraction as a map on scale factor. early_zero and today_one fix the endpoints $Z_{\mathrm{frac}}(0)=0$ and $Z_{\mathrm{frac}}(1)=1$. The field scale_affine_from_early_to_today asserts that $Z_{\mathrm{frac}}$ preserves the affine combination $(1-a)\cdot 0+a\cdot 1$ between those endpoints. Downstream theorems discharge uniqueness by substituting the endpoints into that identity.
why it matters
This structure is the named hypothesis that forces the canonical dark-energy shape. Downstream, scaleAffine_forces_identity shows every such law has $Z_{\mathrm{frac}}(a)=a$; scaleAffine_forces_linearZ lifts that to $Z(z)=Z_{\mathrm{today}}/(1+z)$; and scaleAffine_forces_canonical_deviation / scaleAffine_forces_canonical_kernel give $\delta w(z)=\delta w_0/(1+z)$ and $w(z)=-1+\delta w_0/(1+z)$. The certificate CosmicZScaleLawCert packages both identity and redshift-history forcing. canonicalScaleAffineZLaw witnesses that the class is inhabited (the identity map). Outside the module, NoHiddenScaleCoordinate in the dark-energy scale-affinity derivation reuses the same no-extra-coordinate reading. Status is theorem conditional on this admissibility law: zero sorry, zero new axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.