noHidden_forces_canonical_deviation
plain-language theorem explainer
Under the no-hidden-scale-coordinate admissibility gate, the cosmic equation-of-state deviation is forced to the canonical form δw(z)=δw₀/(1+z). Cosmologists tracing the U5 dark-energy residue cite this as the theorem-layer link from ledger admissibility to the BIT deviation law. The proof is a one-line wrapper: convert the gate to a scale-affine Z-law, then apply the existing scale-affinity deviation theorem.
Claim. Let $H$ be a no-hidden-scale-coordinate structure (normalized $Z$-fraction with $Z_{\mathrm{frac}}(0)=0$, $Z_{\mathrm{frac}}(1)=1$, and endpoint convex interpolation). For $Z_t\neq 0$ and $1+z\neq 0$, the bit deviation built from the $Z$-history induced by $H$ satisfies $\delta w(z)=\delta w_0/(1+z)$.
background
This module closes the remaining U5 residue around dark-energy scale affinity. Upstream, CosmicZScaleLaw already showed that a scale-affine Z-law implies $Z(z)/Z_{\mathrm{today}}=a(z)$ and therefore the canonical deviation $\delta w(z)=\delta w_0/(1+z)$. The open question was the origin of scale-affinity itself.
The local answer is the admissibility gate NoHiddenScaleCoordinate: once the early endpoint $a=0$ and today endpoint $a=1$ are fixed, the recognition ledger may not insert an extra preferred coordinate on the cosmic scale interval. Concretely, the normalized Z-fraction $Z_{\mathrm{frac}}$ obeys $Z_{\mathrm{frac}}(0)=0$, $Z_{\mathrm{frac}}(1)=1$, and preserves endpoint convex interpolation, $Z_{\mathrm{frac}}((1-a)\cdot 0+a\cdot 1)=(1-a)Z_{\mathrm{frac}}(0)+a Z_{\mathrm{frac}}(1)$.
Bit deviation is the equation-of-state deviation $\delta w(z)=w(z)+1$, built from a cosmic-Z history. The conversion noHidden_to_scaleAffine turns any such gate into a ScaleAffineZLaw, so the prior scale-affinity theorems apply directly.
proof idea
One-line term wrapper. Apply noHidden_to_scaleAffine to the hypothesis $H$ to obtain a ScaleAffineZLaw, then invoke the upstream theorem scaleAffine_forces_canonical_deviation on that law with the same $dw_0$, $Z_t$, $z$ and the nonzero side conditions. No extra algebra is performed here; the identity $\delta w(z)=dw_0/(1+z)$ is inherited wholesale from the scale-affinity layer.
why it matters
This is the strongest honest theorem-layer closure for the dark-energy deviation shape inside the module: the canonical BIT form is forced by the no-hidden-scale-coordinate gate rather than postulated. It is one of the five fields inhabiting scaleAffinityDerivationCert (canonical_deviation_forced), alongside the companion forcings of identity, linear $Z$, and the canonical kernel.
In the broader Recognition chain it sits downstream of the cosmic-Z scale law and upstream of any certificate that packages U5 residue closure. The module doc is explicit that a deeper open problem remains: derive the admissibility gate itself from the universal forcing layer (T0–T8) instead of stating it as a cosmic-Z gate. Until that step, the result is conditional on the named gate, with zero sorry and zero new axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.