Gravity Seven Gaps Curved Operator Underdetermination Curved Continuum Eigenvalu

The curvature gap

The declaration curvedContinuumEigenvalues_distinct is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It proves that two different ways of adding a curvature term to a flat lattice operator produce different limiting eigenvalue values in the continuum, whenever the curvature parameter rho is nonzero. In plain terms: if you take a flat grid operator, add a curvature coupling of strength 1 versus strength 2, the resulting spectra do not agree in the continuum limit. The theorem states that for any nonzero rho and any mode index k, the continuum eigenvalue for coupling 1 differs from that for coupling 2.

The proof is short and direct. The curved continuum eigenvalue is defined as the flat eigenvalue plus coupling times rho. Since the flat part is identical for both couplings, the difference reduces to 1*rho versus 2*rho, which are unequal for nonzero rho. The theorem is tagged THEOREM because it is proved in the Lean 4 kernel with no axioms beyond the standard three. It is part of a larger module called CurvedOperatorUnderdetermination, which addresses what the framework calls Gap 4 in its gravity program.

The wider context matters. The framework's certified spectrum theorem for the flat lattice Laplacian is exact but narrow: it treats axis modes and introduces the continuum Lichnerowicz value definitionally from the flat reduction. It contains no Riemann-curvature endomorphism and therefore cannot determine a curved-background coupling. The module constructs two explicit curvature-coupled operator families that both reduce to the same flat operator at zero curvature, but differ on a concrete nonzero TT polarization at every nonzero curvature. Their eigenvalue branches both satisfy the same flat theorem and both have certified continuum limits, with different curved limits.

What the theorem does not claim is as important as what it proves. It does not define the physical curved Lichnerowicz operator. The scalar parameter rho is a deliberately minimal curvature proxy used to exhibit non-identifiability, not a derived physical quantity. The theorem does not show that the flat spectrum alone determines curvature coupling; it shows the opposite, that it underdetermines it. A 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 an open target.

The consequence for the framework is a precise blocker statement: the flat spectrum of the lattice operator cannot be used to identify how curvature couples to it. This is not a failure but a mapped obstacle, turning a reach gap into a theorem rather than a status flag. The framework's library now contains a formal proof that any curved extension consistent with the flat spectrum must be certified separately, via a quantitative C/N^2 correction bound, before it can claim physical meaning.

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

/-- Continuum eigenvalue branch associated with the same scalar curvature
coupling.  The flat part is exactly the MODEL value from
`DiscreteLichnerowicz`; the curvature term is countermodel data. -/
def curvedContinuumEigenvalue (coupling rho : ℝ) (k : ℕ) : ℝ :=
  DiscreteLichnerowicz.lichnerowiczFlatEigenvalue k + coupling * rho

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

/-- 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 define the physical curved Lichnerowicz operator. The scalar rho is a minimal proxy, not a derived physical curvature quantity. The flat spectrum alone does not determine curvature coupling; the theorem proves the opposite.

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: