ChoiceFailure.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

OutsideLabel

theorem OAI.PartitionConsistency.SupportFilter.perm_mem_iff line 13
def OAI.PartitionConsistency.ProductForcing.labelOutside line 33
Source documentation
The set of labels outside a specified small set. Every entry remains a literal Cohen label, and its support is the specified small set.
```
def labelOutside (c : κ → ZFSet.{u}) (J : Set I) (hJ : Cardinal.mk J ≤ μ) :
    (system (M := M) (I := I) (κ := κ) hμ).Name :=
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.labelOutside_raw line 42
theorem OAI.PartitionConsistency.ProductForcing.smul_labelOutside line 47
theorem OAI.PartitionConsistency.ProductForcing.label_mem_labelOutside line 62
theorem OAI.PartitionConsistency.ProductForcing.mem_labelOutside line 71
theorem OAI.PartitionConsistency.ProductForcing.labelOutside_subset line 92
def OAI.PartitionConsistency.ProductForcing.choiceFailureFamily line 103
Source documentation
The internal family P(A) minus the empty set, formed by the actual Power Set and Separation constructions. Quantified subsets have no rank bound.
```
def choiceFailureFamily (c : κ → ZFSet.{u}) :
    (system (M := M) (I := I) (κ := κ) hμ).Name :=
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.mem_choiceFailureFamily line 109
theorem OAI.PartitionConsistency.ProductForcing.labelOutside_mem_family line 119
theorem OAI.PartitionConsistency.ProductForcing.exists_condition_below line 144
Source documentation
The adjoined largest condition never prevents passing to a genuine Cohen/diagram condition.
```
theorem exists_condition_below [Nonempty (Diagram M I)] (p : Poset M I κ) :
    ∃ q : Condition M I κ, (q : Poset M I κ) ≤ p := by
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.Poset, OAI.PartitionConsistency.ProductForcing.Condition
theorem OAI.PartitionConsistency.ProductForcing.Diagram.exists_outside line 151
theorem OAI.PartitionConsistency.ProductForcing.not_choiceOn line 162
Source documentation
No HS graph can choose from all nonempty subsets of the label set. The proof moves an actual selected label, preserving both the graph's support and its particular argument, and then amalgamates compatible conditions.
```
theorem not_choiceOn [Infinite M] [Infinite I] [Uncountable κ]
    (hcard : Cardinal.mk M = μ) (hsize : Cardinal.mk M < Cardinal.mk I)
    (hmerger : HasFiniteMergers M) (e : M)
    (he : Cardinal.mk ((Set.range (fun x : M => e * x))ᶜ : Set M) = Cardinal.mk M)
    (c : κ → ZFSet.{u}) (hc : Function.Injective c)
    (f : (system (M := M) (I := I) (κ := κ) hμ).Name) (p : Poset M I κ) :
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system, OAI.PartitionConsistency.ProductForcing.Poset
theorem OAI.PartitionConsistency.ProductForcing.forces_members_nonempty line 225
Source documentation
The family in this counterexample consists of nonempty sets, at every condition and with arbitrary HS names as potential elements.
```
theorem forces_members_nonempty (c : κ → ZFSet.{u}) (p : Poset M I κ) :
    (system (M := M) (I := I) (κ := κ) hμ).Forces
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.Poset, OAI.PartitionConsistency.ProductForcing.system

theorem OAI.PartitionConsistency.ProductForcing.forces_not_AC line 241

Source documentation

The actual product symmetric system forces the negation of the encoded first-order Axiom of Choice. No rank bound or countability restriction is placed on the potential choosing graph.

theorem forces_not_AC [Infinite M] [Infinite I] [Uncountable κ]
    (hcard : Cardinal.mk M = μ) (hsize : Cardinal.mk M < Cardinal.mk I)
    (hmerger : HasFiniteMergers M) (e : M)
    (he : Cardinal.mk ((Set.range (fun x : M => e * x))ᶜ : Set M) = Cardinal.mk M)
    (c : κ → ZFSet.{u}) (hc : Function.Injective c) (p : Poset M I κ) :
    (system (M := M) (I := I) (κ := κ) hμ).Forces Fin.elim0 p SetLanguage.AC.neg := by
…

Mentions: OAI.PartitionConsistency.ProductForcing.Poset, OAI.PartitionConsistency.ProductForcing.system

theorem OAI.PartitionConsistency.ProductForcing.forces_at_supporting_root line 279
Source documentation
The direct product-forcing version of decision over a supporting root. Any assertion forced below the root is already forced at the root, with only the witnessing Cohen condition's root restriction retained. All parameters are arbitrary-rank HS names.
```
theorem forces_at_supporting_root [Infinite M] [Infinite I]
    (hsize : Cardinal.mk M < Cardinal.mk I) (hmerger : HasFiniteMergers M)
    {n} (φ : Formula n) (v : Fin n → (system (M := M) (I := I) (κ := κ) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.forces_iff_restrict line 305
Source documentation
In particular, irrelevant Cohen coordinates can be removed from a condition whose diagram supports its entire parameter tuple.
```
theorem forces_iff_restrict [Infinite M] [Infinite I]
    (hsize : Cardinal.mk M < Cardinal.mk I) (hmerger : HasFiniteMergers M)
    {n} (φ : Formula n) (v : Fin n → (system (M := M) (I := I) (κ := κ) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.incompatible_root_of_opposite line 318
Source documentation
Opposite answers about a root-supported tuple cannot have compatible Cohen restrictions to that root, regardless of their stronger diagrams.
```
theorem incompatible_root_of_opposite [Infinite M] [Infinite I]
    (hsize : Cardinal.mk M < Cardinal.mk I) (hmerger : HasFiniteMergers M)
    {n} (φ : Formula n) (v : Fin n → (system (M := M) (I := I) (κ := κ) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.ProductForcing.system