strongFieldSignalModelWitness
plain-language theorem explainer
Packages four strong-field observation channels (EHT shadow, S-star periapsis, Cassini Shapiro delay, ringdown echoes) into a single witness that RS predictions differ from the GR zero baseline on each. Gravity and QG-falsifier work cites it to discharge the Track 6.C strong-field distinctness interface. The body is a structure instance: the proposition is the four-way conjunction of inequalities, proved by the four channel-level separation lemmas.
Claim. There is a witness of strong-field distinctness from GR whose content is the conjunction $$\delta r/r_s^{\mathrm{RS}}\neq 0,\quad \delta t/P^{\mathrm{RS}}\neq 0,\quad \delta\Delta t/\Delta t^{\mathrm{RS}}\neq 0,\quad A_{n+1}/A_n^{\mathrm{RS}}\neq 0,$$ with RS values $2\varphi^{-44}$, $\varphi^{-44}$, $3\varphi^{-44}$, and $\varphi^{-1}$ respectively, each proved unequal to the GR null baseline $0$.
background
The module builds typed observation-channel signal models for the QG falsifier surface. Each channel carries an observable, an RS prediction, a GR/ΛCDM null baseline, sensitivity figures, and a separation proof that the RS value differs from the null by more than the named falsifier threshold. Status is structural: zero sorry, zero RS-internal axioms.
The four strong-field channels used here are: EHT shadow-radius fractional deviation (RS: $2\varphi^{-44}$, GR: $0$); S-star periapsis timing residual near Sgr A* (RS: $\varphi^{-44}$, GR: $0$); Cassini/Shapiro delay residual beyond PPN (RS: $3\varphi^{-44}$, GR: $0$); and ringdown echo amplitude ratio (RS: $\varphi^{-1}\approx 0.618$, GR: no echoes, amplitude $0$).
Upstream, StrongFieldTestsDistinctFromGR is the Track 6.C hypothesis interface: a structure with a proposition field rs_strong_field_distinct_GR_only and a proof field holds. The doc marks it historically OPEN; this witness supplies a concrete inhabitant via the channel models.
proof idea
Definitional structure instance, not a tactic proof. The proposition field is set to the four-way conjunction of rsPrediction ≠ nullBaseline for the EHT, S-star, Cassini, and ringdown channels. The holds field is the corresponding 4-tuple of the channel lemmas ehtChannel.rsPrediction_ne_null, sStarChannel.rsPrediction_ne_null, cassiniChannel.rsPrediction_ne_null, and ringdownChannel.rsPrediction_ne_null. Each of those lemmas is already proved at the channel definition (nonzero powers of $\varphi$ and $\varphi^{-1}\neq 0$).
why it matters
Fills the strong-field half of the observation-channel signal-model layer. Downstream, canonicalStrongFieldDistinctWitness in MasterTheoremUnconditional is definitionally this witness (the doc notes ringdown algebra is quarantined here and is not consumed as a closed physical strong-field witness in the strengthened canonical path). It is also the strong_field_witness field of qgObservableSignalModelsCert, and feeds the one-statement theorem that asserts five typed channels with formula-level RS predictions, null baselines, proved separation, and nonempty PTA and strong-field master-theorem witnesses.
In the Recognition framework this is the concrete discharge of Track 6.C strong-field distinctness: RS deviations sit on the $\varphi$-ladder at rung scale $-44$ (and $\varphi^{-1}$ for echoes), against GR zeros. It does not by itself close experimental falsification; it packages the structural separation claims the master cert and unconditional master theorem route through.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.