FlowSpace
plain-language theorem explainer
FlowSpace n is the real vector space of all assignments to directed pairs among n nodes, serving as the carrier for ledger flows in the Recognition algebra. Algebraists constructing categories of conserved flows cite it as the ambient type before imposing antisymmetry and node-wise conservation. The declaration is a direct type abbreviation with no lemmas or computational steps.
Claim. For a natural number $n$, the flow space on $n$ nodes is the real vector space of all functions from ordered pairs of nodes to the reals, written as the set of maps $f : [n] × [n] → ℝ$.
background
In the RecognitionCategory module the ambient space for flows is introduced before the antisymmetry and conservation predicates. IsAntisymmetricFlow requires that every assignment satisfies $f(u,v) = -f(v,u)$ for all nodes $u,v$. IsConservedFlow requires that the outgoing sum at each node vanishes: for every $u$, the sum over $v$ of $f(u,v)$ equals zero. These two predicates together define the carrier of admissibleFlows, whose elements are then used to build LedgerAlgObj as submodules of the flow space.
proof idea
The declaration is a one-line type abbreviation that directly expands to the function type Fin n → Fin n → ℝ. No upstream lemmas are invoked and no tactics are applied.
why it matters
FlowSpace supplies the underlying type for the LedgerAlg category whose objects are subspaces of admissible flows. It is referenced by admissibleFlows, IsAntisymmetricFlow, IsConservedFlow, and LedgerAlgObj, thereby anchoring the algebraic presentation of conserved flows that later connect to the Recognition Composition Law and the eight-tick octave structure. The definition closes the scaffolding step that lets the category be equipped with linear morphisms between flow spaces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.