IsAntisymmetricFlow
plain-language theorem explainer
IsAntisymmetricFlow defines the predicate that a flow f on n nodes satisfies f(u,v) = -f(v,u) for all node pairs. Constructions of admissible flow subspaces and ledger algebra objects cite it when building the RecognitionCategory structures. The definition is a direct one-line predicate on the FlowSpace type with no auxiliary lemmas.
Claim. A map $f : (Fin n) × (Fin n) → ℝ$ is antisymmetric when $f(u,v) = -f(v,u)$ for all $u,v ∈ Fin n$.
background
FlowSpace n is the ambient type of all real-valued maps on pairs drawn from a finite node set of size n, i.e., the space of n-by-n real matrices. The RecognitionCategory module assembles category objects for recognition algebras; its ledger-algebra fragment uses antisymmetry together with a conservation predicate to carve out admissible subspaces. The predicate is stated directly on the FlowSpace abbrev supplied in the same module.
proof idea
This is a definition whose body is the universal statement ∀ u v, f u v = -f v u. No lemmas or tactics are invoked; the declaration simply names the predicate.
why it matters
The predicate supplies the antisymmetry half of the carrier in admissibleFlows and the antisymm field in LedgerAlgObj. It therefore participates in the algebraic layer that models ledger flows inside the Recognition framework, ensuring skew-symmetry before conservation and submodule structure are imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.