cubicDeficitFunctional

formal source

 166      simp
 167
 168/-- The cubic deficit functional. -/
 169def cubicDeficitFunctional (n : ℕ) : DeficitAngleFunctional n :=
 170  { deficit := cubicDeficit
 171  , area := cubicArea
 172  , area_pos := cubicArea_nonneg
 173  }
 174
 175/-! ## §4. Hinge product at a singleton hinge -/
 176
 177/-- Area × deficit at a singleton hinge for pair `(i, j)`, on the
 178    conformal edge-length field. -/
 179theorem singletonHinge_product {n : ℕ} (a : ℝ) (ha : 0 < a)
 180    (ε : LogPotential n) (i j : Fin n) (w : ℝ) (hw : 0 ≤ w) :
 181    cubicArea (conformal_edge_length_field a ha ε) (singletonHinge i j w hw) *
 182      cubicDeficit (conformal_edge_length_field a ha ε) (singletonHinge i j w hw)
 183    = (jcost_to_regge_factor / 2) * w * (ε i - ε j) ^ 2 := by
 184  rw [cubicArea_singleton, cubicDeficit_singleton,
 185      recoverEps_conformal a ha ε i, recoverEps_conformal a ha ε j]
 186  ring
 187
 188/-! ## §5. The cubic hinge list via `Finset.univ.toList`
 189
 190Enumerate one hinge per ordered pair `(i, j) ∈ Fin n × Fin n`. Pairs with
 191`i = j` contribute 0 because `(ε_i − ε_i)² = 0`. -/
 192
 193/-- The hinge list: one singleton hinge per ordered pair. -/
 194def cubicHinges {n : ℕ} (G : WeightedLedgerGraph n) : List (HingeDatum n) :=
 195  (Finset.univ : Finset (Fin n × Fin n)).toList.map (fun ij =>
 196    singletonHinge ij.1 ij.2 (G.weight ij.1 ij.2) (G.weight_nonneg ij.1 ij.2))
 197
 198/-! ## §6. Summing the hinge list — reduction to a `Finset.sum` -/
 199