LedgerAlgObj
plain-language theorem explainer
A LedgerAlgObj for n nodes is a submodule of real-valued flows on those nodes whose elements are antisymmetric and node-conserved. Algebraists constructing the recognition category cite this structure when assembling the ledger layer of a multi-layer system. The declaration is introduced directly as a structure with a carrier submodule and two forall predicates.
Claim. For a natural number $n$, a LedgerAlgObj consists of a submodule $C$ of the space of real functions on pairs of nodes such that every flow $f$ in $C$ satisfies $f(u,v)=-f(v,u)$ for all nodes $u,v$ and the sum over $v$ of $f(u,v)$ equals zero for each node $u$.
background
FlowSpace n is the vector space of all real-valued functions from pairs of n nodes to reals. IsAntisymmetricFlow requires that the flow from u to v equals the negative of the flow from v to u. IsConservedFlow requires that the sum of flows out of each node is zero. The module RecognitionCategory assembles algebraic objects for recognition by combining cost algebras, phi rings, ledgers, and octave algebras. The upstream admissible predicate from information thermodynamics is the trivial true predicate.
proof idea
This is a structure definition with no proof body. It directly introduces the type with three fields: a carrier submodule of FlowSpace n together with the two universal conditions on antisymmetry and conservation.
why it matters
LedgerAlgObj supplies the objects of the LedgerAlg category. It is instantiated in canonicalLedgerAlgObj as the full admissible flow space and appears inside LayerSysPlusObj, which packages the cost layer, PhiRing, LedgerAlg, and OctaveAlg layers together with the bridge axioms (B1) and (B2) from §4.1. The structure therefore provides the algebraic substrate for conserved antisymmetric flows used in downstream category constructions and layer-system definitions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.