closureStatus_unconditional_has_open_target
plain-language theorem explainer
The unconditional gravity master-theorem closure record still flags at least one load-bearing physical target as open; on the current route that target is D2 quadrature. Auditors and certificate writers cite this to block treating scoped witnesses as full quantum-gravity recovery. The proof is a one-line left injection of reflexivity on the D2-open field.
Claim. In the unconditional master-theorem closure-status record, at least one of the following holds: D2 quadrature is open, general triangulation is open, tensor $TT$ recovery is open, Lorentzian causal triangulations are open, the boundary Gibbons–Hawking–York term is open, or the echo mechanism is open or rejected.
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 remains the audit surface; this file supplies the canonical zero-argument route through it.
The upstream record closureStatus_unconditional is intentionally conservative: theorem-built witnesses are marked installed, yet full physical closure is false. Its fields keep D2 quadrature, general triangulation, tensor $TT$ recovery, and related targets open so downstream papers cannot count scoped witnesses as complete physical recovery.
D2 content on the primary route is physical: Regge/EH continuum convergence of the normalized nonlinear Regge aggregate on the canonical periodic six-tet cubic torus under product-filter refinement, plus the contracted discrete Bianchi identity at every vertex for Schläfli-satisfying Regge data.
proof idea
One-line term proof. The first disjunct is d2_quadrature_open = true. That field is definitionally true in the upstream record, so rfl discharges the equality and Or.inl injects it into the six-way disjunction. No other fields are inspected.
why it matters
This is a guardrail, not a physics derivation. The parent record states that the theorem-built assembly exists but the full physical quantum-gravity framework is not closed. Naming an explicit open target (D2 quadrature on the scoped route) stops certificates from equating the unconditional witness package with complete recovery of continuum EH, general triangulations, tensor $TT$ modes, Lorentzian CDT, boundary GHY, or echo mechanisms.
No downstream consumers are wired yet; the declaration sits at the end of the unconditional closure surface. In the broader RS gravity stack it pairs with the master theorem handoff, page-curve, PTA, and strong-field structural modules imported here, keeping the audit honest while the D2 quadrature and related targets remain open work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.