OAI/SetTheory/PartitionConsistency/Construction/BlockTowers.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

BlockIndex

  1. abbrev OAI.PartitionConsistency.ConservativeMonoids.BlockIndex.Interior line 22
  2. abbrev OAI.PartitionConsistency.ConservativeMonoids.BlockIndex.Index line 23
  3. instance OAI.PartitionConsistency.ConservativeMonoids.BlockIndex.(instance at line 25) line 25
  4. instance OAI.PartitionConsistency.ConservativeMonoids.BlockIndex.(instance at line 38) line 38
  5. def OAI.PartitionConsistency.ConservativeMonoids.BlockIndex.cut line 40
  6. theorem OAI.PartitionConsistency.ConservativeMonoids.BlockIndex.cut_le_cut line 47
  7. theorem OAI.PartitionConsistency.ConservativeMonoids.BlockIndex.cut_lt_cut line 51
  8. theorem OAI.PartitionConsistency.ConservativeMonoids.BlockIndex.cut_lt_of_lt line 55
  9. theorem OAI.PartitionConsistency.ConservativeMonoids.BlockIndex.cut_lt_top line 57
  10. theorem OAI.PartitionConsistency.ConservativeMonoids.BlockIndex.cut_bot line 62
  11. theorem OAI.PartitionConsistency.ConservativeMonoids.BlockIndex.succ_inner line 66

    Source documentation

    Successors within a block.

    theorem succ_inner (i : I) (j : J i) (hj : j < ⊤) :
    Order.succ (cut i j) = cut i (Order.succ j) := by
…

    Mentions: OAI.PartitionConsistency.ConservativeMonoids.BlockIndex.cut

  12. theorem OAI.PartitionConsistency.ConservativeMonoids.BlockIndex.succ_boundary line 85

    Source documentation

    The final cut of one block is followed by the initial cut of the next.

    theorem succ_boundary (i : I) :
    Order.succ (cut i (⊤ : J i)) = cut (Order.succ i) (⊥ : J (Order.succ i)) := by
…

    Mentions: OAI.PartitionConsistency.ConservativeMonoids.BlockIndex.cut

  13. theorem OAI.PartitionConsistency.ConservativeMonoids.BlockIndex.inner_limit line 100

    Source documentation

    A noninitial limit inside a block must be a limit of that block.

    theorem inner_limit {i : I} {j : J i} (h : Order.IsSuccLimit (cut i j)) (hj : j ≠ ⊥) :
    Order.IsSuccLimit j := by
…

    Mentions: OAI.PartitionConsistency.ConservativeMonoids.BlockIndex.cut

  14. theorem OAI.PartitionConsistency.ConservativeMonoids.BlockIndex.outer_limit line 112

    Source documentation

    A limit at an initial cut must be an outer limit (not a successor or zero). This includes the identity boundary cuts in the argument.

    theorem outer_limit {i : I} (h : Order.IsSuccLimit (cut i (⊥ : J i))) :
    Order.IsSuccLimit i := by
…

    Mentions: OAI.PartitionConsistency.ConservativeMonoids.BlockIndex.cut

  15. structure OAI.PartitionConsistency.ConservativeMonoids.BlockTower line 144

    Source documentation

    An iterated cellular construction before flattening. All stages are literal submonoids of the same final monoid.

    structure BlockTower where
…
  16. def OAI.PartitionConsistency.ConservativeMonoids.BlockTower.flatStage line 159
  17. theorem OAI.PartitionConsistency.ConservativeMonoids.BlockTower.flatStage_cut line 164
  18. def OAI.PartitionConsistency.ConservativeMonoids.BlockTower.flatten line 168

    Source documentation

    Flattening retains every original cell and does not change the terminal monoid or any of the limit unions.

    def flatten : CellTower T (Index I J) where
…

    Mentions: OAI.PartitionConsistency.ConservativeMonoids.CellTower

  19. theorem OAI.PartitionConsistency.ConservativeMonoids.BlockTower.flatten_bottom line 228
  20. theorem OAI.PartitionConsistency.ConservativeMonoids.Cell.simulation_surjective line 245
  21. def OAI.PartitionConsistency.ConservativeMonoids.Cell.simulationEquiv line 258
  22. theorem OAI.PartitionConsistency.ConservativeMonoids.Cell.simulationEquiv_old line 263
  23. def OAI.PartitionConsistency.ConservativeMonoids.Cell.rangeAttachment line 269

    Source documentation

    Identify an original executed cell with the literal ranges inside its terminal monoid. Surjectivity here is proved from the presentation.

    def rangeAttachment {T : Object.{u}} (f : M ⟶ T) (g : d.extension ⟶ T)
    (h : ∀ x, g (d.inclusion x) = f x) :
    Attachment (Subobject.range f) (Subobject.range g) := by
…

    Mentions: OAI.PartitionConsistency.ConservativeMonoids.Attachment, OAI.PartitionConsistency.ConservativeMonoids.Subobject.range

  24. theorem OAI.PartitionConsistency.ConservativeMonoids.Hom.range_comp_of_surjective line 286
  25. theorem OAI.PartitionConsistency.ConservativeMonoids.request_rangeAttachment line 310

    Source documentation

    The literal range of an executed request is the range attachment of its actual probe or merger presentation.

    theorem request_rangeAttachment {M : MonoidConstruction.Object.{u}} {T : Object.{u}}
    (d : MonoidConstruction.Request M) (f : forgetMargins.obj M ⟶ T)
    (g : forgetMargins.obj d.target ⟶ T) (h : ∀ x, g (d.inclusion x) = f x) :
    Nonempty (Attachment (Subobject.range f) (Subobject.range g)) := by
…

    Mentions: OAI.PartitionConsistency.MonoidConstruction.Request, OAI.PartitionConsistency.ConservativeMonoids.Attachment, OAI.PartitionConsistency.ConservativeMonoids.Subobject.range

  26. instance OAI.PartitionConsistency.MonoidConstruction.RoundOrdinal.(instance at line 328) line 328
  27. abbrev OAI.PartitionConsistency.MonoidConstruction.Saturation.blockBase line 334
  28. abbrev OAI.PartitionConsistency.MonoidConstruction.Saturation.blockIndex line 335
  29. abbrev OAI.PartitionConsistency.MonoidConstruction.Saturation.blockFunctor line 336
  30. def OAI.PartitionConsistency.MonoidConstruction.Saturation.blockMap line 338
  31. def OAI.PartitionConsistency.MonoidConstruction.Saturation.blockStage line 342
  32. def OAI.PartitionConsistency.MonoidConstruction.Saturation.outerStage line 346
  33. theorem OAI.PartitionConsistency.MonoidConstruction.Saturation.blockMap_naturality line 350
  34. theorem OAI.PartitionConsistency.MonoidConstruction.Saturation.outerMap_naturality line 355
  35. theorem OAI.PartitionConsistency.MonoidConstruction.Saturation.blockStage_base line 360
  36. theorem OAI.PartitionConsistency.MonoidConstruction.Saturation.blockStage_top line 376
  37. theorem OAI.PartitionConsistency.MonoidConstruction.Saturation.blockStage_mono line 394
  38. theorem OAI.PartitionConsistency.MonoidConstruction.Saturation.outerStage_mono line 402
  39. theorem OAI.PartitionConsistency.MonoidConstruction.Saturation.blockStage_limit line 409
  40. theorem OAI.PartitionConsistency.MonoidConstruction.Saturation.outerStage_limit line 419
  41. theorem OAI.PartitionConsistency.MonoidConstruction.Saturation.blockStage_step line 429
  42. def OAI.PartitionConsistency.MonoidConstruction.Saturation.blocks line 450

    Source documentation

    The executed omega-one many saturation rounds form a literal block tower inside the very same final monoid.

    def blocks : BlockTower (I := RoundOrdinal.{u}) (J := blockIndex M K)
…

    Mentions: OAI.PartitionConsistency.MonoidConstruction.Saturation.blockIndex

  43. abbrev OAI.PartitionConsistency.MonoidConstruction.Saturation.FlatIndex line 483
  44. def OAI.PartitionConsistency.MonoidConstruction.Saturation.cells line 484