Gravity Analysis Regge Ttbloch Assembly Cos Local Edge Eq Cell Slot

The edge-phase identity

In the Recognition Science framework's machine-checked library of formal theorems, the declaration cos_localEdge_eq_cell_slot proves a precise identity about how waves are represented on a discrete grid. The framework models physical space as a finite, periodic lattice of cells, and it tracks the phase of a wave at the midpoint of each edge of that lattice. The theorem states that the cosine of the phase computed directly from the edge's global position is always equal to the cosine of the phase computed from the cell's local coordinates plus a slot-specific offset. In plainer terms: two different bookkeeping methods for the same wave phase on a grid edge produce exactly the same number, with no approximation.

The proof rests on a decomposition of the edge's phase into a cell-relative part and a slot-relative part, plus an integer number of full turns caused by periodic wrapping. Because the cosine function is periodic with period 2π, those extra full turns do not change the cosine value. The theorem therefore confirms that the local, cell-based description of a wave is consistent with the global, edge-based description. This is a structural consistency result: it does not compute any specific physical quantity, but rather guarantees that two definitions within the framework's formalism cannot diverge.

This identity is a necessary step in a larger assembly. The framework's gravity analysis builds a finite approximation of a continuous system by summing contributions from many cells. A later theorem, canonicalFiniteH_eq_rawCosineBlochFold, uses this edge-phase identity to show that the full finite approximation equals a sum over cosine evaluators. The identity is therefore not an isolated fact; it is the hinge that lets the framework move from a local, cell-by-cell description to a global, Fourier-like sum. Without it, the two descriptions could drift apart, and the finite assembly would not be trustworthy.

What the theorem does not claim is equally important. It does not assert that this identity holds for all possible wave vectors; it requires a non-aliasing condition, meaning the wave's frequency must not be a multiple of the grid's Nyquist frequency in any coordinate. It also does not claim that the framework's model of gravity is physically correct, only that this particular internal computation is self-consistent. The theorem is a statement about the framework's own definitions, not about the empirical world.

/-- 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 _ _

/-- 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 _ _

/-- 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]

What this page does not claim

The identity holds for all wave vectors without the non-aliasing condition. The framework's model of gravity is empirically validated by this theorem. The theorem computes a specific physical constant or observable.

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: