StrongFieldTestsDistinctFromGR
plain-language theorem explainer
Named hypothesis package for Track 6.C: RS strong-field observables (S-stars near Sgr A*, EHT shadow, Cassini Shapiro delay) differ from pure GR. Gravity master-theorem authors cite it as one of five open inputs to the conditional quantum-gravity master statement. It is a structure carrying a bare Prop plus a holds witness, with no proof content.
Claim. A structure packaging a proposition $P$ asserting that Recognition Science strong-field test predictions are distinct from pure general relativity, together with a witness that $P$ holds. The intended content of $P$ is that RS forecasts for S-star orbits near Sgr A*, the EHT black-hole shadow, and Cassini Shapiro delay differ from the pure-GR baselines.
background
Module Gravity.MasterTheorem authors the Track 7.A master statement of the RS quantum-gravity discovery as a twelve-clause conjunction aligned to six done-criteria sectors (D1 substrate through D6 zero free parameters). Eight clauses are already discharged from existing Lean theorems; five remain open and are exposed as named hypothesis structures.
This declaration is the D5 strong-field discriminator slot (master-plan Track 6.C). Sibling closed discriminators already exist: the QNM/ringdown certificate proves the RS leading-log entropy coefficient $c_{RS}=-\log\varphi/2$ is separated from the LQG value $-1/2$ and the string value $-3/2$. The strong-field package is the analogous claim for solar-system and galactic-center tests, still awaiting a theorem-grade witness.
In the master template the clause appears as rs_strong_field_distinct_GR_only inside the D5 block alongside QNM and PTA discriminators. Downstream structural notes record the intended algebraic seed as something like $\varphi^{-44}>0$, to be upgraded into concrete deviation patterns for S-stars, EHT, and Cassini.
proof idea
No proof. The declaration is a two-field structure: a field of type Prop naming the open claim, and a field holds inhabiting that Prop. Instantiating the structure is exactly supplying a proof of the strong-field distinctness statement. Downstream conditional master theorems take an inhabitant of this structure as a hypothesis and project holds into the big conjunction; they do not construct it.
why it matters
Closes the authoring half of Track 7.A for the strong-field discriminator without pretending Track 6.C is done. Parent consumers are RSQuantumGravityMaster, rs_quantum_gravity_master_conditional, and rs_quantum_gravity_master_one_statement, each of which threads this structure as H_strong among the five open inputs. Structural honesty theorems (honest_scope_statement, MasterTheoremStructuralCert) explicitly list it as still requiring a dynamical upgrade from a bare positivity seed to derived deviation patterns.
Within the Recognition framework this is the D5 empirical-discriminator counterpart to closed pieces such as Hawking temperature in SI form, BMV positivity, cost uniqueness, and the T0–T8 forcing chain. The discovery claim stays conditional until Track 6.C (and the other four open tracks) discharge this interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.