admissibleFlows
plain-language theorem explainer
admissibleFlows n defines the submodule of all real flows on n nodes that are antisymmetric under index swap and conserve net flow at every node. Ledger algebra constructions cite it as the carrier for canonical objects in the RecognitionCategory module. The definition forms the carrier set by conjunction of the two predicates and verifies submodule axioms by direct expansion and ring arithmetic.
Claim. Let $F_n$ be the vector space of all real-valued assignments on pairs of nodes from a finite set of cardinality $n$. Then admissibleFlows $n$ is the submodule consisting of those $f$ such that $f(u,v)=-f(v,u)$ for all indices and the sum of $f(u,v)$ over the second index vanishes for every fixed first index $u$.
background
FlowSpace n is the ambient real vector space of all functions from pairs of nodes in a finite set of size n to the reals. IsAntisymmetricFlow requires that the assignment reverses sign under index interchange. IsConservedFlow requires that the net outflow from each node is identically zero. These two predicates are the only constraints appearing in the carrier set.
proof idea
The definition constructs a Submodule by direct set comprehension on the conjunction of the two predicates, then supplies the three required membership proofs. zero_mem' follows by simplification. add_mem' applies the antisymmetry and conservation assumptions componentwise and closes under addition via the ring tactic. smul_mem' distributes the scalar through the sum and reuses the conservation hypothesis.
why it matters
canonicalLedgerAlgObj takes admissibleFlows n as its carrier, thereby making the admissible space the canonical ledger object. The definition therefore supplies the algebraic foundation for all subsequent LedgerAlgObj constructions inside RecognitionCategory. It encodes the minimal flow constraints compatible with the Recognition Composition Law at the level of linear algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.