OAI/SetTheory/PartitionConsistency/Models/ClassFibers.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

LocalList

  1. def OAI.PartitionConsistency.SetLanguage.wellorderableFormula line 12

    Source documentation

    A set is wellorderable exactly when it embeds in some ordinal. Both quantified witnesses are internal sets; the injection is an internal graph.

    def wellorderableFormula : Formula 1 :=
…

    Mentions: OAI.PartitionConsistency.Formula

  2. def OAI.PartitionConsistency.SetLanguage.wellorderable line 15
  3. theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_wellorderable line 27
  4. theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.wellorderable_of_check_injection line 65

    Source documentation

    Injecting a set into a checked ordinal is enough for the genuine wellorderability formula. No ordinal preservation assumption is used.

    theorem wellorderable_of_check_injection (Y J : S.Name) (α : Ordinal.{u}) (p : P)
    (h : S.Forces ![J,Y,Name.check α.toZFSet] p (SetLanguage.injection 0 1 2)) :
    S.Forces ![Y] p (SetLanguage.wellorderable 0) := by
…

    Mentions: OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.check, OAI.PartitionConsistency.SetLanguage.injection, OAI.PartitionConsistency.SetLanguage.wellorderable

  5. theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.no_check_injection_of_not_wellorderable line 73
  6. def OAI.PartitionConsistency.ProductForcing.quotientName line 93

    Source documentation

    The range of all canonical E-classes of labels. For an equivalence relation this is A/E, with the actual classes as its members.

    def quotientName (E : (system (M := M) (I := I) (κ := κ) hμ).Name) :
…

    Mentions: OAI.PartitionConsistency.ProductForcing.system

  7. theorem OAI.PartitionConsistency.ProductForcing.mem_quotientName line 102
  8. theorem OAI.PartitionConsistency.ProductForcing.mem_quotientName_iff_isClass line 118

    Source documentation

    Membership is exactly the first-order class predicate, not a quotient surrogate supplied with the desired comparison property.

    theorem mem_quotientName_iff_isClass
    (E y : (system (M := M) (I := I) (κ := κ) hμ).Name) (p : Poset M I κ) :
…

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

  9. theorem OAI.PartitionConsistency.ProductForcing.quotientName_fixed line 134
  10. def OAI.PartitionConsistency.ProductForcing.localListOrdinal line 149

    Source documentation

    A ground ordinal enumerating the entire normalized local-name set.

    def localListOrdinal (r : Diagram M I) : Ordinal.{u} :=
…
  11. def OAI.PartitionConsistency.ProductForcing.localListEquiv line 152
  12. def OAI.PartitionConsistency.ProductForcing.localListEntry line 156
  13. theorem OAI.PartitionConsistency.ProductForcing.localListEntry_fixed line 159
  14. theorem OAI.PartitionConsistency.ProductForcing.localList_support line 164
  15. def OAI.PartitionConsistency.ProductForcing.localList line 170

    Source documentation

    The canonical evaluation list range, formed as a genuine HS name with support D_r; its domain has been enumerated by a ground ordinal.

    def localList (hcard : Cardinal.mk M ≤ μ) (r : Diagram M I) :
    (system (M := M) (I := I) (κ := κ) hμ).Name :=
…

    Mentions: OAI.PartitionConsistency.ProductForcing.system

  16. theorem OAI.PartitionConsistency.ProductForcing.localList_fixed line 180
  17. theorem OAI.PartitionConsistency.ProductForcing.mem_localList line 188
  18. theorem OAI.PartitionConsistency.ProductForcing.localName_mem_localList line 204
  19. theorem OAI.PartitionConsistency.ProductForcing.localList_wellorderable line 212

    Source documentation

    The list is wellorderable inside the symmetric interpretation, via its least-occurrence injection into its checked index ordinal.

    theorem localList_wellorderable (hcard : Cardinal.mk M ≤ μ) (r : Diagram M I)
    (p : Poset M I κ) :
    (system hμ).Forces ![localList hμ c hcard r] p (SetLanguage.wellorderable 0) :=
…

    Mentions: OAI.PartitionConsistency.ProductForcing.Poset, OAI.PartitionConsistency.ProductForcing.system, OAI.PartitionConsistency.ProductForcing.localList, OAI.PartitionConsistency.SetLanguage.wellorderable

  20. theorem OAI.PartitionConsistency.ProductForcing.outside_localList line 224

    Source documentation

    Nonwellorderability supplies densely an actual E-class outside every value on the local evaluation list. Nonmembership persists below the chosen condition; it is not just a failure to decide membership.

    theorem outside_localList (hcard : Cardinal.mk M ≤ μ) (r : Diagram M I)
    (E : (system (M := M) (I := I) (κ := κ) hμ).Name)
…

    Mentions: OAI.PartitionConsistency.ProductForcing.system

  21. def OAI.PartitionConsistency.ProductForcing.outsideClassSet line 255

    Source documentation

    A class outside the entire local-name evaluation list, decided in a literal stronger diagram that also contains all the condition coordinates. The right factor of the root is recorded and is necessarily nontrivial.

    def outsideClassSet (hcard : Cardinal.mk M ≤ μ) (p : Diagram M I)
    (E : (system (M := M) (I := I) (κ := κ) hμ).Name) :
…

    Mentions: OAI.PartitionConsistency.ProductForcing.system

  22. theorem OAI.PartitionConsistency.ProductForcing.outsideClassSet_denseBelow line 265

    Source documentation

    This is a local dense-set theorem derived from nonwellorderability, not an additional assumption that the unavailable class exists.

    theorem outsideClassSet_denseBelow [Infinite M] [Infinite I]
    (hcard : Cardinal.mk M ≤ μ) (hsize : Cardinal.mk M < Cardinal.mk I) (e : M)
    (he : Cardinal.mk ((Set.range (fun x : M => e*x))ᶜ : Set M) = Cardinal.mk M)
    (p : Diagram M I) (E : (system (M := M) (I := I) (κ := κ) hμ).Name)
…

    Mentions: OAI.PartitionConsistency.ProductForcing.system

  23. def OAI.PartitionConsistency.ProductForcing.outsideClassDenseSet line 311

    Source documentation

    The standard incompatible padding gives a dense set in the whole Cohen forcing. This is the precise requirement to be met by the intermediate ordinary extension.

    def outsideClassDenseSet (hcard : Cardinal.mk M ≤ μ) (p : Diagram M I)
    (E : (system (M := M) (I := I) (κ := κ) hμ).Name) (d₀ : CohenForcing.Condition I κ) :
…

    Mentions: OAI.PartitionConsistency.ProductForcing.system, OAI.PartitionConsistency.CohenForcing.Condition

  24. theorem OAI.PartitionConsistency.ProductForcing.outsideClassDenseSet_dense line 316
  25. theorem OAI.PartitionConsistency.ProductForcing.outsideClass_of_meets line 331

    Source documentation

    An actual hit supplies the nontrivial witness used in the probe argument. Only the explicitly identified dense set is mentioned here; this lemma does not posit existence of an ambient filter meeting every ambient dense set.

    theorem outsideClass_of_meets (hcard : Cardinal.mk M ≤ μ)
    (F : GenericFilter (CohenForcing.Condition I κ)) (p : Diagram M I)
    (E : (system (M := M) (I := I) (κ := κ) hμ).Name)
…

    Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system

  26. def OAI.PartitionConsistency.ProductForcing.OutsideLocal line 357

    Source documentation

    Persistent exclusion from the evaluation list of all local names at p. This statement is expressed in the actual symmetric forcing relation.

    def OutsideLocal (hcard : Cardinal.mk M ≤ μ) (p s : Diagram M I)
    (d : CohenForcing.Condition I κ) (σ : LocalName hμ c s) : Prop :=
…

    Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.LocalName

  27. theorem OAI.PartitionConsistency.ProductForcing.outsideLocal_not_image line 365

    Source documentation

    A class outside the full evaluation list cannot be the inclusion of any local quotient element at that root. Only membership of its witnessing condition in the filter is used here.

    theorem outsideLocal_not_image (hcard : Cardinal.mk M ≤ μ)
    (F : GenericFilter (CohenForcing.Condition I κ)) (p s : Diagram M I)
    (hsp : s ≤ p) (d : CohenForcing.Condition I κ) (hd : d ∈ F)
    (σ : LocalName hμ c s) (hout : OutsideLocal hμ c hcard p s d σ)
    (x : LocalQuotient (c := c) hμ F p) :
…

    Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.LocalName, OAI.PartitionConsistency.ProductForcing.OutsideLocal, OAI.PartitionConsistency.ProductForcing.LocalQuotient

  28. theorem OAI.PartitionConsistency.ProductForcing.outsideLocal_not_equal line 388

    Source documentation

    Support descent over an exact intersection prevents an outside class from equaling any element supported by the other diagram.

    theorem outsideLocal_not_equal [Infinite M] [Infinite I]
    (hcard : Cardinal.mk M ≤ μ) (hsize : Cardinal.mk M < Cardinal.mk I)
    (hmerger : HasFiniteMergers M) (F : GenericFilter (CohenForcing.Condition I κ))
    (p s₀ s₁ v : Diagram M I) (hs₀ : s₀ ≤ p) (hs₁ : s₁ ≤ p)
    (hinter : s₀.range ∩ s₁.range = p.range) (hv₀ : v ≤ s₀) (hv₁ : v ≤ s₁)
    (d : CohenForcing.Condition I κ) (hd : d ∈ F) (σ : LocalName hμ c s₀)
    (hout : OutsideLocal hμ c hcard p s₀ d σ)
    (y : LocalQuotient (c := c) hμ F s₁) :
…

    Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.LocalName, OAI.PartitionConsistency.ProductForcing.OutsideLocal, OAI.PartitionConsistency.ProductForcing.LocalQuotient

  29. def OAI.PartitionConsistency.ProductForcing.classFromLocal line 405

    Source documentation

    A supported eligible class at any subdiagram gives a genuine element of D_F(r), even when that subdiagram is not itself below q.

    def classFromLocal [Infinite M] [Infinite I]
    (hcard : Cardinal.mk M ≤ μ) (hsize : Cardinal.mk M < Cardinal.mk I)
    (hmerger : HasFiniteMergers M) (F : GenericFilter (CohenForcing.Condition I κ))
    (q r s : Diagram M I) (hrq : r ≤ q) (hrs : r ≤ s)
    (E : (system (M := M) (I := I) (κ := κ) hμ).Name)
…

    Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system

  30. theorem OAI.PartitionConsistency.ProductForcing.classFromLocal_profile line 419

    Source documentation

    The exact profile for a class on one probe. The positive availability comes from retaining the name on larger ranges; the negative test is the actual support-descent contradiction, not a multiplicity assumption.

    theorem classFromLocal_profile [Infinite M] [Infinite I]
    (hcard : Cardinal.mk M ≤ μ) (hsize : Cardinal.mk M < Cardinal.mk I)
    (hmerger : HasFiniteMergers M) (F : GenericFilter (CohenForcing.Condition I κ))
    (q r p : Diagram M I) (a e m b : M) (hqa : r.sub a = q)
    (hp : r.sub (a*e) = p) (hmb : m*b = a*e)
    (U : ConeIdeal (show LeftDivOrder M from a))
    (hm : ∀ n : M, n ∣ a ∧ n ∣ m ↔ n ∈ U.carrier)
    (hinter : ∀ n : M, n ∣ a → n ∉ U.carrier →
      ∀ z : M, n ∣ z ∧ m ∣ z ↔ a*e ∣ z)
    (E : (system (M := M) (I := I) (κ := κ) hμ).Name)
…

    Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system

  31. def OAI.PartitionConsistency.ProductForcing.classFiberEmbedding line 470

    Source documentation

    Distinct hit probes yield distinct symbolic classes, all in the exact specified fiber. This map uses actual names, actual forcing eligibility, and the proved intersection theorem.

    def classFiberEmbedding [Infinite M] [Infinite I]
    (hcard : Cardinal.mk M ≤ μ) (hsize : Cardinal.mk M < Cardinal.mk I)
    (hmerger : HasFiniteMergers M) (F : GenericFilter (CohenForcing.Condition I κ))
    {q : Diagram M I} (w : Vertex q) (p : Diagram M I) (e b : M)
    (hp : w.diagram.sub (w.index*e) = p) {K : Type u} (m : K → M)
    (hmb : ∀ i, m i*b = w.index*e)
    (hm : ∀ i (n : M), n ∣ w.index ∧ n ∣ m i ↔ n ∈ w.ideal.carrier)
    (hinter : ∀ i (n : M), n ∣ w.index → n ∉ w.ideal.carrier →
      ∀ z : M, n ∣ z ∧ m i ∣ z ↔ w.index*e ∣ z)
    (hind : ∀ i j, i ≠ j → ∀ z : M, m i ∣ z ∧ m j ∣ z ↔ w.index*e ∣ z)
    (E : (system (M := M) (I := I) (κ := κ) hμ).Name)
…

    Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system

  32. theorem OAI.PartitionConsistency.ProductForcing.outsideClass_copies line 508

    Source documentation

    Transport the actual outside label-class witness to all copies of its diagram over p. The names remain normalized names in the stated local sets, and their exclusions are forced at the transported conditions.

    theorem outsideClass_copies (hcard : Cardinal.mk M ≤ μ)
    (hsize : Cardinal.mk M < Cardinal.mk I) (p r : Diagram M I) (a e b : M)
    (hp : r.sub (a*e) = p) {K : Type u} (m : K → M) (hm : ∀ i, m i*b = a*e)
    (E : (system (M := M) (I := I) (κ := κ) hμ).Name)
…

    Mentions: OAI.PartitionConsistency.ProductForcing.system

  33. theorem OAI.PartitionConsistency.ProductForcing.classFiber_dense_lower line 565

    Source documentation

    A uniform family of genuinely dense Cohen requirements which forces the lower exact-fiber bound. The requirements are built from transported copies of one outside witness. Every filter meeting them has the displayed embedding; no ambient filter is presumed to meet all ambient dense sets.

    theorem classFiber_dense_lower [Infinite M] [Infinite I]
    (hcard : Cardinal.mk M ≤ μ) (hsize : Cardinal.mk M < Cardinal.mk I)
    (hmerger : HasFiniteMergers M) {q : Diagram M I} (w : Vertex q) (e b : M)
    {K : Type u} [Uncountable K] (m : K × K → M)
    (hmb : ∀ i, m i*b = w.index*e)
    (hm : ∀ i (n : M), n ∣ w.index ∧ n ∣ m i ↔ n ∈ w.ideal.carrier)
    (hinter : ∀ i (n : M), n ∣ w.index → n ∉ w.ideal.carrier →
      ∀ z : M, n ∣ z ∧ m i ∣ z ↔ w.index*e ∣ z)
    (hind : ∀ i j, i ≠ j → ∀ z : M, m i ∣ z ∧ m j ∣ z ↔ w.index*e ∣ z)
    (E : (system (M := M) (I := I) (κ := κ) hμ).Name)
…

    Mentions: OAI.PartitionConsistency.ProductForcing.system