Gravity Seven Gaps Curved Operator Underdetermination Extensions Agree On Entire

The flat specialization agreement

In the study of gravity on a lattice, a key operator called the Lichnerowicz Laplacian describes how small disturbances evolve. On a flat space, this operator has a well-understood spectrum, a set of allowed frequencies. The framework's library of formal theorems proves that two distinct curved extensions of this flat operator, one with a single curvature coupling and one with a double coupling, both reduce to the exact same flat operator when the curvature parameter rho is zero. This agreement holds for every lattice resolution and every tensor field, so the two extensions are indistinguishable in flat space.

The theorem extensions_agree_on_entire_flat_specialization states this precisely: for any lattice size N and any field H, the single-curvature extension at rho = 0 equals the double-curvature extension at rho = 0. The proof chains together two simpler facts. First, the flat specialization of the general curvature-coupled operator is independent of the coupling strength. Second, both extensions are built from that same general operator, so they inherit that equality. This is a formal result in the machine-checked library, not a numerical approximation.

What this theorem does not claim is just as important. It does not say the two extensions agree when curvature is nonzero. In fact, a companion theorem proves they differ on a specific nonzero polarization at every nonzero curvature. The flat agreement is a special case, not a general equivalence. The theorem also does not define the physical curved Lichnerowicz operator. The scalar parameter rho is a minimal proxy for curvature, used only to exhibit the underdetermination. The genuine curvature endomorphism remains an open construction.

The consequence is a sharp statement about measurement. A flat-space experiment, no matter how fine the lattice, cannot distinguish between these two curved extensions. The flat spectrum alone underdetermines the curvature coupling. This is a precise, formal articulation of a gap in the framework's gravity program, not a claim that the gap is closed.

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

/-- 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 theorem does not claim the two curved extensions agree when curvature is nonzero. The theorem does not define the physical curved Lichnerowicz operator. The theorem does not close the Gap 4 construction; it only formalizes the obstruction.

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: