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

edgeAreaGraph

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 527def edgeAreaGraph {n : ℕ} (W : WeakFieldReggeData n)
 528    (hpos : ∀ i j, 0 ≤ edgeArea W i j) : WeightedLedgerGraph n :=

proof body

Definition body.

 529  { weight := edgeArea W
 530  , weight_nonneg := hpos
 531  , weight_symm := edgeArea_symm W }
 532
 533/-- **BRIDGE TO `laplacian_action`.**
 534    The second-order Regge action equals `(1/2) · laplacian_action`
 535    on the `edgeAreaGraph`. Concretely:
 536
 537        S^(2)[ξ] = (1/2) · laplacian_action (edgeAreaGraph W) ε.
 538
 539    Combined with `EdgeLengthFromPsi.field_curvature_identity_under_linearization`,
 540    this is the explicit second-order content of the bridge identity:
 541    "J-cost Dirichlet energy = (1/κ) · Regge sum, at second order in ξ". -/

used by (1)

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

depends on (24)

Lean names referenced from this declaration's body.