IsRecognitionFlow
plain-language theorem explainer
A finite-support flow is a recognition flow when it puts non-zero integer weight on some evolving pair of distinct events. Downstream lemmas use this predicate to replace the over-strong axiom that every flow is non-trivial. The body is a pure existential Prop on the flow's support and the evolution relation.
Claim. Let $E$ be a discrete event system, $\mathrm{ev}$ an evolution on $E$, and $f$ a finite-support integer flow on pairs of events. Then $f$ is a recognition flow if there exist events $e_1 \neq e_2$ such that $\mathrm{ev}$ relates $e_1$ to $e_2$ and $f(e_1,e_2) \neq 0$.
background
The module ConservationNecessity derives non-trivial conservation from the Meta-Principle (MP), so the old axiom recognition_requires_distinguishability is no longer needed. The chain is: MP makes recognition possible on non-empty types; recognition needs distinction; distinction in a discrete event system needs structural difference, i.e. non-zero flow; hence MP forces non-trivial conservation.
A discrete event system is a countable carrier of events. Event evolution packages a binary relation evolves with a well-foundedness witness on its reverse. A finite-support flow assigns an integer (finitely many non-zero) to each ordered pair of events. Non-triviality of a flow means some edge has non-zero value; distinguishability is the same idea packaged for the necessity theorems.
The original axiom claimed every flow is non-trivial. That is too strong. The corrected stance is: when recognition occurs, there exists a non-trivial flow (the recognition flow itself). This definition names that class of flows.
proof idea
Definitional predicate, not a proved theorem. The Prop is the existential: two events that are unequal, related by the evolution, and carry non-zero flow value. No tactics or upstream lemmas are applied; the body is the meaning of the name.
why it matters
This predicate is the weakened interface that lets the module discharge the old axiom without claiming every flow is non-trivial. Immediate consumers are recognition_flow_distinguishable (recognition flows are distinguishable) and recognition_flow_implies_distinguishable (under MP, a recognition flow is distinguishable), the latter documented as a "Weakened Axiom Replacement" provable with no placeholders.
In the module argument, it sits at step 3–4: distinction requires structure, and the structure that carries recognition is exactly a flow with non-zero weight on an evolving edge. That feeds the key theorem that MP implies distinguishability for recognition-carrying flows, closing the conservation-necessity gap recorded in the module docs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.