edgeArea_symm
plain-language theorem explainer
The theorem establishes symmetry of the edge-area coefficients extracted from any WeakFieldReggeData structure under interchange of the two vertex indices. It is invoked when constructing WeightedLedgerGraph objects that carry the Dirichlet weights for the second-order Regge action. The proof is a one-line wrapper that unfolds the definition of edgeArea and rewrites via the symmetry already recorded for the underlying bilinear coefficient matrix.
Claim. Let $n$ be a natural number and let $W$ be a WeakFieldReggeData structure on $n$ vertices. For indices $i,j$ the edge-area coefficient satisfies $A_{ij}(W)=A_{ji}(W)$.
background
The module develops the algebraic core of the weak-field conformal reduction of the Regge action. WeakFieldReggeData packages the first-order linear responses dArea and dDeficit of hinge areas and deficits under conformal vertex perturbations, together with explicit symmetry hypotheses on those fields. The edgeArea function is the entrywise product of these responses that appears in the second-variation bilinear form after the conformal length expansion has been substituted. The surrounding module already proves that any symmetric zero-row-sum matrix induces the Dirichlet identity turning the bilinear form into a sum of squared differences.
proof idea
The proof is a one-line wrapper. It unfolds the definition of edgeArea and rewrites the resulting expression by the already-proved symmetry lemma bilinearCoefficient_symm.
why it matters
Symmetry of the coefficient matrix is required to equip it with the structure of a WeightedLedgerGraph, which supplies the Dirichlet weights for the graph-Laplacian decomposition of the second-order Regge action. The declaration therefore closes one of the three algebraic claims listed in the module documentation. It is used directly by the downstream definition edgeAreaGraph that packages the weights for the Recognition Science ledger formalism. The result is independent of the geometric origin of the coefficients and therefore applies to any lattice satisfying the flat-mode row-sum condition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.