GroundModels.lean`

33 declarations, 0 contain sorry, 0 declared as axioms

A concrete choice ground and collapse in Lean's universe metatheory.

This supplies an actual well-founded choice ground rather than hypothesizing one. It does not supply the source's symmetric extension, does not prove the constructible interpretation in ZF; the main proof below instead uses the concrete forcing interpretation.

theorem OAI.PartitionConsistency.Formula.realize_close line 22
theorem OAI.PartitionConsistency.SetLanguage.realize_relation line 45
theorem OAI.PartitionConsistency.SetLanguage.realize_separation line 58
theorem OAI.PartitionConsistency.SetLanguage.realize_replacement line 81
abbrev OAI.PartitionConsistency.ZFUniverse.E line 106
theorem OAI.PartitionConsistency.ZFUniverse.realize_subset line 109
theorem OAI.PartitionConsistency.ZFUniverse.realize_empty line 113
theorem OAI.PartitionConsistency.ZFUniverse.realize_nonempty line 117
theorem OAI.PartitionConsistency.ZFUniverse.realize_pair line 121
theorem OAI.PartitionConsistency.ZFUniverse.realize_successor line 126
theorem OAI.PartitionConsistency.ZFUniverse.realize_orderedPair line 131
theorem OAI.PartitionConsistency.ZFUniverse.realize_edge line 135
theorem OAI.PartitionConsistency.ZFUniverse.realize_functionOn line 139
theorem OAI.PartitionConsistency.ZFUniverse.realize_mapsTo line 145
theorem OAI.PartitionConsistency.ZFUniverse.separation_true line 166
Source documentation
The full parameterized Separation schema holds in the genuine set universe.
```
theorem separation_true {n} (p : Formula (n + 1)) :
    Realize E.{u} Fin.elim0 (separation p) := by
…
```
Mentions: OAI.PartitionConsistency.Formula
theorem OAI.PartitionConsistency.ZFUniverse.replacement_true line 173
Source documentation
The full parameterized Replacement schema holds in the genuine set universe.
```
theorem replacement_true {n} (p : Formula (n + 2)) :
    Realize E.{u} Fin.elim0 (replacement p) := by
…
```
Mentions: OAI.PartitionConsistency.Formula
theorem OAI.PartitionConsistency.ZFUniverse.models_ZF line 191
Source documentation
A concrete model of every axiom and schema instance of pure ZF.
```
theorem models_ZF : Models E.{u} SetLanguage.ZF := by
…
```
Mentions: OAI.PartitionConsistency.Models, OAI.PartitionConsistency.SetLanguage.ZF
theorem OAI.PartitionConsistency.ZFUniverse.realize_choiceOn line 239
theorem OAI.PartitionConsistency.ZFUniverse.AC_true line 246
Source documentation
The set-graph version of Choice is true in the ambient universe. It is obtained from Lean's permitted Classical.choice, not an additional axiom.
```
theorem AC_true : Realize E.{u} Fin.elim0 AC := by
…
```
theorem OAI.PartitionConsistency.ZFUniverse.models_ZFC line 270
Source documentation
Full ZFC in exactly the syntax used for the selected consistency target.
```
theorem models_ZFC : Models E.{u} (SetLanguage.ZF ∪ {AC}) := by
…
```
Mentions: OAI.PartitionConsistency.Models, OAI.PartitionConsistency.SetLanguage.ZF
theorem OAI.PartitionConsistency.Formula.realize_equiv line 281
Source documentation
Truth in the target syntax is invariant under genuine structure isomorphisms.
```
theorem realize_equiv {M N : Type*} (E : M → M → Prop) (F : N → N → Prop)
    (e : M ≃ N) (he : ∀ a b, E a b ↔ F (e a) (e b)) {n} (p : Formula n)
    (v : Fin n → M) : Realize E v p ↔ Realize F (e ∘ v) p := by
…
```
Mentions: OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.Formula.Realize
theorem OAI.PartitionConsistency.models_equiv line 309
Source documentation
Transport of a whole theory, including schemas, across a relational isomorphism.
```
theorem models_equiv {M N : Type*} (E : M → M → Prop) (F : N → N → Prop)
    (e : M ≃ N) (he : ∀ a b, E a b ↔ F (e a) (e b)) (T : Theory) :
    Models E T ↔ Models F T := by
…
```
Mentions: OAI.PartitionConsistency.Theory, OAI.PartitionConsistency.Models
def OAI.PartitionConsistency.Mostowski.collapse line 323
Source documentation
Collapse by genuine external well-founded recursion, not recursion over an arbitrary first-order model's internal membership relation.
```
noncomputable def collapse : M → ZFSet.{u} :=
…
```
theorem OAI.PartitionConsistency.Mostowski.collapse_eq line 326
theorem OAI.PartitionConsistency.Mostowski.mem_collapse_iff line 330
theorem OAI.PartitionConsistency.Mostowski.collapse_injective line 340
Source documentation
Extensionality makes the collapse injective.
```
theorem collapse_injective : Function.Injective (collapse.{u} hw) := by
…
```
theorem OAI.PartitionConsistency.Mostowski.collapse_mem_collapse line 362
theorem OAI.PartitionConsistency.Mostowski.range_transitive line 371
Source documentation
The range of the collapse is transitive as a collection of actual sets.
```
theorem range_transitive : ∀ a ∈ Set.range (collapse.{u} hw), ∀ b ∈ a,
    b ∈ Set.range (collapse hw) := by
…
```
Mentions: OAI.PartitionConsistency.Mostowski.collapse
def OAI.PartitionConsistency.Mostowski.rangeEquiv line 378
Source documentation
Collapse is a membership isomorphism onto its transitive range.
```
noncomputable def rangeEquiv : M ≃ Set.range (collapse.{u} hw) :=
…
```
theorem OAI.PartitionConsistency.Mostowski.rangeEquiv_mem line 381
theorem OAI.PartitionConsistency.Mostowski.range_models line 387
Source documentation
A well-founded extensional small model has an isomorphic transitive model.
```
theorem range_models {T : Theory} (hT : Models E T) :
    Models (fun a b : Set.range (collapse.{u} hw) => a.val ∈ b.val) T :=
…
```
Mentions: OAI.PartitionConsistency.Theory, OAI.PartitionConsistency.Models
theorem OAI.PartitionConsistency.ZFUniverse.exists_countable_transitive_ZFC line 399
Source documentation
In Lean's universe metatheory there is a countable, transitive pure-set model of full ZFC. This is proved using ZFSet, downward Löwenheim–Skolem, and the collapse; it is NOT an assumption inferred from bare Con(ZF).
```
theorem exists_countable_transitive_ZFC :
    ∃ M : Set ZFSet.{0}, M.Nonempty ∧ M.Countable ∧
      (∀ a ∈ M, ∀ b ∈ a, b ∈ M) ∧
      Models (fun a b : M => a.val ∈ b.val) (SetLanguage.ZF ∪ {AC}) := by
…
```
Mentions: OAI.PartitionConsistency.Models, OAI.PartitionConsistency.SetLanguage.ZF
theorem OAI.PartitionConsistency.ZFUniverse.consistent_ZFC line 422
Source documentation
Existence of an actual choice ground, not yet an extension violating Choice.
```
theorem consistent_ZFC : Consistent (SetLanguage.ZF ∪ {AC}) :=
…
```
Mentions: OAI.PartitionConsistency.Consistent, OAI.PartitionConsistency.SetLanguage.ZF