[dkaysin]

This PR constructs the Cayley graph (realized as a SimpleGraph) for a group G with respect to a generating family P : Group.Generators G ι, implements the link between walks in the Cayley graph and words, and establishes equivalence of the word metric and the distance on the Cayley graph.

---

Resolves TODO from #43118.

Implementation details:

• SimpleGraph was chosen vs Quiver/Schreier because it has a more comprehensive API at the moment. More context: Zulip thread.
• To accommodate possible future implementation for Quiver/Schreier, I've included "Simple" in the names of definitions and theorems (e.g., cayleySimpleGraph).
• Because simple graph has no loops, in several places we have to check that a letter/generator is not trivial.

Use of AI: I used Claude Opus 5.5 to help me with gathering context, designing API and implementation of several proofs.

• I used AI to brainstorm and compare API design ideas based on the context from previous Zulip threads and existing repo code.
• I used AI for suggesting parts of the proofs for exists_walk_of_word and exists_word_of_walk lemmas.
• I used AI for checking docstrings for consistency.

All AI-generated content was reviewed and edited by me.

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to Zulip and join the Lean community.
Thank you again for joining our community.

[github-actions]

PR summary 279e4103bb

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Geometry.Group.CayleySimpleGraph (new file)	1311

---

Declarations diff (regex)

+ AddGroup.Generators
+ IsLetter
+ cayleySimpleGraph
+ cayleySimpleGraph_adj
+ dist_cayleySimpleGraph
+ dist_cayleySimpleGraph_one_left
+ exists_walk_of_word
+ exists_word_of_walk
+ isLetter_iff

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)

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

• +64 new declarations
• −0 removed declarations

+AddGroup.Generators
+AddGroup.Generators.IsGeodesic
+AddGroup.Generators.IsGeodesic.eq
+AddGroup.Generators.IsLetter
+AddGroup.Generators.addGroupNorm
+AddGroup.Generators.casesOn
+AddGroup.Generators.cayleySimpleGraph
+AddGroup.Generators.cayleySimpleGraph_adj
+AddGroup.Generators.closure_eq_top
+AddGroup.Generators.ctorIdx
+AddGroup.Generators.dist_cayleySimpleGraph
+AddGroup.Generators.dist_cayleySimpleGraph_zero_left
+AddGroup.Generators.exists_isGeodesic
+AddGroup.Generators.exists_walk_of_word
+AddGroup.Generators.exists_word_of_walk
+AddGroup.Generators.fg
+AddGroup.Generators.hom_ext
+AddGroup.Generators.isLetter_iff
+AddGroup.Generators.lift
+AddGroup.Generators.lift_surjective
+AddGroup.Generators.map
+AddGroup.Generators.map_val
+AddGroup.Generators.mk
+AddGroup.Generators.mk.inj
+AddGroup.Generators.mk.injEq
+AddGroup.Generators.mk.noConfusion
+AddGroup.Generators.mk.sizeOf_spec
+AddGroup.Generators.noConfusion
+AddGroup.Generators.noConfusionType
+AddGroup.Generators.normedAddGroup
+AddGroup.Generators.ofFreeAddGroupHom
+AddGroup.Generators.ofFreeAddGroupHom_lift
+AddGroup.Generators.ofFreeAddGroupHom_val
+AddGroup.Generators.ofSet
+AddGroup.Generators.ofSet_val
+AddGroup.Generators.range_lift_eq_top
+AddGroup.Generators.rec
+AddGroup.Generators.recOn
+AddGroup.Generators.reindex
+AddGroup.Generators.reindex_val
+AddGroup.Generators.val
+AddGroup.Generators.wordLength
+AddGroup.Generators.wordLength_add_le
+AddGroup.Generators.wordLength_eq_zero_iff
+AddGroup.Generators.wordLength_le_iff
+AddGroup.Generators.wordLength_neg
+AddGroup.Generators.wordLength_wordSum_le
+AddGroup.Generators.wordLength_zero
+AddGroup.Generators.wordSum
+AddGroup.Generators.wordSum_append
+AddGroup.Generators.wordSum_cons
+AddGroup.Generators.wordSum_negRev
+AddGroup.Generators.wordSum_nil
+AddGroup.Generators.wordSum_singleton
+AddGroup.Generators.wordSum_surjective
+AddGroup.fg_iff_nonempty_finite_generators
+Group.Generators.IsLetter
+Group.Generators.cayleySimpleGraph
+Group.Generators.cayleySimpleGraph_adj
+Group.Generators.dist_cayleySimpleGraph
+Group.Generators.dist_cayleySimpleGraph_one_left
+Group.Generators.exists_walk_of_word
+Group.Generators.exists_word_of_walk
+Group.Generators.isLetter_iff

---

No changes to strong technical debt.

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

Current number	Change	Type (weak)
5101	1	exposed public sections

Current commit 279e4103bb
Reference commit 74e558e2f8

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).