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

WeightedLedgerGraph

show as:
view Lean formalization →

WeightedLedgerGraph equips a finite set of n vertices with a symmetric nonnegative real weight matrix that models the discrete ledger graph. Researchers deriving the Einstein field equations from J-cost stationarity cite this as the discrete object on which the Laplacian action is defined. The declaration is a direct structure definition that introduces the weight function together with its two axioms.

claimA weighted simplicial graph on $n$ vertices is a function $w : [n] × [n] → ℝ$ such that $w(i,j) ≥ 0$ and $w(i,j) = w(j,i)$ for all indices $i,j$.

background

The module establishes the continuum bridge by showing that J-cost stationarity on the simplicial ledger yields the Einstein field equations in the continuum limit. J-cost is the quadratic cost functional induced by multiplicative recognizers on positive ratios and by recognition events on states. The upstream cost definitions supply the J-cost that is evaluated on the weight matrix of this graph.

proof idea

The declaration is a direct structure definition that introduces the weight matrix together with its nonnegativity and symmetry axioms.

why it matters in Recognition Science

This structure is the foundational object in the JCostToEFE derivation chain and appears in ContinuumBridgeCert. It enables the identification of the discrete Laplacian action with the linearized Regge action, closing the gap between the discrete RS ledger and the continuum Einstein equations with coupling constant κ = 8φ⁵.

scope and limits

formal statement (Lean)

  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. -/

used by (40)

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

… and 10 more

depends on (2)

Lean names referenced from this declaration's body.