scaleAffinityDerivationCert
plain-language theorem explainer
The scale-affinity derivation certificate is inhabited: the no-hidden-scale-coordinate gate yields the scale-affine Z-law and the canonical dark-energy shape. Cosmologists closing the RS dark-energy sector cite it as the single packaged witness of that forcing chain. The definition is a pure structure inhabitant that assigns five already-proved forcing lemmas to the certificate fields.
Claim. There is an inhabited certificate asserting that any no-hidden-scale-coordinate hypothesis $H$ produces a scale-affine Z-law, forces the normalized Z-fraction to equal the scale factor ($H.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)$ with kernel $w(z)=-1+\delta w_0/(1+z)$.
background
The module tightens the remaining U5 residue in RS cosmology. Upstream, CosmicZScaleLaw already showed that a scale-affine Z-law implies $Z(z)/Z_{\mathrm{today}}=a(z)$ and hence the canonical deviation $\delta w(z)=\delta w_0/(1+z)$. The open question was the origin of that scale-affine law.
The local answer is the admissibility gate NoHiddenScaleCoordinate: once the early endpoint $a=0$ and the today endpoint $a=1$ are fixed, the recognition ledger may not insert an extra preferred coordinate on the cosmic scale interval. Normalized Z-fraction must therefore preserve endpoint convex interpolation. That condition is exactly the scale-affine law.
Sibling lemmas convert the gate into the scale-affine structure, force identity $Z_{\mathrm{frac}}(a)=a$, force linear redshift history, and force the canonical bit-deviation and bit-kernel. The certificate structure packages those five facts as a single witness.
proof idea
Pure structure inhabitant. Each certificate field is assigned the corresponding already-proved lemma: conversion of the no-hidden gate to a scale-affine Z-law; identity forcing via that conversion plus the upstream scale-affine identity lemma; linear-Z forcing likewise; and the two canonical dark-energy forcing theorems for deviation and kernel. No new reasoning occurs at this site.
why it matters
This is the strongest honest theorem-layer closure of the U5 dark-energy residue: the canonical shape is forced by the no-hidden-scale-coordinate admissibility condition, with zero sorry and zero new axiom. The module status is theorem conditional on that named gate. Downstream consumers (none yet wired in the graph) can treat the certificate as a single hypothesis package rather than five separate lemmas. 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 stating it as a cosmic-Z gate. No direct link to phi, the eight-tick octave, or the alpha band appears here; the content is pure cosmic-scale admissibility.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.