noHidden_forces_canonical_kernel
plain-language theorem explainer
The no-hidden-scale-coordinate admissibility gate forces the BIT dark-energy equation of state into the canonical form w(z)=-1+δw₀/(1+z). Cosmologists closing the RS U5 residue cite this when tracing the kernel from ledger admissibility rather than from an assumed scale-affine law. The proof is a one-line wrapper: convert the gate to a scale-affine Z-law, then apply the upstream scale-affinity kernel theorem.
Claim. Let $H$ be a no-hidden-scale-coordinate law (a normalized Z-fraction with $Z_{\mathrm{frac}}(0)=0$, $Z_{\mathrm{frac}}(1)=1$, and endpoint convex interpolation preserved). For $\delta w_0,Z_t,z\in\mathbb{R}$ with $Z_t\neq 0$ and $1+z\neq 0$, the BIT kernel built on the cosmic-Z history induced by $H$ satisfies $w(z)=-1+\delta w_0/(1+z)$.
background
In the RS cosmology stack the BIT dark-energy equation of state is $w(z)=-1+\delta w_0\cdot Z(z)/Z_{\mathrm{today}}$, with $Z$ the accumulated cosmic recognition ledger. Module CosmicZScaleLaw already proved that any scale-affine Z-law forces the linear history $Z(z)=Z_{\mathrm{today}}/(1+z)$ and therefore the canonical kernel $w(z)=-1+\delta w_0/(1+z)$.
The remaining question is the origin of scale-affinity. This module introduces the lower admissibility principle NoHiddenScaleCoordinate: once the early endpoint $a=0$ and today endpoint $a=1$ are fixed, the normalized ledger fraction may not insert an extra preferred coordinate inside the interval, so it preserves endpoint convex interpolation. That condition is exactly the scale-affine law.
The conversion lemma turns any such witness into a ScaleAffineZLaw, which is the input expected by the upstream kernel theorem scaleAffine_forces_canonical_kernel.
proof idea
One-line wrapper. Convert the hypothesis $H$ via noHidden_to_scaleAffine into a scale-affine Z-law, then apply CosmicZScaleLaw.scaleAffine_forces_canonical_kernel with the same $\delta w_0$, $Z_t$, $z$ and the nonzero side conditions. No further algebra is done here; the identity is inherited from the upstream result, which reduces the BIT kernel through the forced linear-in-scale-factor history and a short linear arithmetic step.
why it matters
Terminal forcing step of the dark-energy scale-affinity derivation: the no-hidden-coordinate gate alone produces the canonical equation of state. It is packaged into scaleAffinityDerivationCert as canonical_kernel_forced, completing the certificate that the U5 residue closes at the theorem layer under the named admissibility condition.
The module doc is explicit that this is the strongest honest closure available without deriving the gate from the universal forcing chain (T0–T8). The remaining deeper problem, if desired, is to obtain NoHiddenScaleCoordinate from the foundation layer rather than stating it as a cosmic-Z admissibility hypothesis. Within cosmology the result pins the BIT kernel shape used for dark-energy phenomenology in RS-native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.