OAI/SetTheory/PartitionConsistency/Construction/CompleteRounds.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

RequestSize

  1. def OAI.PartitionConsistency.MonoidConstruction.ProbeData.code line 15
  2. theorem OAI.PartitionConsistency.MonoidConstruction.ProbeData.code_injective line 16
  3. theorem OAI.PartitionConsistency.MonoidConstruction.ProbeData.data_cardinal_le line 21
  4. def OAI.PartitionConsistency.MonoidConstruction.MergerData.code line 35
  5. theorem OAI.PartitionConsistency.MonoidConstruction.MergerData.code_injective line 38
  6. theorem OAI.PartitionConsistency.MonoidConstruction.MergerData.data_cardinal_le line 46
  7. theorem OAI.PartitionConsistency.MonoidConstruction.Request.data_cardinal_le line 73
  8. theorem OAI.PartitionConsistency.MergerAlgebra.Word.snoc_cones_disjoint line 97

    Source documentation

    Disjoint terminal-letter cones give disjoint cones with any fixed prefix.

    theorem snoc_cones_disjoint (w : Word M D) (s t : D)
    (hst : ∀ d : D, ¬ (RightFreeAction.Reaches M s d ∧ RightFreeAction.Reaches M t d))
    (z : Word M D) : ¬ (snoc w s ∣ z ∧ snoc w t ∣ z) := by
…

    Mentions: OAI.PartitionConsistency.MergerAlgebra.Word, OAI.PartitionConsistency.MergerAlgebra.RightFreeAction.Reaches

  9. def OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.RootSystem line 114

    Source documentation

    The cone form of exact realization. Unlike checking only old right factors, this form persists under arbitrary conservative embeddings.

    def RootSystem (P : OverlapPrescription M n) (l : Fin n → M) : Prop :=
…

    Mentions: OAI.PartitionConsistency.DiagramForcing.OverlapPrescription

  10. theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.RootSystem.map line 121
  11. theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.RootSystem.realization line 138
  12. theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.root_system line 172

    Source documentation

    A literal merger realizes prescribed cones in its entire normal-form monoid, not only at the old factors.

    theorem root_system (P : OverlapPrescription M n) (hP : P.Valid) :
    (P.map (Word.oldHom : M →* P.Merger hP)).RootSystem (P.root hP) := by
…

    Mentions: OAI.PartitionConsistency.DiagramForcing.OverlapPrescription, OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.RootSystem

  13. theorem OAI.PartitionConsistency.MonoidConstruction.MergerData.cone_realization line 206
  14. theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.map_comp line 221
  15. def OAI.PartitionConsistency.MonoidConstruction.Round.requestIso line 233

    Source documentation

    Identification of the next stage with the actual operation's normal forms.

    def requestIso (j : J) (hj : ¬IsMax j) (d : Request M) (hd : schedule j = d) :
    (functor M schedule).obj (Order.succ j) ≅ (d.map (fromBase M schedule j)).target :=
…

    Mentions: OAI.PartitionConsistency.MonoidConstruction.Request, OAI.PartitionConsistency.MonoidConstruction.Round.functor, OAI.PartitionConsistency.MonoidConstruction.Round.fromBase

  16. theorem OAI.PartitionConsistency.MonoidConstruction.Round.map_succ_request line 237
  17. def OAI.PartitionConsistency.MonoidConstruction.Round.afterRequestMap line 246
  18. theorem OAI.PartitionConsistency.MonoidConstruction.Round.inclusion_afterRequestMap line 251
  19. theorem OAI.PartitionConsistency.MonoidConstruction.Round.fromBase_afterRequestMap line 258
  20. theorem OAI.PartitionConsistency.MonoidConstruction.Round.afterRequestMap_preservesProfiles line 267
  21. theorem OAI.PartitionConsistency.MonoidConstruction.Round.creates_merger line 275

    Source documentation

    Each scheduled finite merger stays exact at every subsequent cut, including for the new right factors at that cut.

    theorem creates_merger (j : J) (hj : ¬IsMax j) (d : MergerData M)
    (hd : schedule j = .inr d) (k : J) (hjk : Order.succ j ≤ k) :
    ∃ l : Fin d.n → (functor M schedule).obj k,
      (d.prescription.map (fromBase M schedule k).toMonoidHom).RootSystem l := by
…

    Mentions: OAI.PartitionConsistency.MonoidConstruction.MergerData, OAI.PartitionConsistency.MonoidConstruction.Round.functor, OAI.PartitionConsistency.MonoidConstruction.Round.fromBase

  22. def OAI.PartitionConsistency.MonoidConstruction.Round.probe line 294

    Source documentation

    The actual new probe after its conservative transport to a later cut.

    def probe (j : J) (hj : ¬IsMax j) (d : ProbeData M)
    (hd : schedule j = .inl d) (k : J) (hjk : Order.succ j ≤ k) :
    (functor M schedule).obj k :=
…

    Mentions: OAI.PartitionConsistency.MonoidConstruction.ProbeData, OAI.PartitionConsistency.MonoidConstruction.Round.functor

  23. theorem OAI.PartitionConsistency.MonoidConstruction.Round.probe_transition line 299
  24. theorem OAI.PartitionConsistency.MonoidConstruction.Round.probe_profile line 308
  25. theorem OAI.PartitionConsistency.MonoidConstruction.Round.probe_new line 325
  26. theorem OAI.PartitionConsistency.MonoidConstruction.Round.probe_independent line 337

    Source documentation

    Independence is with respect to the whole previous stage, not merely the round's starting monoid.

    theorem probe_independent (j : J) (hj : ¬IsMax j) (d : ProbeData M)
    (hd : schedule j = .inl d) (k : J) (hjk : Order.succ j ≤ k)
    (x : (functor M schedule).obj j)
    (hx : x ∣ (fromBase M schedule j d.a) * ((functor M schedule).obj j).e)
    (hxa : ¬ x ∣ fromBase M schedule j d.a) (z : (functor M schedule).obj k) :
    (functor M schedule).map (homOfLE ((Order.le_succ j).trans hjk)) x ∣ z ∧
      probe M schedule j hj d hd k hjk ∣ z ↔ fromBase M schedule k d.a * ((functor M schedule).obj k).e ∣ z := by
…

    Mentions: OAI.PartitionConsistency.MonoidConstruction.ProbeData, OAI.PartitionConsistency.MonoidConstruction.Round.functor, OAI.PartitionConsistency.MonoidConstruction.Round.fromBase, OAI.PartitionConsistency.MonoidConstruction.Round.probe

  27. theorem OAI.PartitionConsistency.MonoidConstruction.Round.probes_ne_of_lt line 371
  28. theorem OAI.PartitionConsistency.MonoidConstruction.Round.probes_independent_of_lt line 384

    Source documentation

    Any two distinct executions of one datum have exactly the common exit cone.

    theorem probes_independent_of_lt (i j : J) (hi : ¬IsMax i) (hj : ¬IsMax j)
    (d : ProbeData M) (hdi : schedule i = .inl d) (hdj : schedule j = .inl d)
    (hij : i < j) (k : J) (hjk : Order.succ j ≤ k) (z : (functor M schedule).obj k) :
    probe M schedule i hi d hdi k ((Order.succ_le_iff_of_not_isMax hi).2 hij |>.trans
      ((Order.le_succ j).trans hjk)) ∣ z ∧ probe M schedule j hj d hdj k hjk ∣ z ↔
      fromBase M schedule k d.a * ((functor M schedule).obj k).e ∣ z := by
…

    Mentions: OAI.PartitionConsistency.MonoidConstruction.ProbeData, OAI.PartitionConsistency.MonoidConstruction.Round.functor, OAI.PartitionConsistency.MonoidConstruction.Round.probe, OAI.PartitionConsistency.MonoidConstruction.Round.fromBase

  29. abbrev OAI.PartitionConsistency.MonoidConstruction.CompleteRound.Index line 403
  30. def OAI.PartitionConsistency.MonoidConstruction.CompleteRound.schedule line 405
  31. def OAI.PartitionConsistency.MonoidConstruction.CompleteRound.place line 409
  32. theorem OAI.PartitionConsistency.MonoidConstruction.CompleteRound.at_place line 411
  33. theorem OAI.PartitionConsistency.MonoidConstruction.CompleteRound.place_not_isMax line 413
  34. theorem OAI.PartitionConsistency.MonoidConstruction.CompleteRound.place_injective line 418
  35. abbrev OAI.PartitionConsistency.MonoidConstruction.CompleteRound.tower line 422
  36. def OAI.PartitionConsistency.MonoidConstruction.CompleteRound.target line 423
  37. def OAI.PartitionConsistency.MonoidConstruction.CompleteRound.inclusion line 424
  38. theorem OAI.PartitionConsistency.MonoidConstruction.CompleteRound.preservesProfiles line 426
  39. theorem OAI.PartitionConsistency.MonoidConstruction.CompleteRound.cardinal_le line 429
  40. def OAI.PartitionConsistency.MonoidConstruction.CompleteRound.probe line 438
  41. theorem OAI.PartitionConsistency.MonoidConstruction.CompleteRound.probe_profile line 441
  42. theorem OAI.PartitionConsistency.MonoidConstruction.CompleteRound.probe_injective line 446
  43. theorem OAI.PartitionConsistency.MonoidConstruction.CompleteRound.probes_independent line 456
  44. theorem OAI.PartitionConsistency.MonoidConstruction.CompleteRound.realizes_merger line 466
  45. abbrev OAI.PartitionConsistency.MonoidConstruction.RoundOrdinal line 485

    Source documentation

    The first uncountable ordinal, as a small indexing type. There is no inaccessible-cardinal or chain-length closure assumption in this index.

    abbrev RoundOrdinal : Type u := (Cardinal.aleph.{u} 1).ord.ToType
…
  46. instance OAI.PartitionConsistency.MonoidConstruction.RoundOrdinal.(instance at line 487) line 487
  47. instance OAI.PartitionConsistency.MonoidConstruction.RoundOrdinal.(instance at line 489) line 489
  48. instance OAI.PartitionConsistency.MonoidConstruction.RoundOrdinal.(instance at line 490) line 490
  49. instance OAI.PartitionConsistency.MonoidConstruction.RoundOrdinal.(instance at line 492) line 492
  50. theorem OAI.PartitionConsistency.MonoidConstruction.RoundOrdinal.countable_bounded line 495

    Source documentation

    Countably many round indices are bounded before the last union.

    theorem countable_bounded {A : Type v} [Countable A] (f : A → RoundOrdinal.{u}) :
    ∃ j : RoundOrdinal.{u}, ∀ i, f i ≤ j := by
…
  51. theorem OAI.PartitionConsistency.MonoidConstruction.RoundOrdinal.cardinal line 515
  52. abbrev OAI.PartitionConsistency.MonoidConstruction.OuterIndex line 519
  53. instance OAI.PartitionConsistency.MonoidConstruction.(instance at line 520) line 520
  54. theorem OAI.PartitionConsistency.MonoidConstruction.outer_top_limit line 522
  55. theorem OAI.PartitionConsistency.MonoidConstruction.outer_countable_bound line 524
  56. def OAI.PartitionConsistency.MonoidConstruction.Saturation.step line 535
  57. abbrev OAI.PartitionConsistency.MonoidConstruction.Saturation.tower line 537
  58. def OAI.PartitionConsistency.MonoidConstruction.Saturation.botIso line 539
  59. def OAI.PartitionConsistency.MonoidConstruction.Saturation.succIso line 540
  60. theorem OAI.PartitionConsistency.MonoidConstruction.Saturation.map_succ line 544
  61. def OAI.PartitionConsistency.MonoidConstruction.Saturation.target line 549
  62. def OAI.PartitionConsistency.MonoidConstruction.Saturation.fromStage line 550
  63. def OAI.PartitionConsistency.MonoidConstruction.Saturation.inclusion line 552
  64. theorem OAI.PartitionConsistency.MonoidConstruction.Saturation.preservesProfiles line 554
  65. theorem OAI.PartitionConsistency.MonoidConstruction.Saturation.cardinal_le line 563
  66. theorem OAI.PartitionConsistency.MonoidConstruction.Saturation.countable_stage line 580

    Source documentation

    Every countable set of final elements, with no restriction on their birth rounds, lies in one proper stage, before a following complete round.

    theorem countable_stage {A : Type v} [Countable A] (f : A → target M K) :
    ∃ j : OuterIndex.{u}, j < ⊤ ∧ ∃ g : A → (tower M K).obj j,
      ∀ a, fromStage M K j (g a) = f a := by
…

    Mentions: OAI.PartitionConsistency.MonoidConstruction.Saturation.target, OAI.PartitionConsistency.MonoidConstruction.Saturation.tower, OAI.PartitionConsistency.MonoidConstruction.Saturation.fromStage