d2_regge_field_is
plain-language theorem explainer
Definitional disclosure that the master theorem's D2 Regge→EH continuum field is exactly the concrete physical product-filter convergence proposition (a universal claim over refinement data), not True and not the master conclusion. Gravity auditors and referees checking non-circularity of the unconditional QG master theorem cite this. Proof is a one-line rfl equality against the canonical witness packing.
Claim. By definition, the Regge-to-Einstein-Hilbert continuum field of the canonical Regge/EH-and-Bianchi witness equals the concrete physical proposition: for every product-filter refinement datum $D$, the full nonlinear Regge aggregate converges to the supplied continuum Einstein-Hilbert/Dirichlet integral on that filter.
background
This module is a field-by-field non-circularity audit of the unconditional quantum-gravity master theorem. A referee objection is that witness structures of shape $\Sigma(P:\mathrm{Prop}), P$ can be inhabited by trivial placeholders. The audit answers by disclosing, for each atom, exactly which proposition sits in the slot and proving that proposition holds on its own.
The D2 slot is the Regge calculus continuum limit. Upstream, concretePhysicalRegEHContinuumProp is the physical content: for any product-filter refinement data $D$, the Track-1 residual target holds (nonlinear Regge aggregate converges to the continuum EH/Dirichlet integral). The canonical witness packs that proposition into regge_to_einstein_hilbert_continuum together with a separate Schläfli contracted discrete Bianchi field.
Local classification distinguishes trivial placeholders from inhabited certificates and carried physics. This declaration is the disclosure half for D2 Regge→EH: it pins the field to a named, non-self-referential convergence statement.
proof idea
One-line term proof by rfl. The canonical witness is defined by setting regge_to_einstein_hilbert_continuum := concretePhysicalRegEHContinuumProp, so the equality is definitional. No lemmas are applied; inspection of the witness constructor is the entire argument.
why it matters
Closes the peer-review non-circularity demand (F1 / Rec 2) for the D2 continuum field: a reader can see by definitional equality that the master theorem does not smuggle in its own conclusion or a tautology. The packed proposition is the genuine product-filter Regge→EH convergence content required by discrete gravity, paired in the same witness with the contracted Bianchi identity.
Downstream the module assembles independent field disclosures and standalone holds proofs so the master conjunction is built from concretely named atoms. No used_by edges are recorded for this disclosure itself; it is audit surface for human and machine inspection of the unconditional master packing. Framework role is gravity-side continuum recovery of Einstein-Hilbert from Regge data, not the T0-T8 forcing chain directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.