CosmicZShapeCert
plain-language theorem explainer
Certificate packing the four facts that reduce the dark-energy EOS shape to the cosmic-Z accumulation history. Under the BIT kernel, the deviation equals δw₀ times Z(z)/Z_today, so the normalized shape is exactly the normalized Z-history and equals δw₀ today. Linear-in-scale-factor accumulation forces the canonical δw(z)=δw₀/(1+z). Cosmologists citing the U5 reduction use this bundle; fields are discharged by named lemmas in the module.
Claim. A cosmic-Z shape certificate is a record of four statements: (i) the EOS deviation satisfies $\delta w(z)=\delta w_0\cdot Z(z)/Z_{\mathrm{today}}$ for any history $Z$; (ii) if $Z(0)=Z_{\mathrm{today}}\neq 0$, then $\delta w(0)=\delta w_0$; (iii) if $\delta w_0\neq 0$, the normalized deviation equals the normalized Z-history; (iv) under linear-in-$a$ accumulation $Z(z)=Z_{\mathrm{today}}/(1+z)$ with $Z_{\mathrm{today}}\neq 0$ and $1+z\neq 0$, one has $\delta w(z)=\delta w_0/(1+z)$.
background
The module treats the dark-energy shape problem (U5) under the BIT mechanism: the equation of state is $w(z)=-1+\delta w\cdot Z(z)/Z_{\mathrm{today}}$, where $Z(z)$ is the integrated cosmic Z-complexity at redshift $z$ and $Z_{\mathrm{today}}=Z(0)$.
The deviation $\delta w(z):=w(z)+1$ is written bitDeviation; by definition of the BIT kernel it equals $\delta w_0\cdot Z(z)/Z_{\mathrm{today}}$. The linear history linearZ is the scale-factor accumulation law $Z(z)=Z_{\mathrm{today}}/(1+z)$. Boundary conditions forced by the kernel are $\delta w(0)=\delta w_0$ today and $\delta w\to 0$ as $Z\to 0$ (early-universe ΛCDM recovery).
Shape reduction is unconditional: deriving the dark-energy shape is exactly deriving $Z(z)$. The canonical $1/(1+z)$ kernel is then a theorem conditional on linear-in-$a$ accumulation.
proof idea
No proof body: this is a structure whose four fields are Prop-valued requirements. An inhabitant must supply proofs of the deviation formula, the today value, the normalized shape identity, and the linear-accumulation forcing of the canonical kernel.
The module inhabitant fills those fields by the existing lemmas bitDeviation_eq, bitDeviation_today, shape_reduction, and linear_accumulation_forces_canonical_kernel respectively. Each field is therefore a one-line assignment of a prior theorem, not a new argument.
why it matters
This certificate is the formal packaging of the honest U5 reduction stated in the module doc: shape reduction is a theorem; the canonical $\delta w(z)=\delta w_0/(1+z)$ is a theorem conditional on linear-in-$a$ Z-accumulation; the only residual freedom is the accumulation law itself.
The sole downstream use is the concrete inhabitant cosmicZShapeCert, which discharges every field with the named lemmas above. Anyone citing the BIT dark-energy shape, or arguing that U5 has been localized to a single physical premise about $Z(z)$, points here.
It does not touch the forcing chain (T0–T8), RCL, or the alpha band; it sits in the cosmology layer that consumes the BIT kernel and isolates what remains open: why Z accumulates linearly in $a$ rather than in cosmic time or $a^p$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.