LeanPool.Polylean.ConjInvLength.ProvedBound

structure LeanPool.Polylean.ProvedSplit (l : Letter) (w : Word) : Type

A split of a word around a distinguished letter, with a proof of reconstruction.

• fst : Word

  The part before the distinguished letter.

• snd : Word

  The part after the distinguished letter.

• proof : w = self.fst ++ [l] ++ self.snd

  Reconstruction proof for the split.

def LeanPool.Polylean.ProvedSplit.head (x : Letter) (ys : Word) : ProvedSplit x (x :: ys)

Split with the first piece empty when the head matches the splitting letter.

Equations

• LeanPool.Polylean.ProvedSplit.head x ys = { fst := [], snd := ys, proof := ⋯ }

def LeanPool.Polylean.ProvedSplit.prepend {l : Letter} {ys : Word} (x : Letter) (ps : ProvedSplit l ys) : ProvedSplit l (x :: ys)

Prepend a letter to the first component of a proved split.

Equations

• LeanPool.Polylean.ProvedSplit.prepend x ps = { fst := x :: ps.fst, snd := ps.snd, proof := ⋯ }

def LeanPool.Polylean.provedSplits (z : Letter) (w : Word) : List (ProvedSplit z w)

All proved splits of a word around a letter.

Equations

• One or more equations did not get rendered due to their size.
• LeanPool.Polylean.provedSplits z [] = []

@[reducible, inline]

abbrev LeanPool.Polylean.Length : Type

A length function on words.

Equations

• LeanPool.Polylean.Length = (LeanPool.Polylean.Word → ℕ)

def LeanPool.Polylean.conjInv (l : Length) : Prop

A length function invariant under conjugation by letters.

Equations

• LeanPool.Polylean.conjInv l = ∀ (x : LeanPool.Polylean.Letter) (g : LeanPool.Polylean.Word), l (g ^ x) = l g

def LeanPool.Polylean.triangIneq (l : Length) : Prop

The triangle inequality for a length function.

Equations

• LeanPool.Polylean.triangIneq l = ∀ (g h : LeanPool.Polylean.Word), l (g ++ h) ≤ l g + l h

def LeanPool.Polylean.normalized (l : Length) : Prop

A length function normalized on single letters.

Equations

• LeanPool.Polylean.normalized l = ∀ (x : LeanPool.Polylean.Letter), l [x] = 1

def LeanPool.Polylean.emptyWord (l : Length) : Prop

A length function that sends the empty word to zero.

Equations

• LeanPool.Polylean.emptyWord l = (l [] = 0)

structure LeanPool.Polylean.ProvedBound (g : Word) : Type

A certified upper bound for the length of a word.

• bound : ℕ

  The numeric upper bound.

• pf (l : Length) : Polylean.emptyWord l → normalized l → conjInv l → triangIneq l → l g ≤ self.bound

  The proof that every normalized conjugation-invariant length is bounded by bound.

theorem LeanPool.Polylean.conj_split (x : Letter) (ys fst snd : Word) : ys = fst ++ [x⁻¹] ++ snd → x :: ys = fst ^ x ++ snd

def LeanPool.Polylean.ProvedBound.headMatches (x : Letter) (ys fst snd : Word) (eqn : ys = fst ++ [x⁻¹] ++ snd) : ProvedBound fst → ProvedBound snd → ProvedBound (x :: ys)

Combine certified bounds across a split around a conjugating letter.

Equations

• LeanPool.Polylean.ProvedBound.headMatches x ys fst snd eqn pb1 pb2 = { bound := pb1.bound + pb2.bound, pf := ⋯ }

def LeanPool.Polylean.ProvedBound.prepend {w : Word} (x : Letter) (ps : ProvedBound w) : ProvedBound (x :: w)

Prepend a letter to a certified bound.

Equations

• LeanPool.Polylean.ProvedBound.prepend x ps = { bound := ps.bound + 1, pf := ⋯ }

def LeanPool.Polylean.ProvedBound.emptyWord : ProvedBound []

The zero bound for the empty word.

Equations

• LeanPool.Polylean.ProvedBound.emptyWord = { bound := 0, pf := LeanPool.Polylean.ProvedBound.emptyWord._proof_1 }

def LeanPool.Polylean.ProvedBound.min {w : Word} : ProvedBound w → List (ProvedBound w) → ProvedBound w

Choose the better bound from a nonempty list of alternatives.

Equations

• head.min tail = List.foldl (fun (pb1 pb2 : LeanPool.Polylean.ProvedBound w) => if pb1.bound ≤ pb2.bound then pb1 else pb2) head tail

theorem LeanPool.Polylean.splitFirst {l : Letter} {w : Word} (ps : ProvedSplit l w) : List.length ps.fst + 1 ≤ List.length w

theorem LeanPool.Polylean.splitSecond {l : Letter} {w : Word} (ps : ProvedSplit l w) : List.length ps.snd + 1 ≤ List.length w

@[irreducible]

def LeanPool.Polylean.provedBound (w : Word) : ProvedBound w

Compute a certified length bound for a word.

Equations

• One or more equations did not get rendered due to their size.
• LeanPool.Polylean.provedBound [] = LeanPool.Polylean.ProvedBound.emptyWord