WeightedLedgerGraph
plain-language theorem explainer
A finite undirected weighted graph on n vertices: a symmetric nonnegative real weight on every ordered pair of sites. It is the carrier for the discrete Dirichlet (quadratic J-cost) action in the simplicial ledger. Anyone building continuum-bridge, pair-kernel, or onsite-exclusion arguments cites it as the graph type. As a structure definition there is no proof body; the content is the three fields.
Claim. For each $n \in \mathbb{N}$, a weighted ledger graph is a map $w : \{0,\ldots,n-1\}^2 \to \mathbb{R}$ such that $w(i,j) \ge 0$ and $w(i,j) = w(j,i)$ for all sites $i,j$.
background
The module isolates the finite weighted-graph Dirichlet action used by the simplicial ledger continuum bridge. Imports are Mathlib-only; the action, Laplacian, and pairing identities carry no physical normalization and no continuum endpoint assumptions.
A weighted ledger graph packages the coupling data of that discrete action: a real weight on every ordered pair of the $n$ sites, forced nonnegative and symmetric. Downstream the discrete Laplacian action on such a graph is identified with the quadratic J-cost (the recognition cost $J(x) = (x+x^{-1})/2-1$ in the forcing chain). Related cost primitives elsewhere (observer events, multiplicative recognizers, rung-coarsened multisets) all ultimately feed the same J-shaped ledger cost; this structure is the graph-level place where those weights live.
The continuum-bridge module carries an identical structure declaration; the present copy is the Mathlib-local foundation used by locality and onsite-exclusion arguments.
proof idea
Pure structure definition: three fields and no proof obligations beyond the Prop fields themselves. weight is an arbitrary real bilinear table on Fin n; weight_nonneg and weight_symm are the two axioms (nonnegativity and symmetry). Instantiation elsewhere discharges those axioms by split/norm_num or by construction (e.g. indicator of a symmetric distance band).
why it matters
This is the graph type for the finite Dirichlet action that the simplicial ledger continuum bridge and the pair-kernel stack both consume. Downstream, bandWeight builds the nearest-neighbor admissible instance; FiniteRange states the L0 locality hypothesis on its weights (coupling vanishes beyond fixed cell distance; provenance still open, expected via atomic-tick adjacency); and meanFieldLedgerCost_not_finiteRange uses it to reject all-to-all mean-field screening as non-local.
On the onsite-exclusion side, exactJCostAsGeneralLedgerCost re-expresses the exact J-cost action as a general ledger cost with zero onsite term and link $u \mapsto \cosh u - 1$, taking a weighted ledger graph as the coupling carrier. That ties the structure to T5 J-uniqueness and the Recognition Composition Law: the quadratic graph action is the discrete avatar of the unique J-cost. Without a shared nonnegative symmetric weight type, the locality teeth and the onsite-zero consistency checks cannot even be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.