feat(Archive): Meinhold family — five Sabidussi coset graphs of G₂(2)#39698
feat(Archive): Meinhold family — five Sabidussi coset graphs of G₂(2)#39698RaggedR wants to merge 36 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.
Defines CellularSurface (2-cell embedding of a graph on a closed surface) with boundary operators ∂₁, ∂₂ over F₂ and proves the chain complex condition ∂₁∘∂₂ = 0. Rank theorems rank(∂₁) = V-1 and rank(∂₂) = F-1 via kernel characterisation of connected graphs. Assembles into the CSS surface code theorem: a genus-g surface tiling encodes k = 2g logical qubits (Breuckmann-Terhal, arXiv:1506.04029).
Four CellularSurface instances spanning three orders of magnitude: - Heawood (genus 1): Fano plane on torus, 14V/21E/7F, k=2 - Bolza (genus 2): Möbius-Kantor on genus 2, 16V/24E/6F, k=4 - Klein quartic (genus 3): PSL(2,7) on genus 3, 56V/84E/24F, k=6 - Clayworth (genus 505): G₂(2)/C₃ on genus 505, 4032V/6048E/1008F, k=1010 Klein and Clayworth use Array-backed data to avoid elaborator crash on large vector literals.
Each surface docstring now names the Sabidussi graph: Sab(G₄₂, C₃), Sab(GL(2,3), C₃), Sab(PSL(2,7), C₃) (primitive), Sab(G₂(2), C₃). heawood_surface_eq_voltage bridges the CellularSurface and voltage graph descriptions of the Heawood graph via v ↦ (v/7, v mod 7).
The Zhou graph is cubic arc-transitive on 182 vertices. Contrary to earlier claims, it is IMPRIMITIVE: S₃ is not maximal in PSL(2,13), giving a Z₂ block system with 91 blocks of size 2. Edge list computed by GAP from the suborbit of size 3 in the coset action.
- Add missing documentation string for `CellularSurface.nextPerm` - Remove unused `Pi.one_apply` from two `simp` calls - Replace `show` with `change` where it transforms the goal
Link to symmetry-aware drawings hosted in the symmetric-graphs repo.
Link to underlying graph drawings (Möbius-Kantor F016A and Heawood F014A) hosted in the symmetric-graphs repo.
The Zhou graph's unique block system (91 blocks of size 2) gives the quotient Sab(PSL(2,13), D₁₂), a 6-regular primitive graph. D₁₂ is maximal in PSL(2,13). Quotient defined via zhouGraph.quotientGraph with the block map from GAP. Regularity omitted (existential over Fin 182 too expensive for native_decide).
Both Zhou (182v, 3-reg) and Zhou-6 (91v, 6-reg) now use edge lists from the same suborbit of PSL(2,13). Zhou-6 is defined directly and verified 6-regular. The abstract quotient zhouGraph.quotientGraph zhouBlockMap is also defined. Formal proof of their equality awaits a structural PSL(2,13) argument (native_decide too expensive on the existential over Fin 182²).
All references to "Zhou graph" now say "Zhou-3 graph" to distinguish from the 6-regular Zhou-6 quotient. Re-adds image links that were lost during the Zhou-6 edge list addition.
- Move documentation from copyright block to /-! ... -/ module docstring - Module docstring placed immediately after imports - Replace indented dash lists with * lists (no double spaces) - Wrap data array lines to stay under 100 characters - Wrap ++ concatenation lines in Clayworth
- Move CellularSurface before Colex in Mathlib.lean (alphabetical) - Add set_option linter.style.longFile 4200 for the 4048-line Clayworth surface data file (genus 505, 4032 vertices)
Add kleinSabidussiIso: the Klein graph (56 vertices, cubic) is isomorphic to a coset graph via the Sabidussi representation theorem. PGL(2,7) (order 336) acts vertex-transitively with stabilizer of order 6: kleinGraph ≃g Sab(PGL(2,7), H₆, D) with 56 = 336/6 vertices. Generators computed by GAP (GRAPE AutGroupGraph) from the Lean edge data.
Add SabidussiWitness.lean with shared helpers (applyWord', closureGraphAction, applyWord'_mem) for proving concrete graphs are Sabidussi coset graphs via generators and BFS witness words. Zhou-3 (182v): Sab(PSL(2,13), S₃) — two generators of order 7 and 2 Zhou-6 (91v): Sab(PSL(2,13), D₁₂) — two generators of order 7 and 3 Zhou quotient: zhou6Graph = zhouGraph.quotientGraph zhouBlockMap, proved via precomputed block representatives to avoid expensive existential quantifiers. Also fixes KleinSurface.lean import to reference SabidussiWitness.
The representation theorem proves an isomorphism for any transitive graph action, but the classical Sabidussi coset graph Sab(G, H, HaH) with a single double coset specifically characterizes arc-transitive (symmetric) graphs. For merely vertex-transitive graphs the connection set may be a union of several double cosets.
Prove bolza_surface_eq_voltage: the Bolza CellularSurface graph (GP(8,3))
is isomorphic to mobiusKantorVoltage (voltageGraphK2 8 0 1 3) via a
GAP-computed bijection. This connects all three descriptions:
CellularSurface (genus 2) ↔ voltageGraphK2 8 {0,1,3} ↔ Sab(GL(2,3), C₃, D)
Lean 4.30 requires all Mathlib/ files to declare `module` and use `public import`. Also fixes `show` → `change` for linter.style.show.
The Clayworth graph (4032 vertices, cubic, genus 505) is a Sabidussi coset graph: Sab(G₂(2), C₃). Two generators (orders 7 and 6) of G₂(2) ≤ Sym(4032) preserve adjacency, and BFS witness words prove vertex-transitivity.
The 4032-vertex IsPretransitive and sabidussiIso need increased maxRecDepth (deep unfolding of Subgroup.closure) and maxHeartbeats (elaboration of group membership proofs with large data).
… longLine - KleinSurface.lean: "Primitive" → "Imprimitive" (C₃ not maximal in PSL(2,7)) - KleinSurface.lean: add `set_option linter.style.longLine false` - ClayworthSabidussi.lean: bump maxHeartbeats 800000 → 1600000 for CI
Replace 4 native_decide proofs checking ∀ u v : Fin 4032 (16M pairs each) with O(n) edge-list checks: for each vertex, verify its 3 neighbors map to neighbors under the generator. 12096 checks instead of 16M per theorem. Build time: 40+ minutes → estimated <1 minute.
Replace the 4048-line array-backed ClayworthSurface with an algebraic construction from the triangle group Δ(2,3,12). The face rotation R (order 12) and vertex rotation S (order 3) generate G₂(2) in its regular representation on 12096 darts. Vertices, edges, and faces arise as left cosets of ⟨S⟩, ⟨T⟩, ⟨R⟩ respectively. The general TriangleGroupSurface construction derives a CellularSurface from any finite quotient of Δ(2,3,r), with face_closed following from the identity T = RS (the "other end" of a dart has the same vertex as its R-successor, because S preserves vertex cosets). Build time drops from >30 minutes (CI timeout) to ~50 seconds.
The Sabidussi coset graph proof for Clayworth (4032 vertices) is independent of the CellularSurface instances and belongs with the Meinhold quotient construction (leanprover-community#39684) where it is actually used. Removing it from this PR eliminates a CI timeout.
|
LLM-generated |
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. |
github-actions
Bot
added
LLM-generated
PR summary af73577478
|
| 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.SabidussiWitness (new file) Mathlib.Combinatorics.SimpleGraph.Symmetric (new file) |
839 |
Mathlib.Combinatorics.SimpleGraph.QuotientGraph (new file) |
962 |
Mathlib.Combinatorics.CellularSurface (new file) |
1669 |
Declarations diff (regex)
+ CSSFromTiling
+ CellularSurface
+ CellularSurface.css_k_eq_2g_from_surface
+ CellularSurface.toSurfaceTiling
+ GraphAction
+ IsArcTransitive
+ IsConnectionSet
+ IsLocallyTransitive
+ IsVertexTransitive
+ KleinSurface_edge_src_data
+ KleinSurface_edge_src_size
+ KleinSurface_edge_tgt_data
+ KleinSurface_edge_tgt_size
+ KleinSurface_face_dir_data
+ KleinSurface_face_dir_size
+ KleinSurface_face_edge_data
+ KleinSurface_face_edge_size
+ Q62_H
+ Q62_self_orthogonal
+ Q62form
+ SimpleGraph.cosetGraph
+ SimpleGraph.quotientGraph
+ SurfaceTiling
+ T
+ TriangleGroupData
+ adj_mk
+ adj_smul_iff
+ applyGen
+ applyGen_dist2_inv
+ applyGen_langer_inv
+ applyGen_mem
+ applyWord
+ applyWord'
+ applyWord'_mem
+ applyWord_dist2_inv
+ applyWord_langer_inv
+ applyWord_mem
+ arrayToFin
+ arrayToFin'
+ atkinson63
+ atkinson91
+ blockIsFull63
+ blockIsFull91
+ bolzaBij
+ bolzaBijData
+ bolzaBijData_size
+ bolzaSurface
+ bolza_d1_mul_d2_eq_zero
+ bolza_euler
+ bolza_surface_eq_voltage
+ clayworth63BlockMap
+ clayworth63BlockMapData
+ clayworth63BlockMapData_size
+ clayworth63BlockMap_degree
+ clayworthAdjBool
+ clayworthDecAdj
+ clayworthEdgeOf_data
+ clayworthEdgeOf_data_c0
+ clayworthEdgeOf_data_c1
+ clayworthEdgeOf_data_c10
+ clayworthEdgeOf_data_c11
+ clayworthEdgeOf_data_c12
+ clayworthEdgeOf_data_c13
+ clayworthEdgeOf_data_c14
+ clayworthEdgeOf_data_c15
+ clayworthEdgeOf_data_c16
+ clayworthEdgeOf_data_c17
+ clayworthEdgeOf_data_c18
+ clayworthEdgeOf_data_c19
+ clayworthEdgeOf_data_c2
+ clayworthEdgeOf_data_c20
+ clayworthEdgeOf_data_c21
+ clayworthEdgeOf_data_c22
+ clayworthEdgeOf_data_c23
+ clayworthEdgeOf_data_c24
+ clayworthEdgeOf_data_c3
+ clayworthEdgeOf_data_c4
+ clayworthEdgeOf_data_c5
+ clayworthEdgeOf_data_c6
+ clayworthEdgeOf_data_c7
+ clayworthEdgeOf_data_c8
+ clayworthEdgeOf_data_c9
+ clayworthEdgeOf_data_size
+ clayworthEdgeRep_data
+ clayworthEdgeRep_data_c0
+ clayworthEdgeRep_data_c1
+ clayworthEdgeRep_data_c10
+ clayworthEdgeRep_data_c11
+ clayworthEdgeRep_data_c12
+ clayworthEdgeRep_data_c2
+ clayworthEdgeRep_data_c3
+ clayworthEdgeRep_data_c4
+ clayworthEdgeRep_data_c5
+ clayworthEdgeRep_data_c6
+ clayworthEdgeRep_data_c7
+ clayworthEdgeRep_data_c8
+ clayworthEdgeRep_data_c9
+ clayworthEdgeRep_data_size
+ clayworthFaceOf_data
+ clayworthFaceOf_data_c0
+ clayworthFaceOf_data_c1
+ clayworthFaceOf_data_c10
+ clayworthFaceOf_data_c11
+ clayworthFaceOf_data_c12
+ clayworthFaceOf_data_c13
+ clayworthFaceOf_data_c14
+ clayworthFaceOf_data_c15
+ clayworthFaceOf_data_c16
+ clayworthFaceOf_data_c17
+ clayworthFaceOf_data_c18
+ clayworthFaceOf_data_c19
+ clayworthFaceOf_data_c2
+ clayworthFaceOf_data_c20
+ clayworthFaceOf_data_c21
+ clayworthFaceOf_data_c22
+ clayworthFaceOf_data_c23
+ clayworthFaceOf_data_c24
+ clayworthFaceOf_data_c3
+ clayworthFaceOf_data_c4
+ clayworthFaceOf_data_c5
+ clayworthFaceOf_data_c6
+ clayworthFaceOf_data_c7
+ clayworthFaceOf_data_c8
+ clayworthFaceOf_data_c9
+ clayworthFaceOf_data_size
+ clayworthFaceRep_data
+ clayworthFaceRep_data_c0
+ clayworthFaceRep_data_c1
+ clayworthFaceRep_data_c2
+ clayworthFaceRep_data_size
+ clayworthGraph
+ clayworthNeighborData
+ clayworthNeighborData_chunk0
+ clayworthNeighborData_chunk1
+ clayworthNeighborData_chunk10
+ clayworthNeighborData_chunk11
+ clayworthNeighborData_chunk12
+ clayworthNeighborData_chunk13
+ clayworthNeighborData_chunk14
+ clayworthNeighborData_chunk15
+ clayworthNeighborData_chunk16
+ clayworthNeighborData_chunk17
+ clayworthNeighborData_chunk18
+ clayworthNeighborData_chunk19
+ clayworthNeighborData_chunk2
+ clayworthNeighborData_chunk20
+ clayworthNeighborData_chunk21
+ clayworthNeighborData_chunk22
+ clayworthNeighborData_chunk23
+ clayworthNeighborData_chunk24
+ clayworthNeighborData_chunk25
+ clayworthNeighborData_chunk26
+ clayworthNeighborData_chunk27
+ clayworthNeighborData_chunk28
+ clayworthNeighborData_chunk29
+ clayworthNeighborData_chunk3
+ clayworthNeighborData_chunk30
+ clayworthNeighborData_chunk4
+ clayworthNeighborData_chunk5
+ clayworthNeighborData_chunk6
+ clayworthNeighborData_chunk7
+ clayworthNeighborData_chunk8
+ clayworthNeighborData_chunk9
+ clayworthNeighborData_size
+ clayworthR_fwd
+ clayworthR_fwd_c0
+ clayworthR_fwd_c1
+ clayworthR_fwd_c10
+ clayworthR_fwd_c11
+ clayworthR_fwd_c12
+ clayworthR_fwd_c13
+ clayworthR_fwd_c14
+ clayworthR_fwd_c15
+ clayworthR_fwd_c16
+ clayworthR_fwd_c17
+ clayworthR_fwd_c18
+ clayworthR_fwd_c19
+ clayworthR_fwd_c2
+ clayworthR_fwd_c20
+ clayworthR_fwd_c21
+ clayworthR_fwd_c22
+ clayworthR_fwd_c23
+ clayworthR_fwd_c24
+ clayworthR_fwd_c3
+ clayworthR_fwd_c4
+ clayworthR_fwd_c5
+ clayworthR_fwd_c6
+ clayworthR_fwd_c7
+ clayworthR_fwd_c8
+ clayworthR_fwd_c9
+ clayworthR_fwd_size
+ clayworthR_inv
+ clayworthR_inv_c0
+ clayworthR_inv_c1
+ clayworthR_inv_c10
+ clayworthR_inv_c11
+ clayworthR_inv_c12
+ clayworthR_inv_c13
+ clayworthR_inv_c14
+ clayworthR_inv_c15
+ clayworthR_inv_c16
+ clayworthR_inv_c17
+ clayworthR_inv_c18
+ clayworthR_inv_c19
+ clayworthR_inv_c2
+ clayworthR_inv_c20
+ clayworthR_inv_c21
+ clayworthR_inv_c22
+ clayworthR_inv_c23
+ clayworthR_inv_c24
+ clayworthR_inv_c3
+ clayworthR_inv_c4
+ clayworthR_inv_c5
+ clayworthR_inv_c6
+ clayworthR_inv_c7
+ clayworthR_inv_c8
+ clayworthR_inv_c9
+ clayworthR_inv_size
+ clayworthS_fwd
+ clayworthS_fwd_c0
+ clayworthS_fwd_c1
+ clayworthS_fwd_c10
+ clayworthS_fwd_c11
+ clayworthS_fwd_c12
+ clayworthS_fwd_c13
+ clayworthS_fwd_c14
+ clayworthS_fwd_c15
+ clayworthS_fwd_c16
+ clayworthS_fwd_c17
+ clayworthS_fwd_c18
+ clayworthS_fwd_c19
+ clayworthS_fwd_c2
+ clayworthS_fwd_c20
+ clayworthS_fwd_c21
+ clayworthS_fwd_c22
+ clayworthS_fwd_c23
+ clayworthS_fwd_c24
+ clayworthS_fwd_c3
+ clayworthS_fwd_c4
+ clayworthS_fwd_c5
+ clayworthS_fwd_c6
+ clayworthS_fwd_c7
+ clayworthS_fwd_c8
+ clayworthS_fwd_c9
+ clayworthS_fwd_size
+ clayworthS_inv
+ clayworthS_inv_c0
+ clayworthS_inv_c1
+ clayworthS_inv_c10
+ clayworthS_inv_c11
+ clayworthS_inv_c12
+ clayworthS_inv_c13
+ clayworthS_inv_c14
+ clayworthS_inv_c15
+ clayworthS_inv_c16
+ clayworthS_inv_c17
+ clayworthS_inv_c18
+ clayworthS_inv_c19
+ clayworthS_inv_c2
+ clayworthS_inv_c20
+ clayworthS_inv_c21
+ clayworthS_inv_c22
+ clayworthS_inv_c23
+ clayworthS_inv_c24
+ clayworthS_inv_c3
+ clayworthS_inv_c4
+ clayworthS_inv_c5
+ clayworthS_inv_c6
+ clayworthS_inv_c7
+ clayworthS_inv_c8
+ clayworthS_inv_c9
+ clayworthS_inv_size
+ clayworthSurface
+ clayworthTriangleData
+ clayworthVertexOf_data
+ clayworthVertexOf_data_c0
+ clayworthVertexOf_data_c1
+ clayworthVertexOf_data_c10
+ clayworthVertexOf_data_c11
+ clayworthVertexOf_data_c12
+ clayworthVertexOf_data_c13
+ clayworthVertexOf_data_c14
+ clayworthVertexOf_data_c15
+ clayworthVertexOf_data_c16
+ clayworthVertexOf_data_c17
+ clayworthVertexOf_data_c18
+ clayworthVertexOf_data_c19
+ clayworthVertexOf_data_c2
+ clayworthVertexOf_data_c20
+ clayworthVertexOf_data_c21
+ clayworthVertexOf_data_c22
+ clayworthVertexOf_data_c23
+ clayworthVertexOf_data_c24
+ clayworthVertexOf_data_c3
+ clayworthVertexOf_data_c4
+ clayworthVertexOf_data_c5
+ clayworthVertexOf_data_c6
+ clayworthVertexOf_data_c7
+ clayworthVertexOf_data_c8
+ clayworthVertexOf_data_c9
+ clayworthVertexOf_data_size
+ clayworthVertexRep_data
+ clayworthVertexRep_data_c0
+ clayworthVertexRep_data_c1
+ clayworthVertexRep_data_c2
+ clayworthVertexRep_data_c3
+ clayworthVertexRep_data_c4
+ clayworthVertexRep_data_c5
+ clayworthVertexRep_data_c6
+ clayworthVertexRep_data_c7
+ clayworthVertexRep_data_c8
+ clayworthVertexRep_data_size
+ closureGraphAction
+ connectionSet
+ connectionSet_eq_doubleCoset
+ cosetQuotientMap
+ cosetQuotientMap_mk
+ css_k_eq_2g
+ d1
+ d1T_mulVec_entry
+ d1_col_sum_eq_zero
+ d1_eq_start_add_end
+ d1_mul_d2_eq_zero
+ d1_rank_eq
+ d1_rank_le
+ d2
+ d2_entry
+ d2_mulVec_one_of_two_sides
+ d2_rank_eq
+ d2_rank_le
+ 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
+ genOrInv'
+ genOrInv'_mem_closure
+ gen_mem_closure'
+ graphAction
+ graphs_agree_at_zero
+ heawoodBij
+ heawoodSurface
+ heawoodVoltage
+ heawoodVoltage_directedEdges
+ heawoodVoltage_quotient_complete
+ heawoodVoltage_regular
+ heawood_d1_mul_d2_eq_zero
+ heawood_euler
+ heawood_surface_eq_voltage
+ instance : DecidableRel (heawoodVoltage.quotientGraph
+ instance : DecidableRel (mobiusKantorVoltage.quotientGraph
+ instance : DecidableRel heawoodVoltage.Adj := by
+ instance : DecidableRel mobiusKantorVoltage.Adj := by
+ instance : DecidableRel zhou6Graph.Adj
+ instance : DecidableRel zhouGraph.Adj
+ instance : GraphAction kGroup (Fin 56) kleinGraph
+ instance : GraphAction m1344Group (Fin 1344) meinhold1344Graph
+ instance : GraphAction m2016Group (Fin 2016) meinhold2016Graph
+ instance : GraphAction m504Group (Fin 504) meinhold504Graph
+ instance : GraphAction m576Group (Fin 576) meinhold576Graph
+ instance : GraphAction mGroup (Fin 72) meinhold72Graph
+ instance : GraphAction z6Group (Fin 91) zhou6Graph
+ instance : GraphAction zGroup (Fin 182) zhouGraph
+ instance : MulAction kGroup (Fin 56) := MulAction.compHom _ kGroup.subtype
+ instance : MulAction m1344Group (Fin 1344)
+ instance : MulAction m2016Group (Fin 2016)
+ instance : MulAction m504Group (Fin 504)
+ instance : MulAction m576Group (Fin 576)
+ instance : MulAction mGroup (Fin 72)
+ instance : MulAction z6Group (Fin 91) := MulAction.compHom _ z6Group.subtype
+ instance : MulAction zGroup (Fin 182) := MulAction.compHom _ zGroup.subtype
+ instance : MulAction.IsPretransitive kGroup (Fin 56)
+ instance : MulAction.IsPretransitive m1344Group (Fin 1344)
+ instance : MulAction.IsPretransitive m2016Group (Fin 2016)
+ instance : MulAction.IsPretransitive m504Group (Fin 504)
+ instance : MulAction.IsPretransitive m576Group (Fin 576)
+ instance : MulAction.IsPretransitive mGroup (Fin 72)
+ instance : MulAction.IsPretransitive z6Group (Fin 91)
+ instance : MulAction.IsPretransitive zGroup (Fin 182)
+ inv_eq_self_of_sq_eq_one
+ inv_mem
+ isArcTransitive_of_vertexTransitive_locallyTransitive
+ isConnectionSet
+ k
+ kG1
+ kG1F
+ kG1F_s
+ kG1I
+ kG1I_s
+ kG2
+ kG2F
+ kG2F_s
+ kG2I
+ kG2I_s
+ kGens
+ kGroup
+ kWD
+ kWD_s
+ kWit
+ kWit_ok
+ ker_d1T_edge_eq
+ ker_d1T_finrank_eq_one
+ ker_d1T_le_span_one
+ ker_d2_dual_adj_eq
+ kleinAdjBool
+ kleinDecAdj
+ kleinGraph
+ kleinSabidussiIso
+ kleinSurface
+ kleinSurface_euler
+ kleinZ7Data
+ klein_edges
+ klein_regular
+ 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
+ m1344Group
+ m2016Group
+ m504Group
+ m576Group
+ mGroup
+ meinhold1344AdjBool
+ meinhold1344DecAdj
+ meinhold1344Gen1Fwd
+ meinhold1344Gen1Fwd_size
+ meinhold1344Gen1Rev
+ meinhold1344Gen1Rev_size
+ meinhold1344Gen1_adj
+ meinhold1344Gen2Fwd
+ meinhold1344Gen2Fwd_size
+ meinhold1344Gen2Rev
+ meinhold1344Gen2Rev_size
+ meinhold1344Gen2_adj
+ meinhold1344Gens
+ meinhold1344Graph
+ meinhold1344SabidussiIso
+ meinhold1344WitnessWords
+ meinhold1344Witness_correct
+ meinhold1344_connected
+ meinhold1344_has_6cycle
+ meinhold1344_triangleFree
+ meinhold2016AdjBool
+ meinhold2016DecAdj
+ meinhold2016Gen1Fwd
+ meinhold2016Gen1Fwd_size
+ meinhold2016Gen1Rev
+ meinhold2016Gen1Rev_size
+ meinhold2016Gen1_adj
+ meinhold2016Gen2Fwd
+ meinhold2016Gen2Fwd_size
+ meinhold2016Gen2Rev
+ meinhold2016Gen2Rev_size
+ meinhold2016Gen2_adj
+ meinhold2016Gens
+ meinhold2016Graph
+ meinhold2016SabidussiIso
+ meinhold2016WitnessWords
+ meinhold2016Witness_correct
+ meinhold2016_connected
+ meinhold2016_has_8cycle
+ meinhold2016_triangleFree
+ meinhold504AdjBool
+ meinhold504DecAdj
+ meinhold504Gen1Fwd
+ meinhold504Gen1Fwd_size
+ meinhold504Gen1Rev
+ meinhold504Gen1Rev_size
+ meinhold504Gen1_adj
+ meinhold504Gen2Fwd
+ meinhold504Gen2Fwd_size
+ meinhold504Gen2Rev
+ meinhold504Gen2Rev_size
+ meinhold504Gen2_adj
+ meinhold504Gens
+ meinhold504Graph
+ meinhold504SabidussiIso
+ meinhold504WitnessWords
+ meinhold504Witness_correct
+ meinhold504_connected
+ meinhold504_has_4cycle
+ meinhold504_triangleFree
+ meinhold576DecAdj
+ meinhold576Gen1Fwd
+ meinhold576Gen1Fwd_size
+ meinhold576Gen1Rev
+ meinhold576Gen1Rev_size
+ meinhold576Gen1_adj
+ meinhold576Gen2Fwd
+ meinhold576Gen2Fwd_size
+ meinhold576Gen2Rev
+ meinhold576Gen2Rev_size
+ meinhold576Gen2_adj
+ meinhold576Gens
+ meinhold576Graph
+ meinhold576SabidussiIso
+ meinhold576WitnessWords
+ meinhold576Witness_correct
+ meinhold576_connected
+ meinhold576_has_6cycle
+ meinhold576_triangleFree
+ meinhold72AdjBool
+ meinhold72DecAdj
+ meinhold72Gen1Fwd
+ meinhold72Gen1Fwd_size
+ meinhold72Gen1Rev
+ meinhold72Gen1Rev_size
+ meinhold72Gen1_adj
+ meinhold72Gen2Fwd
+ meinhold72Gen2Fwd_size
+ meinhold72Gen2Rev
+ meinhold72Gen2Rev_size
+ meinhold72Gen2_adj
+ meinhold72Gens
+ meinhold72Graph
+ meinhold72NeighborData
+ meinhold72NeighborData_size
+ meinhold72SabidussiIso
+ meinhold72WitnessWords
+ meinhold72Witness_correct
+ meinhold72_connected
+ meinhold72_degree
+ meinhold72_has_4cycle
+ meinhold72_triangleFree
+ meinholdBlockMap
+ meinholdBlockMapData
+ meinholdBlockMapData_size
+ meinholdBlockMap_adj
+ meinholdBlockMap_fiber_card
+ meinholdBlockMap_lifts
+ meinholdBlockMap_surjective
+ mergeRep63
+ mergeRep91
+ mobiusKantorVoltage
+ mobiusKantorVoltage_directedEdges
+ mobiusKantorVoltage_quotient_complete
+ mobiusKantorVoltage_regular
+ nextIdx
+ nextIdx_bijective
+ nextIdx_injective
+ nextPerm
+ one_mem_ker_d1T
+ one_ne_zero_fin
+ q62Indices
+ q62Point
+ q62_card
+ quotient_cosetGraph_iso
+ sabidussiEquiv
+ sabidussiEquiv_smul
+ sabidussiEquiv_symm_mk
+ sabidussiIso
+ sabidussiSymmetricGraph
+ stabilizer_transitive_on_neighbors
+ stepEnd
+ stepEnd_eq_stepStart_next
+ stepStart
+ symm_preserves_dist2
+ symm_preserves_langer
+ toBitVec
+ toCellularSurface
+ toDualSimpleGraph
+ toIso
+ toIso_apply
+ toIso_mul
+ toIso_symm
+ toSimpleGraph
+ transport_dist2
+ transport_langer
+ tutte12AdjBool
+ tutte12CageGraph
+ tutte12DecAdj
+ tutte12Distance2Bool
+ tutte12Edges
+ tutte12Side
+ tutte12_bipartite
+ tutte12_points_independent
+ tutte12_regular
+ vertexOf_T_eq_R
+ voltageGraphK2
+ walk_preserves_ker
+ witnessWord
+ witnessWordData
+ witnessWordData_size
+ witnessWord_correct
+ z6G1
+ z6G1F
+ z6G1F_s
+ z6G1I
+ z6G1I_s
+ z6G2
+ z6G2F
+ z6G2F_s
+ z6G2I
+ z6G2I_s
+ z6Gens
+ z6Group
+ z6WD
+ z6WD_s
+ z6Wit
+ z6Wit_ok
+ zG1
+ zG1F
+ zG1F_s
+ zG1I
+ zG1I_s
+ zG2
+ zG2F
+ zG2F_s
+ zG2I
+ zG2I_s
+ zGens
+ zGroup
+ zWD
+ zWD_s
+ zWit
+ zWit_ok
+ zhou6AdjBool
+ zhou6Gen1
+ zhou6Gen1Fwd
+ zhou6Gen1Fwd_size
+ zhou6Gen1Inv
+ zhou6Gen1Inv_size
+ zhou6Gen1_adj
+ zhou6Gen2
+ zhou6Gen2Fwd
+ zhou6Gen2Fwd_size
+ zhou6Gen2Inv
+ zhou6Gen2Inv_size
+ zhou6Gen2_adj
+ zhou6Graph
+ zhou6Graph_edgeCount
+ zhou6Graph_regular
+ zhou6SabidussiIso
+ zhou6_action_primitive
+ zhou6_eq_quotient
+ zhouAdjBool
+ zhouBlockData
+ zhouBlockData_length
+ zhouBlockMap
+ zhouBlockMap_exhaustive
+ zhouBlockReps
+ zhouBlockReps_correct
+ zhouBlockReps_size
+ zhouEdges
+ zhouGraph
+ zhouGraph_edgeCount
+ zhouGraph_regular
+ zhouQuotientGraph
+ zhouSabidussiIso
++ 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.
Increase in strong tech debt: (relative, absolute) = (2.00, 0.67)
| Current number | Change | Type (strong) |
|---|---|---|
| 3 | 2 | maxHeartBeats modifications |
Increase in weak tech debt: (relative, absolute) = (7.00, 0.00)
| Current number | Change | Type (weak) |
|---|---|---|
| 4997 | 7 | exposed public sections |
Current commit af73577478
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
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
Adds LangerGraph.lean (Langer graph, Tutte 12-cage, G₂(2) generators, structural equality) and PrimitiveGraphs.lean (Atkinson's algorithm proving Langer and Zhou-6 primitive, Tutte 12-cage point subgraph edgeless).
Five coset graphs of G₂(2) via intermediate subgroups C₃ ≤ K ≤ G₂(2), each with Sabidussi isomorphism, connectivity, and girth witnesses. Proves the Langer graph is not a quotient of Clayworth.
e4eb08c to
4c5b233
Compare
These files belong in their own PRs (leanprover-community#39695 for Zhou, leanprover-community#39649/leanprover-community#39698 for Langer and primitivity). This branch should only contain the four CellularSurface instances and supporting infrastructure.
|
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 |
mathlib-merge-conflicts
Bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
…tients # Conflicts: # Mathlib.lean
github-actions
Bot
removed
the
merge-conflict
mathlib-merge-conflicts
Bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
1 participant
Five coset graphs of the exceptional Chevalley group G₂(2), each arising as Sab(G₂(2), K, D) for intermediate subgroups C₃ ≤ K ≤ G₂(2). The Clayworth graph (4032 vertices, cubic, genus 505) is the base case K = C₃.
Meinhold-72 has 72 vertices, is 7-regular with girth 4, via K = PSL(3,2). Meinhold-504 has 504 vertices, is 24-regular with girth 4, via S₄. Meinhold-576 has 576 vertices, is 7-regular with girth 6, via C₇:C₃. Meinhold-1344 has 1344 vertices, is 9-regular with girth 6, via C₃×C₃. Meinhold-2016 has 2016 vertices, is 6-regular with girth 8, via C₆. Each graph has a Sabidussi isomorphism proving arc-transitivity, is connected, and has a shortest cycle witness establishing the girth.
The Langer graph (63 vertices, 6-regular) is proved not to be a quotient of Clayworth: the three G₂(2)-invariant 63-block systems have quotient degrees 24, 32, 32, none of which equals 6.
The Clayworth graph itself is proved to be a Sabidussi coset graph Sab(G₂(2), C₃, D) with two generators of orders 7 and 6 preserving adjacency, and BFS witness words establishing transitivity. The current approach is admittedly brute-force — the Clayworth graph is defined via a flat adjacency array and the quotient maps are verified by native_decide on concrete vertex data. A more algebraic treatment, deriving the Meinhold graphs directly from the coset lattice of G₂(2) without storing explicit adjacency data, would be cleaner and is planned as a follow-up.
These graphs arise from my honours thesis on symmetric graph quotients (arXiv:1306.4798). The Meinhold family is named after Nick Meinhold, co-founder of Imagineering Melbourne.
Depends on #39654 (CellularSurface instances, Clayworth graph).
LLM tools were used to assist with Lean formalization. The mathematical content is the author's own work.