feat(Combinatorics): cellular surfaces, CSS quantum codes, and k = 2g#39653
feat(Combinatorics): cellular surfaces, CSS quantum codes, and k = 2g#39653RaggedR wants to merge 12 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).
|
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 7bf43ce822
|
| 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.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
+ SimpleGraph.cosetGraph
+ SimpleGraph.quotientGraph
+ SurfaceTiling
+ adj_mk
+ adj_smul_iff
+ 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
+ graphAction
+ inv_eq_self_of_sq_eq_one
+ inv_mem
+ isArcTransitive_of_vertexTransitive_locallyTransitive
+ isConnectionSet
+ k
+ ker_d1T_edge_eq
+ ker_d1T_finrank_eq_one
+ ker_d1T_le_span_one
+ ker_d2_dual_adj_eq
+ locallyTransitive_at_one
+ locallyTransitive_everywhere
+ lorimer_forward
+ lorimer_reverse
+ 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
+ toDualSimpleGraph
+ toIso
+ toIso_apply
+ toIso_mul
+ toIso_symm
+ toSimpleGraph
+ 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.
No changes to strong technical debt.
Increase in weak tech debt: (relative, absolute) = (6.00, 0.00)
| Current number | Change | Type (weak) |
|---|---|---|
| 4996 | 6 | exposed public sections |
Current commit 7bf43ce822
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).
|
Could a maintainer please add the |
- 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
|
LLM-generated |
github-actions
Bot
added
the
LLM-generated
themathqueen
added
the
blocked-by-other-PR
mathlib-dependent-issues
Bot
removed
the
blocked-by-other-PR
e43dc4a to
b794a3a
Compare
|
Please add the |
|
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 |
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 |
…codes # 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 formalises CSS quantum error-correcting codes from surface tilings, following Breuckmann & Terhal (arXiv:1506.04029).
CellularSurface encodes the combinatorial data of a 2-cell embedding of a graph on a closed surface: vertices, edges with endpoints, and faces whose boundaries are closed directed trails. The boundary operators ∂₁ (vertex-edge incidence) and ∂₂ (edge-face boundary) are matrices over F₂.
The theorem
d1_mul_d2_eq_zeroproves ∂₁ ∘ ∂₂ = 0 (the chain complex condition) from the closed walk axiom: each vertex in a face boundary is visited an even number of times, so the sum vanishes in characteristic 2. The theoremd1_rank_eqproves rank(∂₁) = V − 1 for connected graphs — the kernel of ∂₁ᵀ is span{1} because elements of the kernel assign equal values to adjacent vertices, and connectivity propagates this to all vertices. The theoremd2_rank_eqproves rank(∂₂) = F − 1 for connected dual graphs with the two-sides condition (each edge borders exactly 2 faces).The main result
css_k_eq_2ggives the number of logical qubits k = 2g. This is pure arithmetic: k = E − rank(∂₁) − rank(∂₂) = E − (V−1) − (F−1) = E − V − F + 2 = 2g by Euler's formula.No
native_decide— all proofs are structural.LLM tools were used to assist with Lean formalization. The mathematical content is the author's own work.