feat(Archive): dual Langer graph and GH(2,2) non-self-duality#39718
feat(Archive): dual Langer graph and GH(2,2) non-self-duality#39718RaggedR wants to merge 37 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.
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.
Introduce the dual Langer graph (line-collinearity of the split Cayley hexagon GH(2,2)) and prove that the G₂(2) line-action preserves the share-vertex relation algebraically via Finset.image_inter and Finset.image_nonempty. The line-action is derived from the point-action (LangerGraph.lean) through the triangle-line bijection, verified equivariant at each generator (63-case native_decide). The bridge connecting dual Langer adjacency to the share-vertex relation and the full non-isomorphism proof are left as sorry, pending computational verification.
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 0f7d41a830
|
| 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
+ applyLineGen
+ applyLineGen_share_inv
+ applyLineWord
+ applyLineWord_dualLanger_inv
+ applyLineWord_share_inv
+ 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
+ decLinesShareVertex
+ disjoint_stabilizer
+ doubleCoset_isConnectionSet
+ double_coset_stable
+ dualLangerAdjBool
+ dualLangerDecAdj
+ dualLangerSimpleGraph
+ dualLanger_iff_share
+ 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
+ g2lineGen1
+ g2lineGen1Fwd
+ g2lineGen1Fwd_size
+ g2lineGen1Inv
+ g2lineGen1Inv_size
+ g2lineGen1_share_inv
+ g2lineGen2
+ g2lineGen2Fwd
+ g2lineGen2Fwd_size
+ g2lineGen2Inv
+ g2lineGen2Inv_size
+ g2lineGen2_share_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
+ langerTriangles
+ langer_action_primitive
+ langer_edges
+ langer_eq_tutte12_distance2'
+ langer_not_iso_dualLanger
+ langer_regular
+ langer_triangles_count
+ linePointSet
+ linePointSet_gen1_equivariant
+ linePointSet_gen2_equivariant
+ lineToTriangle
+ lineToTriangle_injective
+ lineToTriangle_mem
+ lineToTriangle_surjective
+ lineTriangleData
+ lineTriangleData_size
+ linesShareVertex
+ 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
+ share_vertex_equivariant
+ stabilizer_transitive_on_neighbors
+ stepEnd
+ stepEnd_eq_stepStart_next
+ stepStart
+ symm_preserves_dist2
+ symm_preserves_langer
+ symm_preserves_share
+ 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) = (3.00, 0.75)
| Current number | Change | Type (strong) |
|---|---|---|
| 4 | 3 | 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 0f7d41a830
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).
|
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 |
|
This pull request has conflicts, please merge |
mathlib-merge-conflicts
Bot
added
the
merge-conflict
…noniso # 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
This PR introduces the dual Langer graph, the line-collinearity graph of the split Cayley hexagon GH(2,2), and establishes the algebraic infrastructure for proving that it is not isomorphic to the Langer graph (the point-collinearity graph). Both graphs share the intersection array {6, 4, 4; 1, 1, 3} but are distinguished by the connectivity of their distance-3 subgraphs.
The key mathematical contribution is deriving the G₂(2) line-action from the point-action (already in Archive.LangerGraph) via the triangle-line bijection. Each line of GH(2,2) corresponds to a unique triangle in the Langer graph, and the point-action sends triangles to triangles, inducing an action on lines. The induced line-action preserves the share-a-vertex relation, which is proved algebraically using Finset.image_inter (injective maps commute with intersection) and Finset.image_nonempty (images preserve non-emptiness). The equivariance of each generator is a 63-case native_decide verification, after which the word-level preservation follows by structural induction with no further computation.
Two sorries remain. The bridge theorem connecting dual Langer adjacency to the share-vertex relation is a native_decide that needs tuning for the kernel recursion limit. The non-isomorphism theorem, which uses d₃-subgraph connectivity as a distinguishing invariant transported to all vertices via the line-action, depends on this bridge. These will be closed in a follow-up once the computational proofs are optimized.
This PR depends on Archive.LangerGraph.