Gravity Seven Gaps Curved Operator Underdetermination Extensions Distinct At Non

Curved extensions diverge

In the study of discrete gravity, a lattice operator is a rule that acts on fields defined on a grid of points, much like a matrix acts on a vector. The flat lattice Laplacian, written here as discLap3, is the standard discrete version of the familiar Laplacian from calculus, adapted to a three-dimensional grid. A central question is how to extend this flat operator to a curved background, where space is bent or warped. The declaration extensions_distinct_at_nonzero_curvature proves a precise underdetermination result: two different curved extensions of the same flat operator exist, and they are provably distinct whenever the curvature parameter rho is nonzero.

The two extensions are built by adding a curvature-coupling term to the flat Laplacian. The first, singleCurvatureExtension, adds rho times the field itself; the second, doubleCurvatureExtension, adds twice that amount. In flat space, where rho equals zero, both extensions reduce to the same operator, as the theorem extensions_agree_on_entire_flat_specialization shows. But the moment rho is nonzero, the two operators differ on at least one concrete field, a fact the theorem establishes for every lattice resolution N. This is not a subtle numerical difference; it is a structural distinction in the operators themselves.

The theorem also connects this distinction to the spectrum, the set of eigenvalues that characterize an operator's behavior. For each curvature value and each mode index k, the two extensions produce different continuum eigenvalues, as curvedContinuumEigenvalues_distinct proves. In addition, both discrete eigenvalue families converge as the lattice resolution grows, but to different continuum limits, as flat_spectrum_underdetermines_curvature_coupling confirms. This means that observing the flat spectrum alone cannot tell you which curved extension is the correct one; the flat data underdetermines the curvature coupling.

What the declaration does not claim is equally important. It does not define the physical curved Lichnerowicz operator, the genuine object of interest in curved discrete geometry. The parameter rho is a deliberately minimal proxy for curvature, used only to exhibit non-identifiability, not a derived physical quantity. The theorem does not say which extension is correct, only that they are different. A complete resolution of the gap would require deriving the true curvature endomorphism from curved discrete geometry and proving its correction is consistent with the continuum Riemann coupling, a task the module explicitly leaves open.

The practical consequence is a caution for numerical gravity: if a simulation uses a flat lattice operator and adds curvature by hand, the result is not unique. Two equally reasonable choices produce different physics on curved backgrounds, and the flat spectrum cannot arbitrate between them. This is a concrete obstruction that any candidate theory of discrete gravity must address, not a philosophical worry.

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

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

/-- The two curved continuum values differ whenever curvature is nonzero. -/
theorem curvedContinuumEigenvalues_distinct
    (rho : ℝ) (hrho : rho ≠ 0) (k : ℕ) :
    curvedContinuumEigenvalue 1 rho k ≠
      curvedContinuumEigenvalue 2 rho k := by
  intro h
  unfold curvedContinuumEigenvalue at h
  exact hrho (by linarith)

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

What this page does not claim

The declaration does not define the physical curved Lichnerowicz operator. The parameter rho is a minimal proxy for curvature, not a derived physical quantity. The theorem does not state which curved extension is physically correct, only that they differ.

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: