Gravity Seven Gaps Curved Operator Underdetermination Curved Spectrum Converges

The convergence equivalence

In numerical analysis, a sequence of discrete approximations converges to a continuum limit when the values from finer and finer grids approach a single target. For the recognition framework's discrete geometry, a theorem in its machine-checked library of formal theorems establishes an exact equivalence for curved operators: the curved spectrum converges if and only if the curvature correction is consistent. The curvature correction is the difference between the curved eigenvalue and the certified flat eigenvalue at each grid resolution. This equivalence means that to verify convergence of a curved family, one need only check that this correction term settles down, rather than tracking the full spectrum.

The theorem is a biconditional, so it cuts both ways. If the correction is consistent, the spectrum converges; if the spectrum converges, the correction is consistent. This is not a heuristic or an approximation; it is a proved logical equivalence in the framework's library. The proof relies on the definitions of the two properties: convergence of the full curved eigenvalue sequence and consistency of the correction term. The result holds for any pair of discrete and continuum curved eigenvalue families that satisfy the stated conditions, not for one specific operator.

What the theorem does not do is choose a physical curved operator. The framework's library constructs two distinct curvature-coupled operator families, one with a single curvature coupling and one with a double coupling. Both reduce to the same flat operator at zero curvature, but they differ at every nonzero curvature. Both families satisfy the convergence equivalence, and both have certified continuum limits with different curved limits. This shows that the flat spectrum alone cannot determine which curved extension is correct. The theorem establishes a criterion for convergence, not a unique physical operator.

The scalar parameter rho in the construction is a deliberately minimal curvature proxy, not the genuine Riemann curvature endomorphism. The framework has not yet derived the physical curved Lichnerowicz operator from discrete geometry. That remains an open target. The equivalence theorem is a stepping stone: it gives a precise condition any candidate curved operator must satisfy, but it does not by itself identify that operator.

The practical consequence is a sharper verification tool. When a future construction proposes a curved discrete operator, the framework can check convergence by testing the correction term against the certified flat value. A quantitative bound of order 1 over N squared suffices as a discretization-consistency certificate. This turns a potentially difficult spectral convergence question into a simpler, checkable condition.

/-- Blocker theorem: because the flat branch already converges, full curved
convergence is equivalent to convergence of precisely the omitted curvature
correction.  Thus the flat theorem cannot discharge the curved target unless
this independent consistency premise is supplied. -/
theorem curvedSpectrumConverges_iff_curvatureCorrectionConsistent
    (discreteCurved : ℝ → ℕ → ℕ → ℝ)
    (continuumCurved : ℝ → ℕ → ℝ) :
    CurvedSpectrumConverges discreteCurved continuumCurved ↔
      CurvatureCorrectionConsistent discreteCurved continuumCurved := by
  constructor
  · intro hCurved rho k
    exact (hCurved rho k).sub (DiscreteLichnerowicz.discreteEigenvalue_tendsto k)
  · intro hCorrection rho k
    have hSum :=
      (DiscreteLichnerowicz.discreteEigenvalue_tendsto k).add (hCorrection rho k)
    convert hSum using 1
    · funext N
      ring
    · congr 1
      rw [DiscreteLichnerowicz.lichnerowiczFlatEigenvalue]
      ring_nf

/-- The two named curved extensions agree on the entire flat specialization,
not merely on one mode or one eigenvalue. -/
theorem extensions_agree_on_entire_flat_specialization :
    ∀ (N : ℕ) (H : DiscreteLichnerowicz.LatticeTensorField),
      singleCurvatureExtension 0 N H = doubleCurvatureExtension 0 N H := by
  intro N H
  trans curvatureCoupledOperator 0 0 N H
  · exact curvatureCoupledOperator_flat_specialization 1 N H
  · exact (curvatureCoupledOperator_flat_specialization 2 N H).symm

/-- At every nonzero curvature and every resolution, the two extensions are
different operators.  The witness is the constant plus polarization, on
which the flat Laplacian vanishes while the two curvature coefficients act
by `rho` and `2 * rho`. -/
theorem extensions_distinct_at_nonzero_curvature
    (rho : ℝ) (hrho : rho ≠ 0) (N : ℕ) :
    (singleCurvatureExtension rho N :
        DiscreteLichnerowicz.LatticeTensorField → DiscreteLichnerowicz.LatticeTensorField) ≠
      (doubleCurvatureExtension rho N :
        DiscreteLichnerowicz.LatticeTensorField → DiscreteLichnerowicz.LatticeTensorField) := by
  intro hEq
  have hField := congrFun hEq constantPlusField
  have hSite := congrFun hField ((0, 0, 0) : DiscreteLichnerowicz.Site3)
  have hEntry := congrFun (congrFun hSite (1 : Fin 3)) (1 : Fin 3)
  simp [singleCurvatureExtension, doubleCurvatureExtension,
    curvatureCoupledOperator, DiscreteLichnerowicz.discLap3, constantPlusField, DiscreteLichnerowicz.epsPlus] at hEntry
  have hEntryRe := congrArg Complex.re hEntry
  norm_num at hEntryRe
  exact hrho (by linarith)

/-- A quantitative `C / N^2` bound on the curvature correction supplies the
exact missing consistency premise, using the spectral convergence toolkit. -/
theorem curvatureCorrectionConsistent_of_rateBound
    (discreteCurved : ℝ → ℕ → ℕ → ℝ)
    (continuumCurved : ℝ → ℕ → ℝ)
    (hRate : CurvatureCorrectionRateBound discreteCurved continuumCurved) :
    CurvatureCorrectionConsistent discreteCurved continuumCurved := by
  intro rho k
  obtain ⟨C, N0, hBound⟩ := hRate rho k
  exact Gravity.Analysis.eigenvalue_limit_of_uniform_bound
    (fun N => discreteCurved rho N k - DiscreteLichnerowicz.discreteEigenvalue N k)
    (continuumCurved rho k - DiscreteLichnerowicz.lichnerowiczFlatEigenvalue k)
    C N0 hBound

What this page does not claim

The theorem does not define the physical curved Lichnerowicz operator. The flat spectrum alone does not determine which curved extension is correct. The scalar rho is a minimal curvature proxy, not the genuine Riemann curvature endomorphism.

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