UniformNames.lean`

28 declarations, 0 contain sorry, 0 declared as axioms

UniformFamily

def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.uniformRange line 17
Source documentation
The range of a small ground family all of whose entries have the same literal support. This is an actual HS name, not an external evaluated set.
```
def uniformRange {ι : Type t} [Small.{u} ι] (f : ι → S.Name)
    (H : Subgroup Γ) (hH : H ∈ S.filter) (hfix : ∀ g ∈ H, ∀ i, g • f i = f i) : S.Name :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.uniformRange_fixed line 22
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mem_uniformRange line 30
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.uniformRange_mem line 45
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.indexedGraph_surjection line 53
Source documentation
The canonical family graph enumerates exactly the corresponding range. The witnesses of the surjection formula are internal ordered-pair sets.
```
theorem indexedGraph_surjection (X : ZFSet.{u}) (f : X → S.Name)
    (H : Subgroup Γ) (hH : H ∈ S.filter) (hfix : ∀ g ∈ H, ∀ i, g • f i = f i) (p : P) :
    S.Forces ![S.indexedGraph X f H hH hfix,Name.check X,S.uniformRange f H hH hfix] p
      (SetLanguage.surjection 0 1 2) := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.check, OAI.PartitionConsistency.SetLanguage.surjection

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_injection line 74

Source documentation

The injection sentence, with its full maps-to conjunct retained.

theorem forces_injection {n} (v : Fin n → S.Name) (p : P) (f a b : Fin n) :
    S.Forces v p (SetLanguage.injection f a b) ↔
      S.Forces ![v f,v a,v b] p (SetLanguage.mapsTo 0 1 2) ∧
      ∀ x y z : S.Name, ∀ q, q ≤ p → S.atomic.MemF q x (v a) →
        ∀ r, r ≤ q → S.atomic.MemF r y (v a) → ∀ s, s ≤ r →
          S.App s (v f) x z ∧ S.App s (v f) y z → S.atomic.EqF s x y := by
…

Mentions: OAI.PartitionConsistency.SetLanguage.injection, OAI.PartitionConsistency.SetLanguage.mapsTo

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.BinaryRelation.graph_injection line 92

Source documentation

A bounded functional relation which is also one-to-one gives an actual internal injection graph.

theorem BinaryRelation.graph_injection (R : S.BinaryRelation)
    (X Y : S.Name) (H : Subgroup Γ) (hH : H ∈ S.filter)
    (hX : ∀ g ∈ H, g • X = X) (hY : ∀ g ∈ H, g • Y = Y)
    (hR : ∀ g ∈ H, ∀ p x y, R.holds p x y → R.holds (S.move g p) (g • x) (g • y))
    (p : P)
    (htotal : ∀ x : S.Name, ∀ q, q ≤ p → S.atomic.MemF q x X →
      ∀ r, r ≤ q → ∃ s, s ≤ r ∧ ∃ y : S.Name, S.atomic.MemF s y Y ∧ R.holds s x y)
    (hone : ∀ q, q ≤ p → ∀ x y z : S.Name, R.holds q x y → R.holds q x z →
      S.atomic.EqF q y z)
    (hinj : ∀ q, q ≤ p → ∀ x y z : S.Name, R.holds q x z → R.holds q y z →
      S.atomic.EqF q x y) :
    S.Forces ![R.graph X Y H hH hX hY hR,X,Y] p (SetLanguage.injection 0 1 2) := by
…

Mentions: OAI.PartitionConsistency.SetLanguage.injection

def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.UniformInverse.LeastValue line 117
Source documentation
The index is the least possible index of this value. Negative equality with every earlier entry is forced, not merely unforced at this condition.
```
def LeastValue (p : P) (x : S.Name) (i : X) : Prop :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.UniformInverse.least_mono line 121
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.UniformInverse.least_congr line 126
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.UniformInverse.least_unique line 136
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.UniformInverse.Holds line 144
Source documentation
Regularization of the indexed least-value relation.
```
def Holds (p : P) (x y : S.Name) : Prop :=
…
```
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.UniformInverse.relation line 148
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.UniformInverse.relation_one line 165
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.UniformInverse.relation_inj line 176
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.UniformInverse.relation_total line 191
Source documentation
Least indices are dense below every condition forcing membership in this range. Minimality is proved using the ground wellorder; no choice function in the symmetric extension or completeness of a filter is assumed.
```
theorem relation_total (H : Subgroup Γ) (hH : H ∈ S.filter)
    (hfix : ∀ g ∈ H, ∀ i, g • f i = f i) (x : S.Name) (p : P)
    (hm : S.atomic.MemF p x (S.uniformRange f H hH hfix)) :
    ∀ q, q ≤ p → ∃ r, r ≤ q ∧ ∃ y : S.Name,
      S.atomic.MemF r y (Name.check X) ∧ (relation X f).holds r x y := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.check, OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.UniformInverse.relation
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.UniformInverse.least_move line 212
Source documentation
The least-value test is covariant under each automorphism fixing all entries of the family. Its negative conjunct is transported at every stronger condition by the inverse order isomorphism.
```
theorem least_move (H : Subgroup Γ)
    (hfix : ∀ g ∈ H, ∀ i, g • f i = f i) (g : Γ) (hg : g ∈ H)
    {p : P} {x : S.Name} {i : X} (hi : LeastValue X f p x i) :
    LeastValue X f (S.move g p) (g • x) i := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.UniformInverse.LeastValue
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.UniformInverse.relation_move line 224
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.uniformRangeInverse line 239
Source documentation
The sequence range admits an internal injection into its ground index set. This implements the least-occurrence argument with an actual HS graph; it does not assume that all its values are ground or that equalities of values can be decided uniformly by a single condition.
```
def uniformRangeInverse (X : ZFSet.{u}) (f : X → S.Name)
    (H : Subgroup Γ) (hH : H ∈ S.filter) (hfix : ∀ g ∈ H, ∀ i, g • f i = f i) : S.Name :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.uniformRangeInverse_injection line 245
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.uniformSubsetInverse line 259
Source documentation
The same least-index graph restricted to an arbitrary supported set. The set need not have a literal representative among the indexed entries.
```
def uniformSubsetInverse (X : ZFSet.{u}) (f : X → S.Name) (Y : S.Name)
    (H : Subgroup Γ) (hH : H ∈ S.filter) (hfix : ∀ g ∈ H, ∀ i, g • f i = f i)
    (hY : ∀ g ∈ H, g • Y = Y) : S.Name :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.uniformSubsetInverse_injection line 265

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.outside_uniformRange line 282

Source documentation

If a set cannot be injected into the index set, then densely it has an element outside this evaluation list. Nonmembership in the list is forced below the witness condition, rather than just presently undecided.

theorem outside_uniformRange (X : ZFSet.{u}) (f : X → S.Name) (Y : S.Name)
    (H : Subgroup Γ) (hH : H ∈ S.filter) (hfix : ∀ g ∈ H, ∀ i, g • f i = f i)
    (hY : ∀ g ∈ H, g • Y = Y) (p : P)
    (hno : ∀ q, q ≤ p → ∀ J : S.Name,
      ¬ S.Forces ![J,Y,Name.check X] q (SetLanguage.injection 0 1 2)) :
    ∀ q, q ≤ p → ∃ r, r ≤ q ∧ ∃ y : S.Name, S.atomic.MemF r y Y ∧
      ∀ s, s ≤ r → ¬ S.atomic.MemF s y (S.uniformRange f H hH hfix) := by
…

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

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mem_checkOrdinal line 318

Source documentation

Members of a checked ordinal are locally checked smaller ordinals.

theorem mem_checkOrdinal (α : Ordinal.{u}) (x : S.Name) (p : P) :
    S.atomic.MemF p x (Name.check α.toZFSet) ↔
      ∀ q, q ≤ p → ∃ r, r ≤ q ∧ ∃ β : Ordinal.{u}, β < α ∧
        S.atomic.EqF r x (Name.check β.toZFSet) := by
…

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

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.transF_checkOrdinal line 334
Source documentation
Transitivity of a ground ordinal survives arbitrary set symmetric forcing. Quantified members here are all HS names, not just check names.
```
theorem transF_checkOrdinal (α : Ordinal.{u}) (p : P) :
    S.TransF p (Name.check α.toZFSet) := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.check
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.ordF_checkOrdinal line 347
Source documentation
Each member of a check ordinal is forced to be transitive as well.
```
theorem ordF_checkOrdinal (α : Ordinal.{u}) (p : P) :
    S.OrdF p (Name.check α.toZFSet) := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.check
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_membershipWellFounded line 361
Source documentation
Internal membership well-foundedness follows from the proved name-rank Foundation argument, and holds for every set of the symmetric model.
```
theorem forces_membershipWellFounded {n} (v : Fin n → S.Name) (p : P) (a : Fin n) :
    S.Forces v p (SetLanguage.membershipWellFounded a) := by
…
```
Mentions: OAI.PartitionConsistency.SetLanguage.membershipWellFounded
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_checkOrdinal line 378
Source documentation
An actual checked ordinal satisfies the exact ordinal formula used by ACwo. Neither external well-foundedness of a model nor a weakened proxy for that formula is used.
```
theorem forces_checkOrdinal (α : Ordinal.{u}) (p : P) :
    S.Forces ![Name.check α.toZFSet] p (SetLanguage.ordinal 0) := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.check, OAI.PartitionConsistency.SetLanguage.ordinal