derivedChannels
plain-language theorem explainer
Packages the five quantum-gravity falsifier channel predictions (PTA, EHT, S-star, Cassini, ringdown) as a single list of derived channel records. Downstream certificates and positivity lemmas cite this list as the canonical inventory. The body is a five-element list literal of the already-constructed channel structures.
Claim. Define the list of five derived channel predictions: PTA stochastic background, EHT shadow/ring, S-star periapsis, Cassini/Shapiro delay, and ringdown echoes. Each entry carries a rung $r$, geometric prefactor $g$, and correction value $g\,\varphi^{-r}$ with a positivity proof.
background
This module derives $\varphi$-powers for D5 quantum-gravity falsifier channels from the rung scale address of each observable. The recognition substrate assigns rung $r(L)=\log_\varphi(L/\ell_{\mathrm{sub}})$ to length scale $L$; the correction at rung $r$ scales as $\varphi^{-r}$ relative to the Planck-scale value.
The strong-field rung is $s=44$, the half-area rung of an astrophysical black-hole horizon (same rung as the baryon asymmetry $\eta_B=\varphi^{-44}$). Four channels sample that rung with geometric prefactors $1$, $2$, $1$, $3$; ringdown uses the one-step self-similar rung $r=1$.
Each list element is a DerivedChannelPrediction: name, observable string, integer rung, real prefactor, correction value, equality $v=g,\varphi^{-r}$, and $v>0$.
proof idea
Definition by list literal. No proof obligations beyond those already discharged inside the five component definitions (ptaDerived, ehtDerived, sStarDerived, cassiniDerived, ringdownDerived). Each component fills the structure fields and inherits correctionValue_eq and correctionValue_pos from the corresponding correction-value lemmas.
why it matters
Canonical inventory for the QG channel rung-derivation certificate. Downstream, derivedChannels_length asserts length five by rfl; all_derived_channels_pos projects positivity from each record; QGChannelRungDerivationCert bundles count, positivity, the four-way sharing of rung 44, and ringdown rung 1.
In the Recognition framework this closes the structural map from the strong-field rung (linked to $\eta_B=\varphi^{-44}$ and the $\varphi$-ladder) onto concrete observational channels. It does not compute numerical bounds against data; it fixes which $\varphi$-powers and prefactors the D5 falsifiers must use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.