SchlaefliRowSum

formal source

 308
 309    This is the geometric content of "uniform `ξ ≡ c` produces no
 310    curvature change" combined with Schläfli's identity. -/
 311def SchlaefliRowSum {n : ℕ} (W : WeakFieldReggeData n) : Prop :=
 312  ∀ i : Fin n, ∑ j : Fin n, bilinearCoefficient W i j = 0
 313
 314/-- The second-order Regge action functional in the conformal mode.
 315    Plugging the conformal expansion of `ℓ²` into the linearized Regge
 316    action and collecting the order-`ξ²` terms gives this bilinear:
 317
 318        S^(2)[ξ] = (1/4) · Σ_{i,j} (ξ_i + ξ_j)² · M_{ij}
 319                = (1/4) · Σ_{i,j} (ξ_i² + 2 ξ_i ξ_j + ξ_j²) · M_{ij}.
 320
 321    The factor `1/4` comes from the `(ξ_i + ξ_j)/2` factors entering
 322    twice (once from `A_h^(1)`, once from `δ_h^(1)`).
 323
 324    With the Schläfli row-sum property, the `ξ_i² + ξ_j²` parts
 325    vanish on summation and the `2 ξ_i ξ_j` part rearranges via §2 into
 326    the Dirichlet form on differences. -/
 327def secondOrderReggeAction {n : ℕ} (W : WeakFieldReggeData n)
 328    (ε : LogPotential n) : ℝ :=
 329  (1 / 4) * ∑ i : Fin n, ∑ j : Fin n,
 330    bilinearCoefficient W i j * (ε i + ε j) ^ 2
 331
 332/-! ## §4. The reduction theorem
 333
 334The composition of §1 (conformal expansion), §2 (graph-Laplacian
 335decomposition), and §3 (Schläfli-anchored second-order form) yields:
 336
 337  `S^(2)[ξ] = (1/2) · Σ_⟨i,j⟩ A_{ij} · (ξ_i − ξ_j)²`
 338
 339with `A_{ij} = − bilinearCoefficient W i j` (the sign comes from
 340`Q = − D` in §2).
 341