The modified SWAP exchanges adjacent Majorana pairs, with its scalar phase retained
OpenQAlgorithms.Papers.Independent.Intakethird100.P77.modifiedSwap_pairExchangeFor an existing ordered adjacent pair of wires, denote its four CAR generators by in wire order and define
Conjugation by exchanges the pairs: and for . In the Jordan–Wigner representation on those wires,
Here is the fermionic SWAP, rather than the ordinary SWAP alone. This operation moves Majorana pairs while respecting the quadratic construction.
Source correction. The sentence after Eq.(11) omits the scalar ; the exchange identities are unaffected.
import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P77
noncomputable section
namespace QAlgorithms.Papers.Independent.Intakethird100.P77
open QAlgorithms
open QAlgorithms.Complexity (Str)
open QAlgorithms.Papers.Independent.Advance50.P19 (Major CARSystem)
open QAlgorithms.Papers.Independent.Information100.P32 (Op)
open scoped BigOperators Matrix ComplexConjugate
attribute [local instance] Classical.propDecidable Classical.decEq
/-- PDF p.12: exchange of the two Majorana pairs, and corrected matrix
identification S=-i G(Z,X)=-i(CZ)(SWAP). The ordinary physical SWAP alone does
not implement this CAR exchange. The equality printed after Eq.(11) misses -i. -/
theorem modifiedSwap_pairExchange {n : ℕ} (c : CARSystem n) (w : Fin 2 ↪ Fin n)
(hadjacent : (w 0).val + 1 = (w 1).val) :
(∀ a b, star (modifiedSwap c.majorana w) * c.majorana (pairMajor w a b) *
modifiedSwap c.majorana w = c.majorana (pairMajor w (Fin.rev a) b)) ∧
modifiedSwap (jordanWigner n) w =
(-Complex.I) • embedOp (parityGate pauliZ pauliX) w ∧
parityGate pauliZ pauliX = (Gate.ofMatrix2 (controlled pauliZ * swapGate)).mat := by sorry
end QAlgorithms.Papers.Independent.Intakethird100.P77
end
Read-back
What the Lean code literally says, in plain math · gpt-6.1-sol
For every natural number , every family of Hermitian matrices on -bit strings satisfying , and every injection with , three assertions hold. Write and . First, for every and Boolean . Second, for the particular family and , one has , where , , , and is the two-bit matrix acting as on the even-parity sector indexed by the first bit and as on the odd-parity sector, with zero entries between the sectors. Here when agree outside the image of , and is zero otherwise. Third, this same equals controlled- multiplied by the swap matrix, after identifying a two-bit string with its ordered pair of bits; explicitly, if , and otherwise. The wire injection excludes .
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.