StrongFieldObservableChannel
plain-language theorem explainer
Names the three strong-field observational channels on the quantum-gravity falsifier surface: S-stars near Sgr A*, the EHT shadow, and Cassini Shapiro delay. Anyone citing Track 6.C structural discriminators indexes shifts and response factors by this type. Pure inductive definition with decidable equality; no proof content.
Claim. An inductive type of strong-field observable channels with three constructors: S-stars (near Sgr A*), EHT black-hole shadow, and Cassini Shapiro delay, equipped with decidable equality.
background
Track 6.C of the quantum-gravity master plan asks for structural discrimination of Recognition Science from pure GR in strong-field tests: S-stars near Sgr A*, EHT shadow constraints, and Cassini Shapiro delay (among others). This module supplies the algebraic form of that discriminator, not the channel-by-channel physics.
The universal RS strong-field deviation is the positive scale $\varphi^{-44}$ (the same rung-44 forcing that yields $\eta_B = \varphi^{-44}$ on the phi-rung ladder). Pure GR predicts zero deviation. Named channels exist so that each observable can carry a positive response factor times that universal scale, making the per-channel shift strictly positive and unequal to the GR baseline.
The type is the index set for those channel factors and shifts. Downstream definitions map each constructor to a positive real factor and form the RS observable shift as factor times $\varphi^{-44}$.
proof idea
Definitional inductive: three nullary constructors sStars, ehtShadow, cassiniShapiro, with DecidableEq derived. No tactics, lemmas, or proof body.
why it matters
Gives the discrete index set for Track 6.C's named falsifier channels inside Gravity.StrongFieldStructural. Downstream, strongFieldObservableChannelFactor assigns positive response weights (1, 2, 3) to the three constructors; rs_strong_field_observable_shift multiplies those by the universal rung-44 deviation $\varphi^{-44}$; pure GR is the zero baseline on the same index.
Those feed rs_strong_field_observable_shift_pos, inequality with pure GR, and the forall-quantified discriminator rs_strong_field_observable_distinct_GR_prop. That structural package supports the witness retiring StrongFieldTestsDistinctFromGR from the conditional gravity master theorem. Specific deviation patterns per instrument remain future physics; the type only names the channels the algebra ranges over.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.