Gravity Analysis Regge Exact Flat Hessian Bloch Torus Bridge4 D Continuum Symbol

The midpoint limit

The declaration continuumSymbolIs_midpoint_rayleigh is a theorem in the machine-checked library of formal theorems that Recognition Science maintains. It concerns a discrete model of a wave operator on a four-dimensional torus, a space shaped like the surface of a donut but in four dimensions. The theorem states that as the mesh of this discrete model becomes infinitely fine, the ratio of a certain symbol to the square of the momentum converges to a specific limit, which is the second derivative of the symbol with respect to the momentum. This limit is called the midpoint Bloch symbol, and the convergence holds for all non-zero modes and all polarizations.

The proof is not a single step but a composition of two established results. First, a continuous-scale theorem shows that the same ratio converges when the scale parameter is varied continuously. Second, a discrete family of tori is constructed whose mesh sizes shrink to zero, and the continuous theorem is applied along this sequence. The key technical point is that the mesh scale tends to zero through a punctured neighborhood, meaning it approaches zero but never equals it. This ensures the discrete model remains well-defined throughout the convergence.

The theorem is conditional. The uncentered form, which is the one used in the final statement, requires the hypothesis that the midpoint Bloch symbol at zero momentum is itself zero. This is a non-trivial condition, often called the R2 hypothesis. The centered form, which subtracts this zero-momentum value before taking the ratio, holds unconditionally. The final theorem packages the uncentered form under the R2 assumption, and a separate result shows that if R2 holds for all polarizations, then the convergence holds for all of them simultaneously.

In plain terms, the theorem does not assert that the discrete model is exactly equal to the continuous one. It asserts that the discrete model's behavior, normalized by the momentum squared, approaches the continuous behavior in the limit of infinitely fine meshes. The limit is geometric in the sense that it depends on the mode shape, not a single constant. The declaration does not claim that the R2 hypothesis is true, only that if it is true, then the convergence follows. It also does not claim that the limit is finite or that the convergence is uniform across all modes.

/-- 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

/-- 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]

/-- Centered discrete torus family: banked continuous Tendsto along `t(j)`. -/
theorem tendsto_exactMidpointBloch_torus_family_centered
    (m : IntMode4) (E : Mat4) (hm : m ≠ 0) :
    Tendsto
      (fun j : ℕ =>
        (exactMidpointBlochSymbol E (realMode (torusSide j) m) -
            exactMidpointBlochSymbolZero E) /
          momentumNormSq (torusSide j) m)
      atTop
      (nhds
        (exactMidpointBlochM2 E (fun i => (m i : ℝ)) /
          waveNormSq (fun i => (m i : ℝ)))) := by
  let dir : Wave4 := fun i => (m i : ℝ)
  let n : ℝ := waveNormSq dir
  have hn : n ≠ 0 := waveNormSq_intMode_ne_zero m hm
  have hcont := tendsto_exactMidpointBloch_m2_div E dir n hn
  have hcomp := hcont.comp tendsto_torusScale_nhdsWithin_ne_zero
  refine hcomp.congr' ?_
  filter_upwards with j
  dsimp only [Function.comp_apply]
  rw [realMode_eq_scale, momentumNormSq_eq_scale_sq]

What this page does not claim

The theorem does not claim that the R2 hypothesis is true. The theorem does not claim that the discrete model equals the continuous one at any finite mesh size. The theorem does not claim that the limit is a constant independent of the mode shape.

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: