feat(Archive): dual Langer graph, non-isomorphism via d₃-connectivity#39702
feat(Archive): dual Langer graph, non-isomorphism via d₃-connectivity#39702RaggedR wants to merge 19 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.
Link to symmetry-aware drawings hosted in the symmetric-graphs repo.
Formal proof that the G₂(2) action on 63 points is primitive, using
Atkinson's queue-based block closure algorithm. For every v ≠ 0, the
smallest block containing {0, v} is all of Ω — no non-trivial block
system exists, so Stab(0) = H₁₉₂ is a maximal subgroup of G₂(2).
…endent The induced subgraph of the Tutte 12-cage on its 63 point-vertices is edgeless, obstructing any covering map to the 6-regular Langer graph (which has 189 edges). No cubic double cover of the Langer graph exists.
Formal proof that the PSL(2,13) action on 91 cosets of D₁₂ is primitive, using Atkinson's algorithm. Same technique as the Langer graph proof.
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).
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).
…abidussi The Langer graph has three independent definitions: 1. Algebraic — via the Zorn product on Q(6,2) 2. Geometric — distance-2 in the Tutte 12-cage restricted to points 3. Group-theoretic — Sab(G₂(2), H₁₉₂, D) The equivalence (1) ≃g (3) is langerSabidussiIso (Sabidussi representation). The equivalence (2) ≃g (3) is dist2SabidussiIso (same connection set D at vertex 0, proved via graphs_agree_at_zero). Composing gives (1) ≃g (2): langer_iso_tutte12_distance2. The key: both graphs map to the SAME coset graph because they share the same connection set at vertex 0 (connectionSet_eq). The orbit-stabilizer bijection sabidussiEquiv depends only on the group action, not the graph.
…into feat/langer-structural # Conflicts: # Archive/LangerGraph.lean
Extends the Langer graph formalization with its dual: the line-collinearity
graph of GH(2,2), defined as the distance-2 graph of the Tutte 12-cage
restricted to line vertices.
Both graphs share the intersection array {6,4,4; 1,1,3} but are proved
non-isomorphic via a BFS-computed d₃-connectivity invariant, verified at
all 63 vertices by native_decide.
github-actions
Bot
added
the
new-contributor
|
maintainer merge — please add the LLM-generated label |
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 03e1526124
|
| 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
+ AllPairsReachable
+ 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
+ bfsExpand
+ bfsLayers
+ blockIsFullBool
+ connectionSet
+ connectionSet_eq_doubleCoset
+ cosetProjection
+ cosetProjection_mk
+ cosetProjection_surjective
+ cosetQuotientMap
+ cosetQuotientMap_mk
+ decAllPairsReachable
+ disjoint_stabilizer
+ distanceLayer
+ doubleCoset_isConnectionSet
+ double_coset_stable
+ dualLangerAdjBool
+ dualLangerDecAdj
+ dualLangerSimpleGraph
+ dualLanger_d3_not_allPairs
+ dualLanger_d3_not_connected
+ dualLanger_d3_num_components
+ dualLanger_d3_size
+ dualLanger_edges
+ dualLanger_eq_tutte12_distance2_lines
+ dualLanger_lambda
+ dualLanger_regular
+ 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
+ inducedBfsReach
+ inv_eq_self_of_sq_eq_one
+ inv_mem
+ isArcTransitive_of_vertexTransitive_locallyTransitive
+ isConnectionSet
+ isD3ConnectedBool
+ isInducedConnectedBool
+ iso_AllPairsReachable
+ iso_bfsExpand
+ iso_bfsLayers
+ iso_biUnion_neighbors
+ iso_distanceLayer
+ iso_inducedBfsReach
+ iso_induced_neighbors
+ langerAdjBool
+ langerDecAdj
+ langerG
+ langerGens
+ langerGraphAction
+ langerMulAction
+ langerPretransitive
+ langerSabidussiIso
+ langerSimpleGraph
+ langer_action_primitive
+ langer_d3_allPairs
+ langer_d3_connected
+ langer_d3_num_components
+ langer_d3_size
+ langer_edges
+ langer_eq_tutte12_distance2'
+ langer_not_iso_dualLanger
+ langer_regular
+ locallyTransitive_at_one
+ locallyTransitive_everywhere
+ lorimer_forward
+ lorimer_reverse
+ mergeRep
+ mergeRep91
+ numD3Components
+ 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.
No changes to strong technical debt.
No changes to weak technical debt.
b-mehta
added
the
LLM-generated
|
Please refrain from posting any more PRs to this repository. Spamming the repository will result in a ban. |
|
Apologies for the volume — I got carried away and should have waited for earlier PRs to be reviewed before opening more. I've converted all but two foundational PRs to drafts and will proceed incrementally from here. |
2 participants
Depends on #39649.
This PR introduces the dual Langer graph, the line-collinearity graph of the split Cayley hexagon GH(2,2). Where the Langer graph (defined in #39649) connects points that share a line, the dual Langer graph connects lines that share a point. Concretely, it is the distance-2 graph of the Tutte 12-cage restricted to the line vertices (indices 63–125).
GH(2,2) is not self-dual. Cohen and Tits showed that a generalized hexagon GH(q,q) is self-dual if and only if q is a power of 3. Since q = 2 fails this condition, the point-collinearity and line-collinearity graphs are genuinely distinct objects, despite sharing the same intersection array {6,4,4; 1,1,3}, the same regularity (6-regular, 189 edges), and the same λ = 1.
The distinguishing invariant is the connectivity of the d₃-induced subgraph. For any vertex v, the subgraph induced on vertices at graph distance 3 from v is connected (1 component) in the Langer graph and disconnected (2 components of 16 vertices) in the dual. This is verified at all 63 vertices by native_decide, providing a computable non-isomorphism certificate.
The non-isomorphism theorem is proved structurally. A chain of lemmas establishes that graph isomorphisms commute with BFS layer computation (iso_bfsExpand, iso_bfsLayers, iso_distanceLayer) and with BFS reachability within induced subsets (iso_inducedBfsReach, iso_AllPairsReachable). The all-pairs reachability predicate is starting-vertex-independent, avoiding the need for a BFS-start-independence lemma. Since the Langer d₃-subgraph is all-pairs reachable and the dual Langer d₃-subgraph is not, no isomorphism can exist.
This PR also exposes tutte12AdjBool (previously private) so that the dual graph can be defined in terms of the Tutte 12-cage adjacency.
LLM tools were used to assist with Lean formalization. The mathematical content is the author's own work.