ProbeWords.lean`

122 declarations, 0 contain sorry, 0 declared as axioms

Probe extension: direct-limit letters and cancellative normal forms

structure OAI.PartitionConsistency.ProbeAlgebra.Path line 15
Source documentation
The actual nondecreasing sequence occurring in a probe datum. The transition and terminal factors will be derived, not additionally chosen.
```
structure Path (M : Type u) [LeftCancelMonoid M] (a : M) where
…
```
def OAI.PartitionConsistency.ProbeAlgebra.Path.factor line 25
Source documentation
The unique right factor between two nodes of the path.
```
noncomputable def factor (i j : ℕ) (h : i ≤ j) : M := (P.increasing h).choose
```
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.node_factor line 27
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.factor_self line 30
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.factor_trans line 34
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.factor_zero line 39
def OAI.PartitionConsistency.ProbeAlgebra.Path.terminal line 44
Source documentation
The unique terminal factor from a node to a.
```
noncomputable def terminal (i : ℕ) : M := (P.bounded i).choose
```
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.node_terminal line 46
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.factor_terminal line 49
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.terminal_zero line 54
def OAI.PartitionConsistency.ProbeAlgebra.Path.transition line 59
Source documentation
Right multiplication by a transition factor. This map is deliberately not assumed injective: the construction has only left cancellation.
```
noncomputable def transition (i j : ℕ) (h : i ≤ j) : M →[M] M where
…
```
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.transition_apply line 63
instance OAI.PartitionConsistency.ProbeAlgebra.Path.(instance at line 66) line 66
abbrev OAI.PartitionConsistency.ProbeAlgebra.Path.Letters line 71
Source documentation
The direct-limit letters [x,i] of the probe normal forms.
```
abbrev Letters := DirectLimit (fun _ : ℕ => M) P.transition
```
def OAI.PartitionConsistency.ProbeAlgebra.Path.letter line 75
Source documentation
The letter at a specified finite stage. Distinct stage elements need not have distinct images.
```
noncomputable def letter (i : ℕ) (x : M) : P.Letters := Quotient.mk _ ⟨i, x⟩
```

theorem OAI.PartitionConsistency.ProbeAlgebra.Path.letter_eq_iff line 78

Source documentation

Equality in the direct limit is equality at some common finite stage.

theorem letter_eq_iff (i j : ℕ) (x y : M) :
    P.letter i x = P.letter j y ↔
      ∃ k, ∃ hi : i ≤ k, ∃ hj : j ≤ k,
        x * P.factor i k hi = y * P.factor j k hj := Quotient.eq

theorem OAI.PartitionConsistency.ProbeAlgebra.Path.letter_transition line 83
def OAI.PartitionConsistency.ProbeAlgebra.Path.act line 88
Source documentation
Left multiplication commutes with the right transition maps.
```
noncomputable def act (x : M) : P.Letters → P.Letters :=
…
```
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.act_letter line 92
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.act_one line 95
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.act_mul line 101
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.act_injective line 110
Source documentation
Cancellation occurs at a common finite stage. No cancellation on the right, nor injectivity of transition maps, is used here.
```
theorem act_injective (x : M) : Function.Injective (P.act x) := by
…
```
def OAI.PartitionConsistency.ProbeAlgebra.Path.target line 123
Source documentation
The map k([x,i]) = x c_i; compatibility uses the terminal-factor identity, not an incorrectly presumed injective transition map.
```
noncomputable def target : P.Letters → M :=
…
```
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.target_letter line 127
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.target_act line 130
def OAI.PartitionConsistency.ProbeAlgebra.Path.exit line 138
Source documentation
The old element h(s) = k(s)e at which a letter can be consumed.
```
noncomputable def exit (e : M) (s : P.Letters) : M := P.target s * e
```
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.exit_act line 140
def OAI.PartitionConsistency.ProbeAlgebra.Path.InCone line 145
Source documentation
Membership in an old left-translation cone of letters.
```
def InCone (x : M) (s : P.Letters) : Prop := ∃ t : P.Letters, P.act x t = s
```
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.inCone_letter_iff line 149
Source documentation
Cone membership can also be tested at a finite stage, retaining the actual quotient rather than just the existence of an old comparison.
```
theorem inCone_letter_iff (x : M) (i : ℕ) (y : M) :
    P.InCone x (P.letter i y) ↔
      ∃ j, ∃ hij : i ≤ j, x ∣ y * P.factor i j hij := by
…
```
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.dvd_target_of_inCone line 162
Source documentation
Every old divisor of a letter divides its target.
```
theorem dvd_target_of_inCone {x : M} {s : P.Letters} (h : P.InCone x s) : x ∣ P.target s := by
…
```
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.one_inCone line 166
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.inCone_of_dvd line 168
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.inCone_intersection line 176
Source documentation
Old cone intersections lift exactly to the direct limit, including empty intersections.
```
theorem inCone_intersection (x y j : M)
    (hj : ∀ z : M, x ∣ z ∧ y ∣ z ↔ j ∣ z) (s : P.Letters) :
    P.InCone x s ∧ P.InCone y s ↔ P.InCone j s := by
…
```
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.old_common_multiple_of_cones line 199
Source documentation
If two old cones meet in the letters, the old monoid already contains a common right multiple. Thus a new letter creates no old nonjoin.
```
theorem old_common_multiple_of_cones {x y : M} {s : P.Letters}
    (hx : P.InCone x s) (hy : P.InCone y s) : ∃ z : M, x ∣ z ∧ y ∣ z :=
…
```
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.initial_profile line 205
Source documentation
The initial new letter has exactly the old-divisor profile given by the lower closure of the original countable path.
```
theorem initial_profile (x : M) : P.InCone x (P.letter 0 1) ↔ ∃ i : ℕ, x ∣ P.node i := by
…
```
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.head_separation line 211
Source documentation
The important separation between a head and its exit cone. It uses conicality and left cancellation, but does not use right cancellation.
```
theorem head_separation [IsConical M] {e : M} (he : e ≠ 1) (s : P.Letters) :
    ¬ P.InCone (P.exit e s) s := by
…
```
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.letters_cardinal_le line 221
Source documentation
Countably many old copies suffice for the direct-limit alphabet.
```
theorem letters_cardinal_le {μ : Cardinal.{u}} (hω : Cardinal.aleph0 ≤ μ)
    (hM : Cardinal.mk M ≤ μ) : Cardinal.mk P.Letters ≤ μ := by
…
```
structure OAI.PartitionConsistency.ProbeAlgebra.Alphabet line 238
Source documentation
The letter action and exit map used in the terminating probe normal forms. These laws will be realized by the path direct limit above.
```
structure Alphabet (M : Type u) (S : Type v) [Monoid M] where
…
```
def OAI.PartitionConsistency.ProbeAlgebra.Path.alphabet line 251
Source documentation
The direct limit supplies all the alphabet laws for the probe extension.
```
noncomputable def alphabet (P : Path M a) (he : e ≠ 1) : Alphabet M P.Letters where
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Path, OAI.PartitionConsistency.ProbeAlgebra.Alphabet

inductive OAI.PartitionConsistency.ProbeAlgebra.Raw line 262

Source documentation

Unreduced strings, including a compulsory terminal old factor.

inductive Raw (M : Type u) (S : Type v) : Type (max u v)
  | old : M → Raw M S
  | cons : S → Raw M S → Raw M S

namespace Raw
variable {M : Type u} {S : Type v} [Monoid M] (A : Alphabet M S)

Mentions: OAI.PartitionConsistency.ProbeAlgebra.Alphabet

def OAI.PartitionConsistency.ProbeAlgebra.Raw.headDiv line 269
def OAI.PartitionConsistency.ProbeAlgebra.Raw.reduced line 273
def OAI.PartitionConsistency.ProbeAlgebra.Raw.oldAct line 277
theorem OAI.PartitionConsistency.ProbeAlgebra.Raw.oldAct_one line 281
theorem OAI.PartitionConsistency.ProbeAlgebra.Raw.oldAct_mul line 286
theorem OAI.PartitionConsistency.ProbeAlgebra.Raw.reduced_oldAct line 292
theorem OAI.PartitionConsistency.ProbeAlgebra.Raw.headDiv_iff line 295
theorem OAI.PartitionConsistency.ProbeAlgebra.Raw.oldAct_injective line 315
abbrev OAI.PartitionConsistency.ProbeAlgebra.Word line 327
Source documentation
Literal irreducibles for the reductions s(bZ) ↦ h(s)Z.
```
abbrev Word {M : Type u} {S : Type v} [Monoid M] (A : Alphabet M S) (b : M) :=
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Alphabet
def OAI.PartitionConsistency.ProbeAlgebra.Word.old line 333
def OAI.PartitionConsistency.ProbeAlgebra.Word.headDiv line 335
def OAI.PartitionConsistency.ProbeAlgebra.Word.cons line 337
def OAI.PartitionConsistency.ProbeAlgebra.Word.oldAct line 340
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.oldAct_old line 343
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.oldAct_one line 345
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.oldAct_mul line 348
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.oldAct_cons line 352
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.old_inj line 355
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.cons_inj line 360
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.oldAct_injective line 369
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.headDiv_iff line 372
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.headDiv_oldAct line 382
def OAI.PartitionConsistency.ProbeAlgebra.Word.quotient line 385
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.oldAct_quotient line 388
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.quotient_oldAct line 391
def OAI.PartitionConsistency.ProbeAlgebra.Word.letterAct line 397
Source documentation
Prepending a letter performs its only possible front reduction.
```
noncomputable def letterAct (s : S) (w : Word A b) : Word A b := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.letterAct_of_headDiv line 402
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.letterAct_of_not_headDiv line 405
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.letterAct_oldAct_b line 408
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.oldAct_letterAct line 412
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.not_headDiv_exit_cons line 419
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.oldAct_exit_ne_cons line 423
Source documentation
The two branches of prepending have disjoint ranges by head separation.
```
theorem oldAct_exit_ne_cons (s : S) (v w : Word A b) (hw) :
    oldAct A b (A.exit s) v ≠ cons A b s w hw := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.oldAct, OAI.PartitionConsistency.ProbeAlgebra.Word.cons
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.letterAct_injective line 428
def OAI.PartitionConsistency.ProbeAlgebra.Raw.eval line 453
Source documentation
Evaluate a word by its successive left multipliers.
```
noncomputable def eval : Raw M S → Word A b → Word A b
  | .old x, w => Word.oldAct A b x w
  | .cons s v, w => Word.letterAct A b s (eval v w)
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Raw, OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.oldAct, OAI.PartitionConsistency.ProbeAlgebra.Word.letterAct
theorem OAI.PartitionConsistency.ProbeAlgebra.Raw.eval_oldAct line 457
theorem OAI.PartitionConsistency.ProbeAlgebra.Raw.eval_injective line 463
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.eval_oldAct line 472
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.eval_letterAct line 476
def OAI.PartitionConsistency.ProbeAlgebra.Word.mul line 486
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.old_mul line 488
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.cons_mul line 491
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.mul_assoc line 494
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.mul_one line 504
instance OAI.PartitionConsistency.ProbeAlgebra.Word.(instance at line 515) line 515
instance OAI.PartitionConsistency.ProbeAlgebra.Word.(instance at line 522) line 522
def OAI.PartitionConsistency.ProbeAlgebra.Word.oldHom line 526
Source documentation
A literal conservative homomorphism of old elements into probe normal forms.
```
noncomputable def oldHom : M →* Word A b where
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.oldHom_apply line 531
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.oldHom_injective line 533
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.old_mul_eq_old_iff line 536
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.old_dvd_old_iff line 553
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.old_dvd_iff_headDiv line 561
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.exit_ne_one line 567
Source documentation
Having no old nontrivial unit prevents a letter from being consumed into 1.
```
theorem exit_ne_one (s : S) : A.exit s ≠ 1 := by
…
```
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.oldAct_exit_ne_one line 571
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.letterAct_ne_one line 577
instance OAI.PartitionConsistency.ProbeAlgebra.Word.(instance at line 588) line 588
def OAI.PartitionConsistency.ProbeAlgebra.Word.generator line 600
Source documentation
The new generator represented by a letter, with terminal identity.
```
def generator [IsConical M] (hb : b ≠ 1) (s : S) : Word A b :=
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.generator_mul line 605
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.generator_mul_b line 610
def OAI.PartitionConsistency.ProbeAlgebra.Word.evalHom line 628
Source documentation
Evaluation in any monoid satisfying the letter equivariance and exit relations. This will give the presentation's universal property.
```
def evalHom : Raw M S → N
  | .old x => f x
  | .cons s v => q s * evalHom v

variable (heq : ∀ x s, q (A.act x s) = f x * q s)
  (hexit : ∀ s, q s * f b = f (A.exit s))

include heq in
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Raw, OAI.PartitionConsistency.ProbeAlgebra.Word.old, OAI.PartitionConsistency.ProbeAlgebra.Word.cons
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.evalHom_oldAct line 636
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.evalHom_letterAct line 643
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.evalHom_mul line 657
def OAI.PartitionConsistency.ProbeAlgebra.Word.liftHom line 669
Source documentation
No extra relations were introduced by using irreducibles: any model of the displayed reductions and old-action relation admits this homomorphism.
```
noncomputable def liftHom : Word A b →* N where
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.liftHom_old line 674
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.liftHom_generator line 677
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.generator_mul_of_not_headDiv line 683
Source documentation
A same-headed normal form is literally a generator times its suffix.
```
theorem generator_mul_of_not_headDiv [IsConical M] (hb : b ≠ 1)
    (s : S) (v : Word A b) (hv : ¬ headDiv A b b v) :
    generator A b hb s * v = cons A b s v hv :=
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.headDiv, OAI.PartitionConsistency.ProbeAlgebra.Word.generator, OAI.PartitionConsistency.ProbeAlgebra.Word.cons
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.hom_ext line 688
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.exit_dvd_of_letterAct_eq_old line 704
Source documentation
Any product with a letter that is old must have gone through its exit.
```
theorem exit_dvd_of_letterAct_eq_old (s : S) (v : Word A b) {y : M}
    (hy : letterAct A b s v = old A b y) : A.exit s ∣ y := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.letterAct, OAI.PartitionConsistency.ProbeAlgebra.Word.old
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.generator_dvd_old_iff line 716
Source documentation
The gate of a single letter is its exit. The right factor b witnesses attainment rather than a merely limiting old upper bound.
```
theorem generator_dvd_old_iff [IsConical M] (hb : b ≠ 1) (s : S) (y : M) :
    generator A b hb s ∣ old A b y ↔ A.exit s ∣ y := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.generator, OAI.PartitionConsistency.ProbeAlgebra.Word.old
abbrev OAI.PartitionConsistency.ProbeAlgebra.Path.Extension line 732

theorem OAI.PartitionConsistency.ProbeAlgebra.Path.old_cone_intersection line 735

Source documentation

Preservation of the entire old-cone intersection, in every new word.

theorem old_cone_intersection (x y j : M)
    (hj : ∀ z : M, x ∣ z ∧ y ∣ z ↔ j ∣ z) (w : P.Extension he b) :
    Word.old (P.alphabet he) b x ∣ w ∧ Word.old (P.alphabet he) b y ∣ w ↔
      Word.old (P.alphabet he) b j ∣ w := by
…

Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.old

theorem OAI.PartitionConsistency.ProbeAlgebra.Path.common_multiple_reflection line 747
Source documentation
A new probe word cannot create a common multiple for two disjoint old cones, even though it may itself divide an old element.
```
theorem common_multiple_reflection {x y : M} {w : P.Extension he b}
    (hx : Word.old (P.alphabet he) b x ∣ w) (hy : Word.old (P.alphabet he) b y ∣ w) :
    ∃ z : M, x ∣ z ∧ y ∣ z := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.old
def OAI.PartitionConsistency.ProbeAlgebra.Path.probe line 758
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.probe_mul_b line 763
Source documentation
The prescribed old right factor sends every adjoined path probe to its specified old exit.
```
theorem probe_mul_b (i : ℕ) :
    P.probe he b hb i * Word.old (P.alphabet he) b b =
      Word.old (P.alphabet he) b (P.terminal i * e) := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.old
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.probe_zero_mul_b line 770
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.probe_transition line 776
Source documentation
The transition relations are genuine equalities in these normal forms.
```
theorem probe_transition {i j : ℕ} (hij : i ≤ j) :
    Word.old (P.alphabet he) b (P.factor i j hij) * P.probe he b hb j =
      P.probe he b hb i := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.old
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.probe_old_profile line 785
Source documentation
Precisely the old elements in the countable lower closure divide p₀.
```
theorem probe_old_profile (x : M) :
    Word.old (P.alphabet he) b x ∣ P.probe he b hb 0 ↔ ∃ i, x ∣ P.node i := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.old
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.probe_not_dvd_a line 791
Source documentation
No right cancellation is needed to show the probe is not below a.
```
theorem probe_not_dvd_a :
    ¬ P.probe he b hb 0 ∣ Word.old (P.alphabet he) b a := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.old
def OAI.PartitionConsistency.ProbeAlgebra.Raw.code line 807
theorem OAI.PartitionConsistency.ProbeAlgebra.Raw.code_injective line 811
theorem OAI.PartitionConsistency.ProbeAlgebra.Raw.cardinal_le line 827
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.extension_cardinal_le line 842
Source documentation
The probe extension also respects the infinite scheduling bound.
```
theorem extension_cardinal_le {μ : Cardinal.{u}} (hω : Cardinal.aleph0 ≤ μ)
    (hM : Cardinal.mk M ≤ μ) : Cardinal.mk (P.Extension he b) ≤ μ :=
…
```