Trace — 2607.20401v1
**Planning file inspection and commentary**
I’ll first identify the paper’s exact central theorem and proof dependencies from the local text/PDF, then map the needed group-theoretic notions to mathlib and build the Lean development under `repro/`. I’ll keep the final response to the required single JSON object.
$ /bin/bash -lc "pwd && rg --files -g 'paper.*' -g 'repro/**' | sed -n '1,120p' && wc -l paper.txt && sed -n '1,240p' paper.txt" thlib/LinearAlgebra/AnnihilatingPolynomial.lean repro/.github/actions/get-mathlib-ci/action.yml repro/.github/actions/get-mathlib-ci/README.md repro/Mathlib/LinearAlgebra/CrossProduct.lean repro/.github/actions/setup-build-env/action.yml repro/Mathlib/LinearAlgebra/Charpoly/BaseChange.lean repro/Mathlib/LinearAlgebra/Charpoly/ToMatrix.lean repro/Mathlib/LinearAlgebra/Charpoly/Basic.lean repro/Mathlib/LinearAlgebra/BilinearMap.lean repro/.github/actions/get-cache/action.yml repro/Mathlib/LinearAlgebra/SModEq/Pointwise.lean repro/Mathlib/LinearAlgebra/SModEq/Basic.lean repro/Mathlib/LinearAlgebra/SModEq/Pow.lean repro/.github/actions/cache-trust-dispatch/action.yml repro/Mathlib/LinearAlgebra/TensorPower/Pairing.lean repro/Mathlib/LinearAlgebra/TensorPower/Basic.lean repro/Mathlib/LinearAlgebra/TensorPower/Symmetric.lean repro/.github/actions/get-tools/action.yml repro/.github/actionlint.yml repro/.github/PULL_REQUEST_TEMPLATE.md repro/MathlibTest/RefinedDiscrTree.lean repro/MathlibTest/InferInstanceAsPercent.lean repro/MathlibTest/JacobiSymbol.lean repro/MathlibTest/AssertImported.lean repro/MathlibTest/irreducibleDef.lean repro/MathlibTest/Explode.lean repro/MathlibTest/Perm.lean repro/Mathlib/LinearAlgebra/Span/TensorProduct.lean repro/Mathlib/LinearAlgebra/Span/Basic.lean repro/Mathlib/LinearAlgebra/Span/Defs.lean repro/Mathlib/Combinatorics/SimpleGraph/Maps.lean repro/Mathlib/Combinatorics/SimpleGraph/Tutte.lean repro/Mathlib/Combinatorics/SimpleGraph/DeleteEdges.lean repro/Mathlib/Combinatorics/SimpleGraph/Partition.lean repro/Mathlib/LinearAlgebra/Complex/Module.lean repro/Mathlib/LinearAlgebra/Complex/Orientation.lean repro/Mathlib/LinearAlgebra/Complex/FiniteDimensional.lean repro/Mathlib/LinearAlgebra/Complex/Determinant.lean repro/Mathlib/LinearAlgebra/Prod.lean repro/Mathlib/LinearAlgebra/LinearPMap.lean repro/Mathlib/LinearAlgebra/Pi.lean repro/MathlibTest/DirectoryDependencyLinter/Test.lean repro/MathlibTest/InferParam.lean repro/.github/workflows/commit
**Surveying theorem names**
$ /bin/bash -lc 'rg -n "''^(Theorem|Proposition|Lemma|Corollary|Definition|Remark) [0-9]" paper.txt && rg -n "Theorem 3|central|main theorem|Main Theorem" paper.txt'
95:Remark 4.11. We give an elementary proof that the conjugator length functions
103:Theorem 5.2 concerns finitely generated groups Λ with a cyclic subgroup whose
204:Theorem 2.1. If G is the fundamental group of a closed, smooth Riemannian
263:Remark 2.2. We stated Theorem 2.1 as a result about Riemannian manifolds
381:Lemma 3.1 (van Kampen’s Lemma). Let G = ⟨A | R⟩ be a finitely presented
407:Lemma 3.2 (Cf. Lemma 5.2 of [LS01], also [Sch66, Sch68]). Suppose G is group
507:Remark 3.3. Every van Kampen diagram admits a continuous, label-preserving,
514:Lemma 3.4. For words u and v that do not represent the identity in a finitely
570:Remark 3.5. The union of the open 2-cells in a t-corridor and the t-edges between
576:Corollary 3.7 in which we describe circumstances in which pairs of conjugate words
665:Remark 3.6. We can combine operations (i) and (ii) to cut a subdiagram out of
683:Corollary 3.7. Let H be a group with finite presentation ⟨X | R⟩ and let ϕ : A → B
721:Remark 3.6 we can remove the inessential t-annuli in Ω, thereby establishing the
786:Lemma 4.1. If G = F (A) is a free group on a finite generating set A, then its
795:Lemma 4.2 (via H.1.7 and H.1.13 of Chapter III.Γ [BH99]). Let k = 8δ + 1. There
798:Lemma 4.3 (Proposition 1.6, page 400 of [BH99]). There exists K > 0 such that,
801:Lemma 4.4 (Lemma 2.9, page 452 of [BH99].). Suppose u ∼ v in G for some words
820:Lemma 4.5 (Section 3 of [AS16]). Suppose u and v are geodesic words such that
959:Theorem 4.6 ([Lys89], [BH99] pp. 451–454, [AS16]). For all δ ≥ 0, there exists
1088:Theorem 4.7 (Cf. Chapter III.Γ of [BH05]). If a group G group with finite generating set A admits a k-synchronous bicombing {wg }g∈G , then it is finitely presentable
1218:Theorem 4.9. The conjugator length function of the 3-dimensional integral Heisenberg group grows quadratically.
1226:Lemma 4.10 (e.g. [BFRT89, BR26a, Kor90]). If the Diophantine equation Ax +
1308:Remark 4.11. The (2m + 1)-dimensional integral Heisenberg group H**Identifying paper’s central theorem**
$ /bin/bash -lc "python3 - <<'PY'
import json
p=json.load(open('paper.json'))
print(type(p))
if isinstance(p,dict):
print(p.keys())
for k,v in p.items():
if isinstance(v,(str,int,float,bool)) or v is None:
print(k,repr(v)[:1000])
PY
sed -n '340,760p' paper.txt
sed -n '1180,1375p' paper.txt"
<class 'dict'>
dict_keys(['id', 'title', 'authors', 'abstract', 'primary_category', 'categories', 'published', 'updated', 'arxiv_url', 'pdf_url', 'fetched_at'])
id '2607.20401v1'
title 'Conjugator length in finitely presented groups'
abstract 'The conjugator length function of a finitely generated group $G$ gives the minimal upper bound on the length of a conjugator for a pair of words that represent conjugate elements in $G$, as a function of the sum of the lengths of the words. Here, we seek to promote the systematic study of conjugator length functions by explaining their significance, by surveying what is known about them and by explaining fundamental techniques and examples.'
primary_category 'math.GR'
published '2026-07-22'
updated '2026-07-22'
arxiv_url 'https://arxiv.org/abs/2607.20401v1'
pdf_url 'https://arxiv.org/pdf/2607.20401v1'
fetched_at '2026-07-23T21:41:03Z'
recovering a from the pair g and g a or b from g and g b and then calculating g ab
8
M. R. BRIDSON, T. R. RILEY AND A. W. SALE
for themselves and (modulo an issue with centralizers) this is the conjugacy search
problem.
A brute-force approach to cracking the conjugacy search problem is to try all words
of length 1, then all of length 2, and so on. If conjugators are sure to be sufficiently
long, then this length-based attack is hopeless. So it would seem that a fast growing
conjugator length function for G is desirable.
In truth, the situation is more subtle. The conjugator length functions of mapping
class groups, and in particular of braid groups, are linear [MM00, Tao13]. Nevertheless, the number of possible words that one has to try to find a conjugator
grows exponentially with length, so this brute-force approach can be prohibitively
expensive even without particularly long conjugators. On the other hand, many
cases can by bypassed. See [GGM10] and references therein for insights on how this
plays out in braid groups.
Conjugacy search problems and, therefore, conjugator length functions **Planning formal proof of conjugator length**
The paper is primarily a survey, but its first substantive new theorem is Theorem 4.9: the conjugator-length function of the integral 3-dimensional Heisenberg group grows quadratically. I’m treating that as the central result. The local proof reduces it to exact integer-coordinate algebra plus a bounded Bézout/Diophantine lemma, which is a realistic route to a fully kernel-checked development.
$ /bin/bash -lc 'rg -n "def .*wordLength|wordLength|WordLength|Cayley.*distance|group.*length" Mathlib | head -200
rg -n "Int.*gcd|gcd.*Int|bezout|Bezout|gcd_eq.*linear|exists.*gcd" Mathlib/Data/Int Mathlib/NumberTheory Mathlib/Algebra | head -200
rg -n "FreeGroup|PresentedGroup|presentation" Mathlib/GroupTheory/FreeGroup Mathlib/GroupTheory | head -200'
Mathlib/Analysis/Analytic/Composition.lean:1174:group together some blocks of `a`, giving altogether `b.length` blocks of blocks. These blocks of
Mathlib/RingTheory/Depth/Rees.lean:20:certain `Ext` groups and the length of a maximal regular sequence in a certain ideal.
Mathlib/Algebra/Free.lean:490:def length (x : FreeSemigroup α) : ℕ := x.tail.length + 1
Mathlib/Algebra/Free.lean:493:theorem length_mul (x y : FreeSemigroup α) : (x * y).length = x.length + y.length := by
Mathlib/Algebra/Free.lean:561: FreeSemigroup.recOnMul x (fun _ ↦ rfl) (fun x y hx hy ↦ by simp only [map_mul, length_mul, *])
Mathlib/Algebra/Free.lean:702:theorem length_toFreeSemigroup (x : FreeMagma α) : (toFreeSemigroup x).length = x.length :=
Mathlib/Algebra/Free.lean:704: rw [map_mul, FreeSemigroup.length_mul, hx, hy]; rfl
Mathlib/Data/Int/GCD.lean:32:Bézout's lemma, Bezout's lemma
Mathlib/Data/Int/GCD.lean:130:theorem exists_mul_mod_eq_gcd {k n : ℕ} (hk : gcd n k < k) : ∃ m < k, n * m % k = gcd n k := by
Mathlib/Data/Int/GCD.lean:134: refine ⟨(n.gcdA k % k).toNat, ?_, (Int.ofNat_inj.1 ?_).trans key.symm⟩
Mathlib/Data/Int/GCD.lean:142: simpa [hkn, hk] using exists_mul_mod_eq_gcd (k := k) (n := n)
Mathlib/Data/Int/GCD.lean:175: show (_ : ℤ) = _ + -(n + 1) * -_ by rw [Int.neg_mul_neg]; apply Nat.gcd_eq_gcd_ab
Mathlib/Data/Int/GCD.lean:177: show (_ : ℤ) = -(m + 1) * -_ + _ by rw [Int.neg_mul_neg]; apply Nat.gcd_eq_gcd_ab
Mathlib/Data/Int/GCD.lean:203:theorem exists_gcd_one {m n : ℤ} (H : 0 < gcd m n) :
Mathlib/Data/Int/GCD.lean:205: ⟨_, _, gcd_div_gcd_div_gcd H, (Int.ediv_mul_cancel (gcd_dvd_left ..)).symm,
Mathlib/Data/Int/GCD.lean:206: (Int.ediv_mul_cancel (gcd_dvd_right ..)).symm⟩
Mathlib/Data/Int/GCD.lean:208:theorem exists_gcd_one' {m n : ℤ} (H : 0 < gcd m n) :
Mathlib/Data/Int/GCD.lean:210: let ⟨m', n', h⟩ := exists_gcd_one H
Mathlib/Data/Int/GCD.lean:216: rw [← Nat.mul_div_cancel' h, Int.natCast_mul, gcd_eq_gcd_ab, Int.add_mul, mul_assoc, mul_assoc]
Mathlib/Data/Int/GCD**Defining wordLength with Nat.find** **Defining conjugatorLengthFunction with finite balls** **Generating finite word sets by length**
**Refining quadratic growth definition** **Formalizing conjugator length function** **Establishing quadratic lower bound**
**Establishing quadratic bounds for CL** **Verifying group commutator calculations**
**Inspecting matrix representation inconsistencies** **Verifying group commutator conventions**
**Verifying group element conjugation relations** **Confirming coordinate assignments and length bounds**
**Verifying bounded solution existence** **Inspecting gcd coefficient bounds**
$ /bin/bash -lc "sed -n '1,270p' Mathlib/Data/Int/GCD.lean
rg -n \"gcdA.*le|natAbs.*gcdA|gcdB.*le|gcdA.*abs|gcdB.*abs\" Mathlib | head -100
rg -n \"Finset.*List|List.*Finset|wordsOfLength|listsOfLength|ofFn.*Finset\" Mathlib/Data/List Mathlib | head -200"
/-
Copyright (c) 2018 Guy Leroy. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sangwoo Jo (aka Jason), Guy Leroy, Johannes Hölzl, Mario Carneiro
-/
module
public import Mathlib.Algebra.Divisibility.Basic
public import Mathlib.Algebra.Group.Commute.Units
public import Mathlib.Algebra.Group.Int.Defs
public import Mathlib.Algebra.Group.Nat.Defs
public import Mathlib.Algebra.GroupWithZero.Semiconj
public import Mathlib.Data.Set.Operations
public import Mathlib.Order.Basic
public import Mathlib.Order.Bounds.Defs
/-!
# Extended GCD and divisibility over ℤ
## Main definitions
* Given `x y : ℕ`, `xgcd x y` computes the pair of integers `(a, b)` such that
`gcd x y = x * a + y * b`. `gcdA x y` and `gcdB x y` are defined to be `a` and `b`,
respectively.
## Main statements
* `gcd_eq_gcd_ab`: Bézout's lemma, given `x y : ℕ`, `gcd x y = x * gcdA x y + y * gcdB x y`.
## Tags
Bézout's lemma, Bezout's lemma
-/
@[expose] public section
/-! ### Extended Euclidean algorithm -/
namespace Nat
/-- Helper function for the extended GCD algorithm (`Nat.xgcd`). -/
def xgcdAux : ℕ → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ :=
Nat.strongRec fun n ih s t r' s' t' ↦ match n with
| 0 => (r', s', t')
| succ k =>
let q := r' / succ k
ih (r' % succ k) (mod_lt _ <| (succ_pos _).gt) (s' - q * s) (t' - q * t) (succ k) s t
@[simp]
theorem xgcd_zero_left {s t r' s' t'} : xgcdAux 0 s t r' s' t' = (r', s', t') := by
rw [xgcdAux, Nat.strongRec_eq]
theorem xgcdAux_rec {r s t r' s' t'} (h : 0 < r) :
xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t := by
obtain ⟨r, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h.ne'
rw [xgcdAux, Nat.strongRec_eq]
rfl
/-- Use the extended GCD algorithm to generate the `a` and `b` values
satisfying `gcd x y = x * a + y * b`. -/
def xgcd (x y : ℕ) : ℤ × ℤ :=
(xgcdAux x 1 0 y 0 1).2
/-- The extended GCD `a` value in the equation `gcd x y = x * a + y * b`. -/
def gc**Deriving coordinate bounds with modular reduction** **Confirming word length bounds via generator ordering**
**Defining y' and bounding its absolute value** **Planning explicit word length construction**
**Defining integer word representations** **Planning group presentation and matrix equivalence**
**Defining and proving commutator relation** **Planning inductive Letter and coordinate bounds proof**
$ /bin/bash -lc 'rg -n "natAbs_(add|sub|mul).*le|natAbs_add|natAbs_mul|abs_add|abs_sub" Mathlib/Data/Int Mathlib/Algebra/Order | head -150 rg -n "theorem.*prod_cons|prod_replicate|List.prod_replicate" Mathlib/Algebra/BigOperators/Group/List Mathlib | head -100 rg -n "class IsConj|def IsConj|IsConj" Mathlib/GroupTheory/Conj | head -100' Mathlib/Data/Int/NatAbs.lean:31: map_mul' := Int.natAbs_mul Mathlib/Algebra/Order/Archimedean/Basic.lean:445: ⟨q, abs_sub_lt_iff.2 ⟨sub_lt_comm.1 h₁, sub_lt_iff_lt_add.2 h₂⟩⟩ Mathlib/Algebra/Order/Ring/Abs.lean:161:theorem abs_sub_sq (a b : α) : |a - b| * |a - b| = a * a + b * b - (1 + 1) * a * b := by Mathlib/Algebra/Order/Ring/Abs.lean:175: refine (abs_add_le ..).trans ?_ Mathlib/Data/Int/NatPrime.lean:25: not_prime_of_mul_eq (natAbs_mul_natAbs_eq hc) ha hb Mathlib/Data/Int/NatPrime.lean:33: rw [← Int.natAbs_mul]; apply Int.natCast_dvd_natCast.1 <| Int.dvd_natAbs.2 hpmn Mathlib/Data/Int/NatPrime.lean:41: rwa [sq, ← natAbs_mul, ← natCast_dvd, ← sq] Mathlib/Data/Int/ModEq.lean:367: rw [lcm_eq_mul_iff.mpr (.inr <| .inr hmn), ← natAbs_mul, modEq_natAbs] Mathlib/Data/Int/Sqrt.lean:31: rw [sqrt, ← natAbs_mul_self, toNat_natCast, Nat.sqrt_eq] Mathlib/Data/Int/Sqrt.lean:34: ⟨fun ⟨n, hn⟩ => by rw [← hn, sqrt_eq, ← Int.natCast_mul, natAbs_mul_self], fun h => ⟨sqrt x, h⟩⟩ Mathlib/Data/Int/Lemmas.lean:67:/-- A specialization of `abs_sub_le_of_nonneg_of_le` for working with the signed subtraction Mathlib/Data/Int/Lemmas.lean:72: exact abs_sub_le_of_nonneg_of_le (natCast_nonneg a) (ofNat_le.mpr a_le_n) Mathlib/Data/Int/Lemmas.lean:75:/-- A specialization of `abs_sub_lt_of_nonneg_of_lt` for working with the signed subtraction Mathlib/Data/Int/Lemmas.lean:80: exact abs_sub_lt_of_nonneg_of_lt (natCast_nonneg a) (ofNat_lt.mpr a_lt_n) Mathlib/Algebra/Order/Round.lean:148:theorem abs_sub_round_eq_min (x : α) : |x - round x| = min (fract x) (1 - fract x) := by Mathlib/Algebra/Order/Round.lean:155: rw [if_neg (not_lt.mpr hx), if_neg (not_lt.mpr hx), abs_sub_comm, ceil_sub_self_eq this.ne.symm, Mathlib/Algebra/Order/Round.lean:159: rw [abs_sub_round_eq_min, min_le_iff] Mathlib/Algebra/Order/Round.lean:193:theorem abs_sub_round (x : α) : |x - round x| ≤ 1 / 2 := by Mathlib/Algebra/Order/Round.lean:194: rw [round_eq, abs_sub_le_iff] Mathlib/Algebra/Order/Round.lean:199:t
**Exploring integer absolute inequalities**
$ /bin/bash -lc "rg -n \"def IsConj|inductive IsConj|IsConj \\(\" Mathlib/Algebra Mathlib/GroupTheory | head -150
rg -n \"ConjAct|conjugate.*iff|isConj\" Mathlib/Algebra/Group Mathlib/GroupTheory | head -150
sed -n '1,120p' Mathlib/Data/Int/NatAbs.lean"
Mathlib/GroupTheory/GroupExtension/Defs.lean:317:def IsConj (s s' : S.Splitting) : Prop := ∃ n : N, s = fun g ↦ S.inl n * s' g * (S.inl n)⁻¹
Mathlib/GroupTheory/SpecificGroups/Alternating.lean:169:theorem isConj_of {σ τ : alternatingGroup α} (hc : IsConj (σ : Perm α) (τ : Perm α))
Mathlib/GroupTheory/SpecificGroups/Alternating.lean:329: IsConj (swap 0 4 * swap 1 3) g := by
Mathlib/GroupTheory/Perm/Sign.lean:151:theorem isConj_swap {w x y z : α} (hwx : w ≠ x) (hyz : y ≠ z) : IsConj (swap w x) (swap y z) :=
Mathlib/GroupTheory/Perm/Cycle/Type.lean:285: have key : IsConj (σ' * τ * σ'⁻¹) τ := (isConj_iff.2 ⟨σ', rfl⟩).symm
Mathlib/GroupTheory/Perm/Finite.lean:161: (hc2 : IsConj τ ρ) (hd1 : Disjoint σ τ) (hd2 : Disjoint π ρ) : IsConj (σ * τ) (π * ρ) := by
Mathlib/Algebra/Group/Conj.lean:32:def IsConj (a b : α) :=
Mathlib/Algebra/Group/Conj.lean:52:theorem IsConj.pow {a b : α} (n : ℕ) : IsConj a b → IsConj (a ^ n) (b ^ n)
Mathlib/Algebra/Group/Conj.lean:62:protected theorem MonoidHom.map_isConj (f : α →* β) {a b : α} : IsConj a b → IsConj (f a) (f b)
Mathlib/GroupTheory/GroupExtension/Defs.lean:8:public import Mathlib.GroupTheory.GroupAction.ConjAct
Mathlib/GroupTheory/GroupExtension/Defs.lean:312:/-- A splitting of an extension `S` is `N`-conjugate to another iff there exists `n : N` such that
Mathlib/GroupTheory/GroupExtension/Defs.lean:315:/-- A splitting of an extension `S` is `N`-conjugate to another iff there exists `n : N` such
Mathlib/GroupTheory/Subgroup/Center.lean:147: simp only [mem_carrier_iff_mk_eq, mk_eq_mk_iff_isConj] at hx hy
Mathlib/GroupTheory/Subgroup/Center.lean:149: · rw [mk_eq_mk_iff_isConj] at H
Mathlib/GroupTheory/Subgroup/Center.lean:159: apply mk_eq_mk_iff_isConj.mpr
Mathlib/GroupTheory/Subgroup/Center.lean:160: rw [isConj_comm, isConj_iff]
Mathlib/Algebra/Group/Subgroup/Pointwise.lean:13:public import Mathlib.GroupTheory.GroupAction.ConjAct
Mathlib/Algebra/Group/Subgroup/Pointwise.lean:537:theorem Normal.conjAct {H : Subgroup **Starting core file with Mathlib import**
**Compiling project**
$ /bin/bash -lc 'lake env lean ConjugatorLength/Heisenberg.lean'
ConjugatorLength/Heisenberg.lean:51:2: error: `inv_mul_cancel₀` is not a field of structure `Group`
ConjugatorLength/Heisenberg.lean:47:28: error: Fields missing: `inv_mul_cancel`
ConjugatorLength/Heisenberg.lean:81:22: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
@Membership.mem ?m.6 (Finset ?m.6) SetLike.instMembership { val := ?m.8, nodup := ?m.9 } ?m.7
in the target expression
@Membership.mem Letter (Finset Letter) SetLike.instMembership
{ val := ↑Letter.enumList, nodup := Letter.enumList_nodup } x✝
x✝ : Letter
⊢ x✝ ∈ { val := ↑Letter.enumList, nodup := Letter.enumList_nodup }
Note: The target expression is not type-correct under the `implicit` transparency level, which may have triggered the failure. This is usually caused by unfolding of semireducible definitions in prior tactic steps. Use `set_option linter.tacticCheckInstances true` to investigate the source of the issue.
Full error:
Application type mismatch: The argument
Letter.enumList_nodup
has type
Letter.enumList.Nodup
but is expected to have type
(↑Letter.enumList).Nodup
in the application
{ val := ↑Letter.enumList, nodup := Letter.enumList_nodup }
ConjugatorLength/Heisenberg.lean:85:2: error: Type mismatch
a
has type
Letter
but is expected to have type
Heisenberg
ConjugatorLength/Heisenberg.lean:86:13: error: Application type mismatch: The argument
a
has type
Letter
but is expected to have type
Heisenberg
in the application
a⁻¹
ConjugatorLength/Heisenberg.lean:87:2: error: Type mismatch
b
has type
Letter
but is expected to have type
Heisenberg
ConjugatorLength/Heisenberg.lean:88:13: error: Application type mismatch: The argument
b
has type
Letter
but is expected to have type
Heisenberg
in the application
b⁻¹
ConjugatorLength/Heisenberg.lean:89:2: error: Type mismatch
c
has type
Letter
but is expected to have type
Heisenberg
ConjugatorLength/Heisenberg.lean:90:13: error: Application type mismatch: The argu**Diagnosing Letter deriving Fintype bug** **Implementing Fintype and fixing wordLength predicate**
**Compiling codebase**
$ /bin/bash -lc 'lake env lean ConjugatorLength/Heisenberg.lean'
ConjugatorLength/Heisenberg.lean:51:42: warning: this tactic is never executed
Note: This linter can be disabled with `set_option linter.unreachableTactic false`
ConjugatorLength/Heisenberg.lean:51:42: warning: 'ring' tactic does nothing
Note: This linter can be disabled with `set_option linter.unusedTactic false`
ConjugatorLength/Heisenberg.lean:127:18: error: unsolved goals
case ofNat.succ.x
n : ℕ
ih : eval (intWord Letter.a Letter.aInv (Int.ofNat n)) = { x := Int.ofNat n, y := 0, z := 0 }
⊢ 1 + ↑n = ↑n + 1
ConjugatorLength/Heisenberg.lean:134:13: error: unsolved goals
case negSucc.zero.x
⊢ -1 = Int.negSucc 0
ConjugatorLength/Heisenberg.lean:136:18: error: unsolved goals
case negSucc.succ.x
n : ℕ
ih : eval (intWord Letter.a Letter.aInv (Int.negSucc n)) = { x := Int.negSucc n, y := 0, z := 0 }
⊢ -1 + Int.negSucc n = Int.negSucc (n + 1)
ConjugatorLength/Heisenberg.lean:149:18: error: unsolved goals
case ofNat.succ.y
n : ℕ
ih : eval (intWord Letter.b Letter.bInv (Int.ofNat n)) = { x := 0, y := Int.ofNat n, z := 0 }
⊢ 1 + ↑n = ↑n + 1
ConjugatorLength/Heisenberg.lean:156:13: error: unsolved goals
case negSucc.zero.y
⊢ -1 = Int.negSucc 0
ConjugatorLength/Heisenberg.lean:158:18: error: unsolved goals
case negSucc.succ.y
n : ℕ
ih : eval (intWord Letter.b Letter.bInv (Int.negSucc n)) = { x := 0, y := Int.negSucc n, z := 0 }
⊢ -1 + Int.negSucc n = Int.negSucc (n + 1)
ConjugatorLength/Heisenberg.lean:171:18: error: unsolved goals
case ofNat.succ.z
n : ℕ
ih : eval (intWord Letter.c Letter.cInv (Int.ofNat n)) = { x := 0, y := 0, z := Int.ofNat n }
⊢ 1 + ↑n = ↑n + 1
ConjugatorLength/Heisenberg.lean:178:13: error: unsolved goals
case negSucc.zero.z
⊢ -1 = Int.negSucc 0
ConjugatorLength/Heisenberg.lean:180:18: error: unsolved goals
case negSucc.succ.z
n : ℕ
ih : eval (intWord Letter.c Letter.cInv (Int.negSucc n)) = { x := 0, y := 0, z := Int.negSucc n }
⊢ -1 + Int.negSucc n = Int.negSucc (n + 1)**Adding omega after ext norm_num**
$ /bin/bash -lc 'lake env lean ConjugatorLength/Heisenberg.lean' ConjugatorLength/Heisenberg.lean:51:42: warning: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` ConjugatorLength/Heisenberg.lean:51:42: warning: 'ring' tactic does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` ConjugatorLength/Heisenberg.lean:131:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:135:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:141:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:153:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:157:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:163:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:175:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:179:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:185:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with
**Coordinating coordinate bounds on evaluation**
$ /bin/bash -lc "cat > /tmp/Check.lean <<'EOF'
import Mathlib
#check Int.natAbs_add_le
#check Int.natAbs_sub_le
#check Int.natAbs_mul
#check Int.natAbs_ofNat
#check Int.natAbs_natCast
#check Int.natAbs_of_nonneg
#check Int.natAbs_ofNat
#check Int.emod_nonneg
#check Int.emod_lt
#check Int.ediv_add_emod
#check Int.ediv_emod_unique
#check Int.abs_eq_natAbs
#check Int.natCast_natAbs
#check Finset.sup_le
#check Finset.le_sup
#check Finset.le_sup_of_mem
#check Finset.mem_univ
#check List.toFinset
#check Nat.find_spec
#check Nat.find_min'
#check Nat.find_min
EOF
lake env lean /tmp/Check.lean"
Int.natAbs_add_le (a b : ℤ) : (a + b).natAbs ≤ a.natAbs + b.natAbs
Int.natAbs_sub_le (a b : ℤ) : (a - b).natAbs ≤ a.natAbs + b.natAbs
Int.natAbs_mul (a b : ℤ) : (a * b).natAbs = a.natAbs * b.natAbs
/tmp/Check.lean:5:7: error(lean.unknownIdentifier): Unknown constant `Int.natAbs_ofNat`
Int.natAbs_natCast (n : ℕ) : (↑n).natAbs = n
Int.natAbs_of_nonneg {a : ℤ} (H : 0 ≤ a) : ↑a.natAbs = a
/tmp/Check.lean:8:7: error(lean.unknownIdentifier): Unknown constant `Int.natAbs_ofNat`
Int.emod_nonneg (a : ℤ) {b : ℤ} : b ≠ 0 → 0 ≤ a % b
Int.emod_lt (a : ℤ) {b : ℤ} (h : b ≠ 0) : a % b < ↑b.natAbs
/tmp/Check.lean:11:7: error(lean.unknownIdentifier): Unknown constant `Int.ediv_add_emod`
Int.ediv_emod_unique {a b r q : ℤ} (h : 0 < b) : a / b = q ∧ a % b = r ↔ r + b * q = a ∧ 0 ≤ r ∧ r < b
Int.abs_eq_natAbs (a : ℤ) : |a| = ↑a.natAbs
Int.natCast_natAbs (n : ℤ) : ↑n.natAbs = |n|
Finset.sup_le.{u_2, u_3} {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α}
{a : α} : (∀ b ∈ s, f b ≤ a) → s.sup f ≤ a
Finset.le_sup.{u_2, u_3} {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α}
{b : β} (hb : b ∈ s) : f b ≤ s.sup f
/tmp/Check.lean:17:7: error(lean.unknownIdentifier): Unknown constant `Finset.le_sup_of_mem`
Finset.mem_univ.{u_1} {α : Type u_1} [Fintype α] (x : α) : x ∈ Finset.univ
List.toFinset.{u_1} {α : Type u_1} [DecidableEq α] (l : List α) : Finset α
Nat.find_spec {p : ℕ → Prop} [DecidablePred p] (H : ∃ n, p n) : p (Nat.find H)
Nat.find_min' {p : ℕ → Prop} [DecidablePred p] (H : ∃ n, p n) {m : ℕ} (h : p m) : Nat.find H ≤ m
Nat.find_min {p : ℕ → Prop} [DecidablePred p] (H : ∃ n, p n) {m : ℕ} : m < Nat.find H → ¬p m**Bounding eval components using natAbs** **Relating word length bound to shortest word**
$ /bin/bash -lc "sed -n '1,100p' Mathlib/Algebra/Group/Conj.lean"
/-
Copyright (c) 2018 Patrick Massot. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Patrick Massot, Chris Hughes, Michael Howes
-/
module
public import Mathlib.Algebra.Group.End
public import Mathlib.Algebra.Group.Semiconj.Units
/-!
# Conjugacy of group elements
See also `MulAut.conj` and `Quandle.conj`.
-/
@[expose] public section
assert_not_exists MonoidWithZero Multiset MulAction
universe u v
variable {α : Type u} {β : Type v}
section Monoid
variable [Monoid α] [Monoid β]
/-- We say that `a` is conjugate to `b` if for some unit `c` we have `c * a * c⁻¹ = b`. -/
@[to_additive /-- We say that `a` is additively conjugate to `b` if for some additive unit `c` we
have `c + a + -c = b`. -/]
def IsConj (a b : α) :=
∃ c : αˣ, SemiconjBy (↑c) a b
@[to_additive (attr := refl)]
theorem IsConj.refl (a : α) : IsConj a a :=
⟨1, SemiconjBy.one_left a⟩
@[to_additive (attr := symm)]
theorem IsConj.symm {a b : α} : IsConj a b → IsConj b a
| ⟨c, hc⟩ => ⟨c⁻¹, hc.units_inv_symm_left⟩
@[to_additive]
theorem isConj_comm {g h : α} : IsConj g h ↔ IsConj h g :=
⟨IsConj.symm, IsConj.symm⟩
@[to_additive (attr := trans)]
theorem IsConj.trans {a b c : α} : IsConj a b → IsConj b c → IsConj a c
| ⟨c₁, hc₁⟩, ⟨c₂, hc₂⟩ => ⟨c₂ * c₁, hc₂.mul_left hc₁⟩
@[to_additive]
theorem IsConj.pow {a b : α} (n : ℕ) : IsConj a b → IsConj (a ^ n) (b ^ n)
| ⟨c, hc⟩ => ⟨c, hc.pow_right n⟩
@[to_additive (attr := simp)]
theorem isConj_iff_eq {α : Type*} [CommMonoid α] {a b : α} : IsConj a b ↔ a = b :=
⟨fun ⟨c, hc⟩ => by
rw [SemiconjBy, mul_comm, ← Units.mul_inv_eq_iff_eq_mul, mul_assoc, c.mul_inv, mul_one] at hc
exact hc, fun h => by rw [h]⟩
@[to_additive]
protected theorem MonoidHom.map_isConj (f : α →* β) {a b : α} : IsConj a b → IsConj (f a) (f b)
| ⟨c, hc⟩ => ⟨Units.map f c, by rw [Units.coe_map, SemiconjBy, ← f.map_mul, hc.eq, f.map_mul]⟩
@[to_additive (attr := simp)]
theorem isConj_one_right {a : α} : IsConj 1 a ↔ a = 1**Defining conjugator length functions** **Constructing exact and bounded word sets**
The coordinate model now compiles as an actual Lean `Group`, with the standard generators, the Heisenberg relators, literal six-letter words, a genuine minimum word length, and normal-form words that generate every coordinate triple. I’m now proving the two quantitative ingredients: coordinates of a length-\(n\) word are bounded, and any solvable conjugacy equation has a polynomially bounded solution.
**Compiling codebase**
$ /bin/bash -lc 'lake env lean ConjugatorLength/Heisenberg.lean' ConjugatorLength/Heisenberg.lean:51:42: warning: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` ConjugatorLength/Heisenberg.lean:51:42: warning: 'ring' tactic does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` ConjugatorLength/Heisenberg.lean:131:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:135:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:141:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:153:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:157:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:163:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:175:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:179:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:185:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with
**Refining algebraic conjugation proof** **Applying rewrites and linarith simplification**
$ /bin/bash -lc 'lake env lean ConjugatorLength/Heisenberg.lean' ConjugatorLength/Heisenberg.lean:51:42: warning: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` ConjugatorLength/Heisenberg.lean:51:42: warning: 'ring' tactic does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` ConjugatorLength/Heisenberg.lean:131:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:135:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:141:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:153:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:157:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:163:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:175:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:179:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:185:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with
**Refining normalization and rewriting steps**
$ /bin/bash -lc 'lake env lean ConjugatorLength/Heisenberg.lean' ConjugatorLength/Heisenberg.lean:51:42: warning: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` ConjugatorLength/Heisenberg.lean:51:42: warning: 'ring' tactic does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` ConjugatorLength/Heisenberg.lean:131:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:135:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:141:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:153:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:157:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:163:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:175:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:179:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:185:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with
**Evaluating ring_nf normalization impact**
$ /bin/bash -lc 'lake env lean ConjugatorLength/Heisenberg.lean' ConjugatorLength/Heisenberg.lean:51:42: warning: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` ConjugatorLength/Heisenberg.lean:51:42: warning: 'ring' tactic does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` ConjugatorLength/Heisenberg.lean:131:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:135:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:141:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:153:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:157:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:163:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:175:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:179:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:185:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with
**Refining linear combination for hz**
$ /bin/bash -lc 'lake env lean ConjugatorLength/Heisenberg.lean' ConjugatorLength/Heisenberg.lean:51:42: warning: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` ConjugatorLength/Heisenberg.lean:51:42: warning: 'ring' tactic does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` ConjugatorLength/Heisenberg.lean:131:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:135:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:141:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:153:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:157:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:163:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:175:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:179:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:185:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with
**Correcting linear combination sign**
$ /bin/bash -lc 'lake env lean ConjugatorLength/Heisenberg.lean' ConjugatorLength/Heisenberg.lean:51:42: warning: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` ConjugatorLength/Heisenberg.lean:51:42: warning: 'ring' tactic does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` ConjugatorLength/Heisenberg.lean:131:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:135:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:141:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:153:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:157:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:163:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:175:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:179:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:185:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with
**Formulating bounded solution theorem with cases** **Completing bound proofs with case analysis and division lemma**
$ /bin/bash -lc "cat >/tmp/Check.lean <<'EOF'
import Mathlib
#check Int.emod_add_ediv
#check Int.ediv_mul_add_emod
#check Int.add_emod_ediv
#check Int.emod_add_ediv
#check Int.natAbs_pos
#check Int.natAbs_ne_zero
#check Int.natAbs_eq_zero
#check Int.natAbs_of_nonneg
#check Int.natAbs_ofNat
EOF
lake env lean /tmp/Check.lean"
/tmp/Check.lean:2:7: error(lean.unknownIdentifier): Unknown constant `Int.emod_add_ediv`
Int.ediv_mul_add_emod (a b : ℤ) : a / b * b + a % b = a
/tmp/Check.lean:4:7: error(lean.unknownIdentifier): Unknown constant `Int.add_emod_ediv`
/tmp/Check.lean:5:7: error(lean.unknownIdentifier): Unknown constant `Int.emod_add_ediv`
Int.natAbs_pos {a : ℤ} : 0 < a.natAbs ↔ a ≠ 0
Int.natAbs_ne_zero {a : ℤ} : a.natAbs ≠ 0 ↔ a ≠ 0
Int.natAbs_eq_zero {a : ℤ} : a.natAbs = 0 ↔ a = 0
Int.natAbs_of_nonneg {a : ℤ} (H : 0 ≤ a) : ↑a.natAbs = a
/tmp/Check.lean:10:7: error(lean.unknownIdentifier): Unknown constant `Int.natAbs_ofNat`**Adding lemma and compiling**
$ /bin/bash -lc 'lake env lean ConjugatorLength/Heisenberg.lean' ConjugatorLength/Heisenberg.lean:51:42: warning: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` ConjugatorLength/Heisenberg.lean:51:42: warning: 'ring' tactic does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` ConjugatorLength/Heisenberg.lean:131:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:135:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:141:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:153:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:157:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:163:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:175:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:179:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:185:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with
**Proving natural number inequalities using multiplication lemmas**
$ /bin/bash -lc 'lake env lean ConjugatorLength/Heisenberg.lean' ConjugatorLength/Heisenberg.lean:51:42: warning: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` ConjugatorLength/Heisenberg.lean:51:42: warning: 'ring' tactic does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` ConjugatorLength/Heisenberg.lean:131:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:135:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:141:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:153:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:157:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:163:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:175:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:179:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:185:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with
**Adding missing inequality lemma**
$ /bin/bash -lc 'lake env lean ConjugatorLength/Heisenberg.lean' ConjugatorLength/Heisenberg.lean:51:42: warning: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` ConjugatorLength/Heisenberg.lean:51:42: warning: 'ring' tactic does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` ConjugatorLength/Heisenberg.lean:131:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:135:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:141:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:153:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:157:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:163:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:175:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:179:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:185:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with
**Bounding conjugator word length** **Refining bounds with case analysis**
**Defining short conjugator theorem** **Planning explicit commutator word construction**
**Planning conjugatorLength implementation** **Adding conjugatorLength inequalities and specifications**
**Compiling codebase**
$ /bin/bash -lc 'lake env lean ConjugatorLength/Heisenberg.lean' ConjugatorLength/Heisenberg.lean:51:42: warning: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` ConjugatorLength/Heisenberg.lean:51:42: warning: 'ring' tactic does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` ConjugatorLength/Heisenberg.lean:131:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:135:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:141:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:153:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:157:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:163:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:175:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:179:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:185:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with
**Applying simpa with sub_eq_add_neg and natAbs rewrites**
$ /bin/bash -lc "sed -n '418,492p' ConjugatorLength/Heisenberg.lean"
_ ≤ C.natAbs + A.natAbs * B.natAbs := by gcongr
/-- A quadratic upper bound for an individual conjugacy instance, measured
using the actual standard word metric. -/
theorem exists_conjugator_wordLength_le {u v : Heisenberg} {n : ℕ}
(huv : Conjugate u v) (hlen : wordLength u + wordLength v ≤ n) :
∃ w, IsConjugator u v w ∧ wordLength w ≤ 4 * n ^ 2 := by
obtain ⟨w₀, hw₀⟩ := huv
have hcoord := (isConjugator_iff u v w₀).mp hw₀
obtain ⟨x, y, hxy, hx, hy⟩ :=
bounded_diophantine_solution
(A := v.y) (B := -u.x) (C := u.z - v.z)
(x := w₀.x) (y := w₀.y) (by simpa using hcoord.2.2)
let w : Heisenberg := ⟨x, y, 0⟩
refine ⟨w, ?_, ?_⟩
· apply (isConjugator_iff u v w).mpr
refine ⟨hcoord.1, hcoord.2.1, ?_⟩
simpa [w] using hxy
· have hux : u.x.natAbs ≤ wordLength u := x_natAbs_le_wordLength u
have hvy : v.y.natAbs ≤ wordLength v := y_natAbs_le_wordLength v
have huz : u.z.natAbs ≤ wordLength u ^ 2 := z_natAbs_le_wordLength_sq u
have hvz : v.z.natAbs ≤ wordLength v ^ 2 := z_natAbs_le_wordLength_sq v
have hC : (u.z - v.z).natAbs ≤ n ^ 2 := by
calc
(u.z - v.z).natAbs ≤ u.z.natAbs + v.z.natAbs := Int.natAbs_sub_le _ _
_ ≤ wordLength u ^ 2 + wordLength v ^ 2 := Nat.add_le_add huz hvz
_ ≤ (wordLength u + wordLength v) ^ 2 := by nlinarith
_ ≤ n ^ 2 := Nat.pow_le_pow_left hlen 2
have huxn : u.x.natAbs ≤ n := le_trans hux (le_trans (Nat.le_add_right _ _) hlen)
have hvyn : v.y.natAbs ≤ n :=
le_trans hvy (le_trans (Nat.le_add_left _ _) hlen)
have hx' : x.natAbs ≤ n + n ^ 2 := by
simpa using le_trans hx (Nat.add_le_add huxn hC)
have hy' : y.natAbs ≤ n ^ 2 + n * n := by
calc
y.natAbs ≤ (u.z - v.z).natAbs + v.y.natAbs * (-u.x).natAbs := hy
_ ≤ n ^ 2 + n * n := by
rw [Int.natAbs_neg]
gcongr
have hn : n ≤ n ^ 2 := by
cases n with
| zero => simp
| succ n => simp only [pow_two]; nlinarith
calc
wordLengt$ /bin/bash -lc 'lake env lean ConjugatorLength/Heisenberg.lean' ConjugatorLength/Heisenberg.lean:51:42: warning: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` ConjugatorLength/Heisenberg.lean:51:42: warning: 'ring' tactic does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` ConjugatorLength/Heisenberg.lean:131:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:135:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:141:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:153:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:157:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:163:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:175:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:179:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:185:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with
**Defining conjugatorLength and wordsExact functions** **Inducting and simplifying wordsExact membership**
**Proving pairCL quadratic bound** **Defining coarse equivalence with bounds**
**Establishing quadratic conjugator length equivalence** **Planning conjugator length function equivalence proof**
**Implementing Main function**
**Compiling project code**
$ /bin/bash -lc 'lake env lean ConjugatorLength/Main.lean' ConjugatorLength/Main.lean:1:0: error: unknown module prefix 'ConjugatorLength' No directory 'ConjugatorLength' or file 'ConjugatorLength.olean' in the search path entries: /work/repro/.lake/packages/Cli/.lake/build/lib/lean /work/repro/.lake/packages/batteries/.lake/build/lib/lean /work/repro/.lake/packages/Qq/.lake/build/lib/lean /work/repro/.lake/packages/aesop/.lake/build/lib/lean /work/repro/.lake/packages/proofwidgets/.lake/build/lib/lean /work/repro/.lake/packages/importGraph/.lake/build/lib/lean /work/repro/.lake/packages/LeanSearchClient/.lake/build/lib/lean /work/repro/.lake/packages/plausible/.lake/build/lib/lean /work/repro/.lake/build/lib/lean /opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/lib/lean /opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/lib/lean
**Checking build facet configuration**
$ /bin/bash -lc "sed -n '1,160p' lakefile.lean && ls -la .lake/build/lib/lean/ConjugatorLength 2>/dev/null || true"
import Lake
open Lake DSL
/-!
## Mathlib dependencies on upstream projects
-/
require "leanprover-community" / "batteries" @ git "main"
require "leanprover-community" / "Qq" @ git "master"
require "leanprover-community" / "aesop" @ git "master"
require "leanprover-community" / "proofwidgets" @ git "main"
with NameMap.empty.insert `errorOnBuild
"ProofWidgets failed to reuse pre-built JS code. \
Please report this issue on the Lean Zulip."
require "leanprover-community" / "importGraph" @ git "main"
require "leanprover-community" / "LeanSearchClient" @ git "main"
require "leanprover-community" / "plausible" @ git "main"
/-!
## Options for building mathlib
-/
/-- These options are used as `leanOptions`, prefixed by `` `weak``, so that
`lake build` uses them, as well as `Archive` and `Counterexamples`. -/
abbrev mathlibOnlyLinters : Array LeanOption := #[
⟨`linter.mathlibStandardSet, true⟩,
-- Explicitly enable the header linter, since the standard set is defined in `Mathlib.Init`
-- but we want to run this linter in files imported by `Mathlib.Init`.
⟨`linter.style.header, true⟩,
⟨`linter.checkInitImports, true⟩,
⟨`linter.allScriptsDocumented, true⟩,
⟨`linter.pythonStyle, true⟩,
⟨`linter.style.longFile, .ofNat 1500⟩,
-- ⟨`linter.nightlyRegressionSet, true⟩,
-- `latest_import.yml` uses this comment: if you edit it, make sure that the workflow still works
]
/-- These options are passed as `leanOptions` to building mathlib, as well as the
`Archive` and `Counterexamples`. (`tests` omits the first two options.) -/
abbrev mathlibLeanOptions := #[
⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
⟨`autoImplicit, false⟩,
⟨`maxSynthPendingDepth, .ofNat 3⟩,
] ++ -- options that are used in `lake build`
mathlibOnlyLinters.map fun s ↦ { s with name := `weak ++ s.name }
package mathlib where
testDriver := "MathlibTest"
lintDriver := "batteries/runLinter"
lintDriverArgs := #["Mathlib"]
-- A version of Mathlib only su**Adding lean_lib ConjugatorLength to lakefile**
$ /bin/bash -lc 'lake build ConjugatorLength.Heisenberg && lake env lean ConjugatorLength/Main.lean' ⚠ [8677/8677] Built ConjugatorLength.Heisenberg (9.3s) warning: ConjugatorLength/Heisenberg.lean:51:42: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: ConjugatorLength/Heisenberg.lean:51:42: 'ring' tactic does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: ConjugatorLength/Heisenberg.lean:131:54: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: ConjugatorLength/Heisenberg.lean:135:63: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: ConjugatorLength/Heisenberg.lean:141:54: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: ConjugatorLength/Heisenberg.lean:153:54: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: ConjugatorLength/Heisenberg.lean:157:63: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: ConjugatorLength/Heisenberg.lean:163:54: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: ConjugatorLength/Heisenberg.lean:175:54: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: ConjugatorLength/Heisenberg.lean:179:63: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: ConjugatorLength/Heisenberg.lean:185:54: Used `tac1 <;> tac2` where `(tac1; tac2)`
**Inspecting function type inference**
$ /bin/bash -lc "nl -ba ConjugatorLength/Main.lean | sed -n '112,175p'"
112 eval u * eval w = eval w * eval v ∧ w.length ≤ N
113
114 /-- Sanity theorem: the finite maximum used in
115 `conjugatorLengthFunction` is exactly the naive word-based definition in the
116 paper. -/
117 theorem conjugatorLengthFunction_le_iff {n N : ℕ} :
118 conjugatorLengthFunction n ≤ N ↔ NaiveConjugatorBound n N := by
119 constructor
120 · intro h u v huv hconj
121 have hp : (u, v) ∈ inputPairs n := by simpa using huv
122 have hpcl :
123 pairConjugatorLength (eval u) (eval v) ≤ conjugatorLengthFunction n := by
124 exact Finset.le_sup hp
125 obtain ⟨g, hg, hglen⟩ := pairConjugatorLength_spec hconj
126 obtain ⟨w, heval, hwlen⟩ := exists_word_wordLength g
127 refine ⟨w, ?_, ?_⟩
128 · dsimp [IsConjugator] at hg
129 simpa [heval] using hg
130 · rw [hwlen, hglen]
131 exact le_trans hpcl h
132 · intro h
133 apply Finset.sup_le
134 rintro ⟨u, v⟩ hp
135 have huv : u.length + v.length ≤ n := mem_inputPairs.mp hp
136 by_cases hconj : Conjugate (eval u) (eval v)
137 · obtain ⟨w, hw, hwlen⟩ := h u v huv hconj
138 have hpcl :
139 pairConjugatorLength (eval u) (eval v) ≤ wordLength (eval w) :=
140 pairConjugatorLength_le_of hw
141 exact le_trans hpcl (le_trans (wordLength_le_of_eval rfl) hwlen)
142 · simp [pairConjugatorLength_eq_zero_of_not_conjugate hconj]
143
144 theorem conjugatorLengthFunction_upper (n : ℕ) :
145 conjugatorLengthFunction n ≤ 4 * n ^ 2 := by
146 apply Finset.sup_le
147 rintro ⟨u, v⟩ hp
148 have huv : u.length + v.length ≤ n := mem_inputPairs.mp hp
149 apply pairConjugatorLength_le_quadratic
150 calc
151 wordLength (eval u) + wordLength (eval v) ≤ u.length + v.length :=
152 Nat.add_le_add (wordLength_le_of_eval rfl) (wordLength_le_of_eval rfl)
153 _ ≤ n := huv
154
155 theorem**Unfolding conjugatorLengthFunction in Finset lemma**
$ /bin/bash -lc 'lake env lean ConjugatorLength/Main.lean'
**Planning matrix representation proof** **Implementing and testing matrix function**
$ /bin/bash -lc "cat >/tmp/MatrixTest.lean <<'EOF'
import ConjugatorLength.Heisenberg
open Matrix
open ConjugatorLength
namespace ConjugatorLength.Heisenberg
def toMatrix (g : Heisenberg) : Matrix (Fin 3) (Fin 3) ℤ :=
"'!![1, g.x, g.z; 0, 1, g.y; 0, 0, 1]
example (g h : Heisenberg) : toMatrix (g*h) = toMatrix g * toMatrix h := by
ext i j
fin_cases i <;> fin_cases j <;>
simp [toMatrix, Matrix.mul_apply, Fin.sum_univ_succ] <;> ring
example : Function.Injective toMatrix := by
intro g h H
ext
· have := congrFun (congrFun H (0 : Fin 3)) (1 : Fin 3)
simpa [toMatrix] using this
· have := congrFun (congrFun H (1 : Fin 3)) (2 : Fin 3)
simpa [toMatrix] using this
· have := congrFun (congrFun H (0 : Fin 3)) (2 : Fin 3)
simpa [toMatrix] using this
end ConjugatorLength.Heisenberg
EOF
lake env lean /tmp/MatrixTest.lean'**Adding Heisenberg group presentation and proving eval surjectivity** **Verifying axiom usage and clarifying sign conventions**
The full theorem now compiles, including the paper’s exact coarse comparison \( \simeq \), not merely upper/lower examples. The formal function is a finite maximum over literal input words, and I have also proved it is equivalent to the naive three-word definition, so the result is tied to the paper’s stated notion rather than a coordinate surrogate. I’m doing the final representation and assumption audit now.
**Compiling both builds**
$ /bin/bash -lc 'lake env lean ConjugatorLength/Heisenberg.lean && lake build ConjugatorLength.Heisenberg && lake env lean ConjugatorLength/Main.lean' ConjugatorLength/Heisenberg.lean:51:42: warning: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` ConjugatorLength/Heisenberg.lean:51:42: warning: 'ring' tactic does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` ConjugatorLength/Heisenberg.lean:157:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:161:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:167:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:179:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:183:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:189:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:201:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:205:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:211:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with
**Reviewing warning at line 51**
$ /bin/bash -lc "nl -ba ConjugatorLength/Heisenberg.lean | sed -n '44,56p'; rg -n \"sorry|axiom|admit\" ConjugatorLength README.md 2>/dev/null || true; git status --short" M lakefile.lean ?? ConjugatorLength/
**Planning theorem audit and README creation** **Refining matrix group definitions and conjugator length proofs**
**Creating initial README file**
**Auditing build and verifying axioms**
$ /bin/bash -lc "lake env lean ConjugatorLength/Main.lean && lake build ConjugatorLength rg -n \"\\bsorry\\b|\\badmit\\b|"'^axiom'"\\b\" ConjugatorLength || true cat >/tmp/ConjugatorLengthAudit.lean <<'EOF' import ConjugatorLength.Main #print axioms ConjugatorLength.Heisenberg.heisenberg_conjugator_length_quadratic #print axioms ConjugatorLength.Heisenberg.conjugatorLengthFunction_le_iff #print axioms ConjugatorLength.Heisenberg.toMatrix_mul EOF lake env lean /tmp/ConjugatorLengthAudit.lean git diff --check git status --short" ✖ [0/1] Running job computation error: ConjugatorLength: some modules have bad imports Some required targets logged failures: - job computation error: build failed /tmp/ConjugatorLengthAudit.lean:1:0: error: object file '/work/repro/.lake/build/lib/lean/ConjugatorLength/Main.olean' of module ConjugatorLength.Main does not exist M README.md M lakefile.lean ?? ConjugatorLength/
**Testing building specific library module**
The source-level checks are clean. The final library-wide command exposed a Lake configuration issue (“bad imports”) rather than a proof failure: the local library was not declared as depending on the `Mathlib` library even though its modules import mathlib. I’m correcting that build metadata and rerunning the theorem/axiom audit.
$ /bin/bash -lc 'rg -n "lean_lib .* where|require .* from|lean_lib.*Mathlib" lakefile.lean .lake/packages/*/lakefile.lean | head -100 && lake build ConjugatorLength.Main -v' ✔ [0/419] Ran mathlib:extraDep ✔ [1/419] Ran batteries:extraDep ✔ [2/419] Replayed Batteries.Util.LibraryNote ✔ [3/419] Replayed Batteries.Classes.Cast ✔ [4/419] Replayed Batteries.Tactic.Unreachable ✔ [5/419] Replayed Batteries.Linter.UnreachableTactic ✔ [6/419] Replayed Batteries.Lean.TagAttribute ✔ [7/419] Replayed Batteries.Lean.AttributeExtra ✔ [8/419] Replayed Batteries.Linter.UnnecessarySeqFocus ✔ [9/419] Replayed Batteries.Linter ✔ [10/419] Replayed Batteries.Tactic.Init ✔ [11/419] Replayed Batteries.Tactic.SeqFocus ✔ [12/419] Replayed Batteries.Tactic.Lint.Basic ✔ [13/419] Replayed Batteries.Tactic.Lint.Misc ✔ [14/419] Replayed Batteries.Lean.Syntax ✔ [15/419] Replayed Batteries.Util.ProofWanted ✔ [16/419] Replayed Batteries.Tactic.Basic ✔ [17/419] Replayed Batteries.Classes.Order ✔ [18/419] Replayed Batteries.Classes.RatCast ✔ [19/419] Replayed Batteries.Lean.EStateM ✔ [20/419] Replayed Batteries.Lean.Except ✔ [21/419] Replayed Batteries.Recycling.MonadSatisfying.Basic ✔ [22/419] Replayed Batteries.Classes.SatisfiesM ✔ [23/419] Replayed Batteries.CodeAction.Attr ✔ [24/419] Replayed Batteries.CodeAction.Basic ✔ [25/419] Replayed Batteries.Lean.Position ✔ [26/419] Replayed Batteries.CodeAction.Misc ✔ [27/419] Replayed Batteries.CodeAction.Deprecated ✔ [28/419] Replayed Batteries.Tactic.Alias ✔ [29/419] Replayed Batteries.Data.List.Basic ✔ [30/419] Replayed Batteries.CodeAction.Match ✔ [31/419] Replayed Batteries.CodeAction ✔ [32/419] Replayed Batteries.Control.Lemmas ✔ [33/419] Replayed Batteries.Control.LawfulMonadState ✔ [34/419] Replayed Batteries.Control.OptionT ✔ [35/419] Replayed Batteries.Control.AlternativeMonad ✔ [36/419] Replayed Batteries.Control.ForInStep.Basic ✔ [37/419] Replayed Batteries.Control.ForInStep.Lemmas ✔ [38/419] Replayed Batteries.Control.ForInStep ✔ [39/419] Replayed Batteries.Control.Monad ✔ [40/419] Replayed Batteries.Data.MLList.Basic ✔ [41/419] Replayed Batteries.Control.Nondet.Basic ✔ [42/419] Replayed Batteries.Data.UInt ✔ [4
**Investigating import configuration issues in library build** **Searching configuration for extra dependencies**
$ /bin/bash -lc "rg -n \"extraDepTargets|lean_lib .* where[\\s\\S]{0,100}globs\" /opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/src/lean/lake .lake/packages -g 'lakefile.lean' | head -100
rg -n \"structure LeanLibConfig|LeanLibConfig where|extraDepTargets\" /opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/src/lean/lake | head -100"
/opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/src/lean/lake/Lake/Build/Facets.lean:241:/-- A package's `extraDepTargets` mixed with its transitive dependencies'. -/
/opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/src/lean/lake/Lake/Build/Facets.lean:268:/-- A Lean library's `extraDepTargets` mixed with its package's. -/
/opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/src/lean/lake/Lake/Config/LeanExe.lean:34: extraDepTargets := self.extraDepTargets
/opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/src/lean/lake/Lake/Config/LeanLibConfig.lean:73: extraDepTargets : Array Name := #[]
/opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/src/lean/lake/Lake/Config/LeanLib.lean:96:/-- The library's `extraDepTargets` configuration. -/
/opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/src/lean/lake/Lake/Config/LeanLib.lean:97:@[inline] public def extraDepTargets (self : LeanLib) :=
/opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/src/lean/lake/Lake/Config/LeanLib.lean:98: self.config.extraDepTargets
/opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/src/lean/lake/Lake/Build/Package.lean:95:Build the `extraDepTargets` for the package.
/opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/src/lean/lake/Lake/Build/Package.lean:105: for target in self.extraDepTargets do
/opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/src/lean/lake/Lake/Build/Library.lean:160:Build extra target dependencies of the library (e.g., `extraDepTargets`, `needs`). -/
/opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/src/lean/lake/Lake/Build/Library.lean:164: for target in self.extraDepTargets do
/opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/src/lean/lake/Lake/Config/Package.lean:239:/-- The package's `extraDepTargets` configuration. -/
/opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/src/lean/lake/Lake/Config/Package.lean:240:@[inline] public def extraDepTargets (self : Package) : Array Name :=
/opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/src/l$ /bin/bash -lc "sed -n '35,90p' /opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/src/lean/lake/Lake/Config/LeanLibConfig.lean
sed -n '100,180p' /opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/src/lean/lake/Lake/Build/Library.lean"
-/
roots : Array Name := #[name]
/--
An `Array` of module `Glob`s to build for the library.
Defaults to a `Glob.one` of each of the library's `roots`.
Submodule globs build every source file within their directory.
Local imports of glob'ed files (i.e., fellow modules of the workspace) are
also recursively built.
-/
globs : Array Glob := roots.map Glob.one
/--
The name of the library artifact.
Used as a base for the file names of its static and dynamic binaries.
Defaults to the mangled name of the target.
-/
libName : String := ""
/--
Whether static and shared binaries of this library should be prefixed with `lib` on Windows.
Unlike Unix, Windows does not require native libraries to start with `lib` and,
by convention, they usually do not. However, for consistent naming across all platforms,
users may wish to enable this.
Defaults to `false`.
-/
libPrefixOnWindows : Bool := false
/-- An `Array` of targets to build before the executable's modules. -/
needs : Array PartialBuildKey := #[]
/--
**Deprecated. Use `needs` instead.**
An `Array` of target names to build before the library's modules.
-/
extraDepTargets : Array Name := #[]
/--
Whether to compile each of the library's modules into a native shared library
that is loaded whenever the module is imported. This speeds up evaluation of
metaprograms and enables the interpreter to run functions marked `@[extern]`.
Defaults to `false`.
-/
precompileModules : Bool := false
/--
An `Array` of library facets to build on a bare `lake build` of the library.
For example, `#[LeanLib.sharedFacet]` will build the shared library facet.
-/
defaultFacets : Array Name := #[LeanLib.leanArtsFacet]
/--
let filelistPath := libFile.addExtension "filelist"
let h ← IO.FS.Handle.mk filelistPath .write
oFiles.forM fun f => h.putStr s!"{f}\n"
proc {cmd := "libtool", args := #["-static", "-o", libFile.toStri**Updating globs to fix imports**
**Building aggregate audit**
$ /bin/bash -lc "lake build ConjugatorLength cat >/tmp/ConjugatorLengthAudit.lean <<'EOF' import ConjugatorLength.Main #print axioms ConjugatorLength.Heisenberg.heisenberg_conjugator_length_quadratic #print axioms ConjugatorLength.Heisenberg.conjugatorLengthFunction_le_iff #print axioms ConjugatorLength.Heisenberg.toMatrix_mul EOF lake env lean /tmp/ConjugatorLengthAudit.lean rg -n \"\\bsorry\\b|\\badmit\\b|"'^axiom'"\\b\" ConjugatorLength || true git diff --check git status --short" ⚠ [8677/8679] Replayed ConjugatorLength.Heisenberg warning: ConjugatorLength/Heisenberg.lean:51:42: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: ConjugatorLength/Heisenberg.lean:51:42: 'ring' tactic does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: ConjugatorLength/Heisenberg.lean:157:54: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: ConjugatorLength/Heisenberg.lean:161:63: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: ConjugatorLength/Heisenberg.lean:167:54: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: ConjugatorLength/Heisenberg.lean:179:54: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: ConjugatorLength/Heisenberg.lean:183:63: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: ConjugatorLength/Heisenberg.lean:189:54: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: ConjugatorLength/Heisenberg.lean:201:54: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: ConjugatorLength/Heisenberg.lean:205:63: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: ConjugatorLength/Heisenberg.lean:211:54: Used `tac1 <;> tac2` where `(tac1; tac2)` wou
**Clarifying central theorem identification** **Evaluating multiple novel theorems** **Planning formalization of Theorem 4.14**
**Assessing lemma precision and finite presentation** **Verifying definitions and planning README updates**
**Removing redundant warning group and cleaning unused code**
$ /bin/bash -lc "nl -ba ConjugatorLength/Heisenberg.lean | sed -n '386,397p'"
386 theorem bounded_diophantine_solution {A B C x y : ℤ}
387 (h : A * x + B * y = C) :
388 ∃ x' y' : ℤ, A * x' + B * y' = C ∧
389 x'.natAbs ≤ B.natAbs + C.natAbs ∧
390 y'.natAbs ≤ C.natAbs + A.natAbs * B.natAbs := by
391 by_cases hB : B = 0
392 · subst B
393 simp only [mul_zero, zero_mul, add_zero] at h ⊢
394 by_cases hA : A = 0
395 · subst A
396 simp at h
397 subst C**Removing unused mul_zero lemma**
**Performing final compile after patch**
$ /bin/bash -lc "lake env lean ConjugatorLength/Heisenberg.lean && lake build ConjugatorLength.Heisenberg && lake env lean ConjugatorLength/Main.lean && lake build ConjugatorLength rg -n \"\\bsorry\\b|\\badmit\\b|"'^axiom'"\\b\" ConjugatorLength || true git diff --check" ConjugatorLength/Heisenberg.lean:157:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:161:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:167:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:179:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:183:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:189:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:201:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:205:63: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:211:54: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ConjugatorLength/Heisenberg.lean:542:62: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` ⚠ [8677/8677] Built ConjugatorLength.Heisenberg (9.6s) warning: ConjugatorLength
**Completing update plan**
**Finalizing JSON theorem summary**
{"status":"reproduced","claim":"Theorem 4.9: for the standard generators of the integral Heisenberg group H₃(ℤ), its conjugator-length function satisfies CL ≃ (n ↦ n²) under the paper's comparison relation. No hypotheses or custom axioms are declared.","note":"A self-contained proof is in repro/ConjugatorLength/, documented in repro/README.md. It proves the matrix-model correspondence, standard relators, genuine minimum word metric, equivalence with the paper's naive three-word definition, CL(n) ≤ 4n², and n² ≤ CL(4n+2). Both Lean files and the complete library build succeed with zero sorry; the axiom audit reports only propext, Classical.choice, and Quot.sound.","significance":"The paper claims that shortest conjugators in H₃(ℤ) have quadratic worst-case growth in the total input length. This gives a sharp quantitative measure of conjugacy complexity in a foundational finitely presented nilpotent group."}