IndisputableMonolith.Gravity.SevenGaps.CurvedOperatorUnderdetermination

   1import IndisputableMonolith.Gravity.SevenGaps.DiscreteLichnerowicz
   2import IndisputableMonolith.Gravity.Analysis.SpectralConvergence
   3
   4/-!
   5# Gap 4 blocker: flat spectrum does not determine curvature coupling
   6
   7The current certified spectrum theorem in `DiscreteLichnerowicz` has an exact
   8but narrow reach.  It treats axis modes of the componentwise flat lattice
   9Laplacian, and its continuum Lichnerowicz value is introduced definitionally
  10from the flat reduction `Delta_L = -Delta`.  It contains no Riemann-curvature
  11endomorphism and therefore cannot determine a curved-background coupling.
  12
  13This module turns that reach gap into a theorem rather than a status flag.
  14On the actual lattice tensor-field type, it constructs two explicit
  15zeroth-order curvature-coupled operator families.  Both reduce to the same
  16`-discLap3` operator for every field and every resolution at zero curvature,
  17but they differ on a concrete nonzero TT polarization at every nonzero
  18curvature.  Their eigenvalue branches both satisfy the same flat theorem and
  19both have certified continuum limits, with different curved limits.
  20
  21The second half isolates the exact missing analytic premise.  Relative to the
  22existing flat convergence theorem, convergence of an arbitrary curved
  23eigenvalue family is equivalent to convergence of its curvature correction
  24(curved value minus the certified flat value).  A quantitative `C / N^2`
  25correction bound is a sufficient discretization-consistency certificate via
  26`SpectralConvergence.eigenvalue_limit_of_uniform_bound`.
  27
  28Nothing here defines the physical curved Lichnerowicz operator.  The scalar
  29parameter `rho` is a deliberately minimal curvature proxy used to exhibit
  30non-identifiability.  A closing Gap 4 construction must derive the genuine
  31curvature endomorphism from curved discrete geometry and prove its correction
  32consistent with the continuum Riemann coupling.
  33-/
  34
  35namespace IndisputableMonolith
  36namespace Gravity
  37namespace SevenGaps
  38namespace CurvedOperatorUnderdetermination
  39
  40open Filter Topology
  41
  42noncomputable section
  43
  44/-! ## Two genuinely distinct curved extensions of the flat operator -/
  45
  46/-- A one-parameter family of lattice tensor-field operators.  The first term
  47is the certified positive flat operator `-discLap3`; the second is a
  48zeroth-order scalar curvature coupling.  This is a countermodel family, not a
  49definition of the physical curved Lichnerowicz operator. -/
  50def curvatureCoupledOperator (coupling rho : ℝ) (N : ℕ)
  51    (H : DiscreteLichnerowicz.LatticeTensorField) : DiscreteLichnerowicz.LatticeTensorField :=
  52  fun x => (-1 : ℝ) • DiscreteLichnerowicz.discLap3 N H x + (coupling * rho) • H x
  53
  54/-- The first explicit curved extension, with curvature coefficient one. -/
  55def singleCurvatureExtension (rho : ℝ) (N : ℕ)
  56    (H : DiscreteLichnerowicz.LatticeTensorField) : DiscreteLichnerowicz.LatticeTensorField :=
  57  curvatureCoupledOperator 1 rho N H
  58
  59/-- The second explicit curved extension, with curvature coefficient two. -/
  60def doubleCurvatureExtension (rho : ℝ) (N : ℕ)
  61    (H : DiscreteLichnerowicz.LatticeTensorField) : DiscreteLichnerowicz.LatticeTensorField :=
  62  curvatureCoupledOperator 2 rho N H
  63
  64/-- A constant plus-polarized tensor field used to distinguish the two
  65operator families. -/
  66def constantPlusField : DiscreteLichnerowicz.LatticeTensorField := fun _ => DiscreteLichnerowicz.epsPlus
  67
  68/-- The flat lattice Laplacian annihilates the constant plus field. -/
  69theorem discLap3_constantPlusField_zero (N : ℕ) :
  70    DiscreteLichnerowicz.discLap3 N constantPlusField = 0 := by
  71  funext x
  72  ext i j
  73  simp only [DiscreteLichnerowicz.discLap3, constantPlusField,
  74    Matrix.of_apply, Pi.zero_apply, Matrix.zero_apply]
  75  rw [Fin.sum_univ_three]
  76  ring
  77
  78/-- Every member of the countermodel family has exactly the same complete
  79flat specialization, on every field and at every lattice resolution. -/
  80theorem curvatureCoupledOperator_flat_specialization
  81    (coupling : ℝ) (N : ℕ) (H : DiscreteLichnerowicz.LatticeTensorField) :
  82    curvatureCoupledOperator coupling 0 N H =
  83      curvatureCoupledOperator 0 0 N H := by
  84  ext x i j
  85  simp [curvatureCoupledOperator]
  86
  87/-- The two named curved extensions agree on the entire flat specialization,
  88not merely on one mode or one eigenvalue. -/
  89theorem extensions_agree_on_entire_flat_specialization :
  90    ∀ (N : ℕ) (H : DiscreteLichnerowicz.LatticeTensorField),
  91      singleCurvatureExtension 0 N H = doubleCurvatureExtension 0 N H := by
  92  intro N H
  93  trans curvatureCoupledOperator 0 0 N H
  94  · exact curvatureCoupledOperator_flat_specialization 1 N H
  95  · exact (curvatureCoupledOperator_flat_specialization 2 N H).symm
  96
  97/-- At every nonzero curvature and every resolution, the two extensions are
  98different operators.  The witness is the constant plus polarization, on
  99which the flat Laplacian vanishes while the two curvature coefficients act
 100by `rho` and `2 * rho`. -/
 101theorem extensions_distinct_at_nonzero_curvature
 102    (rho : ℝ) (hrho : rho ≠ 0) (N : ℕ) :
 103    (singleCurvatureExtension rho N :
 104        DiscreteLichnerowicz.LatticeTensorField → DiscreteLichnerowicz.LatticeTensorField) ≠
 105      (doubleCurvatureExtension rho N :
 106        DiscreteLichnerowicz.LatticeTensorField → DiscreteLichnerowicz.LatticeTensorField) := by
 107  intro hEq
 108  have hField := congrFun hEq constantPlusField
 109  have hSite := congrFun hField ((0, 0, 0) : DiscreteLichnerowicz.Site3)
 110  have hEntry := congrFun (congrFun hSite (1 : Fin 3)) (1 : Fin 3)
 111  simp [singleCurvatureExtension, doubleCurvatureExtension,
 112    curvatureCoupledOperator, DiscreteLichnerowicz.discLap3, constantPlusField, DiscreteLichnerowicz.epsPlus] at hEntry
 113  have hEntryRe := congrArg Complex.re hEntry
 114  norm_num at hEntryRe
 115  exact hrho (by linarith)
 116
 117/-! ## The corresponding eigenvalue branches -/
 118
 119/-- Discrete eigenvalue branch associated with the scalar curvature coupling. -/
 120def curvedDiscreteEigenvalue (coupling rho : ℝ) (N k : ℕ) : ℝ :=
 121  DiscreteLichnerowicz.discreteEigenvalue N k + coupling * rho
 122
 123/-- Continuum eigenvalue branch associated with the same scalar curvature
 124coupling.  The flat part is exactly the MODEL value from
 125`DiscreteLichnerowicz`; the curvature term is countermodel data. -/
 126def curvedContinuumEigenvalue (coupling rho : ℝ) (k : ℕ) : ℝ :=
 127  DiscreteLichnerowicz.lichnerowiczFlatEigenvalue k + coupling * rho
 128
 129/-- The countermodel operator acts on every certified transverse axis mode
 130with the corresponding curved eigenvalue. -/
 131theorem curvatureCoupledOperator_planeH
 132    (coupling rho : ℝ) (N k : ℕ)
 133    (eps : Matrix (Fin 3) (Fin 3) ℂ) (hrow : ∀ j, eps 0 j = 0)
 134    (x : DiscreteLichnerowicz.Site3) :
 135    curvatureCoupledOperator coupling rho N (DiscreteLichnerowicz.planeH N (k : ℤ) eps) x =
 136      curvedDiscreteEigenvalue coupling rho N k •
 137        DiscreteLichnerowicz.planeH N (k : ℤ) eps x := by
 138  have hFlat :=
 139    (DiscreteLichnerowicz.discrete_tt_spectrum_converges_to_flat_lichnerowicz k eps hrow).2.1 N x
 140  unfold curvatureCoupledOperator
 141  rw [hFlat, smul_smul, ← add_smul]
 142  congr 1
 143  simp only [curvedDiscreteEigenvalue]
 144  ring
 145
 146/-- Each countermodel branch converges, by adding its constant curvature
 147correction to the existing certified flat convergence theorem. -/
 148theorem curvedDiscreteEigenvalue_tendsto
 149    (coupling rho : ℝ) (k : ℕ) :
 150    Filter.Tendsto
 151      (fun N : ℕ => curvedDiscreteEigenvalue coupling rho N k)
 152      Filter.atTop (nhds (curvedContinuumEigenvalue coupling rho k)) := by
 153  exact (DiscreteLichnerowicz.discreteEigenvalue_tendsto k).add tendsto_const_nhds
 154
 155/-- The two curved continuum values differ whenever curvature is nonzero. -/
 156theorem curvedContinuumEigenvalues_distinct
 157    (rho : ℝ) (hrho : rho ≠ 0) (k : ℕ) :
 158    curvedContinuumEigenvalue 1 rho k ≠
 159      curvedContinuumEigenvalue 2 rho k := by
 160  intro h
 161  unfold curvedContinuumEigenvalue at h
 162  exact hrho (by linarith)
 163
 164/-- Certified underdetermination package.  The same full flat operator data
 165admits two operator extensions that separate at every nonzero curvature; both
 166eigenvalue branches converge, but to distinct curved values. -/
 167theorem flat_spectrum_underdetermines_curvature_coupling
 168    (rho : ℝ) (hrho : rho ≠ 0) (k : ℕ) :
 169    (∀ (N : ℕ) (H : DiscreteLichnerowicz.LatticeTensorField),
 170      singleCurvatureExtension 0 N H = doubleCurvatureExtension 0 N H) ∧
 171    (∀ N : ℕ,
 172      (singleCurvatureExtension rho N :
 173          DiscreteLichnerowicz.LatticeTensorField → DiscreteLichnerowicz.LatticeTensorField) ≠
 174        (doubleCurvatureExtension rho N :
 175          DiscreteLichnerowicz.LatticeTensorField → DiscreteLichnerowicz.LatticeTensorField)) ∧
 176    Filter.Tendsto
 177      (fun N : ℕ => curvedDiscreteEigenvalue 1 rho N k)
 178      Filter.atTop (nhds (curvedContinuumEigenvalue 1 rho k)) ∧
 179    Filter.Tendsto
 180      (fun N : ℕ => curvedDiscreteEigenvalue 2 rho N k)
 181      Filter.atTop (nhds (curvedContinuumEigenvalue 2 rho k)) ∧
 182    curvedContinuumEigenvalue 1 rho k ≠
 183      curvedContinuumEigenvalue 2 rho k :=
 184  ⟨extensions_agree_on_entire_flat_specialization,
 185    fun N => extensions_distinct_at_nonzero_curvature rho hrho N,
 186    curvedDiscreteEigenvalue_tendsto 1 rho k,
 187    curvedDiscreteEigenvalue_tendsto 2 rho k,
 188    curvedContinuumEigenvalues_distinct rho hrho k⟩
 189
 190/-! ## Exact missing curved discretization-consistency premise -/
 191
 192/-- A curved discrete spectrum converges to its proposed curved continuum
 193spectrum at every curvature and wavenumber.  This is the Gap 4 target shape,
 194kept separate from the premise below. -/
 195def CurvedSpectrumConverges
 196    (discreteCurved : ℝ → ℕ → ℕ → ℝ)
 197    (continuumCurved : ℝ → ℕ → ℝ) : Prop :=
 198  ∀ rho k,
 199    Filter.Tendsto (fun N => discreteCurved rho N k)
 200      Filter.atTop (nhds (continuumCurved rho k))
 201
 202/-- The exact missing consistency premise relative to the certified flat
 203theorem: the discrete curvature correction converges to the continuum
 204curvature correction.  This does not assume the curved target itself; it
 205isolates the part absent from `DiscreteLichnerowicz`. -/
 206def CurvatureCorrectionConsistent
 207    (discreteCurved : ℝ → ℕ → ℕ → ℝ)
 208    (continuumCurved : ℝ → ℕ → ℝ) : Prop :=
 209  ∀ rho k,
 210    Filter.Tendsto
 211      (fun N =>
 212        discreteCurved rho N k - DiscreteLichnerowicz.discreteEigenvalue N k)
 213      Filter.atTop
 214      (nhds
 215        (continuumCurved rho k - DiscreteLichnerowicz.lichnerowiczFlatEigenvalue k))
 216
 217/-- Quantitative certificate form of curvature-correction consistency. -/
 218def CurvatureCorrectionRateBound
 219    (discreteCurved : ℝ → ℕ → ℕ → ℝ)
 220    (continuumCurved : ℝ → ℕ → ℝ) : Prop :=
 221  ∀ rho k, ∃ C : ℝ, ∃ N0 : ℕ, ∀ N : ℕ, N0 ≤ N →
 222    |(discreteCurved rho N k - DiscreteLichnerowicz.discreteEigenvalue N k) -
 223        (continuumCurved rho k - DiscreteLichnerowicz.lichnerowiczFlatEigenvalue k)|
 224      ≤ C / (N : ℝ) ^ 2
 225
 226/-- Blocker theorem: because the flat branch already converges, full curved
 227convergence is equivalent to convergence of precisely the omitted curvature
 228correction.  Thus the flat theorem cannot discharge the curved target unless
 229this independent consistency premise is supplied. -/
 230theorem curvedSpectrumConverges_iff_curvatureCorrectionConsistent
 231    (discreteCurved : ℝ → ℕ → ℕ → ℝ)
 232    (continuumCurved : ℝ → ℕ → ℝ) :
 233    CurvedSpectrumConverges discreteCurved continuumCurved ↔
 234      CurvatureCorrectionConsistent discreteCurved continuumCurved := by
 235  constructor
 236  · intro hCurved rho k
 237    exact (hCurved rho k).sub (DiscreteLichnerowicz.discreteEigenvalue_tendsto k)
 238  · intro hCorrection rho k
 239    have hSum :=
 240      (DiscreteLichnerowicz.discreteEigenvalue_tendsto k).add (hCorrection rho k)
 241    convert hSum using 1
 242    · funext N
 243      ring
 244    · congr 1
 245      rw [DiscreteLichnerowicz.lichnerowiczFlatEigenvalue]
 246      ring_nf
 247
 248/-- A quantitative `C / N^2` bound on the curvature correction supplies the
 249exact missing consistency premise, using the spectral convergence toolkit. -/
 250theorem curvatureCorrectionConsistent_of_rateBound
 251    (discreteCurved : ℝ → ℕ → ℕ → ℝ)
 252    (continuumCurved : ℝ → ℕ → ℝ)
 253    (hRate : CurvatureCorrectionRateBound discreteCurved continuumCurved) :
 254    CurvatureCorrectionConsistent discreteCurved continuumCurved := by
 255  intro rho k
 256  obtain ⟨C, N0, hBound⟩ := hRate rho k
 257  exact Gravity.Analysis.eigenvalue_limit_of_uniform_bound
 258    (fun N => discreteCurved rho N k - DiscreteLichnerowicz.discreteEigenvalue N k)
 259    (continuumCurved rho k - DiscreteLichnerowicz.lichnerowiczFlatEigenvalue k)
 260    C N0 hBound
 261
 262/-- Package theorem in the direction needed by a future curved
 263discretization: a proved correction-rate estimate, combined with the
 264existing flat convergence theorem, yields curved spectral convergence. -/
 265theorem curvedSpectrumConverges_of_correctionRateBound
 266    (discreteCurved : ℝ → ℕ → ℕ → ℝ)
 267    (continuumCurved : ℝ → ℕ → ℝ)
 268    (hRate : CurvatureCorrectionRateBound discreteCurved continuumCurved) :
 269    CurvedSpectrumConverges discreteCurved continuumCurved :=
 270  (curvedSpectrumConverges_iff_curvatureCorrectionConsistent
 271    discreteCurved continuumCurved).2
 272      (curvatureCorrectionConsistent_of_rateBound
 273        discreteCurved continuumCurved hRate)
 274
 275/-- Every scalar-coupling countermodel has a zero-error correction-rate
 276certificate.  Hence consistency alone cannot select the physical coupling;
 277the continuum curvature endomorphism itself must be independently derived. -/
 278theorem curvedEigenvalueFamily_rateBound (coupling : ℝ) :
 279    CurvatureCorrectionRateBound
 280      (fun rho N k => curvedDiscreteEigenvalue coupling rho N k)
 281      (fun rho k => curvedContinuumEigenvalue coupling rho k) := by
 282  intro rho k
 283  refine ⟨0, 1, ?_⟩
 284  intro N hN
 285  have hNpos : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hN
 286  simp only [curvedDiscreteEigenvalue, curvedContinuumEigenvalue]
 287  rw [show
 288      (DiscreteLichnerowicz.discreteEigenvalue N k + coupling * rho -
 289          DiscreteLichnerowicz.discreteEigenvalue N k) -
 290        (DiscreteLichnerowicz.lichnerowiczFlatEigenvalue k + coupling * rho -
 291          DiscreteLichnerowicz.lichnerowiczFlatEigenvalue k) = 0 by ring]
 292  simp
 293
 294/-- Final certified blocker.  Coefficients one and two both satisfy the same
 295flat specialization and the same quantitative correction-consistency shape,
 296yet they are distinct at every nonzero curvature.  Therefore the existing
 297flat spectrum theorem plus generic consistency machinery does not determine
 298the curved Lichnerowicz curvature coupling. -/
 299theorem gap4_curvature_coupling_blocker
 300    (rho : ℝ) (hrho : rho ≠ 0) :
 301    (∀ (N : ℕ) (H : DiscreteLichnerowicz.LatticeTensorField),
 302      singleCurvatureExtension 0 N H = doubleCurvatureExtension 0 N H) ∧
 303    (∀ N : ℕ,
 304      (singleCurvatureExtension rho N :
 305          DiscreteLichnerowicz.LatticeTensorField → DiscreteLichnerowicz.LatticeTensorField) ≠
 306        (doubleCurvatureExtension rho N :
 307          DiscreteLichnerowicz.LatticeTensorField → DiscreteLichnerowicz.LatticeTensorField)) ∧
 308    CurvatureCorrectionRateBound
 309      (fun r N k => curvedDiscreteEigenvalue 1 r N k)
 310      (fun r k => curvedContinuumEigenvalue 1 r k) ∧
 311    CurvatureCorrectionRateBound
 312      (fun r N k => curvedDiscreteEigenvalue 2 r N k)
 313      (fun r k => curvedContinuumEigenvalue 2 r k) :=
 314  ⟨extensions_agree_on_entire_flat_specialization,
 315    fun N => extensions_distinct_at_nonzero_curvature rho hrho N,
 316    curvedEigenvalueFamily_rateBound 1,
 317    curvedEigenvalueFamily_rateBound 2⟩
 318
 319end
 320
 321end CurvedOperatorUnderdetermination
 322end SevenGaps
 323end Gravity
 324end IndisputableMonolith
 325
 326#print axioms IndisputableMonolith.Gravity.SevenGaps.CurvedOperatorUnderdetermination.extensions_agree_on_entire_flat_specialization
 327#print axioms IndisputableMonolith.Gravity.SevenGaps.CurvedOperatorUnderdetermination.extensions_distinct_at_nonzero_curvature
 328#print axioms IndisputableMonolith.Gravity.SevenGaps.CurvedOperatorUnderdetermination.flat_spectrum_underdetermines_curvature_coupling
 329#print axioms IndisputableMonolith.Gravity.SevenGaps.CurvedOperatorUnderdetermination.curvedSpectrumConverges_iff_curvatureCorrectionConsistent
 330#print axioms IndisputableMonolith.Gravity.SevenGaps.CurvedOperatorUnderdetermination.curvedSpectrumConverges_of_correctionRateBound
 331#print axioms IndisputableMonolith.Gravity.SevenGaps.CurvedOperatorUnderdetermination.gap4_curvature_coupling_blocker
 332