OrbitNames.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

OrderedPair

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.smul_pair line 15
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.opair line 21
Source documentation
The equivariant name for the actual Kuratowski pair.
```
def Name.opair {S : SymmetricSystem.{u} P Γ} (σ τ : S.Name) : S.Name := (σ.pair σ).pair (σ.pair τ)
```
Mentions: OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.pair
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.smul_opair line 23
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mem_pair_left line 26
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mem_pair_right line 29
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.eq_pair_congr line 32
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mem_singleton line 50
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.eq_pair_singleton line 61
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.eq_pair_cancel_left line 71
Source documentation
Cancellation for unordered pairs with a common first entry.
```
theorem eq_pair_cancel_left {p : P} {σ τ ν : S.Name}
    (he : S.atomic.EqF p (σ.pair τ) (σ.pair ν)) : S.atomic.EqF p τ ν := by
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.eq_opair_congr line 82
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.eq_opair_iff line 89
Source documentation
Injectivity of ordered-pair names is a forcing theorem, not an assumption on the name quotient.
```
theorem eq_opair_iff {p : P} {σ σ' τ τ' : S.Name} :
    S.atomic.EqF p (σ.opair τ) (σ'.opair τ') ↔
      S.atomic.EqF p σ σ' ∧ S.atomic.EqF p τ τ' := by
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_unorderedPair line 110
Source documentation
The pure first-order unordered-pair formula agrees with the canonical name.
```
theorem forces_unorderedPair {n} (v : Fin n → S.Name) (p : P) (a x y : Fin n) :
    S.Forces v p (SetLanguage.unorderedPair a x y) ↔
      S.atomic.EqF p (v a) ((v x).pair (v y)) := by
…
```
Mentions: OAI.PartitionConsistency.SetLanguage.unorderedPair
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_orderedPair line 134
Source documentation
The pure first-order Kuratowski-pair formula agrees with the canonical name.
```
theorem forces_orderedPair {n} (v : Fin n → S.Name) (p : P) (a x y : Fin n) :
    S.Forces v p (SetLanguage.orderedPair a x y) ↔
      S.atomic.EqF p (v a) ((v x).opair (v y)) := by
…
```
Mentions: OAI.PartitionConsistency.SetLanguage.orderedPair
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.app_iff_mem_opair line 154
Source documentation
Internal application is literal membership of the Kuratowski-pair name.
```
theorem app_iff_mem_opair (p : P) (f x y : S.Name) :
    S.App p f x y ↔ S.atomic.MemF p (x.opair y) f := by
…
```

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mem_collect line 182

Source documentation

The forcing membership value of an arbitrary collected family. The index type, not the ranks of its entries, is required to be small.

theorem mem_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) (p : P) :
    S.atomic.MemF p ν (S.collect f R H hH permutes) ↔
      ∀ q, q ≤ p → ∃ r, r ≤ q ∧ ∃ i a, R i a ∧ r ≤ a ∧ S.atomic.EqF r ν (f i) := by
…

theorem OAI.PartitionConsistency.DiagramForcing.Diagram.eq_of_compatible_centers line 209
Source documentation
Compatible diagrams with the same center agree pointwise. This is the functional feature of diagram forcing used by the name-orbit presentation.
```
theorem eq_of_compatible_centers {r p q : Diagram M I}
    (hrp : r ≤ p) (hrq : r ≤ q) (hcenter : p 1 = q 1) : p = q := by
…
```
Mentions: OAI.PartitionConsistency.DiagramForcing.Diagram
theorem OAI.PartitionConsistency.CohenForcing.Condition.permute_top line 222
theorem OAI.PartitionConsistency.ProductForcing.smul_name_eq_of_diagram_eq line 238
Source documentation
Ordinary names in an orbit agree literally when their supporting diagrams do. This does not define an action on an evaluated symmetric model.
```
theorem smul_name_eq_of_diagram_eq
    (σ : (system (M := M) (I := I) (κ := κ) hμ).Name) (p : Diagram M I)
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system
def OAI.PartitionConsistency.ProductForcing.orbitGraph line 254
Source documentation
The invariant graph of the partial name-orbit map in eq:partial-orbit-map. Each entry is activated by its actual moved diagram.
```
def orbitGraph (c : κ → ZFSet.{u})
    (σ : (system (M := M) (I := I) (κ := κ) hμ).Name) (p : Diagram M I) :
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.smul_orbitGraph line 268
theorem OAI.PartitionConsistency.ProductForcing.mem_orbitGraph line 283
Source documentation
Complete local-witness description of the partial graph, including the moved diagram that authorizes a contributed pair.
```
theorem mem_orbitGraph (c : κ → ZFSet.{u})
    (σ : (system (M := M) (I := I) (κ := κ) hμ).Name) (p : Diagram M I)
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.app_orbitGraph line 294
Source documentation
Application is computed by actual contributed input-output pairs.
```
theorem app_orbitGraph (c : κ → ZFSet.{u})
    (σ : (system (M := M) (I := I) (κ := κ) hμ).Name) (p : Diagram M I)
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.orbitGraph_app_self line 307
Source documentation
The identity copy maps the label at the supporting diagram's center to the original arbitrary-rank name.
```
theorem orbitGraph_app_self (c : κ → ZFSet.{u})
    (σ : (system (M := M) (I := I) (κ := κ) hμ).Name) (p : Diagram M I) :
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.orbitGraph_input line 319
Source documentation
All contributed inputs lie in the one invariant label set.
```
theorem orbitGraph_input (c : κ → ZFSet.{u})
    (σ : (system (M := M) (I := I) (κ := κ) hμ).Name) (p : Diagram M I)
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.orbitGraph_unique line 331
Source documentation
The graph is forced single-valued. Its two contributing diagrams are compared only below a common condition, never by moving a fixed generic.
```
theorem orbitGraph_unique [Uncountable κ] (c : κ → ZFSet.{u})
    (hc : Function.Injective c)
    (σ : (system (M := M) (I := I) (κ := κ) hμ).Name) (p : Diagram M I)
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system