ProductNames.lean`

46 declarations, 0 contain sorry, 0 declared as axioms

ProductSystem

def OAI.PartitionConsistency.SetForcingNames.posetCode line 15
Source documentation
A genuine small set of condition codes, obtained by wellordering the condition type. The codes carry no forcing or satisfaction information.
```
def posetCode (P : Type u) (p : P) : ZFSet.{u} :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.posetCode_injective line 18
def OAI.PartitionConsistency.SetForcingNames.conditionSet line 21
def OAI.PartitionConsistency.SetForcingNames.conditionEquiv line 23
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.codedAction line 35
Source documentation
Conjugating an honest order action by the coding equivalence.
```
def codedAction : ConditionAction.{u} Γ where
…
```
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.ofOrderAction line 42
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.move_ofOrderAction line 53
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.code_ofOrderAction line 58
abbrev OAI.PartitionConsistency.ProductForcing.Poset line 72
Source documentation
The paper explicitly allows adjoining a fixed largest condition.
```
abbrev Poset (M I κ : Type u) := WithTop (Condition M I κ)
```
Mentions: OAI.PartitionConsistency.ProductForcing.Condition
def OAI.PartitionConsistency.ProductForcing.actionHom line 74
def OAI.PartitionConsistency.ProductForcing.system line 89
Source documentation
The literal Cohen/diagram symmetric system, with exactly the small-support subgroup filter. Neither ZF nor any target axiom is a structure field.
```
def system {μ : Cardinal.{u}} (hμ : Cardinal.aleph0 ≤ μ) :
    SymmetricSystem.{u} (Poset M I κ) (Equiv.Perm I) :=
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.Poset
theorem OAI.PartitionConsistency.ProductForcing.move_coe line 96
theorem OAI.PartitionConsistency.ProductForcing.move_top line 101
theorem OAI.PartitionConsistency.ProductForcing.forces_ZF line 107
Source documentation
Full ZF follows from the already proved unbounded HS-name theorem for this actual action and filter. This is not a proof of the extra axioms.
```
theorem forces_ZF (p : Poset M I κ) :
    ∀ φ ∈ SetLanguage.ZF, (system hμ).Forces Fin.elim0 p φ :=
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.Poset, OAI.PartitionConsistency.SetLanguage.ZF, OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.name_support line 112
Source documentation
Each HS name has a literal support of size at most the prescribed bound.
```
theorem name_support (σ : (system (M := M) (I := I) (κ := κ) hμ).Name) :
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.smul_check line 131
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.eq_check_iff line 138
Source documentation
Check names reflect ground equality at every condition. This uses well-foundedness of actual sets, and does not presume a generic extension.
```
theorem eq_check_iff (x y : ZFSet.{u}) (p : P) :
    S.atomic.EqF p (Name.check x) (Name.check y) ↔ x = y := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.check
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mem_check_check line 161

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.collectRaw_move line 170

Source documentation

Exact transport of a set-sized collected entry family.

theorem collectRaw_move {ι : Type t} [Small.{u} ι]
    (f f' : ι → S.Name) (R R' : ι → P → Prop) (g : Γ) (e : Equiv.Perm ι)
    (hf : ∀ i, g • f i = f' (e i))
    (hR : ∀ i p, R i p ↔ R' (e i) (S.move g p)) :
    mapConditions (S.action.actCode g) (S.collectRaw f R) = S.collectRaw f' R' := by
…

Mentions: OAI.PartitionConsistency.SetForcingNames.mapConditions

def OAI.PartitionConsistency.ProductForcing.Bit line 205
Source documentation
The Boolean assignment actually contained in a product condition. The adjoined top condition supplies no assignment.
```
def Bit (p : Poset M I κ) (j : I) (α : κ) (b : Bool) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.Poset
theorem OAI.PartitionConsistency.ProductForcing.bit_coe line 209
theorem OAI.PartitionConsistency.ProductForcing.not_bit_top line 215
theorem OAI.PartitionConsistency.ProductForcing.bit_mono line 218
theorem OAI.PartitionConsistency.ProductForcing.bit_functional line 227
theorem OAI.PartitionConsistency.ProductForcing.bit_move line 232
def OAI.PartitionConsistency.ProductForcing.label line 241
Source documentation
An index is coded by an actual ground set (eventually a ground ordinal). At coordinate j the name has precisely the positively assigned indices.
```
def label (c : κ → ZFSet.{u}) (j : I) : (system (M := M) (I := I) (κ := κ) hμ).Name :=
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.label_raw line 250
theorem OAI.PartitionConsistency.ProductForcing.smul_label line 254
theorem OAI.PartitionConsistency.ProductForcing.mem_label_of_bit line 263
Source documentation
Positive bits force their ground indices into the named label.
```
theorem mem_label_of_bit (c : κ → ZFSet.{u}) {j : I} {α : κ} {p : Poset M I κ}
    (hb : Bit p j α true) : (system (M := M) (I := I) (κ := κ) hμ).atomic.MemF p (Name.check (c α)) (label (M := M) hμ c j) := by
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.Poset, OAI.PartitionConsistency.ProductForcing.Bit, OAI.PartitionConsistency.ProductForcing.system, OAI.PartitionConsistency.ProductForcing.label
theorem OAI.PartitionConsistency.ProductForcing.mem_label line 270
Source documentation
The complete local-witness membership characterization of a canonical label.
```
theorem mem_label (c : κ → ZFSet.{u}) (j : I) (ν : (system (M := M) (I := I) (κ := κ) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.not_mem_label_of_bit line 292
Source documentation
Negative bits force nonmembership; injectivity here is injectivity of the ordinary ground-coordinate coding, not an assumed distinctness of labels.
```
theorem not_mem_label_of_bit (c : κ → ZFSet.{u}) (hc : Function.Injective c)
    {j : I} {α : κ} {p : Poset M I κ} (hb : Bit p j α false) :
    ¬ (system (M := M) (I := I) (κ := κ) hμ).atomic.MemF p (Name.check (c α)) (label (M := M) hμ c j) := by
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.Poset, OAI.PartitionConsistency.ProductForcing.Bit, OAI.PartitionConsistency.ProductForcing.system, OAI.PartitionConsistency.ProductForcing.label
theorem OAI.PartitionConsistency.ProductForcing.label_not_equal line 304
Source documentation
Distinct index coordinates give forced-distinct actual set names, below every product condition.
```
theorem label_not_equal [Uncountable κ] (c : κ → ZFSet.{u})
    (hc : Function.Injective c) [Nonempty (DiagramForcing.Diagram M I)]
    {j k : I} (hjk : j ≠ k) (p : Poset M I κ) :
    ¬ (system (M := M) (I := I) (κ := κ) hμ).atomic.EqF p (label (M := M) hμ c j) (label (M := M) hμ c k) := by
…
```
Mentions: OAI.PartitionConsistency.DiagramForcing.Diagram, OAI.PartitionConsistency.ProductForcing.Poset, OAI.PartitionConsistency.ProductForcing.system, OAI.PartitionConsistency.ProductForcing.label
def OAI.PartitionConsistency.ProductForcing.labelSet line 324
Source documentation
The invariant set of all canonical generic labels.
```
def labelSet (c : κ → ZFSet.{u}) : (system (M := M) (I := I) (κ := κ) hμ).Name :=
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.labelSet_raw line 330
theorem OAI.PartitionConsistency.ProductForcing.smul_labelSet line 334
theorem OAI.PartitionConsistency.ProductForcing.label_mem_labelSet line 347
theorem OAI.PartitionConsistency.ProductForcing.mem_labelSet line 353
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.App line 384
Source documentation
Application is the forcing of the literal internal ordered-pair graph formula. It does not replace a set function by an external function.
```
def App (p : P) (f x y : S.Name) : Prop :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_edge line 387
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.app_mono line 395
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.app_congr line 398
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.app_symmetry line 405

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.functionOn_total line 411

Source documentation

The totality/uniqueness conjunct of the internal set-function sentence.

theorem functionOn_total {n} (v : Fin n → S.Name) (p : P) (f d : Fin n)
    (hf : S.Forces v p (SetLanguage.functionOn f d))
    (x : S.Name) {q : P} (hqp : q ≤ p) (hx : S.atomic.MemF q x (v d)) :
    ∀ r, r ≤ q → ∃ s, s ≤ r ∧ ∃ y : S.Name, S.App s (v f) x y ∧
      ∀ z : S.Name, ∀ t, t ≤ s → S.App t (v f) x z → S.atomic.EqF t z y := by
…

Mentions: OAI.PartitionConsistency.SetLanguage.functionOn

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.functionOn_unique line 424

Source documentation

Forced single-valuedness, with three unrestricted HS names as arguments.

theorem functionOn_unique {n} (v : Fin n → S.Name) (p : P) (f d : Fin n)
    (hf : S.Forces v p (SetLanguage.functionOn f d))
    (x y z : S.Name) (hx : S.atomic.MemF p x (v d))
    (hy : S.App p (v f) x y) (hz : S.App p (v f) x z) : S.atomic.EqF p y z := by
…

Mentions: OAI.PartitionConsistency.SetLanguage.functionOn

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_nonempty line 434

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_choiceOn line 442

Source documentation

Unpacking a choice function retains exactly the original graph formula.

theorem forces_choiceOn {n} (v : Fin n → S.Name) (p : P) (c a : Fin n) :
    S.Forces v p (SetLanguage.choiceOn c a) ↔
      S.Forces ![v c,v a] p (SetLanguage.functionOn 0 1) ∧
      ∀ x : S.Name, ∀ q, q ≤ p → S.atomic.MemF q x (v a) →
        ∀ r, r ≤ q → ∃ s, s ≤ r ∧ ∃ y : S.Name,
          S.App s (v c) x y ∧ S.atomic.MemF s y x := by
…

Mentions: OAI.PartitionConsistency.SetLanguage.choiceOn, OAI.PartitionConsistency.SetLanguage.functionOn