Pith. sign in
module module moderate

IndisputableMonolith.Gravity.Analysis.ReggeTTGateBBridgeCore

show as:
view Lean formalization →

Literal rational raw-coefficient table for the Regge TT core stencil, identifying kernel weights with the continuum spike sum. Gravity analysts closing Gate B (spike convention bridge) cite it when folding the raw stencil into tetBlock moments. The module is mostly definitional equalities: six core-block identities plus one triple-sum match to the spike sum.

claimThe module fixes the rational core weights, slot dispersions, and triple-term coefficients of the Regge TT raw stencil, and records the identities $\mathrm{coreBlock}_i = \mathrm{spikeBlock}_i$ for $i=0,\ldots,5$ together with equality of the core triple sum to the continuum spike sum.

background

In the Recognition Science gravity stack, Regge TT analysis compares a discrete tetrahedral stencil to a continuum spike certificate. Gate C-A2f identifies the kernel with the raw Jacobian coefficient; this module supplies the matching literal rational table for the core (support / phase-quadratic / amplitude) pieces.

Sibling definitions introduce the core weight, slot dispersion, midpoint doubling, polynomial edge coefficients, and the triple term that assemble each block. The six block equalities and the summed identity coreTripleSum_eq_spikeSum are the algebraic spine.

Upstream material lives in the continuum certificate spike module. Downstream, Gate B instantiates the interface moment fold on support, phase quadratic, and amplitude built from this raw stencil.

proof idea

Definition-and-table module, not a deep proof development. Core weights and polynomial edge coefficients are fixed as rationals; each coreBlock_i_eq is a direct algebraic identification of that block with the corresponding spike block expression. The closing lemma equates the sum of the six core triple terms to the committed spike sum by assembling those block identities (big-operator / Fin arithmetic from Mathlib).

why it matters in Recognition Science

Feeds ReggeTTGateBBridge, which closes the panel-locked Gate B target of the Bloch convention audit: the interface moment fold reggeTTMoment, built from the actual raw stencil, equals the committed spike LHS (sum of tetBlock0 through tetBlock5) under the seven TT hypotheses. That bridge is QG full-theory campaign Paper C / Pillar 1, Lane C of the finishing charter. Without this coefficient table, the Gate B convention match has no concrete kernel to fold. It is the arithmetic substrate linking discrete Regge TT moments to the continuum spike certificate in the gravity analysis lane.

scope and limits

used by (1)

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 (12)