NameActions.lean`

41 declarations, 0 contain sorry, 0 declared as axioms

def OAI.PartitionConsistency.SetForcingNames.ConditionAction.MixtureEdges line 13
Source documentation
The index set for the mixture in the support-descent argument. Both the trigger and the original member condition are respected.
```
def MixtureEdges (R : ZFSet.{u} → ZFSet.{u} → Prop) (H : Subgroup Γ)
    (δ σ : ZFSet.{u}) :=
…
```
instance OAI.PartitionConsistency.SetForcingNames.ConditionAction.(instance at line 19) line 19
def OAI.PartitionConsistency.SetForcingNames.ConditionAction.mixtureName line 26
Source documentation
A set name formed from all translates with active triggers. Using all common strengthenings is essential: a selected meet need not exist.
```
noncomputable def mixtureName (R : ZFSet.{u} → ZFSet.{u} → Prop) (H : Subgroup Γ)
    (δ σ : ZFSet.{u}) : ZFSet.{u} :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.mem_mixtureName_iff line 31
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.edge_mixtureName_iff line 43
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.mixtureName_isName line 56

theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.evaluate_mixtureName line 66

Source documentation

The value is exactly the union of the values of the triggered copies. The statement does not presume that moved conditions stay in the same filter.

theorem evaluate_mixtureName {R : ZFSet.{u} → ZFSet.{u} → Prop} {H : Subgroup Γ}
    {G : Set ZFSet.{u}} (hGP : G ⊆ S.conditions)
    (hup : ∀ p ∈ S.conditions, ∀ q ∈ G, R q p → p ∈ G)
    (hdir : ∀ p ∈ G, ∀ r ∈ G, ∃ q ∈ G, R q p ∧ R q r)
    {δ σ : ZFSet.{u}} (hδ : δ ∈ S.conditions) (hσ : IsName S.conditions σ) :
    evaluate G (S.mixtureName R H δ σ) = ZFSet.sUnion
      (ZFSet.range fun g : {g : H // S.actCode g.val δ ∈ G} =>
        evaluate G (mapConditions (S.actCode g.val.val) σ)) := by
…

Mentions: OAI.PartitionConsistency.SetForcingNames.IsName, OAI.PartitionConsistency.SetForcingNames.evaluate, OAI.PartitionConsistency.SetForcingNames.mapConditions

theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.mapConditions_actCode_mul line 94
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.mapConditions_mixtureName line 103
Source documentation
Left multiplication by any element of the mixing subgroup permutes the entries of the mixture literally. No equality of interpreted values is used.
```
theorem mapConditions_mixtureName (R : ZFSet.{u} → ZFSet.{u} → Prop)
    (hR : ∀ g p q, R (S.actCode g p) (S.actCode g q) ↔ R p q)
    (H : Subgroup Γ) {g : Γ} (hg : g ∈ H) (δ σ : ZFSet.{u}) :
    mapConditions (S.actCode g) (S.mixtureName R H δ σ) = S.mixtureName R H δ σ := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.mapConditions
def OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.mixture line 136
Source documentation
Literal mixture of names, with no fixed name-rank cutoff.
```
noncomputable def mixture (R : ZFSet.{u} → ZFSet.{u} → Prop) (H : Subgroup Γ)
    (δ : ZFSet.{u}) (σ : S.Name) : S.Name :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.smul_mixture line 140
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.mixture_HS line 149
Source documentation
The descent constructor is HS when the mixing subgroup is in the normal filter. Its subnames are actual translates of subnames of the original.
```
theorem mixture_HS {F : Set (Subgroup Γ)} (hF : SupportFilter.IsNormalFilter F)
    (R : ZFSet.{u} → ZFSet.{u} → Prop)
    (hR : ∀ g p q, R (S.actCode g p) (S.actCode g q) ↔ R p q)
    (H : Subgroup Γ) (hH : H ∈ F) (δ : ZFSet.{u}) {σ : S.Name} (hσ : HS F σ) :
    HS F (mixture R H δ σ) := by
…
```
Mentions: OAI.PartitionConsistency.SupportFilter.IsNormalFilter, OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.HS, OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.mixture

theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.evaluate_mixture_eq line 167

Source documentation

Once coherence of active copies has been established, the mixture is a name for their common value. Coherence itself is a separate forcing argument.

theorem evaluate_mixture_eq {R : ZFSet.{u} → ZFSet.{u} → Prop} {H : Subgroup Γ}
    {G : Set ZFSet.{u}} (hGP : G ⊆ S.conditions)
    (hup : ∀ p ∈ S.conditions, ∀ q ∈ G, R q p → p ∈ G)
    (hdir : ∀ p ∈ G, ∀ r ∈ G, ∃ q ∈ G, R q p ∧ R q r)
    {δ : ZFSet.{u}} (hδ : δ ∈ G) (σ : S.Name)
    (hcoh : ∀ g ∈ H, S.actCode g δ ∈ G → evaluate G (g • σ).val = evaluate G σ.val) :
    evaluate G (mixture R H δ σ).val = evaluate G σ.val := by
…

Mentions: OAI.PartitionConsistency.SetForcingNames.evaluate, OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.mixture

def OAI.PartitionConsistency.TransitiveSets.IsTransitive line 197
Source documentation
Usual external transitivity of an actual collection of pure sets.
```
def IsTransitive (M : Set ZFSet.{u}) : Prop := ∀ a ∈ M, ∀ b ∈ a, b ∈ M
```
def OAI.PartitionConsistency.TransitiveSets.E line 200
Source documentation
Internal membership is literal membership, restricted to the collection.
```
def E (M : Set ZFSet.{u}) (a b : M) : Prop := a.val ∈ b.val
…
```
theorem OAI.PartitionConsistency.TransitiveSets.IsTransitive.pair_left line 204
theorem OAI.PartitionConsistency.TransitiveSets.IsTransitive.pair_right line 208
theorem OAI.PartitionConsistency.TransitiveSets.IsTransitive.child line 213
Source documentation
An active subname of a name in a transitive ground is itself in the ground.
```
theorem IsTransitive.child (hM : IsTransitive M) {σ τ : ZFSet.{u}}
    (hσ : σ ∈ M) (he : SetForcingNames.Child τ σ) : τ ∈ M := by
…
```
Mentions: OAI.PartitionConsistency.TransitiveSets.IsTransitive, OAI.PartitionConsistency.SetForcingNames.Child
theorem OAI.PartitionConsistency.TransitiveSets.realize_subset line 218
theorem OAI.PartitionConsistency.TransitiveSets.realize_empty line 229
theorem OAI.PartitionConsistency.TransitiveSets.realize_nonempty line 238
theorem OAI.PartitionConsistency.TransitiveSets.realize_pair line 246
theorem OAI.PartitionConsistency.TransitiveSets.realize_orderedPair line 268
theorem OAI.PartitionConsistency.TransitiveSets.realize_edge line 287
theorem OAI.PartitionConsistency.TransitiveSets.extensionality_true line 300
Source documentation
Extensionality is inherited by every transitive collection of actual sets.
```
theorem extensionality_true (hM : IsTransitive M) :
    Realize (E M) Fin.elim0 extensionality := by
…
```
Mentions: OAI.PartitionConsistency.TransitiveSets.IsTransitive, OAI.PartitionConsistency.TransitiveSets.E
theorem OAI.PartitionConsistency.TransitiveSets.foundation_true line 315
Source documentation
Foundation is inherited, including when the collection is not closed under arbitrary subsets. This uses actual membership, not a purported action on values.
```
theorem foundation_true (hM : IsTransitive M) :
    Realize (E M) Fin.elim0 foundation := by
…
```
Mentions: OAI.PartitionConsistency.TransitiveSets.IsTransitive, OAI.PartitionConsistency.TransitiveSets.E
theorem OAI.PartitionConsistency.TransitiveSets.empty_mem line 335
Source documentation
Closure under the empty set follows from the actual first-order ground axiom.
```
theorem empty_mem : (∅ : ZFSet.{u}) ∈ M := by
…
```
theorem OAI.PartitionConsistency.TransitiveSets.pair_mem line 341
Source documentation
Literal unordered pairing is absolute for a transitive ZF ground.
```
theorem pair_mem {a b : ZFSet.{u}} (ha : a ∈ M) (hb : b ∈ M) :
    ({a, b} : ZFSet.{u}) ∈ M := by
…
```
theorem OAI.PartitionConsistency.TransitiveSets.singleton_mem line 347
theorem OAI.PartitionConsistency.TransitiveSets.orderedPair_mem line 350
theorem OAI.PartitionConsistency.TransitiveSets.sUnion_mem line 355
Source documentation
Union is also absolute; no closure under all external subsets is asserted.
```
theorem sUnion_mem {a : ZFSet.{u}} (ha : a ∈ M) : ZFSet.sUnion a ∈ M := by
…
```
theorem OAI.PartitionConsistency.TransitiveSets.separation_mem line 374
Source documentation
The Separation schema yields every formula-defined relative subset, with parameters in the ground. The subset predicate is internal satisfaction.
```
theorem separation_mem {n} (φ : Formula (n + 1)) (v : Fin n → M)
    {a : ZFSet.{u}} (ha : a ∈ M) :
    ZFSet.sep (fun x => ∃ hx : x ∈ M, Realize (E M) (Fin.snoc v ⟨x, hx⟩) φ) a ∈ M := by
…
```
Mentions: OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.TransitiveSets.E
def OAI.PartitionConsistency.SetForcingNames.ConditionAction.symmetricValues line 401
Source documentation
The actual symmetric interpretation of ground set-name codes. Membership in this domain is witnessed by a ground HS name, not by a required target axiom.
```
def symmetricValues (M : Set ZFSet.{u}) (F : Set (Subgroup Γ))
    (G : Set ZFSet.{u}) : Set ZFSet.{u} :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.symmetricValues_transitive line 407
Source documentation
Hereditary symmetry and transitivity of the ground make the interpretation transitive. No filter genericity or rank restriction is needed for this fact.
```
theorem symmetricValues_transitive {M : Set ZFSet.{u}}
    (hM : TransitiveSets.IsTransitive M) (F : Set (Subgroup Γ)) (G : Set ZFSet.{u}) :
    TransitiveSets.IsTransitive (S.symmetricValues M F G) := by
…
```
Mentions: OAI.PartitionConsistency.TransitiveSets.IsTransitive
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.symmetricValues_countable line 415
Source documentation
A countable ground gives a countable actual symmetric interpretation.
```
theorem symmetricValues_countable {M : Set ZFSet.{u}} (hc : M.Countable)
    (F : Set (Subgroup Γ)) (G : Set ZFSet.{u}) : (S.symmetricValues M F G).Countable := by
…
```
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.symmetricValues_extensionality line 421
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.symmetricValues_foundation line 427
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.empty_mem_symmetricValues line 433
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.pair_mem_symmetricValues line 439
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.symmetricValues_emptySet line 456
Source documentation
This is only the empty-set axiom, not an assertion of the full symmetric model theorem or of its Separation and Replacement schemas.
```
theorem symmetricValues_emptySet {M : Set ZFSet.{u}}
    (hM : TransitiveSets.IsTransitive M) (hZF : Models (TransitiveSets.E M) SetLanguage.ZF)
    {F : Set (Subgroup Γ)} (htop : (⊤ : Subgroup Γ) ∈ F) (G : Set ZFSet.{u}) :
    Formula.Realize (TransitiveSets.E (S.symmetricValues M F G)) Fin.elim0
      SetLanguage.emptySet := by
…
```
Mentions: OAI.PartitionConsistency.TransitiveSets.IsTransitive, OAI.PartitionConsistency.Models, OAI.PartitionConsistency.TransitiveSets.E, OAI.PartitionConsistency.SetLanguage.ZF, OAI.PartitionConsistency.Formula.Realize, OAI.PartitionConsistency.SetLanguage.emptySet
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.symmetricValues_pairing line 465
Source documentation
Pairing holds with the actual ground pairing-name code as witness.
```
theorem symmetricValues_pairing {M : Set ZFSet.{u}}
    (hM : TransitiveSets.IsTransitive M) (hZF : Models (TransitiveSets.E M) SetLanguage.ZF)
    {F : Set (Subgroup Γ)} (hF : SupportFilter.IsNormalFilter F) {G : Set ZFSet.{u}}
    {t : ZFSet.{u}} (ht : t ∈ S.conditions) (htM : t ∈ M) (htG : t ∈ G)
    (hfixed : ∀ g : Γ, S.actCode g t = t) :
    Formula.Realize (TransitiveSets.E (S.symmetricValues M F G)) Fin.elim0
      SetLanguage.pairing := by
…
```
Mentions: OAI.PartitionConsistency.TransitiveSets.IsTransitive, OAI.PartitionConsistency.Models, OAI.PartitionConsistency.TransitiveSets.E, OAI.PartitionConsistency.SetLanguage.ZF, OAI.PartitionConsistency.SupportFilter.IsNormalFilter, OAI.PartitionConsistency.Formula.Realize, OAI.PartitionConsistency.SetLanguage.pairing