bilinearCoefficient_symm
plain-language theorem explainer
The bilinear coefficient matrix induced by first-order area and deficit responses in a weak-field Regge configuration is symmetric. Researchers reducing the Regge action to a discrete Dirichlet form cite this algebraic fact when assembling the quadratic form on conformal perturbations. The proof is a one-line wrapper that unfolds the definition as an entrywise product and applies the symmetry fields built into the WeakFieldReggeData structure.
Claim. Let $W$ be a weak-field Regge data structure on $n$ vertices whose first-order area responses $dA_{ij}$ and deficit responses $dδ_{ij}$ are each symmetric. Define the bilinear coefficients by $M_{ij} := dA_{ij} · dδ_{ij}$. Then $M_{ij} = M_{ji}$.
background
In the weak-field conformal reduction of the Regge action the second-order term arises from the product of first-order changes in hinge area and deficit angle. The structure WeakFieldReggeData packages these linear responses together with their symmetry properties. The bilinear coefficient is the entrywise product that enters the quadratic form $S^{(2)} = Σ M_{ij} ξ_i ξ_j$. This module establishes the algebraic scaffolding that converts such a symmetric zero-row-sum matrix into the Dirichlet energy on edge differences, as required for the conformal reduction.
proof idea
The proof is a one-line wrapper. It unfolds the definition of bilinearCoefficient as the product of dArea and dDeficit, then rewrites using the symmetry fields dArea_symm and dDeficit_symm supplied by the WeakFieldReggeData structure.
why it matters
This lemma supplies the symmetry needed to define the edge weights in the Dirichlet form that appears in the main reduction theorem. It is invoked by edgeArea_symm and by weak_field_conformal_reduction, which states that the second-order Regge action equals half the Dirichlet form on the conformal mode under the Schläfli row-sum hypothesis. The result closes one algebraic step in the program of reducing the Regge action to a discrete Laplacian on the conformal sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.