IndisputableMonolith.Gravity.RestrictedIncidenceRecovery

   1import IndisputableMonolith.Gravity.DiscreteVacuumEinstein
   2
   3/-!
   4# Restricted Incidence Recovery
   5
   6The unrestricted recovery predicate in `DiscreteVacuumEinstein` asks vertex
   7probes to recover an arbitrary edge-deficit vector.  That is too strong for
   8bulk 3D lattices, where there are generally more edge variables than vertex
   9probes.
  10
  11This module states and proves the mathematically valid version: recovery and
  12separation on an explicitly declared geometric deficit subspace.
  13-/
  14
  15namespace IndisputableMonolith
  16namespace Gravity
  17namespace RestrictedIncidenceRecovery
  18
  19open Geometry.ReggeTriangulation3D
  20open Geometry.ReggeHessian3D
  21open Geometry.Triangulation3DConsistency
  22open Geometry.ReggeActionConcrete
  23open Geometry.ReggeActionSmoothness
  24open Geometry.ReggeActionFirstVariation
  25open DiscreteVacuumEinstein
  26
  27noncomputable section
  28
  29abbrev DeficitSubspace (K : Triangulation3D) := (Fin K.nE → ℝ) → Prop
  30
  31def RestrictedIncidenceDeficitSeparating
  32    (K : Triangulation3D) (S : DeficitSubspace K) : Prop :=
  33  ∀ δ : Fin K.nE → ℝ,
  34    S δ →
  35    (∀ η : VertexPotential K,
  36      ∑ e : Fin K.nE, δ e * directionalLengthCoefficient K η e = 0) →
  37    δ = 0
  38
  39def RestrictedIncidenceDeficitRecovering
  40    (K : Triangulation3D) (S : DeficitSubspace K) : Prop :=
  41  ∃ recover : Fin K.nE → Fin K.nV → ℝ,
  42    ∀ δ : Fin K.nE → ℝ, S δ →
  43      ∀ e : Fin K.nE,
  44        δ e =
  45          ∑ i : Fin K.nV,
  46            recover e i *
  47              (∑ e' : Fin K.nE,
  48                δ e' * directionalLengthCoefficient K
  49                  (fun j : Fin K.nV => if j = i then (1 : ℝ) else 0) e')
  50
  51theorem restrictedIncidenceDeficitSeparating_of_recovering
  52    (K : Triangulation3D) (S : DeficitSubspace K)
  53    (hRecover : RestrictedIncidenceDeficitRecovering K S) :
  54    RestrictedIncidenceDeficitSeparating K S := by
  55  rcases hRecover with ⟨recover, hrecover⟩
  56  intro δ hS hpair
  57  funext e
  58  rw [hrecover δ hS e]
  59  apply Finset.sum_eq_zero
  60  intro i _
  61  rw [hpair (fun j : Fin K.nV => if j = i then (1 : ℝ) else 0)]
  62  ring
  63
  64/-- The subspace generated by a chosen recovery matrix: by definition, its
  65elements are exactly those recovered from vertex-basis probes by that matrix. -/
  66def RecoverableDeficitSubspace
  67    (K : Triangulation3D) (recover : Fin K.nE → Fin K.nV → ℝ) :
  68    DeficitSubspace K :=
  69  fun δ =>
  70    ∀ e : Fin K.nE,
  71      δ e =
  72        ∑ i : Fin K.nV,
  73          recover e i *
  74            (∑ e' : Fin K.nE,
  75              δ e' * directionalLengthCoefficient K
  76                (fun j : Fin K.nV => if j = i then (1 : ℝ) else 0) e')
  77
  78theorem restrictedRecovering_recoverableSubspace
  79    (K : Triangulation3D) (recover : Fin K.nE → Fin K.nV → ℝ) :
  80    RestrictedIncidenceDeficitRecovering K
  81      (RecoverableDeficitSubspace K recover) := by
  82  refine ⟨recover, ?_⟩
  83  intro δ hS e
  84  exact hS e
  85
  86theorem restrictedSeparating_recoverableSubspace
  87    (K : Triangulation3D) (recover : Fin K.nE → Fin K.nV → ℝ) :
  88    RestrictedIncidenceDeficitSeparating K
  89      (RecoverableDeficitSubspace K recover) :=
  90  restrictedIncidenceDeficitSeparating_of_recovering K
  91    (RecoverableDeficitSubspace K recover)
  92    (restrictedRecovering_recoverableSubspace K recover)
  93
  94/-- The geometric deficit subspace generated by conformal vertex-potential
  95edge-length directions.  This is the natural image of the incidence operator
  96`η ↦ directionalLengthCoefficient K η`. -/
  97def DirectionalLengthImageSubspace (K : Triangulation3D) : DeficitSubspace K :=
  98  fun δ => ∃ η : VertexPotential K,
  99    ∀ e : Fin K.nE, δ e = directionalLengthCoefficient K η e
 100
 101theorem directionalLengthImageSubspace_separating
 102    (K : Triangulation3D) :
 103    RestrictedIncidenceDeficitSeparating K
 104      (DirectionalLengthImageSubspace K) := by
 105  intro δ hS hpair
 106  rcases hS with ⟨η, hη⟩
 107  have hsum :
 108      (∑ e : Fin K.nE,
 109        directionalLengthCoefficient K η e *
 110          directionalLengthCoefficient K η e) = 0 := by
 111    simpa [hη] using hpair η
 112  have hzero_all :
 113      ∀ e ∈ (Finset.univ : Finset (Fin K.nE)),
 114        directionalLengthCoefficient K η e *
 115          directionalLengthCoefficient K η e = 0 := by
 116    have hnonneg :
 117        ∀ x ∈ (Finset.univ : Finset (Fin K.nE)),
 118          0 ≤ directionalLengthCoefficient K η x *
 119            directionalLengthCoefficient K η x := by
 120      intro x _
 121      exact mul_self_nonneg _
 122    exact (Finset.sum_eq_zero_iff_of_nonneg hnonneg).mp hsum
 123  funext e
 124  have hsq := hzero_all e (Finset.mem_univ e)
 125  have hcoeff : directionalLengthCoefficient K η e = 0 := by
 126    exact mul_self_eq_zero.mp hsq
 127  change δ e = 0
 128  rw [hη e, hcoeff]
 129
 130/-- Reverse vacuum implication restricted to a declared geometric deficit
 131subspace.  The actual deficit vector must be shown to belong to the subspace. -/
 132theorem zero_deficit_of_critical_of_restrictedVariationFormula
 133    (K : Triangulation3D) (hK : IncidenceConsistent K)
 134    (S : DeficitSubspace K)
 135    (hDeficitInS : S (fun e : Fin K.nE => deficitAngle K (zeroPotential K) e))
 136    (hFormula : ReggeFirstVariationFormula K hK)
 137    (hSep : RestrictedIncidenceDeficitSeparating K S)
 138    (hCrit : CriticalAtFlat K hK) :
 139    ZeroDeficitAtFlat K := by
 140  unfold CriticalAtFlat ReggeActionCriticalAtZero at hCrit
 141  unfold ZeroDeficitAtFlat
 142  have hdelta :
 143      (fun e : Fin K.nE => deficitAngle K (zeroPotential K) e) = 0 := by
 144    apply hSep
 145    · exact hDeficitInS
 146    · intro η
 147      have happly := congrArg (fun L : VertexPotential K →L[ℝ] ℝ => L η) hCrit
 148      have hzero :
 149          (fderiv ℝ (reggeAction K hK) (zeroPotential K)) η = 0 := by
 150        simpa using happly
 151      have hformula := hFormula.variation_formula η
 152      rw [hformula] at hzero
 153      simpa using hzero
 154  intro e
 155  exact congrFun hdelta e
 156
 157def discreteVacuumEinsteinInput_of_restrictedRecovery
 158    (K : Triangulation3D) (hK : IncidenceConsistent K)
 159    (h_flat : FlatConfiguration K hK)
 160    (hFirst : ReggeActionFirstVariationInput K hK h_flat)
 161    (S : DeficitSubspace K)
 162    (hDeficitInS : S (fun e : Fin K.nE => deficitAngle K (zeroPotential K) e))
 163    (hFormula : ReggeFirstVariationFormula K hK)
 164    (hSep : RestrictedIncidenceDeficitSeparating K S) :
 165    DiscreteVacuumEinsteinInput K hK h_flat where
 166  critical_iff_zero_deficit := by
 167    constructor
 168    · intro hCrit
 169      exact zero_deficit_of_critical_of_restrictedVariationFormula
 170        K hK S hDeficitInS hFormula hSep hCrit
 171    · intro _hZero
 172      exact hFirst.firstVariation_zero
 173
 174end
 175
 176end RestrictedIncidenceRecovery
 177end Gravity
 178end IndisputableMonolith
 179