distinction_implies_flow_structure
plain-language theorem explainer
In a discrete event system with a well-founded evolution relation, any finite-support integer flow that already takes a non-zero value on some edge is non-trivial. The lemma packages that definitional fact under hypotheses that two events are distinct and evolution-related. Anyone tracing the MP-to-conservation forcing chain in ConservationNecessity would cite it. The proof is a one-line term: NonTrivialFlow is definitionally the given existential.
Claim. Let $E$ be a discrete event system (countable event carrier), $\mathrm{evolves}$ a well-founded evolution relation on $E$, and $f$ a finite-support integer-valued flow on ordered event pairs. If there exist events $e_1 \neq e_2$ with $\mathrm{evolves}(e_1,e_2)$, and if $f$ is non-zero on at least one pair, then $f$ is a non-trivial flow (some edge carries non-zero value).
background
The module ConservationNecessity derives non-trivial conservation laws from the Meta-Principle (MP), so that recognition_requires_distinguishability need not be an axiom. The local argument is: MP makes recognition possible on non-empty types; recognition needs distinction; distinction in a discrete event graph needs structural difference, read as non-zero flow; hence MP forces non-trivial conservation.
A DiscreteEventSystem is a countable carrier of events. EventEvolution packages a binary evolution predicate with a well-foundedness witness (no infinite backward chains). A FlowFS is a finitely supported map from ordered event pairs to $\mathbb{Z}$. NonTrivialFlow f is defined exactly as $\exists p,, f.\mathrm{value}(p)\neq 0$.
Sibling notions in the same file (Distinguishable, RecognitionEvent, HasRecognitionEvents, FlowOnEdge) set up the larger forcing chain toward the main theorem that MP implies Distinguishable $f$ for every such flow.
proof idea
Pure definitional discharge. NonTrivialFlow f unfolds to $\exists p,, f.\mathrm{value}, p \neq 0$, which is literally the hypothesis hNontrivialSystem. The proof is the term exact hNontrivialSystem. The parameters $e_1$, $e_2$, the inequality $e_1\neq e_2$, and the evolution witness are unused; they only situate the lemma in the distinction narrative.
why it matters
Sits in Part 3 of the ConservationNecessity argument: "distinction requires structure," the step that turns event-graph distinction into non-zero flow. The module's target is recognition_requires_distinguishability_proven, which replaces the former axiom of the same name in LedgerNecessity and closes the chain MP $\to$ non-trivial conservation.
No downstream uses are recorded yet (used_by is empty), so this is presently a local stepping-stone rather than a widely applied lemma. In the broader Recognition Science forcing picture it supports the claim that conservation is not an extra physical postulate but a consequence of MP plus discrete event structure. It does not itself touch T5–T8, the RCL, or the $\varphi$-ladder; those enter only once conservation is in place for ledger and mass bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.