Pith. sign in
module module high

IndisputableMonolith.Gravity.Analysis.ReggeTTGateBBridge

show as:
view Lean formalization →

Bridge module grounding Gate B of the Regge TT Bloch campaign: the doubled-midpoint table reproduces the preregistered midpoint Bloch phase on the N=4 campaign torus. It equates raw triple-weight moments to the committed spike LHS so production stages can import the certificate without the full symbol-program chain. Algebraic closers cite it for the C8 form and TT isotropy value. Proofs are leaf-algebra equalities plus phase grounding at the base cell.

claimOn the base cell of the $N=4$ campaign torus, for every momentum $k$ and slot the local-edge midpoint Bloch phase equals $\sum_i k_i\,(\mathrm{slotMidTwice}\,t\,f\,i)/2$. The module identifies core weights, polynomial edge coefficients, and raw triple-sum moments with the committed spike left-hand side, so the doubled-midpoint table matches the preregistered periodic geometry phase.

background

Lane C of the QG full-theory finishing charter (Paper C / Pillar 1) splits the Regge transverse-traceless (TT) Bloch analysis into gates. Gate B is the spike-convention bridge: it must show that a preregistered algebraic certificate (the committed spike transcription) agrees with the geometric midpoint phases and stencil moments of the periodic lattice, without dragging the full symbol-program import graph into every consumer.

The hinge-aware zero-mode module (Gate C-A3) already closed the zero-mode sector. The Bloch-convention audit is a non-production sidecar that folds the interface moment as a stencil rather than wiring it to spike blocks. The leaf core module isolates the heavy polynomial algebra (ring normalizations of order ~200 terms) behind a minimal import of the committed spike and basic real arithmetic.

This bridge re-exports those pieces and states the grounding equalities: edge midpoint phase from the doubled-midpoint table, core weight and edge-coefficient identities, bucket keys, raw phase quadratics, triple weights, and the equality of the Regge TT moment to the raw triple sum and to the committed spike LHS.

proof idea

Not a single theorem: a thin production-facing shell over three imports. Heavy ring/linear-combination work lives in the leaf core (committed spike only). Hinge-aware zero mode supplies the Gate C-A3 zero-mode context; the Bloch audit supplies convention checks without entering the production DAG.

Sibling results are mostly definitional or one-line algebraic identities: midpoint phase grounding at the base cell (cell-relative offsets), core weight and polynomial edge coefficients equal to raw forms, slot dispersion core equality, bucket-key and support lemmas, raw phase quadratic and triple-weight expansions, then reggeTTMoment as a raw triple sum and the raw moment equal to the committed spike LHS. No continuum limit or isotropy evaluation happens here.

why it matters in Recognition Science

Sole bridge into production for the committed algebraic certificate spike. The algebraic closer (stage C-DAG3 in the panel-locked order ReggeTTBlochAssembly → ContinuumLimit → AlgebraicCloser → ContinuumCloser) is the only production importer of that spike, and it imports through this chain. That closer delivers the C8 closed form $(1/2),x^{\mathsf T}\mathrm{adj}(E),x$ and the TT isotropy value $-1/4$.

Without the grounding equalities, Gate B would remain an audit-only claim and the continuum TT isotropy certificate could not cite the spike. The module therefore closes the Lane C Gate C-B charter item and keeps the heavy algebra out of every downstream file. Framework context is discrete Regge gravity on the periodic torus, not the T0–T8 forcing chain directly; it supports the gravity-sector continuum limit that later meets RS units and the eight-tick structure.

scope and limits

used by (1)

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

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (13)