isMinimalIn
open lean source
IndisputableMonolith.Foundation.Atomicity on GitHub at line 40.
browse module
All declarations in this module, on Recognition.
plain-language theorem explainer
The predicate isMinimalIn identifies an event e in a finite set H as minimal under a precedence relation prec if e belongs to H and no other element in H precedes it. Researchers constructing sequential schedules for finite recognition histories cite this predicate when enforcing causal constraints. The definition is realized directly as the conjunction of membership and the universal negation of precedence.
Claim. Let $E$ be a type of events and let $H$ be a finite subset of $E$. Let $e$ be an event in $E$ and let $prec$ be a precedence relation on $E$. Then $e$ is minimal in $H$ under $prec$ when $e$ belongs to $H$ and no $e'$ in $H$ satisfies $prec$ $e'$ $e$.
background
The Atomicity module supplies a constructive, axiom-free serialization result for finite recognition histories. It works abstractly over an event type $E$ equipped with a precedence relation $prec$, where $prec$ $e_1$ $e_2$ means $e_1$ must occur before $e_2$. This setting tightens T2 by providing deterministic one-per-tick schedules that respect the relation, remaining independent of cost or convexity assumptions from T5.
proof idea
The definition directly encodes the minimality condition as the conjunction of membership in the finite set $H$ together with the assertion that no element $e'$ in $H$ satisfies the precedence relation to $e$. No lemmas are applied; it is the primitive predicate used by subsequent existence results such as exists_minimal_in.
why it matters
This definition enables the existence of sequential schedules for finite histories, supporting the serialization outcome that tightens T2 in the forcing chain. It is referenced by the Precedence abstraction and by downstream constructions such as exists_minimal_in and topoSort in the same module. By providing an axiom-free way to pick minimal events, it contributes to deterministic ordering without relying on the J-uniqueness or phi fixed point from T5-T6.
depends on
-
H -
H -
H -
H -
Precedence -
Precedence -
E -
E -
mem
used by
formal source
37variable {E : Type _}
38
39/-- `isMinimalIn prec H e` means `e` is in `H` and has no predecessors in `H`. -/
40def isMinimalIn (prec : Precedence E) [DecidableEq E] [DecidableRel prec]
41 (H : Finset E) (e : E) : Prop :=
42 e ∈ H ∧ ∀ e' ∈ H, ¬ prec e' e
43
44lemma isMinimalIn.mem {prec : Precedence E} [DecidableEq E] [DecidableRel prec]
45 {H : Finset E} {e : E} :
46 isMinimalIn (E:=E) prec H e → e ∈ H :=
47 And.left
48
49/-- Minimality existence on a finite, nonempty `H` under well‑founded precedence. -/
50lemma exists_minimal_in
51 (prec : Precedence E) [DecidableRel prec] [DecidableEq E]
52 (wf : WellFounded prec) {H : Finset E} (hH : H.Nonempty) :
53 ∃ e ∈ H, ∀ e' ∈ H, ¬ prec e' e := by
54 classical
55 refine hH.elim ?_
56 intro a ha
57 have : ∀ x : E, x ∈ H → ∃ m ∈ H, ∀ y ∈ H, ¬ prec y m := by
58 intro x hx
59 -- Well-founded recursion down the precedence relation until a minimal element is reached.
60 refine wf.induction x (C := fun x => x ∈ H → ∃ m ∈ H, ∀ y ∈ H, ¬ prec y m) ?_ hx
61 intro x ih hx
62 by_cases hmin : ∀ y ∈ H, ¬ prec y x
63 · exact ⟨x, hx, hmin⟩
64 · have hnot : ¬ (∀ y ∈ H, ¬ prec y x) := hmin
65 push_neg at hnot
66 obtain ⟨y, hyH, hy⟩ := hnot
67 have hyx : prec y x := not_not.mp hy
68 exact ih y hyx hyH
69 exact this a ha
70