Gravity Analysis Regge Exact Flat Hessian Bloch Torus Bridge4 D Eventually Torus

The scale never vanishes

In the framework's analysis of gravity, a torus is a flat, four-dimensional shape with its edges glued together, like a video game screen that wraps around. To study how a wave behaves on this torus as the torus gets larger, the framework defines a scale, a number that controls the spacing of the grid used for the calculation. This scale is defined as 2π divided by the side length of the torus, which itself is just the index j plus 3. As j grows without bound, the side length grows, and the scale shrinks toward zero.

The declaration eventually_torusScale_ne_zero proves, in the machine-checked library of formal theorems, that for all sufficiently large j, this scale is not zero. This is not a trivial observation; it is a necessary condition for the next step. The framework wants to divide by the square of this scale to form a ratio that measures a certain curvature quantity. Dividing by zero is undefined, so this theorem guarantees that the ratio is well-defined for all large enough tori. It is the mathematical equivalent of ensuring the denominator of a fraction never vanishes, so the fraction always makes sense.

This theorem is a small but load-bearing piece of a larger result. It allows the framework to prove that a certain ratio, built from a curvature symbol and the square of the scale, approaches a finite limit as the torus grows. That limit is the value the framework associates with the continuum, the smooth infinite space that the discrete tori approximate. Without the guarantee that the scale is never zero, the whole limiting argument would collapse. The theorem is the quiet guardian that keeps the division legal.

The theorem does not claim that the scale is never zero for every j, only for all sufficiently large j. It does not claim that the scale itself has any particular nonzero value, only that it is not zero. It also does not claim that the limiting ratio is finite, or even that it exists; that is the job of the subsequent theorems that use this one as a hypothesis. This declaration is a precise, narrow guarantee about a single number in an infinite family, and its only job is to make the next step possible.

theorem eventually_torusScale_ne_zero :
    ∀ᶠ j : ℕ in atTop, torusScale j ≠ 0 := by
  filter_upwards with j
  have hden : ((torusSide j : ℕ) : ℝ) ≠ 0 := by
    exact Nat.cast_ne_zero.mpr (ne_of_gt (by unfold torusSide; omega))
  have hnum : (2 * Real.pi : ℝ) ≠ 0 :=
    mul_ne_zero (by norm_num : (2 : ℝ) ≠ 0) Real.pi_ne_zero
  exact div_ne_zero hnum hden

What this page does not claim

The scale is never zero for every index j, only for all sufficiently large ones. The scale has any particular nonzero value, only that it is not zero. The limiting ratio is finite or exists, which is proved by subsequent theorems.

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