WeakFieldReggeData
plain-language theorem explainer
WeakFieldReggeData records the pair of symmetric matrices that give the first-order responses of hinge areas and deficit angles to conformal vertex perturbations on a finite vertex set. Gravity researchers linearizing the Regge action around flat backgrounds cite this structure when packaging the geometric coefficients before the Dirichlet decomposition step. The definition is a direct record of the two matrices together with their symmetry axioms.
Claim. A structure on a finite vertex set $n$ consisting of two symmetric real matrices $dA_{ij}$ and $dδ_{ij}$ on $Fin(n)×Fin(n)$, where $dA_{ij}$ is the coefficient of $(ξ_i + ξ_j)/2$ in the first-order area change of the hinge on edge $⟨i,j⟩$ and $dδ_{ij}$ is the corresponding coefficient for the deficit angle.
background
The module develops the algebraic core of the weak-field conformal reduction of the Regge action. The starting point is the Regge action $S = (1/κ) Σ_h A_h δ_h$. Under the conformal ansatz ℓ_{ij} = ℓ_0 exp((ξ_i + ξ_j)/2) the action expands to second order in the vertex potentials ξ, and the reduction isolates the quadratic term that becomes a Dirichlet form on edge differences (ξ_i − ξ_j)².
proof idea
This is a structure definition that directly encodes the two symmetric matrices dArea and dDeficit together with their symmetry properties. No lemmas or tactics are applied; the definition serves as the packaging layer for the linearization data that downstream constructions such as bilinearCoefficient and edgeArea consume.
why it matters
The structure supplies the geometric hypothesis package required by the algebraic claims of the module and feeds directly into bilinearCoefficient, edgeArea, and the Dirichlet-form theorems. It realizes the third layer of the weak-field reduction while leaving explicit computation of the coefficients from Schläfli or Cayley-Menger data as an open geometric task. The construction closes the algebraic core before the identity Σ M_{ij} ξ_i ξ_j = −½ Σ M_{ij} (ξ_i − ξ_j)² is applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.