Pith. sign in
def

reggeTTMoment

definition
show as:
module
IndisputableMonolith.Gravity.Analysis.ReggeTTBlochInterfaceAudit
domain
Gravity
line
215 · github
papers citing
none yet

plain-language theorem explainer

Defines the Regge TT moment as a Bloch-bucket fold of amplitudes against the cosine two-jet weight −q/2, where q is a caller-supplied phase quadratic. Gravity continuum and algebraic-closer theorems cite it as the production moment surface for TT polarizations. The body is a one-line wrapper around the existing Bloch fold.

Claim. Given a finite support of buckets, a phase-quadratic map $q$ on buckets, and an amplitude map $a$ on buckets, the Regge TT moment is the Bloch fold of $a$ against the weight $b \mapsto -q(b)/2$. That weight is the cosine two-jet value at the frozen $x(1/4)$ normalization encoded by $q$.

background

This module is the panel-locked C11 Regge TT Bloch interface audit (attempt 2). It keeps the first gate deliberately non-tautological: the raw cell stencil is a literal $6\times6\times6$ triple sum over tetrahedra and ordered slot pairs, and the A2 reduced second variation is identified with that sum by distributing a finite inner sum (sign matching the live A2 theorem: negative Schläfli-reduced contraction).

A bucket is a triple (left slot, right slot, phase vector) with slots in $\mathrm{Fin},6$; the intended external convention only identifies $(f,g,u)$ with $(g,f,-u)$, and this attempt does not yet quotient fibers. The moment surface does not claim full rational bucket aggregation or assembled zero-mode cancellation. Gate A2-full, Gate A3 (hinge-aware zero-mode), and Gate B (spike convention bridge) remain open; no ContinuumLimit or spike certificate module is imported here.

The cosine two-jet route is the intended path once the hinge/diagonal constant block is formally connected: the stencil-only constant block has a nonzero residual on the reported TT witness.

proof idea

One-line definitional wrapper. It applies the in-module Bloch fold reggeTTBlochFold on the given support and amplitude, substituting the weight $b \mapsto -(q(b))/2$ for the phase-quadratic $q$. No further algebraic reduction or tactic proof is present.

why it matters

This is the production moment evaluator that the algebraic closer and continuum-limit campaign hang on. Downstream, continuumMoment_eq_bridgeMoment identifies the continuum bucket fold with the Gate B bridge fold; bridgeMoment_eq_half_adjugate and the headline continuumMoment_eq_half_adjugate then close the C8 form: the continuum moment equals $\tfrac12 x^{\mathsf T}\mathrm{adj}(E)x$ for every symmetric polarization $E$ and real direction $x$.

The TT specialization theorems reggeTTMoment_tt_real and reggeTTMoment_tt_value (P1.1b headline) evaluate the same fold at unit-normalized real TT data to the continuum coefficient $-1/4$. Gate B's open target proposition is literally a statement about instances of this moment matching the committed spike LHS under the seven TT equations, without using the continuum certificate.

In the broader RS gravity stack this sits under the discrete Regge second-variation analysis feeding continuum TT coefficients; it does not itself touch T5–T8 forcing, RCL, or the alpha band.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.