canonicalStrongFieldDistinctWitness
plain-language theorem explainer
Canonical zero-argument witness that Recognition Science strong-field channels (EHT shadow, S-star orbits near Sgr A*, Cassini Shapiro delay) each differ from the pure-GR null baseline. Gravity auditors and the unconditional master-theorem assembly cite it as the D5 strong-field input. The body is a one-line alias of the typed signal-model witness; ringdown-echo algebra is deliberately not consumed.
Claim. There is a canonical inhabitant of the strong-field distinctness structure: the proposition that the RS prediction on each named observation channel (EHT shadow, S-star near Sgr A*, Cassini Shapiro delay) is unequal to that channel's pure-GR null baseline, together with a proof that the proposition holds.
background
This module closes the older conditional quantum-gravity master theorem by installing theorem-built, zero-argument witnesses for its five external inputs. The strong-field slot is Track 6.C: RS predictions for S-stars near Sgr A*, the EHT shadow, and Cassini Shapiro delay should be distinct from pure GR.
The target type is a thin structure packing a single proposition rs_strong_field_distinct_GR_only and a holds field. Upstream, the signal-model witness fills that proposition by a conjunction of three channel inequalities: each typed observation channel carries an RS prediction and a GR null baseline, and the witness asserts strict inequality on EHT, S-star, and Cassini.
Ringdown-echo algebra lives in the same signal-model module but is quarantined; it is not part of this closed physical strong-field witness.
proof idea
One-line definitional wrapper. The body is exactly the upstream strongFieldSignalModelWitness, which already inhabits StrongFieldTestsDistinctFromGR by setting the proposition to the three-way conjunction of channel deviations (EHT, S-star, Cassini each unequal to their GR null baselines) and discharging holds from that construction. No extra tactics or lemmas are applied here.
why it matters
Supplies the D5 named strong-field channel input to the scoped unconditional master assembly rs_quantum_gravity_master_unconditional and to the parallel endpoint-route validity theorem. Downstream non-circularity audit theorems consume the canonical witness suite so that the master theorem depends only on standalone fields, none of which assume a master clause.
In the Recognition framework this is the gravity-side claim that strong-field observables leave a nonzero RS residual relative to GR, complementary to the PTA band and the Regge/EH plus Page-curve witnesses. The parent structure was marked OPEN as a hypothesis; this definition routes a concrete signal-model discharge into the unconditional surface without absorbing quarantined ringdown algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.