feat(Archive): primitivity of Langer and Zhou-6, covering structure#39686
feat(Archive): primitivity of Langer and Zhou-6, covering structure#39686RaggedR wants to merge 15 commits into
Conversation
This adds the first connection between Mathlib's `MulAction` and `SimpleGraph` libraries, defining what it means for a group action to preserve adjacency and providing the standard transitivity predicates used in algebraic graph theory. The `GraphAction` class asserts that `g • u` is adjacent to `g • v` whenever `u` is adjacent to `v`. For group actions this is automatically an iff (`adj_smul_iff`), and each group element induces a graph isomorphism (`toIso`). On top of this, `IsVertexTransitive` combines `GraphAction` with `IsPretransitive`, and `IsArcTransitive` requires transitivity on ordered adjacent pairs. The main result is the characterization theorem: a vertex-transitive graph that is locally transitive (the stabilizer of each vertex acts transitively on its neighbors) is arc-transitive, and conversely an arc-transitive graph with no isolated vertices is vertex-transitive. This is the standard equivalence between arc-transitivity and the combination of vertex-transitivity with local transitivity, used throughout the theory of symmetric graphs.
…ia G₂(2) The Langer graph (collinearity graph of GH(2,2), 63 vertices, 6-regular) is defined algebraically via the Zorn product on Q(6,2). The Tutte 12-cage (incidence graph of GH(2,2), 126 vertices, semisymmetric) is defined by edge list. Their equality — algebraic Langer = geometric distance-2 — is proved structurally via G₂(2) transitivity: both graphs are invariant under two generators of G₂(2) and agree at vertex 0. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Link to symmetry-aware drawings hosted in the symmetric-graphs repo. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Add langerSabidussiIso: the Langer graph (63 vertices, 6-regular) is isomorphic to the coset graph Sab(G₂(2), H₁₉₂, D) via the Sabidussi representation theorem. G₂(2) = ⟨σ₁, σ₂⟩ ≤ Sym(63) acts vertex-transitively preserving adjacency (via closure_induction), so sabidussiIso gives the graph isomorphism to cosetGraph(stabilizer, connectionSet). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Add the natural projection G ⧸ H → G ⧸ K when H ≤ K and prove it is a graph homomorphism for coset graphs sharing the same connection set. Cherry-picked from feat/coset-graph (d4e81f9). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Two primitivity results and two covering results for cubic arc-transitive graphs: 1. Langer graph (63v, 6-regular) — G₂(2) acts primitively (Atkinson's algorithm) 2. Zhou-6 graph (91v, 6-regular) — PSL(2,13) acts primitively (Atkinson's algorithm) 3. Zhou-3 (182v, cubic) → Zhou-6 covering via Z₂ block system (S₃ ≤ D₁₂) 4. No cubic double cover of Langer — Tutte 12-cage point subgraph is edgeless Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
github-actions
Bot
added
the
new-contributor
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 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. |
PR summary c76bfaec2e
|
| Files | Import difference |
|---|---|
Mathlib.Combinatorics.SimpleGraph.Action (new file) |
648 |
Mathlib.Combinatorics.SimpleGraph.CosetGraph (new file) |
842 |
Mathlib.Combinatorics.SimpleGraph.Representation (new file) |
843 |
Mathlib.Combinatorics.SimpleGraph.Symmetric (new file) |
844 |
Mathlib.Combinatorics.SimpleGraph.QuotientGraph (new file) |
967 |
Declarations diff
+ 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
+ atkinson63
+ atkinson91
+ blockIsFull63
+ blockIsFull91
+ connectionSet
+ connectionSet_eq_doubleCoset
+ cosetProjection
+ cosetProjection_mk
+ cosetProjection_surjective
+ cosetQuotientMap
+ cosetQuotientMap_mk
+ disjoint_stabilizer
+ doubleCoset_isConnectionSet
+ double_coset_stable
+ expandConnectionSet
+ expandConnectionSet_isConnectionSet
+ 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
+ mergeRep63
+ 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
+ zhou3AdjBool
+ zhou3DecAdj
+ zhou3Edges
+ zhou3Graph
+ zhou3_edges
+ zhou3_regular
+ zhou6AdjBool
+ zhou6DecAdj
+ zhou6Edges
+ zhou6Gen1
+ zhou6Gen1Fwd
+ zhou6Gen1Fwd_size
+ zhou6Gen1Inv
+ zhou6Gen1Inv_size
+ zhou6Gen1_adj
+ zhou6Gen2
+ zhou6Gen2Fwd
+ zhou6Gen2Fwd_size
+ zhou6Gen2Inv
+ zhou6Gen2Inv_size
+ zhou6Gen2_adj
+ zhou6Graph
+ zhou6_action_primitive
+ zhou6_edges
+ zhou6_eq_quotient
+ zhou6_regular
+ zhouBlockMap
+ zhouBlockMap_fibre_size
+ zhouBlockMap_hom
+ zhouBlockMap_surj
++ 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.
No changes to strong technical debt.
No changes to weak technical debt.
The generic `blockIsFullGeneric {n : Nat}` failed to resolve
DecidableEq instances at native_decide time. Use concrete
`blockIsFull63` and `blockIsFull91` instead.
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This comment was marked as low quality.
This comment was marked as low quality.
The style linter requires `change` instead of `show` when the tactic modifies the goal rather than just annotating it. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
|
We appreciate your desire to contribute to mathlib. Unfortunately, this PR does not meet community standards. Our reviewer time is very limited so we must prioritize both individuals who can learn and contribute back to the community and sufficiently high quality content as to make the process smooth and valuable. |
mathlib-triage
Bot
added
the
LLM-generated
|
Note for future reference: the Zhou-3 → Zhou-6 covering relationship proved here by brute force (native_decide on all vertex pairs) has a cleaner algebraic proof in #39695, which uses Lorimer's quotient theorem. The block system is shown to be PSL(2,13)-invariant by closure induction, the overgroup K = D₁₂ is the setwise stabilizer of {0, 137}, and the quotient follows from quotient_cosetGraph_iso with H ≤ K and D ∩ K = ∅ verified structurally. |
1 participant
Four results connecting primitivity and covering structure for cubic arc-transitive graphs.
The Langer graph has a primitive action: G₂(2) acts primitively on 63 points because H₁₉₂ is a maximal subgroup, verified by Atkinson's block-merging algorithm (1975). For each v ≠ 0, the smallest block containing {0, v} is verified to be all of Ω. The Zhou-6 graph is also primitive: PSL(2,13) acts primitively on 91 points because D₁₂ is maximal, again by Atkinson's algorithm.
The Zhou-3 graph (F182A, 182 vertices, cubic) is a Z₂ double cover of the Zhou-6 graph (91 vertices, 6-regular) via the block system S₃ ≤ D₁₂. In the other direction, there is no cubic double cover of the Langer graph — the Tutte 12-cage point subgraph is edgeless, obstructing any covering map.
Primitivity is proved computationally via Atkinson's algorithm, with generator data computed in GAP and verified by Lean's native_decide.
Depends on #39649 (LangerGraph).
LLM tools were used to assist with Lean formalization. The mathematical content is the author's own work.