Pith. sign in
module module high

IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumAssemble

show as:
view Lean formalization →

Assembly module for the exact midpoint identity relating the 4D Regge m² numerator to eight times an explicit Z-table. It stitches eleven kernel-decide chunks into one equality used by the Bloch TT mass-squared certificate. Gravity analysts cite it when closing the midpoint m² TT identity. The argument is pure import-and-glue of finite kernel certificates.

claimThe 4D Regge midpoint $m^2$ numerator equals eight times the explicit $Z$ coefficient table: $m^2_{\mathrm{num}} = 8\,Z_{\mathrm{explicit}}$, assembled by partitioning the 256-entry kernel into chunks and deciding each chunk.

background

In the Recognition Science gravity stack, the exact midpoint Bloch $m^2$ TT identity is a finite algebraic certificate on 4D Regge edge data. The numerator of the mass-squared expression is reduced to a scaled integer table $Z_{\mathrm{explicit}}$; the factor eight is the combinatorial weight of the midpoint sampling.

Each upstream chunk module states the same equality on a 256-kernel slice and discharges it by decide on integer certificates. This assemble module imports those slices (chunks 0 through 10 and siblings) so a single named equality is available to the parent 4D identity file and to the kernel-glue layer that lifts Int folds to Q coefficient tables.

The local setting is discrete Regge calculus at the exact midpoint configuration, not continuum GR. Notation follows the QG scripts that generate the kernel certs and the scale-32 tables.

proof idea

No independent analytic proof lives here. The module imports the chunk modules, each of which proves $m^2_{\mathrm{num}}=8,Z_{\mathrm{explicit}}$ on its kernel block by kernel decide. Assembly exposes the global equality (sibling m2Num_eq_eight_explicitZ) as the concatenation of those finite certificates. Downstream glue then maps the Int certificates onto the Array-sum and scale-32 Q tables used by the closed 4D identity.

why it matters in Recognition Science

Parent consumers are ReggeExactMidpointM2TTIdentity4D, which closes exact_midpoint_m2_tt_identity, and ReggeExactMidpointM2TTIdentity4DKernelGlue, which lifts kernel decide Int certificates to the Q coefficient tables. Without this assemble step the chunked 256-kernel certificates remain fragmented and cannot feed the midpoint TT mass-squared identity. The work sits in the discrete gravity analysis path (Regge 4D m² TT scripts), not in the T0–T8 forcing chain, but it is load-bearing for the exact algebraic side of the RS gravity certificates.

scope and limits

used by (2)

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

depends on (16)

Lean names referenced from this declaration's body.

declarations in this module (1)