mp_forces_distinguishable_flow_exists
plain-language theorem explainer
Under the Meta-Principle, any discrete event system with a nontrivial evolution admits a distinguishable finite-support flow. Conservation-necessity arguments cite this as the existence form of the old distinguishability axiom. The proof is a one-line wrapper around nontrivial-flow existence, using that distinguishability is defined as flow nontriviality.
Claim. Let $E$ be a discrete event system with evolution relation $\mathrm{evolves}$, and assume the Meta-Principle. If there exist distinct events $e_1 \neq e_2$ with $e_1$ evolving to $e_2$, then there exists a finite-support integer-valued flow $f$ on pairs of events such that $f$ is distinguishable (i.e., nontrivial: some edge carries nonzero value).
background
This module derives non-trivial conservation from the Meta-Principle (MP), so the older axiom recognition_requires_distinguishability is no longer free-standing. A discrete event system is a countable carrier of events. An evolution packages a binary relation evolves with a well-foundedness witness. A finite-support flow assigns integers to event pairs with only finitely many nonzero values.
Distinguishability of a flow is defined exactly as nontriviality: some edge has nonzero value. The module argument is: MP makes recognition possible on nonempty types; recognition needs distinct events; distinction in a discrete system needs structural difference, i.e. nonzero flow. The present theorem is the existence form of that last step.
Upstream, the sibling existence result already produces a nontrivial finite-support flow from MP plus a nontrivial evolution pair. This declaration only renames that conclusion through the distinguishability abbreviation.
proof idea
One-line wrapper. Apply mp_forces_nontrivial_flow_exists to the same data $(E, \mathrm{ev}, \mathrm{MP},$ nontrivial evolution pair$)$ to obtain a flow $f$ together with a nontriviality witness. Return that same pair: by definition, Distinguishable f is NonTrivialFlow f, so the witness transfers unchanged.
why it matters
This is the summary existence theorem that replaces the old universal axiom "every flow is distinguishable" with the correct claim "a distinguishable flow exists." The physical reading in the module is that flow is information transfer during recognition; MP guarantees recognition can occur, hence information can flow, hence nontrivial flows must exist.
It feeds conservation_necessity_status, which records the conservation-necessity chain as complete and lists this result (via the nontrivial-flow sibling) among the proven steps. That status note stresses the key correction: the original axiom asked whether every flow is nontrivial; the right question is existence of a nontrivial flow. Closing this gap removes an axiom from the LedgerNecessity layer and tightens the MP → non-trivial conservation forcing path in the Verification domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.