2607.20401v1 / README.md

all files

# Reproduction of “Conjugator length in finitely presented groups”

## Verdict

Reproduced.  The development proves Theorem 4.9 of the paper: the
conjugator-length function of the three-dimensional integral Heisenberg group
is equivalent to the quadratic function under exactly the comparison relation
defined in Section 2.2 of the paper.  There are no `sorry`s, custom axioms, or
declared mathematical hypotheses.

The final Lean theorem is

```lean
theorem heisenberg_conjugator_length_quadratic :
    GrowthEquivalent conjugatorLengthFunction (fun n => n ^ 2)
```

in `ConjugatorLength/Main.lean`.

## Files

- `ConjugatorLength/Heisenberg.lean` constructs the integer Heisenberg group,
  its literal words and standard word metric, and proves the coordinate,
  Diophantine, upper-bound, and lower-bound lemmas.
- `ConjugatorLength/Main.lean` defines the pairwise and global
  conjugator-length functions, proves that the definition is exactly the
  paper's naive word definition, and proves quadratic growth.
- `lakefile.lean` has one additional local Lean library,
  `ConjugatorLength`, so the two modules can be checked in the usual way.

## Why this is the same group

`Heisenberg` consists of triples `(x,y,z)` of integers with multiplication

```text
(x,y,z)(x',y',z') = (x+x', y+y', z+z'+xy').
```

The map `toMatrix` sends such a triple to

```text
[1 x z]
[0 1 y]
[0 0 1].
```

Lean proves `toMatrix_mul`, `toMatrix_one`, and `toMatrix_injective`.  Thus this
is precisely the upper-unitriangular integer matrix group displayed before
Theorem 4.9, not an abstract replacement with a convenient norm.

The standard generators are

```text
a = (1,0,0),  b = (0,1,0),  c = (0,0,1).
```

Lean proves the presentation relations

```text
a⁻¹ b⁻¹ a b = c,   ac = ca,   bc = cb
```

and `eval_surjective`: every group element is represented by a literal word in
the six letters `a,a⁻¹,b,b⁻¹,c,c⁻¹`.  `normalWord` supplies an explicit
spelling.  These results connect the coordinate/matrix model to the standard
finite generating set and relators used in equation (4) of the paper.

## Why this is the same length function

`wordLength g` is defined with `Nat.find` as the least length of a literal word
evaluating to `g`; it is not a coordinate norm.  The file proves both that a
shortest word exists and that `wordLength g` is no larger than any proposed
spelling.

`conjugatorLengthFunction n` is a finite maximum over every pair of literal
input words whose total length is at most `n`.  For each conjugate pair it uses
the minimum standard word length of an element `w` satisfying

```text
u * w = w * v.
```

Non-conjugate pairs contribute zero and therefore do not change the maximum.
The key validation theorem is

```lean
theorem conjugatorLengthFunction_le_iff {n N : ℕ} :
    conjugatorLengthFunction n ≤ N ↔ NaiveConjugatorBound n N
```

where `NaiveConjugatorBound` quantifies directly over three literal words and
asserts that every conjugate input pair of total length at most `n` has a
conjugating word of length at most `N`.  The subsequent theorem
`conjugatorLengthFunction_isLeast` proves that the formal function is the least
such integer, word for word matching Section 1.1.

`Conjugate` is also proved equivalent to mathlib's standard `IsConj`.

## Proof outline

For a word of length `m`, Lean proves

```text
|x| ≤ m,   |y| ≤ m,   |z| ≤ m².
```

The equality `u*w = w*v` is proved equivalent to equality of the two horizontal
coordinates of `u,v` together with the Diophantine equation

```text
v.y * w.x - u.x * w.y = u.z - v.z.
```

The development proves a bounded-solution lemma for this equation directly,
by reducing one solution modulo a nonzero coefficient and separately handling
the zero-coefficient cases.  This gives the explicit global upper bound

```lean
conjugatorLengthFunction n ≤ 4 * n^2.
```

For the lower bound, `lowerUWord n` is the literal word

```text
b [a^n,b^n]
```

of length `4n+1`, while `lowerVWord` is `b`.  Their values are conjugate, and
the coordinate conjugacy equation forces every conjugator to have first
coordinate `n²`; the word-coordinate bound then forces its word length to be
at least `n²`.  Lean therefore proves

```lean
n^2 ≤ conjugatorLengthFunction (4*n + 2).
```

Finally `Dominated` is exactly the paper's relation

```text
f(n) ≤ C g(Cn+C) + Cn + C
```

for some positive integer `C`, and `GrowthEquivalent` is mutual domination.
The explicit upper and lower bounds yield the theorem with `C = 4` in both
directions.

## Checking

From this directory:

```bash
lake env lean ConjugatorLength/Heisenberg.lean
lake build ConjugatorLength.Heisenberg
lake env lean ConjugatorLength/Main.lean
lake build ConjugatorLength
```

The intermediate build is needed before checking `Main.lean` directly because
it imports the first local module.  The complete library build also handles
the dependency automatically.

## Assumptions and tooling

No external theorem is assumed under the exception in the task.  The proof
uses only Lean's logic and mathlib.  No network resources or additional
packages were needed.  An explicit `#print axioms` audit of the final theorem
reports only Lean/mathlib's standard logical principles `propext`,
`Classical.choice`, and `Quot.sound`; there are no project-defined axioms.

One harmless sign convention deserves mention.  With the paper's declared
commutator convention `[a,b]=a⁻¹b⁻¹ab` and relation `[a,b]=c`, the displayed
lower-bound word `b[a^n,b^n]` is conjugated to `b` by the positive
`a^{n²}` coordinate in this matrix convention.  The paper writes an inverse
power in one sentence of that calculation.  The coordinate equation (6), the
length lower bound, and the quadratic theorem are unaffected; the Lean proof
checks the defining equation `u*w=w*v` directly.