FlowOnEdge
plain-language theorem explainer
Unit flow on a single directed edge between two events of a discrete event system: mass 1 on that ordered pair, zero elsewhere. Cited wherever conservation necessity needs an explicit non-trivial flow witness from the Meta-Principle. Construction is the finite-support singleton on the edge pair.
Claim. Given a discrete event system $E$ (countable event carrier), an evolution relation on its events, and two events $e_1,e_2$, the flow on the edge $(e_1,e_2)$ is the finite-support map $(E.\mathrm{Event}\times E.\mathrm{Event})\to_0\mathbb{Z}$ with value $1$ at $(e_1,e_2)$ and $0$ on every other ordered pair.
background
The Conservation Necessity module derives non-trivial conservation from the Meta-Principle (MP), replacing the older axiom that recognition requires distinguishability. The chain is: MP makes recognition possible on non-empty types; recognition needs distinction; distinction in a discrete event system needs non-zero structural flow; hence MP forces non-trivial conservation.
A discrete event system is a countable carrier of events. Event evolution packages a binary evolves-relation with a well-foundedness witness. A finite-support flow is an integer-valued finitely supported function on ordered event pairs: the ledger of how much "information" moves along each directed edge.
This definition supplies the elementary one-edge ledger used as the canonical witness later in the module.
proof idea
Pure constructor, not a proof. Builds a FlowFS record whose value field is Finsupp.single (e₁, e₂) 1: the unique finite-support function equal to 1 at the ordered pair and 0 elsewhere. No lemmas are applied.
why it matters
This is the atomic non-trivial flow used throughout the conservation-necessity argument. Downstream, flow_on_edge_nontrivial shows the singleton has non-zero mass on its edge; mp_forces_nontrivial_flow_exists uses it as the existential witness that any system with two distinct evolving events admits a non-trivial flow under MP; and RecognitionFlow is defined as this construction on a recognition event's source and target.
In framework terms it closes the gap between "recognition can occur" and "a ledger edge carries non-zero flow," which is the structural content of conservation forced by MP rather than postulated. It does not itself invoke T5–T8 or the RCL; it sits at the verification layer that makes those later conservation claims axiom-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.