WeightedLedgerGraph
plain-language theorem explainer
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.
Claim. A 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
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φ⁵.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.