Pith. sign in
module module moderate

IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DKernelCert

show as:
view Lean formalization →

Banks the Int-encoded kernel certificate data for the 4D Regge exact midpoint Bloch m² TT identity. Gravity analysts cite it when discharging rational coefficient identities by kernel `decide` after clearing denominators. The module is a generated, chunked coupling table (CZ, edge displacements, doubled midpoint offsets) imported from the flat Hessian Bloch data, not a proof script.

claimInt-encoded midpoint Bloch coupling bank for 4D Regge calculus: rational Hessian couplings $s=p/q$ cleared to integers, edge displacements $\Delta e,\Delta e'\in\{0,1\}^4$, and doubled midpoint offsets $\delta_2=2(\mathrm{mid}_e-\mathrm{mid}_{e'})$, chunked so that kernel `decide` can certify the $m^2$ TT coefficient identities (and related symbol-zero quartics) after fixed integer scales.

background

In the 4D Regge analysis, the flat Hessian of the action is evaluated on midpoint Bloch modes. Couplings are rational; edge pairs carry binary displacements and a doubled midpoint offset. The upstream module ReggeExactFlatHessianBlochData4D is the auto-generated rational table (script regge_4d_exact_m2_table_20260721.py), chunked to stay under Lean maxRecDepth.

This certificate module re-encodes that table for kernel decision procedures: denominators are cleared to an integer bank (couplingZList / CZ chunks), with edge data De, Dep and doubled offset D2. Downstream consumers scale further (e.g. factor 8 relating m2Num to explicitZ, or scale 16/32 for quartic symbol-zero coefficients) so that identities become pure integer equalities.

Local setting is discrete gravity / Regge calculus on a 4D lattice, restricted to the exact flat Hessian midpoint Bloch sector used to prove the $m^2$ transverse-traceless identity.

proof idea

Definition and data module, not a theorem proof. It exposes the Int coupling bank (CZ, toCZ), displacement and offset projections (De, Dep, D2), a contribution map (contrib), and chunked tables (czChunk0–czChunk5) so elaboration stays bounded. Downstream kernel certificates import these arrays and run decide (no native_decide) on cleared integer equalities; glue modules then lift the Int folds back to the $\mathbb{Q}$ coefficient tables of the main identity.

why it matters in Recognition Science

Feeds the closure of the exact midpoint Bloch $m^2$ TT identity in 4D (ReggeExactMidpointM2TTIdentity4D) and the algebraic glue that connects Array-sum $m^2$ coefficients to Int folds and scale-32 tables (ReggeExactMidpointM2TTIdentity4DKernelGlue). Also supplies the banked KernelCert.couplingZList reused by the symbol-zero quartic vanishing certificate (ReggeExactFlatHessianBlochSymbolZero4DKernelCert) and by the m2Num = 8·explicitZ chunk modules (256 kernel decides each).

Without this Int bank, the rational midpoint identities cannot be discharged inside the kernel. It is the certificate substrate for the generated Regge 4D $m^2$ TT pipeline (regge_4d_m2_tt_identity_20260721.py / kernel cert scripts), sitting under the broader gravity analysis that supports discrete curvature and continuum-limit checks in the Recognition framework.

scope and limits

used by (22)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (46)