Encyclopedia Gravity Gravity Seven Gaps Curved Operator Underdetermination

ARTICLE 4 claims 4 theorems

Gravity Seven Gaps Curved Operator Underdetermination

A flat spectrum cannot tell you how gravity couples to curvature, and a machine-checked proof now shows exactly why.

Verify this page

The curvature blind spot

The problem is a blind spot in how physicists discretize gravity. On a flat lattice, a standard operator called the Laplacian has a well-defined spectrum of eigenvalues, and that spectrum converges to a known continuum limit. The trouble begins when curvature enters. The flat spectrum alone does not determine how a curved-background operator should couple to that curvature. Two different curved operators can share the same flat spectrum and still disagree at every nonzero curvature.

The module CurvedOperatorUnderdetermination turns that blind spot into a theorem. It constructs two explicit operator families on a lattice tensor-field type. Both families reduce to the same flat operator for every field and every resolution when curvature is zero. At any nonzero curvature, they differ on a concrete nonzero transverse-traceless polarization. Their eigenvalue branches both satisfy the same flat convergence theorem and both have certified continuum limits, but those limits are different. The theorem flat_spectrum_underdetermines_curvature_coupling states this precisely: the flat spectrum underdetermines the curvature coupling.

The second half of the module isolates the missing analytic premise. Convergence of an arbitrary curved eigenvalue family is equivalent to convergence of its curvature correction, the curved value minus the certified flat value. A quantitative bound of the form C divided by N squared is a sufficient certificate for discretization consistency. The theorem curvedSpectrumConverges_iff_curvatureCorrectionConsistent proves this equivalence, and the rate-bound theorem gives the practical certificate.

What this does not do is define the physical curved Lichnerowicz operator. The scalar parameter rho is a deliberately minimal curvature proxy, used only to exhibit non-identifiability. The closing Gap 4 construction must derive the genuine curvature endomorphism from curved discrete geometry and prove its correction consistent with the continuum Riemann coupling. That remains open.

THEOREM flat_spectrum_underdetermines_curvature_coupling · IndisputableMonolith/Gravity/SevenGaps/CurvedOperatorUnderdetermination.lean
flat_spectrum_underdetermines_curvature_coupling · IndisputableMonolith/Gravity/SevenGaps/CurvedOperatorUnderdetermination.lean:164 
/-- Certified underdetermination package.  The same full flat operator data
admits two operator extensions that separate at every nonzero curvature; both
eigenvalue branches converge, but to distinct curved values. -/
theorem flat_spectrum_underdetermines_curvature_coupling
    (rho : ℝ) (hrho : rho ≠ 0) (k : ℕ) :
    (∀ (N : ℕ) (H : DiscreteLichnerowicz.LatticeTensorField),
      singleCurvatureExtension 0 N H = doubleCurvatureExtension 0 N H) ∧
    (∀ N : ℕ,
      (singleCurvatureExtension rho N :
          DiscreteLichnerowicz.LatticeTensorField → DiscreteLichnerowicz.LatticeTensorField) ≠
        (doubleCurvatureExtension rho N :
          DiscreteLichnerowicz.LatticeTensorField → DiscreteLichnerowicz.LatticeTensorField)) ∧
    Filter.Tendsto
      (fun N : ℕ => curvedDiscreteEigenvalue 1 rho N k)
      Filter.atTop (nhds (curvedContinuumEigenvalue 1 rho k)) ∧
    Filter.Tendsto
      (fun N : ℕ => curvedDiscreteEigenvalue 2 rho N k)
      Filter.atTop (nhds (curvedContinuumEigenvalue 2 rho k)) ∧
    curvedContinuumEigenvalue 1 rho k ≠
      curvedContinuumEigenvalue 2 rho k :=
  ⟨extensions_agree_on_entire_flat_specialization,
    fun N => extensions_distinct_at_nonzero_curvature rho hrho N,
    curvedDiscreteEigenvalue_tendsto 1 rho k,
    curvedDiscreteEigenvalue_tendsto 2 rho k,
    curvedContinuumEigenvalues_distinct rho hrho k⟩
THEOREM extensions_distinct_at_nonzero_curvature · IndisputableMonolith/Gravity/SevenGaps/CurvedOperatorUnderdetermination.lean
extensions_distinct_at_nonzero_curvature · IndisputableMonolith/Gravity/SevenGaps/CurvedOperatorUnderdetermination.lean:97 
/-- 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)
THEOREM curvedSpectrumConverges_iff_curvatureCorrectionConsistent · IndisputableMonolith/Gravity/SevenGaps/CurvedOperatorUnderdetermination.lean
curvedSpectrumConverges_iff_curvatureCorrectionConsistent · IndisputableMonolith/Gravity/SevenGaps/CurvedOperatorUnderdetermination.lean:226 
/-- 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
THEOREM curvedSpectrumConverges_of_correctionRateBound · IndisputableMonolith/Gravity/SevenGaps/CurvedOperatorUnderdetermination.lean
curvedSpectrumConverges_of_correctionRateBound · IndisputableMonolith/Gravity/SevenGaps/CurvedOperatorUnderdetermination.lean:262 
/-- Package theorem in the direction needed by a future curved
discretization: a proved correction-rate estimate, combined with the
existing flat convergence theorem, yields curved spectral convergence. -/
theorem curvedSpectrumConverges_of_correctionRateBound
    (discreteCurved : ℝ → ℕ → ℕ → ℝ)
    (continuumCurved : ℝ → ℕ → ℝ)
    (hRate : CurvatureCorrectionRateBound discreteCurved continuumCurved) :
    CurvedSpectrumConverges discreteCurved continuumCurved :=
  (curvedSpectrumConverges_iff_curvatureCorrectionConsistent
    discreteCurved continuumCurved).2
      (curvatureCorrectionConsistent_of_rateBound
        discreteCurved continuumCurved hRate)

What this page does not claim

This module defines the physical curved Lichnerowicz operator. The scalar rho is a genuine geometric curvature endomorphism. The two operator families are the only possible curved extensions of the flat operator.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND