OAI/SetTheory/PartitionConsistency/Models/ConcreteSystem.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

CardinalParameters

  1. theorem OAI.PartitionConsistency.CardinalParameters.countable_bound line 16

    Source documentation

    Every countable sequence below a regular uncountable initial ordinal is strictly bounded. We use the small representative of that ordinal.

    theorem countable_bound {μ : Cardinal.{0}} (hμ : μ.IsRegular) (hω : aleph0 < μ)
    (f : ℕ → μ.ord.ToType) : ∃ a : μ.ord.ToType, ∀ n, f n < a := by
…

    Mentions: OAI.PartitionConsistency.CardinalParameters.μ

  2. theorem OAI.PartitionConsistency.CardinalParameters.succ_power_aleph0 line 31

    Source documentation

    The cardinal arithmetic used in the paper for a successor of a fixed point of countable exponentiation. This is not an inaccessible assumption.

    theorem succ_power_aleph0 {c : Cardinal.{0}} (hω : aleph0 ≤ c)
    (hc : c ^ aleph0 = c) : (Order.succ c) ^ aleph0 = Order.succ c := by
…
  3. def OAI.PartitionConsistency.CardinalParameters.μ line 61

    Source documentation

    The parameters of RC262 over the ambient choice ground.

    def μ : Cardinal.{0} := Order.succ Cardinal.continuum
  4. theorem OAI.PartitionConsistency.CardinalParameters.aleph_one_le_μ line 63
  5. theorem OAI.PartitionConsistency.CardinalParameters.aleph0_le_μ line 66
  6. theorem OAI.PartitionConsistency.CardinalParameters.μ_countable_power line 69
  7. theorem OAI.PartitionConsistency.CardinalParameters.μ_regular line 72
  8. abbrev OAI.PartitionConsistency.ConcreteSystem.K line 85

    Source documentation

    A small type of precisely the source's probe multiplicity.

    abbrev K : Type := μ.ord.ToType
  9. instance OAI.PartitionConsistency.ConcreteSystem.(instance at line 86) line 86
  10. theorem OAI.PartitionConsistency.ConcreteSystem.cardinal_K line 88
  11. def OAI.PartitionConsistency.ConcreteSystem.T line 92

    Source documentation

    The fully executed, omega-one-length saturation.

    def T : Object := Saturation.target Base.object K

    Mentions: OAI.PartitionConsistency.ConcreteSystem.K

  12. theorem OAI.PartitionConsistency.ConcreteSystem.base_cardinal_le line 94
  13. theorem OAI.PartitionConsistency.ConcreteSystem.cardinal_T line 98
  14. instance OAI.PartitionConsistency.ConcreteSystem.(instance at line 102) line 102
  15. theorem OAI.PartitionConsistency.ConcreteSystem.finiteMergers line 104
  16. theorem OAI.PartitionConsistency.ConcreteSystem.complement_cardinal line 106
  17. abbrev OAI.PartitionConsistency.ConcreteSystem.I line 117

    Source documentation

    The coordinates and Cohen length specified in the source.

    abbrev I : Type := (Order.succ μ).ord.ToType
  18. abbrev OAI.PartitionConsistency.ConcreteSystem.κ line 118
  19. theorem OAI.PartitionConsistency.ConcreteSystem.cardinal_I line 120
  20. theorem OAI.PartitionConsistency.ConcreteSystem.cardinal_κ line 123
  21. instance OAI.PartitionConsistency.ConcreteSystem.(instance at line 126) line 126
  22. instance OAI.PartitionConsistency.ConcreteSystem.(instance at line 128) line 128
  23. theorem OAI.PartitionConsistency.ConcreteSystem.size_lt line 131
  24. abbrev OAI.PartitionConsistency.ConcreteSystem.P line 134
  25. def OAI.PartitionConsistency.ConcreteSystem.S line 136
  26. theorem OAI.PartitionConsistency.ConcreteSystem.forces_ZF line 138
  27. theorem OAI.PartitionConsistency.ConcreteSystem.forces_not_AC line 140
  28. theorem OAI.PartitionConsistency.ConcreteSystem.consistent_ZF_not_AC line 146

    Source documentation

    Consistency of the ZF + ¬AC subtheory. The full target, also including PP and ordinal-indexed choice, is proved below in consistent_target.

    theorem consistent_ZF_not_AC : Consistent (Set.insert SetLanguage.AC.neg SetLanguage.ZF) := by
…

    Mentions: OAI.PartitionConsistency.Consistent, OAI.PartitionConsistency.SetLanguage.ZF

  29. theorem OAI.PartitionConsistency.LocalDiagramSystem.label_available_iff line 166

    Source documentation

    Label availability is literal membership in the subdiagram range.

    theorem label_available_iff (r : Diagram M I) (j : r.range) (n : M) :
    (labelSystem (M := M) (I := I)).Available r j n ↔ j.val ∈ (r.sub n).range := by
…

    Mentions: OAI.PartitionConsistency.LocalDiagramSystem.labelSystem

  30. theorem OAI.PartitionConsistency.LocalDiagramSystem.label_available_center line 175

    Source documentation

    The availability test at a center is precisely left divisibility.

    theorem label_available_center (r : Diagram M I) (k n : M) :
    (labelSystem (M := M) (I := I)).Available r ⟨r k,⟨k,rfl⟩⟩ n ↔ n ∣ k := by
…

    Mentions: OAI.PartitionConsistency.LocalDiagramSystem.labelSystem

  31. def OAI.PartitionConsistency.LocalDiagramSystem.labelFiberEmbedding line 186

    Source documentation

    A probe profile supplies a genuine exact-fiber label, rather than merely an element of the ambient label range.

    def labelFiberEmbedding {q : Diagram M I} (w : Vertex q) {K : Type u}
    (m : K → M) (hinj : Function.Injective m)
    (hprofile : ∀ i (x : M), x ∣ w.index ∧ x ∣ m i ↔ x ∈ w.ideal.carrier) :
    K ↪ (labelSystem (M := M) (I := I)).vertexFiber w where
…

    Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex, OAI.PartitionConsistency.LocalDiagramSystem.labelSystem

  32. def OAI.PartitionConsistency.LocalDiagramSystem.labelFiberSet line 204

    Source documentation

    The common ground subset of label indices underlying a component.

    def labelFiberSet {q : Diagram M I} (w : Vertex q) : Set I :=
…

    Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex

  33. theorem OAI.PartitionConsistency.LocalDiagramSystem.labelFiberSet_subset line 207
  34. theorem OAI.PartitionConsistency.LocalDiagramSystem.label_arrowMap_val line 213

    Source documentation

    Contractions act as the identity on label indices.

    theorem label_arrowMap_val (hj : HasConditionalJoins (LeftDivOrder M))
    {q : Diagram M I} {w z : Vertex q} (f : w.Arrow z)
    (x : (labelSystem (M := M) (I := I)).vertexFiber z) :
…

    Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex, OAI.PartitionConsistency.LocalDiagramSystem.labelSystem

  35. theorem OAI.PartitionConsistency.LocalDiagramSystem.labelFiberSet_arrow line 218
  36. theorem OAI.PartitionConsistency.LocalDiagramSystem.labelFiberSet_common line 230

    Source documentation

    The label fibers of a whole connected component are literally the same subset of the coordinate set, not just equinumerous sets.

    theorem labelFiberSet_common (hj : HasConditionalJoins (LeftDivOrder M))
    {q : Diagram M I} {w z : Vertex q} (h : Vertex.Common w z) :
    labelFiberSet w = labelFiberSet z := by
…

    Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex, OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Common, OAI.PartitionConsistency.LocalDiagramSystem.labelFiberSet

  37. theorem OAI.PartitionConsistency.MonoidConstruction.Saturation.labelFiber_cardinal line 248

    Source documentation

    The source's exact label-fiber count in the actual executed saturated monoid. All ideals at all final vertices are covered. No count of symbolic E-classes is postulated here.

    theorem labelFiber_cardinal {μ : Cardinal.{u}} (hω : Cardinal.aleph 1 ≤ μ)
    (hpow : μ ^ Cardinal.aleph0 = μ) (hM : Cardinal.mk M ≤ μ) (hK : Cardinal.mk K = μ)
    {I : Type u} {q : Diagram (target M K) I} (w : Vertex q) :
    Cardinal.mk ((labelSystem (M := target M K) (I := I)).vertexFiber w) = μ := by
…

    Mentions: OAI.PartitionConsistency.MonoidConstruction.Saturation.target

  38. theorem OAI.PartitionConsistency.MonoidConstruction.Saturation.gluedLabel_cardinal line 261

    Source documentation

    Gluing changes neither this label fiber nor its cardinality.

    theorem gluedLabel_cardinal {μ : Cardinal.{u}} (hω : Cardinal.aleph 1 ≤ μ)
    (hpow : μ ^ Cardinal.aleph0 = μ) (hM : Cardinal.mk M ≤ μ) (hK : Cardinal.mk K = μ)
    {I : Type u} {q : Diagram (target M K) I} (w : Vertex q) :
    Cardinal.mk ((labelSystem (M := target M K) (I := I)).Glued (target M K).joins w) = μ := by
…

    Mentions: OAI.PartitionConsistency.MonoidConstruction.Saturation.target

  39. abbrev OAI.PartitionConsistency.LocalDiagramSystem.Vertex.RootGroup line 282
  40. def OAI.PartitionConsistency.LocalDiagramSystem.Vertex.permute line 286

    Source documentation

    The action fixes the chosen root diagram literally, and leaves the monoid index and ideal unchanged.

    def permute (π : RootGroup q) (v : Vertex q) : Vertex q where
…

    Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex.RootGroup, OAI.PartitionConsistency.LocalDiagramSystem.Vertex

  41. theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.permute_one line 294
  42. theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.permute_mul line 298
  43. instance OAI.PartitionConsistency.LocalDiagramSystem.Vertex.(instance at line 303) line 303
  44. theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.smul_diagram line 308
  45. theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.smul_index line 310
  46. theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.smul_ideal line 311
  47. def OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Arrow.move line 315

    Source documentation

    Coordinate transport preserves the entire contraction, not merely a relation between ranges.

    def Arrow.move {v w : Vertex q} (π : RootGroup q) (f : Arrow v w) :
    Arrow (π • v) (π • w) where
…

    Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex, OAI.PartitionConsistency.LocalDiagramSystem.Vertex.RootGroup, OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Arrow

  48. theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Common.move line 322
  49. def OAI.PartitionConsistency.LocalDiagramSystem.Vertex.componentStabilizer line 329

    Source documentation

    Setwise stabilizer of the component of v. Common is already proved to be exactly connectedness under finite contraction zigzags.

    def componentStabilizer (hj : HasConditionalJoins (LeftDivOrder M)) (v : Vertex q) :
    Subgroup (RootGroup q) where
…

    Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex, OAI.PartitionConsistency.LocalDiagramSystem.Vertex.RootGroup

  50. theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.common_moved line 344
  51. structure OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Chain line 350

    Source documentation

    A concrete cofinal chain in a component. Its arrows contain actual translation indices, and the initial term is the chosen vertex.

    structure Chain (v : Vertex q) where
…

    Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex

  52. theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.exists_chain line 358

    Source documentation

    Chains are constructed from the height-cost theorem, not postulated when they are used with the saturated monoid.

    theorem exists_chain (hj : HasConditionalJoins (LeftDivOrder M))
    (H : HeightCost (LeftDivOrder M)) (v : Vertex q) : Nonempty (Chain v) := by
…

    Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex, OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Chain

  53. theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Chain.common line 366
  54. theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Chain.ranges_antitone line 370
  55. def OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Chain.tailFixer line 378

    Source documentation

    The increasing union of pointwise tail fixers, regarded inside the actual component stabilizer.

    def tailFixer (hj : HasConditionalJoins (LeftDivOrder M)) :
    Subgroup (componentStabilizer hj v) where
…

    Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex.componentStabilizer

  56. theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Chain.mem_tailFixer line 397

    Source documentation

    Membership is eventual pointwise fixation, not a condition on an assigned bijection or on the result of the quotient construction.

    theorem mem_tailFixer (hj : HasConditionalJoins (LeftDivOrder M))
    (π : componentStabilizer hj v) : π ∈ C.tailFixer hj ↔
      ∃ i, ∀ j ∈ (C.vertex i).diagram.range, π.val.val j = j := Iff.rfl

    Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex.componentStabilizer

  57. theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Chain.fixes_mem_stabilizer line 403

    Source documentation

    A permutation fixing a chain diagram belongs to the component stabilizer. This justifies viewing the displayed union of full fixers inside that group.

    theorem fixes_mem_stabilizer (hj : HasConditionalJoins (LeftDivOrder M))
    (π : RootGroup q) (i : ℕ)
    (h : ∀ j ∈ (C.vertex i).diagram.range, π.val j = j) :
    π ∈ componentStabilizer hj v := by
…

    Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex.RootGroup, OAI.PartitionConsistency.LocalDiagramSystem.Vertex.componentStabilizer

  58. instance OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Chain.tailFixer_normal line 418

    Source documentation

    Cofinality of the chain makes the union of its tail fixers normal. The conjugating permutation is allowed to move the entire chain.

    instance tailFixer_normal (hj : HasConditionalJoins (LeftDivOrder M)) :
    (C.tailFixer hj).Normal where
…
  59. theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Chain.tailFixer_fixes_labels line 434

    Source documentation

    The name-independent label set is fixed pointwise by every tail fixer.

    theorem tailFixer_fixes_labels (hj : HasConditionalJoins (LeftDivOrder M))
    (k : C.tailFixer hj) (j : I) (hjv : j ∈ labelFiberSet v) : k.val.val.val j = j := by
…

    Mentions: OAI.PartitionConsistency.LocalDiagramSystem.labelFiberSet