OrdinalPresentation.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

Completion

def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.BinaryRelation.ofFormula line 17
Source documentation
Any fixed formula with two distinguished free variables gives a regular binary forcing relation. Its other free variables remain actual parameters.
```
def ofFormula {n} (v : Fin n → S.Name) (φ : Formula (n+2)) : S.BinaryRelation where
…
```
Mentions: OAI.PartitionConsistency.Formula
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.BinaryRelation.ofFormula_symmetry line 31
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.defaultFormula line 50
Source documentation
Use a partial graph's value when it belongs to the codomain, and otherwise use the specified default. The variables are f,X,x₀,a,y, respectively.
```
def defaultFormula : Formula 5 :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.defaultRelation line 54
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.NoValue line 57
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.noValue_mono line 61

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.defaultRelation_iff line 68

Source documentation

An exact description of the default relation's Boolean disjunction. The fallback is used only when every possible bounded graph value is ruled out.

theorem defaultRelation_iff (f X x₀ a y : S.Name) (p : P) :
    (S.defaultRelation f X x₀).holds p a y ↔
      ∀ q, q ≤ p → ∃ r, r ≤ q ∧
        ((S.App r f a y ∧ S.atomic.MemF r y X) ∨
          (S.NoValue f X r a ∧ S.atomic.EqF r y x₀)) := by
…

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.defaultRelation_of_app line 96

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.defaultRelation_total line 106

Source documentation

The default construction is densely total, with values actually in X, whenever the default belongs to X.

theorem defaultRelation_total (f X x₀ a : S.Name) {p : P} (hx₀ : S.atomic.MemF p x₀ X) :
    ∀ q, q ≤ p → ∃ r, r ≤ q ∧ ∃ y : S.Name,
      S.atomic.MemF r y X ∧ (S.defaultRelation f X x₀).holds r a y := by
…

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.defaultRelation_unique line 122

Source documentation

Completing a genuinely single-valued partial graph preserves uniqueness.

theorem defaultRelation_unique (f X x₀ : S.Name)
    (hf : ∀ p, ∀ a y z : S.Name, S.App p f a y → S.App p f a z → S.atomic.EqF p y z)
    (p : P) (a y z : S.Name) (hy : (S.defaultRelation f X x₀).holds p a y)
    (hz : (S.defaultRelation f X x₀).holds p a z) : S.atomic.EqF p y z := by
…

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.defaultRelation_symmetry line 138
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.completionRelation line 149
Source documentation
A ground-indexed family of completed partial maps, with an actual ordered pair as input. Local witnesses are regularized, as in existential forcing.
```
def completionRelation (O : ZFSet.{u}) (f : O → S.Name) (X x₀ : S.Name) : S.BinaryRelation where
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.completionRelation_at line 173
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.completionRelation_symmetry line 178

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.completionRelation_unique line 191

Source documentation

Uniqueness for a family of partial functions survives both completion and packaging into one Cartesian-domain graph.

theorem completionRelation_unique (O : ZFSet.{u}) (f : O → S.Name) (X x₀ : S.Name)
    (hf : ∀ i p, ∀ a y z : S.Name, S.App p (f i) a y → S.App p (f i) a z →
      S.atomic.EqF p y z) (p : P) (x y z : S.Name)
    (hy : (S.completionRelation O f X x₀).holds p x y)
    (hz : (S.completionRelation O f X x₀).holds p x z) : S.atomic.EqF p y z := by
…

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.completionRelation_total line 211

Source documentation

The completed relation is total on the literal product name.

theorem completionRelation_total (O : ZFSet.{u}) (f : O → S.Name) (A X x₀ : S.Name)
    {p : P} (hx₀ : S.atomic.MemF p x₀ X) (x : S.Name) {q : P} (hqp : q ≤ p)
    (hx : S.atomic.MemF q x (S.cartesianName A (Name.check O))) :
    ∀ r, r ≤ q → ∃ s, s ≤ r ∧ ∃ y : S.Name,
      S.atomic.MemF s y X ∧ (S.completionRelation O f X x₀).holds s x y := by
…

Mentions: OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.check

def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.completionGraph line 230
Source documentation
Auxiliary graph construction for a family of invariant partial orbit maps. The support is precisely a common support for the three displayed set names.
```
def completionGraph (O : ZFSet.{u}) (f : O → S.Name) (A X x₀ : S.Name)
    (hf : ∀ g : Γ, ∀ i, g • f i = f i) : S.Name :=
…
```

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.completionGraph_surjection line 243

Source documentation

A densely covering family of invariant partial functions yields an actual internal surjection from A × O onto X. All graph and domain names have been constructed; the family and its covering property are explicit inputs here.

theorem completionGraph_surjection (O : ZFSet.{u}) (f : O → S.Name) (A X x₀ : S.Name)
    (hinv : ∀ g : Γ, ∀ i, g • f i = f i)
    (hf : ∀ i p, ∀ a y z : S.Name, S.App p (f i) a y → S.App p (f i) a z →
      S.atomic.EqF p y z) (p : P) (hx₀ : S.atomic.MemF p x₀ X)
    (hcover : ∀ y : S.Name, ∀ q, q ≤ p → S.atomic.MemF q y X →
      ∀ r, r ≤ q → ∃ s, s ≤ r ∧ ∃ i : O, ∃ a : S.Name,
        S.atomic.MemF s a A ∧ S.App s (f i) a y) :
    S.Forces ![S.completionGraph O f A X x₀ hinv,S.cartesianName A (Name.check O),X]
      p (SetLanguage.surjection 0 1 2) := by
…

Mentions: OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.check, OAI.PartitionConsistency.SetLanguage.surjection

theorem OAI.PartitionConsistency.exists_ordinal_equiv line 284
Source documentation
Every small type can be enumerated by the elements of an actual ground ordinal. This is an external use of Choice, not of Choice in the symmetric model being constructed.
```
theorem exists_ordinal_equiv (α : Type (u+1)) [Small.{u} α] :
    ∃ o : Ordinal.{u}, Nonempty (o.toZFSet ≃ α) := by
…
```
def OAI.PartitionConsistency.ProductForcing.PresentationIndex line 305
Source documentation
All literal member names of X together with all their supporting diagrams. No rank bound is placed on X or on its descendants.
```
def PresentationIndex (X : (system (M := M) (I := I) (κ := κ) hμ).Name) :=
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system
instance OAI.PartitionConsistency.ProductForcing.(instance at line 309) line 309
def OAI.PartitionConsistency.ProductForcing.presentationPartial line 316
Source documentation
The partial function associated to a presentation record is a literal orbit graph, not a selected representative in an evaluated universe.
```
def presentationPartial (c : κ → ZFSet.{u})
    (X : (system (M := M) (I := I) (κ := κ) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.smul_presentationPartial line 321
theorem OAI.PartitionConsistency.ProductForcing.presentationPartial_unique line 329
Source documentation
Single-valuedness uses genuine label separation and the support recorded in the index. It is proved uniformly for all records.
```
theorem presentationPartial_unique [Uncountable κ] (c : κ → ZFSet.{u})
    (hc : Function.Injective c)
    (X : (system (M := M) (I := I) (κ := κ) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.presentationPartial_cover line 342
Source documentation
Every member is densely reached by one of the presentation's partial functions. The supporting diagram is chosen below the condition witnessing membership, rather than presumed to belong to a generic filter.
```
theorem presentationPartial_cover [Infinite I]
    (hcard : Cardinal.mk M = μ) (hsize : Cardinal.mk M < Cardinal.mk I)
    (e : M)
    (he : Cardinal.mk ((Set.range (fun x : M => e * x))ᶜ : Set M) = Cardinal.mk M)
    (c : κ → ZFSet.{u})
    (X y : (system (M := M) (I := I) (κ := κ) hμ).Name) (t : Poset M I κ)
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system, OAI.PartitionConsistency.ProductForcing.Poset
theorem OAI.PartitionConsistency.ProductForcing.ordinal_presentation line 385
Source documentation
The unrestricted-rank presentation theorem. Given a single member of X at a condition, this constructs an actual internal graph forced to surject from the Cartesian product of the invariant label set with a ground ordinal. There is no inaccessible cardinal, name-rank bound, or assumed coverage.
```
theorem ordinal_presentation [Infinite I] [Uncountable κ]
    (hcard : Cardinal.mk M = μ) (hsize : Cardinal.mk M < Cardinal.mk I)
    (e : M)
    (he : Cardinal.mk ((Set.range (fun x : M => e * x))ᶜ : Set M) = Cardinal.mk M)
    (c : κ → ZFSet.{u}) (hc : Function.Injective c)
    (X x₀ : (system (M := M) (I := I) (κ := κ) hμ).Name) (p : Poset M I κ)
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system, OAI.PartitionConsistency.ProductForcing.Poset