Gravity Analysis Regge Exact Flat Hessian Bloch Torus Bridge4 D

The bridge to the continuum

In physics, a lattice is a discrete grid of points used to approximate a continuous space. The finer the grid, the closer the approximation should be to the smooth equations of the continuum. This result proves, in a machine-checked library of formal theorems, that a specific four-dimensional lattice built on a torus, a shape like the surface of a doughnut, converges to the exact continuum limit as the grid spacing shrinks to zero.

The key object is the exact midpoint Bloch symbol, which measures the difference between the discrete lattice's behavior and the continuous one at the midpoint of a cell. The theorem shows that as the torus side length grows, making the grid finer, this difference, divided by the square of the momentum, tends to a finite, well-defined limit. This limit is precisely the second-order term, the Hessian, of the continuous symbol. The result holds for all nonzero modes and all polarizations, meaning it is not a special case but a general property of the lattice.

In Recognition Science, this establishes a formal bridge between the discrete ledger of recognition events and the smooth geometry of general relativity. The framework models gravity not as a fundamental field but as an emergent property of a discrete underlying structure. This result provides the rigorous link: the discrete torus family, as it becomes infinitely fine, reproduces the exact flat-space Hessian of the continuous theory. It is the mathematical guarantee that the discrete model has the correct continuum limit, a necessary condition for any theory of quantum gravity.

The practical consequence is that calculations done on the discrete torus are not artifacts of the grid. They reflect genuine continuous physics. This is a foundational step, proving that the discrete starting point of the framework does not lose the smooth structure of gravity but recovers it exactly in the limit.

/-- Uncentered form matching `TypedResidual_discrete_torus_family_bridge`.
Requires the R2 hypothesis `exactMidpointBlochSymbolZero E = 0`. -/
theorem tendsto_exactMidpointBloch_torus_family
    (m : IntMode4) (E : Mat4) (hm : m ≠ 0)
    (h0 : exactMidpointBlochSymbolZero E = 0) :
    Tendsto
      (fun j : ℕ =>
        exactMidpointBlochSymbol E (realMode (torusSide j) m) /
          momentumNormSq (torusSide j) m)
      atTop
      (nhds
        (exactMidpointBlochM2 E (fun i => (m i : ℝ)) /
          waveNormSq (fun i => (m i : ℝ)))) := by
  have h := tendsto_exactMidpointBloch_torus_family_centered m E hm
  refine h.congr' ?_
  filter_upwards with j
  rw [h0, sub_zero]

/-- **THEOREM (R4):** discrete torus family bridge, uncentered, for all
nonzero modes and all polarizations.  Composes banked continuous Tendsto
with R2 (`typedResidual_midpointBloch_symbolZero`). -/
theorem discrete_torus_family_bridge :
    ∀ (m : IntMode4) (E : Mat4),
      m ≠ 0 →
        Tendsto
          (fun j : ℕ =>
            exactMidpointBlochSymbol E (realMode (torusSide j) m) /
              momentumNormSq (torusSide j) m)
          atTop
          (nhds
            (exactMidpointBlochM2 E (fun i => (m i : ℝ)) /
              waveNormSq (fun i => (m i : ℝ)))) :=
  discrete_torus_family_bridge_of_symbolZero
    ReggeExactFlatHessianBlochSymbolZero4D.typedResidual_midpointBloch_symbolZero

/-- Mesh ContinuumSymbolIs binder is definitionally the torus-family
midpoint sequence; bridge therefore inhabits ContinuumSymbolIs at the
m² Rayleigh value (still geometric / j-dependent; not a constant face). -/
theorem continuumSymbolIs_midpoint_rayleigh
    (m : IntMode4) (E : Mat4) (hm : m ≠ 0) :
    Regge4DContinuumSymbolIs m E
      (exactMidpointBlochM2 E (fun i => (m i : ℝ)) /
        waveNormSq (fun i => (m i : ℝ))) :=
  discrete_torus_family_bridge m E hm

What this page does not claim

This result does not prove that the discrete model is quantum gravity, only that it has the correct classical limit. The convergence proof does not establish the uniqueness of the continuum limit. The result does not derive the value of any physical constant.

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: