LedgerAlgObj
plain-language theorem explainer
LedgerAlgObj n defines objects in the LedgerAlg category as submodules of the n-node flow space in which every flow satisfies antisymmetry and node-wise conservation. Algebraists building the RecognitionCategory cite this when forming LayerSysPlusObj or the canonical ledger object. The declaration is a direct structure that bundles the carrier submodule with the two predicate assertions.
Claim. For each natural number $n$, a LedgerAlgObj consists of a submodule $C$ of the space of real $n$-by-$n$ matrices such that every matrix $f$ in $C$ obeys antisymmetry $f(u,v)=-f(v,u)$ for all nodes $u,v$ and conservation $sum_v f(u,v)=0$ for each node $u$.
background
The RecognitionCategory module assembles algebraic layers for recognition processes, including cost, phi-ring, ledger, and octave structures. FlowSpace n is the ambient space of all real matrices indexed by Fin n, serving as the pool of possible flows between n nodes. IsAntisymmetricFlow requires that the flow from u to v equals the negative of the flow from v to u; IsConservedFlow requires that the net outflow from every node is zero. These two predicates, together with the submodule carrier, select admissible ledger flows; the upstream admissible predicate from Thermodynamics is the trivial predicate True.
proof idea
This is a structure definition. The carrier field selects a submodule of FlowSpace n; the antisymm and conserved fields are universal quantifiers asserting that IsAntisymmetricFlow and IsConservedFlow hold on every element of that submodule.
why it matters
LedgerAlgObj supplies the objects of the LedgerAlg category and is used by canonicalLedgerAlgObj, LayerSysPlusObj, ledgerAlg_comp, ledgerAlg_id, and LedgerAlgHom. LayerSysPlusObj packages it with the cost layer, PhiRingObj, and OctaveAlgObj to satisfy bridge axioms (B1) and (B2). The construction supports the Recognition Composition Law by furnishing a category of conserved antisymmetric flows compatible with the phi-ladder and eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.