2607.20401v1 / ConjugatorLength/Main.lean

all files

import ConjugatorLength.Heisenberg

/-!
# The quadratic conjugator-length theorem

This file defines the paper's function literally from finite words and proves
that it is equivalent, in the paper's comparison relation, to `n ↦ n²`.
-/

namespace ConjugatorLength.Heisenberg

/-- The minimum standard word length of a conjugator.  It is set to zero for a
non-conjugate pair; those pairs are ignored by the global definition below. -/
noncomputable def pairConjugatorLength (u v : Heisenberg) : ℕ := by
  classical
  exact if h : Conjugate u v then
    Nat.find
      (show ∃ n : ℕ, ∃ w : Heisenberg, IsConjugator u v w ∧ wordLength w = n from
        let ⟨w, hw⟩ := h
        ⟨wordLength w, w, hw, rfl⟩)
  else 0

theorem pairConjugatorLength_spec {u v : Heisenberg} (h : Conjugate u v) :
    ∃ w, IsConjugator u v w ∧ wordLength w = pairConjugatorLength u v := by
  classical
  rw [pairConjugatorLength, dif_pos h]
  exact Nat.find_spec
    (show ∃ n : ℕ, ∃ w : Heisenberg, IsConjugator u v w ∧ wordLength w = n from
      let ⟨w, hw⟩ := h
      ⟨wordLength w, w, hw, rfl⟩)

theorem pairConjugatorLength_le_of {u v w : Heisenberg}
    (hw : IsConjugator u v w) :
    pairConjugatorLength u v ≤ wordLength w := by
  classical
  have h : Conjugate u v := ⟨w, hw⟩
  rw [pairConjugatorLength, dif_pos h]
  apply Nat.find_min'
  exact ⟨w, hw, rfl⟩

theorem pairConjugatorLength_eq_zero_of_not_conjugate {u v : Heisenberg}
    (h : ¬Conjugate u v) :
    pairConjugatorLength u v = 0 := by
  simp [pairConjugatorLength, h]

theorem pairConjugatorLength_le_quadratic {u v : Heisenberg} {n : ℕ}
    (hlen : wordLength u + wordLength v ≤ n) :
    pairConjugatorLength u v ≤ 4 * n ^ 2 := by
  by_cases h : Conjugate u v
  · obtain ⟨w, hw, hwlen⟩ := exists_conjugator_wordLength_le h hlen
    exact le_trans (pairConjugatorLength_le_of hw) hwlen
  · simp [pairConjugatorLength_eq_zero_of_not_conjugate h]

theorem lower_le_pairConjugatorLength (n : ℕ) :
    n ^ 2 ≤ pairConjugatorLength (lowerU n) lowerV := by
  obtain ⟨w, hw, hwlen⟩ := pairConjugatorLength_spec (lower_conjugate n)
  rw [← hwlen]
  exact lower_wordLength hw

/-- All words of exactly the indicated length. -/
def wordsExact : ℕ → Finset (List Letter)
  | 0 => {[]}
  | n + 1 =>
      (Finset.univ : Finset Letter).biUnion fun s =>
        (wordsExact n).image fun w => s :: w

@[simp] theorem mem_wordsExact {n : ℕ} {w : List Letter} :
    w ∈ wordsExact n ↔ w.length = n := by
  induction n generalizing w with
  | zero => simp [wordsExact]
  | succ n ih =>
      cases w with
      | nil => simp [wordsExact]
      | cons s w => simp [wordsExact, ih]

/-- The finite set of words of length at most `n`. -/
def wordsUpTo (n : ℕ) : Finset (List Letter) :=
  (Finset.range (n + 1)).biUnion wordsExact

@[simp] theorem mem_wordsUpTo {n : ℕ} {w : List Letter} :
    w ∈ wordsUpTo n ↔ w.length ≤ n := by
  simp only [wordsUpTo, Finset.mem_biUnion, Finset.mem_range, mem_wordsExact]
  constructor
  · rintro ⟨k, hk, hw⟩
    omega
  · intro hw
    exact ⟨w.length, by omega, rfl⟩

/-- The finite set of pairs of input words whose total length is at most
`n`. -/
def inputPairs (n : ℕ) : Finset (List Letter × List Letter) :=
  ((wordsUpTo n) ×ˢ (wordsUpTo n)).filter fun p => p.1.length + p.2.length ≤ n

@[simp] theorem mem_inputPairs {n : ℕ} {p : List Letter × List Letter} :
    p ∈ inputPairs n ↔ p.1.length + p.2.length ≤ n := by
  simp only [inputPairs, Finset.mem_filter, Finset.mem_product, mem_wordsUpTo]
  omega

/-- The conjugator-length function from Section 1.1 of the paper.  The
`Finset.sup` is the maximum over all pairs of literal input words of total
length at most `n`. -/
noncomputable def conjugatorLengthFunction (n : ℕ) : ℕ :=
  (inputPairs n).sup fun p =>
    pairConjugatorLength (eval p.1) (eval p.2)

/-- A completely literal restatement of “`N` is a conjugator-length bound at
input size `n`”, quantifying over three words. -/
def NaiveConjugatorBound (n N : ℕ) : Prop :=
  ∀ u v : List Letter, u.length + v.length ≤ n →
    Conjugate (eval u) (eval v) →
    ∃ w : List Letter,
      eval u * eval w = eval w * eval v ∧ w.length ≤ N

/-- Sanity theorem: the finite maximum used in
`conjugatorLengthFunction` is exactly the naive word-based definition in the
paper. -/
theorem conjugatorLengthFunction_le_iff {n N : ℕ} :
    conjugatorLengthFunction n ≤ N ↔ NaiveConjugatorBound n N := by
  constructor
  · intro h u v huv hconj
    have hp : (u, v) ∈ inputPairs n := by simpa using huv
    have hpcl :
        pairConjugatorLength (eval u) (eval v) ≤ conjugatorLengthFunction n := by
      simpa [conjugatorLengthFunction] using
        (Finset.le_sup
          (s := inputPairs n)
          (f := fun p => pairConjugatorLength (eval p.1) (eval p.2)) hp)
    obtain ⟨g, hg, hglen⟩ := pairConjugatorLength_spec hconj
    obtain ⟨w, heval, hwlen⟩ := exists_word_wordLength g
    refine ⟨w, ?_, ?_⟩
    · dsimp [IsConjugator] at hg
      simpa [heval] using hg
    · rw [hwlen, hglen]
      exact le_trans hpcl h
  · intro h
    apply Finset.sup_le
    rintro ⟨u, v⟩ hp
    have huv : u.length + v.length ≤ n := mem_inputPairs.mp hp
    by_cases hconj : Conjugate (eval u) (eval v)
    · obtain ⟨w, hw, hwlen⟩ := h u v huv hconj
      have hpcl :
          pairConjugatorLength (eval u) (eval v) ≤ wordLength (eval w) :=
        pairConjugatorLength_le_of hw
      exact le_trans hpcl (le_trans (wordLength_le_of_eval rfl) hwlen)
    · simp [pairConjugatorLength_eq_zero_of_not_conjugate hconj]

/-- Consequently the formal function is literally the *least* integer with
the bounding property, as in Section 1.1. -/
theorem conjugatorLengthFunction_isLeast (n : ℕ) :
    IsLeast {N : ℕ | NaiveConjugatorBound n N} (conjugatorLengthFunction n) := by
  constructor
  · exact conjugatorLengthFunction_le_iff.mp le_rfl
  · intro N hN
    exact conjugatorLengthFunction_le_iff.mpr hN

theorem conjugatorLengthFunction_upper (n : ℕ) :
    conjugatorLengthFunction n ≤ 4 * n ^ 2 := by
  apply Finset.sup_le
  rintro ⟨u, v⟩ hp
  have huv : u.length + v.length ≤ n := mem_inputPairs.mp hp
  apply pairConjugatorLength_le_quadratic
  calc
    wordLength (eval u) + wordLength (eval v) ≤ u.length + v.length :=
      Nat.add_le_add (wordLength_le_of_eval rfl) (wordLength_le_of_eval rfl)
    _ ≤ n := huv

theorem lower_le_conjugatorLengthFunction_of_le {k N : ℕ}
    (hN : 4 * k + 2 ≤ N) :
    k ^ 2 ≤ conjugatorLengthFunction N := by
  have hp : (lowerUWord k, lowerVWord) ∈ inputPairs N := by
    rw [mem_inputPairs, length_lowerUWord, length_lowerVWord]
    omega
  calc
    k ^ 2 ≤ pairConjugatorLength (lowerU k) lowerV :=
      lower_le_pairConjugatorLength k
    _ = pairConjugatorLength (eval (lowerUWord k)) (eval lowerVWord) := by simp
    _ ≤ conjugatorLengthFunction N := by
      simpa [conjugatorLengthFunction] using
        (Finset.le_sup
          (s := inputPairs N)
          (f := fun p => pairConjugatorLength (eval p.1) (eval p.2)) hp)

theorem conjugatorLengthFunction_lower (n : ℕ) :
    n ^ 2 ≤ conjugatorLengthFunction (4 * n + 2) :=
  lower_le_conjugatorLengthFunction_of_le (le_rfl)

/-- The comparison `f ≼ g` from Section 2.2 of the paper. -/
def Dominated (f g : ℕ → ℕ) : Prop :=
  ∃ C : ℕ, 0 < C ∧
    ∀ n, f n ≤ C * g (C * n + C) + C * n + C

/-- The paper's equivalence relation `f ≃ g`. -/
def GrowthEquivalent (f g : ℕ → ℕ) : Prop :=
  Dominated f g ∧ Dominated g f

/-- **Theorem 4.9.**  The conjugator-length function of the
three-dimensional integral Heisenberg group grows quadratically. -/
theorem heisenberg_conjugator_length_quadratic :
    GrowthEquivalent conjugatorLengthFunction (fun n => n ^ 2) := by
  constructor
  · refine ⟨4, by norm_num, ?_⟩
    intro n
    have h := conjugatorLengthFunction_upper n
    dsimp
    nlinarith
  · refine ⟨4, by norm_num, ?_⟩
    intro n
    have h :
        n ^ 2 ≤ conjugatorLengthFunction (4 * n + 4) :=
      lower_le_conjugatorLengthFunction_of_le (by omega)
    dsimp
    nlinarith

end ConjugatorLength.Heisenberg