Pith. sign in
module module moderate

IndisputableMonolith.Gravity.Track1BCStructural

show as:
view Lean formalization →

Structural packaging for gravity Tracks 1.B–C: flat-substrate Regge action, Regge-to-Einstein–Hilbert continuum witness, and discrete Bianchi (Schläfli) witness, bundled as one certificate. Gravity master-theorem structural form and physical residual upgrades import this bundle. Argument shape is definitional witness assembly and conjunction, not a dynamical continuum derivation.

claimOn the flat substrate the abstract Regge action $S_{\mathrm{Regge}}(a)$ vanishes for every lattice spacing $a$. The module supplies canonical witnesses that the Regge–Einstein–Hilbert continuum structural proposition and the discrete Bianchi structural proposition both hold, and packages them as the joint Track 1.B–C structural certificate.

background

Recognition Science gravity splits continuum recovery of Einstein–Hilbert from discrete curvature identities. Track 1.B is the Regge-to-EH continuum interface; Track 1.C is discrete Bianchi via the Schläfli identity on a simplicial complex.

This module sits at the structural-witness layer. The abstract Regge action is a function of lattice spacing that, on the flat substrate, is identically zero; the spacing argument is intentionally unused in the canonical-witness form. An abstract EH action is paired with it. Structural propositions name the continuum and Bianchi claims; canonical witnesses inhabit those propositions.

Upstream, Geometry.DiscreteBianchi closes Track 1.C as a structural theorem (0 sorry, 0 RS-internal axiom). Gravity.MasterTheorem authors the conditional Track 7.A master statement gated on the seven tracks. Local exports are the joint holding proposition, the paired witness, and the named certificate used by downstream structural and physical residual modules.

proof idea

Definitional packaging, not a deep derivation. Abstract Regge and EH actions are introduced; the flat-substrate Regge action is the zero function of spacing. Structural propositions for Regge–EH continuum and discrete Bianchi are stated, each with a canonical witness (flat zero action; DiscreteBianchi import). A joint proposition asserts both hold, inhabited by a pair witness. The certificate type and its value expose that bundle for import. No curvature computation or dynamical continuum analysis runs in-file.

why it matters in Recognition Science

Feeds Gravity.MasterTheoremStructural, which pre-fills all five hypothesis inputs of the Track 7.A master theorem with structural witnesses to obtain the fully structural (zero hypothesis input) master form. Also feeds Gravity.Track1BCPhysicalResidual, which treats this flat-substrate witness as baseline and upgrades it with physical finite-probe Regge-to-EH residual theorems from the six-tetrahedra cubic Dirichlet instance.

In the quantum-gravity master plan, Tracks 1.B and 1.C gate the master theorem. This certificate is the structural closure those gates report into before physical residuals and unconditional upgrades. It freezes the interface later modules refine; it does not replace dynamical continuum proofs.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (14)