Gravity Analysis Regge Bloch All Orbit Symbol4 D Factorized Bloch Fold All Zero

The zero-momentum fold

In the study of discrete gravity, a ledger (a discrete record of geometric events) can be analyzed by summing contributions from its elementary building blocks. The declaration factorizedBlochFoldAll_zeroMomentum is a theorem about one such sum: it states that when the momentum parameter is set to zero, the full sum over all hinge types equals a single quadratic expression, trueWeightZeroMomQuadratic. This is not a numerical coincidence; it is a proved identity in the machine-checked library of formal theorems.

The sum in question, factorizedBlochFoldAll, adds up contributions from six types of hinges (the edges where triangular faces meet) in a four-dimensional Regge calculus model. Each hinge contributes a product of two terms: one from the area of the hinge and one from the deficit angle (the amount by which the surrounding geometry fails to be flat). The theorem shows that at zero momentum, this complicated product-sum reduces to a quadratic form in the geometry variables. This is a structural simplification: it means the leading behavior of the fold at zero momentum is captured by a simple expression, not by the full product structure.

The theorem has two notable corollaries. For a specific geometry called the axis, the zero-momentum fold equals zero, and for a test configuration called the decoy gauge, it also equals zero. These are not accidents; they follow from the quadratic form vanishing on those inputs. The framework also proves that the fold is an even function of the momentum scale: reversing the sign of the momentum leaves the fold unchanged. This evenness is a symmetry that holds before any limit is taken.

What the theorem does not claim is equally important. It does not prove that the full, non-factorized fold (which transports the (1,1) hinge type) has the same behavior; the theorem is scoped to factorized, orbit-constant kernels. It does not prove recovery of continuum Einstein-Hilbert gravity from this discrete model. And it does not establish the two-jet limit for arbitrary momentum directions; that remains an open problem, explicitly marked as such in the library. The theorem is a precise statement about a restricted case, not a general principle of quantum gravity.

/-- All-orbit fold at zero momentum is the committed true-weight Hessian. -/
theorem factorizedBlochFoldAll_zeroMomentum (H : Mat4) :
    factorizedBlochFoldAll H (fun _ => (0 : ℝ)) =
      trueWeightZeroMomQuadratic H := by
  unfold factorizedBlochFoldAll trueWeightZeroMomQuadratic
  exact Finset.sum_congr rfl fun ty _ =>
    factorizedBlochFoldOrbit_zeroMomentum ty H

theorem factorizedBlochFoldAll_axis_zeroMomentum :
    factorizedBlochFoldAll axisTTPlus (fun _ => (0 : ℝ)) = 0 := by
  rw [factorizedBlochFoldAll_zeroMomentum, trueWeightZeroMomQuadratic_axisTTPlus]

theorem factorizedBlochFoldAll_gauge_zeroMomentum :
    factorizedBlochFoldAll decoyGauge (fun _ => (0 : ℝ)) = 0 := by
  rw [factorizedBlochFoldAll_zeroMomentum, trueWeightZeroMomQuadratic_decoyGauge]

theorem foldAllAlong_even (H : Mat4) (dir : Fin 4 → ℝ) :
    Function.Even (foldAllAlong H dir) :=
  fun μ => foldAllAlong_neg H dir μ

/-- All-orbit fold at zero momentum is the committed true-weight Hessian. -/
theorem factorizedBlochFoldAll_zeroMomentum (H : Mat4) :
    factorizedBlochFoldAll H (fun _ => (0 : ℝ)) =
      trueWeightZeroMomQuadratic H := by
  unfold factorizedBlochFoldAll trueWeightZeroMomQuadratic
  exact Finset.sum_congr rfl fun ty _ =>
    factorizedBlochFoldOrbit_zeroMomentum ty H

What this page does not claim

This theorem does not prove continuum Einstein-Hilbert gravity recovery. This theorem does not apply to non-factorized or transported hinge folds. This theorem does not establish the arbitrary-direction two-jet limit, which remains open.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/Analysis/ReggeBlochAllOrbitSymbol4D.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: