canonicalNoHiddenScaleCoordinate
plain-language theorem explainer
The identity map on the cosmic scale factor is a concrete inhabitant of the no-hidden-scale-coordinate admissibility condition: the normalized Z-fraction equals the scale factor itself. Endpoint conditions Z(0)=0 and Z(1)=1 hold, and convex interpolation is preserved. Cosmologists closing the scale-affine dark-energy law from RS ledger admissibility cite this witness. Fields discharge by reflexivity and a one-line ring identity.
Claim. The canonical no-hidden-scale-coordinate law is the normalized Z-fraction $Z_{\mathrm{frac}}(a)=a$ on the scale factor $a$, satisfying the early endpoint $Z_{\mathrm{frac}}(0)=0$, the today endpoint $Z_{\mathrm{frac}}(1)=1$, and endpoint convex interpolation $Z_{\mathrm{frac}}((1-a)\cdot 0+a\cdot 1)=(1-a)Z_{\mathrm{frac}}(0)+a Z_{\mathrm{frac}}(1)$ for every real $a$.
background
This module closes the remaining U5 residue around dark-energy scale affinity. Upstream, CosmicZScaleLaw already showed that a scale-affine Z-law forces $Z(z)/Z_{\mathrm{today}}=a(z)$ and hence $\delta w(z)=\delta w_0/(1+z)$. The open question was the origin of that scale-affine law.
The structure here packages the lower admissibility gate: with only the early endpoint $a=0$ and the today endpoint $a=1$ fixed, a normalized ledger fraction may not insert an extra preferred coordinate on the interval. Concretely it carries a map $Z_{\mathrm{frac}}:\mathbb{R}\to\mathbb{R}$, the two endpoint equalities, and the convex-interpolation identity $Z_{\mathrm{frac}}((1-a)\cdot 0+a\cdot 1)=(1-a)Z_{\mathrm{frac}}(0)+a Z_{\mathrm{frac}}(1)$. That identity is exactly linear interpolation between the endpoints, so under the endpoint normalizations it forces $Z_{\mathrm{frac}}(a)=a$.
proof idea
Structure instance, not a deep proof. Set the Z-fraction to the identity $a\mapsto a$. The early-endpoint and today-endpoint fields are definitional equalities, closed by rfl. The no-hidden-coordinate field reduces, after substituting the identity and the endpoints, to the algebraic identity $a=(1-a)\cdot 0+a\cdot 1$, discharged by intro a; ring.
why it matters
Supplies the concrete witness that the no-hidden-scale-coordinate gate is inhabited, so the conversion theorems are non-vacuous. Downstream, canonicalNoHidden_maps_to_canonical shows that feeding this witness through the structure map yields exactly the canonical scale-affine Z-law of CosmicZScaleLaw. That is the strongest honest theorem-layer closure claimed in the module: the canonical dark-energy scale-affine shape is forced by the no-hidden-coordinate admissibility condition, with zero sorry and no new axiom.
The remaining deeper problem, flagged in the module doc, is to derive the admissibility gate itself from the universal forcing layer (T0–T8) rather than postulating it as a cosmic-Z gate. This definition does not touch that deeper step; it only pins the canonical inhabitant used by the certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.