ProbeGates.lean`

48 declarations, 0 contain sorry, 0 declared as axioms

Probe extension: all gates, conditional joins, and presentation

def OAI.PartitionConsistency.ProbeAlgebra.Raw.head line 13
def OAI.PartitionConsistency.ProbeAlgebra.Raw.length line 17
def OAI.PartitionConsistency.ProbeAlgebra.Word.head line 25
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.head_old line 27
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.head_cons line 28
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.head_eq_none_iff line 32
Source documentation
The first-letter blocks and the old elements partition the irreducibles.
```
theorem head_eq_none_iff (w : Word A b) :
    head A b w = none ↔ ∃ x, w = old A b x := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.head, OAI.PartitionConsistency.ProbeAlgebra.Word.old
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.head_eq_some_iff line 42
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.headDiv_of_head_eq_some line 60
Source documentation
Membership in an old cone depends only on the head of a new form.
```
theorem headDiv_of_head_eq_some {x : M} {w : Word A b} {s : S}
    (hw : head A b w = some s) : headDiv A b x w ↔ ∃ t, A.act x t = s := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.head, OAI.PartitionConsistency.ProbeAlgebra.Word.headDiv
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.headDiv_of_same_head line 65
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.head_oldAct_exit_ne line 70
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.head_letterAct_ne_iff line 78
Source documentation
A prepended letter exits its original block exactly when its input is in the distinguished old b-cone.
```
theorem head_letterAct_ne_iff (s : S) (w : Word A b) :
    head A b (letterAct A b s w) ≠ some s ↔ headDiv A b b w := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.head, OAI.PartitionConsistency.ProbeAlgebra.Word.letterAct, OAI.PartitionConsistency.ProbeAlgebra.Word.headDiv
def OAI.PartitionConsistency.ProbeAlgebra.Word.Gate line 89
Source documentation
A gate is an old generator for precisely the part of a right cone lying outside its word's first-letter block.
```
def Gate (w : Word A b) (s : S) (g : M) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.Gate.dvd line 92
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.Gate.head_ne line 95
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.Gate.dvd_old_iff line 99
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.Gate.old_intersection line 106
Source documentation
An old cone either contains a whole first-letter block or is disjoint from that block; in the latter case it sees only the gate of a word.
```
theorem Gate.old_intersection {w : Word A b} {s : S} {g x : M}
    (hg : Gate A b w s g) (hw : head A b w = some s)
    (hx : ¬ headDiv A b x w) (z : Word A b) :
    old A b x ∣ z ∧ w ∣ z ↔ old A b x ∣ z ∧ old A b g ∣ z := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.Gate, OAI.PartitionConsistency.ProbeAlgebra.Word.head, OAI.PartitionConsistency.ProbeAlgebra.Word.headDiv, OAI.PartitionConsistency.ProbeAlgebra.Word.old
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.gate_of_suffix_intersection line 120
Source documentation
A principal old intersection for the suffix computes the exit cone of the word. The quotient u is an old right factor of the intersection.
```
theorem gate_of_suffix_intersection (s : S) (Y : Word A b)
    (hY : ¬ headDiv A b b Y) (u : M)
    (hI : ∀ z : Word A b,
      Y ∣ z ∧ old A b b ∣ z ↔ old A b (b * u) ∣ z) :
    Gate A b (cons A b s Y hY) s (A.exit s * u) := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.headDiv, OAI.PartitionConsistency.ProbeAlgebra.Word.old, OAI.PartitionConsistency.ProbeAlgebra.Word.Gate, OAI.PartitionConsistency.ProbeAlgebra.Word.cons
def OAI.PartitionConsistency.ProbeAlgebra.Word.OldIntersections line 157
Source documentation
Only old cone intersections are required for the recursive gate calculation. The path alphabet supplies this law from old conditional joins.
```
def OldIntersections : Prop :=
…
```
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.exists_gate_of_exit line 164
Source documentation
Every genuine exit of a new word determines a least old right-multiple cone. This induction is on literal suffix length, not on a presumed join operation for new words.
```
theorem exists_gate_of_exit (hOld : OldIntersections A b) (w : Word A b)
    {s : S} (hs : head A b w = some s) {z : Word A b}
    (hwz : w ∣ z) (hz : head A b z ≠ some s) :
    ∃ g : M, Gate A b w s g := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.OldIntersections, OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.head, OAI.PartitionConsistency.ProbeAlgebra.Word.Gate
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.append_old_exit_isOld line 211
Source documentation
An old right multiplier can leave the first-letter block only after all the intervening letters have been consumed. Thus an exit obtained by such a multiplier is itself old.
```
theorem append_old_exit_isOld (w : Word A b) {s : S}
    (hs : head A b w = some s) (d : M)
    (hex : head A b (w * old A b d) ≠ some s) :
    ∃ y : M, w * old A b d = old A b y := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.head, OAI.PartitionConsistency.ProbeAlgebra.Word.old
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.Gate.append_old line 250
Source documentation
The actual least-old-multiple rule required for the later descending birth-ordinal argument.
```
theorem Gate.append_old {w : Word A b} {s : S} {g : M}
    (hg : Gate A b w s g) (hs : head A b w = some s) (d : M)
    (hd : old A b g ∣ w * old A b d) :
    ∃ y : M, w * old A b d = old A b y :=
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.Gate, OAI.PartitionConsistency.ProbeAlgebra.Word.head, OAI.PartitionConsistency.ProbeAlgebra.Word.old
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.dvd_of_different_head line 258
Source documentation
A common multiple in one first-letter block forces every different- headed divisor of that multiple to divide the entire block.
```
theorem dvd_of_different_head (hOld : OldIntersections A b)
    {w v z : Word A b} {s t : S}
    (hw : head A b w = some s) (hv : head A b v = some t) (hst : s ≠ t)
    (hvz : v ∣ z) (hz : head A b z = some s) : v ∣ w := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.OldIntersections, OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.head
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.dvd_of_other_block line 272
Source documentation
Old divisors and differently headed new divisors both divide an entire block as soon as they divide one member of that block.
```
theorem dvd_of_other_block (hOld : OldIntersections A b)
    {w v z : Word A b} {s : S}
    (hw : head A b w = some s) (hv : head A b v ≠ some s)
    (hvz : v ∣ z) (hz : head A b z = some s) : v ∣ w := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.OldIntersections, OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.head
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.old_word_cone_join line 287
Source documentation
The nonempty intersection of an old cone and any new cone is computed by an old join, unless the old element already divides the word.
```
theorem old_word_cone_join (hOld : OldIntersections A b) (x : M) (w z : Word A b)
    (hxz : old A b x ∣ z) (hwz : w ∣ z) :
    ∃ j : Word A b, ∀ q : Word A b, old A b x ∣ q ∧ w ∣ q ↔ j ∣ q := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.OldIntersections, OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.old
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.different_head_cone_join line 309
Source documentation
Distinct incomparable first-letter blocks can meet only through both of their gates, and the old cone law computes that intersection.
```
theorem different_head_cone_join (hOld : OldIntersections A b)
    {w v z : Word A b} {s t : S}
    (hw : head A b w = some s) (hv : head A b v = some t) (hst : s ≠ t)
    (hwz : w ∣ z) (hvz : v ∣ z) :
    ∃ j : Word A b, ∀ q, w ∣ q ∧ v ∣ q ↔ j ∣ q := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.OldIntersections, OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.head

theorem OAI.PartitionConsistency.ProbeAlgebra.translate_cone_intersection line 340

Source documentation

Left translation preserves an exact cone-intersection equation in a left-cancellative monoid.

theorem translate_cone_intersection {N : Type*} [LeftCancelMonoid N]
    (c x y j : N) (hj : ∀ q, x ∣ q ∧ y ∣ q ↔ j ∣ q) :
    ∀ q, c * x ∣ q ∧ c * y ∣ q ↔ c * j ∣ q := by
…

theorem OAI.PartitionConsistency.ProbeAlgebra.Word.cone_join line 360
Source documentation
All new conditional joins exist. Only the old cone theorem was used in constructing gates; no intermediate join theorem is assumed.
```
theorem cone_join (hOld : OldIntersections A b) (w v z : Word A b)
    (hwz : w ∣ z) (hvz : v ∣ z) :
    ∃ j : Word A b, ∀ q, w ∣ q ∧ v ∣ q ↔ j ∣ q := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.OldIntersections, OAI.PartitionConsistency.ProbeAlgebra.Word
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.oldIntersections line 407
Source documentation
The old cone law used above is realized by the path alphabet.
```
theorem oldIntersections (hM : HasConditionalJoins (LeftDivOrder M)) :
    Word.OldIntersections (P.alphabet he) b := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.OldIntersections
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.extension_hasConditionalJoins line 416
Source documentation
Conditional joins in the actual probe extension, not just in the old monoid or in the direct-limit alphabet.
```
theorem extension_hasConditionalJoins (hM : HasConditionalJoins (LeftDivOrder M)) (hb : b ≠ 1) :
    HasConditionalJoins (LeftDivOrder (P.Extension he b)) := by
…
```
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.generator_gate line 439
Source documentation
The exit of a one-letter probe is not merely a lower bound on its old multiples: the entire exit cone is its precise gate cone.
```
theorem generator_gate (s : S) : Gate A b (generator A b hb s) s (A.exit s) := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.Gate, OAI.PartitionConsistency.ProbeAlgebra.Word.generator
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.generator_dvd_of_head line 449
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.old_factor_of_other_block line 457
Source documentation
Entering a differently headed block factors through one old element, including the case where the entering divisor was old to begin with.
```
theorem old_factor_of_other_block (hOld : OldIntersections A b)
    {w z : Word A b} {s : S} (hw : head A b w ≠ some s)
    (hz : head A b z = some s) (hwz : w ∣ z) :
    ∃ g : M, w ∣ old A b g ∧ old A b g ∣ z := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.OldIntersections, OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.head, OAI.PartitionConsistency.ProbeAlgebra.Word.old
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.probe_zero_gate line 479
Source documentation
The gate of the initial probe is exactly the specified old ae.
```
theorem probe_zero_gate : Word.Gate (P.alphabet he) b
    (P.probe he b hb 0) (P.letter 0 1) (a * e) := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.Gate
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.head_ne_initial_of_dvd_a line 487
Source documentation
No divisor of a, whether old or newly created, belongs to the first- letter block of the initial probe.
```
theorem head_ne_initial_of_dvd_a {w : P.Extension he b}
    (hwa : w ∣ Word.old (P.alphabet he) b a) :
    Word.head (P.alphabet he) b w ≠ some (P.letter 0 1) := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.old, OAI.PartitionConsistency.ProbeAlgebra.Word.head
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.probe_full_profile line 497
Source documentation
The full divisor profile of the initial probe, including the newly created divisors of a. This is equality of the actual two downsets in the extension, not only agreement on the old submonoid.
```
theorem probe_full_profile (hM : HasConditionalJoins (LeftDivOrder M)) (w : P.Extension he b) :
    w ∣ P.probe he b hb 0 ∧ w ∣ Word.old (P.alphabet he) b a ↔
      ∃ i : ℕ, w ∣ Word.old (P.alphabet he) b (P.node i) := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.old

theorem OAI.PartitionConsistency.ProbeAlgebra.Path.probe_join_profile line 514

Source documentation

Every divisor of a outside the probe's downset has join ae with the probe. Both old and new divisors are covered.

theorem probe_join_profile (hM : HasConditionalJoins (LeftDivOrder M))
    {w : P.Extension he b} (hwa : w ∣ Word.old (P.alphabet he) b a)
    (hwm : ¬ w ∣ P.probe he b hb 0) (z : P.Extension he b) :
    w ∣ z ∧ P.probe he b hb 0 ∣ z ↔ Word.old (P.alphabet he) b (a * e) ∣ z := by
…

Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.old

theorem OAI.PartitionConsistency.ProbeAlgebra.Path.probe_join_isLUB line 532

Source documentation

Explicitly, ae is the order-theoretic least upper bound required by the last line of the probe-algebra lemma.

theorem probe_join_isLUB (hM : HasConditionalJoins (LeftDivOrder M))
    {w : LeftDivOrder (P.Extension he b)} (hwa : w ∣ Word.old (P.alphabet he) b a)
    (hwm : ¬ w ∣ P.probe he b hb 0) :
    IsLUB (α := LeftDivOrder (P.Extension he b)) {w, P.probe he b hb 0} (Word.old (P.alphabet he) b (a * e)) := by
…

Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.old

theorem OAI.PartitionConsistency.ProbeAlgebra.Path.least_old_multiple line 545

Source documentation

Every new word with an old right multiple has a least old right multiple, and multiplication by an old element past its gate is old.

theorem least_old_multiple (hM : HasConditionalJoins (LeftDivOrder M))
    {w : P.Extension he b} (hw : ¬ ∃ y : M, w = Word.old (P.alphabet he) b y)
    {y : M} (hy : w ∣ Word.old (P.alphabet he) b y) :
    ∃ g : M, w ∣ Word.old (P.alphabet he) b g ∧
      (∀ z : M, w ∣ Word.old (P.alphabet he) b z ↔ g ∣ z) ∧
      (∀ d : M, Word.old (P.alphabet he) b g ∣ w * Word.old (P.alphabet he) b d →
        ∃ z : M, w * Word.old (P.alphabet he) b d = Word.old (P.alphabet he) b z) := by
…

Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.old

theorem OAI.PartitionConsistency.ProbeAlgebra.Path.transitions_from_adjacent line 573
Source documentation
Adjacent transition relations imply every finite-stage transition relation, without any right cancellation in either monoid.
```
theorem transitions_from_adjacent
    (hp : ∀ i, p i = f (P.factor i (i+1) (Nat.le_succ i)) * p (i+1))
    (i j : ℕ) (hij : i ≤ j) : p i = f (P.factor i j hij) * p j := by
…
```
def OAI.PartitionConsistency.ProbeAlgebra.Path.interpretedLetter line 591
Source documentation
A family satisfying the original presentation's transition relations induces its equivariant interpretation on direct-limit letters.
```
noncomputable def interpretedLetter : P.Letters → N :=
…
```
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.interpretedLetter_mk line 598
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.interpretedLetter_act line 602
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.interpretedLetter_exit line 611
def OAI.PartitionConsistency.ProbeAlgebra.Path.presentedLift line 622
Source documentation
Universal evaluation for exactly the indexed probe presentation from the source: no gate, join, normal-form, or height law is imposed on the target monoid.
```
noncomputable def presentedLift : P.Extension he b →* N :=
…
```
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.presentedLift_old line 626
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.presentedLift_probe line 629
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.presentedHom_ext line 636
Source documentation
Old elements and the displayed indexed generators determine every homomorphism out of the actual extension.
```
theorem presentedHom_ext (hb : b ≠ 1) (F G : P.Extension he b →* N)
    (hOld : ∀ x : M, F (Word.old (P.alphabet he) b x) = G (Word.old (P.alphabet he) b x))
    (hNew : ∀ i : ℕ, F (P.probe he b hb i) = G (P.probe he b hb i)) : F = G := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.old
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.existsUnique_presentedHom line 656
Source documentation
The actual extension has the universal property of the source's monoid presentation over M.
```
theorem existsUnique_presentedHom (hb : b ≠ 1) :
    ∃! F : P.Extension he b →* N,
      (∀ x : M, F (Word.old (P.alphabet he) b x) = f x) ∧
      (∀ i : ℕ, F (P.probe he b hb i) = p i) := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.old