CoherentClosures.lean`

41 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.SeparableQuotient.CoherentClosures.PreSystem line 12
Source documentation
Finite closures on the strict initial segment at β.
```
abbrev PreSystem (β : Γ) := Set.Iio β → ℕ → Finset Γ
```
structure OAI.SeparableQuotient.CoherentClosures.PreGood line 15
Source documentation
Coherence conditions below β.
```
structure PreGood (β : Γ) (G : PreSystem β) : Prop where
…
```
Mentions: OAI.SeparableQuotient.CoherentClosures.PreSystem
structure OAI.SeparableQuotient.CoherentClosures.ExtensionGood line 24
Source documentation
The closure conditions at a new endpoint, relative to earlier closures.
```
structure ExtensionGood (β : Γ) (G : PreSystem β) (H : ℕ → Finset Γ) : Prop where
…
```
Mentions: OAI.SeparableQuotient.CoherentClosures.PreSystem
lemma OAI.SeparableQuotient.CoherentClosures.exists_next_threshold line 33
Source documentation
A threshold beyond which two specified earlier coordinates are recorded.
```
lemma exists_next_threshold {β : Γ} {G : PreSystem β} (hg : PreGood β G)
    (a b : Set.Iio β) (p : ℕ) :
    ∃ q > p, a.val ∈ G (max a b) q ∧ b.val ∈ G (max a b) q := by
…
```
Mentions: OAI.SeparableQuotient.CoherentClosures.PreSystem, OAI.SeparableQuotient.CoherentClosures.PreGood
def OAI.SeparableQuotient.CoherentClosures.stage line 46
Source documentation
Each stage of the endpoint construction keeps one earlier endpoint and an activation threshold. The next endpoint is the maximum of the old endpoint and the next enumerated predecessor.
```
noncomputable def stage {β : Γ} {G : PreSystem β} (hg : PreGood β G)
    (e : ℕ → Set.Iio β) : ℕ → Set.Iio β × ℕ
  | 0 => (e 0, 0)
  | n+1 => let v := stage hg e n
…
```
Mentions: OAI.SeparableQuotient.CoherentClosures.PreSystem, OAI.SeparableQuotient.CoherentClosures.PreGood
lemma OAI.SeparableQuotient.CoherentClosures.stage_zero line 52
lemma OAI.SeparableQuotient.CoherentClosures.stage_succ_threshold line 55
lemma OAI.SeparableQuotient.CoherentClosures.stage_threshold_strictMono line 63
lemma OAI.SeparableQuotient.CoherentClosures.stage_threshold_ge line 67
def OAI.SeparableQuotient.CoherentClosures.active line 72
Source documentation
The last activated stage at parameter p.
```
noncomputable def active {β : Γ} {G : PreSystem β} (hg : PreGood β G)
    (e : ℕ → Set.Iio β) (p : ℕ) : ℕ :=
…
```
Mentions: OAI.SeparableQuotient.CoherentClosures.PreSystem, OAI.SeparableQuotient.CoherentClosures.PreGood
lemma OAI.SeparableQuotient.CoherentClosures.active_threshold line 76
lemma OAI.SeparableQuotient.CoherentClosures.stage_le_active line 81
lemma OAI.SeparableQuotient.CoherentClosures.active_mono line 86
lemma OAI.SeparableQuotient.CoherentClosures.active_at_threshold line 91
lemma OAI.SeparableQuotient.CoherentClosures.stage_subset_succ line 98
Source documentation
Earlier stage closures embed in later ones once the later stage is active.
```
lemma stage_subset_succ {β : Γ} {G : PreSystem β} (hg : PreGood β G)
    (e : ℕ → Set.Iio β) (n p : ℕ) (hp : (stage hg e (n+1)).2 ≤ p) :
    G (stage hg e n).1 p ⊆ G (stage hg e (n+1)).1 p := by
…
```
Mentions: OAI.SeparableQuotient.CoherentClosures.PreSystem, OAI.SeparableQuotient.CoherentClosures.PreGood, OAI.SeparableQuotient.CoherentClosures.stage
lemma OAI.SeparableQuotient.CoherentClosures.stage_subset line 105
def OAI.SeparableQuotient.CoherentClosures.extended line 116
Source documentation
The new closure: keep the activated earlier closure and append β.
```
noncomputable def extended {β : Γ} {G : PreSystem β} (hg : PreGood β G)
    (e : ℕ → Set.Iio β) (p : ℕ) : Finset Γ :=
…
```
Mentions: OAI.SeparableQuotient.CoherentClosures.PreSystem, OAI.SeparableQuotient.CoherentClosures.PreGood
lemma OAI.SeparableQuotient.CoherentClosures.extended_good line 120
lemma OAI.SeparableQuotient.CoherentClosures.singleton_good line 158
Source documentation
Empty strict segments require no recursive information.
```
lemma singleton_good {β : Γ} {G : PreSystem β} (h : IsEmpty (Set.Iio β)) :
    ExtensionGood β G (fun _ => {β}) := by
…
```
Mentions: OAI.SeparableQuotient.CoherentClosures.PreSystem, OAI.SeparableQuotient.CoherentClosures.ExtensionGood
lemma OAI.SeparableQuotient.CoherentClosures.exists_extension line 171
Source documentation
Countability of the strict segment suffices to extend the coherent system.
```
lemma exists_extension {β : Γ} [Countable (Set.Iio β)]
    {G : PreSystem β} (hg : PreGood β G) :
    ∃ H : ℕ → Finset Γ, ExtensionGood β G H := by
…
```
Mentions: OAI.SeparableQuotient.CoherentClosures.PreSystem, OAI.SeparableQuotient.CoherentClosures.PreGood, OAI.SeparableQuotient.CoherentClosures.ExtensionGood
structure OAI.SeparableQuotient.CoherentClosures.GoodAt line 183
Source documentation
Full endpoint property for a total system.
```
structure GoodAt (F : Γ → ℕ → Finset Γ) (β : Γ) : Prop where
…
```
Mentions: OAI.SeparableQuotient.CoherentClosures.F
def OAI.SeparableQuotient.CoherentClosures.next line 194
Source documentation
The recursion step is defined even on bad predecessor data; the bad branch is never used in the well-founded construction.
```
noncomputable def next (β : Γ) (G : PreSystem β) : ℕ → Finset Γ := by
…
```
Mentions: OAI.SeparableQuotient.CoherentClosures.PreSystem
lemma OAI.SeparableQuotient.CoherentClosures.next_good line 199
def OAI.SeparableQuotient.CoherentClosures.system line 206
Source documentation
The actual coherently nested finite closures on the well-order.
```
noncomputable def system : Γ → ℕ → Finset Γ :=
…
```
lemma OAI.SeparableQuotient.CoherentClosures.system_eq line 209
theorem OAI.SeparableQuotient.CoherentClosures.system_goodAt line 213
Source documentation
Transfinite induction establishes the coherent closure properties.
```
theorem system_goodAt (β : Γ) : GoodAt system β := by
…
```
Mentions: OAI.SeparableQuotient.CoherentClosures.GoodAt, OAI.SeparableQuotient.CoherentClosures.system

theorem OAI.SeparableQuotient.CoherentClosures.exists_coherent_closures line 233

Source documentation

Coherent finite closures on a well-order with countable initial segments, indexed from zero.

theorem exists_coherent_closures : ∃ F : Γ → ℕ → Finset Γ,
    (∀ β n, β ∈ F β n) ∧
    (∀ β n x, x ∈ F β n → x ≤ β) ∧
    (∀ β, Monotone (F β)) ∧
    (∀ β x, x ≤ β → ∃ n, x ∈ F β n) ∧
    (∀ β α n, α ∈ F β n → F α n = (F β n).filter (fun x => x ≤ α)) := by
…

Mentions: OAI.SeparableQuotient.CoherentClosures.F

abbrev OAI.SeparableQuotient.CoherentClosures.OmegaOne line 253
Source documentation
The coordinate set of the negative construction is really ω₁.
```
abbrev OmegaOne := (Cardinal.aleph 1).ord.ToType
```
instance OAI.SeparableQuotient.CoherentClosures.omegaOne_initialSegment_countable line 255
def OAI.SeparableQuotient.CoherentClosures.F line 262
Source documentation
Positive-indexed finite closures.
```
noncomputable def F (β : OmegaOne) (p : ℕ) : Finset OmegaOne :=
…
```
Mentions: OAI.SeparableQuotient.CoherentClosures.OmegaOne
lemma OAI.SeparableQuotient.CoherentClosures.F_self line 265
lemma OAI.SeparableQuotient.CoherentClosures.F_lower line 268
lemma OAI.SeparableQuotient.CoherentClosures.F_mono line 271
lemma OAI.SeparableQuotient.CoherentClosures.F_exhaust line 275
lemma OAI.SeparableQuotient.CoherentClosures.F_coherent line 279
lemma OAI.SeparableQuotient.CoherentClosures.shared_initial_segment line 284
Source documentation
Two closures containing α have the same ordered initial segment through α.
```
lemma shared_initial_segment (β γ α : OmegaOne) (p : ℕ)
    (hβ : α ∈ F β p) (hγ : α ∈ F γ p) :
    (F β p).filter (fun x => x ≤ α) = (F γ p).filter (fun x => x ≤ α) := by
…
```
Mentions: OAI.SeparableQuotient.CoherentClosures.OmegaOne, OAI.SeparableQuotient.CoherentClosures.F
def OAI.SeparableQuotient.CoherentClosures.rho line 291
Source documentation
The first positive parameter at which α enters the closure of β. The irrelevant case α > β is set to zero.
```
noncomputable def rho (α β : OmegaOne) : ℕ := by
…
```
Mentions: OAI.SeparableQuotient.CoherentClosures.OmegaOne
lemma OAI.SeparableQuotient.CoherentClosures.rho_pos line 295
lemma OAI.SeparableQuotient.CoherentClosures.mem_F_rho line 300
lemma OAI.SeparableQuotient.CoherentClosures.rho_le_iff line 305
lemma OAI.SeparableQuotient.CoherentClosures.finite_cover line 318
Source documentation
A finite nonempty set is contained in a common closure of its largest coordinate, with one positive parameter for all its elements.
```
lemma finite_cover {A : Finset OmegaOne} (hA : A.Nonempty) :
    ∃ p ≥ 1, A ⊆ F (A.max' hA) p := by
…
```
Mentions: OAI.SeparableQuotient.CoherentClosures.OmegaOne, OAI.SeparableQuotient.CoherentClosures.F