module module high

`IndisputableMonolith.Gravity.Analysis.ReggeBlochFold4D`

Factorized Bloch fold for the 4D Regge (1,1) hinge orbit, with a zero-momentum consistency gate against the committed flat Hessian quadratic. Continuum and symbol analysts on the Freudenthal lattice cite it before multi-orbit folds and m² expansions. The module is mostly definitional packaging plus algebraic linearity and orbit-count identities.

claimOn the 4D Freudenthal lattice, the factorized Bloch fold over $(1,1)$ hinge slots equals the committed flat second-variation quadratic of that orbit at vanishing Bloch momentum $k=0$. The module supplies phased class-dots, the $(1,1)$ slot predicate, factorized slot terms, and the natural/real $(1,1)$ counts used in that gate.

background

This sits in the QG full-theory campaign for 4D Regge calculus on the Freudenthal (Kuhn) triangulation of the 4-cube. Upstream modules fix the 15-class edge stencil, triangle-hinge orbit types under $S_4$ (with complement), star deficit kernels, and the flat Hessian assembled from Heron area gradients with true zero-momentum weights, replacing the provisional weight-1 aggregate.

A Bloch fold packages the second variation as a momentum-dependent quadratic form on edge classes. The $(1,1)$ orbit is the shortest hinge type and the natural first consistency check: at $k=0$ phases drop out and the fold must recover the already-committed orbit quadratic from the flat Hessian assembly.

Sibling objects include coordinate masks, hinge bases, a phased class-dot (linear in the class vector), the $(1,1)$ predicate via pop-count, factorized slot terms, and natural/real counts of $(1,1)$ slots.

proof idea

Definition-heavy module with short algebraic lemmas, not a long tactic proof. It introduces mask and hinge-base coordinates, then a phased class-dot with additivity, scalar homogeneity, and a zero-momentum reduction to the unphased class-dot. The $(1,1)$ slot predicate is tied to a pop-count characterization. Factorized slot terms and the factorized $(1,1)$ Bloch fold are assembled from those pieces; natural and real $(1,1)$ counts support the zero-momentum consistency gate against the committed orbit quadratic. No continuum limit or multi-orbit sum is proved here.

why it matters in Recognition Science

This is the consistency gate named in the module doc: factorized fold at zero momentum recovers the committed $(1,1)$ orbit quadratic. Downstream, ReggeBlochAllOrbitSymbol4D consumes the same factorization pattern over all six $S_4$ hinge types; ReggeBlochM2Symbol4D expands the small-momentum ($m^2$) symbol of the $(1,1)$ fold; orbit-transport, star-edge-origin, local-incidence, and transported all-orbit modules import the fold API; the transported algebraic closer banks identities without claiming Einstein-Hilbert Tendsto. In the campaign ladder it sits after stencil, orbit classification, star kernels, and flat Hessian assembly, and before full multi-orbit Bloch symbols and continuum preflight.

scope and limits

Does not prove Einstein-Hilbert continuum convergence or any Tendsto rate.
Does not alone assemble the full six-orbit Bloch symbol; only the (1,1) factorized fold and gate.
Does not redefine stencil, star kernels, or flat Hessian weights; imports them.
Does not claim positivity, spectrum gaps, or TT projection beyond the zero-momentum match.
Does not treat curved backgrounds or non-periodic lattices.

used by (8)

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

IndisputableMonolith.Gravity.Analysis.Regge4DTransportedAlgebraicCloser module_import
IndisputableMonolith.Gravity.Analysis.ReggeBlochAllOrbitSymbol4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeBlochFold4DAudit module_import
IndisputableMonolith.Gravity.Analysis.ReggeBlochLocalIncidence4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeBlochM2Symbol4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeBlochOrbitTransport4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeBlochStarEdgeOrigins4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeBlochTransportedAllOrbit4D module_import

depends on (5)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.Analysis.ReggeEdgeStencil4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeFlat4DHessianAssembly module_import
IndisputableMonolith.Gravity.Analysis.ReggeHinge4DFlatKernel module_import
IndisputableMonolith.Gravity.Analysis.ReggeHinge4DOrbitClassification module_import
IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel module_import

declarations in this module (82)

def maskCoord L69
def hingeBase L72
def phasedClassDot L75
theorem phasedClassDot_add L78
theorem phasedClassDot_smul L85
theorem phasedClassDot_zeroMomentum L93
def isT11 L102
theorem isT11_iff_pop L108
def factorizedSlotTerm L119
def factorizedBlochFold11 L127
lemma t11_count_nat L130
lemma t11_count_real L145
theorem factorizedBlochFold11_zeroMomentum L156
def transportPermOfDiff L185
def permClass L201
def transportedDeficit L208
def slotTransportPerm L214
def slotAreaCov L217
def slotDeficitKer L223
def transportedSlotTerm L226
def blochFold11 L234
def blochFold11Bilinear L237
theorem blochFold11_eq_bilinear L247
theorem blochFold11Bilinear_symm L270
theorem blochFold11Bilinear_add_left L279
theorem blochFold11Bilinear_smul_left L293
theorem transportedSlotTerm_zeroMomentum L319
theorem classCoeff_axisTTPlus_mask_1 L330
theorem classCoeff_axisTTPlus_mask_2 L336
theorem classCoeff_axisTTPlus_mask_3 L342
theorem slotAreaCov_support L348
theorem phasedClassDot_area_axis_of_masks_1_2 L357
theorem phasedClassDot_area_axis_of_masks_2_1 L382
theorem transportedSlotTerm_axis_seedMasks L407
def waveStar L425
def axisStarKind L431
def axisStarContrib L440
def gaugeStarKind L445
def gaugeStarContrib L448
theorem axisStarKind_count1 L451
theorem axisStarKind_count2 L456
theorem gaugeStarKind_count1 L461
theorem sum_axisStarContrib L467
theorem sum_gaugeStarContrib L502
def baseTurns L529
def dispTurns L535
def quarterTurns L541
def cosC1 L545
def cosC2 L551
lemma waveStar_dot_maskCoord L558
lemma waveStar_dot_classDisp L569
theorem classMidpointPhase_waveStar L579
theorem cos_quarterTurns L588
def slotAreaCovZ4 L627
lemma slotAreaCov_eq_cast L632
def slotA1 L638
def slotA2 L643
def slotK1 L648
def slotK2 L654
def slotN1 L660
def slotN2 L666
theorem phasedClassDot_transportedDeficit L673
theorem phasedA_waveStar L696
theorem phasedK_waveStar L711
theorem transportedSlotTerm_waveStar_eval L727
def axisCertN1 L746
def axisCertN2 L750
def gaugeCertN1 L755
def gaugeCertN2 L759
theorem slotN_axis_match L766
def decoyGaugeCoeffZ L773
theorem classCoeff_decoyGauge_int L775
theorem slotN_gauge_match L785
theorem transportedSlotTerm_axis_waveStar L793
theorem transportedSlotTerm_gauge_waveStar L807
theorem blochFold11_axisTTPlus_waveStar L821
theorem blochFold11_axisTTPlus_waveStar_ne_zero L828
theorem blochFold11_decoyGauge_waveStar L835
theorem blochFold11_decoyGauge_waveStar_ne_zero L841
structure BlochFold4DStatus L852

… and 2 more