module module moderate

`IndisputableMonolith.Gravity.Analysis.ReggeTTBlochAssembly`

Finite Bloch assembly for Regge TT modes on periodic lattice cells: natural vertex coordinates, bit-split cube/slot displacements, wrap phases, and the raw cosine evaluator with bucket support. Gravity analysts cite it as the discrete Fourier bookkeeping layer between hinge-aware zero mode and the continuum two-jet limit. The module is definitional assembly over classical cell-sum orthogonality, not a single theorem.

claimOn a periodic Regge lattice cell, assign natural coordinates to vertices, decompose cube and slot displacements into bit data, and form wrap counts and slot phases. Build the raw cosine evaluator on those phases together with its bucket-key support, so the discrete Fourier cell sum folds into finite buckets before any continuum limit.

background

This module sits in the quantum-gravity full-theory campaign (Paper C / Pillar 1), after the hinge-aware zero-mode gate and the pure discrete-Fourier cell-sum identities. BlochCellSum supplies classical orthogonality on Fin N index cubes (torus cells) with Mathlib-only analysis and no physics claims. ReggeTTHingeAwareZeroMode closes Gate C-A3 for transverse-traceless Regge modes that know about hinges.

The assembly layer turns that geometry into explicit discrete data: natural representatives of periodic vertex coordinates, bit extractions for cube vertices and slot bases/displacements, midpoints, wrap counts and turns, and the resulting slot phase. From those it defines a raw cosine evaluator, a bucket key, and the support of the cosine sum over buckets.

Notation is lattice-combinatorial rather than continuum: phases live on the discrete torus cell, and the cosine is the real part of the Bloch character used in the finite fold. No continuum certificate is claimed here.

proof idea

Definition and assembly module, not a monolithic proof. It wires coordinate and bit helpers (vertex natural coordinates, cube/slot vertex and displacement bits, midpoints) into wrap counts, wrap turns, and slot phases. Those feed a raw cosine evaluator, a bucket-key map, and the declared support of the raw cosine sum. Analytic content is imported: cell-sum orthogonality from BlochCellSum and the hinge-aware zero-mode setup from the upstream Regge TT gate. Downstream continuum work treats the resulting finite raw bucket fold as given.

why it matters in Recognition Science

Parent consumer is ReggeTTContinuumLimit (C-DAG2 continuum stage). That module "imports the finite Bloch assembly and no continuum-certificate spike": exact Bloch orthogonality has already removed the cell sum, so the continuum proof reduces to a local cosine two-jet limit of the finite raw bucket fold, including the reusable scale limit on the raw cosine fold.

In the campaign chain this is the bookkeeping bridge between Gate C-A3 (hinge-aware zero mode) and the continuum two-jet statement. It does not itself force $D=3$ or the eight-tick octave; those live earlier in the forcing chain. Its job is to make the discrete TT Bloch data explicit enough that the continuum stage can quote a finite fold rather than an unresolved cell sum.

scope and limits

Does not prove continuum or two-jet limits; that is ReggeTTContinuumLimit.
Does not re-prove Bloch cell-sum orthogonality; imports it as classical discrete Fourier fact.
Does not close hinge-aware zero mode; assumes ReggeTTHingeAwareZeroMode.
Does not claim physical values of G, c, or alpha; pure discrete assembly.
Does not assert continuum certificates or spike removals beyond the finite fold.

used by (1)

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

IndisputableMonolith.Gravity.Analysis.ReggeTTContinuumLimit module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.Analysis.BlochCellSum module_import
IndisputableMonolith.Gravity.Analysis.ReggeTTHingeAwareZeroMode module_import

declarations in this module (26)

def vertexNatCoord L36
def cubeVertexBit L42
def slotBaseBit L48
def cubeDispBit L53
def slotDispBit L59
def slotMidTwice L65
def slotWrapCount L71
def slotWrapTurns L76
def slotPhase L81
def rawCosineEvaluator L87
def bucketKeyOf L95
def rawCosineSupport L101
def rawTripleWeight L105
def rawBucketAmplitude L112
theorem addBit_val_real L116
theorem vertCoord_addVertexBits L134
theorem slotMidTwice_eq_geometry L146
theorem localEdge_phase_decomposition L161
theorem cos_localEdge_eq_cell_slot L196
theorem rawCosineEvaluator_bucketKeyOf L211
theorem neg_rawCellStencilTerm_eq L232
theorem rawCosineFold_eq_rawTripleSum L249
theorem rawTriple_cellSum L267
theorem rawCellStencil_eq_rawCosineBlochFold L300
theorem canonicalFiniteH_eq_rawCosineBlochFold L387
theorem eventually_canonicalFiniteH_eq_rawCosineBlochFold L399