# Techniques: String Diagrams for Defect-Based Surface Code Computing

## What the paper contributes (one paragraph)
The paper formalises defect braiding in surface codes as a string-diagram calculus called KNOT. Where braiding has historically been described by informal, partly 3D pictures validated by ad hoc rewrite rules or correlation-surface checks, the authors gather the standard braiding rules into a category with explicit equivalences and stated assumptions. They give KNOT a semantics in the (0, pi)-fragment of the ZX-calculus and prove this interpretation sound. A doubling construction recovers the conventional defect-pair encoding and yields two interoperable sublanguages, tangle-like and ribbon-like, each proven sound and complete for the (0, pi)-fragment of ZX. The paper also shows KNOT is sound for the affine Lagrangian relations describing how logical operators evolve, so a braiding pattern is characterised up to classical byproducts. Together this gives a formal substrate for automated verification and optimisation of defect-based fault-tolerant protocols.

## Techniques offered
- **KNOT string-diagram calculus for defect braiding (diagrammatic compilation and verification)** - a formal graphical language and equational rewrite system for the logical effects of defect braiding in surface codes, supplying a compositional substrate for automated verification and optimisation of braiding protocols.
  - guarantee: static proof; KNOT rewrites are sound (functorial) for the (0, pi)-fragment of ZX-calculus, giving a standardised compositional semantics for equational reasoning.
  - quote: "This paper introduces a graphical language $\catname{KNOT}$, to formalize defect-based surface code computation."
- **Soundness and completeness of doubled KNOT for the (0, pi)-fragment of ZX-calculus** - a doubling construction with tangle-like and ribbon-like sublanguages that faithfully and exactly capture (0, pi) ZX diagrams, supplying interoperable, equivalence-checkable representations of standard braiding techniques.
  - guarantee: static proof of soundness and completeness; the doubled calculus represents exactly the (0, pi)-fragment of ZX-calculus with a unique normal form.
  - quote: "$\catname{KNOT}_{\text{doubled}}$ via the interpretation $K \circ Z$ is sound and complete for the ($0$, $\pi$)-fragment of ZX-calculus."
- **Soundness of KNOT for affine Lagrangian relations (logical-operator evolution)** - an interpretation of braiding diagrams as affine Lagrangian relations over F2, supplying a characterisation of the logical map implemented by a braiding procedure up to classical byproducts.
  - guarantee: static proof; KNOT is sound for the transformations of surface-code first homology and for the logical maps of the braided procedure up to classical byproducts.
  - quote: "$\catname{KNOT}$ is sound for the logical maps implemented by the braided surface code error correction procedure up to classical byproducts."

## Where it could apply
- Target primitive(s): logical two-qubit gates (CNOT) and Clifford-level braiding subroutines; circuit-level compilation and equivalence checking, not VQE/QAOA/QPE/sampling directly.
- Target application group(s): error_correction, platforms_tooling.
- Code family / hardware assumptions: surface code, specifically defect-based (single and double defect) braiding; results stated up to byproducts and for the (0, pi) Clifford fragment of ZX.

## Caveats
The calculus targets defect braiding under specific boundary conditions (effectively an infinite lattice) and the (0, pi) Clifford fragment, omitting non-Clifford gates and magic states. Results hold only up to probabilistic byproduct operations, which the framework does not yet track; byproduct handling, general topologies, and a full correlation-surface calculus are stated as future work. The soundness claim is for the logical effect of some physical procedures realising a braiding pattern, not a full account of all braiding patterns or hardware-level error behaviour. No decoder, threshold, or resource-estimation result is supplied.