derivedChannels_length
plain-language theorem explainer
The list of derived QG channel predictions has exactly five entries. Anyone assembling the rung-derivation certificate cites this count. The proof is reflexivity on the five-element list literal (PTA, EHT, S-star, Cassini, ringdown).
Claim. The list of derived channel predictions has length $5$.
background
This module derives $\varphi$-powers for five quantum-gravity falsifier channels from rung scale addresses. The recognition substrate assigns rung $r(L)=\log_\varphi(L/\ell_{\mathrm{sub}})$ to each length scale; corrections scale as $\varphi^{-r}$.
The five channels are PTA (strain at strong-field injection), EHT (shadow shift, $\times 2$), S-star (periapsis residual), Cassini (Shapiro delay, $\times 3$), and ringdown (one-rung reflection). Four share the strong-field rung $s=44$ (the same rung as baryon asymmetry $\eta_B=\varphi^{-44}$); ringdown sits at rung $1$.
The list derivedChannels packages the five concrete predictions. List length here is ordinary finite-list cardinality (as in the primitive recognition calculus length on traces).
proof idea
One-line term proof by rfl. The definition is the five-element literal [ptaDerived, ehtDerived, sStarDerived, cassiniDerived, ringdownDerived], so List.length reduces definitionally to $5$.
why it matters
Feeds the certificate field derived_count in qgChannelRungDerivationCert, which bundles count, positivity of all corrections, the shared rung-44 fact for four channels, ringdown at rung 1, and the golden-ratio partition. Without a locked length of five, the D5 channel table in the module doc cannot be certified as complete relative to the listed predictions. Structural only: it pins cardinality of the derived list, not the physics of each $\varphi$-power.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.