Gravity Analysis Regge Ttbloch Assembly Raw Cosine Fold Eq Raw Triple Sum

The cosine fold identity

In lattice calculations, a common task is to sum a function over all the points of a grid. The Recognition Science framework's library of formal theorems contains a result about one such sum, where the function involves cosines of angles that depend on a wave vector and a grid position. The theorem, named rawCosineFold_eq_rawTripleSum, states that a particular way of grouping these cosine terms, called a fold, produces exactly the same number as a direct sum over all the individual terms. The identity holds for any grid side length and any integer wave vector, with no extra conditions on the wave vector itself.

The proof of this identity is a piece of formal mathematics, checked step by step by a machine. It works by expanding the cosine of a sum into a product of cosines, using the standard trigonometric identity, and then showing that the periodic wrapping of the grid, where a point that moves off one edge reappears on the opposite edge, does not change the value of the cosine. This wrapping is handled by an explicit decomposition of the phase into an integer number of full turns, which leave the cosine unchanged. The result is a clean equality between the folded sum and the triple sum.

What this theorem does not claim is that this identity applies to every possible sum of cosines. It is specific to the particular fold and the particular triple sum defined in the framework's Regge TT Bloch assembly module. It does not say anything about the physical meaning of the sum, only that the two algebraic expressions are equal. It also does not claim that the sum itself converges to a finite value in any limit; that is a separate question about the behavior of the terms as the grid becomes infinitely large.

The value of this theorem is that it provides a bridge between two different computational approaches. One approach, the fold, is efficient for certain kinds of analysis. The other, the triple sum, is easier to write down and to reason about. By proving that they are always equal, the framework's library allows a mathematician to use whichever form is more convenient for a given problem, with the guarantee that the answer will be the same. This is a small but solid step in building a foundation for more complex lattice calculations.

/-- The raw cosine bucket fold expands to the plain sum over all 216 raw
triples, with bucket collisions retained through the fiber amplitude. -/
theorem rawCosineFold_eq_rawTripleSum (N : ℕ) [NeZero N]
    (E : Fin 3 → Fin 3 → ℝ) (m : Fin 3 → ℤ) :
    reggeTTBlochFold rawCosineSupport (rawCosineEvaluator N m)
        (rawBucketAmplitude E) =
      ∑ p : Fin 6 × Fin 6 × Fin 6,
        rawCosineEvaluator N m (bucketKeyOf p) * rawTripleWeight E p := by
  unfold reggeTTBlochFold rawCosineSupport
  rw [Finset.sum_image' (fun p : Fin 6 × Fin 6 × Fin 6 =>
    rawCosineEvaluator N m (bucketKeyOf p) * rawTripleWeight E p)]
  intro p _
  unfold rawBucketAmplitude
  rw [Finset.mul_sum]
  refine Finset.sum_congr rfl fun q hq => ?_
  have hkey : bucketKeyOf q = bucketKeyOf p := (Finset.mem_filter.mp hq).2
  rw [hkey]

/-- The raw cosine bucket fold expands to the plain sum over all 216 raw
triples, with bucket collisions retained through the fiber amplitude. -/
theorem rawCosineFold_eq_rawTripleSum (N : ℕ) [NeZero N]
    (E : Fin 3 → Fin 3 → ℝ) (m : Fin 3 → ℤ) :
    reggeTTBlochFold rawCosineSupport (rawCosineEvaluator N m)
        (rawBucketAmplitude E) =
      ∑ p : Fin 6 × Fin 6 × Fin 6,
        rawCosineEvaluator N m (bucketKeyOf p) * rawTripleWeight E p := by
  unfold reggeTTBlochFold rawCosineSupport
  rw [Finset.sum_image' (fun p : Fin 6 × Fin 6 × Fin 6 =>
    rawCosineEvaluator N m (bucketKeyOf p) * rawTripleWeight E p)]
  intro p _
  unfold rawBucketAmplitude
  rw [Finset.mul_sum]
  refine Finset.sum_congr rfl fun q hq => ?_
  have hkey : bucketKeyOf q = bucketKeyOf p := (Finset.mem_filter.mp hq).2
  rw [hkey]

What this page does not claim

The theorem does not claim the sum converges to a finite value in any limit. The theorem does not claim the equality holds for any sum of cosines beyond the specific fold and triple sum defined in the module. The theorem does not assign any physical meaning to the sum, only the algebraic equality of the two expressions.

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: