IndisputableMonolith.Gravity.Analysis.ReggeBlochM2Tendsto4D
Module for the formal second-jet coefficient of the directional kernel after K(0)=0 in the 4D Regge Bloch m² analysis, plus the tendsto statements that normalize that kernel by squared momentum. Continuum and algebraic-closer authors cite it when wiring the small-momentum symbol into the transported multi-orbit fold. Arguments reduce to cosine two-jet limits imported from the TT continuum stage and elementary continuity of the area factor.
claimAfter imposing $K(0)=0$, the module defines the second-jet coefficient of the directional kernel along a momentum slot, proves $\mathrm{ker}/|q|^2\to$ that coefficient as $q\to 0$, records vanishing on axis and gauge directions, and establishes continuity of the area factor together with a slot-product continuum limit used by the 4D Bloch $m^2$ symbol.
background
In the Recognition Science gravity stack, the 4D Regge Bloch fold assembles finite stencil contributions before any continuum certificate. The upstream module on the small-momentum ($m^2$) symbol of the (1,1) orbit supplies the folded kernel and area factors without redefining Hessians or stencils. Exact Bloch orthogonality has already removed the cell sum, so continuum work is local.
The companion TT continuum module is the C-DAG2 stage: it treats a free real scale and proves a reusable raw cosine two-jet limit of the finite bucket fold. The present module specializes that jet calculus to the directional kernel along a momentum slot, after the algebraic constraint $K(0)=0$ kills the constant term.
Objects introduced here include the area and kernel pulled back along a direction, their zero lemmas (including axis and gauge vanishing), the named second-jet coefficient, continuity of the area factor, and the normalized tendsto $\mathrm{ker}/q^2$ together with a slot-product limit.
proof idea
Definition layer first: directional area and kernel are pullbacks of the upstream symbol data; equality and zero lemmas are immediate from those definitions and from $K(0)=0$. Axis and gauge vanishing follow by specialization of the kernel along those slots.
The second-jet coefficient is the formal quadratic coefficient of the directional kernel. The main analytic content is a tendsto of that kernel divided by squared momentum, obtained by feeding the directional cosine fold into the reusable raw cosine two-jet continuum limit from the TT stage. Continuity of the area factor is a direct continuity argument on the finite fold. The slot-product tendsto multiplies the normalized kernel limit by the continuous area factor.
why it matters in Recognition Science
The transported 4D algebraic closer imports this module to bind a concrete continuum sequence and bank algebraic identities for the multi-orbit fold, without yet claiming Einstein-Hilbert tendsto of $-1/4$ or inhabiting the full $S_{RS}\to EH$ convergence proposition. That closer needs a named $m^2$ coefficient and the normalized kernel limit so the preflight continuum Prop can be attached to the transported fold.
In the broader gravity analysis chain this sits between the (1,1)-orbit $m^2$ symbol and the algebraic closer that packages continuum data for later EH matching. It does not itself close the Einstein-Hilbert continuum claim; it only supplies the second-jet and tendsto ingredients that closer banks.
scope and limits
- Does not claim Einstein-Hilbert continuum tendsto of $-1/4$.
- Does not inhabit full $S_{RS}$ converges to EH in 4D.
- Does not redefine Hessians, kernels, or stencils; imports them.
- Does not treat orbits beyond the directional data used by the (1,1) $m^2$ symbol.
- Does not supply continuum-certificate spikes beyond cosine two-jet limits.
used by (1)
depends on (2)
declarations in this module (19)
-
def
areaAlong -
def
kerAlong -
theorem
areaAlong_eq -
theorem
kerAlong_eq -
theorem
areaAlong_zero -
theorem
kerAlong_zero -
theorem
kerAlong_axis_zero -
theorem
kerAlong_gauge_zero -
def
kerM2Coeff -
theorem
tendsto_kerAlong_div_sq -
theorem
continuous_areaAlong -
theorem
tendsto_slot_product -
theorem
m2SlotCoeff_eq_area_kerM2 -
theorem
tendsto_transportedSlotTerm_div_sq -
theorem
tendsto_foldAlong_div_sq -
theorem
FoldAlongM2Tendsto_of_axisTTPlus -
theorem
FoldAlongM2Tendsto_of_decoyGauge -
theorem
FoldAlongM2Tendsto_axisTTPlus_holds -
theorem
FoldAlongM2Tendsto_decoyGauge_holds