Pith. sign in
module module moderate

IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochTorusBridge4D

show as:
view Lean formalization →

Bridges the exact midpoint Bloch flat-Hessian symbol to the shrinking 4-torus family used in the Regge continuum limit. Introduces the continuum scale $2\pi/(j+3)$ and proves centered Tendsto of the rescaled symbol as the torus collapses. Downstream consumers are the Recognition-mesh exact-J bridge and the SRS$\to$EH weak-field export. The argument wires torus-scale asymptotics to the already-named Bloch trig polynomial and its zero-momentum vanishing.

claimOn the periodic Freudenthal 4-torus family at continuum index $j$, with scale $s_j=2\pi/(j+3)$, the exact midpoint Bloch symbol of the flat Regge Hessian, after centering and dividing by $s_j^2$, tends (in the centered sense) to the continuum cosine two-jet target as $j\to\infty$, equivalently $s_j\to 0$. Integer wave modes are related to real momenta by this same scale, and the zero-momentum vanishing of the symbol is inherited.

background

This sits in the QG full-theory 4D continuum closure plan. The preflight module freezes the independent continuum target (weak-field Einstein-Hilbert quadratic action), the canonical mesh carrier, normalized TT data, pure-gauge family, and honesty decoys before any recovery proof. Nothing in preflight proves continuum recovery.

Upstream, the Stage-1 unit-cell exact flat Hessian is named as a finite trig polynomial over a 1208-entry coupling table, and a separate module proves that this exact midpoint Bloch symbol vanishes at zero momentum by expanding it as a quartic form with rational coefficients and discharging all coefficients by native decision over $\mathbb{Q}$.

The present module supplies the torus geometry that turns those unit-cell facts into a continuum family: continuum index $j$, scale $s_j=2\pi/(j+3)$, 4-component waves and $4\times 4$ metric perturbations, and the dictionary between integer torus modes and real momenta.

proof idea

Definition layer first: matrix and wave types, torusScale as $2\pi/(j+3)$, and equalities relating real modes, integer-mode wave norms, and momentum norms to that scale. Non-vanishing of integer-mode wave norms is recorded so later divisions are legal.

Analytic layer: prove $s_j\to 0$ as $j\to\infty$, that $s_j$ is eventually nonzero, and the corresponding nhdsWithin Tendsto away from zero. The main continuum statement specializes the centered trig-polynomial Tendsto (from the Bloch-symbol module) along this torus family, using zero-momentum vanishing to justify the centered quotient by $s_j^2$. Structure is scale bookkeeping plus reuse of the named symbol Tendsto, not a fresh expansion of the 1208 couplings.

why it matters in Recognition Science

Without a torus-family bridge, the named Bloch symbol stays a unit-cell object and cannot feed continuum recovery. This module is the geometric hinge between Stage-1 exact flat Hessian data and the continuum weak-field target frozen in preflight.

It is imported by the Recognition-mesh exact-J bridge, which "constructs the canonical Recognition mesh carrier for the periodic Freudenthal 4-torus and attaches a value-level action whose amplitude Hessian is the geometric Option-C midpoint Bloch symbol on the same torus family." It is also imported by the SRS$\to$EH export that holds the named closers edge_tt_decomposition and S_RS_converges_EH_4d for the ledger flip, and by an audit companion.

In the broader RS gravity campaign this is infrastructure for proving that the discrete Recognition/Regge quadratic action recovers the continuum Einstein-Hilbert weak-field Hessian in $D=4$, not a mass or $\alpha$ claim.

scope and limits

used by (3)

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