feat(Archive): Zhou-3 arc-transitivity and Lorimer quotient to Zhou-6#39695
feat(Archive): Zhou-3 arc-transitivity and Lorimer quotient to Zhou-6#39695RaggedR wants to merge 38 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.
The Z₂ block system on the Zhou-3 graph (182 → 91 vertices) is invariant
under both generators of PSL(2,13). The block partner of vertex 0 is
vertex 137, and the word g₁·g₂·g₁³·g₂·g₁·g₂ gives an explicit involution
swapping them. This is the first step toward expressing the Zhou-3 → Zhou-6
quotient via Lorimer's quotient theorem: the setwise stabilizer of {0, 137}
is D₁₂ ≥ S₃ = Stab(0), and the coset projection G/S₃ → G/D₁₂ recovers
the block map algebraically.
The set {0, 137} forms a block of the PSL(2,13) action on the Zhou-3
graph. The block swapper preserves this block setwise, and no element
of the block is adjacent to vertex 0 — the key fact needed to show
the connection set D is disjoint from the setwise stabilizer K = D₁₂.
Every element of PSL(2,13) preserves the Zhou-3 block map, proved by induction on the group closure. The generator cases are native_decide, the multiplication case composes, and the inverse case uses the same pigeonhole argument as closureGraphAction: σ acts injectively on the set of same-block pairs, so by finiteness it acts surjectively, which gives a preimage witness for any target pair.
The setwise stabilizer of {0, 137} is defined as a subgroup of zGroup
whose elements map both 0 and 137 into {0, 137}. The point stabilizer
of 0 is contained in K because closureBlockInvariant forces any element
fixing 0 to also preserve the partner 137. The connection set is disjoint
from K because any element of K maps 0 into {0, 137}, but neither 0 nor
137 is adjacent to 0 in the Zhou-3 graph. These are the two hypotheses
needed for Lorimer's quotient theorem.
First concrete instantiation of quotient_cosetGraph_iso in the library. The quotient of the Zhou-3 coset graph Sab(PSL(2,13), S₃, D) by the overgroup K ≅ D₁₂ is isomorphic to Sab(PSL(2,13), D₁₂, D₁₂·D·D₁₂), which is a 6-regular graph on 91 vertices. All hypotheses verified: H ≤ K via closureBlockInvariant, D ∩ K = ∅ via the neighbor argument.
The connection set of the Zhou-3 Sabidussi graph is a single double coset HaH where a is an involution sending vertex 0 to its neighbor 3. The involution is the word g₁⁻¹g₂g₁⁻²g₂g₁²g₂g₁ in the PSL(2,13) generators. Lorimer's forward theorem then gives arc-transitivity of the associated coset graph Sab(PSL(2,13), S₃, S₃·a·S₃).
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 d880245946
|
| 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
+ ClayworthSurface_edge_src_data
+ ClayworthSurface_edge_src_data_chunk0
+ ClayworthSurface_edge_src_data_chunk1
+ ClayworthSurface_edge_src_data_chunk10
+ ClayworthSurface_edge_src_data_chunk11
+ ClayworthSurface_edge_src_data_chunk12
+ ClayworthSurface_edge_src_data_chunk2
+ ClayworthSurface_edge_src_data_chunk3
+ ClayworthSurface_edge_src_data_chunk4
+ ClayworthSurface_edge_src_data_chunk5
+ ClayworthSurface_edge_src_data_chunk6
+ ClayworthSurface_edge_src_data_chunk7
+ ClayworthSurface_edge_src_data_chunk8
+ ClayworthSurface_edge_src_data_chunk9
+ ClayworthSurface_edge_src_size
+ ClayworthSurface_edge_tgt_data
+ ClayworthSurface_edge_tgt_data_chunk0
+ ClayworthSurface_edge_tgt_data_chunk1
+ ClayworthSurface_edge_tgt_data_chunk10
+ ClayworthSurface_edge_tgt_data_chunk11
+ ClayworthSurface_edge_tgt_data_chunk12
+ ClayworthSurface_edge_tgt_data_chunk2
+ ClayworthSurface_edge_tgt_data_chunk3
+ ClayworthSurface_edge_tgt_data_chunk4
+ ClayworthSurface_edge_tgt_data_chunk5
+ ClayworthSurface_edge_tgt_data_chunk6
+ ClayworthSurface_edge_tgt_data_chunk7
+ ClayworthSurface_edge_tgt_data_chunk8
+ ClayworthSurface_edge_tgt_data_chunk9
+ ClayworthSurface_edge_tgt_size
+ ClayworthSurface_face_dir_data
+ ClayworthSurface_face_dir_data_chunk0
+ ClayworthSurface_face_dir_data_chunk1
+ ClayworthSurface_face_dir_data_chunk10
+ ClayworthSurface_face_dir_data_chunk11
+ ClayworthSurface_face_dir_data_chunk12
+ ClayworthSurface_face_dir_data_chunk13
+ ClayworthSurface_face_dir_data_chunk14
+ ClayworthSurface_face_dir_data_chunk15
+ ClayworthSurface_face_dir_data_chunk16
+ ClayworthSurface_face_dir_data_chunk17
+ ClayworthSurface_face_dir_data_chunk18
+ ClayworthSurface_face_dir_data_chunk19
+ ClayworthSurface_face_dir_data_chunk2
+ ClayworthSurface_face_dir_data_chunk20
+ ClayworthSurface_face_dir_data_chunk21
+ ClayworthSurface_face_dir_data_chunk22
+ ClayworthSurface_face_dir_data_chunk23
+ ClayworthSurface_face_dir_data_chunk24
+ ClayworthSurface_face_dir_data_chunk3
+ ClayworthSurface_face_dir_data_chunk4
+ ClayworthSurface_face_dir_data_chunk5
+ ClayworthSurface_face_dir_data_chunk6
+ ClayworthSurface_face_dir_data_chunk7
+ ClayworthSurface_face_dir_data_chunk8
+ ClayworthSurface_face_dir_data_chunk9
+ ClayworthSurface_face_dir_size
+ ClayworthSurface_face_edge_data
+ ClayworthSurface_face_edge_data_chunk0
+ ClayworthSurface_face_edge_data_chunk1
+ ClayworthSurface_face_edge_data_chunk10
+ ClayworthSurface_face_edge_data_chunk11
+ ClayworthSurface_face_edge_data_chunk12
+ ClayworthSurface_face_edge_data_chunk13
+ ClayworthSurface_face_edge_data_chunk14
+ ClayworthSurface_face_edge_data_chunk15
+ ClayworthSurface_face_edge_data_chunk16
+ ClayworthSurface_face_edge_data_chunk17
+ ClayworthSurface_face_edge_data_chunk18
+ ClayworthSurface_face_edge_data_chunk19
+ ClayworthSurface_face_edge_data_chunk2
+ ClayworthSurface_face_edge_data_chunk20
+ ClayworthSurface_face_edge_data_chunk21
+ ClayworthSurface_face_edge_data_chunk22
+ ClayworthSurface_face_edge_data_chunk23
+ ClayworthSurface_face_edge_data_chunk24
+ ClayworthSurface_face_edge_data_chunk3
+ ClayworthSurface_face_edge_data_chunk4
+ ClayworthSurface_face_edge_data_chunk5
+ ClayworthSurface_face_edge_data_chunk6
+ ClayworthSurface_face_edge_data_chunk7
+ ClayworthSurface_face_edge_data_chunk8
+ ClayworthSurface_face_edge_data_chunk9
+ ClayworthSurface_face_edge_size
+ 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
+ SimpleGraph.cosetGraph
+ SimpleGraph.quotientGraph
+ SurfaceTiling
+ adj_mk
+ adj_smul_iff
+ applyWord'
+ applyWord'_mem
+ arcSwapper
+ arcSwapper_image
+ arcSwapper_mem
+ arcSwapper_mul_self
+ arcSwapper_not_in_stab
+ arcSwapper_sq
+ arcSwapper_sq_eq_one
+ arrayToFin
+ arrayToFin₂
+ blockMap_eq_on_block
+ blockMap_invariant_g1
+ blockMap_invariant_g2
+ blockMap_invariant_inv
+ blockSwapper
+ blockSwapper_mem
+ blockSwapper_preserves_block
+ blockSwapper_sq
+ blockSwapper_zero
+ block_disjoint_neighbors
+ block_partner
+ bolzaBij
+ bolzaBijData
+ bolzaBijData_size
+ bolzaSurface
+ bolza_d1_mul_d2_eq_zero
+ bolza_euler
+ bolza_surface_eq_voltage
+ cGroup
+ clayworthAdjBool
+ clayworthDecAdj
+ clayworthGen1
+ clayworthGen1Fwd
+ clayworthGen1Fwd_chunk0
+ clayworthGen1Fwd_chunk1
+ clayworthGen1Fwd_chunk10
+ clayworthGen1Fwd_chunk2
+ clayworthGen1Fwd_chunk3
+ clayworthGen1Fwd_chunk4
+ clayworthGen1Fwd_chunk5
+ clayworthGen1Fwd_chunk6
+ clayworthGen1Fwd_chunk7
+ clayworthGen1Fwd_chunk8
+ clayworthGen1Fwd_chunk9
+ clayworthGen1Fwd_size
+ clayworthGen1Inv
+ clayworthGen1Inv_chunk0
+ clayworthGen1Inv_chunk1
+ clayworthGen1Inv_chunk10
+ clayworthGen1Inv_chunk2
+ clayworthGen1Inv_chunk3
+ clayworthGen1Inv_chunk4
+ clayworthGen1Inv_chunk5
+ clayworthGen1Inv_chunk6
+ clayworthGen1Inv_chunk7
+ clayworthGen1Inv_chunk8
+ clayworthGen1Inv_chunk9
+ clayworthGen1Inv_size
+ clayworthGen1_adj
+ clayworthGen1_adj_edges
+ clayworthGen1_inv_adj
+ clayworthGen1_inv_adj_edges
+ clayworthGen2
+ clayworthGen2Fwd
+ clayworthGen2Fwd_chunk0
+ clayworthGen2Fwd_chunk1
+ clayworthGen2Fwd_chunk10
+ clayworthGen2Fwd_chunk2
+ clayworthGen2Fwd_chunk3
+ clayworthGen2Fwd_chunk4
+ clayworthGen2Fwd_chunk5
+ clayworthGen2Fwd_chunk6
+ clayworthGen2Fwd_chunk7
+ clayworthGen2Fwd_chunk8
+ clayworthGen2Fwd_chunk9
+ clayworthGen2Fwd_size
+ clayworthGen2Inv
+ clayworthGen2Inv_chunk0
+ clayworthGen2Inv_chunk1
+ clayworthGen2Inv_chunk10
+ clayworthGen2Inv_chunk2
+ clayworthGen2Inv_chunk3
+ clayworthGen2Inv_chunk4
+ clayworthGen2Inv_chunk5
+ clayworthGen2Inv_chunk6
+ clayworthGen2Inv_chunk7
+ clayworthGen2Inv_chunk8
+ clayworthGen2Inv_chunk9
+ clayworthGen2Inv_size
+ clayworthGen2_adj
+ clayworthGen2_adj_edges
+ clayworthGen2_inv_adj
+ clayworthGen2_inv_adj_edges
+ clayworthGens
+ 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
+ clayworthSabidussiIso
+ clayworthSurface
+ clayworthSurface_euler
+ clayworthWitnessData
+ clayworthWitnessData_chunk0
+ clayworthWitnessData_chunk1
+ clayworthWitnessData_chunk10
+ clayworthWitnessData_chunk2
+ clayworthWitnessData_chunk3
+ clayworthWitnessData_chunk4
+ clayworthWitnessData_chunk5
+ clayworthWitnessData_chunk6
+ clayworthWitnessData_chunk7
+ clayworthWitnessData_chunk8
+ clayworthWitnessData_chunk9
+ clayworthWitnessData_size
+ clayworthWitnessWords
+ clayworthWitness_correct
+ closureBlockInvariant
+ closureGraphAction
+ connectionSet
+ connectionSet_disjoint_zhouOvergroup
+ 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
+ genOrInv'
+ genOrInv'_mem_closure
+ gen_mem_closure'
+ graphAction
+ 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 cGroup (Fin 4032) clayworthGraph
+ instance : GraphAction kGroup (Fin 56) kleinGraph
+ instance : GraphAction z6Group (Fin 91) zhou6Graph
+ instance : GraphAction zGroup (Fin 182) zhouGraph
+ instance : MulAction cGroup (Fin 4032)
+ instance : MulAction kGroup (Fin 56) := MulAction.compHom _ kGroup.subtype
+ instance : MulAction z6Group (Fin 91) := MulAction.compHom _ z6Group.subtype
+ instance : MulAction zGroup (Fin 182) := MulAction.compHom _ zGroup.subtype
+ instance : MulAction.IsPretransitive cGroup (Fin 4032)
+ instance : MulAction.IsPretransitive kGroup (Fin 56)
+ 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
+ locallyTransitive_at_one
+ locallyTransitive_everywhere
+ lorimer_forward
+ lorimer_reverse
+ mobiusKantorVoltage
+ mobiusKantorVoltage_directedEdges
+ mobiusKantorVoltage_quotient_complete
+ mobiusKantorVoltage_regular
+ nextIdx
+ nextIdx_bijective
+ nextIdx_injective
+ nextPerm
+ not_adj_zero_partner
+ not_adj_zero_self
+ one_mem_ker_d1T
+ one_ne_zero_fin
+ quotient_cosetGraph_iso
+ sabidussiEquiv
+ sabidussiEquiv_smul
+ sabidussiEquiv_symm_mk
+ sabidussiIso
+ sabidussiSymmetricGraph
+ stabilizer_le_zhouOvergroup
+ stabilizer_transitive_on_neighbors
+ stepEnd
+ stepEnd_eq_stepStart_next
+ stepStart
+ toDualSimpleGraph
+ toIso
+ toIso_apply
+ toIso_mul
+ toIso_symm
+ toSimpleGraph
+ voltageGraphK2
+ walk_preserves_ker
+ 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
+ zhou6Graph
+ zhou6Graph_edgeCount
+ zhou6Graph_regular
+ zhou6SabidussiIso
+ zhou6_eq_quotient
+ zhouAdjBool
+ zhouArcTransitive
+ zhouBlock
+ zhouBlockData
+ zhouBlockData_length
+ zhouBlockMap
+ zhouBlockMap_exhaustive
+ zhouBlockReps
+ zhouBlockReps_correct
+ zhouBlockReps_size
+ zhouEdges
+ zhouGraph
+ zhouGraph_edgeCount
+ zhouGraph_regular
+ zhouLorimerQuotientIso
+ zhouOvergroup
+ 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 d880245946
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).
d89291d to
8da900b
Compare
b-mehta
added
the
LLM-generated
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 |
# 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 |
2 participants
The Zhou-3 graph (Foster census F182A, 182 vertices, cubic) has an imprimitive block system of 91 blocks of size 2. This PR proves the block system is invariant under the full PSL(2,13) action via closure induction on the generators, with a pigeonhole argument for the inverse case. The setwise stabilizer of the block containing vertex 0 is D₁₂ (dihedral of order 12), which contains the point stabilizer S₃ at index 2.
With the block structure established, Lorimer's quotient theorem (from #39551) is instantiated for the first time on a concrete graph: the quotient of Sab(PSL(2,13), S₃, D) by D₁₂ is isomorphic to Sab(PSL(2,13), D₁₂, D₁₂·D·D₁₂). The two hypotheses — H ≤ K and D ∩ K = ∅ — are verified, the first using the closure block invariance theorem and the second by observing that any element of K maps vertex 0 into {0, 137}, but neither is a neighbor of 0.
Arc-transitivity of Zhou-3 is proved via Lorimer's forward theorem: the connection set is a single double coset S₃·a·S₃ where a is an explicit involution (a word of length 9 in the generators) that swaps vertex 0 with its neighbor 3.
This depends on the Sabidussi/Lorimer chain (#39530, #39548, #39550, #39551) and on #39654 for the Zhou-3 Sabidussi representation and SabidussiWitness infrastructure.