A two-qubit witness with a nonzero discarded component

A concrete non-vacuity witness for apd:eq:step_component and apd:thm:triangle. The input P = ZI has weight one. A rotation generated by G = XX through conjugation angle π / 2 turns it into Q = YX, of weight two and Pauli norm one. A second rotation, generated by Q, leaves this component unchanged. A weight-one cutoff at the end of this two-rotation step therefore removes a nonzero observable. So the statements about discarded operators in Pauli/Discard and Pauli/TrotterTruncate are not vacuous: they are exercised on a step whose high-weight sector is nonempty and whose retained set is not univ.

The angle π / 2 tests a nonzero discard and the placement of the cutoff at the step boundary, not small-angle damping.

All statements use the library's rotation rot and its entrywise Pauli model toMatrix. That these are the matrix exponential and a phase times the Kronecker product of Pauli matrices is proved separately, in RotationExp and Pauli/Tensor.

Main results

• first_rotation, second_rotation: the two conjugations, P ↦ Q and Q ↦ Q.
• traj_two: the untruncated two-rotation trajectory ends at Q.
• interior_highNorm, boundary_eq_zero: the truncated trajectory carries high-weight norm one inside the step and is zero at the step boundary.
• discardedStep_zero, discardedStep_ne_zero, discardedStep_pauliNorm: the first discarded operator is Q, it is nonzero, and its Pauli norm is one.

def Lean4LPD.DiscardWitness.G : PauliString 2

The Hermitian two-qubit generator XX, defined in the entrywise Pauli model.

Equations

• Lean4LPD.DiscardWitness.G = { x := ![1, 1], z := ![0, 0], phase := 0 }

def Lean4LPD.DiscardWitness.P : PauliString 2

The nonzero weight-one input ZI.

Equations

• Lean4LPD.DiscardWitness.P = { x := ![0, 0], z := ![1, 0], phase := 0 }

def Lean4LPD.DiscardWitness.Q : PauliString 2

The weight-two partner YX that the first rotation creates.

Equations

• Lean4LPD.DiscardWitness.Q = { x := ![1, 1], z := ![1, 0], phase := 1 }

theorem Lean4LPD.DiscardWitness.isSelfAdjoint_G : IsSelfAdjoint G

Concrete regression data for apd:eq:step_component: G is Hermitian.

theorem Lean4LPD.DiscardWitness.isSelfAdjoint_P : IsSelfAdjoint P

Concrete regression data for apd:eq:step_component: the input is Hermitian.

theorem Lean4LPD.DiscardWitness.isSelfAdjoint_Q : IsSelfAdjoint Q

Concrete regression data for apd:eq:step_component: the new component is Hermitian.

theorem Lean4LPD.DiscardWitness.weight_G : G.weight = 2

Concrete regression data for apd:eq:step_component: n = k_h = 2, so the generator is not one-local.

theorem Lean4LPD.DiscardWitness.weight_P : P.weight = 1

Concrete regression data for apd:eq:step_component: k_o = 1 < n = 2.

theorem Lean4LPD.DiscardWitness.weight_Q : Q.weight = 2

Concrete regression data for apd:eq:step_component: the created Pauli lies strictly above w* = 1.

theorem Lean4LPD.DiscardWitness.herm_P : PauliString.herm P.cls = P

Concrete regression helper for apd:eq:step_component: the input uses the canonical Hermitian representative.

theorem Lean4LPD.DiscardWitness.herm_Q : PauliString.herm Q.cls = Q

Concrete regression helper for apd:eq:step_component: the created Pauli uses the canonical Hermitian representative.

theorem Lean4LPD.DiscardWitness.sympForm_G_P : G.sympForm P = 1

Concrete regression helper for apd:eq:step_component: the first generator anticommutes with the input.

theorem Lean4LPD.DiscardWitness.phaseMul_G_P : PauliString.phaseMul 1 (G * P) = Q

Concrete regression helper for apd:eq:step_component: the first rotation's Hermitian partner is exactly Q.

theorem Lean4LPD.DiscardWitness.input_ne_zero : P.toMatrix ≠ 0

Concrete regression example for apd:eq:step_component: the input is nonzero.

theorem Lean4LPD.DiscardWitness.input_local (p : PauliIndex 2) (hp : 1 < PauliString.wt p) : PauliString.coeff P.toMatrix p = 0

Concrete regression example for apd:eq:step_component: input locality is genuinely k_o = 1, not k_o = n.

theorem Lean4LPD.DiscardWitness.input_highNorm : PauliString.highNorm 1 P.toMatrix = 0

Concrete regression example for apd:eq:step_component: no high-weight mass is present initially; the later discarded mass must be produced by the rotation.

theorem Lean4LPD.DiscardWitness.first_rotation : rot G.toMatrix (Real.pi / 2) * P.toMatrix * rot G.toMatrix (-(Real.pi / 2)) = Q.toMatrix

Concrete regression example for apd:eq:step_component: the first rotation creates exactly one unit-amplitude weight-two Pauli, not a merely reachable branch.

theorem Lean4LPD.DiscardWitness.second_rotation (θ : ℝ) : rot Q.toMatrix θ * Q.toMatrix * rot Q.toMatrix (-θ) = Q.toMatrix

Concrete regression example for apd:eq:step_component: a genuine second rotation preserves the high-weight component until the step boundary.

theorem Lean4LPD.DiscardWitness.highSet_nonempty : (PauliString.highSet 2 1).Nonempty

Concrete regression example for apd:eq:step_component: the high-weight sector at the chosen cutoff is nonempty.

theorem Lean4LPD.DiscardWitness.cutoff_ne_univ : (PauliString.highSet 2 1)ᶜ ≠ Finset.univ

Concrete regression example for apd:eq:step_component: the retained set is a proper subset of all Pauli classes, since it excludes the class of Q.

theorem Lean4LPD.DiscardWitness.cutoff_Q : PauliString.truncOp (PauliString.highSet 2 1)ᶜ Q.toMatrix = 0

Concrete regression example for apd:eq:step_component: the cutoff removes the whole new component, by its coefficients, not by an assumed operator identity.

theorem Lean4LPD.DiscardWitness.discarded_eq_Q : Q.toMatrix - PauliString.truncOp (PauliString.highSet 2 1)ᶜ Q.toMatrix = Q.toMatrix

Concrete regression example for apd:eq:step_component: the discarded operator is Q. This is the subtraction defining the paper's Õ^{(d)}_{≥w*+1}, specialized to the evolved witness.

theorem Lean4LPD.DiscardWitness.discarded_ne_zero : Q.toMatrix - PauliString.truncOp (PauliString.highSet 2 1)ᶜ Q.toMatrix ≠ 0

Concrete regression example for apd:eq:step_component: the discarded operator is provably nonzero.

theorem Lean4LPD.DiscardWitness.input_pauliNorm : PauliString.pauliNorm P.toMatrix = 1

Concrete regression helper for apd:thm:triangle: the normalized Pauli norm of the input is exactly one.

theorem Lean4LPD.DiscardWitness.Q_pauliNorm : PauliString.pauliNorm Q.toMatrix = 1

Concrete regression example for apd:eq:step_component: the produced Pauli has exact normalized norm one.

theorem Lean4LPD.DiscardWitness.discarded_pauliNorm : PauliString.pauliNorm (Q.toMatrix - PauliString.truncOp (PauliString.highSet 2 1)ᶜ Q.toMatrix) = 1

Concrete regression example for apd:thm:triangle: the discarded norm, the scalar used in the triangle bound's summand, is exactly one.

theorem Lean4LPD.DiscardWitness.Q_highNorm : PauliString.highNorm 1 Q.toMatrix = 1

Concrete regression example for apd:eq:step_component: the high-weight scalar before the cutoff is also exactly one.

def Lean4LPD.DiscardWitness.Gs (g : ℕ) : PauliString 2

The two-generator period: first XX, then YX. Both are genuine weight-two Hermitian strings. YX commutes with the evolved observable Q, not with the first generator XX.

Equations

• Lean4LPD.DiscardWitness.Gs g = if g % 2 = 0 then Lean4LPD.DiscardWitness.G else Lean4LPD.DiscardWitness.Q

noncomputable def Lean4LPD.DiscardWitness.angles : ℕ → ℝ

Both rotations use conjugation angle π / 2; no zero-angle padding is used.

Equations

• Lean4LPD.DiscardWitness.angles x✝ = Real.pi / 2

theorem Lean4LPD.DiscardWitness.generators_selfAdjoint (g : ℕ) : IsSelfAdjoint (Gs g)

Concrete regression data for apd:eq:step_component: every generator is Hermitian.

theorem Lean4LPD.DiscardWitness.generators_weight (g : ℕ) : (Gs g).weight = 2

Concrete regression data for apd:eq:step_component: every generator has exactly k_h = 2, rather than only a degenerate upper bound.

theorem Lean4LPD.DiscardWitness.traj_one : PauliString.traj Gs angles P.toMatrix 1 = Q.toMatrix

Concrete regression example for apd:eq:step_component: the first rotation creates weight-two mass in the actual recursive, untruncated trajectory.

theorem Lean4LPD.DiscardWitness.traj_two : PauliString.traj Gs angles P.toMatrix 2 = Q.toMatrix

Concrete regression example for apd:eq:step_component: the two-rotation evolution still contains exactly Q immediately before its end-of-step cutoff.

theorem Lean4LPD.DiscardWitness.schedule_zero : PauliString.trotterSchedule 2 1 0 = Finset.univ

Concrete regression example for apd:thm:triangle: the first rotation of the length-two step is not followed by a cutoff.

theorem Lean4LPD.DiscardWitness.schedule_one : PauliString.trotterSchedule 2 1 1 = (PauliString.highSet 2 1)ᶜ

Concrete regression example for apd:thm:triangle: the second rotation is followed by the genuine weight-one cutoff, at the end of the step.

theorem Lean4LPD.DiscardWitness.step_one : PauliString.trotterStepTraj Gs angles 2 1 P.toMatrix 1 = 0

Concrete regression example for apd:eq:step_component: the independent full-step recurrence removes the newly generated weight-two observable at the first step boundary.

theorem Lean4LPD.DiscardWitness.interior_eq_Q : PauliString.trotterTraj Gs angles 2 1 P.toMatrix 1 = Q.toMatrix

Concrete regression example for apd:thm:triangle: the rotation-indexed trajectory still contains Q inside the step, because the cutoff acts at the step boundary and not after every rotation.

theorem Lean4LPD.DiscardWitness.interior_highNorm : PauliString.highNorm 1 (PauliString.trotterTraj Gs angles 2 1 P.toMatrix 1) = 1

Concrete regression example for apd:thm:triangle: the interior high-weight mass is exactly one. This excludes a vacuous zero-sector witness.

theorem Lean4LPD.DiscardWitness.boundary_eq_zero : PauliString.trotterTraj Gs angles 2 1 P.toMatrix 2 = 0

Concrete regression example for apd:eq:step_component: after the second rotation, the rotation-indexed execution agrees with the independently computed step cutoff.

theorem Lean4LPD.DiscardWitness.boundary_highNorm : PauliString.highNorm 1 (PauliString.trotterTraj Gs angles 2 1 P.toMatrix 2) = 0

Concrete regression example for apd:eq:step_component: the kept high-weight mass is zero at the boundary, in contrast to the positive mass discarded at that same boundary.

theorem Lean4LPD.DiscardWitness.discardedStep_zero : PauliString.discardedStep Gs angles 2 1 P.toMatrix 0 = Q.toMatrix

Concrete regression example for apd:eq:step_component: the named discarded-step operator X₁, not only an independently written difference, is exactly Q.

theorem Lean4LPD.DiscardWitness.discardedStep_ne_zero : PauliString.discardedStep Gs angles 2 1 P.toMatrix 0 ≠ 0

Concrete regression example for apd:eq:step_component: the algorithm's first discarded operator is provably nonzero.

theorem Lean4LPD.DiscardWitness.discardedStep_pauliNorm : PauliString.pauliNorm (PauliString.discardedStep Gs angles 2 1 P.toMatrix 0) = 1

Concrete regression example for apd:thm:triangle: the generic discarded-operator norm bridge computes the first error summand as exactly one.

theorem Lean4LPD.DiscardWitness.discardedStep_pauliNorm_pos : 0 < PauliString.pauliNorm (PauliString.discardedStep Gs angles 2 1 P.toMatrix 0)

Concrete regression example for apd:thm:triangle: the first discarded norm is strictly positive, unlike the high-weight norm of the retained boundary state.