edgeAreaGraph
plain-language theorem explainer
edgeAreaGraph packages the first-order area coefficients from WeakFieldReggeData into a WeightedLedgerGraph for use in Dirichlet-form calculations. Workers deriving the second-order Regge action as half the Laplacian action on vertex potentials cite this construction. It is realized by a direct record definition that supplies the weight matrix, the supplied non-negativity hypothesis, and symmetry inherited from edgeArea_symm.
Claim. Let $W$ be weak-field Regge data on $n$ vertices whose derived edge areas $A_{ij}$ satisfy $A_{ij}≥0$ for all $i,j$. The associated weighted ledger graph is the graph on $n$ vertices with weights $A_{ij}$, equipped with the non-negativity hypothesis and the symmetry $A_{ij}=A_{ji}$.
background
In the weak-field conformal reduction the Regge action expands to second order in the conformal vertex perturbation ξ. WeakFieldReggeData stores the linear responses dArea and dDeficit of hinge areas and deficits; the first-order areas Aij are the coefficients that multiply the squared differences (ξi−ξj)² after the algebraic reduction to Dirichlet form. The module states that non-negativity of these areas holds automatically on regular lattices and is therefore packaged as an explicit hypothesis rather than a derived theorem.
proof idea
Direct record construction. The weight field is set to edgeArea W, the non-negativity field receives the hypothesis hpos, and the symmetry field is filled by the lemma edgeArea_symm W.
why it matters
This definition supplies the weighted graph required by the downstream bridge theorem secondOrder_eq_half_laplacian_action, which equates the second-order Regge action to (1/2) times the Laplacian action on edgeAreaGraph W. It thereby completes the finite-dimensional algebraic step that converts the Regge bilinear form into a Dirichlet energy, consistent with the Recognition Science reduction of gravity to J-cost. The construction precedes the geometric task of computing the actual coefficients from Schläfli identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.