OAI/SetTheory/PartitionConsistency/Construction/MonoidBase.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Base

  1. structure OAI.PartitionConsistency.MonoidConstruction.Object line 15

    Source documentation

    The objects used by the construction retain the real margin together with an actual cancellative conical monoid; no saturation property is built in.

    structure Object where
…
  2. instance OAI.PartitionConsistency.MonoidConstruction.(instance at line 24) line 24
  3. abbrev OAI.PartitionConsistency.MonoidConstruction.Base.M line 28
  4. def OAI.PartitionConsistency.MonoidConstruction.Base.degree line 30
  5. instance OAI.PartitionConsistency.MonoidConstruction.Base.(instance at line 32) line 32
  6. theorem OAI.PartitionConsistency.MonoidConstruction.Base.le_iff line 37
  7. theorem OAI.PartitionConsistency.MonoidConstruction.Base.lt_iff line 42
  8. theorem OAI.PartitionConsistency.MonoidConstruction.Base.joins line 45
  9. def OAI.PartitionConsistency.MonoidConstruction.Base.height line 53
  10. def OAI.PartitionConsistency.MonoidConstruction.Base.cost line 54
  11. theorem OAI.PartitionConsistency.MonoidConstruction.Base.height_pos line 56
  12. theorem OAI.PartitionConsistency.MonoidConstruction.Base.height_lt_one line 60
  13. theorem OAI.PartitionConsistency.MonoidConstruction.Base.margin line 65
  14. def OAI.PartitionConsistency.MonoidConstruction.Base.heightCost line 85
  15. def OAI.PartitionConsistency.MonoidConstruction.Base.object line 95

    Source documentation

    The free monoid on one generator, with the source's concrete base heights.

    noncomputable def object : Object.{0} where
…
  16. def OAI.PartitionConsistency.MonoidConstruction.missedSup line 116

    Source documentation

    The amount reserved by the margin at an ordered pair.

    def missedSup (M : Object.{u}) (x y : M) : ℝ :=
…
  17. structure OAI.PartitionConsistency.MonoidConstruction.Hom line 121

    Source documentation

    Maps of construction stages retain right factors, disjointness, and exact old suprema. Such maps make continuous unions legitimate stages.

    structure Hom (M : Object.{u}) (N : Object.{v}) extends M →* N where
…
  18. instance OAI.PartitionConsistency.MonoidConstruction.(instance at line 128) line 128
  19. theorem OAI.PartitionConsistency.MonoidConstruction.Hom.ext line 135
  20. def OAI.PartitionConsistency.MonoidConstruction.Hom.id line 140
  21. def OAI.PartitionConsistency.MonoidConstruction.Hom.comp line 148
  22. theorem OAI.PartitionConsistency.MonoidConstruction.Hom.id_apply line 156
  23. theorem OAI.PartitionConsistency.MonoidConstruction.Hom.comp_apply line 157
  24. theorem OAI.PartitionConsistency.MonoidConstruction.Hom.id_comp line 160
  25. theorem OAI.PartitionConsistency.MonoidConstruction.Hom.comp_id line 161
  26. theorem OAI.PartitionConsistency.MonoidConstruction.Hom.injective line 163
  27. structure OAI.PartitionConsistency.MonoidConstruction.ProbeData line 170

    Source documentation

    A probe request has exactly the old parameters in the presentation; its path contains its countably many transition and terminal quotients by conservativity, not an additional saturation assumption.

    structure ProbeData (M : Object.{u}) where
…
  28. def OAI.PartitionConsistency.MonoidConstruction.ProbeData.extension line 180

    Source documentation

    Executing a request uses the established literal normal forms.

    def extension : Object.{u} where
…
  29. def OAI.PartitionConsistency.MonoidConstruction.ProbeData.inclusion line 190
  30. def OAI.PartitionConsistency.MonoidConstruction.ProbeData.probe line 198
  31. theorem OAI.PartitionConsistency.MonoidConstruction.ProbeData.profile line 200
  32. theorem OAI.PartitionConsistency.MonoidConstruction.ProbeData.probe_new line 204
  33. theorem OAI.PartitionConsistency.MonoidConstruction.ProbeData.gates line 210
  34. theorem OAI.PartitionConsistency.MonoidConstruction.ProbeData.cardinal_le line 213
  35. theorem OAI.PartitionConsistency.MonoidConstruction.ProbeData.preserves_profile line 219

    Source documentation

    Later probes preserve the full previous profile, including their own new divisors of the upper bound.

    theorem preserves_profile {a b e m : M} {n : ℕ → M} (h : ProbeProfile a b e m n) :
    ProbeProfile (d.inclusion a) (d.inclusion b) (d.inclusion e)
      (d.inclusion m) (fun k => d.inclusion (n k)) :=
…
  36. structure OAI.PartitionConsistency.MonoidConstruction.MergerData line 226
  37. def OAI.PartitionConsistency.MonoidConstruction.MergerData.extension line 235
  38. def OAI.PartitionConsistency.MonoidConstruction.MergerData.inclusion line 245
  39. def OAI.PartitionConsistency.MonoidConstruction.MergerData.root line 253
  40. theorem OAI.PartitionConsistency.MonoidConstruction.MergerData.realization line 255
  41. theorem OAI.PartitionConsistency.MonoidConstruction.MergerData.no_new_old_divisors line 260
  42. theorem OAI.PartitionConsistency.MonoidConstruction.MergerData.gates line 268
  43. theorem OAI.PartitionConsistency.MonoidConstruction.MergerData.cardinal_le line 271
  44. theorem OAI.PartitionConsistency.MonoidConstruction.MergerData.preserves_profile line 275