Distinguishable
plain-language theorem explainer
In a discrete event system with evolution and finite-support flow, a flow is called distinguishable exactly when it is non-trivial: some ordered event pair carries a non-zero integer weight. The definition packages that predicate for the conservation-necessity argument from the Meta-Principle. Citation targets are proofs that MP forces meaningful recognition and non-trivial conserved flow. The body is a one-line abbreviation of non-triviality.
Claim. Fix a discrete event system $E$ (countable event carrier), an evolution relation on $E$ with a well-foundedness witness, and a finite-support integer flow $f$ on ordered event pairs. The flow $f$ is distinguishable when it is non-trivial: there exists at least one ordered pair of events on which $f$ takes a non-zero value.
background
The module derives non-trivial conservation from the Meta-Principle (MP), so that recognition-requires-distinguishability need not be axiomatic. The local chain is: MP makes recognition possible on non-empty types; recognition needs distinction; in a discrete event system distinction needs structural difference, i.e. non-zero flow; hence MP forces non-trivial conservation.
A discrete event system is a countable type of events. Event evolution packages a binary evolves-relation together with well-foundedness of the reverse relation. A finite-support flow assigns an integer to each ordered event pair, with only finitely many non-zeros. Non-trivial flow means some edge has non-zero value. Distinguishability of a flow is exactly that non-triviality predicate, phrased so later theorems can say "the flow structure differentiates states."
proof idea
Definitional abbreviation, not a proof. The predicate on a finite-support flow $f$ is definitionally equal to non-triviality of $f$: some support edge carries a non-zero integer. No lemmas are applied; downstream theorems unfold this name or treat it as the Prop standing for non-zero flow.
why it matters
This is the local language for "distinction" in the conservation-necessity forcing chain. The module key theorem recognition_requires_distinguishability_proven states that MP implies every such flow is distinguishable, replacing the former axiom in LedgerNecessity. Downstream in the same module, mp_forces_distinguishable_flow_exists and related recognition-event lemmas use the predicate to connect MP to non-trivial conserved structure.
In the broader Recognition framework this sits under verification of necessity: conservation is not postulated but forced once recognition is possible and discrete events carry finite-support flow. Homonymous distinguishability predicates in RecogGeom (recognizer maps sending configs to different events) are separate; composition monotonicity theorems there use that other notion. The present definition is the flow-side hinge for eliminating the distinguishability axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.