feat(Geometry/Group): define a via word metric with respect to Group.Generators via wordProd.

[homeowmorphism]

A word over a generating family P : Group.Generators G ι is a list of letters, each carrying a
sign: List (ι × Bool). The evaluation map is then given by Group.Generators.wordProd.

The word length of an element is the length of a shortest representing word, over a generating
family given by Group.Generators, and the word metric is the distance it induces on G. The
resulting object is NormGroup G with dist g h = ‖g⁻¹ * h‖.

---

Use of AI: Claude Fable was used to advise with API design using mathlib-api. I also used it to pair-program with me which means it would (at times heavily) hint at how to write statements/proofs. I used it for golfing and re-factoring as well.

[github-actions]

PR summary 8433b14463

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Geometry.Group.WordProd (new file)	711
Mathlib.Geometry.Group.WordMetric (new file)	1113

---

Declarations diff (regex)

+ IsGeodesic
+ IsGeodesic.eq
+ exists_isGeodesic
+ groupNorm
+ normedGroup
+ wordLength
+ wordLength_eq_zero_iff
+ wordLength_inv
+ wordLength_inv_le
+ wordLength_mul_le
+ wordLength_one
+ wordLength_wordProd_le
+ wordProd
+ wordProd_append
+ wordProd_cons
+ wordProd_invRev
+ wordProd_nil
+ wordProd_singleton
+ wordProd_surjective

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- stale; merge master and push to refresh)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit cac7921).

• +19 new declarations
• −0 removed declarations

+Group.Generators.IsGeodesic
+Group.Generators.IsGeodesic.eq
+Group.Generators.exists_isGeodesic
+Group.Generators.groupNorm
+Group.Generators.normedGroup
+Group.Generators.wordLength
+Group.Generators.wordLength_eq_zero_iff
+Group.Generators.wordLength_inv
+Group.Generators.wordLength_inv_le
+Group.Generators.wordLength_mul_le
+Group.Generators.wordLength_one
+Group.Generators.wordLength_wordProd_le
+Group.Generators.wordProd
+Group.Generators.wordProd_append
+Group.Generators.wordProd_cons
+Group.Generators.wordProd_invRev
+Group.Generators.wordProd_nil
+Group.Generators.wordProd_singleton
+Group.Generators.wordProd_surjective

---

No changes to strong technical debt.

Increase in weak tech debt: (relative, absolute) = (2.00, 0.00)

Current number	Change	Type (weak)
exposed public sections	5001	2

Current commit 8433b14463
Reference commit 13bd10aec8

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[github-actions]

🚨 PR Title Needs Formatting

Please update the title to match our commit style conventions.

Errors from script:

labels are [t-geometric-group-theory]
error: the PR title should not end with a space

Details on the required title format

The title should fit the following format:

<kind>(<optional-scope>): <subject>

<kind> is:

• feat (feature)
• fix (bug fix)
• doc (documentation)
• style (formatting, missing semicolons, ...)
• refactor
• test (when adding missing tests)
• chore (maintain)
• perf (performance improvement, optimization, ...)
• ci (changes to continuous integration, repo automation, ...)

<optional-scope> is a name of module or a directory which contains changed modules.
This is not necessary to include, but may be useful if the <subject> is insufficient.
The Mathlib directory prefix is always omitted.
For instance, it could be

• Data/Nat/Basic
• Algebra/Group/Defs
• Topology/Constructions

<subject> has the following constraints:

• do not capitalize the first letter
• no dot(.) at the end
• use imperative, present tense: "change" not "changed" nor "changes"

[homeowmorphism]

Starting to wonder if I should call “wordLength” just “length” or use the Coxeter notation as “wordLength” over a group element sounds misleading.

[tb65536]

Suggested change

	lemma wordProd_singleton : P.wordProd [(i,b)] = cond b (P.val i) (P.val i)⁻¹ := by
	lemma wordProd_singleton : P.wordProd [(i, b)] = cond b (P.val i) (P.val i)⁻¹ := by

[tb65536]

I wonder, perhaps this one should be tagged @[simp] instead of wordProd_singleton?

[tb65536]

Suggested change

	* `Group.Generators.IsGeodesic`: a word is geodesic if of minimal length among the words
	* `Group.Generators.IsGeodesic`: a word is geodesic if it is of minimal length among the words

[tb65536]

I wonder whether it's worth proving a lemma like this:

/-- The word length of a group element given by a word `l` is smaller or equal to the
length of `l`. -/
lemma wordLength_le_iff {n : ℕ} :
    P.wordLength g ≤ n ↔ ∃ l, l.length ≤ n ∧ P.wordProd l = g := by
  classical
  have h : {n | ∃ l, P.wordProd l = g ∧ l.length = n}.Nonempty := sorry
  rw [wordLength, Nat.sInf_def h]
  simp

This might help golf wordLength_eq_zero_iff, for instance.