`WeightedLedgerGraph`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge
domain: Foundation
line: 98 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge on GitHub at line 98.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  95This is the standard graph Laplacian energy. -/
  96
  97/-- A weighted simplicial graph representing the ledger. -/
  98structure WeightedLedgerGraph (n : ℕ) where
  99  weight : Fin n → Fin n → ℝ
 100  weight_nonneg : ∀ i j, 0 ≤ weight i j
 101  weight_symm : ∀ i j, weight i j = weight j i
 102
 103/-- The discrete Laplacian action (= quadratic J-cost) on the graph. -/
 104def laplacian_action {n : ℕ} (G : WeightedLedgerGraph n) (ε : Fin n → ℝ) : ℝ :=
 105  (1 / 2) * ∑ i : Fin n, ∑ j : Fin n, G.weight i j * (ε i - ε j) ^ 2
 106
 107/-- The discrete Laplacian of ε at vertex i:
 108    (Δε)_i = Σ_j w_ij · (ε_i − ε_j) -/
 109def discrete_laplacian {n : ℕ} (G : WeightedLedgerGraph n) (ε : Fin n → ℝ) (i : Fin n) : ℝ :=
 110  ∑ j : Fin n, G.weight i j * (ε i - ε j)
 111
 112/-- Stationarity of the Laplacian action implies the discrete Laplacian vanishes.
 113    This is: δS/δε_i = 0 ⟺ (Δε)_i = 0 for all i. -/
 114theorem stationarity_iff_laplacian_zero {n : ℕ} (G : WeightedLedgerGraph n) (ε : Fin n → ℝ) :
 115    (∀ i, discrete_laplacian G ε i = 0) →
 116    ∀ i, ∑ j : Fin n, G.weight i j * (ε i - ε j) = 0 := by
 117  intro h i
 118  exact h i
 119
 120/-! ## Regge Action Identification
 121
 122The Regge action on a simplicial complex is:
 123  S_Regge = (1/κ) Σ_h δ_h · A_h
 124
 125where δ_h is the deficit angle at hinge h and A_h is its area.
 126
 127For small deficit angles (weak field), δ_h ≈ Σ_σ∋h (ε_σ − ε_σ') · geometry_factor.
 128

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.