Gravity Analysis Regge Ttcontinuum Limit Real Mode Norm Sq Int Cast Pos

The positivity lemma

In Recognition Science, the framework's account of gravity begins with a discrete lattice of points, not with a smooth spacetime. The calculation at issue here concerns a mode, a direction of displacement on that lattice, and the quantity Euclidean norm: the ordinary length of a vector, the square root of the sum of the squares of its components. The declaration realModeNormSq_intCast_pos proves a fact so basic it is easy to miss: if an integer vector is not the zero vector, then its squared Euclidean norm, when its entries are read as real numbers, is strictly positive.

The proof is a direct unpacking of the definition. A nonzero integer vector has at least one nonzero component. The square of that component is a positive real number, and the squares of the other components are nonnegative. Their sum, the squared norm, is therefore positive. The declaration formalizes this in the machine-checked library of formal theorems, using the fact that a nonzero integer is a nonzero real number.

Why does this matter? The positivity is a precondition for dividing by the norm. In the broader Regge TT continuum limit, the framework normalizes a mode to unit length before taking a limit. That normalization requires the norm to be nonzero, and this lemma supplies exactly that guarantee for every nonzero integer mode. Without it, the normalized direction would be undefined, and the limit could not be taken.

The lemma does not say anything about the value of the norm, only that it is positive. It does not identify which mode is being considered, only that the mode is nonzero. It does not assert that the limit exists or what it equals; those are separate theorems in the same module. Its role is narrow: it clears the way for the normalization step.

/-- A nonzero integer mode has positive real squared norm. -/
theorem realModeNormSq_intCast_pos (m : Fin 3 → ℤ)
    (hm : ∃ i : Fin 3, m i ≠ 0) :
    0 < realModeNormSq (fun i => (m i : ℝ)) := by
  obtain ⟨i, hi⟩ := hm
  unfold realModeNormSq
  have hi' : (m i : ℝ) ≠ 0 := by exact_mod_cast hi
  exact Finset.sum_pos' (fun j _ => sq_nonneg (m j : ℝ))
    ⟨i, Finset.mem_univ i, sq_pos_of_ne_zero hi'⟩

What this page does not claim

The lemma does not assert that any particular mode has a positive norm, only that every nonzero integer mode does. The lemma does not establish that the continuum limit exists or what value it converges to. The lemma does not involve the golden ratio, the cost function, or any other constant from the forcing chain.

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