dirichletForm_edgeArea
The theorem establishes that the Dirichlet form on the edge-area matrix from weak-field Regge data equals the negation of the Dirichlet form on the bilinear coefficient matrix. Discrete gravity researchers reducing the second-order Regge action to a graph Laplacian on conformal modes would cite this identity. The proof is a one-line wrapper that invokes the general negation property of the Dirichlet form once the definitional equality edgeArea W = - bilinearCoefficient W is noted.
claimLet $W$ be weak-field Regge data on $n$ vertices with first-order responses $dArea$ and $dDeficit$, and let $M$ be the bilinear coefficient matrix with entries $M_{ij} = dArea_{ij} dDeficit_{ij}$. Let $A$ be the edge-area matrix defined by $A = -M$. For any log-potential $ε$, the Dirichlet form satisfies $D(A, ε) = -D(M, ε)$.
background
The module develops the algebraic core of the weak-field conformal reduction of the Regge action. Under the ansatz $ℓ_{ij} = ℓ_0 exp((ξ_i + ξ_j)/2)$, the second-order term in the action becomes a bilinear form on the conformal mode $ε$. WeakFieldReggeData packages the linear responses: its fields $dArea$ and $dDeficit$ record the first-order changes in hinge area and deficit angle. Their entrywise product defines the bilinearCoefficient matrix $M$, while edgeArea is defined as its negation to match the sign convention in the action expansion.
proof idea
The proof is a one-line wrapper. It applies the general lemma dirichletForm_neg to the bilinearCoefficient matrix and the potential $ε$. The accompanying comment records that edgeArea W is definitionally equal to the pointwise negation of bilinearCoefficient W, so the desired equality follows at once.
why it matters in Recognition Science
This identity is invoked inside the main theorem weak_field_conformal_reduction to finish the algebraic reduction of the second-order Regge action to half the Dirichlet energy on the edge-area matrix. It supplies the sign-management step in the graph-Laplacian decomposition of §2. Within the Recognition framework it supports the conformal sector of the weak-field limit, consistent with the eight-tick octave once the geometric coefficients satisfying the Schläfli row-sum condition are supplied. The result is fully proved with no remaining scaffolding.
scope and limits
- Does not compute explicit values of dArea or dDeficit from Cayley-Menger formulas.
- Does not verify or enforce the Schläfli row-sum hypothesis on W.
- Applies only to the conformal perturbation mode ε.
- Assumes symmetry and zero row sums as encoded in WeakFieldReggeData.
formal statement (Lean)
378theorem dirichletForm_edgeArea
379 {n : ℕ} (W : WeakFieldReggeData n) (ε : LogPotential n) :
380 dirichletForm (edgeArea W) ε
381 = - dirichletForm (bilinearCoefficient W) ε := by
proof body
Tactic-mode proof.
382 have h := dirichletForm_neg (bilinearCoefficient W) ε
383 -- `(fun i j => - bilinearCoefficient W i j)` is definitionally `edgeArea W`.
384 exact h
385
386/-- **WEAK-FIELD CONFORMAL REDUCTION (the main theorem).**
387
388 Under the Schläfli row-sum hypothesis (§3) on the linearization
389 data `W`, the second-order Regge action equals the discrete
390 Dirichlet energy on the conformal mode `ε`, with edge weights
391 `A_{ij} = − dArea_{ij} · dDeficit_{ij}`:
392
393 secondOrderReggeAction W ε
394 = (1/2) · Σ_{i,j} ½ · (ε i − ε j)² · A_{ij}
395 = ½ · dirichletForm A ε.
396
397 Multiplying through by `1/κ` recovers Jon's equation (d):
398
399 S^(2)/κ = (1/κ) · Σ_⟨i,j⟩ ½ · (ξ_i − ξ_j)² · A_{ij}.
400
401 Proof:
402 1. Expand `(ξ_i + ξ_j)² = ξ_i² + 2 ξ_i ξ_j + ξ_j²`.
403 2. The `ξ_i²` and `ξ_j²` pieces collapse via Schläfli row-sum.
404 3. The `2 ξ_i ξ_j` piece is `quadraticForm M ε = − dirichletForm M ε`
405 by `dirichlet_eq_neg_quadratic` (§2).
406 4. `dirichletForm (edgeArea W) ε = − dirichletForm M ε`
407 by `dirichletForm_edgeArea`.
408 Combining: LHS = `(1/4)·(0 + 2·(−D) + 0) = −D/2 = (1/2)·(−D)
409 = (1/2) · dirichletForm (edgeArea W) ε = RHS`. -/