Gravity Analysis Regge Ttbloch Assembly Local Edge Phase Decomposition

The phase identity

In numerical gravity, space is often cut into small cubes, and the gravitational field is sampled at the corners and edges of each cube. A recognition ledger, a discrete record of events, tracks how these samples combine. When a wave with a given momentum moves across such a cube, its phase, the position in its cycle, must be computed at the midpoint of each edge. The theorem localEdge_phase_decomposition states that this edge-midpoint phase equals the cell's own phase plus a slot-specific phase, minus a multiple of 2π that accounts for wrapping around the cube's periodic boundary. In symbols: edgeMidpointPhase = theta + slotPhase - 2π * slotWrapTurns.

The identity is not a physical law but a bookkeeping guarantee. The cell phase, theta, is shared by all edges of one cube. The slot phase depends only on which of the six edge directions and which of the six slots within that direction you pick. The wrapping term, slotWrapTurns, is an integer that counts how many full turns the wave's phase gains when the edge crosses the cube's boundary. The theorem proves these three pieces add up exactly, with no leftover error, for every cube size, every integer wave vector, and every edge. This exactness matters because the larger computation, assembling the whole grid, relies on this decomposition to hold without approximation.

The theorem is proved in the framework's machine-checked library of formal theorems. The proof uses the cosine periodicity: a cosine of an angle plus any integer multiple of 2π equals the cosine of the angle alone. So while the phase itself may jump by a full turn at the boundary, its cosine, the quantity that actually enters the physical sums, is unchanged. This is what makes the decomposition safe to use: the wrapping correction is real, but it is invisible to the cosine evaluator that feeds the final assembly.

What the theorem does not claim is just as important. It does not say that the phase decomposition is physically meaningful on its own, only that it is arithmetically correct. It does not assert that the cosine evaluator equals the true gravitational amplitude; that is a separate, later step in the assembly chain. And it does not claim that the wrapping correction is small or negligible, only that it is exactly accounted for. The theorem is a precise, narrow tool: it guarantees that one step in a larger calculation is exact, so that any error in the final result must come from elsewhere, not from this phase bookkeeping.

/-- Exact phase decomposition for every cell, including periodic seams.
The wrapped representative differs from the unwrapped cell-relative phase
by an integral number of full turns. -/
theorem localEdge_phase_decomposition (N : ℕ) [NeZero N]
    (m : Fin 3 → ℤ) (cell : Vertex N N N) (t f : Fin 6) :
    edgeMidpointPhase N (commensurateMomentum N m) (localEdgeOf cell t f) =
      BlochCellSum.theta N m cell + slotPhase N m t f -
        2 * Real.pi * (slotWrapTurns N m cell t f : ℝ) := by
  have hwrap :
      (slotWrapTurns N m cell t f : ℝ) =
        ∑ i : Fin 3, (m i : ℝ) * (slotWrapCount N cell t f i : ℝ) := by
    unfold slotWrapTurns
    rw [Int.cast_sum]
    refine Finset.sum_congr rfl fun i _ => ?_
    norm_cast
  unfold edgeMidpointPhase slotPhase
  simp only [Fin.sum_univ_three]
  rw [show (localEdgeOf cell t f).base =
      addVertexBits cell
        (cubeEdgeBase
          (Geometry.FreudenthalCubeTriangulation.localEdgeOf t f)) from rfl]
  rw [vertCoord_addVertexBits N cell _ 0,
    vertCoord_addVertexBits N cell _ 1,
    vertCoord_addVertexBits N cell _ 2]
  rw [slotMidTwice_eq_geometry N cell t f 0,
    slotMidTwice_eq_geometry N cell t f 1,
    slotMidTwice_eq_geometry N cell t f 2]
  rw [hwrap]
  unfold BlochCellSum.theta commensurateMomentum slotWrapCount
  simp only [Fin.sum_univ_three]
  unfold slotBaseBit vertexNatCoord
  push_cast
  have hN : (N : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (NeZero.ne N)
  field_simp [hN]
  ring

/-- Cosine form of the phase decomposition.  Integral seam corrections
disappear by `2*pi` periodicity. -/
theorem cos_localEdge_eq_cell_slot (N : ℕ) [NeZero N]
    (m : Fin 3 → ℤ) (cell : Vertex N N N) (t f : Fin 6) :
    Real.cos
        (edgeMidpointPhase N (commensurateMomentum N m)
          (localEdgeOf cell t f)) =
      Real.cos (BlochCellSum.theta N m cell + slotPhase N m t f) := by
  rw [localEdge_phase_decomposition N m cell t f]
  rw [show 2 * Real.pi * (slotWrapTurns N m cell t f : ℝ) =
      (slotWrapTurns N m cell t f : ℝ) * (2 * Real.pi) by ring]
  exact Real.cos_sub_int_mul_two_pi _ _

/-- Exact phase decomposition for every cell, including periodic seams.
The wrapped representative differs from the unwrapped cell-relative phase
by an integral number of full turns. -/
theorem localEdge_phase_decomposition (N : ℕ) [NeZero N]
    (m : Fin 3 → ℤ) (cell : Vertex N N N) (t f : Fin 6) :
    edgeMidpointPhase N (commensurateMomentum N m) (localEdgeOf cell t f) =
      BlochCellSum.theta N m cell + slotPhase N m t f -
        2 * Real.pi * (slotWrapTurns N m cell t f : ℝ) := by
  have hwrap :
      (slotWrapTurns N m cell t f : ℝ) =
        ∑ i : Fin 3, (m i : ℝ) * (slotWrapCount N cell t f i : ℝ) := by
    unfold slotWrapTurns
    rw [Int.cast_sum]
    refine Finset.sum_congr rfl fun i _ => ?_
    norm_cast
  unfold edgeMidpointPhase slotPhase
  simp only [Fin.sum_univ_three]
  rw [show (localEdgeOf cell t f).base =
      addVertexBits cell
        (cubeEdgeBase
          (Geometry.FreudenthalCubeTriangulation.localEdgeOf t f)) from rfl]
  rw [vertCoord_addVertexBits N cell _ 0,
    vertCoord_addVertexBits N cell _ 1,
    vertCoord_addVertexBits N cell _ 2]
  rw [slotMidTwice_eq_geometry N cell t f 0,
    slotMidTwice_eq_geometry N cell t f 1,
    slotMidTwice_eq_geometry N cell t f 2]
  rw [hwrap]
  unfold BlochCellSum.theta commensurateMomentum slotWrapCount
  simp only [Fin.sum_univ_three]
  unfold slotBaseBit vertexNatCoord
  push_cast
  have hN : (N : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (NeZero.ne N)
  field_simp [hN]
  ring

What this page does not claim

The decomposition is not a physical law, only an exact arithmetic identity. The theorem does not assert that the cosine evaluator equals the true gravitational amplitude. The wrapping correction is not claimed to be small or negligible, only exactly accounted for.

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