File size: 5,156 Bytes
eef9104 5736180 eef9104 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 | /-
Copyright (c) 2026 Ahmad Ali Parr and others.
This program and the accompanying materials are made available under the
terms of the CPSC Eclipse Strict Copyleft License, Version 1.0, or, at your
option, the GNU Affero General Public License, Version 3 only. Both options
are strict copyleft. There is no classpath exception and no permissive
relicensing.
SPDX-License-Identifier: LicenseRef-CPSC-ESCL-1.0 OR AGPL-3.0-only
-/
/-!
Boolean certificate layer.
These lemmas are proved. They do not mention operators. The operator model
lives in `CPSC.Operator`, and the bridge lemmas in `CPSC.Lemmas`.
-/
namespace CPSC
inductive GateKind where
| zz : Nat β Nat β GateKind
| parityEvenPair : Nat β Nat β GateKind
| transverseFlip : Nat β GateKind
| loneZ : Nat β GateKind
deriving DecidableEq, Repr
inductive Mode where
| ising
| spinFlip
deriving DecidableEq, Repr
/-- Ξ» = 0. A single transverse flip changes magnetization. -/
def preservesMagnetization : GateKind β Bool
| .zz _ _ => true
| .parityEvenPair _ _ => false
| .transverseFlip _ => false
| .loneZ _ => true
/-- Ξ» β 0. The TFIM symmetry is β X, which a lone Z anticommutes with. -/
def preservesSpinFlip : GateKind β Bool
| .zz _ _ => true
| .parityEvenPair _ _ => true
| .transverseFlip _ => true
| .loneZ _ => false
def preserves : Mode β GateKind β Bool
| .ising, g => preservesMagnetization g
| .spinFlip, g => preservesSpinFlip g
def allPreserve (p : GateKind β Bool) : List GateKind β Bool
| [] => true
| g :: rest => p g && allPreserve p rest
def admitted (mode : Mode) (gs : List GateKind) : Bool :=
allPreserve (preserves mode) gs
theorem nil_preserves (p : GateKind β Bool) : allPreserve p [] = true := rfl
theorem bool_and_parts {a b : Bool} (h : (a && b) = true) : a = true β§ b = true := by
cases a <;> cases b <;> simp_all
theorem cons_preserves
(p : GateKind β Bool) (g : GateKind) (rest : List GateKind)
(hg : p g = true) (hr : allPreserve p rest = true) :
allPreserve p (g :: rest) = true := by
simp [allPreserve, hg, hr]
theorem allPreserve_cons_iff
(p : GateKind β Bool) (g : GateKind) (rest : List GateKind) :
allPreserve p (g :: rest) = true β p g = true β§ allPreserve p rest = true := by
constructor
Β· intro h
exact bool_and_parts h
Β· intro h
exact cons_preserves p g rest h.1 h.2
theorem allPreserve_append
(p : GateKind β Bool) (xs ys : List GateKind) :
allPreserve p (xs ++ ys) = (allPreserve p xs && allPreserve p ys) := by
induction xs with
| nil => simp [allPreserve]
| cons g rest ih =>
simp [allPreserve, List.cons_append, ih, Bool.and_assoc]
theorem allPreserve_of_append
(p : GateKind β Bool) {xs ys : List GateKind}
(h : allPreserve p (xs ++ ys) = true) :
allPreserve p xs = true β§ allPreserve p ys = true :=
bool_and_parts (by simpa [allPreserve_append] using h)
theorem transverse_breaks_ising (i : Nat) :
preservesMagnetization (.transverseFlip i) = false := rfl
theorem pair_breaks_ising (i j : Nat) :
preservesMagnetization (.parityEvenPair i j) = false := rfl
theorem loneZ_breaks_spin_flip (i : Nat) :
preservesSpinFlip (.loneZ i) = false := rfl
theorem zz_preserves_both (i j : Nat) :
preservesMagnetization (.zz i j) = true β§ preservesSpinFlip (.zz i j) = true := by
constructor <;> rfl
theorem flip_preserves_spin (i : Nat) :
preservesSpinFlip (.transverseFlip i) = true := rfl
theorem z_preserves_ising (i : Nat) :
preservesMagnetization (.loneZ i) = true := rfl
theorem mode_switch_flip (i : Nat) :
preserves .ising (.transverseFlip i) = false β§
preserves .spinFlip (.transverseFlip i) = true := by
constructor <;> rfl
theorem mode_switch_z (i : Nat) :
preserves .ising (.loneZ i) = true β§
preserves .spinFlip (.loneZ i) = false := by
constructor <;> rfl
def isingRing4 : List GateKind :=
[.zz 0 1, .zz 1 2, .zz 2 3, .zz 3 0]
theorem isingRing4_admitted : allPreserve preservesMagnetization isingRing4 = true := rfl
def spinFlip4 : List GateKind :=
isingRing4 ++ [.transverseFlip 0, .transverseFlip 1, .transverseFlip 2, .transverseFlip 3]
theorem spinFlip4_admitted : allPreserve preservesSpinFlip spinFlip4 = true := rfl
theorem adversarial_ising_rejected :
allPreserve preservesMagnetization (isingRing4 ++ [.transverseFlip 2]) = false := rfl
theorem adversarial_spin_flip_rejected :
allPreserve preservesSpinFlip (spinFlip4 ++ [.loneZ 1]) = false := rfl
theorem rejected_cons
(p : GateKind β Bool) (g : GateKind) (rest : List GateKind)
(hg : p g = false) :
allPreserve p (g :: rest) = false := by
simp [allPreserve, hg]
theorem adversarial_head_rejected (i : Nat) (rest : List GateKind) :
admitted .ising (.transverseFlip i :: rest) = false :=
rejected_cons _ _ _ (transverse_breaks_ising i)
/-- Orbit closure is a predicate on supports. A ring of length n is the full orbit of one bond. -/
def bondOrbit (n : Nat) : List GateKind :=
List.range n |>.map fun i => .zz i ((i + 1) % n)
theorem bondOrbit_four_agrees : bondOrbit 4 = isingRing4 := by
rfl
end CPSC
|