ZAgingChannel
plain-language theorem explainer
ZAgingChannel enumerates the five channels through which the recognition field ages over cosmic time in the Hubble tension pipeline. Cosmologists using Recognition Science cite this enumeration when certifying that the predicted H0 late/early ratio band contains the empirical value 1.083. The declaration is a direct inductive type with five named constructors and automatic derivation of DecidableEq, Repr, BEq, and Fintype.
Claim. The Z-aging channels are the five cases matter density, radiation density, dark energy, curvature, and scalar perturbation.
background
The module sets out the A5 precision closure for the Hubble tension: RS predicts the late/early H0 ratio lies in (1.075, 1.091) via Z-complexity aging of the recognition field. The amplitude formula is r_H = 1 + (1/φ^5) · c with φ^5 = 5φ + 3. Five channels are introduced under configDim D = 5, each tied to a rung of the φ-ladder. The setting uses RS-native constants with φ ∈ (1.61, 1.62) giving 1/φ^5 ∈ (0.0900, 0.0906) and c ≈ 0.91 placing the ratio near 1.083.
proof idea
The declaration is an inductive definition that introduces the five constructors and derives the required type-class instances in one step.
why it matters
The definition supplies the five channels required by HubbleTensionCert to certify that the ratio band contains 1.083 and by zAgingChannel_count to prove Fintype.card ZAgingChannel = 5. It completes the enumeration step in the Z-aging pipeline, connecting directly to the Recognition Science prediction of the H0 tension through the φ-ladder and the five-channel structure. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.