feat(Archive): Langer graph, Tutte 12-cage, and structural equality via G₂(2)

[RaggedR]

This adds three constructions from the theory of generalized polygons over finite fields to Archive/, and proves they give the same graph using the Sabidussi representation theorem from #39548 and #39550.

The Langer graph (63 vertices, 6-regular) is the collinearity graph of the split Cayley hexagon GH(2,2). It has three independent definitions: algebraically via the Zorn product on Q(6,2) (langerSimpleGraph), geometrically as the distance-2 graph of the Tutte 12-cage restricted to points (tutte12Distance2Graph), and group-theoretically as the coset graph Sab(G₂(2), H₁₉₂, D) where H₁₉₂ is the point stabiliser of order 192 (langerCosetGraph).

The main result langer_iso_tutte12_distance2 proves the algebraic and geometric definitions are isomorphic by composing two Sabidussi isos through a common coset graph. Both graphs are G₂(2)-invariant and arc-transitive, so sabidussiIso maps each to Sab(G₂(2), Stab(0), D). Since they have the same 6 neighbors at vertex 0, their connection sets are equal (dist2_connectionSet_eq), so both map to the same coset graph. The proof is langerSabidussiIso.trans dist2SabidussiIso.symm.

Also included: the Tutte 12-cage (126 vertices, semisymmetric because GH(2,2) has no polarity over F₂), and self-orthogonality of the Q(6,2) parity-check matrix.

Generator data was produced by compute_g2_generators.py in the source repo at RaggedR/symmetric-graphs.

Depends on #39548 (coset graphs), #39550 (Sabidussi representation), #39551 (quotient graphs). The sabidussiIso, connectionSet, and GraphAction from those PRs are load-bearing in the equivalence proof.

---

LLM tools were used to assist with Lean formalization. The mathematical content is the author's own work.

[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 https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary 0f9eb98bf2

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Combinatorics.SimpleGraph.Action (new file)	644
Mathlib.Combinatorics.SimpleGraph.CosetGraph (new file)	837
Mathlib.Combinatorics.SimpleGraph.Representation (new file)	838
Mathlib.Combinatorics.SimpleGraph.Symmetric (new file)	839
Mathlib.Combinatorics.SimpleGraph.QuotientGraph (new file)	962

---

Declarations diff (regex)

+ GraphAction
+ IsArcTransitive
+ IsConnectionSet
+ IsLocallyTransitive
+ IsVertexTransitive
+ Q62_H
+ Q62_self_orthogonal
+ Q62form
+ SimpleGraph.cosetGraph
+ SimpleGraph.cosetGraph.proj_adj
+ SimpleGraph.quotientGraph
+ adj_mk
+ adj_smul_iff
+ applyGen
+ applyGen_dist2_inv
+ applyGen_langer_inv
+ applyGen_mem
+ applyWord
+ applyWord_dist2_inv
+ applyWord_langer_inv
+ applyWord_mem
+ atkinson
+ atkinson91
+ blockIsFullBool
+ connectionSet
+ connectionSet_eq_doubleCoset
+ cosetProjection
+ cosetProjection_mk
+ cosetProjection_surjective
+ cosetQuotientMap
+ cosetQuotientMap_mk
+ disjoint_stabilizer
+ doubleCoset_isConnectionSet
+ double_coset_stable
+ expandConnectionSet
+ expandConnectionSet_isConnectionSet
+ g2AllGens
+ g2gen1
+ g2gen1Fwd
+ g2gen1Fwd_size
+ g2gen1Inv
+ g2gen1Inv_size
+ g2gen1_dist2_inv
+ g2gen1_langer_inv
+ g2gen2
+ g2gen2Fwd
+ g2gen2Fwd_size
+ g2gen2Inv
+ g2gen2Inv_size
+ g2gen2_dist2_inv
+ g2gen2_langer_inv
+ graphAction
+ graphs_agree_at_zero
+ inv_eq_self_of_sq_eq_one
+ inv_mem
+ isArcTransitive_of_vertexTransitive_locallyTransitive
+ isConnectionSet
+ langerAdjBool
+ langerDecAdj
+ langerG
+ langerGens
+ langerGraphAction
+ langerMulAction
+ langerPretransitive
+ langerSabidussiIso
+ langerSimpleGraph
+ langer_action_primitive
+ langer_edges
+ langer_eq_tutte12_distance2'
+ langer_regular
+ locallyTransitive_at_one
+ locallyTransitive_everywhere
+ lorimer_forward
+ lorimer_reverse
+ mergeRep
+ mergeRep91
+ q62Indices
+ q62Point
+ q62_card
+ quotient_cosetGraph_iso
+ sabidussiEquiv
+ sabidussiEquiv_smul
+ sabidussiEquiv_symm_mk
+ sabidussiIso
+ sabidussiSymmetricGraph
+ stabilizer_transitive_on_neighbors
+ symm_preserves_dist2
+ symm_preserves_langer
+ toBitVec
+ toIso
+ toIso_apply
+ toIso_mul
+ toIso_symm
+ transport_dist2
+ transport_langer
+ tutte12AdjBool
+ tutte12CageGraph
+ tutte12DecAdj
+ tutte12Distance2Bool
+ tutte12Edges
+ tutte12Side
+ tutte12_bipartite
+ tutte12_points_independent
+ tutte12_regular
+ witnessWord
+ witnessWordData
+ witnessWordData_size
+ witnessWord_correct
+ zhou6AllGens
+ zhou6BlockIsFullBool
+ zhou6Gen1
+ zhou6Gen1Fwd
+ zhou6Gen1Fwd_size
+ zhou6Gen1Inv
+ zhou6Gen1Inv_size
+ zhou6Gen2
+ zhou6Gen2Fwd
+ zhou6Gen2Fwd_size
+ zhou6Gen2Inv
+ zhou6Gen2Inv_size
+ zhou6_action_primitive
++ isVertexTransitive
++ one_not_mem

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

Computed after the build finishes.

---

No changes to strong technical debt.

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

Current number	Change	Type (weak)
4995	5	exposed public sections

Current commit 0f9eb98bf2
Reference commit 88d006abbc

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

[RaggedR]

Could a maintainer please add the LLM-generated label? Claude was used as a coding assistant for the Lean formalisation. Thank you.

[wwylele]

Hi, you can add the LLM-generated tag yourself. See here

Could you explain more on why you want these to be Mathlib's Archive, as opposite to a separately maintained repo?

[RaggedR]

LLM-generated

[RaggedR]

Hi @wwylele, apologies for the slow response to your question.

You're right to ask why this belongs in Archive rather than a separate repo. The honest answer is that the original PR wasn't demonstrating what it should have been. I was relying on Claude for the Lean formalisation, and it brute-forced the main equivalence proof via manual generator transport instead of using the Sabidussi representation theorem — which is the whole point of the upstream library PRs. I didn't catch this until your comment made me look more carefully at what was actually in the code.

I've now reworked the PR substantially. The main theorem (langer_iso_tutte12_distance2) proves that three independent definitions of the Langer graph are isomorphic — the algebraic definition via the Zorn product on Q(6,2), the geometric definition as the distance-2 graph of the Tutte 12-cage, and the group-theoretic definition as the Sabidussi coset graph Sab(G₂(2), H₁₉₂, D). The proof is a one-liner composing two Sabidussi representation isomorphisms through a common coset graph: both graphs have the same connection set at vertex 0, so both map to the same coset graph, so they're isomorphic to each other. This genuinely uses sabidussiIso from the representation theorem as the proof engine.

This PR now depends on the earlier Sabidussi construction PRs (#39548, #39550, #39551) which define cosetGraph, sabidussiIso, and quotientGraph in Mathlib. The Archive file is a non-trivial consumer of that library code — the abstract representation theorem is doing real work, not just sitting there as decoration. I've also gone back through the other PRs in the series and updated proofs where Claude had similarly brute-forced things that should have used the Sabidussi framework.

The reason I think this belongs in Archive: it connects algebraic graph theory to finite geometry on a concrete example (the split Cayley hexagon GH(2,2) and the exceptional group G₂(2)), and the proof depends on the new Mathlib library in a way that a standalone repo wouldn't demonstrate. Sorry again for the initial state of the PR — lesson learned about reviewing AI-generated proofs more carefully before submitting.

[RaggedR]

Please add the LLM-generated label to this PR.

[mathlib-bors]

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.