LF3 Setup: signs, detector settings, system-apparatus interfaces, two-qubit Pauli layer

Category: 3-Local (LF3 foundational types and concrete two-qubit Pauli / spin-projector layer).

Paper §2 / §9.4.

Defines the foundational types (Sign, DetectorSetting), the abstract pointer-readout and system-apparatus interfaces, and the concrete two-qubit Pauli / spin-projector layer used by Singlet/*. The setup-level matrix identities (§2.8: pauliDot_isHermitian, pauliDot_sq, spinProj_idem, spinProj_isHermitian, spinProj_complete) are proved below from DetectorSetting.sum_sq_components_eq_one, Sign.val_mul_self, and 2×2 matrix arithmetic.

Sign type

inductive CSD.LF3.Sign : Type

Two-element sign type for outcome labels (paper §9.4).

• plus : Sign
• minus : Sign

@[instance_reducible]

instance CSD.LF3.instDecidableEqSign : DecidableEq Sign

Equations

• CSD.LF3.instDecidableEqSign x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance CSD.LF3.instReprSign : Repr Sign

Equations

• CSD.LF3.instReprSign = { reprPrec := CSD.LF3.instReprSign.repr }

def CSD.LF3.instReprSign.repr : Sign → ℕ → Std.Format

Equations

• CSD.LF3.instReprSign.repr CSD.LF3.Sign.plus prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CSD.LF3.Sign.plus")).group prec✝
• CSD.LF3.instReprSign.repr CSD.LF3.Sign.minus prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CSD.LF3.Sign.minus")).group prec✝

@[instance_reducible]

instance CSD.LF3.instFintypeSign : Fintype Sign

Sign is a finite type with elements {plus, minus}. (Manual instance: the deriving Fintype handler regressed on a List.Nodup/Multiset.Nodup coercion under the Lean v4.33 toolchain; the explicit instance is equivalent and stable.)

Equations

• CSD.LF3.instFintypeSign = { elems := {CSD.LF3.Sign.plus, CSD.LF3.Sign.minus}, complete := ⋯ }

def CSD.LF3.Sign.val : Sign → ℝ

Numerical value: .plus ↦ 1, .minus ↦ -1.

Equations

• CSD.LF3.Sign.plus.val = 1
• CSD.LF3.Sign.minus.val = -1

def CSD.LF3.Sign.neg : Sign → Sign

Sign negation.

Equations

• CSD.LF3.Sign.plus.neg = CSD.LF3.Sign.minus
• CSD.LF3.Sign.minus.neg = CSD.LF3.Sign.plus

@[simp]

theorem CSD.LF3.Sign.neg_neg (s : Sign) : s.neg.neg = s

@[simp]

theorem CSD.LF3.Sign.val_plus : plus.val = 1

@[simp]

theorem CSD.LF3.Sign.val_minus : minus.val = -1

@[simp]

theorem CSD.LF3.Sign.val_neg (s : Sign) : s.neg.val = -s.val

@[simp]

theorem CSD.LF3.Sign.val_mul_self (s : Sign) : s.val * s.val = 1

@[simp]

theorem CSD.LF3.Sign.val_sq (s : Sign) : s.val ^ 2 = 1

theorem CSD.LF3.Sign.sum_univ {α : Type u_1} [AddCommMonoid α] (f : Sign → α) : ∑ s : Sign, f s = f plus + f minus

Sum over Sign as a two-term sum.

Detector settings

structure CSD.LF3.DetectorSetting : Type

Detector setting: a unit vector in ℝ³ (paper §2.5).

• vec : EuclideanSpace ℝ (Fin 3)

  The underlying real 3-vector.

• unit : ‖self.vec‖ = 1

  The vector has unit norm.

theorem CSD.LF3.DetectorSetting.sum_sq_components_eq_one (a : DetectorSetting) : a.vec.ofLp 0 ^ 2 + a.vec.ofLp 1 ^ 2 + a.vec.ofLp 2 ^ 2 = 1

For a unit vector in ℝ³, the sum of squared components is 1.

Abstract pointer-readout algebra

structure CSD.LF3.BinaryPointerProjectors (K : Type u_1) [NormedAddCommGroup K] [InnerProductSpace ℂ K] [FiniteDimensional ℂ K] : Type u_1

Binary pointer-readout algebra on a finite-dimensional pointer Hilbert space K (paper §2.7, spec §9.11). Self-adjointness is stated via the inner-product equation directly, avoiding the Star typeclass synthesis on K →L[ℂ] K (which requires the adjoint construction + completeness).

• proj : Sign → K →L[ℂ] K

  The two sign-indexed projectors.

• selfAdjoint (s : Sign) (x y : K) : inner ℂ ((self.proj s) x) y = inner ℂ x ((self.proj s) y)

  Each projector is self-adjoint with respect to the inner product.

• idem (s : Sign) : self.proj s ∘SL self.proj s = self.proj s

  Each projector is idempotent.

• orthogonal : self.proj Sign.plus ∘SL self.proj Sign.minus = 0

  The two projectors are mutually orthogonal.

• complete : self.proj Sign.plus + self.proj Sign.minus = 1

  The two projectors sum to the identity.

System-apparatus container

structure CSD.LF3.SystemApparatusSetup (K_A : Type u_1) (K_B : Type u_2) (H_SA : Type u_3) [NormedAddCommGroup K_A] [InnerProductSpace ℂ K_A] [FiniteDimensional ℂ K_A] [NormedAddCommGroup K_B] [InnerProductSpace ℂ K_B] [FiniteDimensional ℂ K_B] [NormedAddCommGroup H_SA] [InnerProductSpace ℂ H_SA] [FiniteDimensional ℂ H_SA] : Type (max u_1 u_2)

Finite-dimensional system-apparatus container (paper §2.7). Carrier types and instances are type parameters, Mathlib idiom.

• ptrA : BinaryPointerProjectors K_A

  Pointer-readout algebra on the A-side pointer space.

• ptrB : BinaryPointerProjectors K_B

  Pointer-readout algebra on the B-side pointer space.

Concrete two-qubit Pauli / spin-projector layer

HAB := EuclideanSpace ℂ (Fin 2 × Fin 2).

noncomputable def CSD.LF3.pauliDot (a : DetectorSetting) : Matrix (Fin 2) (Fin 2) ℂ

Pauli operator σ·a = a_x σ_x + a_y σ_y + a_z σ_z as a 2×2 matrix.

Equations

• CSD.LF3.pauliDot a = !![↑(a.vec.ofLp 2), ↑(a.vec.ofLp 0) - Complex.I * ↑(a.vec.ofLp 1); ↑(a.vec.ofLp 0) + Complex.I * ↑(a.vec.ofLp 1), -↑(a.vec.ofLp 2)]

noncomputable def CSD.LF3.sigmaDotLeft (a : DetectorSetting) : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ

(σ·a) ⊗ I on HAB.

Equations

• CSD.LF3.sigmaDotLeft a = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (CSD.LF3.pauliDot a) 1

noncomputable def CSD.LF3.sigmaDotRight (b : DetectorSetting) : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ

I ⊗ (σ·b) on HAB.

Equations

• CSD.LF3.sigmaDotRight b = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 (CSD.LF3.pauliDot b)

noncomputable def CSD.LF3.sigmaDotJoint (a b : DetectorSetting) : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ

(σ·a) ⊗ (σ·b) on HAB.

Equations

• CSD.LF3.sigmaDotJoint a b = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (CSD.LF3.pauliDot a) (CSD.LF3.pauliDot b)

noncomputable def CSD.LF3.spinProj (s : Sign) (a : DetectorSetting) : Matrix (Fin 2) (Fin 2) ℂ

One-qubit spin projector Πˢ(a) = (I + s σ·a) / 2.

Equations

• CSD.LF3.spinProj s a = (1 / 2) • (1 + ↑s.val • CSD.LF3.pauliDot a)

noncomputable def CSD.LF3.jointSpinProj (s t : Sign) (a b : DetectorSetting) : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ

Joint two-qubit spin projector Πˢ(a) ⊗ Πᵗ(b).

Equations

• CSD.LF3.jointSpinProj s t a b = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (CSD.LF3.spinProj s a) (CSD.LF3.spinProj t b)

Setup theorem targets (paper §2.8)

Each proof reduces to straightforward 2×2 matrix arithmetic over Mathlib's Matrix / !![…] API plus DetectorSetting.sum_sq_components_eq_one and Sign.val_mul_self.

theorem CSD.LF3.pauliDot_isHermitian (a : DetectorSetting) : (pauliDot a).IsHermitian

σ·a is Hermitian. Cell-by-cell from the pauliDot definition: diagonal entries are real (so star = id), off-diagonal entries are a_x ∓ i a_y (star = flip the imaginary part).

theorem CSD.LF3.pauliDot_sq (a : DetectorSetting) : pauliDot a * pauliDot a = 1

(σ·a)² = I for a unit vector a. Diagonal entries collapse to a_0² + a_1² + a_2² = 1 via Complex.I_sq = -1; off-diagonal entries cancel pairwise.

theorem CSD.LF3.spinProj_isHermitian (s : Sign) (a : DetectorSetting) : (spinProj s a).IsHermitian

The spin projector is Hermitian. (1/2) • (1 + s • σ·a) is real-linear in the Hermitian operator pauliDot a; both scalars 1/2 and s.val are real, so star-fixed.

theorem CSD.LF3.spinProj_idem (s : Sign) (a : DetectorSetting) : spinProj s a * spinProj s a = spinProj s a

The spin projector is idempotent. Expand ((1/2) • A)² = (1/4) • A², where A² = (1 + s·σ)² = 1 + 2s·σ + s²·σ² = 2 + 2s·σ = 2A via pauliDot_sq and Sign.val_mul_self.

theorem CSD.LF3.spinProj_complete (a : DetectorSetting) : spinProj Sign.plus a + spinProj Sign.minus a = 1

The two spin projectors sum to the identity.

Pointer-completeness re-exports (paper §2.8)

theorem CSD.LF3.pointer_a_complete {K_A : Type u_1} {K_B : Type u_2} {H_SA : Type u_3} [NormedAddCommGroup K_A] [InnerProductSpace ℂ K_A] [FiniteDimensional ℂ K_A] [NormedAddCommGroup K_B] [InnerProductSpace ℂ K_B] [FiniteDimensional ℂ K_B] [NormedAddCommGroup H_SA] [InnerProductSpace ℂ H_SA] [FiniteDimensional ℂ H_SA] (S : SystemApparatusSetup K_A K_B H_SA) : S.ptrA.proj Sign.plus + S.ptrA.proj Sign.minus = 1

Pointer-completeness re-export, A side (paper §2.8).

theorem CSD.LF3.pointer_b_complete {K_A : Type u_1} {K_B : Type u_2} {H_SA : Type u_3} [NormedAddCommGroup K_A] [InnerProductSpace ℂ K_A] [FiniteDimensional ℂ K_A] [NormedAddCommGroup K_B] [InnerProductSpace ℂ K_B] [FiniteDimensional ℂ K_B] [NormedAddCommGroup H_SA] [InnerProductSpace ℂ H_SA] [FiniteDimensional ℂ H_SA] (S : SystemApparatusSetup K_A K_B H_SA) : S.ptrB.proj Sign.plus + S.ptrB.proj Sign.minus = 1

Pointer-completeness re-export, B side.