IndisputableMonolith.Geometry.ReggeActionNonlinearCorrespondence

   1import IndisputableMonolith.Geometry.ReggeActionCubicTaylorBound
   2import IndisputableMonolith.Cost.FunctionalEquation
   3
   4/-!
   5# Nonlinear Regge/J-Cost Correspondence Target
   6
   7The first Recognition Gravity paper closes the weak-field quadratic bridge.
   8This module states the follow-on nonlinear target without claiming global exact
   9equality between the full Regge action and a summed J-cost action.
  10
  11The theorem surface is local: near a flat configuration, the full nonlinear
  12Regge action equals its flat value plus the canonical J/Dirichlet quadratic
  13term, with an explicitly bounded cubic Taylor remainder.
  14-/
  15
  16namespace IndisputableMonolith
  17namespace Geometry
  18namespace ReggeActionNonlinearCorrespondence
  19
  20open ReggeTriangulation3D
  21open ReggeHessian3D
  22open Triangulation3DConsistency
  23open ReggeActionConcrete
  24open ReggeActionSmoothness
  25open ReggeActionSecondVariation
  26open ReggeActionNonlinearHessianProof
  27open ReggeActionCubicTaylorBound
  28
  29noncomputable section
  30
  31/-- J-cost in log coordinates. -/
  32def jCostLog (t : ℝ) : ℝ :=
  33  Cost.Jcost (Real.exp t)
  34
  35theorem jCostLog_eq_cosh_sub_one (t : ℝ) :
  36    jCostLog t = Real.cosh t - 1 := by
  37  simpa [jCostLog, Cost.FunctionalEquation.G] using
  38    Cost.FunctionalEquation.Jcost_G_eq_cosh_sub_one t
  39
  40theorem jCostLog_neg (t : ℝ) :
  41    jCostLog (-t) = jCostLog t := by
  42  rw [jCostLog_eq_cosh_sub_one, jCostLog_eq_cosh_sub_one]
  43  rw [Real.cosh_neg]
  44
  45/-- The full weighted J-cost edge action associated to the canonical incidence
  46weights.  This is the nonlinear J-cost expression; the present local theorem
  47uses only its quadratic jet. -/
  48def weightedJCostAction
  49    (K : Triangulation3D) (hK : IncidenceConsistent K)
  50    (ξ : VertexPotential K) : ℝ :=
  51  ∑ i : Fin K.nV, ∑ j : Fin K.nV,
  52    canonicalDualWeight K hK i j * jCostLog (ξ i - ξ j)
  53
  54theorem weightedJCostAction_neg
  55    (K : Triangulation3D) (hK : IncidenceConsistent K)
  56    (ξ : VertexPotential K) :
  57    weightedJCostAction K hK (-ξ) = weightedJCostAction K hK ξ := by
  58  unfold weightedJCostAction
  59  refine Finset.sum_congr rfl ?_
  60  intro i _
  61  refine Finset.sum_congr rfl ?_
  62  intro j _
  63  change canonicalDualWeight K hK i j * jCostLog ((-ξ) i - (-ξ) j) =
  64    canonicalDualWeight K hK i j * jCostLog (ξ i - ξ j)
  65  congr 1
  66  have harg : ((-ξ) i - (-ξ) j) = -(ξ i - ξ j) := by
  67    simp
  68    ring
  69  rw [harg, jCostLog_neg]
  70
  71theorem weightedJCostAction_along_line_even
  72    (K : Triangulation3D) (hK : IncidenceConsistent K)
  73    (ξ : VertexPotential K) :
  74    Function.Even
  75      (fun t : ℝ => weightedJCostAction K hK (linePotential K ξ t)) := by
  76  intro t
  77  change weightedJCostAction K hK (linePotential K ξ (-t)) =
  78    weightedJCostAction K hK (linePotential K ξ t)
  79  have hline : linePotential K ξ (-t) = -(linePotential K ξ t) := by
  80    funext i
  81    simp [linePotential]
  82  rw [hline]
  83  exact weightedJCostAction_neg K hK (linePotential K ξ t)
  84
  85/-- The canonical quadratic J/Dirichlet term supplied by the Regge incidence
  86Hessian.  This is the term that the full nonlinear Regge action sees to second
  87order at a flat background. -/
  88def canonicalJQuadraticTerm
  89    (K : Triangulation3D) (hK : IncidenceConsistent K)
  90    (ξ : VertexPotential K) : ℝ :=
  91  (1 / 2) * hessianQuadratic (canonicalReggeHessian K hK) ξ
  92
  93theorem canonicalJQuadraticTerm_eq_dirichlet
  94    (K : Triangulation3D) (hK : IncidenceConsistent K)
  95    (ξ : VertexPotential K) :
  96    canonicalJQuadraticTerm K hK ξ =
  97      (1 / 2) * canonicalDirichletEnergy K hK ξ := by
  98  unfold canonicalJQuadraticTerm
  99  rw [canonicalReggeHessian_quadratic_eq_dirichlet]
 100
 101theorem canonicalJQuadraticTerm_nonneg
 102    (K : Triangulation3D) (hK : IncidenceConsistent K)
 103    (ξ : VertexPotential K) :
 104    0 ≤ canonicalJQuadraticTerm K hK ξ := by
 105  rw [canonicalJQuadraticTerm_eq_dirichlet]
 106  exact mul_nonneg (by norm_num) (canonicalDirichletEnergy_nonneg K hK ξ)
 107
 108/-- Exact algebraic split of the full nonlinear Regge action into the flat
 109value, the canonical quadratic J/Dirichlet term, and the nonlinear remainder. -/
 110theorem nonlinearRegge_exact_canonical_split
 111    (K : Triangulation3D) (hK : IncidenceConsistent K)
 112    (ξ : VertexPotential K) :
 113    reggeAction K hK ξ =
 114      reggeAction K hK (zeroPotential K) +
 115        canonicalJQuadraticTerm K hK ξ +
 116        reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ := by
 117  simpa [canonicalJQuadraticTerm] using
 118    reggeAction_taylor_decomposition K hK (canonicalReggeHessian K hK) ξ
 119
 120/-- Local nonlinear Regge/J-cost correspondence: the full action differs from
 121its flat value plus the canonical J/Dirichlet quadratic jet by a cubic
 122remainder. -/
 123def NonlinearReggeJCostLocalCorrespondence
 124    (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
 125  ∃ (r C : ℝ), 0 < r ∧ 0 ≤ C ∧
 126    ∀ ξ : VertexPotential K, ‖ξ‖ < r →
 127      ‖reggeAction K hK ξ -
 128          reggeAction K hK (zeroPotential K) -
 129          canonicalJQuadraticTerm K hK ξ‖ ≤
 130        C * ‖ξ‖ ^ (3 : ℕ)
 131
 132/-- The strongest true nonlinear Regge/J-cost replacement theorem surface.
 133
 134This is deliberately local and quadratic-core: it says the full nonlinear
 135Regge action equals its flat value plus the canonical J/Dirichlet quadratic
 136term up to a controlled cubic remainder.  It does not assert literal equality
 137with the full weighted J-cost action. -/
 138def StrongestTrueReggeJCostReplacement
 139    (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
 140  NonlinearReggeJCostLocalCorrespondence K hK
 141
 142theorem strongestTrueReggeJCostReplacement_iff_localCorrespondence
 143    (K : Triangulation3D) (hK : IncidenceConsistent K) :
 144    StrongestTrueReggeJCostReplacement K hK ↔
 145      NonlinearReggeJCostLocalCorrespondence K hK :=
 146  Iff.rfl
 147
 148theorem nonlinearRegge_localCorrespondence_of_cubicBound
 149    (K : Triangulation3D) (hK : IncidenceConsistent K)
 150    (hBound : LocalCubicRemainderBound K hK) :
 151    NonlinearReggeJCostLocalCorrespondence K hK := by
 152  rcases hBound with ⟨r, C, hr, hC, hineq⟩
 153  refine ⟨r, C, hr, hC, ?_⟩
 154  intro ξ hξ
 155  simpa [NonlinearReggeJCostLocalCorrespondence, canonicalJQuadraticTerm,
 156    reggeActionRemainder, sub_eq_add_neg, add_assoc, add_left_comm, add_comm]
 157    using hineq ξ hξ
 158
 159theorem nonlinearRegge_localCorrespondence_of_taylorTheorem
 160    (K : Triangulation3D) (hK : IncidenceConsistent K)
 161    (hTaylor : NonlinearReggeCubicTaylorTheorem K hK) :
 162    NonlinearReggeJCostLocalCorrespondence K hK :=
 163  nonlinearRegge_localCorrespondence_of_cubicBound K hK hTaylor
 164
 165theorem nonlinearRegge_localCorrespondence_of_localHessianTaylorInputs
 166    (K : Triangulation3D) (hK : IncidenceConsistent K)
 167    (hFlat : FlatConfiguration K hK)
 168    (hInputs : NonlinearReggeLocalHessianTaylorInputs K hK hFlat) :
 169    NonlinearReggeJCostLocalCorrespondence K hK :=
 170  nonlinearRegge_localCorrespondence_of_cubicBound K hK
 171    hInputs.cubic_remainder.cubic_bound
 172
 173theorem nonlinearRegge_localCorrespondence_of_eventuallyZero_edgeStencil_and_taylor
 174    (K : Triangulation3D) (hK : IncidenceConsistent K)
 175    (hFlat : FlatConfiguration K hK)
 176    (D : ReggeActionFirstVariation.DeficitAngleDirectionalDerivativePackage K hK)
 177    (hZero : WeightedDeficitDerivativeEventuallyZeroTarget K hK hFlat)
 178    (hEdge : MixedHingeDeficitEdgeStencilTarget K hK D)
 179    (hStencil : CanonicalDirichletEqualsEdgeStencilTarget K hK)
 180    (hTaylor : NonlinearReggeCubicTaylorTheorem K hK) :
 181    NonlinearReggeJCostLocalCorrespondence K hK :=
 182  nonlinearRegge_localCorrespondence_of_localHessianTaylorInputs K hK hFlat
 183    (nonlinearReggeLocalHessianTaylorInputs_of_eventuallyZero_edgeStencil_and_taylor
 184      K hK hFlat D hZero hEdge hStencil hTaylor)
 185
 186theorem strongestTrueReggeJCostReplacement_of_eventuallyZero_edgeStencil_and_taylor
 187    (K : Triangulation3D) (hK : IncidenceConsistent K)
 188    (hFlat : FlatConfiguration K hK)
 189    (D : ReggeActionFirstVariation.DeficitAngleDirectionalDerivativePackage K hK)
 190    (hZero : WeightedDeficitDerivativeEventuallyZeroTarget K hK hFlat)
 191    (hEdge : MixedHingeDeficitEdgeStencilTarget K hK D)
 192    (hStencil : CanonicalDirichletEqualsEdgeStencilTarget K hK)
 193    (hTaylor : NonlinearReggeCubicTaylorTheorem K hK) :
 194    StrongestTrueReggeJCostReplacement K hK :=
 195  nonlinearRegge_localCorrespondence_of_eventuallyZero_edgeStencil_and_taylor
 196    K hK hFlat D hZero hEdge hStencil hTaylor
 197
 198theorem nonlinearRegge_localCorrespondence_of_remainder_identically_zero
 199    (K : Triangulation3D) (hK : IncidenceConsistent K)
 200    (hZero :
 201      ∀ ξ : VertexPotential K,
 202        reggeActionRemainder K hK (canonicalReggeHessian K hK) ξ = 0) :
 203    NonlinearReggeJCostLocalCorrespondence K hK :=
 204  nonlinearRegge_localCorrespondence_of_taylorTheorem K hK
 205    (nonlinearReggeCubicTaylorTheorem_of_identically_zero K hK hZero)
 206
 207end
 208
 209end ReggeActionNonlinearCorrespondence
 210end Geometry
 211end IndisputableMonolith
 212