feat(Archive): CellularSurface instances (genus 1, 2, 3, 505)#39654
feat(Archive): CellularSurface instances (genus 1, 2, 3, 505)#39654RaggedR 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.
|
Could a maintainer please add the |
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 5562da99cc
|
| 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
+ SimpleGraph.cosetGraph
+ SimpleGraph.quotientGraph
+ SurfaceTiling
+ T
+ TriangleGroupData
+ adj_mk
+ adj_smul_iff
+ applyWord'
+ applyWord'_mem
+ arrayToFin
+ arrayToFin'
+ bolzaBij
+ bolzaBijData
+ bolzaBijData_size
+ bolzaSurface
+ bolzaSurface_dual_regular
+ bolza_d1_mul_d2_eq_zero
+ bolza_euler
+ bolza_surface_eq_voltage
+ 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
+ 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
+ clayworthSurface_dual_regular
+ 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
+ genOrInv'
+ genOrInv'_mem_closure
+ gen_mem_closure'
+ graphAction
+ heawoodBij
+ heawoodSurface
+ heawoodSurface_dual_regular
+ 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 : GraphAction kGroup (Fin 56) kleinGraph
+ instance : MulAction kGroup (Fin 56) := MulAction.compHom _ kGroup.subtype
+ instance : MulAction.IsPretransitive kGroup (Fin 56)
+ 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_dual_regular
+ 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
+ one_mem_ker_d1T
+ one_ne_zero_fin
+ quotient_cosetGraph_iso
+ sabidussiEquiv
+ sabidussiEquiv_smul
+ sabidussiEquiv_symm_mk
+ sabidussiIso
+ sabidussiSymmetricGraph
+ stabilizer_transitive_on_neighbors
+ stepEnd
+ stepEnd_eq_stepStart_next
+ stepStart
+ toCellularSurface
+ toDualSimpleGraph
+ toIso
+ toIso_apply
+ toIso_mul
+ toIso_symm
+ toSimpleGraph
+ vertexOf_T_eq_R
+ voltageGraphK2
+ walk_preserves_ker
++ 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 5562da99cc
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).
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
|
LLM-generated |
github-actions
Bot
added
the
LLM-generated
- 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)
themathqueen
added
the
blocked-by-other-PR
mathlib-dependent-issues
Bot
removed
the
blocked-by-other-PR
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.
The 4032-vertex IsPretransitive and sabidussiIso need increased maxRecDepth (deep unfolding of Subgroup.closure) and maxHeartbeats (elaboration of group membership proofs with large data).
Klein graph quotient classification (verified by GAP)The Klein graph
No interesting quotients exist. Every connected quotient is complete or near-complete. The only cubic quotient (28v) is disconnected. This contrasts with Zhou-3, where the D₁₂ block system gives the connected primitive Zhou-6 graph. The subgroup lattice between C₃ and PSL(2,7) has intermediate subgroups S₃ (index 28), A₄ (index 14), Z₇⋊C₃ (index 8), S₄ (index 7) — but none produce a non-degenerate connected quotient graph. Computed by |
|
Correction to the table above — the earlier run picked a different suborbit. Recomputed with the correct cubic orbital:
Every connected quotient is complete or near-complete. No non-degenerate quotient exists. The claim in the PR description is correct. |
|
Correction: The PR description says "The Langer graph Sab(G₂(2), H₁₉₂) remains the only primitive graph in the programme." This is wrong — Zhou-6 Sab(PSL(2,13), D₁₂) is also primitive (D₁₂ is maximal in PSL(2,13)). Two primitive graphs, not one. |
… 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.
9e385ff to
3242183
Compare
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.
24cfe3c to
a781943
Compare
|
Please add the |
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).
States (with sorry) that the dual graph of each CellularSurface is regular: Heawood dual 6-regular, Bolza dual 8-regular, Klein dual 7-regular, Clayworth dual 12-regular.
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 |
|
This pull request has conflicts, please merge |
mathlib-merge-conflicts
Bot
added
the
merge-conflict
github-actions
Bot
removed
the
merge-conflict
GitHub Actions
Inactive
mathlib-merge-conflicts
Bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
…ances # 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
This PR provides concrete CellularSurface instances for the four CSS surface codes: Heawood (genus 1), Bolza (genus 2), Klein quartic (genus 3), and Clayworth (genus 505). Each surface embeds a cubic arc-transitive graph arising from a Sabidussi coset construction, and the chain complex d1, d2 satisfies the boundary condition d1 · d2 = 0 that gives the CSS orthogonality. Together with #39653, which proves that k = 2g for any surface tiling, these instances yield formally verified CSS codes with parameters [[21, 2]], [[24, 4]], [[84, 6]], and [[6048, 1010]] respectively.
The Heawood and Bolza surfaces are small enough that all axioms are verified by decide. Both include bridge theorems proving the CellularSurface graph matches the corresponding voltage graph on K₂ from VoltageGraphs.lean. The Klein quartic embeds the Klein graph (56 vertices) from the triangle group Δ(2,3,7) acting on PSL(2,7), with a Sabidussi proof. The Clayworth surface is the interesting case: 4032 vertices, 6048 edges, 1008 dodecagonal faces, genus 505. Rather than storing tens of thousands of array entries, the construction works algebraically from the regular representation of G₂(2) on 12096 darts, using a general TriangleGroupSurface module that derives a CellularSurface from any finite quotient of Δ(2,3,r). The key identity is that T = RS implies the far endpoint of each dart has the same vertex as its R-successor, because S preserves vertex cosets.
There are five sorrys. Four are dual graph regularity theorems (Heawood 6-regular, Bolza 8-regular, Klein 7-regular, Clayworth 12-regular), all of which should be closable by native_decide. The fifth is the Clayworth Sabidussi isomorphism, where the individual native_decide checks all pass but the kernel struggles to assemble the SabidussiWitness structure for 4032 vertices. These are left for a follow-up.
Depends on #39653 (CellularSurface, k = 2g). Cross-references #39649 (Langer/G₂(2) ecosystem), #39651 (voltage graphs).