// *******************************************************************************
// 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;

    // Operator axioms, as operations the compiler is allowed to emit.
    // Lean names are in comments. Q# has no proof kernel; admission is the Bool gate.

    newtype GateKind = (
        Tag : Int,
        Q0 : Int,
        Q1 : Int
    );

    function ZZ(q0 : Int, q1 : Int) : GateKind {
        return GateKind(0, q0, q1);
    }

    function ParityEvenPair(q0 : Int, q1 : Int) : GateKind {
        return GateKind(1, q0, q1);
    }

    function TransverseFlip(q : Int) : GateKind {
        return GateKind(2, q, -1);
    }

    function LoneZ(q : Int) : GateKind {
        return GateKind(3, q, -1);
    }

    // preservesMagnetization
    function Axiom_PreservesMagnetization(g : GateKind) : Bool {
        let tag = g::Tag;
        return tag == 0 or tag == 3;
    }

    // preservesSpinFlip
    function Axiom_PreservesSpinFlip(g : GateKind) : Bool {
        let tag = g::Tag;
        return tag == 0 or tag == 1 or tag == 2;
    }

    // Mode 0 is Ising, mode 1 is spin-flip. Mirrors `preserves`.
    function Axiom_Preserves(mode : Int, g : GateKind) : Bool {
        return mode == 0 ? Axiom_PreservesMagnetization(g) | Axiom_PreservesSpinFlip(g);
    }

    // zz_mag / zz_spin: a bond is legal in both modes.
    operation Axiom_ApplyZZ(left : Qubit, right : Qubit, angle : Double) : Unit is Adj + Ctl {
        Rzz(2.0 * angle, left, right);
    }

    // flip_spin: a transverse flip is legal only after the spin-flip axiom accepts it.
    operation Axiom_ApplyFlip(target : Qubit, angle : Double) : Unit is Adj + Ctl {
        Rx(2.0 * angle, target);
    }

    // z_mag: a lone Z is legal only in Ising mode.
    operation Axiom_ApplyZ(target : Qubit, angle : Double) : Unit is Adj + Ctl {
        Rz(2.0 * angle, target);
    }

    // pair_spin: two flips, the parity-even pair.
    operation Axiom_ApplyPair(left : Qubit, right : Qubit, angle : Double) : Unit is Adj + Ctl {
        Rx(2.0 * angle, left);
        Rx(2.0 * angle, right);
    }
}