IndisputableMonolith.Geometry.ReggeActionSmoothness

   1import Mathlib
   2import IndisputableMonolith.Geometry.AffineIndepInterior
   3import IndisputableMonolith.Geometry.CofactorDerivatives
   4import IndisputableMonolith.Geometry.ReggeActionConcrete
   5
   6/-!
   7# Smoothness Inputs for the Nonlinear Regge Action
   8
   9The closed second-order component theorem works with an exact quadratic
  10truncation.  The full nonlinear action needs analytic input: the conformal
  11edge chart must stay in the nondegenerate tetrahedral cone, the arccos
  12arguments must stay away from `±1`, and the finite Regge action must be
  13smooth at the flat potential.
  14
  15This module records those analytic requirements as a named configuration
  16rather than hiding them as axioms.  The lower-level polynomial and strict
  17interior facts already proved in the geometry stack are exposed as supporting
  18lemmas.
  19-/
  20
  21namespace IndisputableMonolith
  22namespace Geometry
  23namespace ReggeActionSmoothness
  24
  25open ReggeTriangulation3D
  26open ReggeHessian3D
  27open Triangulation3DConsistency
  28open ReggeActionConcrete
  29open DihedralCayleyMenger
  30open CofactorDerivatives
  31open AffineIndepInterior
  32
  33noncomputable section
  34
  35/-- Global zero-deficit flatness is an assembled-triangulation condition.  It
  36does not follow from local nondegeneracy of each tetrahedron. -/
  37def GlobalZeroDeficitAtFlat (K : Triangulation3D) : Prop :=
  38  ∀ e : Fin K.nE, deficitAngle K (zeroPotential K) e = 0
  39
  40/-- Local analytic chart data supplied by Euclidean realizations of every
  41tetrahedron in the triangulation.  This is the local ingredient behind strict
  42arccos endpoint avoidance. -/
  43structure LocalAnalyticFlatChart (K : Triangulation3D) where
  44  realizedTet : ∀ _τ : Fin K.nT, RealizedNonDegenerateTet
  45  realizes_tet : ∀ τ : Fin K.nT, (realizedTet τ).tet = K.tet τ
  46
  47theorem LocalAnalyticFlatChart.local_arccos_endpoint_free
  48    {K : Triangulation3D} (hChart : LocalAnalyticFlatChart K) :
  49    ∀ τ : Fin K.nT, ∀ f : Fin 6,
  50      dihedralCos3Sq ((K.tet τ).sqEdge) f ≠ -1 ∧
  51        dihedralCos3Sq ((K.tet τ).sqEdge) f ≠ 1 := by
  52  intro τ f
  53  have hstrict := (hChart.realizedTet τ).dihedralCos3_strict_interior f
  54  have ht : (hChart.realizedTet τ).tet = K.tet τ := hChart.realizes_tet τ
  55  have hstrict' :
  56      -1 < dihedralCos3Sq ((K.tet τ).sqEdge) f ∧
  57        dihedralCos3Sq ((K.tet τ).sqEdge) f < 1 := by
  58    simpa [dihedralCos3, ht] using hstrict
  59  exact DihedralDerivatives.arccos_endpoint_hypotheses_of_interior hstrict'.1 hstrict'.2
  60
  61/-- Smoothness closure for the full nonlinear action from a local analytic
  62chart.  This is the next lower-level target: prove it from the explicit
  63`exp`/cofactor/`sqrt`/`arccos` chain. -/
  64structure ReggeActionContDiffFromLocalChart
  65    (K : Triangulation3D) (hK : IncidenceConsistent K)
  66    (_hChart : LocalAnalyticFlatChart K) where
  67  action_contDiff_at_zero :
  68    ContDiffAt ℝ (⊤ : ℕ∞) (reggeAction K hK) (zeroPotential K)
  69
  70/-- A flat analytic configuration for the nonlinear Regge action.  The first
  71field is the arccos endpoint condition at the base point.  The second field is
  72the zero-deficit flatness condition.  The final field is the smoothness fact
  73needed to invoke Taylor theory for the full nonlinear action. -/
  74structure FlatConfiguration (K : Triangulation3D) (hK : IncidenceConsistent K) where
  75  local_arccos_endpoint_free :
  76    ∀ τ : Fin K.nT, ∀ f : Fin 6,
  77      dihedralCos3Sq ((K.tet τ).sqEdge) f ≠ -1 ∧
  78        dihedralCos3Sq ((K.tet τ).sqEdge) f ≠ 1
  79  flat_deficit_zero :
  80    ∀ e : Fin K.nE, deficitAngle K (zeroPotential K) e = 0
  81  action_contDiff_at_zero :
  82    ContDiffAt ℝ (⊤ : ℕ∞) (reggeAction K hK) (zeroPotential K)
  83
  84/-- Construct the current flat-configuration package from local realized
  85tetrahedra, a separately stated global zero-deficit condition, and the
  86smoothness theorem for the local chart. -/
  87def flatConfiguration_of_localChart_zeroDeficit
  88    (K : Triangulation3D) (hK : IncidenceConsistent K)
  89    (hChart : LocalAnalyticFlatChart K)
  90    (hZero : GlobalZeroDeficitAtFlat K)
  91    (hSmooth : ReggeActionContDiffFromLocalChart K hK hChart) :
  92    FlatConfiguration K hK where
  93  local_arccos_endpoint_free := hChart.local_arccos_endpoint_free
  94  flat_deficit_zero := hZero
  95  action_contDiff_at_zero := hSmooth.action_contDiff_at_zero
  96
  97/-- Nondegenerate tetrahedra already give positive polynomial cofactor
  98denominators for every local dihedral angle. -/
  99theorem local_dihedralDenom3Poly_pos
 100    (K : Triangulation3D) (τ : Fin K.nT) (f : Fin 6) :
 101    0 < dihedralDenom3Poly ((K.tet τ).sqEdge) f :=
 102  dihedralDenom3Poly_pos_of_nonDegenerate (K.tet τ) f
 103
 104/-- Nondegenerate tetrahedra already give nonzero polynomial cofactor
 105denominators for every local dihedral angle. -/
 106theorem local_dihedralDenom3Poly_ne_zero
 107    (K : Triangulation3D) (τ : Fin K.nT) (f : Fin 6) :
 108    dihedralDenom3Poly ((K.tet τ).sqEdge) f ≠ 0 :=
 109  ne_of_gt (local_dihedralDenom3Poly_pos K τ f)
 110
 111theorem local_dihedralDenom3_ne_zero
 112    (K : Triangulation3D) (τ : Fin K.nT) (f : Fin 6) :
 113    dihedralDenom3 ((K.tet τ).sqEdge) f ≠ 0 := by
 114  rw [dihedralDenom3_eq_poly]
 115  exact local_dihedralDenom3Poly_ne_zero K τ f
 116
 117theorem dihedralDenom3_continuousAt
 118    (a : CayleyMengerPolynomial.SqEdges) (f : Fin 6) :
 119    ContinuousAt (fun x : CayleyMengerPolynomial.SqEdges => dihedralDenom3 x f) a := by
 120  unfold dihedralDenom3
 121  let p := (DihedralCayleyMenger.oppositeCMVertices f).1
 122  let q := (DihedralCayleyMenger.oppositeCMVertices f).2
 123  have hp : ContinuousAt (fun x : CayleyMengerPolynomial.SqEdges =>
 124      CayleyMengerMatrix.cmCofactor3 x p p) a :=
 125    (CayleyMengerMatrix.cmCofactor3_contDiff 0 p p).continuous.continuousAt
 126  have hq : ContinuousAt (fun x : CayleyMengerPolynomial.SqEdges =>
 127      CayleyMengerMatrix.cmCofactor3 x q q) a :=
 128    (CayleyMengerMatrix.cmCofactor3_contDiff 0 q q).continuous.continuousAt
 129  simpa [p, q] using (hp.mul hq).sqrt
 130
 131theorem dihedralCos3Sq_continuousAt_of_den_ne_zero
 132    (a : CayleyMengerPolynomial.SqEdges) (f : Fin 6)
 133    (hden : dihedralDenom3 a f ≠ 0) :
 134    ContinuousAt (fun x : CayleyMengerPolynomial.SqEdges => dihedralCos3Sq x f) a := by
 135  unfold dihedralCos3Sq
 136  exact (CayleyMengerMatrix.cmCofactor3_contDiff 0
 137      (DihedralCayleyMenger.oppositeCMVertices f).1
 138      (DihedralCayleyMenger.oppositeCMVertices f).2).continuous.continuousAt.div
 139    (dihedralDenom3_continuousAt a f) hden
 140
 141theorem local_dihedralCos3Sq_continuousAt
 142    (K : Triangulation3D) (τ : Fin K.nT) (f : Fin 6) :
 143    ContinuousAt (fun x : CayleyMengerPolynomial.SqEdges => dihedralCos3Sq x f)
 144      ((K.tet τ).sqEdge) :=
 145  dihedralCos3Sq_continuousAt_of_den_ne_zero ((K.tet τ).sqEdge) f
 146    (local_dihedralDenom3_ne_zero K τ f)
 147
 148theorem conformalLocalSqEdge_contDiff
 149    (K : Triangulation3D) (τ : Fin K.nT) (f : Fin 6) (n : ℕ∞) :
 150    ContDiff ℝ n (fun ξ : VertexPotential K => conformalLocalSqEdge K ξ τ f) := by
 151  unfold conformalLocalSqEdge
 152  fun_prop
 153
 154theorem conformalLocalSqEdge_contDiffAt_zero
 155    (K : Triangulation3D) (τ : Fin K.nT) (f : Fin 6) (n : ℕ∞) :
 156    ContDiffAt ℝ n
 157      (fun ξ : VertexPotential K => conformalLocalSqEdge K ξ τ f)
 158      (zeroPotential K) :=
 159  (conformalLocalSqEdge_contDiff K τ f n).contDiffAt
 160
 161theorem conformalTetSqEdges_contDiff
 162    (K : Triangulation3D) (τ : Fin K.nT) (n : ℕ∞) :
 163    ContDiff ℝ n (fun ξ : VertexPotential K => conformalTetSqEdges K ξ τ) := by
 164  rw [contDiff_pi]
 165  intro f
 166  exact conformalLocalSqEdge_contDiff K τ f n
 167
 168theorem conformalTetSqEdges_zero
 169    (K : Triangulation3D) (τ : Fin K.nT) :
 170    conformalTetSqEdges K (zeroPotential K) τ = (K.tet τ).sqEdge := by
 171  funext f
 172  unfold conformalTetSqEdges conformalLocalSqEdge zeroPotential
 173  simp [Real.exp_zero]
 174
 175theorem dihedralCos3Sq_conformal_continuousAt_zero
 176    (K : Triangulation3D) (τ : Fin K.nT) (f : Fin 6) :
 177    ContinuousAt (fun ξ : VertexPotential K =>
 178      dihedralCos3Sq (conformalTetSqEdges K ξ τ) f) (zeroPotential K) := by
 179  have hbase := local_dihedralCos3Sq_continuousAt K τ f
 180  have hchart : ContinuousAt (fun ξ : VertexPotential K =>
 181      conformalTetSqEdges K ξ τ) (zeroPotential K) :=
 182    (conformalTetSqEdges_contDiff K τ 0).continuous.continuousAt
 183  have hbase' : ContinuousAt
 184      (fun x : CayleyMengerPolynomial.SqEdges => dihedralCos3Sq x f)
 185      (conformalTetSqEdges K (zeroPotential K) τ) := by
 186    simpa [conformalTetSqEdges_zero K τ] using hbase
 187  exact ContinuousAt.comp
 188    (f := fun ξ : VertexPotential K => conformalTetSqEdges K ξ τ)
 189    (g := fun x : CayleyMengerPolynomial.SqEdges => dihedralCos3Sq x f)
 190    (x := zeroPotential K)
 191    hbase' hchart
 192
 193theorem cmCofactor3_conformal_contDiff
 194    (K : Triangulation3D) (τ : Fin K.nT) (r c : Fin 5) (n : ℕ∞) :
 195    ContDiff ℝ n (fun ξ : VertexPotential K =>
 196      CayleyMengerMatrix.cmCofactor3 (conformalTetSqEdges K ξ τ) r c) :=
 197  (CayleyMengerMatrix.cmCofactor3_contDiff n r c).comp
 198    (conformalTetSqEdges_contDiff K τ n)
 199
 200theorem cmCofactor3_conformal_contDiffAt_zero
 201    (K : Triangulation3D) (τ : Fin K.nT) (r c : Fin 5) (n : ℕ∞) :
 202    ContDiffAt ℝ n (fun ξ : VertexPotential K =>
 203      CayleyMengerMatrix.cmCofactor3 (conformalTetSqEdges K ξ τ) r c)
 204      (zeroPotential K) :=
 205  (cmCofactor3_conformal_contDiff K τ r c n).contDiffAt
 206
 207theorem dihedralDenom3_conformal_contDiffAt_zero
 208    (K : Triangulation3D) (τ : Fin K.nT) (f : Fin 6) (n : ℕ∞) :
 209    ContDiffAt ℝ n (fun ξ : VertexPotential K =>
 210      dihedralDenom3 (conformalTetSqEdges K ξ τ) f) (zeroPotential K) := by
 211  unfold dihedralDenom3
 212  let p := (DihedralCayleyMenger.oppositeCMVertices f).1
 213  let q := (DihedralCayleyMenger.oppositeCMVertices f).2
 214  have hp := cmCofactor3_conformal_contDiffAt_zero K τ p p n
 215  have hq := cmCofactor3_conformal_contDiffAt_zero K τ q q n
 216  have hprod : ContDiffAt ℝ n (fun ξ : VertexPotential K =>
 217      CayleyMengerMatrix.cmCofactor3 (conformalTetSqEdges K ξ τ) p p *
 218        CayleyMengerMatrix.cmCofactor3 (conformalTetSqEdges K ξ τ) q q)
 219      (zeroPotential K) :=
 220    hp.mul hq
 221  have hne :
 222      CayleyMengerMatrix.cmCofactor3 (conformalTetSqEdges K (zeroPotential K) τ) p p *
 223        CayleyMengerMatrix.cmCofactor3 (conformalTetSqEdges K (zeroPotential K) τ) q q ≠ 0 := by
 224    have hden := local_dihedralDenom3_ne_zero K τ f
 225    unfold dihedralDenom3 at hden
 226    intro hprod_zero
 227    apply hden
 228    rw [conformalTetSqEdges_zero K τ] at hprod_zero
 229    simp [p, q, hprod_zero]
 230  simpa [p, q] using hprod.sqrt hne
 231
 232theorem dihedralCos3Sq_conformal_contDiffAt_zero
 233    (K : Triangulation3D) (τ : Fin K.nT) (f : Fin 6) (n : ℕ∞) :
 234    ContDiffAt ℝ n (fun ξ : VertexPotential K =>
 235      dihedralCos3Sq (conformalTetSqEdges K ξ τ) f) (zeroPotential K) := by
 236  unfold dihedralCos3Sq
 237  let p := (DihedralCayleyMenger.oppositeCMVertices f).1
 238  let q := (DihedralCayleyMenger.oppositeCMVertices f).2
 239  have hnum := cmCofactor3_conformal_contDiffAt_zero K τ p q n
 240  have hden := dihedralDenom3_conformal_contDiffAt_zero K τ f n
 241  have hden_ne :
 242      dihedralDenom3 (conformalTetSqEdges K (zeroPotential K) τ) f ≠ 0 := by
 243    simpa [conformalTetSqEdges_zero K τ] using local_dihedralDenom3_ne_zero K τ f
 244  simpa [p, q] using hnum.div hden hden_ne
 245
 246theorem tetDihedralAngleUnderConformal_contDiffAt_zero
 247    (K : Triangulation3D) (τ : Fin K.nT) (f : Fin 6) (n : ℕ∞)
 248    (hEndpoint :
 249      dihedralCos3Sq ((K.tet τ).sqEdge) f ≠ -1 ∧
 250        dihedralCos3Sq ((K.tet τ).sqEdge) f ≠ 1) :
 251    ContDiffAt ℝ n (fun ξ : VertexPotential K =>
 252      tetDihedralAngleUnderConformal K ξ τ f) (zeroPotential K) := by
 253  unfold tetDihedralAngleUnderConformal DihedralDerivatives.dihedralAngle3Sq
 254  have hcos := dihedralCos3Sq_conformal_contDiffAt_zero K τ f n
 255  have hm :
 256      dihedralCos3Sq (conformalTetSqEdges K (zeroPotential K) τ) f ≠ -1 := by
 257    simpa [conformalTetSqEdges_zero K τ] using hEndpoint.1
 258  have hp :
 259      dihedralCos3Sq (conformalTetSqEdges K (zeroPotential K) τ) f ≠ 1 := by
 260    simpa [conformalTetSqEdges_zero K τ] using hEndpoint.2
 261  have hacos : ContDiffAt ℝ n Real.arccos
 262      (dihedralCos3Sq (conformalTetSqEdges K (zeroPotential K) τ) f) :=
 263    Real.contDiffAt_arccos hm hp
 264  simpa [Function.comp_def] using
 265    (ContDiffAt.comp (x := zeroPotential K) hacos hcos)
 266
 267theorem localDeficitAngleContribution_contDiffAt_zero
 268    (K : Triangulation3D) (e : Fin K.nE) (τ : Fin K.nT) (n : ℕ∞)
 269    (hEndpoint :
 270      ∀ f : Fin 6,
 271        dihedralCos3Sq ((K.tet τ).sqEdge) f ≠ -1 ∧
 272          dihedralCos3Sq ((K.tet τ).sqEdge) f ≠ 1) :
 273    ContDiffAt ℝ n (fun ξ : VertexPotential K =>
 274      localDeficitAngleContribution K ξ e τ) (zeroPotential K) := by
 275  unfold localDeficitAngleContribution
 276  cases h : K.edgeInTet e τ with
 277  | none =>
 278      simpa [h]
 279        using (contDiffAt_const :
 280          ContDiffAt ℝ n (fun _ξ : VertexPotential K => (0 : ℝ)) (zeroPotential K))
 281  | some f =>
 282      simpa [h] using tetDihedralAngleUnderConformal_contDiffAt_zero
 283        K τ f n (hEndpoint f)
 284
 285theorem deficitAngle_contDiffAt_zero
 286    (K : Triangulation3D) (e : Fin K.nE) (n : ℕ∞)
 287    (hEndpoint :
 288      ∀ τ : Fin K.nT, ∀ f : Fin 6,
 289        dihedralCos3Sq ((K.tet τ).sqEdge) f ≠ -1 ∧
 290          dihedralCos3Sq ((K.tet τ).sqEdge) f ≠ 1) :
 291    ContDiffAt ℝ n (fun ξ : VertexPotential K => deficitAngle K ξ e)
 292      (zeroPotential K) := by
 293  unfold deficitAngle
 294  have hsum : ContDiffAt ℝ n
 295      (fun ξ : VertexPotential K =>
 296        ∑ τ : Fin K.nT, localDeficitAngleContribution K ξ e τ)
 297      (zeroPotential K) := by
 298    simpa using
 299      (ContDiffAt.sum
 300        (s := Finset.univ)
 301        (f := fun τ ξ => localDeficitAngleContribution K ξ e τ)
 302        (x := zeroPotential K)
 303        (fun τ _ => localDeficitAngleContribution_contDiffAt_zero
 304          K e τ n (hEndpoint τ)))
 305  exact (contDiffAt_const.sub hsum)
 306
 307theorem hingeMeasureUnderConformal_contDiff
 308    (K : Triangulation3D) (hK : IncidenceConsistent K) (e : Fin K.nE) (n : ℕ∞) :
 309    ContDiff ℝ n (fun ξ : VertexPotential K =>
 310      hingeMeasureUnderConformal K hK ξ e) := by
 311  unfold hingeMeasureUnderConformal
 312  fun_prop
 313
 314theorem hingeMeasureUnderConformal_contDiffAt_zero
 315    (K : Triangulation3D) (hK : IncidenceConsistent K) (e : Fin K.nE) (n : ℕ∞) :
 316    ContDiffAt ℝ n (fun ξ : VertexPotential K =>
 317      hingeMeasureUnderConformal K hK ξ e) (zeroPotential K) :=
 318  (hingeMeasureUnderConformal_contDiff K hK e n).contDiffAt
 319
 320theorem reggeAction_contDiffAt_zero_of_endpoint_free
 321    (K : Triangulation3D) (hK : IncidenceConsistent K)
 322    (hEndpoint :
 323      ∀ τ : Fin K.nT, ∀ f : Fin 6,
 324        dihedralCos3Sq ((K.tet τ).sqEdge) f ≠ -1 ∧
 325          dihedralCos3Sq ((K.tet τ).sqEdge) f ≠ 1) :
 326    ContDiffAt ℝ (⊤ : ℕ∞) (reggeAction K hK) (zeroPotential K) := by
 327  unfold reggeAction
 328  simpa using
 329    (ContDiffAt.sum
 330      (s := Finset.univ)
 331      (f := fun e ξ =>
 332        hingeMeasureUnderConformal K hK ξ e * deficitAngle K ξ e)
 333      (x := zeroPotential K)
 334      (fun e _ =>
 335        (hingeMeasureUnderConformal_contDiffAt_zero K hK e (⊤ : ℕ∞)).mul
 336          (deficitAngle_contDiffAt_zero K e ⊤ hEndpoint)))
 337
 338theorem reggeAction_contDiffAt_zero_of_localChart
 339    (K : Triangulation3D) (hK : IncidenceConsistent K)
 340    (hChart : LocalAnalyticFlatChart K) :
 341    ContDiffAt ℝ (⊤ : ℕ∞) (reggeAction K hK) (zeroPotential K) :=
 342  reggeAction_contDiffAt_zero_of_endpoint_free K hK
 343    hChart.local_arccos_endpoint_free
 344
 345def reggeActionContDiffFromLocalChart_of_localChart
 346    (K : Triangulation3D) (hK : IncidenceConsistent K)
 347    (hChart : LocalAnalyticFlatChart K) :
 348    ReggeActionContDiffFromLocalChart K hK hChart where
 349  action_contDiff_at_zero :=
 350    reggeAction_contDiffAt_zero_of_localChart K hK hChart
 351
 352/-- Phase-A smoothness theorem for the nonlinear action, conditional on the
 353named flat analytic configuration. -/
 354theorem reggeAction_contDiff_at_zero
 355    (K : Triangulation3D) (hK : IncidenceConsistent K)
 356    (h_flat : FlatConfiguration K hK) :
 357    ContDiffAt ℝ (⊤ : ℕ∞) (reggeAction K hK) (zeroPotential K) :=
 358  h_flat.action_contDiff_at_zero
 359
 360/-- Flat configurations have zero deficit at the base potential. -/
 361theorem deficitAngle_zero_of_flat
 362    (K : Triangulation3D) (hK : IncidenceConsistent K)
 363    (h_flat : FlatConfiguration K hK) :
 364    ∀ e : Fin K.nE, deficitAngle K (zeroPotential K) e = 0 :=
 365  h_flat.flat_deficit_zero
 366
 367end
 368
 369end ReggeActionSmoothness
 370end Geometry
 371end IndisputableMonolith
 372