RecognitionFlow
plain-language theorem explainer
Given a recognition event (two distinct events linked by evolution), the recognition flow is the finite-support integer flow that places unit mass on the ordered edge from source to target. It is the canonical witness that recognition induces a non-zero edge flow. Downstream lemmas cite it to prove that flow is non-trivial and that MP plus recognition events force existence of non-trivial conservation structure. The definition is a one-line constructor via the edge-supported flow builder.
Claim. For a discrete event system $E$ with evolution relation $\mathrm{ev}$, and a recognition event $r$ (distinct source $e_1$ and target $e_2$ with $\mathrm{ev}(e_1,e_2)$), the recognition flow is the finite-support flow $f:(E\times E)\to_0\mathbb{Z}$ equal to the unit flow supported on the ordered edge $(e_1,e_2)$.
background
This module derives non-trivial conservation from the Meta-Principle (MP), replacing an earlier axiom that recognition requires distinguishability. The chain is: MP makes recognition possible on non-empty types; recognition needs $X\neq Y$; in a discrete event system that distinction is carried by non-zero flow; hence MP forces non-trivial conservation structure.
A discrete event system is a countable carrier of events. Evolution packages a binary relation on events with a well-foundedness witness. A recognition event is a pair of distinct events linked by that evolution. A finite-support flow assigns an integer to each ordered pair of events, with only finitely many non-zero values.
The recognition flow is the module's canonical construction: when recognition occurs between $e_1$ and $e_2$, information is treated as flowing on that edge. Sibling structure FlowOnEdge builds the corresponding sparse flow; non-triviality means some edge carries a non-zero value.
proof idea
One-line definitional wrapper. Unpack the recognition event's source and target, then apply the edge-supported flow constructor FlowOnEdge to those two events. No tactics or lemmas: the body is exactly that constructor application, yielding a FlowFS value with unit support on the ordered pair $(source, target)$.
why it matters
This definition is the concrete witness that turns the conservation-necessity argument from an existence claim into an explicit object. The immediate parent lemma recognition_flow_nontrivial shows the constructed flow is non-trivial (some edge non-zero). The refined main theorem recognition_implies_nontrivial_flow_exists then extracts a recognition event from MP plus HasRecognitionEvents and exhibits this flow, replacing the old axiom in LedgerNecessity.
In framework terms it sits in the verification/necessity layer: MP forces recognition, recognition forces distinction, distinction is realized as non-zero ledger flow. That is the discrete precursor to conservation structure on the recognition ledger, upstream of J-cost and the forcing chain, but essential to the claim that conservation is not an extra postulate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.