Gravity Seven Gaps Curved Operator Underdetermination Curvature Correction Consi

The consistency certificate

A ledger, a discrete record of events, often approximates a smooth continuum. In numerical gravity, the question is whether a discrete operator's eigenvalues approach the continuum values as the lattice resolution increases. The declaration curvatureCorrectionConsistent_of_rateBound in the framework's machine-checked library of formal theorems establishes a sufficient condition for that convergence.

Specifically, it proves that if the difference between the curved discrete eigenvalue and the certified flat discrete eigenvalue, minus the analogous difference in the continuum, is bounded by a constant divided by the square of the resolution, then the curved discrete spectrum converges to the curved continuum spectrum. This is a quantitative certificate: a rate bound of order 1/N² guarantees consistency. The proof relies on a standard uniform-bound argument for limits.

The theorem does not define the physical curved Lichnerowicz operator. It works with a deliberately minimal scalar curvature proxy, rho, to exhibit a structural fact: the flat spectrum alone does not determine the curvature coupling. Two distinct operator families, with coupling 1 and 2, reduce to the same flat operator at zero curvature but differ at every nonzero curvature, yet both satisfy the same rate bound and have different continuum limits.

What the declaration establishes is a bridge: from a rate bound on the curvature correction to convergence of the full spectrum. It does not claim that any particular curved operator is the correct physical one. That identification remains an open construction, requiring a genuine curvature endomorphism derived from curved discrete geometry.

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

/-- 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 declaration does not identify which curvature coupling, 1 or 2, is physically correct. It does not prove that any curved operator family satisfies the rate bound; it only shows the rate bound is sufficient for convergence. The theorem does not construct the physical curved Lichnerowicz operator from curved discrete geometry.

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: