Gravity Analysis Regge Exact Flat Hessian Bloch Torus Bridge4 D Tendsto Torus Sc

The shrinking mesh

The declaration tendsto_torusScale_nhdsWithin_ne_zero is a statement about a specific sequence of numbers, the torus scale (a shrinking mesh size used in a discrete model). The sequence is defined by torusScale j = 2π / (j+3). As the index j grows, the denominator grows, so the value gets closer and closer to zero. The theorem proves that this sequence converges to zero, but with an important refinement: it converges to zero while staying strictly away from zero at every step. In plain terms, the mesh never collapses to a single point; it approaches zero as a limit but never reaches it.

Why does this matter? In the broader framework, this sequence of shrinking scales is used to connect a discrete torus model to a continuous one. The theorem is the technical guarantee that this limiting process is well-behaved: the mesh sizes form a sequence that tends to the punctured neighborhood of zero, meaning the limit point is approached from the side of nonzero values. This is a standard and necessary condition for many arguments in analysis and geometry, where one wants to take a limit of objects defined on finer and finer grids without the grids themselves degenerating to a point.

The theorem is a formal, machine-checked result in the framework's library of formal theorems. It is a lemma, not a physical law. It establishes a property of a sequence of real numbers, nothing more. It does not claim that the discrete model is physically correct, nor that the limit of the sequence represents a physical quantity. It is a piece of mathematical infrastructure: a precise statement about convergence that other, larger theorems rely on.

In Recognition Science, this kind of result is part of the effort to show that a discrete, ledger-based model of spacetime can recover continuous behavior in a limit. The framework models physical structure from recognition events, and this theorem is a step in showing that a discrete torus, with its mesh shrinking according to this rule, behaves like a continuous space in the limit. The payoff is that the framework can use the language of continuous geometry while remaining grounded in a discrete foundation.

The theorem does not claim that the sequence torusScale j converges to any particular nonzero value, nor that the limit is unique. It does not claim that the discrete model is the only way to approach the continuous limit. It simply states that the specific sequence defined here tends to zero from the punctured neighborhood, a fact that is used as a building block in the larger bridge between the discrete and continuous descriptions.

theorem tendsto_torusScale_nhds_zero :
    Tendsto torusScale atTop (nhds (0 : ℝ)) := by
  have h :=
    (tendsto_const_div_atTop_nhds_zero_nat (2 * Real.pi)).comp
      (tendsto_add_atTop_nat 3)
  refine h.congr fun j => ?_
  simp [torusScale, torusSide]

theorem tendsto_torusScale_nhdsWithin_ne_zero :
    Tendsto torusScale atTop (𝓝[≠] (0 : ℝ)) := by
  refine tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ tendsto_torusScale_nhds_zero ?_
  filter_upwards [eventually_torusScale_ne_zero] with j hj
  simp only [Set.mem_compl_iff, Set.mem_singleton_iff]
  exact hj

What this page does not claim

The theorem does not claim that the discrete model is physically correct. The theorem does not claim that the limit of the sequence represents a physical quantity. The theorem does not claim that this is the only way to approach the continuous limit.

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: