Gravity Analysis Regge Ttbloch Assembly Canonical Finite H Eq Raw Cosine Bloch F

The finite-cell identity

The declaration canonicalFiniteH_eq_rawCosineBlochFold is a theorem in the framework's machine-checked library of formal theorems. It states a precise equality for a finite-cell gravity operator, which is a discrete approximation of a gravitational field on a small, periodic grid. The theorem proves that this operator, called canonicalFiniteH, can be rewritten as a sum over wave vectors, known as a Bloch fold, using only cosine functions and a simple amplitude weight. This is not an approximation; it is an exact identity that holds under a specific condition.

The condition is that the wave vector must not be aliased. In plain terms, the doubled frequency of the wave must not wrap around the grid's periodic boundary in any coordinate direction. The theorem, proved for every side length N and every commensurate integer wave vector m satisfying this non-aliasing condition, shows that the canonical finite value equals the raw bucket-fiber Bloch fold. This identity is built from a chain of earlier results: it decomposes the phase of each edge midpoint into a cell-relative phase plus a slot phase, handles periodic wrapping by an explicit integer-turn decomposition, and then uses cosine periodicity to complete the proof.

The practical consequence is that the finite-cell gravity operator can be computed efficiently. Instead of summing over every cell and edge, one can sum over the much smaller set of wave-vector buckets. This is a structural simplification that makes the discrete gravity model tractable. The theorem also provides a uniform statement for all sufficiently large grids: eventually, for any non-zero wave vector, the identity holds. This eventual version is a corollary that follows from the fact that any non-zero wave vector becomes non-aliased as the grid grows.

What the theorem does not claim is equally important. It does not assert that this identity holds for aliased wave vectors; those are explicitly excluded. It does not claim that the canonical finite operator is a complete or correct model of gravity; it is a finite-cell assembly stage, and no spike or continuum-certificate module is imported. The theorem is a formal equality about a specific discrete construction, not a physical law. It establishes a computational identity, not a new physical principle.

/-- CANONICAL FINITE ASSEMBLY: the actual reduced finite second variation
equals the raw bucket cosine fold under the same non-aliasing condition. -/
theorem canonicalFiniteH_eq_rawCosineBlochFold (N : ℕ) [NeZero N]
    (E : Fin 3 → Fin 3 → ℝ) (m : Fin 3 → ℤ)
    (halias : ∃ i : Fin 3, ¬ (N : ℤ) ∣ 2 * m i) :
    canonicalFiniteH N E m =
      reggeTTBlochFold rawCosineSupport (rawCosineEvaluator N m)
        (rawBucketAmplitude E) := by
  rw [a2_reduced_eq_rawCellStencil,
    rawCellStencil_eq_rawCosineBlochFold N E m halias]

/-- CANONICAL FINITE ASSEMBLY: the actual reduced finite second variation
equals the raw bucket cosine fold under the same non-aliasing condition. -/
theorem canonicalFiniteH_eq_rawCosineBlochFold (N : ℕ) [NeZero N]
    (E : Fin 3 → Fin 3 → ℝ) (m : Fin 3 → ℤ)
    (halias : ∃ i : Fin 3, ¬ (N : ℤ) ∣ 2 * m i) :
    canonicalFiniteH N E m =
      reggeTTBlochFold rawCosineSupport (rawCosineEvaluator N m)
        (rawBucketAmplitude E) := by
  rw [a2_reduced_eq_rawCellStencil,
    rawCellStencil_eq_rawCosineBlochFold N E m halias]

/-- 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 identity does not hold for aliased wave vectors. The theorem does not establish a physical law of gravity. The canonical finite operator is not a complete gravity model.

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: