IsConservedFlow
plain-language theorem explainer
IsConservedFlow defines the node-wise conservation condition on flows in the finite node set FlowSpace n. Researchers constructing ledger algebras or admissible flow subspaces cite this definition when building the carrier of LedgerAlgObj. The definition is a direct predicate that sums the outgoing flows from each node u and requires the total to vanish.
Claim. A map $f : [n] × [n] → ℝ$ is a conserved flow if for every node $u$, $∑_{v=1}^n f(u,v) = 0$.
background
FlowSpace n is the ambient space of real-valued functions on an n-node set, serving as the domain for ledger flows in the RecognitionCategory module. This module assembles algebraic structures for recognition flows from imports including CostAlgebra, PhiRing, LedgerAlgebra and OctaveAlgebra. Upstream structures such as LedgerFactorization calibrate the J-cost function while PhiForcingDerived supplies the underlying J-cost minimization and SpectralEmergence encodes the discrete tier structure that later constrains admissible flows.
proof idea
This is a direct definition that encodes the conservation law as a universal quantification over nodes with a finite sum equaling zero. It relies on the standard Finset.univ sum from Mathlib and requires no further lemmas or tactics.
why it matters
This definition is used to construct admissibleFlows, the full subspace of antisymmetric conserved flows, and to define LedgerAlgObj, the objects in the ledger algebra category. It supplies the conservation half of admissible flows, supporting the Recognition Composition Law and the eight-tick octave dynamics that appear in downstream ledger constructions. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.