honest_scope_statement
plain-language theorem explainer
All five structural witnesses required by the RS quantum-gravity master theorem are inhabited: Regge–EH continuum plus Bianchi, unconditional amplitude-linear forcing, Page-curve derivation, PTA stochastic GW distinct from inflation, and strong-field tests distinct from GR. Anyone auditing Session-102 structural closure cites this. The proof is a pure term packing the five named witnesses into a five-fold Nonempty conjunction.
Claim. The following five hypothesis-interface types are inhabited: (i) Regge–Einstein–Hilbert continuum limit with Bianchi identity, (ii) amplitude-linear channel forcing without a factor-product axiom, (iii) Page-curve derivation, (iv) RS PTA stochastic gravitational-wave background distinct from inflationary tilt predictions, and (v) strong-field tests distinct from GR.
background
Track 7.A packages the RS quantum-gravity master theorem in fully structural form: zero free hypothesis inputs, zero sorry, zero RS-internal axioms. Session 97 began with five open hypothesis slots; Sessions 100–102 retired them by supplying structural witnesses (canonical inhabitants of named Prop-carrying structures), leaving nine clauses at full theorem grade and five discharged structurally.
Each witness is a structure with a named proposition field and a holds proof. Upstream examples: ptaDistinctFromInflationWitness inhabits the PTA-distinct-from-inflation slot via an algebraic log φ > 0 style separation; AmplitudeLinearForcedUnconditional and PageCurveDerived are the Track 2.C/2.D and Track 3.C slots, still structural rather than dynamical. The module doc is explicit that this is the structural skeleton only.
The unconditional (dynamical) master theorem still needs geometric residual estimates for physical Regge triangulations, Schläfli identities, ledger-dynamical Page-curve evolution, and observational deviation patterns.
proof idea
Pure term-mode construction. The goal is a five-fold conjunction of Nonempty for the five master-theorem hypothesis structures. Each conjunct is discharged by wrapping the corresponding structural witness (regEHContinuumAndBianchiWitness, amplitudeLinearForcedUnconditionalWitness, pageCurveDerivedWitness, ptaDistinctFromInflationWitness, strongFieldDistinctFromGRWitness) in a Nonempty.intro. No tactics, no rewriting, no further lemmas.
why it matters
This is the honesty gate for the structural master theorem. Downstream, masterTheoremStructuralCert records all_hypotheses_inhabited := honest_scope_statement alongside the structural master statement and the Session-102 closure status. Without it, the cert could not claim zero open hypothesis inputs.
In the Recognition framework it marks the end of the Session 97→102 retirement trajectory (PTA, strong-field, Page curve, amplitude-linear, Regge–EH/Bianchi all structurally filled). It does not touch T5–T8 forcing, the RCL, or the mass ladder; it is gravity-track bookkeeping. The doc-comment’s open list (dynamical upgrades of all five witnesses, master paper, §7 falsifier register, six §8 done-criteria) remains the path to the discovery-grade unconditional theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.