recognition_flow_implies_distinguishable
plain-language theorem explainer
A recognition flow on a discrete event system is automatically distinguishable: non-zero support on a genuine evolution edge forces non-trivial flow. Anyone closing the conservation-necessity argument from the Meta-Principle cites this weakened replacement for the old blanket axiom. The proof is a one-line application of the recognition-flow distinguishability lemma; the Meta-Principle hypothesis is carried only for interface uniformity.
Claim. Let $E$ be a discrete event system with evolution relation $\mathrm{ev}$, and let $f$ be a finite-support integer flow on ordered pairs of events of $E$. Assume the Meta-Principle, and assume $f$ is a recognition flow: there exist distinct events $e_1 \neq e_2$ with $\mathrm{ev}(e_1,e_2)$ and $f(e_1,e_2)\neq 0$. Then $f$ is distinguishable, i.e. $f$ is a non-trivial flow.
background
This module derives non-trivial conservation from the Meta-Principle (MP), eliminating the need to take "recognition requires distinguishability" as an axiom. The local setting is discrete event systems: a countable carrier of events together with a well-founded evolution relation. A finite-support flow assigns an integer to each ordered pair of events, with only finitely many non-zero values.
Distinguishability is defined as non-triviality of the flow (some edge has non-zero value). A recognition flow is a stronger witness: non-zero value on a genuine evolution edge between distinct events. The original axiom claimed every flow is non-trivial; that is too strong. The correct local claim is that a flow carrying recognition structure is distinguishable, which is elementary from the definitions.
proof idea
One-line term proof. It applies the sibling lemma that every recognition flow is distinguishable, supplying the flow and the recognition-flow hypothesis. Unfolding the definitions, a recognition flow already provides distinct evolving events with non-zero edge value, which is exactly non-trivial flow, hence distinguishability. The Meta-Principle hypothesis appears in the signature for uniformity with the surrounding MP-to-conservation chain but is not used in the body.
why it matters
This is the weakened axiom replacement advertised in the module: instead of asserting that every flow is distinguishable, one assumes recognition structure on the flow and concludes distinguishability with no placeholders. It feeds the module summary status object, which records that the core conservation-necessity argument is formalized without holes and that the original axiom asked the wrong question ("is every flow non-trivial?" versus "does a non-trivial flow exist?").
Together with sibling results that MP makes recognition meaningful and that non-trivial systems carry recognition events, it supports the chain MP implies non-trivial conservation. That chain is the verification-layer reason conservation laws are forced rather than postulated in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.