ehtCorrectionValue_pos
plain-language theorem explainer
The EHT shadow-radius fractional correction equals 2·φ^(-s) with s the strong-field rung, and is strictly positive. Gravity and EHT-channel work cites this when packaging the derived prediction record. Proof is a one-line wrapper: positivity of the prefactor 2 times positivity of a real power of φ.
Claim. Let $\varphi>1$ be the golden ratio and let $s$ be the strong-field rung. The EHT correction $2\,\varphi^{-s}$ satisfies $0 < 2\,\varphi^{-s}$.
background
This module derives φ-power corrections for quantum-gravity falsifier channels from the rung address of each observable. A length scale $L$ is assigned rung $r(L)=\log_\varphi(L/\ell_{\mathrm{sub}})$; recognition corrections at that rung scale as $\varphi^{-r}$ relative to the Planck value.
The strong-field rung $s$ is fixed at 44: half the horizon information of an astrophysical black hole is processed there, matching the baryon-asymmetry rung $\eta_B=\varphi^{-44}$. The EHT channel correction is defined as $2\cdot\varphi^{-s}$. The factor 2 is the shadow-to-photon-ring projection: the observed shadow radius is the apparent angular radius of the photon ring, so lensing magnification doubles the fractional shift.
Sibling values (PTA, S-star, Cassini, ringdown) use the same ladder with different geometric prefactors.
proof idea
One-line wrapper on the real product rule for strict positivity. The definition is $2\cdot\varphi^{-s}$. The first factor is discharged by norm_num ($0<2$). The second uses zpow_pos with phi_pos: every real power of a positive base stays positive. No rung arithmetic is needed beyond the definition.
why it matters
Feeds ehtDerived, the packaged EHT channel prediction (observable: shadow-radius fractional deviation $\delta r/r_s$, rung 44, geometric prefactor 2, correction value this constant). Without positivity the derived-prediction record cannot assert a physically meaningful fractional shift.
Sits in the D5 gravity falsifier suite: each channel (PTA $\varphi^{-44}$, EHT $2\varphi^{-44}$, S-star $\varphi^{-44}$, Cassini $3\varphi^{-44}$, ringdown $\varphi^{-1}$) is a pure φ-ladder address times a geometric prefactor. The shared rung 44 with $\eta_B$ is structural, not fitted. Landmark contact is the φ-ladder and the strong-field half-area address, not the T0–T8 forcing chain directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.