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. -/
used by (6)
From the project-wide theorem graph. These declarations reference this one in their body.