noHidden_forces_identity
plain-language theorem explainer
Under the no-hidden-scale-coordinate admissibility condition, the normalized cosmic Z-fraction equals the scale factor itself at every real argument. Cosmologists closing the RS dark-energy U5 residue cite this when converting the ledger gate into an identity map on scale. The proof is a one-line wrapper: package the hypothesis as a scale-affine Z-law and apply the uniqueness theorem already proved for that law.
Claim. If a normalized Z-fraction $Z_{\mathrm{frac}}:\mathbb{R}\to\mathbb{R}$ satisfies the no-hidden-scale-coordinate condition (endpoints $Z_{\mathrm{frac}}(0)=0$, $Z_{\mathrm{frac}}(1)=1$, and preservation of endpoint convex interpolation), then $Z_{\mathrm{frac}}(a)=a$ for every real $a$.
background
This module tightens the remaining U5 residue in the RS cosmology stack. CosmicZScaleLaw already proved that a scale-affine Z-law forces $Z(z)/Z_{\mathrm{today}}=a(z)$ and thence $\delta w(z)=\delta w_0/(1+z)$. The remaining question was where scale-affinity itself comes from.
NoHiddenScaleCoordinate is the lower admissibility gate: with only the early endpoint $a=0$ and today endpoint $a=1$ fixed, a normalized ledger fraction may not insert an extra preferred coordinate inside the interval, so it preserves endpoint convex interpolation. The conversion packages that data as a ScaleAffineZLaw.
Upstream, scaleAffine_forces_identity states that any scale-affine law uniquely forces the normalized Z-fraction to be the identity map on scale factor (via the affine identity simplified at the two endpoints).
proof idea
One-line term proof. Convert the NoHiddenScaleCoordinate hypothesis into a ScaleAffineZLaw via the structure map that copies Zfrac, the two endpoint equalities, and the no-hidden-coordinate clause into the scale-affine field. Then apply CosmicZScaleLaw.scaleAffine_forces_identity at the given real $a$. That upstream lemma expands the scale-affine identity and simplifies with early_zero and today_one to obtain Zfrac $a = a$.
why it matters
Feeds the scale-affinity derivation certificate, which packages the full chain from the no-hidden gate through identity, linear-Z, canonical deviation, and canonical kernel. Module doc frames this as the strongest honest theorem-layer closure of the U5 residue: the canonical shape is forced by the no-hidden-scale-coordinate admissibility condition rather than postulated. The remaining deeper problem, if desired, is to derive that admissibility gate from the universal forcing layer (T0-T8) rather than stating it as a cosmic-Z gate. Status is theorem 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.