FlowFS
plain-language theorem explainer
A finite-support integer flow on ordered pairs of events in a discrete event system with a fixed evolution relation. Downstream conservation-necessity lemmas treat this as the carrier of information transfer during recognition. The declaration is a one-field structure packing a finitely supported map $(E\times E)\to_0\mathbb{Z}$; there is no proof content.
Claim. Fix a discrete event system $E$ (countable carrier of events) and an evolution relation $ev$ on $E$ that is well-founded when reversed. A finite-support flow on $(E,ev)$ is a finitely supported map $\mathrm{value}:(E\times E)\to_0\mathbb{Z}$ assigning an integer to each ordered pair of events.
background
The module derives non-trivial conservation from the Meta-Principle (MP), replacing the old axiom that recognition requires distinguishability. The argument runs: 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 a non-trivial conserved flow.
A discrete event system is a countable type of events. Event evolution packages a binary relation evolves together with a well-foundedness witness on the reverse relation, so chains of evolution cannot descend forever. The flow object sits on top of that pair: it records integer weights on ordered event pairs, with only finitely many non-zero weights (Lean Finsupp).
Sibling notions built on this carrier include non-trivial flow (some edge has non-zero weight), distinguishable flow (identified with non-triviality), and the canonical one-edge flow that places weight $1$ on a single ordered pair.
proof idea
No proof: this is a structure definition. It introduces a single field, a finitely supported function from ordered pairs of events to integers, parameterized by a discrete event system and an evolution package. Downstream lemmas construct concrete inhabitants (for example the single-edge flow) and reason about the support and values of that field.
why it matters
This is the basic carrier type for the conservation-necessity chain. Parent results include distinction_implies_flow_structure (distinct evolving events force non-zero weight on that edge for flows that respect the structure), FlowOnEdge (canonical unit flow on one edge), IsRecognitionFlow / NonTrivialFlow / Distinguishable, and the summary theorems mp_forces_nontrivial_flow_exists, mp_forces_distinguishable_flow_exists, and conservation_necessity_proven.
Those theorems close the gap documented in the module: the old axiom claimed every flow is non-trivial; the correct MP consequence is existence of a non-trivial flow when the system itself is non-trivial. In RS terms the flow is information transfer during recognition events, so proving non-trivial flows exist is the formal step from MP to non-trivial conservation without an extra distinguishability axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.