[dkaysin]

This PR adds reachability and connectedness results for Cayley Simple graphs.

---

Implements connectedness results requested here.

Implementation details:

• One-directional reachability results can also be proven for semigroups and monoids. I chose to implement one such result for monoids: reachable_mulCayley_mul_of_mem_submonoidClosure.
• Machinery with values of darts can be useful for further proofs when working with Cayley graphs in geometric group theory. Edit: made private for now as per reviewer's comment.

Use of AI: I used Claude Opus 5.5 for the following tasks:

• To brainstorm and compare API design ideas and naming conventions
• To propose simplifications to proofs
• To check 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 885510aa03

Import changes exceeding 2%

%	File
+43.31%	Mathlib.Combinatorics.SimpleGraph.Cayley

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Combinatorics.SimpleGraph.Cayley	688	986	+298 (+43.31%)

Import changes for all files

Files	Import difference
Mathlib.Combinatorics.SimpleGraph.Cayley	298

---

Declarations diff (regex)

+ Dart.fstInvMulSnd
+ Dart.fstInvMulSnd_mem_subgroupClosure
+ Dart.fstInvMulSnd_mk
+ Walk.prod_map_fstInvMulSnd_darts
+ connected_mulCayley_iff
+ preconnected_mulCayley_iff
+ reachable_mulCayley_iff
+ reachable_mulCayley_mul_of_mem_submonoidClosure

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

• +20 new declarations
• −0 removed declarations

+SimpleGraph.Dart.addValue
+SimpleGraph.Dart.addValue_mem_addSubgroupClosure
+SimpleGraph.Dart.addValue_mk
+SimpleGraph.Dart.addValue_symm
+SimpleGraph.Dart.edge_eq_iff_addValue_add_eq_zero
+SimpleGraph.Dart.edge_eq_iff_value_mul_eq_one
+SimpleGraph.Dart.value
+SimpleGraph.Dart.value_mem_subgroupClosure
+SimpleGraph.Dart.value_mk
+SimpleGraph.Dart.value_symm
+SimpleGraph.Walk.prod_map_value_darts
+SimpleGraph.Walk.sum_map_addValue_darts
+SimpleGraph.connected_addCayley_iff
+SimpleGraph.connected_mulCayley_iff
+SimpleGraph.inv_mul_mem_subgroupClosure_of_reachable_mulCayley
+SimpleGraph.neg_add_mem_addSubgroupClosure_of_reachable_addCayley
+SimpleGraph.reachable_addCayley_add_of_mem_addSubmonoidClosure
+SimpleGraph.reachable_addCayley_iff
+SimpleGraph.reachable_mulCayley_iff
+SimpleGraph.reachable_mulCayley_mul_of_mem_submonoidClosure

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 885510aa03
Reference commit 930ae14551

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

[dkaysin]

-awaiting-author