A nonzero discarded coefficient of weight above w* k_h^Γ in a second-order step

Pauli/LayerWitness.lean shows that on an 8-qubit brickwork with k_h = 2, Γ = 2 and the weight-one input Z₃ (so w* = 1), the Pauli string P₆ of weight 6 is reachable under the four layers L₁, L₂, L₂, L₁ of a second-order product-formula step (apd:eq:suzuki). Reachability ignores the rotation angles, so by itself it does not show that P₆ occurs in the conjugated operator. This file supplies that step. It computes the coefficient of P₆ after the literal four-layer word in closed form,

coeff (pf2Output θ) (cls P₆) = -(sin θ)^3 (sin 2θ)^2,

which is nonzero for 0 < θ < π/2, and shows that the same coefficient survives in the operator discarded by the truncation at w* = 1, the component Õ^{(d)}_{≥w*+1} of apd:eq:step_component. Hence the exponent ΥΓ in the weight bound w* k_h^{ΥΓ} on the discarded component (apd:thm:lightcone) cannot be replaced by Γ: here w* k_h^Γ = 4 < 6.

Main definitions

• pf2Rotations θ: the rotation word L₁ ++ L₂ ++ L₂ ++ L₁, every rotation with the same conjugation angle θ.
• pf2Output θ: the matrix obtained by conjugating Z₃ with that word (layerConj).
• pf2Discard θ: what the truncation at weight 1 removes from pf2Output θ.

Main results

• pf2_coeff_polynomial, pf2_coeff_sines: the coefficient of pf2Output θ at cls P₆ is -4 (cos θ)^2 (sin θ)^5 = -(sin θ)^3 (sin 2θ)^2.
• pf2_named_P6_component: the corresponding operator component is ((sin θ)^3 (sin 2θ)^2) • P₆. The sign changes because the canonical representative is herm (cls P₆) = phaseMul 2 P₆ (herm_P6_sign), whose matrix is -P₆.
• pf2Output_eq_four_layers: pf2Output θ is the nested conjugation by the four layers.
• pf2_coeff_ne_zero: the coefficient is nonzero whenever 0 < θ and 2 * θ < π.
• pf2Discard_coeff, actual_discard_exceeds_gamma_bound: the discarded operator has a nonzero coefficient at a Pauli class of weight greater than w* k_h^Γ = 4.

Method

coeffVec_layerConj turns the matrix conjugation into the coefficient action layerAct, and rotAct_apply gives a two-term recurrence for one rotation. The recurrence is unfolded backwards from the target class through the fourteen rotations of the word. Only 23 coefficient nodes are expanded; every other branch the recurrence meets is shown to vanish by the sound support test backwardReaches (coeff_zero_of_not_backward), and every sign is computed exactly from partnerSign. Nothing is evaluated numerically.

noncomputable def Lean4LPD.LayerCounterexample.pf2Rotations (θ : ℝ) : List (PauliString 8 × ℝ)

The rotation word of one second-order product-formula step (apd:eq:suzuki) on the brickwork of LayerWitness: the four layers L₁, L₂, L₂, L₁, every rotation with the same half-step conjugation angle θ.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Lean4LPD.LayerCounterexample.pf2Output (θ : ℝ) : Matrix (Bits 8) (Bits 8) ℂ

The conjugated operator before truncation: the matrix of Z₃ conjugated by the whole word pf2Rotations θ. It is defined by matrix conjugation (layerConj), not as a member of a reachable set; its high-weight part is the discarded component of apd:eq:step_component.

Equations

• Lean4LPD.LayerCounterexample.pf2Output θ = Lean4LPD.PauliString.layerConj (Lean4LPD.LayerCounterexample.pf2Rotations θ) (Lean4LPD.PauliString.Z 3).toMatrix

theorem Lean4LPD.LayerCounterexample.pf2Rotations_hermitian (θ : ℝ) (g : PauliString 8 × ℝ) : g ∈ pf2Rotations θ → IsSelfAdjoint g.1

Every generator of the word is a Hermitian Pauli string, by isSelfAdjoint_L₁ and isSelfAdjoint_L₂. This is the hypothesis under which coeffVec_layerConj turns the matrix conjugation into the coefficient action layerAct.

theorem Lean4LPD.LayerCounterexample.herm_input : PauliString.herm (PauliString.Z 3).cls = PauliString.Z 3

The input Z₃ is the canonical Hermitian representative herm of its own class, so its coefficient vector can be read off directly (input_coeffVec).

theorem Lean4LPD.LayerCounterexample.input_coeffVec : PauliString.coeffVec (PauliString.Z 3).toMatrix = WithLp.toLp 2 (Pi.single (PauliString.Z 3).cls 1)

The coefficient vector of the input Z₃ is the unit vector at its class cls (Z 3).

theorem Lean4LPD.LayerCounterexample.pf2_coeff_polynomial (θ : ℝ) : PauliString.coeff (pf2Output θ) LayerWitness.P₆.cls = -4 * ↑(Real.cos θ) ^ 2 * ↑(Real.sin θ) ^ 5

The coefficient of P₆ as a polynomial in cos θ and sin θ. The coefficient of pf2Output θ at the weight-six class cls P₆ equals -4 (cos θ)^2 (sin θ)^5, obtained by unfolding the coefficient recurrence rotAct_apply through the fourteen rotations of the literal second-order word. The sign refers to the canonical representative herm (cls P₆); see pf2_named_P6_component for the component on P₆ itself.

theorem Lean4LPD.LayerCounterexample.pf2Output_eq_four_layers (θ : ℝ) : pf2Output θ = PauliString.layerConj (List.map (fun (G : PauliString 8) => (G, θ)) LayerWitness.L₁) (PauliString.layerConj (List.map (fun (G : PauliString 8) => (G, θ)) LayerWitness.L₂) (PauliString.layerConj (List.map (fun (G : PauliString 8) => (G, θ)) LayerWitness.L₂) (PauliString.layerConj (List.map (fun (G : PauliString 8) => (G, θ)) LayerWitness.L₁) (PauliString.Z 3).toMatrix)))

The computed output is the literal four-layer L₁,L₂,L₂,L₁ second-order formula of apd:eq:suzuki: the nested conjugation of Z₃ by the four layers, with the two adjacent L₂ half-steps kept separate and the same angle in every layer, not a merged or angle-rescaled circuit.

theorem Lean4LPD.LayerCounterexample.pf2_coeff_sines (θ : ℝ) : PauliString.coeff (pf2Output θ) LayerWitness.P₆.cls = -↑(Real.sin θ) ^ 3 * ↑(Real.sin (2 * θ)) ^ 2

The coefficient in product form, -(sin θ)^3 (sin 2θ)^2. This is pf2_coeff_polynomial rewritten with sin 2θ = 2 sin θ cos θ; in this form it is evident that the coefficient is nonzero at every small angle (pf2_coeff_ne_zero). The minus sign is that of the canonical representative herm (cls P₆), not of the tensor product P₆ itself (herm_P6_sign). This upgrades the reachability witness LayerWitness.P₆_mem_reachable_unmerged to an actual coefficient.

theorem Lean4LPD.LayerCounterexample.herm_P6_sign : PauliString.herm LayerWitness.P₆.cls = PauliString.phaseMul 2 LayerWitness.P₆

The named witness P₆ has three Y sites and carries the phase 3 = #{Y-sites} mod 4, whereas herm records only the parity of the number of Y sites (phase 1). The two representatives of the class differ by the phase 2, that is by the factor i^2 = -1, which accounts for the sign in pf2_coeff_sines.

theorem Lean4LPD.LayerCounterexample.pf2_named_P6_component (θ : ℝ) : PauliString.coeff (pf2Output θ) LayerWitness.P₆.cls • (PauliString.herm LayerWitness.P₆.cls).toMatrix = (↑(Real.sin θ) ^ 3 * ↑(Real.sin (2 * θ)) ^ 2) • LayerWitness.P₆.toMatrix

On the named positive tensor P₆, the amplitude is sin³θ sin²(2θ). This is an operator-component identity, with coeff • toMatrix (herm (cls P₆)) on the left, not an identification of classes up to an unspecified phase.

theorem Lean4LPD.LayerCounterexample.input_local (p : PauliIndex 8) : 1 < PauliString.wt p → PauliString.coeff (PauliString.Z 3).toMatrix p = 0

The input Z₃ satisfies the weight-one cutoff: its coefficients at all classes of weight greater than 1 vanish. So the step starts from an operator of weight at most w* = 1, as the truncated input in apd:eq:step_component does, rather than from a large initial observable.

theorem Lean4LPD.LayerCounterexample.pf2_coeff_ne_zero {θ : ℝ} (hθ : 0 < θ) (hθπ : 2 * θ < Real.pi) : PauliString.coeff (pf2Output θ) LayerWitness.P₆.cls ≠ 0

The coefficient is nonzero throughout 0<θ<π/2, so the witness works at arbitrarily small angles, not only in a large-angle regime.

noncomputable def Lean4LPD.LayerCounterexample.pf2Discard (θ : ℝ) : Matrix (Bits 8) (Bits 8) ℂ

The operator discarded after this second-order step by the truncation at w* = 1: pf2Output θ minus its part on classes of weight at most one. This is the discarded component Õ^{(d)}_{≥w*+1} of apd:eq:step_component for this step, not the part that is retained.

Equations

• One or more equations did not get rendered due to their size.

theorem Lean4LPD.LayerCounterexample.pf2Discard_coeff (θ : ℝ) : PauliString.coeff (pf2Discard θ) LayerWitness.P₆.cls = PauliString.coeff (pf2Output θ) LayerWitness.P₆.cls

The weight-six coefficient is preserved in the discarded operator: pf2Discard θ and pf2Output θ have the same coefficient at cls P₆, because wt (cls P₆) = 6 > 1 puts that class outside the retained set. This is the truncation step that a reachability argument alone does not provide.

theorem Lean4LPD.LayerCounterexample.actual_discard_exceeds_gamma_bound {θ : ℝ} (hθ : 0 < θ) (hθπ : 2 * θ < Real.pi) : ∃ (p : PauliIndex 8), PauliString.coeff (pf2Discard θ) p ≠ 0 ∧ 1 * 2 ^ 2 < PauliString.wt p

The exponent ΥΓ cannot be replaced by Γ. For every 0<θ<π/2, the two-local disjoint-support layers L₁, L₂ of LayerWitness (so k_h = 2, Γ = 2) produce, after one second-order step from the weight-one input Z₃, a discarded operator X₁ at cutoff w* = 1 (apd:eq:step_component) with a nonzero coefficient at a Pauli class of weight greater than w* k_h^Γ = 1 * 2 ^ 2 = 4; the witness is cls P₆, of weight 6. The weight bound w* k_h^{ΥΓ} of apd:thm:lightcone, which for the ΥΓ = 4 layers of this step equals 16, is compatible with this witness.