Pith. sign in
module module high

IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochData4D

show as:
view Lean formalization →

Data module packing the 4D unit-cell edge-pair couplings for the exact midpoint Bloch symbol of the flat Regge Hessian. It exposes a named Coupling type and a finite coupling table (about 1208 entries, split across couplingChunk0–10) that later modules treat as the coefficient source of a trig polynomial in Bloch momentum. Anyone proving symbol vanishing, cosine two-jet limits, or the midpoint m² TT identity cites this table. There is no proof content: pure structured constants.

claimA finite table of unit-cell edge-pair couplings $C_{e,e'}$ for the exact midpoint Bloch symbol of the flat 4D Regge Hessian, packaged as named chunks that assemble into a single coupling table of length on the order of $1208$. Each entry is one rational (or integer-scaled) weight for a pair of edges in the unit cell, later summed against plane-wave phases $e^{ik\cdot\Delta x}$ to form the Bloch trig polynomial.

background

In discrete Regge gravity one linearizes the action about a flat triangulation and passes to Bloch (Floquet) modes on the periodic unit cell. The exact midpoint discretization yields a quadratic form in edge-length perturbations whose momentum-space kernel is a trigonometric polynomial: a finite sum of cosines (and sines) weighted by edge-pair couplings.

This module is the coefficient warehouse for that polynomial in four spacetime dimensions. It defines a Coupling record for one edge-pair contribution and stores the full table as successive chunks (couplingChunk0 …), so downstream code can name couplingTable without regenerating combinatorics. The surrounding analysis stack treats the table as immutable input to symbol constructions, zero-momentum identities, and m² transverse-traceless projections.

The local setting is pure data: Mathlib only, no analytic lemmas here. Analytic content lives in importers that turn the table into a named trig polynomial and prove continuum limits or algebraic identities.

proof idea

This is a definition and data module; there are no theorems or tactic proofs. Structure is: a small Coupling type for one unit-cell edge-pair weight, then a sequence of concrete chunk definitions that concatenate to the full coupling table used by the Bloch-symbol stack. Downstream modules read the table by name and discharge coefficient identities with native_decide or integer kernel certificates.

why it matters in Recognition Science

Every Stage-1 exact-midpoint Bloch argument in this gravity analysis path imports the table. ReggeExactFlatHessianBlochSymbol4D names the flat Hessian as a finite trig polynomial over the 1208 couplings and routes centered cosine two-jet limits through weight/phase wrappers. ReggeExactFlatHessianBlochSymbolZero4D expands the zero-momentum symbol as a quartic form with rational coefficients read from the table and kills all coefficients by decision procedures; the companion KernelGlue lifts integer qNum certificates to rational qCoeff without pulling the heavier m² stack.

The midpoint m² TT identity modules (ReggeExactMidpointM2TTIdentity4D and its KernelCert/KernelGlue companions) likewise treat these couplings as the source of the m² coefficient arrays, closing exact_midpoint_m2_tt_identity via generated integer fold certificates and scale-32 tables. Without a single canonical coupling table, those symbol-zero and TT identities would not share a common coefficient basis.

scope and limits

used by (6)

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

declarations in this module (19)