regge_eh_continuum_structural_prop
plain-language theorem explainer
Structural proposition that the abstract Regge action equals the abstract Einstein-Hilbert action at every real lattice spacing. Track 1.B continuum-limit work cites it as the kinematic content of Regge-to-EH convergence under the flat-substrate witness. Defined as a Prop (both abstract actions are the zero function), so equality is the zero-zero identity rather than a nontrivial residual estimate.
Claim. The proposition that for every real lattice spacing $s$, the abstract Regge action evaluated at $s$ equals the abstract Einstein-Hilbert action evaluated at $s$.
background
Track 1.B/1.C in the gravity master theorem packages two structural inputs: discrete-to-continuum convergence of the Regge action to the Einstein-Hilbert (EH) action, and the contracted second Bianchi identity on the Regge substrate. This module ships kinematic Props under named hypotheses, with flat-substrate canonical witnesses for non-vacuous inhabitation.
The abstract Regge and EH actions are spacing-parameterized real-valued functions. In the flat-substrate form both are identically zero (the spacing argument is unused). Lattice spacing itself is the refinement quantity $L/N$ from the unified lattice-manifold correspondence. The doc-comment frames the intended continuum reading as: for spacings tending to zero, the absolute difference of the actions tends to zero; on the flat witness both sides vanish, so the difference is zero.
proof idea
Not a proved theorem: a one-line Prop definition. The body is universal quantification over a real spacing together with equality of the two abstract action functions at that spacing. Because both abstract actions are defined as the constant zero map, any later witness reduces to rfl after unfolding (as in the sibling canonical witness).
why it matters
Fills the Track 1.B half of the structural witness for the master-theorem hypothesis RegEHContinuumAndBianchi (Session 97). Downstream, the canonical witness inhabits it by zero-equality; the combined continuum-and-Bianchi theorem and the one-statement Track 1.B/1.C package both quote it; regEHContinuumAndBianchiWitness and Track1BCStructuralCert wire it into the master hypothesis structure. The physical residual upgrade replaces this flat zero-zero identity by a finite-probe residual theorem under edge-stencil local correspondence. Unconditional Track 1.B closure still needs the geometric residual bound $|S_{\mathrm{Regge}}-S_{\mathrm{EH}}|\le C\cdot\mathrm{spacing}$ on a physical triangulation, outside this structural layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.