secondOrderReggeAction_flat
plain-language theorem explainer
The second-order Regge action vanishes on the zero perturbation for any WeakFieldReggeData. Researchers deriving the linearized Regge action in the conformal sector cite this as the flat-background consistency condition. The proof is a direct algebraic reduction: unfold the action, apply ring to each bilinear term times zero, then simplify the double sum via sum_const_zero and mul_zero.
Claim. For any $n$ and any WeakFieldReggeData $W$ on $n$ vertices, with bilinear coefficients $M_{ij} = dA_{ij} dDeficit_{ij}$, the quadratic form $S^{(2)}[0] = 0$ where $S^{(2)}[ξ] = (1/4) ∑_{i,j} M_{ij} (ξ_i + ξ_j)^2$.
background
The module develops the algebraic core of the weak-field conformal reduction of the Regge action. Edge lengths follow the conformal ansatz ℓ_{ij} = ℓ_0 exp((ξ_i + ξ_j)/2). WeakFieldReggeData packages the first-order responses dArea and dDeficit (symmetric maps Fin n → Fin n → ℝ) that encode the linear change in hinge area and deficit under this perturbation. The bilinearCoefficient is the entrywise product M_{ij} = dArea_{ij} · dDeficit_{ij}. The secondOrderReggeAction is then defined as (1/4) ∑{i,j} M{ij} (ε_i + ε_j)^2 for a LogPotential ε. The module doc states that this yields the reduction S^{(2)} = (1/κ) Σ ½ (ξ_i − ξ_j)^2 A_{ij} once the graph-Laplacian identity is applied.
proof idea
Unfold secondOrderReggeAction. Establish the auxiliary fact that bilinearCoefficient W i j * (0 + 0)^2 = 0 for all i,j by the ring tactic. Then simp rewrites the double sum using Finset.sum_const_zero together with mul_zero from ArithmeticFromLogic, collapsing the expression to zero.
why it matters
This supplies the flat-vacuum case required by the downstream certification theorem weakFieldConformalReggeCert, which packages conformal exactness, the second-order Taylor expansion, the graph-Laplacian decomposition dirichlet_eq_neg_quadratic, and the full reduction. It confirms that the linearized Regge action is identically zero on flat backgrounds, closing the consistency check before geometric coefficients are supplied by Schläfli identities. The result sits inside the conformal-sector reduction that converts the Regge bilinear form into a Dirichlet form on vertex differences.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.