zAgingChannel_count
plain-language theorem explainer
The theorem establishes that the Z-aging channel inductive type has cardinality five. Cosmologists using the Recognition Science Hubble tension pipeline cite this count to fix the number of contributions in the late-to-early H0 ratio amplitude. The proof is a one-line decide tactic that succeeds on the derived Fintype instance of the five-constructor inductive type.
Claim. The finite cardinality of the set of Z-aging channels is five: $|Z| = 5$, where $Z$ enumerates the five physical contributions (matter density, radiation density, dark energy, curvature, scalar perturbation).
background
The module derives the Hubble tension prediction from Z-complexity aging of the recognition field. The amplitude formula is $r_H = 1 + (1/φ^5) · c$ with $φ^5 ∈ (11.05, 11.1)$ at $φ ∈ (1.61, 1.62)$, placing the ratio inside (1.075, 1.091) and containing the empirical value 1.083. Five Z-aging channels arise from configDim $D = 5$ and supply separate rungs on the φ-ladder to the total aging correction.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic succeeds because ZAgingChannel derives Fintype, DecidableEq and Repr, so the cardinality is computed statically from the five constructors.
why it matters
This supplies the channel count to the hubbleTensionCert definition, which assembles the full certificate for the Hubble tension prediction. It directly implements the five-channel structure required by the Z-complexity aging model. The parent result hubbleTensionCert invokes five_channels := zAgingChannel_count together with the phi5 bounds and band containment to close the A5 precision claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.