SymmetricNames.lean`

54 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.PartitionConsistency.SetForcingNames.SymmetricSystem line 13
Source documentation
A set symmetric system with a named presentation of the conditions. Every piece of data is algebraic: no forcing axiom or satisfaction assertion is included in this structure. The equivalence also ensures that the poset is a set in the same universe as the literal name codes.
```
structure SymmetricSystem (P : Type w) [Preorder P] (Γ : Type v) [Group Γ] where
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.small_conditions line 26
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.code line 29
Source documentation
The actual set code, not a semantic truth value.
```
def code (p : P) : ZFSet.{u} := (S.codeEquiv p).val
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.code_mem line 31
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.code_injective line 33
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.move line 37
Source documentation
Automorphisms of the poset obtained from its coded action.
```
noncomputable def move (g : Γ) : P ≃o P where
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.actCode_code line 41
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name line 49
Source documentation
All hereditarily symmetric names, without any fixed bound on ranks.
```
def Name := {σ : S.action.Name // ConditionAction.Name.HS S.filter σ}
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.HS
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.raw line 54
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.ext line 56
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.isName line 59
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.hs line 61
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.child line 64
Source documentation
An active entry is automatically HS by hereditary symmetry.
```
def child (σ : S.Name) {ρ c : ZFSet.{u}} (he : ZFSet.pair ρ c ∈ σ.raw) : S.Name :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.child_val line 67
instance OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.(instance at line 70) line 70
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.smul_val line 75
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.empty line 78
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.empty_val line 81
instance OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.(instance at line 83) line 83
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.atomic line 89
Source documentation
The previously constructed recursive atomic relations, restricted to the actual HS class of this set symmetric system.
```
noncomputable def atomic : ForcingQuotient.AtomicData P S.Name where
…
```
Mentions: OAI.PartitionConsistency.ForcingQuotient.AtomicData
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.atomic_regular line 99
abbrev OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Forces line 104
Source documentation
Named formula forcing in this symmetric system. Quantifiers range over all HS names; the existential clause remains density of local witnesses.
```
abbrev Forces {n} (v : Fin n → S.Name) (p : P) (φ : Formula n) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.Formula
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_symmetry line 108
Source documentation
Full formula symmetry for the concrete HS class.
```
theorem forces_symmetry (g : Γ) {n} (φ : Formula n) (v : Fin n → S.Name) (p : P) :
    S.Forces v p φ ↔ S.Forces (fun i => g • v i) (S.move g p) φ := by
…
```
Mentions: OAI.PartitionConsistency.Formula
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.consistent_of_forces line 121
Source documentation
Ordinary syntactic consistency follows if all axioms of a theory are forced. This result does not assert the forcing of PP, ACwo, or failure of Choice. In particular it is not the selected main theorem.
```
theorem consistent_of_forces {T : Theory} (p : P)
    (hT : ∀ φ ∈ T, S.Forces Fin.elim0 p φ) : Consistent T :=
…
```
Mentions: OAI.PartitionConsistency.Theory, OAI.PartitionConsistency.Consistent

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mem_iff line 136

Source documentation

Active members of an HS name are in the same quantifier domain.

theorem mem_iff {p : P} {ν σ : S.Name} : S.atomic.MemF p ν σ ↔
    ∀ q, q ≤ p → ∃ r, r ≤ q ∧ ∃ (τ : S.Name) (c : P),
      ZFSet.pair τ.raw (S.code c) ∈ σ.raw ∧ r ≤ c ∧ S.atomic.EqF r ν τ := by
…

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mem_of_edge line 149
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.eq_of_same_members line 155
Source documentation
Extensionality is proved from the recursive definition of equality, not assumed as another law of a forcing algebra.
```
theorem eq_of_same_members {p : P} {σ τ : S.Name}
    (h : ∀ ν : S.Name, ∀ q, q ≤ p → (S.atomic.MemF q ν σ ↔ S.atomic.MemF q ν τ)) :
    S.atomic.EqF p σ τ := by
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.not_mem_empty line 165
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.minimal_member line 173
Source documentation
A local minimal-member witness obtained by genuine well-founded induction on literal names. No generic filter or external well-foundedness of a model is used in this lemma.
```
theorem minimal_member (σ ν : S.Name) (p : P) (hmem : S.atomic.MemF p ν σ) :
    ∃ q, q ≤ p ∧ ∃ τ : S.Name, S.atomic.MemF q τ σ ∧
      ∀ ρ : S.Name, ∀ r, r ≤ q → S.atomic.MemF r ρ τ → ¬ S.atomic.MemF r ρ σ := by
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_extensionality line 189
Source documentation
The schema's Extensionality instance.
```
theorem forces_extensionality (p : P) : S.Forces Fin.elim0 p SetLanguage.extensionality := by
…
```
Mentions: OAI.PartitionConsistency.SetLanguage.extensionality
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_emptySet line 199
Source documentation
The schema's Empty Set instance.
```
theorem forces_emptySet (p : P) : S.Forces Fin.elim0 p SetLanguage.emptySet := by
…
```
Mentions: OAI.PartitionConsistency.SetLanguage.emptySet
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_foundation line 210
Source documentation
The schema's Foundation instance, uniformly at every condition.
```
theorem forces_foundation (p : P) : S.Forces Fin.elim0 p SetLanguage.foundation := by
…
```
Mentions: OAI.PartitionConsistency.SetLanguage.foundation
theorem OAI.PartitionConsistency.SetForcingNames.mapConditions_mono line 231
Source documentation
Transport of the immediate membership graph preserves inclusions.
```
theorem mapConditions_mono (f : ZFSet.{u} → ZFSet.{u}) {σ τ : ZFSet.{u}} (h : σ ⊆ τ) :
    mapConditions f σ ⊆ mapConditions f τ := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.mapConditions
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.collectRaw line 242
Source documentation
A small family of HS names with any predicate on its entry conditions.
```
noncomputable def collectRaw {ι : Type t} [Small.{u} ι] (f : ι → S.Name)
    (R : ι → P → Prop) : ZFSet.{u} := by
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mem_collectRaw line 248
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.edge_collectRaw line 259
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.isName_collectRaw line 265
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.collectName line 272

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.collect_HS line 277

Source documentation

Permuting the entry family fixes its literal set of pairs. This lemma contains no coherence or forcing premise.

theorem collect_HS {ι : Type t} [Small.{u} ι] (f : ι → S.Name) (R : ι → P → Prop)
    (H : Subgroup Γ) (hH : H ∈ S.filter)
    (permutes : ∀ g ∈ H, ∀ i p, R i p → ∃ j,
      f j = g • f i ∧ R j (S.move g p)) :
    ConditionAction.Name.HS S.filter (S.collectName f R) := by
…

Mentions: OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.HS

def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.collect line 306

Source documentation

The collected name is packaged with the proved hereditary symmetry.

noncomputable def collect {ι : Type t} [Small.{u} ι] (f : ι → S.Name) (R : ι → P → Prop)
    (H : Subgroup Γ) (hH : H ∈ S.filter)
    (permutes : ∀ g ∈ H, ∀ i p, R i p → ∃ j,
      f j = g • f i ∧ R j (S.move g p)) : S.Name :=
…

def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.tupleStabilizer line 313

Source documentation

Finite tuples have a common subgroup in the given normal filter.

noncomputable def tupleStabilizer : {n : ℕ} → (Fin n → S.Name) → Subgroup Γ
  | 0, _ => ⊤
  | n+1, v => tupleStabilizer (fun i => v i.castSucc) ⊓ MulAction.stabilizer Γ (v (Fin.last n)).val

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.tupleStabilizer_mem line 317
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mem_tupleStabilizer line 322
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mem_symmetry line 337
Source documentation
Atomic symmetry, explicitly in the HS-name domain used by all quantifiers.
```
theorem mem_symmetry (g : Γ) (p : P) (σ τ : S.Name) :
    S.atomic.MemF p σ τ ↔ S.atomic.MemF (S.move g p) (g • σ) (g • τ) :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.eq_symmetry line 342
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.forceFormula_close line 355
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_snoc_congr line 379
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.entry_permute line 389
Source documentation
Literal entry families are carried to literal entry families by the group.
```
theorem entry_permute (g : Γ) (σ : S.Name) (i : Edges σ.raw) :
    ∃ j : Edges (g • σ).raw, (g • σ).child j.property = g • σ.child i.property := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.Edges
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.separationTest line 398
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.separationTest_permute line 402
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.separate line 427
Source documentation
The Separation name for an arbitrary formula with an arbitrary finite parameter tuple. Its entries are taken only from the original name's domain.
```
noncomputable def separate {n} (σ : S.Name) (v : Fin n → S.Name)
    (φ : Formula (n+1)) : S.Name :=
…
```
Mentions: OAI.PartitionConsistency.Formula
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.edge_separate line 434
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mem_separate line 449
Source documentation
Verification of the Separation name; quantified names are unrestricted HS names, not a rank-bounded subclass.
```
theorem mem_separate {n} (σ : S.Name) (v : Fin n → S.Name) (φ : Formula (n+1))
    (ν : S.Name) (p : P) : S.atomic.MemF p ν (S.separate σ v φ) ↔
      S.atomic.MemF p ν σ ∧ S.Forces (Fin.snoc v ν) p φ := by
…
```
Mentions: OAI.PartitionConsistency.Formula
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_separation line 485
Source documentation
Every individual instance of full Separation is forced. There is no bound on the finite syntax, parameters, or ranks in this theorem.
```
theorem forces_separation {n} (φ : Formula (n+1)) (p : P) :
    S.Forces Fin.elim0 p (SetLanguage.separation φ) := by
…
```
Mentions: OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.SetLanguage.separation