ehtCorrectionValue
plain-language theorem explainer
The EHT shadow-radius fractional correction equals twice φ to the minus strong-field rung, i.e. 2·φ^(-44). Black-hole and strong-field gravity workers cite it as the RS prediction for photon-ring / shadow shifts. The definition is a one-line product of the geometric projection factor 2 and the φ-ladder correction at rung 44.
Claim. The EHT correction is defined by $\delta_{\mathrm{EHT}} := 2\,\varphi^{-s}$, where $s=44$ is the strong-field rung (half-area rung of stellar-mass horizons). Explicitly, $\delta_{\mathrm{EHT}} = 2\,\varphi^{-44}$.
background
This module derives φ-power corrections for five quantum-gravity falsifier channels from the rung scale address of each observable. A length scale $L$ is assigned rung $r(L)=\log_\varphi(L/\ell_{\mathrm{sub}})$; the recognition correction at that rung scales as $\varphi^{-r}$ relative to the Planck value.
The strong-field rung is fixed at $s=44$: for stellar-mass black holes the horizon cell count is $N=A/\ell_{\mathrm{sub}}^2\approx\varphi^{88}$, so the half-area rung is 44. The same integer appears as $|\eta_B|$ for the baryon asymmetry; the module treats the coincidence as structural rather than accidental.
Among the channel table, EHT is the shadow-radius fractional deviation at the photon ring. The observed shadow radius is the apparent angular radius of the photon ring, so lensing magnification doubles the fractional correction and supplies the prefactor 2.
proof idea
Pure definition, not a proved equality. The body is the product of the constant geometric prefactor 2 with $\varphi$ raised to the negation of strongFieldRung (the integer 44). No tactics or lemmas are invoked; downstream positivity and equality theorems unfold this abbreviation by rfl or zpow arithmetic.
why it matters
Fills the EHT row of the D5 channel table: shadow shift $=2\cdot\varphi^{-44}$. It is the correctionValue field of the packaged ehtDerived prediction (channel name "EHT shadow/ring", observable $\delta r/r_s$, rung 44, geometric prefactor 2). The identity eht_eq_two_times_pta records that this value is exactly twice the PTA strain correction at the same rung, and ehtCorrectionValue_pos certifies positivity from $\varphi>0$. Together these close the structural (0-sorry) derivation of the EHT falsifier from the shared strong-field / baryon-asymmetry rung rather than from a free fit parameter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.