pith. machine review for the scientific record. sign in
structure definition def or abbrev high

WeakFieldReggeData

show as:
view Lean formalization →

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.

claimA 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 279structure WeakFieldReggeData (n : ℕ) where
 280  dArea : Fin n → Fin n → ℝ
 281  dDeficit : Fin n → Fin n → ℝ
 282  dArea_symm : ∀ i j, dArea i j = dArea j i
 283  dDeficit_symm : ∀ i j, dDeficit i j = dDeficit j i
 284
 285/-- The bilinear coefficient matrix induced by the linearization data:
 286    `M_{ij} = dArea_{ij} · dDeficit_{ij}` (the entry-wise product
 287    that appears in `S^(2) = Σ A^(1) δ^(1)` after the conformal
 288    expansion).
 289
 290    This is symmetric because both factors are symmetric. -/

used by (15)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.