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 10 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 b794a3ad67
|
| Files | Import difference |
|---|---|
Mathlib.Combinatorics.SimpleGraph.Action (new file) |
648 |
Mathlib.Combinatorics.SimpleGraph.CosetGraph (new file) |
842 |
Mathlib.Combinatorics.SimpleGraph.Representation (new file) |
843 |
Mathlib.Combinatorics.SimpleGraph.Symmetric (new file) |
844 |
Mathlib.Combinatorics.SimpleGraph.QuotientGraph (new file) |
967 |
Mathlib.Combinatorics.CellularSurface (new file) |
1646 |
Declarations diff
+ 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.
No changes to strong technical debt.
No changes to weak technical debt.
|
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
RaggedR
force-pushed
the
feat/css-surface-codes
branch
from
e43dc4a to
b794a3a
Compare
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₂.
Main results:
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.d1_rank_eqproves rank(∂₁) = V − 1 for connected graphs. The kernel of ∂₁ᵀ isspan{1}because elements of the kernel assign equal values to adjacent vertices; connectivity propagates this to all vertices.d2_rank_eqproves rank(∂₂) = F − 1 for connected dual graphs with the two-sides condition (each edge borders exactly 2 faces).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.