canonicalStrongFieldDistinctWitness_channelRoute
plain-language theorem explainer
Packages the structural strong-field observable witness as the canonical channel-route input of type “strong-field tests distinct from GR.” Gravity auditors cite it when assembling the zero-argument quantum-gravity master surface. The body is a one-line alias of the existing StrongFieldStructural witness; no new argument is given.
Claim. Define the canonical channel-route witness asserting that named strong-field observable channels are distinct from general relativity, equal to the already-constructed structural strong-field distinctness witness.
background
The module Gravity.MasterTheoremUnconditional installs theorem-built witnesses for the five inputs that the older conditional quantum-gravity master theorem took as arguments. The conditional theorem stays the audit surface; this file supplies the zero-argument route through it.
Among those five inputs, D5 covers named strong-field channels: observables in the strong-field regime that RS predicts differ from pure GR. The type being inhabited is the master-theorem proposition that strong-field tests are distinct from GR. The structural module already builds a concrete witness for that proposition from the strong-field observable models.
The local doc marks this definition as an audit alias: the older strong-field observable channel witness remains valid and is reused rather than re-proved.
proof idea
One-line definitional wrapper. The body is exactly the structural witness strongFieldObservableDistinctFromGRWitness from StrongFieldStructural, assigned to the master-theorem type StrongFieldTestsDistinctFromGR. No tactics, no new lemmas, no extra hypotheses.
why it matters
Fills the D5 strong-field channel slot in the scoped theorem-built quantum-gravity master assembly described in this module: the five formerly external master inputs (D2 Regge/EH plus Schläfli Bianchi, D3 many-body amplitude linearity, D4 recognition-tick Page transfer, D5 PTA band, and D5 named strong-field channels) are supplied by canonical witnesses.
That assembly is explicitly not a claim that full physical QG is closed from primitives. Downstream, the module’s closure-status audit records remaining open scope: D2 stays on the canonical product-filter six-tet torus, general triangulation and Lorentzian causal-simplex problems remain open, and the black-hole echo mechanism is not yet horizon-consistent. This alias keeps the older channel witness live on the unconditional route so the master surface can be assembled without reopening strong-field structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.