MergerWords.lean`

74 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.PartitionConsistency.DiagramOrder.pair_lub_iff line 11
lemma OAI.PartitionConsistency.DiagramOrder.LeftDivOrder.le_iff_dvd line 17
lemma OAI.PartitionConsistency.DiagramOrder.exists_cone_join line 21
theorem OAI.PartitionConsistency.DiagramOrder.left_mul_dvd_iff line 35
Source documentation
Cancellation for right divisibility in a left-cancellative monoid.
```
theorem left_mul_dvd_iff {M : Type*} [LeftCancelMonoid M] (a x y : M) :
    a * x ∣ a * y ↔ x ∣ y := by
…
```

theorem OAI.PartitionConsistency.DiagramOrder.exists_cone_residual line 45

Source documentation

A nonempty inverse image of a principal right cone under left multiplication is principal. Its initial element is the right quotient of the conditional join.

theorem exists_cone_residual {M : Type*} [LeftCancelMonoid M]
    (hM : ∀ x y a : M, x ∣ a → y ∣ a → ∃ j : M, ∀ b : M, x ∣ b ∧ y ∣ b ↔ j ∣ b)
    (x a c : M) (hc : x ∣ a * c) :
    ∃ r : M, ∀ t : M, x ∣ a * t ↔ r ∣ t := by
…

class OAI.PartitionConsistency.MergerAlgebra.RightFreeAction line 66
Source documentation
A right action in which each orbit map is injective. This is the property of the prescribed quotient of copies used in the merger normal forms. It does not posit the existence of any monoid extension.
```
class RightFreeAction (M : Type u) (D : Type v) [Monoid M] where
…
```
def OAI.PartitionConsistency.MergerAlgebra.RightFreeAction.Reaches line 76
Source documentation
The right divisibility relation on a right monoid-set.
```
def Reaches (M : Type u) {D : Type v} [Monoid M] [RightFreeAction M D]
    (z w : D) : Prop := ∃ m : M, act z m = w
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.RightFreeAction
theorem OAI.PartitionConsistency.MergerAlgebra.RightFreeAction.reaches_refl line 79
theorem OAI.PartitionConsistency.MergerAlgebra.RightFreeAction.reaches_trans line 81
def OAI.PartitionConsistency.MergerAlgebra.RightFreeAction.HasConeJoins line 88
Source documentation
Conditional joins expressed as exact intersections of right cones.
```
def HasConeJoins (M : Type u) (D : Type v) [Monoid M] [RightFreeAction M D] : Prop :=
…
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.RightFreeAction
inductive OAI.PartitionConsistency.MergerAlgebra.Word line 96
Source documentation
The literal normal forms x z₁ ... zⱼ of equation eq:mono-merger-forms; words with no new letter are the old monoid.
```
inductive Word (M : Type u) (D : Type v) where
…
```
def OAI.PartitionConsistency.MergerAlgebra.Word.act line 105
Source documentation
Multiplication on the right by an old element acts only on the last new letter (or on the old coefficient, if no new letter is present).
```
def act : Word M D → M → Word M D
  | old x, y => old (x * y)
  | snoc w z, y => snoc w (RightFreeAction.act z y)
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word
theorem OAI.PartitionConsistency.MergerAlgebra.Word.act_one line 109
theorem OAI.PartitionConsistency.MergerAlgebra.Word.act_mul line 112
def OAI.PartitionConsistency.MergerAlgebra.Word.product line 118
Source documentation
Concatenation, absorbing the leading old coefficient of the second normal form into the last letter of the first.
```
def product (x : Word M D) : Word M D → Word M D
  | old y => act x y
  | snoc y z => snoc (product x y) z
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word, OAI.PartitionConsistency.MergerAlgebra.Word.act
theorem OAI.PartitionConsistency.MergerAlgebra.Word.product_act line 122
theorem OAI.PartitionConsistency.MergerAlgebra.Word.product_assoc line 128
theorem OAI.PartitionConsistency.MergerAlgebra.Word.old_one_product line 134
instance OAI.PartitionConsistency.MergerAlgebra.Word.(instance at line 139) line 139
theorem OAI.PartitionConsistency.MergerAlgebra.Word.mul_old line 146
theorem OAI.PartitionConsistency.MergerAlgebra.Word.mul_snoc line 147
theorem OAI.PartitionConsistency.MergerAlgebra.Word.old_mul_old line 149
theorem OAI.PartitionConsistency.MergerAlgebra.Word.snoc_mul_old line 151
def OAI.PartitionConsistency.MergerAlgebra.Word.length line 155
Source documentation
Number of new letters, used to distinguish old from genuinely new words.
```
def length : Word M D → ℕ
  | old _ => 0
  | snoc w _ => length w + 1

omit [Monoid M] [RightFreeAction M D] in
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word, OAI.PartitionConsistency.MergerAlgebra.RightFreeAction
theorem OAI.PartitionConsistency.MergerAlgebra.Word.length_old line 160
theorem OAI.PartitionConsistency.MergerAlgebra.Word.length_snoc line 162
theorem OAI.PartitionConsistency.MergerAlgebra.Word.length_act line 164
theorem OAI.PartitionConsistency.MergerAlgebra.Word.length_mul line 167
theorem OAI.PartitionConsistency.MergerAlgebra.Word.length_zero_iff line 173
theorem OAI.PartitionConsistency.MergerAlgebra.Word.act_injective line 179
theorem OAI.PartitionConsistency.MergerAlgebra.Word.product_left_cancel line 190
Source documentation
Left cancellation is proved from the displayed normal forms. Right cancellation is neither used nor asserted.
```
theorem product_left_cancel (x : Word M D) {y z : Word M D} (h : x * y = x * z) :
    y = z := by
…
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word
instance OAI.PartitionConsistency.MergerAlgebra.Word.(instance at line 210) line 210
theorem OAI.PartitionConsistency.MergerAlgebra.Word.factors_of_old line 217
Source documentation
Letter count prevents a new word from acquiring an old right multiple. It also identifies the old right factor, rather than just reflecting order.
```
theorem factors_of_old {x y : Word M D} {a : M} (h : x * y = old a) :
    ∃ b c : M, x = old b ∧ y = old c ∧ b * c = a := by
…
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word
instance OAI.PartitionConsistency.MergerAlgebra.Word.(instance at line 225) line 225
def OAI.PartitionConsistency.MergerAlgebra.Word.oldHom line 232
Source documentation
The old monoid embeds by words with no new letters.
```
def oldHom : M →* Word M D where
…
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word
theorem OAI.PartitionConsistency.MergerAlgebra.Word.oldHom_injective line 237
def OAI.PartitionConsistency.MergerAlgebra.Word.leading line 240
Source documentation
The leading old coefficient of the normal form.
```
def leading : Word M D → M
  | old x => x
  | snoc w _ => leading w

omit [Monoid M] [RightFreeAction M D] in
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word, OAI.PartitionConsistency.MergerAlgebra.RightFreeAction
theorem OAI.PartitionConsistency.MergerAlgebra.Word.leading_old line 245
theorem OAI.PartitionConsistency.MergerAlgebra.Word.leading_snoc line 247
theorem OAI.PartitionConsistency.MergerAlgebra.Word.leading_old_mul line 250
theorem OAI.PartitionConsistency.MergerAlgebra.Word.old_dvd_iff line 257
Source documentation
Old divisors are read solely from the old leading coefficient.
```
theorem old_dvd_iff (x : M) (w : Word M D) :
    old x ∣ w ↔ x ∣ leading w := by
…
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word, OAI.PartitionConsistency.MergerAlgebra.Word.leading
theorem OAI.PartitionConsistency.MergerAlgebra.Word.old_common_multiple_iff line 273
Source documentation
Comparisons and common-right-multiple calculations on old entries are unchanged in the extension, including the absence of a common multiple.
```
theorem old_common_multiple_iff (x y : M) :
    (∃ w : Word M D, old x ∣ w ∧ old y ∣ w) ↔ ∃ a : M, x ∣ a ∧ y ∣ a := by
…
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word
theorem OAI.PartitionConsistency.MergerAlgebra.Word.preserve_old_cone_intersection line 283
Source documentation
The entire right-cone equation for any old conditional join is preserved, not just comparisons among old elements.
```
theorem preserve_old_cone_intersection (x y j : M)
    (hj : ∀ a : M, x ∣ a ∧ y ∣ a ↔ j ∣ a) (w : Word M D) :
    old x ∣ w ∧ old y ∣ w ↔ old j ∣ w := by
…
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word
theorem OAI.PartitionConsistency.MergerAlgebra.Word.dvd_snoc_iff line 290
Source documentation
Dividing a normal form with one more letter means either dividing its prefix, or having precisely that prefix and advancing the last new letter.
```
theorem dvd_snoc_iff (x w : Word M D) (d : D) :
    x ∣ snoc w d ↔ x ∣ w ∨ ∃ z, x = snoc w z ∧ RightFreeAction.Reaches M z d := by
…
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word, OAI.PartitionConsistency.MergerAlgebra.RightFreeAction.Reaches
theorem OAI.PartitionConsistency.MergerAlgebra.Word.length_le_of_dvd line 306
theorem OAI.PartitionConsistency.MergerAlgebra.Word.snoc_not_dvd_prefix line 311
theorem OAI.PartitionConsistency.MergerAlgebra.Word.snoc_not_dvd_old line 317
theorem OAI.PartitionConsistency.MergerAlgebra.Word.snoc_dvd_snoc_iff line 323
theorem OAI.PartitionConsistency.MergerAlgebra.Word.snoc_cone_intersection line 338
Source documentation
With a fixed prefix, the intersection of two word cones is exactly controlled by the intersection of the final-letter cones in the right set.
```
theorem snoc_cone_intersection (w : Word M D) (z t j : D)
    (hj : ∀ d : D, RightFreeAction.Reaches M z d ∧ RightFreeAction.Reaches M t d ↔
      RightFreeAction.Reaches M j d) (a : Word M D) :
    snoc w z ∣ a ∧ snoc w t ∣ a ↔ snoc w j ∣ a := by
…
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word, OAI.PartitionConsistency.MergerAlgebra.RightFreeAction.Reaches
theorem OAI.PartitionConsistency.MergerAlgebra.Word.exists_cone_join line 353
Source documentation
Conditional joins for all normal forms, not only for translated copies. The induction is on the normal form of a common upper bound.
```
theorem exists_cone_join
    (hM : ∀ x y a : M, x ∣ a → y ∣ a → ∃ j : M, ∀ b : M, x ∣ b ∧ y ∣ b ↔ j ∣ b)
    (hD : RightFreeAction.HasConeJoins M D) (x y a : Word M D)
    (hx : x ∣ a) (hy : y ∣ a) :
    ∃ j : Word M D, ∀ b : Word M D, x ∣ b ∧ y ∣ b ↔ j ∣ b := by
…
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.RightFreeAction.HasConeJoins, OAI.PartitionConsistency.MergerAlgebra.Word
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.rel_mul line 387
Source documentation
Right multiplication respects the pair identifications themselves. No extra transitive closure is taken.
```
theorem rel_mul (P : OverlapPrescription M n) {z w : Fin n × M}
    (h : P.Rel z w) (m : M) :
    P.Rel (z.1, z.2 * m) (w.1, w.2 * m) := by
…
```
Mentions: OAI.PartitionConsistency.DiagramForcing.OverlapPrescription
def OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.copySetoid line 408
Source documentation
The quotient of the finitely many prescribed copies. Validity, rather than an equivalence closure, provides its setoid.
```
def copySetoid (P : OverlapPrescription M n) (hP : P.Valid) : Setoid (Fin n × M) :=
…
```
Mentions: OAI.PartitionConsistency.DiagramForcing.OverlapPrescription
def OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.Copies line 411
def OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.copy line 413
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.copy_eq_iff line 416
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.copy_injective line 420
def OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.copiesAct line 425
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.copiesAct_copy line 429
instance OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.copiesRightFreeAction line 435
Source documentation
The injective orbit maps in the prescribed quotient follow from left cancellation within a single original copy.
```
instance copiesRightFreeAction (P : OverlapPrescription M n) (hP : P.Valid) :
    MergerAlgebra.RightFreeAction M (P.Copies hP) where
…
```
Mentions: OAI.PartitionConsistency.DiagramForcing.OverlapPrescription, OAI.PartitionConsistency.MergerAlgebra.RightFreeAction
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.reaches_copy_iff line 459
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.reaches_same_copy_iff line 463
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.same_copy_cone_intersection line 473

theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.overlap_cone_intersection line 492

Source documentation

Intersections from different copies must pass through exactly the specified overlap: validity ensures that the quotient adds no other equality.

theorem overlap_cone_intersection (P : OverlapPrescription M n) (hP : P.Valid)
    {i j : Fin n} (hij : i ≠ j) {a b : M} (hab : P.start i j = some (a, b))
    (x y : M) (z : P.Copies hP) :
    Reaches M (P.copy hP i x) z ∧ Reaches M (P.copy hP j y) z ↔
      ∃ t : M, x ∣ a * t ∧ y ∣ b * t ∧ z = P.copy hP i (a * t) := by
…

Mentions: OAI.PartitionConsistency.DiagramForcing.OverlapPrescription

theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.copies_hasConeJoins line 517
Source documentation
Conditional joins in the actual prescribed quotient of copies. The sequential joins and their right quotients are constructed using only old conditional joins; failing any one of them means there was no common upper bound in the first place.
```
theorem copies_hasConeJoins (P : OverlapPrescription M n) (hP : P.Valid)
    (hM : ∀ x y a : M, x ∣ a → y ∣ a → ∃ j : M, ∀ b : M, x ∣ b ∧ y ∣ b ↔ j ∣ b) :
    HasConeJoins M (P.Copies hP) := by
…
```
Mentions: OAI.PartitionConsistency.DiagramForcing.OverlapPrescription
abbrev OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.Merger line 564
Source documentation
The extension is constructed, not postulated: its elements are the normal forms over the actual prescribed quotient.
```
abbrev Merger (P : OverlapPrescription M n) (hP : P.Valid) :=
…
```
Mentions: OAI.PartitionConsistency.DiagramForcing.OverlapPrescription
def OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.root line 568
Source documentation
The new roots which merge the original copies.
```
def root (P : OverlapPrescription M n) (hP : P.Valid) (i : Fin n) : P.Merger hP :=
…
```
Mentions: OAI.PartitionConsistency.DiagramForcing.OverlapPrescription
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.root_mul_old line 571
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.root_mul_eq_iff line 580
Source documentation
Exact realization of the given valid overlap prescription by left translations. The right-hand side is the original pair relation, not its transitive closure; no extra overlap is introduced.
```
theorem root_mul_eq_iff (P : OverlapPrescription M n) (hP : P.Valid)
    (z w : Fin n × M) :
    P.root hP z.1 * .old z.2 = P.root hP w.1 * .old w.2 ↔ P.Rel z w := by
…
```
Mentions: OAI.PartitionConsistency.DiagramForcing.OverlapPrescription
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.root_not_old line 587
Source documentation
New roots are genuinely new elements, even if an overlap identifies two of them with one another.
```
theorem root_not_old (P : OverlapPrescription M n) (hP : P.Valid)
    (i : Fin n) (x : M) : P.root hP i ≠ .old x := by
…
```
Mentions: OAI.PartitionConsistency.DiagramForcing.OverlapPrescription
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.merger_hasConditionalJoins line 592
Source documentation
All conditional joins in the constructed finite-copy merger.
```
theorem merger_hasConditionalJoins [DiagramOrder.IsConical M]
    (P : OverlapPrescription M n) (hP : P.Valid)
    (hM : DiagramOrder.HasConditionalJoins (DiagramOrder.LeftDivOrder M)) :
    DiagramOrder.HasConditionalJoins (DiagramOrder.LeftDivOrder (P.Merger hP)) := by
…
```
Mentions: OAI.PartitionConsistency.DiagramOrder.IsConical, OAI.PartitionConsistency.DiagramForcing.OverlapPrescription, OAI.PartitionConsistency.DiagramOrder.HasConditionalJoins, OAI.PartitionConsistency.DiagramOrder.LeftDivOrder
def OAI.PartitionConsistency.MergerAlgebra.Word.letters line 621
Source documentation
Finite coding of a normal form; only the existing coefficient and finitely many quotient letters are needed.
```
def letters : Word M D → List D
  | old _ => []
  | snoc w z => z :: letters w

/-- The normal-form encoding is injective, so no presentation-sized
collection beyond finite strings is required. -/
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word
theorem OAI.PartitionConsistency.MergerAlgebra.Word.code_injective line 627
Source documentation
The normal-form encoding is injective, so no presentation-sized collection beyond finite strings is required.
```
theorem code_injective : Function.Injective (fun w : Word M D => (leading w, letters w)) := by
…
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word, OAI.PartitionConsistency.MergerAlgebra.Word.leading, OAI.PartitionConsistency.MergerAlgebra.Word.letters
theorem OAI.PartitionConsistency.MergerAlgebra.Word.cardinal_le line 648
Source documentation
The scheduling bound for the normal forms.
```
theorem cardinal_le {μ : Cardinal.{u}} (hω : Cardinal.aleph0 ≤ μ)
    (hM : Cardinal.mk M ≤ μ) (hD : Cardinal.mk D ≤ μ) :
    Cardinal.mk (Word M D) ≤ μ := by
…
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.merger_cardinal_le line 666
Source documentation
A finite-copy merger preserves the source's infinite cardinal bound.
```
theorem merger_cardinal_le (P : OverlapPrescription M n) (hP : P.Valid)
    {μ : Cardinal.{u}} (hω : Cardinal.aleph0 ≤ μ) (hM : Cardinal.mk M ≤ μ) :
    Cardinal.mk (P.Merger hP) ≤ μ := by
…
```
Mentions: OAI.PartitionConsistency.DiagramForcing.OverlapPrescription