EventEvolution
plain-language theorem explainer
Packages a binary evolution relation on the events of a discrete event system together with a well-foundedness witness (no infinite descending chains). Downstream conservation and distinguishability arguments cite it as the temporal skeleton on which finite-support flows live. As a structure definition there is no proof body; the well-foundedness field is the only nontrivial constraint.
Claim. Given a discrete event system $E$ (a countable type of events), an event evolution consists of a relation $\mathrm{evolves} \subseteq E.\mathrm{Event} \times E.\mathrm{Event}$ together with a proof that the reverse relation is well-founded: there is no infinite descending chain $\cdots \prec e_2 \prec e_1 \prec e_0$ under $\mathrm{evolves}$.
background
The module ConservationNecessity derives non-trivial conservation from the Meta-Principle (MP), replacing an earlier axiom that recognition requires distinguishability. The argument runs: MP makes recognition possible on non-empty types; recognition needs distinction; distinction in a discrete event system needs non-zero flow; hence MP forces non-trivial conserved flows.
A discrete event system is just a countable carrier type of events. Event evolution adds directed temporal structure: which events can follow which, with well-foundedness ruling out infinite regress. That constraint matches the discrete, tick-based setting of Recognition Science (finite support, no eternal past chains).
Flows are later defined as finite-support integer-valued maps on event pairs relative to such an evolution. Distinguishability of a flow is identified with non-triviality (some edge carries non-zero value).
proof idea
Definition only: no proof body. The structure has two fields. The first is an arbitrary binary relation evolves on the event type. The second requires Mathlib well-foundedness of the reverse relation, so every non-empty set of events has an evolves-minimal element and induction on evolution is legal. Downstream lemmas (e.g. distinction implies flow structure, flow-on-edge constructions) take an EventEvolution as a parameter and never reopen this packaging.
why it matters
This is the temporal substrate for the whole conservation-necessity chain. FlowFS, Distinguishable, FlowOnEdge, HasRecognitionEvents, and IsRecognitionFlow are all indexed by an event evolution. The key lemma that distinct evolved pairs force non-zero flow, and the main theorem conservation_necessity_proven (MP plus a non-trivial evolution edge yields a non-trivial conserved flow), both quantify over it.
In framework terms it supplies the discrete event graph on which recognition flow (information transfer during recognition) is defined, closing the gap that previously left recognition_requires_distinguishability as an axiom in LedgerNecessity. It does not itself invoke J-cost, phi, or the T0–T8 forcing chain; those enter elsewhere. Its role is local: make evolution a first-class, well-founded object so conservation can be stated and proved rather than assumed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.