File size: 3,738 Bytes
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 | // *******************************************************************************
// Copyright (c) 2026 Ahmad Ali Parr and others.
//
// SPDX-License-Identifier: LicenseRef-CPSC-ESCL-1.0 OR AGPL-3.0-only
// *******************************************************************************
namespace ConservationPreservingScattering {
open Microsoft.Quantum.Intrinsic;
open Microsoft.Quantum.Arrays;
open Microsoft.Quantum.Canon;
// Lemmas as total functions and interpreting operations.
// Each one is the Q# image of a theorem in lean/CPSC/Lemmas.lean.
function Lemma_NilAdmitted() : Bool {
return true;
}
function Lemma_ConsAdmitted(mode : Int, head : GateKind, tailOk : Bool) : Bool {
return Axiom_Preserves(mode, head) and tailOk;
}
function Lemma_AllAdmitted(mode : Int, schedule : GateKind[]) : Bool {
mutable ok = true;
for g in schedule {
if not Axiom_Preserves(mode, g) {
set ok = false;
}
}
return ok;
}
function Lemma_AppendAdmitted(left : Bool, right : Bool) : Bool {
return left and right;
}
function Lemma_TransverseBreaksIsing(q : Int) : Bool {
return not Axiom_PreservesMagnetization(TransverseFlip(q));
}
function Lemma_LoneZBreaksSpinFlip(q : Int) : Bool {
return not Axiom_PreservesSpinFlip(LoneZ(q));
}
operation Lemma_ApplyAdmitted(
register : Qubit[],
g : GateKind,
angle : Double
) : Unit is Adj + Ctl {
let n = Length(register);
let q0 = g::Q0;
let q1 = g::Q1;
if q0 < 0 or q0 >= n or (q1 >= n) {
fail "CPSC lemma: qubit outside the register";
}
if g::Tag == 0 {
if q1 < 0 {
fail "CPSC lemma: ZZ is missing its second qubit";
}
Axiom_ApplyZZ(register[q0], register[q1], angle);
} elif g::Tag == 1 {
if q1 < 0 {
fail "CPSC lemma: pair is missing its second qubit";
}
Axiom_ApplyPair(register[q0], register[q1], angle);
} elif g::Tag == 2 {
Axiom_ApplyFlip(register[q0], angle);
} elif g::Tag == 3 {
Axiom_ApplyZ(register[q0], angle);
} else {
fail "CPSC lemma: unknown gate tag";
}
}
// circuit_comm_*: interpret only an admitted schedule. A rejected head fails closed.
operation Lemma_Interpret(
register : Qubit[],
mode : Int,
schedule : GateKind[],
angle : Double
) : Unit is Adj + Ctl {
if not Lemma_AllAdmitted(mode, schedule) {
fail "CPSC rejected the schedule: a factor breaks the active invariant";
}
for g in schedule {
Lemma_ApplyAdmitted(register, g, angle);
}
}
function Lemma_BondOrbit(n : Int) : GateKind[] {
mutable gates = [];
for i in 0 .. n - 1 {
set gates += [ZZ(i, (i + 1) % n)];
}
return gates;
}
function Lemma_TransverseOrbit(n : Int) : GateKind[] {
mutable gates = [];
for i in 0 .. n - 1 {
set gates += [TransverseFlip(i)];
}
return gates;
}
operation Lemma_IsingCircuit(register : Qubit[], angle : Double) : Unit is Adj + Ctl {
let schedule = Lemma_BondOrbit(Length(register));
Lemma_Interpret(register, 0, schedule, angle);
}
operation Lemma_SpinFlipCircuit(register : Qubit[], angle : Double) : Unit is Adj + Ctl {
let n = Length(register);
let schedule = Lemma_BondOrbit(n) + Lemma_TransverseOrbit(n);
Lemma_Interpret(register, 1, schedule, angle);
}
}
|