Encyclopedia Gravity Gravity Seven Gaps Curved Operator Underdetermination Flat Spectrum Underdetermi

ARTICLE 4 claims 4 theorems

Gravity Seven Gaps Curved Operator Underdetermination Flat Spectrum Underdetermi

A machine-checked theorem shows why a flat geometry's vibration pattern cannot uniquely determine how curvature couples to matter.

Verify this page

A flat spectrum, two curved worlds

In physics, the spectrum of an operator is the set of its allowed energy levels, the discrete tones a system can play. A lattice is a discrete grid of points, like a crystal lattice, where fields live on the points. The flat spectrum is the collection of tones for a flat, uncurved lattice. The question is whether that flat spectrum alone can tell you how the system would behave if the lattice were curved, like the surface of a sphere.

The theorem flat_spectrum_underdetermines_curvature_coupling proves it cannot. It constructs two distinct families of operators, each a rule that acts on fields on the lattice. Both families reduce to the same flat operator when curvature is zero, meaning they are indistinguishable on a flat lattice. But when curvature is nonzero, they differ on a concrete polarization state, a specific pattern of field values. The theorem shows that both families have well-defined limits as the lattice gets finer, converging to continuum operators, yet those limits differ. So the flat spectrum, the set of tones for the flat case, is compatible with two different curved extensions. The flat data underdetermines the curved coupling.

This is not a failure of the framework. It is a precise identification of a gap in the current theory. The framework's library of machine-checked theorems contains a certified spectrum theorem for the flat lattice Laplacian, but that theorem contains no Riemann-curvature endomorphism, the mathematical object that encodes curvature. The new theorem turns that gap into a formal statement: without additional input, the flat spectrum cannot select the curved operator.

The theorem also isolates what is missing. 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 on that correction, of the form C divided by N squared, is a sufficient certificate for discretization consistency. This gives a concrete target for closing the gap: derive the genuine curvature endomorphism from curved discrete geometry and prove its correction satisfies such a bound.

What the theorem does not claim is equally important. It does not define the physical curved Lichnerowicz operator. The scalar parameter rho is a deliberately minimal proxy for curvature, used only to exhibit non-identifiability. The genuine curvature endomorphism remains to be derived from curved discrete geometry. The theorem establishes a blocker, not a solution.

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 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 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 curvatureCorrectionConsistent_of_rateBound · IndisputableMonolith/Gravity/SevenGaps/CurvedOperatorUnderdetermination.lean
curvatureCorrectionConsistent_of_rateBound · IndisputableMonolith/Gravity/SevenGaps/CurvedOperatorUnderdetermination.lean:248 
/-- 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 scalar rho is a minimal proxy, not a derived curvature endomorphism. The theorem does not claim the flat spectrum is sufficient to determine the curved coupling.

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