QEC development and surface code distance constancy

[wdcraft01]

trafficstars

In addition to other on-going development of quantum-related topics in Prove-It, it's time to begin developing aspects of quantum error correction (QEC) and, in particular, infrastructure (definitions, axioms, theorems) for the formal verification of surface code distance constancy under logical Hadamard operations. A preliminary manual proof of distance conservation for a Kitaev-style planar surface code undergoing a logical Hadamard operation can be found in the pdf linked here:

Distance_Conservation_20250227.pdf

That document offers a basis for initial definitions, axioms, and theorems in the formal verification of distance conservation.