scaleAffine_forces_canonical_deviation
plain-language theorem explainer
Under a scale-affine ledger law on the cosmic interval from a=0 to a=1, the BIT equation-of-state deviation is forced to δw(z)=δw₀/(1+z). Cosmologists deriving the dark-energy shape from Recognition ledger uniformity cite this. The proof identifies the induced Z-history with the linear-in-a history, then applies the linear-accumulation kernel theorem.
Claim. Let $Z_t \neq 0$ and $1+z \neq 0$. If a normalized cosmic-$Z$ history is scale-affine (preserves convex interpolation from the early endpoint $a=0$ to today $a=1$), then the BIT deviation built from the $Z$-history induced by that law satisfies $\delta w(z) = \delta w_0/(1+z)$.
background
The module CosmicZScaleLaw closes the last shape residue in the dark-energy plan. CosmicZHistory already shows that under the BIT kernel one has $\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 remaining question is why that normalized history should be the scale factor $a(z)=1/(1+z)$.
Scale-affine ledger law is the admissibility condition: along the cosmic interval from the early zero-complexity endpoint $a=0$ to today $a=1$, equal scale-factor fractions carry equal recognition-ledger fractions. Formally, a structure ScaleAffineZLaw supplies a normalized fraction $Z_{\mathrm{frac}}$ with endpoints $Z_{\mathrm{frac}}(0)=0$, $Z_{\mathrm{frac}}(1)=1$, and the convex-interpolation identity $Z_{\mathrm{frac}}(a)=(1-a)Z_{\mathrm{frac}}(0)+a Z_{\mathrm{frac}}(1)$. The induced history is $Z(z)=Z_t\cdot Z_{\mathrm{frac}}(a(z))$.
Upstream, scaleAffine_forces_linearZ already forces $Z(z)=Z_t/(1+z)$. Separately, linear_accumulation_forces_canonical_kernel states that with the linear-$a$ history the BIT kernel produces exactly $\delta w(z)=\delta w_0/(1+z)$.
proof idea
Two-step rewrite. First prove functional equality of the induced history with the linear history: by funext, pointwise apply scaleAffine_forces_linearZ, which reduces scale-affinity to $Z_{\mathrm{frac}}(a)=a$ and yields $Z(z)=Z_t/(1+z)$. Rewrite the goal under that equality. Second, discharge by linear_accumulation_forces_canonical_kernel, which unfolds the BIT deviation identity $\delta w=\delta w_0\cdot Z/Z_t$ on the linear history and cancels $Z_t\neq 0$ to leave $\delta w_0/(1+z)$. No new algebra beyond those two lemmas.
why it matters
This is the deviation half of the scale-law certificate: cosmicZScaleLawCert records it as canonical_deviation_forced. The sibling scaleAffine_forces_canonical_kernel lifts the same identity to the equation of state $w(z)=-1+\delta w_0/(1+z)$ by unfolding $\delta w=w+1$. Downstream, DarkEnergyScaleAffinityDerivation uses it as noHidden_forces_canonical_deviation: once a no-hidden-scale-coordinate hypothesis is converted to a scale-affine law, the canonical deviation follows immediately.
In the Recognition dark-energy plan this is the step that turns ledger uniformity (no intermediate scale coordinate selected before new physics is supplied) into the concrete $1/(1+z)$ shape, rather than fitting a kernel family by hand. It sits after the BIT-kernel reduction of CosmicZHistory and before the inhabited certificate that packages identity, redshift history, deviation, and kernel forcing together. Status is fully proved: zero sorry, conditional only on the named scale-affine admissibility structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.