WeakFieldReggeData

formal source

 276
 277    The data is symmetric in `i, j` and lives on a finite vertex set
 278    `Fin n`. -/
 279structure WeakFieldReggeData (n : ℕ) where
 280  dArea : Fin n → Fin n → ℝ
 281  dDeficit : Fin n → Fin n → ℝ
 282  dArea_symm : ∀ i j, dArea i j = dArea j i
 283  dDeficit_symm : ∀ i j, dDeficit i j = dDeficit j i
 284
 285/-- The bilinear coefficient matrix induced by the linearization data:
 286    `M_{ij} = dArea_{ij} · dDeficit_{ij}` (the entry-wise product
 287    that appears in `S^(2) = Σ A^(1) δ^(1)` after the conformal
 288    expansion).
 289
 290    This is symmetric because both factors are symmetric. -/
 291def bilinearCoefficient {n : ℕ} (W : WeakFieldReggeData n)
 292    (i j : Fin n) : ℝ :=
 293  W.dArea i j * W.dDeficit i j
 294
 295theorem bilinearCoefficient_symm {n : ℕ} (W : WeakFieldReggeData n)
 296    (i j : Fin n) :
 297    bilinearCoefficient W i j = bilinearCoefficient W j i := by
 298  unfold bilinearCoefficient
 299  rw [W.dArea_symm i j, W.dDeficit_symm i j]
 300
 301/-- The *Schläfli-derived row-sum vanishing* property. On a flat
 302    background, the deficit-angle linearization satisfies Schläfli's
 303    identity, which forces the bilinear-coefficient matrix to have
 304    zero row sums when contracted with the conformal mode.
 305
 306    Concretely: for each vertex `i`,
 307    `Σ_j dArea_{ij} · dDeficit_{ij} = 0`.
 308
 309    This is the geometric content of "uniform `ξ ≡ c` produces no