Gravity Analysis Regge Bloch M2 Symbol4 D Transported Slot Term Gauge Zero Momen

The zero-momentum gauge slot

The declaration transportedSlotTerm_gauge_zeroMomentum is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It concerns a term called transportedSlotTerm, a component in a calculation of how a discrete geometric structure, a Regge 4D Bloch fold, behaves at small momenta. The theorem states that when this term is evaluated for a particular configuration, the decoyGauge, at zero momentum, the result is exactly zero.

To understand what this means, consider the broader calculation. The framework analyzes a quantity called blochFold11, which is a function of a 4x4 matrix H and a momentum vector. The calculation examines how this function behaves as the momentum approaches zero, specifically along a chosen direction. The decoyGauge is one specific choice of the matrix H, representing a particular gauge configuration. The theorem proves that for this gauge, the transported slot term, which is a piece of the overall sum, vanishes at zero momentum. This is a concrete algebraic fact, verified by the theorem's proof, which relies on a related lemma about the slot deficit kernel.

The theorem is part of a larger effort to compute the second-order coefficient, the m² symbol, of the Bloch fold. This coefficient is built from a sum over many slots, indexed by s and t. The theorem shows that for the decoyGauge, each individual slot term in this sum is zero at zero momentum. This is a necessary condition for the overall m² symbol of the decoyGauge to be zero, a fact that is separately established. The result is one of two such zero-momentum vanishing theorems; the other concerns the axisTTPlus configuration, where the term also vanishes.

What the theorem does not claim is broader significance. It does not prove that the full Hessian symbol, which would include all contributions, is zero. It does not establish that the Bloch fold converges to the Einstein-Hilbert action, a goal that remains open. It does not address the behavior of the term at non-zero momentum. The theorem is a precise, local statement about one term in a specific gauge at a specific point, and its value lies in being a verified piece of a larger, unfinished calculation.

theorem transportedSlotTerm_gauge_zeroMomentum (s : Fin 24) (t : Fin 10) :
    transportedSlotTerm decoyGauge (fun _ => (0 : ℝ)) s t = 0 := by
  rw [transportedSlotTerm_zeroMomentum]
  by_cases ht : isT11 s t <;> simp [ht, classDot_slotDeficitKer_gauge]

theorem transportedSlotTerm_gauge_zeroMomentum (s : Fin 24) (t : Fin 10) :
    transportedSlotTerm decoyGauge (fun _ => (0 : ℝ)) s t = 0 := by
  rw [transportedSlotTerm_zeroMomentum]
  by_cases ht : isT11 s t <;> simp [ht, classDot_slotDeficitKer_gauge]

What this page does not claim

The theorem does not prove the full Hessian symbol is zero for the decoyGauge. The theorem does not establish convergence to the Einstein-Hilbert action. The theorem does not describe the behavior of the transported slot term at non-zero momentum.

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/ReggeBlochM2Symbol4D.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: