Gravity Analysis Regge Bloch M2 Symbol4 D Class Midpoint Phase Symbol Dir

A phase symmetry

In the framework's gravity analysis, a wave is examined along a chosen direction in four-dimensional space. The declaration classMidpointPhase_symbolDir concerns the phase at the midpoint of a discrete cell, a quantity that records how the wave's oscillation is positioned within that cell. The theorem states that when the wave's momentum is scaled by any factor μ, the midpoint phase scales by the same factor. In plain terms, the phase is linear in the momentum: double the momentum, and the phase at the midpoint doubles.

This linearity is a symmetry property. It means that the phase at the midpoint does not depend on the magnitude of the momentum in a complicated way; only the direction matters for the proportionality. The declaration is a formal statement in the machine-checked library of the framework, proved for a specific direction vector, symbolDir = (1,1,0,0). It is a building block for a larger analysis of how a discrete gravity model behaves at small momenta.

The theorem is a local result. It establishes the scaling behavior of the midpoint phase along one direction. It does not, by itself, show that the full gravity model converges to Einstein-Hilbert action, nor does it recover the gap action. Those remain open targets in the framework's development, as recorded in its status structure. The declaration is one step in a longer chain, not the final conclusion.

What this means for the reader is that a specific, checkable symmetry holds in the framework's discrete gravity setup. It is a small but rigorous piece of the larger puzzle, showing that the phase behaves predictably under scaling along a chosen axis. The framework's library records this as a theorem, with the proof checked by the machine, and it does not overstate its reach.

theorem classMidpointPhase_symbolDir (μ : ℝ) (x : Fin 4 → ℝ) (d : Fin 15) :
    classMidpointPhase (fun i => μ * symbolDir i) x d =
      μ * phaseScale x d := by
  unfold classMidpointPhase phaseScale
  have hx :
      (∑ i : Fin 4, (μ * symbolDir i) * x i) =
        μ * ∑ i : Fin 4, symbolDir i * x i := by
    simp [mul_assoc, Finset.mul_sum]
  have hd :
      (∑ i : Fin 4, (μ * symbolDir i) * classDisp d i) =
        μ * ∑ i : Fin 4, symbolDir i * classDisp d i := by
    simp [mul_assoc, Finset.mul_sum]
  rw [hx, hd]; ring

What this page does not claim

This does not claim that the full gravity model converges to Einstein-Hilbert action. This does not claim that the gap action is recovered. This does not claim the symmetry holds for all directions, only for the specific symbolDir.

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: