DerivedChannelPrediction
plain-language theorem explainer
A record type for one quantum-gravity falsifier channel: name, observable string, integer φ-ladder rung, geometric prefactor, and a real correction forced equal to prefactor times φ to the minus rung, with a positivity witness. Gravity authors cite it when packaging PTA, EHT, S-star, Cassini, and ringdown predictions under a common schema. Pure structure definition; the two Prop fields are the only mathematical content.
Claim. A derived channel prediction is a record $(N, O, r, g, c)$ with channel name $N$, observable label $O$, rung $r \in \mathbb{Z}$, geometric prefactor $g \in \mathbb{R}$, and correction $c \in \mathbb{R}$ satisfying $c = g \cdot \varphi^{-r}$ and $c > 0$.
background
The module derives φ-powers for D5 quantum-gravity falsifier channels from the rung scale address of each observable. The recognition substrate assigns to a length $L$ the rung $r(L) = \log_\varphi(L/\ell_{\mathrm{sub}})$; the recognition correction at that rung scales as $\varphi^{-r}$ relative to the Planck-scale value.
For astrophysical black holes the strong-field half-area rung is $s = 44$, the same address that appears in the baryon asymmetry $\eta_B = \varphi^{-44}$. Channel corrections are then geometric prefactors times $\varphi^{-44}$ (or $\varphi^{-1}$ for ringdown). The golden ratio $\varphi$ is the self-similar fixed point forced at T6 in the unified forcing chain.
Upstream rung symbols in the fermion/anchor bridge supply integer ladder addresses for particle species; here the same integer type is reused for gravitational scale addresses rather than fermion identities.
proof idea
No tactic or term proof: this is a structure declaration. Five data fields (two strings, an integer rung, two reals) plus two propositional fields. The equality field asserts correctionValue = geometricPrefactor * phi ^ (-rung); the positivity field asserts strict positivity of the correction. Inhabitants discharge those Props when they construct concrete channel records.
why it matters
Gives a uniform carrier for the five derived D5 channel predictions in this module. Downstream inhabitants are ptaDerived (prefactor 1, rung 44), ehtDerived (prefactor 2, rung 44), sStarDerived (prefactor 1, rung 44), cassiniDerived (prefactor 3, rung 44), and ringdownDerived (prefactor 1, rung 1); derivedChannels collects them as a list.
That packaging makes the module's structural claim checkable: each QG falsifier predicts a correction at a specific φ-power fixed by the rung address principle, with geometric factors (path-integral ×3 for Shapiro, ×2 projection for the photon ring) separated from the ladder power. Ties the strong-field gravitational channels to the same rung 44 that appears in baryon asymmetry, a structural coincidence highlighted in the module doc. Status is definitional scaffolding for proved channel values elsewhere in the file (0 sorry in the module).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.