NoHiddenScaleCoordinate
plain-language theorem explainer
Packages a normalized cosmic-Z fraction of the scale factor that vanishes at a=0, equals 1 at a=1, and preserves convex endpoint interpolation. Cosmologists deriving the RS dark-energy equation of state cite it as the lower admissibility gate forcing scale-affinity. As a structure it has no proof body; conversion and forcing theorems sit downstream.
Claim. A no-hidden-scale-coordinate law is a map $Z_{\mathrm{frac}}:\mathbb{R}\to\mathbb{R}$ with $Z_{\mathrm{frac}}(0)=0$, $Z_{\mathrm{frac}}(1)=1$, and 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)$. Equivalently, the normalized ledger fraction preserves endpoint convex interpolation on the cosmic scale interval $[0,1]$.
background
The module closes the remaining U5 residue in the dark-energy scale-affinity story. Upstream, CosmicZScaleLaw already showed that a scale-affine normalized Z-history yields $Z(z)/Z_{\mathrm{today}}=a(z)$ and hence the deviation law $\delta w(z)=\delta w_0/(1+z)$. The open question was the origin of that scale-affine hypothesis.
A scale-affine Z-law is a normalized cosmic-Z history that preserves interpolation from the early zero-complexity endpoint $a=0$ to today $a=1$. Its key field is the no-extra-coordinate condition: the ledger is uniform in the scale-factor coordinate until further physical structure is introduced.
The present structure is the lower admissibility reading of that condition. With only the two endpoints available, a normalized ledger fraction cannot insert a nonlinear preferred coordinate without extra structure, so it must preserve endpoint convex interpolation.
proof idea
Structure definition, not a theorem. Four fields: a real map $Z_{\mathrm{frac}}$, the early endpoint $Z_{\mathrm{frac}}(0)=0$, the today endpoint $Z_{\mathrm{frac}}(1)=1$, and the no-hidden-coordinate axiom that $Z_{\mathrm{frac}}$ preserves the convex combination $(1-a)\cdot 0+a\cdot 1$. No tactics or lemmas; the mathematical content is the packaged Prop data. Downstream, a one-line field-copy converts any such package into a scale-affine Z-law.
why it matters
This is the named admissibility gate that turns the RS "no hidden coordinate" principle into Lean data for cosmic Z. The conversion noHidden_to_scaleAffine shows the package is exactly the data of a scale-affine Z-law. From there the forcing chain fires: the condition forces $Z_{\mathrm{frac}}(a)=a$, forces the redshift history $Z(z)=Z_{\mathrm{today}}/(1+z)$, and forces the canonical dark-energy deviation $\delta w(z)=\delta w_0/(1+z)$ and kernel $w=-1+\delta w_0/(1+z)$.
The module certificate and the canonical inhabitant (identity fraction) sit on top of this structure. Framework-wise it is the strongest honest theorem-layer closure of the U5 residue: the canonical shape is forced by admissibility rather than postulated. The remaining deeper problem, noted in the module doc, is to derive the admissibility gate itself from the universal forcing layer (T0–T8) instead of stating it cosmologically.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.