ehtChannel
plain-language theorem explainer
Packages the Event Horizon Telescope shadow/ring test as a typed QG signal model: RS predicts a fractional shadow-radius shift of order $2\varphi^{-44}$, while Kerr GR predicts zero. Gravity and strong-field auditors cite it when assembling the five-channel falsifier list. The two positivity obligations are short positivity arguments from $\varphi>0$ and integer powers.
Claim. The EHT observation channel is the typed signal model with name "EHT shadow/ring", observable equal to the fractional shadow-radius deviation $\delta r/r_s$, RS prediction $2\varphi^{-44}$, and GR/Kerr null baseline $0$, together with proofs that the prediction is nonzero and that the absolute separation from the baseline is strictly positive.
background
Module Gravity.QGObservableSignalModels builds typed signal models for the D5 quantum-gravity falsifier surface. Each channel carries an observable string, an RS numeric prediction, a GR/ΛCDM null baseline, and two separation proofs: prediction unequal to null, and positive absolute gap.
The underlying structure ObservationChannelSignalModel is exactly that bundle. Here the channel is the EHT black-hole shadow/ring measurement. Doc-comment: RS predicts a positive deviation of order $\varphi^{-44}$ times the Schwarzschild radius; GR predicts zero deviation from the Kerr shadow template.
The scale $\varphi^{-44}$ sits on the RS $\varphi$-ladder ( Cosmology scale $k\mapsto\varphi^k$ and related rung machinery). Constants $\varphi$ is the golden ratio forced as the self-similar fixed point (forcing chain T6). Null baseline is pure Kerr GR with no extra RS correction.
proof idea
Definitional record fill-in, not a deep theorem. rsPrediction is set to $2\varphi^{-44}$ and nullBaseline to $0$.
rsPrediction_ne_null: assume equality, then $2\varphi^{-44}=0$. Apply zpow_pos with phi_pos to get $\varphi^{-44}>0$, contradict by linarith.
separation_pos: first obtain $0<2\varphi^{-44}$ via mul_pos on a norm_num fact and again zpow_pos phi_pos. Rewrite $|\mathrm{pred}-0|$ with sub_zero and abs_of_pos, then return that same positive quantity.
why it matters
Fills the EHT slot in the five-channel QG falsifier matrix (PTA, EHT, S-star, Cassini, ringdown) described in the module doc. Downstream, qgChannels lists this model with the other four channels. strongFieldSignalModelWitness uses the inequality ehtChannel.rsPrediction ≠ ehtChannel.nullBaseline as the first conjunct of the strong-field "distinct from GR" witness feeding MasterTheorem.StrongFieldTestsDistinctFromGR.
In the Recognition framework this is an observational landing of the $\varphi$-ladder at rung scale 44 in the strong-field/near-horizon regime, complementary to the PTA stochastic-background channel. It does not derive the coefficient 2 or the rung index from first principles inside this file; it freezes the published RS prediction so separation theorems and certificates can quote a single typed object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.