Encyclopedia Gravity Gravity Seven Gaps Discrete Lichnerowicz Status Curved Background Open

ARTICLE 4 claims 4 theorems

Gravity Seven Gaps Discrete Lichnerowicz Status Curved Background Open

A machine-checked flag in the framework's gravity library records that curved spacetimes remain unproved, marking a precise boundary of current knowledge.

Verify this page

The curved-background status flag

The declaration status_curved_background_open is a machine-checked flag inside the framework's library of formal theorems. It records a simple fact: the curved-background case is open. In plain language, the framework has not yet proved anything about how its discrete gravity operators behave on curved spacetimes like Schwarzschild or Kerr. The flag is a formal way of saying this work remains to be done, and it is part of a status record that also marks the quasinormal-mode spectrum as open.

What the framework has proved is narrower. On a flat three-dimensional torus, the discrete eigenvalues of a lattice Laplacian converge to the continuum Lichnerowicz eigenvalues as the lattice is refined. This is a theorem, but it is restricted to the flat background and to a specific axis direction of the lattice. The curved-background flag does not extend this result. It explicitly marks the boundary: no curved-space geometry is formalized or claimed anywhere in this file.

The flag is a definitional truth, not a discovery. It states that a boolean value in the status record is true, meaning the flag is set. It does not prove that curved backgrounds are impossible to handle, nor does it suggest they are intractable. It is a bookkeeping device that keeps the framework honest about what has been established and what remains a target for future work.

THEOREM status_curved_background_open · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean
status_curved_background_open · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean:565 
theorem status_curved_background_open :
    status.curved_background_open = true := rfl
THEOREM status_curved_background_open · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean
status_curved_background_open · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean:565 
theorem status_curved_background_open :
    status.curved_background_open = true := rfl
THEOREM discreteEigenvalue_tendsto · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean
discreteEigenvalue_tendsto · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean:204 
/-- THEOREM (the core convergence result; AXIS SECTOR ONLY). For fixed
wavenumber `k`, the discrete eigenvalue `4 N² sin²(πk/N)` of the AXIS mode
converges to the continuum eigenvalue `(2πk)²` as the lattice is refined.
Proof: `4N² sin²(πk/N) = (2πk)² (sin x / x)²` with `x = πk/N → 0`, and
`sin x / x → 1` at `0` (from `HasDerivAt sin 1 0` via the slope
characterization); the wavenumber `k = 0` is handled separately (both sides
vanish identically).

Scope: this is a statement about axis-aligned modes of the axis-stencil
Laplacian. Test G (`FreudenthalStencilPreflight`/`FreudenthalEnergyLimit`,
commits 7b808f75b4, 1d3ed6da06) kernel-proved the full continuum moment
tensor is anisotropic, `A₀ = (1+√2)I + (√2+√3)J`, which axis stencils
cannot see; do not read this as isotropic flat-space recovery. The
direction-resolved symbol question is governed by the C10 probe (plan
receipt P-iso, 2026-07-15). -/
theorem discreteEigenvalue_tendsto (k : ℕ) :
    Filter.Tendsto (fun N : ℕ => discreteEigenvalue N k) Filter.atTop
      (nhds ((2 * Real.pi * (k : ℝ)) ^ 2)) := by
  rcases Nat.eq_zero_or_pos k with hk | hk
  · subst hk
    have hzero : (fun N : ℕ => discreteEigenvalue N 0) = fun _ : ℕ => (0 : ℝ) := by
      funext N
      norm_num [discreteEigenvalue]
    rw [hzero]
    have h0 : ((2 * Real.pi * ((0 : ℕ) : ℝ)) ^ 2 : ℝ) = 0 := by norm_num
    rw [h0]
    exact tendsto_const_nhds
  · have hk' : (0 : ℝ) < (k : ℝ) := by exact_mod_cast hk
    -- sin y / y → 1 as y → 0 (through nonzero values)
    have hslope : Filter.Tendsto (fun y : ℝ => Real.sin y / y) (𝓝[≠] (0 : ℝ)) (nhds 1) := by
      have h := Real.hasDerivAt_sin 0
      rw [Real.cos_zero] at h
      have h2 := hasDerivAt_iff_tendsto_slope.mp h
      refine h2.congr ?_
      intro y
      rw [slope_def_field]
      simp
    -- x_N = πk/N → 0 within nonzero values
    have hx0 : Filter.Tendsto (fun N : ℕ => Real.pi * (k : ℝ) / (N : ℝ)) Filter.atTop
        (nhds 0) := tendsto_const_div_atTop_nhds_zero_nat (Real.pi * (k : ℝ))
    have hxmem : ∀ᶠ N : ℕ in Filter.atTop,
        Real.pi * (k : ℝ) / (N : ℝ) ∈ ({0}ᶜ : Set ℝ) := by
      filter_upwards [Filter.eventually_ge_atTop 1] with N hN
      have hNpos : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hN
      have hpos : 0 < Real.pi * (k : ℝ) / (N : ℝ) :=
        div_pos (mul_pos Real.pi_pos hk') hNpos
      simp only [Set.mem_compl_iff, Set.mem_singleton_iff]
      exact ne_of_gt hpos
    have hx : Filter.Tendsto (fun N : ℕ => Real.pi * (k : ℝ) / (N : ℝ)) Filter.atTop
        (𝓝[≠] (0 : ℝ)) :=
      tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hx0 hxmem
    have hcomp := hslope.comp hx
    simp only [Function.comp_def] at hcomp
    have hmul : Filter.Tendsto
        (fun N : ℕ => (2 * Real.pi * (k : ℝ)) ^ 2
          * (Real.sin (Real.pi * (k : ℝ) / (N : ℝ)) / (Real.pi * (k : ℝ) / (N : ℝ))) ^ 2)
        Filter.atTop (nhds ((2 * Real.pi * (k : ℝ)) ^ 2 * 1 ^ 2)) :=
      tendsto_const_nhds.mul (hcomp.pow 2)
    rw [one_pow, mul_one] at hmul
    refine hmul.congr' ?_
    filter_upwards [Filter.eventually_ge_atTop 1] with N hN
    have hNpos : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hN
    have hN0 : (N : ℝ) ≠ 0 := ne_of_gt hNpos
    have hπk : Real.pi * (k : ℝ) ≠ 0 := ne_of_gt (mul_pos Real.pi_pos hk')
    simp only [discreteEigenvalue]
    field_simp
    ring
THEOREM status_curved_background_open · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean
status_curved_background_open · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean:565 
theorem status_curved_background_open :
    status.curved_background_open = true := rfl

What this page does not claim

The flag does not claim that curved-background gravity is impossible to formalize. The flag does not claim that the flat-torus convergence result applies to any non-flat spacetime. The flag does not claim that the framework has any results about Schwarzschild or Kerr black holes.

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/SevenGaps/DiscreteLichnerowicz.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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND