diff --git a/LeanPool/SingleCopyStabilizer.lean b/LeanPool/SingleCopyStabilizer.lean new file mode 100644 index 0000000000..577d0dfe24 --- /dev/null +++ b/LeanPool/SingleCopyStabilizer.lean @@ -0,0 +1,52 @@ +/- +Copyright (c) 2026 Antonio Anna Mele. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Antonio Anna Mele +-/ +module + +public import LeanPool.SingleCopyStabilizer.ExactLearningTheorem + +/-! +# Exact adaptive single-copy stabilizer learning + +Source: arxiv:2610.02031 +Authors: Antonio Anna Mele +Status: verified +Main declarations: `LeanPool.SingleCopyStabilizer.ExactLearningTheorem.exact_learning` +Tags: quantum-computing, stabilizer-states, quantum-learning, probability +MSC: 81P68, 68Q32, 81P45 +-/ + +/-! +## Mathematical overview + +Ported from Antonio Anna Mele’s MIT-licensed formalization at +`d8282e1d59a1a9b8d34396f06298f478c54237c6`. + +The original license for this project’s imported sources follows. +-/ + +/- +MIT License + +Copyright (c) 2026 Antonio Anna Mele + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. +-/ diff --git a/LeanPool/SingleCopyStabilizer/AdaptiveProcess.lean b/LeanPool/SingleCopyStabilizer/AdaptiveProcess.lean new file mode 100644 index 0000000000..bf1229e42c --- /dev/null +++ b/LeanPool/SingleCopyStabilizer/AdaptiveProcess.lean @@ -0,0 +1,237 @@ +/- +Copyright (c) 2026 Antonio Anna Mele. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Antonio Anna Mele +-/ +module + +public import Mathlib.Algebra.BigOperators.Field +public import Mathlib.Tactic.Ring +public import Mathlib.Basic.Real.Basic +public import Mathlib.Tactic.Linarith +public import Mathlib.Tactic.Positivity + + +/-! +# A finite-tree tail bound for adaptive rank-decreasing processes + +A state may store the entire previous history. At each state, a finite kernel +chooses an outcome and the state updates deterministically. Rank never +increases, and while positive it strictly decreases with probability at least +`p`. The probability of positive rank after `t` rounds is bounded using a +killed exponential potential. This yields a coarse exponential tail; it does +not establish the paper's sharper leading constant `2n`. +-/ + +@[expose] public section + +noncomputable section + +namespace LeanPool.SingleCopyStabilizer.AdaptiveProcess + +open scoped BigOperators + +/-- A finite outcome kernel together with a monotone natural-valued rank. +There is no Markov restriction: `S` can contain the complete history. -/ +structure RankedProcess (S Ω : Type*) [Fintype Ω] where + /-- Conditional probability of an outcome at the current state. -/ + weight : S → Ω → ℝ + /-- State reached after observing the chosen outcome. -/ + next : S → Ω → S + /-- Natural-valued obstruction whose disappearance marks success. -/ + rank : S → ℕ + weight_nonneg : ∀ s o, 0 ≤ weight s o + weight_sum : ∀ s, ∑ o, weight s o = 1 + rank_mono : ∀ s o, rank (next s o) ≤ rank s + +/-- The exponential potential is killed on reaching rank zero. -/ +def potential (r : ℕ) : ℝ := if r = 0 then 0 else 2 ^ r + +@[simp] theorem potential_zero : potential 0 = 0 := by simp [potential] + +theorem potential_nonneg (r : ℕ) : 0 ≤ potential r := by + unfold potential + split_ifs <;> positivity + +theorem potential_le_pow (r : ℕ) : potential r ≤ (2 : ℝ) ^ r := by + unfold potential + split_ifs + · positivity + · exact le_rfl + +theorem potential_mono {a b : ℕ} (h : a ≤ b) : potential a ≤ potential b := by + by_cases ha : a = 0 + · simpa [ha] using potential_nonneg b + have hb : b ≠ 0 := by omega + simpa [potential, ha, hb] using + (pow_le_pow_right₀ (by norm_num : (1 : ℝ) ≤ 2) h) + +/-- Strict rank progress at least halves the killed exponential potential. -/ +theorem potential_le_half_of_lt {a b : ℕ} (h : a < b) : + potential a ≤ potential b / 2 := by + have hb : b ≠ 0 := by omega + by_cases ha : a = 0 + · rw [ha, potential_zero] + exact div_nonneg (potential_nonneg b) (by norm_num) + have hp : (2 : ℝ) ^ (a + 1) ≤ 2 ^ b := + pow_le_pow_right₀ (by norm_num) (by omega) + rw [pow_succ] at hp + simp only [potential, ite_eq_right ha, ite_eq_right hb] + linarith + +variable {S Ω : Type*} [Fintype Ω] + +namespace RankedProcess + +variable (P : RankedProcess S Ω) + +/-- Total probability assigned to strict progress at the current state. -/ +def progressMass (s : S) : ℝ := + ∑ o, if P.rank (P.next s o) < P.rank s then P.weight s o else 0 + +/-- Probability of positive rank after the given number of rounds, defined +by the finite probability tree. Each recursive layer is one fresh kernel draw. -/ +def failureProbability : ℕ → S → ℝ + | 0, s => if P.rank s = 0 then 0 else 1 + | t + 1, s => ∑ o, P.weight s o * failureProbability t (P.next s o) + +theorem failure_probability_nonneg (t : ℕ) (s : S) : + 0 ≤ P.failureProbability t s := by + induction t generalizing s with + | zero => simp only [failureProbability]; split_ifs <;> norm_num + | succ t ih => + exact Finset.sum_nonneg fun o _ => mul_nonneg (P.weight_nonneg s o) (ih _) + +theorem failure_probability_le_one (t : ℕ) (s : S) : + P.failureProbability t s ≤ 1 := by + induction t generalizing s with + | zero => simp only [failureProbability]; split_ifs <;> norm_num + | succ t ih => + calc + P.failureProbability (t + 1) s = + ∑ o, P.weight s o * P.failureProbability t (P.next s o) := rfl + _ ≤ ∑ o, P.weight s o * 1 := Finset.sum_le_sum fun o _ => + mul_le_mul_of_nonneg_left (ih _) (P.weight_nonneg s o) + _ = 1 := by simp [P.weight_sum] + +/-- Rank zero is absorbing, so positive rank after `t` rounds is equivalent +to not having reached rank zero earlier. -/ +theorem failure_probability_of_rank_zero (t : ℕ) (s : S) (hs : P.rank s = 0) : + P.failureProbability t s = 0 := by + induction t generalizing s with + | zero => simp [failureProbability, hs] + | succ t ih => + have hnext : ∀ o, P.rank (P.next s o) = 0 := fun o => by + have hm := P.rank_mono s o + omega + simp [failureProbability, ih _ (hnext _)] + +/-- A per-node strict-progress mass bound gives a one-step contraction +of the killed potential, including at the terminal states. -/ +theorem potential_drift (p : ℝ) + (hprogress : ∀ s, 0 < P.rank s → p ≤ P.progressMass s) (s : S) : + (∑ o, P.weight s o * potential (P.rank (P.next s o))) ≤ + (1 - p / 2) * potential (P.rank s) := by + by_cases hs : P.rank s = 0 + · have hnext : ∀ o, P.rank (P.next s o) = 0 := fun o => by + have hm := P.rank_mono s o + omega + simp [hs, hnext] + have hpoint (o : Ω) : + P.weight s o * potential (P.rank (P.next s o)) ≤ + P.weight s o * potential (P.rank s) - + (if P.rank (P.next s o) < P.rank s then P.weight s o else 0) * + potential (P.rank s) / 2 := by + split_ifs with hlt + · have hh := mul_le_mul_of_nonneg_left (potential_le_half_of_lt hlt) + (P.weight_nonneg s o) + linarith + · simpa using mul_le_mul_of_nonneg_left (potential_mono (P.rank_mono s o)) + (P.weight_nonneg s o) + calc + _ ≤ ∑ o, (P.weight s o * potential (P.rank s) - + (if P.rank (P.next s o) < P.rank s then P.weight s o else 0) * + potential (P.rank s) / 2) := Finset.sum_le_sum fun o _ => hpoint o + _ = potential (P.rank s) - P.progressMass s * potential (P.rank s) / 2 := by + simp only [Finset.sum_sub_distrib, ← Finset.sum_div, ← Finset.sum_mul, + P.weight_sum, one_mul, progressMass] + _ ≤ (1 - p / 2) * potential (P.rank s) := by + have hh := mul_le_mul_of_nonneg_right (hprogress s (by omega)) + (potential_nonneg (P.rank s)) + nlinarith + +/-- Finite adaptive-tree tail bound. The success assumption is checked at +every reachable or unreachable state of the supplied process, so it applies +uniformly to states encoding arbitrary previous histories. -/ +theorem failure_probability_le_potential (p : ℝ) (hp : p ≤ 2) + (hprogress : ∀ s, 0 < P.rank s → p ≤ P.progressMass s) + (t : ℕ) (s : S) : + P.failureProbability t s ≤ (1 - p / 2) ^ t * potential (P.rank s) := by + have hq : 0 ≤ 1 - p / 2 := by linarith + induction t generalizing s with + | zero => + by_cases hs : P.rank s = 0 + · simp [failureProbability, potential, hs] + · simpa [failureProbability, potential, hs] using + (one_le_pow₀ (by norm_num : (1 : ℝ) ≤ 2) : (1 : ℝ) ≤ 2 ^ P.rank s) + | succ t ih => + calc + P.failureProbability (t + 1) s = + ∑ o, P.weight s o * P.failureProbability t (P.next s o) := rfl + _ ≤ ∑ o, P.weight s o * ((1 - p / 2) ^ t * potential (P.rank (P.next s o))) := + Finset.sum_le_sum fun o _ => mul_le_mul_of_nonneg_left (ih _) (P.weight_nonneg s o) + _ = (1 - p / 2) ^ t * ∑ o, P.weight s o * potential (P.rank (P.next s o)) := by + rw [Finset.mul_sum] + apply Finset.sum_congr rfl + intro o _ + ring + _ ≤ (1 - p / 2) ^ t * ((1 - p / 2) * potential (P.rank s)) := + mul_le_mul_of_nonneg_left (P.potential_drift p hprogress s) (pow_nonneg hq t) + _ = (1 - p / 2) ^ (t + 1) * potential (P.rank s) := by rw [pow_succ]; ring + +/-- A simpler tail bound using only an upper bound on the initial rank. -/ +theorem failure_probability_le (p : ℝ) (hp : p ≤ 2) + (hprogress : ∀ s, 0 < P.rank s → p ≤ P.progressMass s) + (t n : ℕ) (s : S) (hrank : P.rank s ≤ n) : + P.failureProbability t s ≤ (2 : ℝ) ^ n * (1 - p / 2) ^ t := by + have hq : 0 ≤ 1 - p / 2 := by linarith + have hpow : potential (P.rank s) ≤ (2 : ℝ) ^ n := + (potential_le_pow _).trans (pow_le_pow_right₀ (by norm_num) hrank) + calc + _ ≤ (1 - p / 2) ^ t * potential (P.rank s) := + P.failure_probability_le_potential p hp hprogress t s + _ ≤ (1 - p / 2) ^ t * (2 : ℝ) ^ n := mul_le_mul_of_nonneg_left hpow (pow_nonneg hq t) + _ = _ := by ring + +/-- If each nonterminal state progresses with probability at least one +quarter, failure after `t` rounds is at most `2^n (7/8)^t`. -/ +theorem failure_probability_le_seven_eighths + (hprogress : ∀ s, 0 < P.rank s → (1 / 4 : ℝ) ≤ P.progressMass s) + (t n : ℕ) (s : S) (hrank : P.rank s ≤ n) : + P.failureProbability t s ≤ (2 : ℝ) ^ n * (7 / 8 : ℝ) ^ t := by + convert P.failure_probability_le (1 / 4) (by norm_num) hprogress t n s hrank using 1 + norm_num + +/-- A concrete confidence budget: `8(n+k)` rounds give failure probability +at most `2^(-k)` under the quarter-progress hypothesis. This is deliberately +coarser than the paper's sharp geometric-sum estimate. -/ +theorem failure_probability_eight_rounds_per_bit + (hprogress : ∀ s, 0 < P.rank s → (1 / 4 : ℝ) ≤ P.progressMass s) + (n k : ℕ) (s : S) (hrank : P.rank s ≤ n) : + P.failureProbability (8 * (n + k)) s ≤ (1 / 2 : ℝ) ^ k := by + have hblock : (7 / 8 : ℝ) ^ 8 ≤ 1 / 2 := by norm_num + have hp : (7 / 8 : ℝ) ^ (8 * (n + k)) ≤ (1 / 2 : ℝ) ^ (n + k) := by + rw [pow_mul] + exact pow_le_pow_left₀ (by positivity) hblock _ + calc + _ ≤ (2 : ℝ) ^ n * (7 / 8 : ℝ) ^ (8 * (n + k)) := + P.failure_probability_le_seven_eighths hprogress _ n s hrank + _ ≤ (2 : ℝ) ^ n * (1 / 2 : ℝ) ^ (n + k) := + mul_le_mul_of_nonneg_left hp (by positivity) + _ = (1 / 2 : ℝ) ^ k := by + rw [pow_add, ← mul_assoc, ← mul_pow] + norm_num + +end RankedProcess + +end LeanPool.SingleCopyStabilizer.AdaptiveProcess diff --git a/LeanPool/SingleCopyStabilizer/CNOTAction.lean b/LeanPool/SingleCopyStabilizer/CNOTAction.lean new file mode 100644 index 0000000000..38cd237e78 --- /dev/null +++ b/LeanPool/SingleCopyStabilizer/CNOTAction.lean @@ -0,0 +1,98 @@ +/- +Copyright (c) 2026 Antonio Anna Mele. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Antonio Anna Mele +-/ +module + +public import LeanPool.SingleCopyStabilizer.Symplectic +public import LeanPool.SingleCopyStabilizer.Measurement + + +/-! Arbitrary-qubit simultaneous CNOT action and its exact Pauli covariance. +The basis permutation is `x ↦ x - xᵢ w`, with `wᵢ=0`; over F₂ this is the +product of CNOTs controlled by i and targeted at the support of w. -/ + +@[expose] public section + +noncomputable section + + +namespace LeanPool.SingleCopyStabilizer.CNOTAction + +open Measurement + +variable {ι : Type*} [Fintype ι] [DecidableEq ι] + +/-- The invertible coordinate shear underlying simultaneous controlled-NOT gates. -/ +def basisShear (i : ι) (w : Bits ι) (hw : w i = 0) : Bits ι ≃ₗ[ZMod 2] Bits ι where + toFun := shearX i w + invFun x := x + x i • w + left_inv x := by + ext j + simp [shearX, hw] + right_inv x := by + ext j + simp [shearX, hw] + map_add' x y := by + ext j + simp [shearX, add_smul] + ring + map_smul' c x := by + ext j + simp [shearX] + ring + +/-- Pull amplitudes back along the inverse controlled shear. -/ +def applyCNOTs (i : ι) (w : Bits ι) (hw : w i = 0) + (ψ : Amplitude ι) : Amplitude ι := fun x => ψ ((basisShear i w hw).symm x) + +theorem norm_preserved (i : ι) (w : Bits ι) (hw : w i = 0) (ψ : Amplitude ι) : + (∑ x, bornWeight (applyCNOTs i w hw ψ) x) = ∑ x, bornWeight ψ x := by + exact Fintype.sum_equiv (basisShear i w hw).symm.toEquiv _ _ (fun _ => rfl) + +theorem normalized (i : ι) (w : Bits ι) (hw : w i = 0) (ψ : Amplitude ι) + (hψ : IsNormalized ψ) : IsNormalized (applyCNOTs i w hw ψ) := by + unfold IsNormalized + rw [norm_preserved] + exact hψ + +theorem inverse_pairing (i : ι) (w : Bits ι) (hw : w i = 0) (v x : Bits ι) : + shearZ i w v ⬝ᵥ x = v ⬝ᵥ (basisShear i w hw).symm x := by + have h := shear_pairing i hw ((basisShear i w hw).symm x) v + change ((basisShear i w hw) ((basisShear i w hw).symm x)) ⬝ᵥ shearZ i w v = _ at h + rw [LinearEquiv.apply_symm_apply] at h + simpa only [dotProduct_comm] using h + +/-- Exact covariance of the concrete basis-permutation action. -/ +theorem pauli_covariance (i : ι) (w : Bits ι) (hw : w i = 0) + (u v : Bits ι) (ψ : Amplitude ι) : + pauliAction (shearX i w u) (shearZ i w v) (applyCNOTs i w hw ψ) = + applyCNOTs i w hw (pauliAction u v ψ) := by + funext x + have hpre : (basisShear i w hw).symm (x - shearX i w u) = + (basisShear i w hw).symm x - u := by + change (basisShear i w hw).symm (x - (basisShear i w hw) u) = _ + rw [map_sub, LinearEquiv.symm_apply_apply] + have hsign := inverse_pairing i w hw v (x - shearX i w u) + rw [hpre] at hsign + simp only [pauliAction, applyCNOTs, hpre, hsign] + +/-- Every Pauli eigenlabel is transported by the shear used in the paper. -/ +theorem transports_eigenvector (i : ι) (w : Bits ι) (hw : w i = 0) + (ψ : Amplitude ι) (u v : Bits ι) (ζ : ℂ) + (heig : IsPauliEigenvector ψ u v ζ) : + IsPauliEigenvector (applyCNOTs i w hw ψ) (shearX i w u) (shearZ i w v) ζ := by + intro x + rw [congrFun (pauli_covariance i w hw u v ψ) x] + exact heig ((basisShear i w hw).symm x) + +omit [DecidableEq ι] [Fintype ι] in +/-- Explicit two-sided inverse, needed when the learned circuit is undone. -/ +theorem inverse_action (i : ι) (w : Bits ι) (hw : w i = 0) (ψ : Amplitude ι) : + (fun x => applyCNOTs i w hw ψ ((basisShear i w hw) x)) = ψ := by + classical + funext x + simp [applyCNOTs] + +end LeanPool.SingleCopyStabilizer.CNOTAction diff --git a/LeanPool/SingleCopyStabilizer/Circuit.lean b/LeanPool/SingleCopyStabilizer/Circuit.lean new file mode 100644 index 0000000000..300983a450 --- /dev/null +++ b/LeanPool/SingleCopyStabilizer/Circuit.lean @@ -0,0 +1,247 @@ +/- +Copyright (c) 2026 Antonio Anna Mele. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Antonio Anna Mele +-/ +module + +public import LeanPool.SingleCopyStabilizer.CNOTAction +public import LeanPool.SingleCopyStabilizer.CliffordAction +public import LeanPool.SingleCopyStabilizer.Round + + +/-! +# Recorded binary Clifford circuits and exact decoding + +Each recorded outcome specifies precisely the CNOTs and correction used by +one learning round. Lists are chronological: the head is performed first. +The inverse acts on the final computational basis vector to reconstruct the +original amplitude, with its physically irrelevant global phase explicit. +-/ + +@[expose] public section + +noncomputable section + + +namespace LeanPool.SingleCopyStabilizer.Circuit + +open Measurement CNOTAction CliffordAction + +variable {ι : Type*} [Fintype ι] [DecidableEq ι] + +/-- The simultaneous CNOT operation, with its explicit inverse permutation. -/ +def cnotEquiv (i : ι) (w : Bits ι) (hw : w i = 0) : + Amplitude ι ≃ₗ[ℂ] Amplitude ι where + toFun := applyCNOTs i w hw + invFun ψ x := ψ (basisShear i w hw x) + left_inv ψ := inverse_action i w hw ψ + right_inv ψ := by + funext x + simp [applyCNOTs] + map_add' ψ φ := rfl + map_smul' c ψ := rfl + +omit [DecidableEq ι] [Fintype ι] in +@[simp] theorem cnotEquiv_apply (i : ι) (w : Bits ι) (hw : w i = 0) + (ψ : Amplitude ι) : cnotEquiv i w hw ψ = applyCNOTs i w hw ψ := rfl + +omit [DecidableEq ι] [Fintype ι] in +@[simp] theorem cnotEquiv_symm_apply (i : ι) (w : Bits ι) (hw : w i = 0) + (ψ : Amplitude ι) : + (cnotEquiv i w hw).symm ψ = fun x => ψ (basisShear i w hw x) := rfl + +/-- The correction is H for bit zero and HS for bit one. -/ +def correctionEquiv (i : ι) (b : ZMod 2) : Amplitude ι ≃ₗ[ℂ] Amplitude ι := + if b = 0 then localHadamardLinearEquiv i + else (localPhaseLinearEquiv i).trans (localHadamardLinearEquiv i) + +omit [Fintype ι] in +theorem correctionEquiv_apply (i : ι) (b : ZMod 2) (ψ : Amplitude ι) : + correctionEquiv i b ψ = + localHadamard i (if b = 0 then ψ else localPhase i ψ) := by + classical + by_cases hb : b = 0 <;> simp [correctionEquiv, hb, + localHadamardLinearEquiv, localHadamardEquiv, + localPhaseLinearEquiv, localPhaseEquiv] + +theorem correctionEquiv_normalized (i : ι) (b : ZMod 2) (ψ : Amplitude ι) + (hψ : IsNormalized ψ) : IsNormalized (correctionEquiv i b ψ) := by + rw [correctionEquiv_apply] + apply localHadamard_normalized + by_cases hb : b = 0 + · simpa only [ite_eq_left hb] using hψ + · simpa only [ite_eq_right hb] using localPhase_normalized i ψ hψ + +theorem correctionEquiv_norm_preserving (i : ι) (b : ZMod 2) (ψ : Amplitude ι) : + (∑ x, bornWeight (correctionEquiv i b ψ) x) = ∑ x, bornWeight ψ x := by + rw [correctionEquiv_apply, localHadamard_norm_preserving] + by_cases hb : b = 0 + · simp only [ite_eq_left hb] + · simp only [ite_eq_right hb, localPhase_bornWeight] + +omit [Fintype ι] in +/-- The pivot-coordinate vanishes in the CNOT target vector. -/ +theorem pivot_target_zero (u : Bits ι) (hu : u ≠ 0) : + (u - (Pi.single (binaryPivot u hu) 1 : Bits ι)) (binaryPivot u hu) = 0 := by + classical + simp [binaryPivot_spec] + +/-- The physical Clifford operation determined by the sampled difference +and the correction coin. A zero difference records the identity operation. -/ +def roundEquiv (u : Bits ι) (b : ZMod 2) : Amplitude ι ≃ₗ[ℂ] Amplitude ι := + if hu : u = 0 then LinearEquiv.refl ℂ (Amplitude ι) + else (cnotEquiv (binaryPivot u hu) (u - Pi.single (binaryPivot u hu) 1) + (pivot_target_zero u hu)).trans (correctionEquiv (binaryPivot u hu) b) + +@[simp] theorem roundEquiv_zero (b : ZMod 2) : + roundEquiv (0 : Bits ι) b = LinearEquiv.refl ℂ (Amplitude ι) := by + simp [roundEquiv] + +theorem roundEquiv_apply_of_ne (u : Bits ι) (b : ZMod 2) (hu : u ≠ 0) + (ψ : Amplitude ι) : + roundEquiv u b ψ = correctionEquiv (binaryPivot u hu) b + (applyCNOTs (binaryPivot u hu) (u - Pi.single (binaryPivot u hu) 1) + (pivot_target_zero u hu) ψ) := by + simp [roundEquiv, hu] + +theorem roundEquiv_normalized (u : Bits ι) (b : ZMod 2) (ψ : Amplitude ι) + (hψ : IsNormalized ψ) : IsNormalized (roundEquiv u b ψ) := by + by_cases hu : u = 0 + · subst u + simpa using hψ + · rw [roundEquiv_apply_of_ne u b hu] + exact correctionEquiv_normalized _ b _ (CNOTAction.normalized _ _ _ ψ hψ) + +theorem roundEquiv_norm_preserving (u : Bits ι) (b : ZMod 2) (ψ : Amplitude ι) : + (∑ x, bornWeight (roundEquiv u b ψ) x) = ∑ x, bornWeight ψ x := by + by_cases hu : u = 0 + · subst u + simp + · rw [roundEquiv_apply_of_ne u b hu, correctionEquiv_norm_preserving, + CNOTAction.norm_preserved] + +/-- A recorded outcome is sufficient to specify all gates in a round. -/ +abbrev Outcome (ι : Type*) := Bits ι × ZMod 2 + +/-- Circuit composition in chronological order. -/ +def circuitEquiv : List (Outcome ι) → (Amplitude ι ≃ₗ[ℂ] Amplitude ι) + | [] => LinearEquiv.refl ℂ (Amplitude ι) + | op :: ops => (roundEquiv op.1 op.2).trans (circuitEquiv ops) + +@[simp] theorem circuitEquiv_nil : + circuitEquiv ([] : List (Outcome ι)) = LinearEquiv.refl ℂ (Amplitude ι) := rfl + +@[simp] theorem circuitEquiv_cons (op : Outcome ι) (ops : List (Outcome ι)) : + circuitEquiv (op :: ops) = (roundEquiv op.1 op.2).trans (circuitEquiv ops) := rfl + +@[simp] theorem circuitEquiv_cons_apply (op : Outcome ι) (ops : List (Outcome ι)) + (ψ : Amplitude ι) : + circuitEquiv (op :: ops) ψ = circuitEquiv ops (roundEquiv op.1 op.2 ψ) := rfl + +theorem circuitEquiv_append (xs ys : List (Outcome ι)) : + circuitEquiv (xs ++ ys) = (circuitEquiv xs).trans (circuitEquiv ys) := by + induction xs with + | nil => rfl + | cons op ops ih => + ext ψ x + simp only [List.cons_append, circuitEquiv_cons, ih, LinearEquiv.trans_apply] + +theorem circuitEquiv_normalized (ops : List (Outcome ι)) (ψ : Amplitude ι) + (hψ : IsNormalized ψ) : IsNormalized (circuitEquiv ops ψ) := by + induction ops generalizing ψ with + | nil => exact hψ + | cons op ops ih => + exact ih _ (roundEquiv_normalized op.1 op.2 ψ hψ) + +theorem circuitEquiv_norm_preserving (ops : List (Outcome ι)) (ψ : Amplitude ι) : + (∑ x, bornWeight (circuitEquiv ops ψ) x) = ∑ x, bornWeight ψ x := by + induction ops generalizing ψ with + | nil => rfl + | cons op ops ih => + rw [circuitEquiv_cons_apply, ih, roundEquiv_norm_preserving] + +theorem circuitEquiv_symm_normalized (ops : List (Outcome ι)) (ψ : Amplitude ι) + (hψ : IsNormalized ψ) : IsNormalized ((circuitEquiv ops).symm ψ) := by + unfold IsNormalized + rw [← circuitEquiv_norm_preserving ops, LinearEquiv.apply_symm_apply] + exact hψ + +/-- Computational basis amplitudes, with value one at the chosen string. -/ +def basis (z : Bits ι) : Amplitude ι := Pi.single z 1 + +omit [DecidableEq ι] in +@[simp] theorem basis_apply (z x : Bits ι) : + basis z x = if x = z then 1 else 0 := by + classical + simp [basis, Pi.single_apply, eq_comm] + +theorem basis_normalized (z : Bits ι) : IsNormalized (basis z) := by + simp [IsNormalized, bornWeight, basis_apply] + +/-- Classical description of the learned state: undo the recorded circuit +on the final measured basis string. -/ +def decode (ops : List (Outcome ι)) (z : Bits ι) : Amplitude ι := + (circuitEquiv ops).symm (basis z) + +@[simp] theorem decode_nil (z : Bits ι) : decode [] z = basis z := rfl + +@[simp] theorem decode_cons (op : Outcome ι) (ops : List (Outcome ι)) (z : Bits ι) : + decode (op :: ops) z = (roundEquiv op.1 op.2).symm (decode ops z) := rfl + +theorem decode_append (xs ys : List (Outcome ι)) (z : Bits ι) : + decode (xs ++ ys) z = (circuitEquiv xs).symm (decode ys z) := by + simp only [decode, circuitEquiv_append, LinearEquiv.trans_symm, + LinearEquiv.trans_apply] + +@[simp] theorem circuitEquiv_decode (ops : List (Outcome ι)) (z : Bits ι) : + circuitEquiv ops (decode ops z) = basis z := + LinearEquiv.apply_symm_apply _ _ + +theorem decode_normalized (ops : List (Outcome ι)) (z : Bits ι) : + IsNormalized (decode ops z) := + circuitEquiv_symm_normalized ops _ (basis_normalized z) + +/-- Inverting the recorded circuit recovers the original amplitude with the +same global phase as its final computational basis amplitude. -/ +theorem reconstruction_eq_smul_decode (ops : List (Outcome ι)) + (ψ : Amplitude ι) (z : Bits ι) (c : ℂ) + (h : circuitEquiv ops ψ = c • basis z) : ψ = c • decode ops z := by + apply (circuitEquiv ops).injective + simpa only [map_smul, circuitEquiv_decode] using h + +omit [DecidableEq ι] in +theorem smul_basis (z : Bits ι) (c : ℂ) : + c • basis z = fun x => if x = z then c else 0 := by + classical + funext x + by_cases hx : x = z <;> simp [hx] + +/-- Version matching `StabilizerState.full_diagonal_basis_amplitude`. -/ +theorem reconstruction_of_basis_amplitude (ops : List (Outcome ι)) + (ψ : Amplitude ι) (z : Bits ι) (c : ℂ) + (h : circuitEquiv ops ψ = fun x => if x = z then c else 0) : + ψ = c • decode ops z := by + apply reconstruction_eq_smul_decode ops ψ z c + simpa only [smul_basis] using h + +/-- If the input is normalized, the scalar occurring at a basis-vector +endpoint must have unit modulus. -/ +theorem reconstruction_phase_normSq (ops : List (Outcome ι)) (ψ : Amplitude ι) + (hψ : IsNormalized ψ) (z : Bits ι) (c : ℂ) + (h : circuitEquiv ops ψ = c • basis z) : Complex.normSq c = 1 := by + have hn := circuitEquiv_normalized ops ψ hψ + rw [h, smul_basis] at hn + simpa [IsNormalized, bornWeight, apply_ite] using hn + +/-- The circuit endpoint condition and exact recovery up to a specified +global phase are equivalent. -/ +theorem reconstruction_iff (ops : List (Outcome ι)) (ψ : Amplitude ι) + (z : Bits ι) (c : ℂ) : + circuitEquiv ops ψ = c • basis z ↔ ψ = c • decode ops z := by + constructor + · exact reconstruction_eq_smul_decode ops ψ z c + · intro h + rw [h, map_smul, circuitEquiv_decode] + +end LeanPool.SingleCopyStabilizer.Circuit diff --git a/LeanPool/SingleCopyStabilizer/CliffordAction.lean b/LeanPool/SingleCopyStabilizer/CliffordAction.lean new file mode 100644 index 0000000000..569b051559 --- /dev/null +++ b/LeanPool/SingleCopyStabilizer/CliffordAction.lean @@ -0,0 +1,328 @@ +/- +Copyright (c) 2026 Antonio Anna Mele. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Antonio Anna Mele +-/ +module + +public import LeanPool.SingleCopyStabilizer.Measurement +public import LeanPool.SingleCopyStabilizer.HadamardCoefficient + + +/-! Actual arbitrary-qubit local phase and Hadamard actions on amplitudes. -/ + +@[expose] public section + + +noncomputable section + +namespace LeanPool.SingleCopyStabilizer.CliffordAction + +open Measurement +open scoped BigOperators CharTwo + +variable {ι : Type*} [Fintype ι] [DecidableEq ι] + +/-- Every residue modulo two is zero or one. -/ +theorem bit_eq_zero_or_one (a : ZMod 2) : a = 0 ∨ a = 1 := by + -- Exhaust the two canonical residues in the kernel. + revert a + decide + +theorem paritySign_add (a b : ZMod 2) : + paritySign (a + b) = paritySign a * paritySign b := by + rcases bit_eq_zero_or_one a with rfl | rfl <;> + rcases bit_eq_zero_or_one b with rfl | rfl <;> + norm_num [paritySign, CharTwo.add_self_eq_zero] + all_goals decide + +theorem paritySign_mul_self (a : ZMod 2) : paritySign a * paritySign a = 1 := by + rcases bit_eq_zero_or_one a with rfl | rfl <;> norm_num [paritySign, CharTwo.add_self_eq_zero] + +/-- Scalar phase contributed by a computational-basis bit under an S gate. -/ +def phaseBit (a : ZMod 2) : ℂ := if a = 0 then 1 else Complex.I + +@[simp] theorem phaseBit_normSq (a : ZMod 2) : Complex.normSq (phaseBit a) = 1 := by + rcases bit_eq_zero_or_one a with rfl | rfl <;> norm_num [phaseBit] + +theorem phaseBit_twist (a x : ZMod 2) : + paritySign (a * (x - a)) * phaseBit (x - a) = + star (phaseBit a) * phaseBit x := by + rcases bit_eq_zero_or_one a with rfl | rfl <;> + rcases bit_eq_zero_or_one x with rfl | rfl <;> norm_num [paritySign, phaseBit] + +omit [Fintype ι] in +theorem update_sub (x u : Bits ι) (i : ι) (b : ZMod 2) : + Function.update x i b - u = Function.update (x - u) i (b - u i) := by + classical + funext j + by_cases hj : j = i + · subst j + simp + · simp [hj] + +omit [Fintype ι] in +theorem sub_update (x u : Bits ι) (i : ι) (b : ZMod 2) : + x - Function.update u i b = Function.update (x - u) i (x i - b) := by + classical + funext j + by_cases hj : j = i + · subst j + simp + · simp [hj] + +omit [Fintype ι] in +theorem update_as_add_single (x : Bits ι) (i : ι) (b : ZMod 2) : + Function.update x i b = x + (b - x i) • (Pi.single i 1 : Bits ι) := by + classical + funext j + by_cases hj : j = i + · subst j + simp [add_left_comm] + · simp [hj] + +theorem dot_update_left (u v : Bits ι) (i : ι) (b : ZMod 2) : + Function.update u i b ⬝ᵥ v = u ⬝ᵥ v + (b - u i) * v i := by + rw [update_as_add_single] + simp + +theorem dot_update_right (u v : Bits ι) (i : ι) (b : ZMod 2) : + u ⬝ᵥ Function.update v i b = u ⬝ᵥ v + u i * (b - v i) := by + rw [update_as_add_single] + simp [mul_comm] + +/-- Apply S at one site of the full register amplitude. -/ +def localPhase (i : ι) (ψ : Amplitude ι) (x : Bits ι) : ℂ := + phaseBit (x i) * ψ x + +/-- The Z-label update under conjugation by a local S gate. -/ +def phaseZLabel (i : ι) (u v : Bits ι) : Bits ι := + v + u i • (Pi.single i 1 : Bits ι) + +omit [DecidableEq ι] [Fintype ι] in +theorem localPhase_bornWeight (i : ι) (ψ : Amplitude ι) (x : Bits ι) : + bornWeight (localPhase i ψ) x = bornWeight ψ x := by + classical + simp [bornWeight, localPhase, Complex.normSq_mul] + +theorem localPhase_normalized (i : ι) (ψ : Amplitude ι) (hψ : IsNormalized ψ) : + IsNormalized (localPhase i ψ) := by + simpa only [IsNormalized, localPhase_bornWeight] using hψ + +theorem localPhase_covariance (i : ι) (u v : Bits ι) (ψ : Amplitude ι) (x : Bits ι) : + pauliAction u (phaseZLabel i u v) (localPhase i ψ) x = + star (phaseBit (u i)) * localPhase i (pauliAction u v ψ) x := by + unfold pauliAction localPhase phaseZLabel + simp only [add_dotProduct, smul_dotProduct, single_dotProduct, Pi.sub_apply, + smul_eq_mul, one_mul, paritySign_add] + calc + paritySign (v ⬝ᵥ (x - u)) * paritySign (u i * (x i - u i)) * + (phaseBit (x i - u i) * ψ (x - u)) = + (paritySign (u i * (x i - u i)) * phaseBit (x i - u i)) * + (paritySign (v ⬝ᵥ (x - u)) * ψ (x - u)) := by ring + _ = _ := by rw [phaseBit_twist]; ring + +theorem localPhase_eigenvector (i : ι) (ψ : Amplitude ι) (u v : Bits ι) (ζ : ℂ) + (heig : IsPauliEigenvector ψ u v ζ) : + IsPauliEigenvector (localPhase i ψ) u (phaseZLabel i u v) + (star (phaseBit (u i)) * ζ) := by + intro x + rw [localPhase_covariance] + unfold localPhase + rw [heig x] + ring + +/-- Apply H at one site through its two-term amplitude formula. -/ +def localHadamard (i : ι) (ψ : Amplitude ι) (x : Bits ι) : ℂ := + QubitGates.hadamardCoefficient * + (ψ (Function.update x i 0) + paritySign (x i) * ψ (Function.update x i 1)) + +/-- Replace the selected X label by its old Z label. -/ +def hadamardXLabel (i : ι) (u v : Bits ι) : Bits ι := Function.update u i (v i) +/-- Replace the selected Z label by its old X label. -/ +def hadamardZLabel (i : ι) (u v : Bits ι) : Bits ι := Function.update v i (u i) + +theorem localHadamard_covariance (i : ι) (u v : Bits ι) (ψ : Amplitude ι) + (x : Bits ι) : + pauliAction (hadamardXLabel i u v) (hadamardZLabel i u v) + (localHadamard i ψ) x = + paritySign (u i * v i) * localHadamard i (pauliAction u v ψ) x := by + simp only [pauliAction, localHadamard, hadamardXLabel, hadamardZLabel, + sub_update, update_sub, dot_update_left, dot_update_right, + Function.update_self, Function.update_idem, Pi.sub_apply] + simp only [paritySign_add] + generalize ha : u i = a + generalize hb : v i = b + generalize hc : x i = c + rcases bit_eq_zero_or_one a with rfl | rfl <;> + rcases bit_eq_zero_or_one b with rfl | rfl <;> + rcases bit_eq_zero_or_one c with rfl | rfl <;> + norm_num [paritySign, CharTwo.add_self_eq_zero] <;> split_ifs <;> + try simp only [CharTwo.neg_eq] + all_goals ring + +theorem localHadamard_eigenvector (i : ι) (ψ : Amplitude ι) (u v : Bits ι) (ζ : ℂ) + (heig : IsPauliEigenvector ψ u v ζ) : + IsPauliEigenvector (localHadamard i ψ) (hadamardXLabel i u v) + (hadamardZLabel i u v) (paritySign (u i * v i) * ζ) := by + intro x + rw [localHadamard_covariance] + unfold localHadamard + rw [heig (Function.update x i 0), heig (Function.update x i 1)] + ring + +theorem hadamardCoefficient_normSq : + Complex.normSq QubitGates.hadamardCoefficient = 1 / 2 := by + rw [QubitGates.hadamardCoefficient, Complex.normSq_ofReal, + Real.mul_self_sqrt (by norm_num : (0 : ℝ) ≤ 1 / 2)] + +theorem hadamard_pair_norm (a b : ℂ) : + Complex.normSq (QubitGates.hadamardCoefficient * (a + b)) + + Complex.normSq (QubitGates.hadamardCoefficient * (a - b)) = + Complex.normSq a + Complex.normSq b := by + simp only [Complex.normSq_mul, hadamardCoefficient_normSq] + simp only [Complex.normSq_apply, Complex.add_re, Complex.add_im, Complex.sub_re, + Complex.sub_im] + ring + +omit [Fintype ι] in +theorem localHadamard_pair_bornWeight (i : ι) (ψ : Amplitude ι) (x : Bits ι) : + bornWeight (localHadamard i ψ) (Function.update x i 0) + + bornWeight (localHadamard i ψ) (Function.update x i 1) = + bornWeight ψ (Function.update x i 0) + bornWeight ψ (Function.update x i 1) := by + classical + simpa [bornWeight, localHadamard, paritySign, sub_eq_add_neg] using + hadamard_pair_norm (ψ (Function.update x i 0)) (ψ (Function.update x i 1)) + + +omit [Fintype ι] in +theorem flip_eq_update (i : ι) (x : Bits ι) : + x + (Pi.single i 1 : Bits ι) = Function.update x i (x i + 1) := by + classical + funext j + by_cases hj : j = i + · subst j + simp + · simp [hj] + +theorem sum_update_pair (i : ι) (f : Bits ι → ℝ) : + (∑ x, (f (Function.update x i 0) + f (Function.update x i 1))) = + 2 * ∑ x, f x := by + have hpair (x : Bits ι) : + f (Function.update x i 0) + f (Function.update x i 1) = + f x + f (x + (Pi.single i 1 : Bits ι)) := by + have hfix : Function.update x i (x i) = x := Function.update_eq_self i x + rcases bit_eq_zero_or_one (x i) with hx | hx + · have h0 : Function.update x i 0 = x := by simpa only [hx] using hfix + rw [flip_eq_update, hx] + norm_num + rw [h0] + · have h1 : Function.update x i 1 = x := by simpa only [hx] using hfix + rw [flip_eq_update, hx, show (1 + 1 : ZMod 2) = 0 by decide, h1, add_comm] + have hflip : (∑ x, f (x + (Pi.single i 1 : Bits ι))) = ∑ x, f x := + Fintype.sum_equiv (Equiv.addRight (Pi.single i 1 : Bits ι)) _ _ (fun _ => rfl) + simp_rw [hpair] + rw [Finset.sum_add_distrib, hflip] + ring + +theorem localHadamard_norm_preserving (i : ι) (ψ : Amplitude ι) : + (∑ x, bornWeight (localHadamard i ψ) x) = ∑ x, bornWeight ψ x := by + have h := Finset.sum_congr (s₁ := (Finset.univ : Finset (Bits ι))) rfl + (fun x _ => localHadamard_pair_bornWeight i ψ x) + rw [sum_update_pair, sum_update_pair] at h + linarith + +theorem localHadamard_normalized (i : ι) (ψ : Amplitude ι) (hψ : IsNormalized ψ) : + IsNormalized (localHadamard i ψ) := by + unfold IsNormalized + rw [localHadamard_norm_preserving] + exact hψ + +/-- The adjoint S action on amplitudes. -/ +def localPhaseInverse (i : ι) (ψ : Amplitude ι) (x : Bits ι) : ℂ := + star (phaseBit (x i)) * ψ x + +theorem phaseBit_star_mul (a : ZMod 2) : star (phaseBit a) * phaseBit a = 1 := by + rcases bit_eq_zero_or_one a with rfl | rfl <;> norm_num [phaseBit] + +omit [DecidableEq ι] [Fintype ι] in +theorem localPhaseInverse_localPhase (i : ι) (ψ : Amplitude ι) : + localPhaseInverse i (localPhase i ψ) = ψ := by + classical + funext x + simp only [localPhaseInverse, localPhase, ← mul_assoc, phaseBit_star_mul, one_mul] + +omit [DecidableEq ι] [Fintype ι] in +theorem localPhase_localPhaseInverse (i : ι) (ψ : Amplitude ι) : + localPhase i (localPhaseInverse i ψ) = ψ := by + classical + funext x + unfold localPhase localPhaseInverse + rw [← mul_assoc, mul_comm (phaseBit _), phaseBit_star_mul, one_mul] + +omit [Fintype ι] in +theorem localHadamard_involutive (i : ι) (ψ : Amplitude ι) : + localHadamard i (localHadamard i ψ) = ψ := by + classical + have ht : QubitGates.hadamardCoefficient ^ 2 = (1 / 2 : ℂ) := by + simpa only [pow_two] using QubitGates.hadamardCoefficient_mul + funext x + have hfix : Function.update x i (x i) = x := Function.update_eq_self i x + rcases bit_eq_zero_or_one (x i) with hx | hx + · have h0 : Function.update x i 0 = x := by simpa only [hx] using hfix + simp only [localHadamard, Function.update_self, Function.update_idem, + hx, paritySign] + norm_num + rw [h0] + ring_nf + rw [ht] + ring + · have h1 : Function.update x i 1 = x := by simpa only [hx] using hfix + simp only [localHadamard, Function.update_self, Function.update_idem, + hx, paritySign] + norm_num + rw [h1] + ring_nf + rw [ht] + ring + +/-- H is a bijection on the full amplitude space, with itself as inverse. -/ +def localHadamardEquiv (i : ι) : Amplitude ι ≃ Amplitude ι where + toFun := localHadamard i + invFun := localHadamard i + left_inv := localHadamard_involutive i + right_inv := localHadamard_involutive i + +/-- S is a bijection on the full amplitude space with the explicit S† inverse. -/ +def localPhaseEquiv (i : ι) : Amplitude ι ≃ Amplitude ι where + toFun := localPhase i + invFun := localPhaseInverse i + left_inv := localPhaseInverse_localPhase i + right_inv := localPhase_localPhaseInverse i + +/-- The complex-linear involution induced by H at a selected site. -/ +def localHadamardLinearEquiv (i : ι) : Amplitude ι ≃ₗ[ℂ] Amplitude ι where + toEquiv := localHadamardEquiv i + map_add' ψ φ := by + funext x + simp only [localHadamardEquiv, localHadamard, Pi.add_apply] + ring + map_smul' c ψ := by + funext x + simp only [localHadamardEquiv, localHadamard, Pi.smul_apply, smul_eq_mul, + RingHom.id_apply] + ring + +/-- The complex-linear equivalence induced by S at a selected site. -/ +def localPhaseLinearEquiv (i : ι) : Amplitude ι ≃ₗ[ℂ] Amplitude ι where + toEquiv := localPhaseEquiv i + map_add' ψ φ := by + funext x + simp [localPhaseEquiv, localPhase, mul_add] + map_smul' c ψ := by + funext x + simp only [localPhaseEquiv, localPhase, Pi.smul_apply, smul_eq_mul, + RingHom.id_apply] + ring + +end LeanPool.SingleCopyStabilizer.CliffordAction diff --git a/LeanPool/SingleCopyStabilizer/ExactLearning.lean b/LeanPool/SingleCopyStabilizer/ExactLearning.lean new file mode 100644 index 0000000000..2c36f08f78 --- /dev/null +++ b/LeanPool/SingleCopyStabilizer/ExactLearning.lean @@ -0,0 +1,267 @@ +/- +Copyright (c) 2026 Antonio Anna Mele. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Antonio Anna Mele +-/ +module + +public import LeanPool.SingleCopyStabilizer.Round +public import Mathlib.FieldTheory.Finiteness +public import LeanPool.SingleCopyStabilizer.AdaptiveProcess + + +/-! +# Stochastic compression of unsigned binary stabilizer labels + +This module instantiates the finite adaptive-process theorem with the actual +binary label-space update. At every round, it samples an X label uniformly +from the current X projection and an independent uniform binary correction. +The progress lower bound is proved from the one-round symplectic results. + +This is a theorem about unsigned label spaces. It does not assert that a +quantum measurement supplies the stated distribution or reconstruct phases. +-/ + +@[expose] public section + +noncomputable section +open scoped BigOperators + +namespace LeanPool.SingleCopyStabilizer.ExactLearning + +variable {ι : Type*} [Fintype ι] [DecidableEq ι] + +/-- An unsigned binary Lagrangian label space. -/ +abbrev State (ι : Type*) [Fintype ι] := + {L : BinarySpace ι // IsIsotropic L ∧ Module.finrank (ZMod 2) L = Fintype.card ι} + +/-- An observed X label together with its independent correction bit. -/ +abbrev Outcome (ι : Type*) := BinaryVec ι × ZMod 2 + +/-- The number of diagonal generators still missing. -/ +def rank (s : State ι) : ℕ := + Fintype.card ι - Module.finrank (ZMod 2) (diagonalSpace s.val) + +/-- Totalized round update, with the Lagrangian invariants preserved. -/ +def next (s : State ι) (o : Outcome ι) : State ι := + ⟨safeBinaryRound s.val o.1 o.2, + safeBinaryRound_isotropic s.val s.property.1 o.1 o.2, + (safeBinaryRound_finrank s.val o.1 o.2).trans s.property.2⟩ + +open Classical in +/-- Uniform sampling on the current X projection, independently of a +uniform correction bit. Impossible X labels have weight zero. -/ +def weight (s : State ι) (o : Outcome ι) : ℝ := + if o.1 ∈ xProjection s.val then + 1 / ((Nat.card (xProjection s.val) : ℝ) * 2) else 0 + +omit [DecidableEq ι] in +theorem projection_card_pos (s : State ι) : + 0 < Nat.card (xProjection s.val) := Nat.card_pos + +omit [DecidableEq ι] in +theorem weight_nonneg (s : State ι) (o : Outcome ι) : 0 ≤ weight s o := by + classical + unfold weight + split_ifs <;> positivity + +theorem weight_sum (s : State ι) : ∑ o, weight s o = 1 := by + classical + have hc : (Nat.card (xProjection s.val) : ℝ) ≠ 0 := by + exact_mod_cast Nat.ne_of_gt (projection_card_pos s) + have hinner (u : BinaryVec ι) : + (∑ b : ZMod 2, weight s (u, b)) = + if u ∈ xProjection s.val then 1 / (Nat.card (xProjection s.val) : ℝ) else 0 := by + by_cases hu : u ∈ xProjection s.val + · simp [weight, hu] + · simp [weight, hu] + rw [Fintype.sum_prod_type] + simp_rw [hinner] + rw [← Finset.sum_filter] + simp only [Finset.sum_const, nsmul_eq_mul] + have hcard : (Finset.univ.filter fun u : BinaryVec ι => u ∈ xProjection s.val).card = + Nat.card (xProjection s.val) := by + simp only [Nat.card_eq_fintype_card, Fintype.card_subtype] + rw [hcard] + field_simp + +omit [DecidableEq ι] in +theorem diagonal_finrank_le (s : State ι) : + Module.finrank (ZMod 2) (diagonalSpace s.val) ≤ Fintype.card ι := by + classical + have h := finrank_xProjection_add_diagonal s.val + rw [s.property.2] at h + omega + +omit [DecidableEq ι] in +theorem rank_eq_projection_finrank (s : State ι) : + rank s = Module.finrank (ZMod 2) (xProjection s.val) := by + classical + have h := finrank_xProjection_add_diagonal s.val + rw [s.property.2] at h + unfold rank + omega + +omit [DecidableEq ι] in +/-- The current X projection contains exactly `2^rank` labels. -/ +theorem projection_card_eq_pow_rank (s : State ι) : + Nat.card (xProjection s.val) = 2 ^ rank s := by + classical + rw [Nat.card_eq_fintype_card, rank_eq_projection_finrank, + Module.card_eq_pow_finrank (K := ZMod 2)] + simp + +theorem rank_mono (s : State ι) (o : Outcome ι) : rank (next s o) ≤ rank s := by + classical + exact Nat.sub_le_sub_left (safeBinaryRound_diagonal_mono s.val s.property.1 o.1 o.2) _ + +/-- The finite probability process whose random outcomes are projection +labels and correction bits, and whose state is the evolving label space. -/ +def process : AdaptiveProcess.RankedProcess (State ι) (Outcome ι) where + weight := weight + next := next + rank := rank + weight_nonneg := weight_nonneg + weight_sum := weight_sum + rank_mono := rank_mono + +/-- Any nonzero allowed X label admits at least one correction that strictly +reduces the number of missing diagonal generators. -/ +theorem exists_rank_progress (s : State ι) (u : BinaryVec ι) + (hu : u ∈ xProjection s.val) (hzero : u ≠ 0) : + ∃ b : ZMod 2, rank (next s (u, b)) < rank s := by + classical + obtain ⟨b, hb⟩ := binaryRound_exists_progress s.val s.property.1 u hu hzero + refine ⟨b, ?_⟩ + have hdiag := diagonal_finrank_le (next s (u, b)) + change Module.finrank (ZMod 2) (diagonalSpace (safeBinaryRound s.val u b)) ≤ _ at hdiag + have hnext : safeBinaryRound s.val u b = binaryRound s.val u b := by + simp [safeBinaryRound, hu] + rw [hnext] at hdiag + change Fintype.card ι - Module.finrank (ZMod 2) (diagonalSpace (safeBinaryRound s.val u b)) < + Fintype.card ι - Module.finrank (ZMod 2) (diagonalSpace s.val) + rw [hnext] + omega + +omit [DecidableEq ι] in +/-- Positive rank guarantees at least two possible X labels. -/ +theorem two_le_projection_card (s : State ι) (hrank : 0 < rank s) : + 2 ≤ Nat.card (xProjection s.val) := by + classical + rw [Nat.card_eq_fintype_card] + rw [rank_eq_projection_finrank] at hrank + have : Nontrivial (xProjection s.val) := Module.finrank_pos_iff.mp hrank + have h := Fintype.one_lt_card (α := xProjection s.val) + omega + +open Classical in +/-- Cardinality of the nonzero part of the X projection. -/ +theorem nonzero_projection_card (s : State ι) : + (Finset.univ.filter fun u : BinaryVec ι => u ∈ xProjection s.val ∧ u ≠ 0).card = + Nat.card (xProjection s.val) - 1 := by + classical + have hset : (Finset.univ.filter fun u : BinaryVec ι => u ∈ xProjection s.val ∧ u ≠ 0) = + (Finset.univ.filter fun u : BinaryVec ι => u ∈ xProjection s.val).erase 0 := by + ext u + simp [and_comm] + rw [hset, Finset.card_erase_of_mem (Finset.mem_filter.mpr + ⟨Finset.mem_univ _, (xProjection s.val).zero_mem⟩)] + simp only [Nat.card_eq_fintype_card, Fintype.card_subtype] + +/-- Counting one successful correction for every nonzero X label gives +an unconditional progress mass of at least `(#X-1)/(2#X)`. -/ +theorem progress_mass_lower_bound (s : State ι) : + ((Nat.card (xProjection s.val) : ℝ) - 1) / + ((Nat.card (xProjection s.val) : ℝ) * 2) ≤ process.progressMass s := by + classical + let c : ℝ := 1 / ((Nat.card (xProjection s.val) : ℝ) * 2) + have hnonneg (u : BinaryVec ι) (b : ZMod 2) : + 0 ≤ if rank (next s (u, b)) < rank s then weight s (u, b) else 0 := by + split_ifs + · exact weight_nonneg _ _ + · exact le_rfl + have hinner (u : BinaryVec ι) : + (if u ∈ xProjection s.val ∧ u ≠ 0 then c else 0) ≤ + ∑ b : ZMod 2, if rank (next s (u, b)) < rank s then weight s (u, b) else 0 := by + by_cases hu : u ∈ xProjection s.val ∧ u ≠ 0 + · obtain ⟨b, hb⟩ := exists_rank_progress s u hu.1 hu.2 + have hsingle := Finset.single_le_sum (fun b _ => hnonneg u b) (Finset.mem_univ b) + simpa [hu, hb, weight, hu.1, c] using hsingle + · simp only [ite_eq_right hu] + exact Finset.sum_nonneg fun b _ => hnonneg u b + calc + _ = ∑ u : BinaryVec ι, if u ∈ xProjection s.val ∧ u ≠ 0 then c else 0 := by + rw [← Finset.sum_filter] + simp only [Finset.sum_const, nsmul_eq_mul, nonzero_projection_card] + rw [Nat.cast_sub (by + have := projection_card_pos s + omega : 1 ≤ Nat.card (xProjection s.val))] + simp only [Nat.cast_one] + dsimp [c] + ring + _ ≤ ∑ u : BinaryVec ι, ∑ b : ZMod 2, + if rank (next s (u, b)) < rank s then weight s (u, b) else 0 := + Finset.sum_le_sum fun u _ => hinner u + _ = process.progressMass s := by + simp only [AdaptiveProcess.RankedProcess.progressMass, Fintype.sum_prod_type, process] + rfl + +/-- The exact rank-dependent progress parameter used in the paper is also +proved for this label process. -/ +theorem progress_mass_ge_rank_parameter (s : State ι) : + (1 - (1 / 2 : ℝ) ^ rank s) / 2 ≤ process.progressMass s := by + classical + have h := progress_mass_lower_bound s + rw [projection_card_eq_pow_rank] at h + push_cast at h + have heq : (((2 : ℝ) ^ rank s) - 1) / ((2 : ℝ) ^ rank s * 2) = + (1 - (1 / 2 : ℝ) ^ rank s) / 2 := by + rw [div_pow, one_pow] + field_simp + rwa [heq] at h + +/-- The quarter-progress assumption is derived from the label-space update, +not left as a hypothesis of the compression theorem. -/ +theorem progress_mass_ge_quarter (s : State ι) (hrank : 0 < rank s) : + (1 / 4 : ℝ) ≤ process.progressMass s := by + classical + have hcard : (2 : ℝ) ≤ Nat.card (xProjection s.val) := by + exact_mod_cast two_le_projection_card s hrank + apply le_trans _ (progress_mass_lower_bound s) + apply (le_div_iff₀ (by positivity : (0 : ℝ) < (Nat.card (xProjection s.val) : ℝ) * 2)).2 + nlinarith + +/-- After `8(n+k)` uniform-X-label rounds, the probability that the label +space is not fully diagonal is at most `2^(-k)`. Here `n = #ι`, and all the +per-round progress hypotheses have been discharged. -/ +theorem compression_failure_probability (s : State ι) (k : ℕ) : + process.failureProbability (8 * (Fintype.card ι + k)) s ≤ (1 / 2 : ℝ) ^ k := by + classical + apply process.failure_probability_eight_rounds_per_bit + (fun s hs => progress_mass_ge_quarter s hs) (Fintype.card ι) k s + exact Nat.sub_le _ _ + +omit [DecidableEq ι] in +/-- The terminal event has exactly the expected algebraic meaning. -/ +theorem rank_zero_iff_full_diagonal (s : State ι) : + rank s = 0 ↔ Module.finrank (ZMod 2) (diagonalSpace s.val) = Fintype.card ι := by + classical + have h := diagonal_finrank_le s + unfold rank + omega + +omit [DecidableEq ι] in +/-- Equivalently, at termination every binary vector is a diagonal label. -/ +theorem rank_zero_iff_diagonal_eq_top (s : State ι) : + rank s = 0 ↔ diagonalSpace s.val = ⊤ := by + classical + constructor + · intro hs + apply Submodule.eq_top_of_finrank_eq + simpa using (rank_zero_iff_full_diagonal s).mp hs + · intro hs + apply (rank_zero_iff_full_diagonal s).mpr + rw [hs] + simp + +end LeanPool.SingleCopyStabilizer.ExactLearning diff --git a/LeanPool/SingleCopyStabilizer/ExactLearningTheorem.lean b/LeanPool/SingleCopyStabilizer/ExactLearningTheorem.lean new file mode 100644 index 0000000000..0841e1f949 --- /dev/null +++ b/LeanPool/SingleCopyStabilizer/ExactLearningTheorem.lean @@ -0,0 +1,89 @@ +/- +Copyright (c) 2026 Antonio Anna Mele. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Antonio Anna Mele +-/ +module + +public import LeanPool.SingleCopyStabilizer.Transcript +public import LeanPool.SingleCopyStabilizer.InstructionSemantics + + +/-! +# Exact qubit learning: correctness and physical resources + +This is the public combined theorem. The learner returns a finite recorded +circuit and one computational-basis string. Its exact correctness probability, +copy count, and interpreted elementary gate cost are proved together. + +The confidence constants are conservative. Classical machine runtime and +lower bounds are not asserted by this theorem. +-/ + +@[expose] public section + +noncomputable section + +namespace LeanPool.SingleCopyStabilizer.ExactLearningTheorem + +open Measurement OutputCorrectness ExactResources +variable {ι : Type*} [Fintype ι] [DecidableEq ι] + +open Classical in +/-- Real probability that the returned description is exactly the input +pure state, with global phase ignored. -/ +def successProbability (T : ℕ) (S : PureStabilizerState ι) : ℝ := + (((descriptionPMF T S).map fun d => + decide (SameRay S.amplitude (Circuit.decode d.1 d.2))) true).toReal + +/-- Exact recovery at the explicit leading-`2n` round budget. Every possible +execution uses `2T+1` copies and at most `(n+1)T²` elementary gate applications. +The counted instructions implement the circuit used by the learned-state +decoder; they are not merely a separate numerical cost assignment. -/ +theorem exact_learning (S : PureStabilizerState ι) (δ : ℝ) + (hδ : 0 < δ) (hδmax : δ ≤ 1) : + let T := SharpExactLearning.roundBudget (Fintype.card ι) δ + 1 - δ ≤ successProbability T S ∧ + ∀ d ∈ (descriptionPMF T S).support, + d.1.length = T ∧ + protocolCopyCount d.1 = 2 * T + 1 ∧ + protocolGateCost d.1 ≤ (Fintype.card ι + 1) * T ^ 2 ∧ + InstructionSemantics.instructionsEquiv (circuitInstructions d.1) = + Circuit.circuitEquiv d.1 ∧ + IsNormalized (Circuit.decode d.1 d.2) := by + classical + dsimp only + refine ⟨description_success_probability S δ hδ hδmax, ?_⟩ + intro d hd + exact ⟨Transcript.supported_length _ S d hd, + Transcript.supported_copy_count _ S d hd, + Transcript.supported_protocol_gate_cost _ S d hd, + InstructionSemantics.circuitInstructions_denote d.1, + Circuit.decode_normalized d.1 d.2⟩ + +/-- The number of copies at this budget has the explicit leading `4n` bound. -/ +theorem exact_learning_copy_bound (S : PureStabilizerState ι) (δ : ℝ) + (hδ : 0 < δ) (hδmax : δ ≤ 1) (d : Description ι) + (hd : d ∈ (descriptionPMF + (SharpExactLearning.roundBudget (Fintype.card ι) δ) S).support) : + (protocolCopyCount d.1 : ℝ) < 4 * (Fintype.card ι : ℝ) + 11 + + 16 * Real.sqrt ((2 * (Fintype.card ι : ℝ) + 4) * Real.log (1 / δ)) + + 128 * Real.log (1 / δ) := by + classical + rw [Transcript.supported_copy_count _ S d hd] + exact SharpExactLearning.copyBudget_upper (Fintype.card ι) δ hδ hδmax + +/-- Every supported output of the exact learner obeys an explicit +`O(n + log(1/δ))` copy bound with a universal constant. -/ +theorem exact_learning_copy_bound_linear (hn : 1 ≤ Fintype.card ι) + (S : PureStabilizerState ι) (δ : ℝ) (hδ : 0 < δ) (hδmax : δ ≤ 1) + (d : Description ι) + (hd : d ∈ (descriptionPMF + (SharpExactLearning.roundBudget (Fintype.card ι) δ) S).support) : + (protocolCopyCount d.1 : ℝ) < + 136 * ((Fintype.card ι : ℝ) + Real.log (1 / δ)) := by + classical + rw [Transcript.supported_copy_count _ S d hd] + exact SharpExactLearning.copyBudget_linear (Fintype.card ι) hn δ hδ hδmax + +end LeanPool.SingleCopyStabilizer.ExactLearningTheorem diff --git a/LeanPool/SingleCopyStabilizer/ExactResources.lean b/LeanPool/SingleCopyStabilizer/ExactResources.lean new file mode 100644 index 0000000000..aa2ee1edaa --- /dev/null +++ b/LeanPool/SingleCopyStabilizer/ExactResources.lean @@ -0,0 +1,213 @@ +/- +Copyright (c) 2026 Antonio Anna Mele. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Antonio Anna Mele +-/ +module + +public import LeanPool.SingleCopyStabilizer.Round +public import Mathlib.Tactic.Linarith +public import Mathlib.Tactic.Ring + + +/-! +# Symbolic gate and copy costs of the exact protocol + +An outcome list determines explicit symbolic CNOT/S/H instructions. Costs +count those instructions and their repeated execution on fresh copies. These +are not running-time claims about Lean's noncomputable state simulation. +-/ + +@[expose] public section + +noncomputable section + +namespace LeanPool.SingleCopyStabilizer.ExactResources + +open Finset + +/-- Elementary instructions counted by the protocol's gate model. -/ +inductive Instruction (ι : Type*) + | cnot (control target : ι) + | phase (site : ι) + | hadamard (site : ι) + +/-- The classical difference and correction coin recorded for one round. -/ +abbrev RoundOutcome (ι : Type*) := BinaryVec ι × ZMod 2 + +variable {ι : Type*} [Fintype ι] [DecidableEq ι] + +/-- Actual targets in the simultaneous pivot-controlled CNOT circuit. -/ +def cnotTargets (u : BinaryVec ι) (pivot : ι) : Finset ι := + Finset.univ.filter (fun j => j ≠ pivot ∧ u j = 1) + +/-- The pivot itself is never a CNOT target. -/ +theorem cnotTargets_card_add_one_le (u : BinaryVec ι) (pivot : ι) : + (cnotTargets u pivot).card + 1 ≤ Fintype.card ι := by + have hsubset : cnotTargets u pivot ⊆ (Finset.univ : Finset ι).erase pivot := by + intro j hj + have hne : j ≠ pivot := (Finset.mem_filter.mp hj).2.1 + simp [hne] + have hcard := Finset.card_le_card hsubset + have herase := Finset.card_erase_add_one (Finset.mem_univ pivot) + simp only [Finset.card_univ] at herase + omega + +/-- In chronological order: the pivot CNOTs, optional S, then H. A zero +computational difference appends no gates. -/ +def roundInstructions (outcome : RoundOutcome ι) : List (Instruction ι) := by + classical + exact if hzero : outcome.1 = 0 then [] else + let pivot := binaryPivot outcome.1 hzero + ((cnotTargets outcome.1 pivot).toList.map (Instruction.cnot pivot)) ++ + (if outcome.2 = 0 then [] else [Instruction.phase pivot]) ++ + [Instruction.hadamard pivot] + +/-- Gate cost is the length of the actual symbolic instruction list. -/ +def roundGateCount (outcome : RoundOutcome ι) : ℕ := (roundInstructions outcome).length + +@[simp] theorem roundInstructions_zero (b : ZMod 2) : + roundInstructions ((0 : BinaryVec ι), b) = [] := by + simp [roundInstructions] + +@[simp] theorem roundGateCount_zero (b : ZMod 2) : + roundGateCount ((0 : BinaryVec ι), b) = 0 := by + simp [roundGateCount] + +/-- The nonzero branch has exactly the chosen CNOTs, one H, and at most one S. -/ +theorem roundGateCount_of_ne (outcome : RoundOutcome ι) (hzero : outcome.1 ≠ 0) : + roundGateCount outcome = + (cnotTargets outcome.1 (binaryPivot outcome.1 hzero)).card + 1 + + if outcome.2 = 0 then 0 else 1 := by + classical + by_cases hb : outcome.2 = 0 <;> + simp [roundGateCount, roundInstructions, hzero, hb] + +/-- One round appends at most `n+1` gates, including both possible corrections. -/ +theorem roundGateCount_le (outcome : RoundOutcome ι) : + roundGateCount outcome ≤ Fintype.card ι + 1 := by + classical + by_cases hzero : outcome.1 = 0 + · simp [roundGateCount, roundInstructions, hzero] + · have htargets := cnotTargets_card_add_one_le outcome.1 (binaryPivot outcome.1 hzero) + rw [roundGateCount_of_ne outcome hzero] + split_ifs <;> omega + +/-- The accumulated circuit appends each round's instructions in order. -/ +def circuitInstructions (outcomes : List (RoundOutcome ι)) : List (Instruction ι) := + outcomes.flatMap roundInstructions + +/-- The accumulated gate count is the sum of all appended round costs. -/ +def listCircuitGateCount (outcomes : List (RoundOutcome ι)) : ℕ := + (outcomes.map roundGateCount).sum + +/-- The sum-based cost equals the length of the actual flattened gate list. -/ +theorem circuitInstructions_length (outcomes : List (RoundOutcome ι)) : + (circuitInstructions outcomes).length = listCircuitGateCount outcomes := by + induction outcomes with + | nil => simp [circuitInstructions, listCircuitGateCount] + | cons outcome outcomes ih => + simpa [circuitInstructions, listCircuitGateCount, roundGateCount] using + congrArg ((roundInstructions outcome).length + ·) ih + +/-- A circuit accumulated over `T` rounds has at most `(n+1)T` gates. -/ +theorem listCircuitGateCount_le (outcomes : List (RoundOutcome ι)) : + listCircuitGateCount outcomes ≤ (Fintype.card ι + 1) * outcomes.length := by + induction outcomes with + | nil => simp [listCircuitGateCount] + | cons outcome outcomes ih => + have hround := roundGateCount_le outcome + simp only [listCircuitGateCount, List.map_cons, List.sum_cons, List.length_cons] at * + nlinarith + +/-- Prefix circuits have a gate count linear in the prefix index. -/ +theorem prefixCircuitGateCount_le (outcomes : List (RoundOutcome ι)) (t : ℕ) : + listCircuitGateCount (outcomes.take t) ≤ (Fintype.card ι + 1) * t := by + have h := listCircuitGateCount_le (outcomes.take t) + have hlength : (outcomes.take t).length ≤ t := by simp + exact h.trans (Nat.mul_le_mul_left _ hlength) + +/-- Total gate applications: execute the current prefix twice in every round, +then execute the complete circuit once for the final computational readout. -/ +def protocolGateCost (outcomes : List (RoundOutcome ι)) : ℕ := + 2 * (∑ t ∈ Finset.range outcomes.length, listCircuitGateCount (outcomes.take t)) + + listCircuitGateCount outcomes + +/-- Twice the triangular sum plus its endpoint equals the square. -/ +theorem twice_prefix_sum_add (T : ℕ) : + 2 * (∑ t ∈ Finset.range T, t) + T = T ^ 2 := by + induction T with + | zero => norm_num + | succ T ih => + rw [Finset.sum_range_succ] + nlinarith + +/-- Total quantum gate applications are at most `(n+1)T²`, for every possible +outcome history, including unsuccessful histories. -/ +theorem protocolGateCost_le (outcomes : List (RoundOutcome ι)) : + protocolGateCost outcomes ≤ (Fintype.card ι + 1) * outcomes.length ^ 2 := by + have hprefix : (∑ t ∈ Finset.range outcomes.length, + listCircuitGateCount (outcomes.take t)) ≤ + (Fintype.card ι + 1) * (∑ t ∈ Finset.range outcomes.length, t) := by + calc + _ ≤ ∑ t ∈ Finset.range outcomes.length, (Fintype.card ι + 1) * t := + Finset.sum_le_sum (fun t _ => prefixCircuitGateCount_le outcomes t) + _ = _ := (Finset.mul_sum _ _ _).symm + calc + protocolGateCost outcomes ≤ + 2 * ((Fintype.card ι + 1) * (∑ t ∈ Finset.range outcomes.length, t)) + + (Fintype.card ι + 1) * outcomes.length := by + unfold protocolGateCost + exact Nat.add_le_add (Nat.mul_le_mul_left 2 hprefix) (listCircuitGateCount_le outcomes) + _ = (Fintype.card ι + 1) * + (2 * (∑ t ∈ Finset.range outcomes.length, t) + outcomes.length) := by ring + _ = (Fintype.card ι + 1) * outcomes.length ^ 2 := by rw [twice_prefix_sum_add] + +/-- For at least one qubit this is the explicit `2nT²` gate-resource bound. -/ +theorem protocolGateCost_le_two_n (outcomes : List (RoundOutcome ι)) + (hn : 1 ≤ Fintype.card ι) : + protocolGateCost outcomes ≤ 2 * Fintype.card ι * outcomes.length ^ 2 := by + apply (protocolGateCost_le outcomes).trans + exact Nat.mul_le_mul_right _ (by omega) + +/-- A zero-qubit register can produce no nonzero difference and appends no gates. -/ +theorem roundGateCount_of_zero_qubits (outcome : RoundOutcome ι) + (hn : Fintype.card ι = 0) : roundGateCount outcome = 0 := by + have : IsEmpty ι := Fintype.card_eq_zero_iff.mp hn + have hzero : outcome.1 = 0 := by ext i; exact isEmptyElim i + simp [roundGateCount, roundInstructions, hzero] + +/-- The full symbolic circuit is empty on a zero-qubit register. -/ +theorem listCircuitGateCount_of_zero_qubits (outcomes : List (RoundOutcome ι)) + (hn : Fintype.card ι = 0) : listCircuitGateCount outcomes = 0 := by + unfold listCircuitGateCount + induction outcomes with + | nil => simp + | cons outcome outcomes ih => simp [roundGateCount_of_zero_qubits outcome hn, ih] + +/-- Zero-qubit executions require no gates, regardless of the round count. -/ +theorem protocolGateCost_of_zero_qubits (outcomes : List (RoundOutcome ι)) + (hn : Fintype.card ι = 0) : protocolGateCost outcomes = 0 := by + simp [protocolGateCost, listCircuitGateCount_of_zero_qubits _ hn] + +/-- Every round consumes two input copies, and final readout consumes one. +Even rounds whose difference is zero consume their two measurement copies. -/ +def protocolCopyCount (outcomes : List (RoundOutcome ι)) : ℕ := 2 * outcomes.length + 1 + +omit [Fintype ι] [DecidableEq ι] in +@[simp] theorem protocolCopyCount_nil : protocolCopyCount ([] : List (RoundOutcome ι)) = 1 := rfl + +omit [Fintype ι] [DecidableEq ι] in +/-- Appending a round always consumes exactly two additional copies. -/ +theorem protocolCopyCount_cons (outcome : RoundOutcome ι) (outcomes : List (RoundOutcome ι)) : + protocolCopyCount (outcome :: outcomes) = protocolCopyCount outcomes + 2 := by + simp [protocolCopyCount] + omega + +omit [Fintype ι] [DecidableEq ι] in +/-- The protocol's exact total copy count. -/ +theorem protocolCopyCount_eq (outcomes : List (RoundOutcome ι)) (T : ℕ) + (hT : outcomes.length = T) : protocolCopyCount outcomes = 2 * T + 1 := by + simp [protocolCopyCount, hT] + +end LeanPool.SingleCopyStabilizer.ExactResources diff --git a/LeanPool/SingleCopyStabilizer/FiniteProbability.lean b/LeanPool/SingleCopyStabilizer/FiniteProbability.lean new file mode 100644 index 0000000000..033d848bfa --- /dev/null +++ b/LeanPool/SingleCopyStabilizer/FiniteProbability.lean @@ -0,0 +1,274 @@ +/- +Copyright (c) 2026 Antonio Anna Mele. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Antonio Anna Mele +-/ +module + +public import Mathlib.Probability.ProbabilityMassFunction.Constructions +public import Mathlib.Algebra.Order.BigOperators.Ring.Finset +public import Mathlib.Probability.Distributions.Uniform +public import Mathlib.Algebra.Order.Chebyshev +public import Mathlib.Tactic.Abel +public import Mathlib.Tactic.FieldSimp +public import Mathlib.Tactic.Linarith +public import Mathlib.Tactic.NormNum +public import Mathlib.Tactic.Positivity + + +/-! +# Finite probability calculations for adaptive stabilizer learning + +These are finite counting identities and real inequalities used in the paper. +They do not assert the quantum measurement laws, independence of physical +samples, or stochastic domination of a history-dependent stopping time. +-/ + +@[expose] public section + +noncomputable section + +namespace LeanPool.SingleCopyStabilizer.FiniteProbability + +open scoped BigOperators + +section Collision + +variable {A : Type*} [Fintype A] + +/-- The collision mass of a finite vector of class probabilities. -/ +def collisionMass (p : A → ℝ) : ℝ := ∑ a, p a ^ 2 + +/-- For independent draws with weights `p`, the diagonal of the product +weight has total mass `∑ a, p a²`. -/ +theorem independent_collision_mass (p : A → ℝ) [DecidableEq A] : + (∑ a, ∑ b, if a = b then p a * p b else 0) = collisionMass p := by + simp [collisionMass, sq] + +/-- Cauchy--Schwarz in the form used for the coset collision estimate. -/ +theorem one_le_card_mul_collision (p : A → ℝ) (hp : ∑ a, p a = 1) : + 1 ≤ (Fintype.card A : ℝ) * collisionMass p := by + have h := sq_sum_le_card_mul_sum_sq (s := Finset.univ) (f := p) + simpa [hp, collisionMass] using h + +/-- Any normalized class weights have collision mass at least `1 / #A`. -/ +theorem inv_card_le_collision [Nonempty A] (p : A → ℝ) (hp : ∑ a, p a = 1) : + 1 / (Fintype.card A : ℝ) ≤ collisionMass p := by + have hc : (0 : ℝ) < Fintype.card A := by exact_mod_cast Fintype.card_pos + apply (div_le_iff₀ hc).2 + simpa [mul_comm] using one_le_card_mul_collision p hp + +/-- At most `2^r` cosets give the paper's collision lower bound `2^(-r)`. +The expression on the left is written `1 / 2^r` to use natural exponents. -/ +theorem inverse_two_pow_le_collision (p : A → ℝ) (hp : ∑ a, p a = 1) + (r : ℕ) (hcard : Fintype.card A ≤ 2 ^ r) : + 1 / (2 : ℝ) ^ r ≤ collisionMass p := by + have hc : (Fintype.card A : ℝ) ≤ (2 : ℝ) ^ r := by exact_mod_cast hcard + have hn : 0 ≤ collisionMass p := Finset.sum_nonneg fun a _ => sq_nonneg (p a) + have hb := one_le_card_mul_collision p hp + apply (div_le_iff₀ (by positivity : (0 : ℝ) < 2 ^ r)).2 + nlinarith + +end Collision + +section Differences + +variable {G : Type*} [AddCommGroup G] + +/-- Fixing a difference leaves precisely one free outcome: `(x,y) ↦ y`, +with inverse `y ↦ (u+y,y)`. -/ +def differenceFiberEquiv (u : G) : {xy : G × G // xy.1 - xy.2 = u} ≃ G where + toFun xy := xy.val.2 + invFun y := ⟨(u + y, y), by simp⟩ + left_inv xy := by + apply Subtype.ext + apply Prod.ext + · exact (sub_eq_iff_eq_add.mp xy.property).symm + · rfl + right_inv _ := rfl + +/-- Translating both samples by the same affine offset leaves their +additive difference unchanged. -/ +theorem affine_difference (z x y : G) : (z + x) - (z + y) = x - y := by + abel + +variable [Fintype G] [DecidableEq G] + +/-- Every difference has exactly `#G` ordered representations in `G × G`. -/ +theorem difference_fiber_card (u : G) : + Fintype.card {xy : G × G // xy.1 - xy.2 = u} = Fintype.card G := + Fintype.card_congr (differenceFiberEquiv u) + +/-- Thus the difference of two independent uniform samples is uniform, +expressed as the ratio of favorable ordered pairs to all ordered pairs. -/ +theorem uniform_difference_probability (u : G) : + (Fintype.card {xy : G × G // xy.1 - xy.2 = u} : ℝ) / + (Fintype.card (G × G) : ℝ) = 1 / (Fintype.card G : ℝ) := by + rw [difference_fiber_card, Fintype.card_prod] + push_cast + have hc : (Fintype.card G : ℝ) ≠ 0 := by exact_mod_cast Fintype.card_ne_zero + field_simp + +omit [DecidableEq G] in +/-- The probability-mass-function pushforward of the uniform ordered-pair +distribution under subtraction is exactly the uniform distribution on `G`. -/ +theorem uniform_difference_pmf : + (PMF.uniformOfFintype (G × G)).map (fun xy => xy.1 - xy.2) = + PMF.uniformOfFintype G := by + classical + ext u + rw [PMF.map_apply] + simp only [PMF.uniformOfFintype_apply, tsum_fintype] + rw [← Finset.sum_filter] + have hcount : (Finset.univ.filter fun xy : G × G => u = xy.1 - xy.2).card = + Fintype.card G := by + simpa only [Fintype.card_subtype, eq_comm] using difference_fiber_card (G := G) u + simp only [Finset.sum_const, hcount, nsmul_eq_mul, Fintype.card_prod, Nat.cast_mul] + rw [ENNReal.mul_inv (Or.inr (ENNReal.natCast_ne_top _)) (Or.inl (ENNReal.natCast_ne_top _))] + apply ENNReal.mul_inv_cancel_left + · exact_mod_cast Fintype.card_ne_zero + · exact ENNReal.natCast_ne_top _ + +/-- The mass of one specified within-class difference when each class is +uniform internally and class `a` has mass `p a`. -/ +def sameClassDifferenceMass {A : Type*} [Fintype A] (p : A → ℝ) (u : G) : ℝ := + ∑ a, ∑ _xy : {xy : G × G // xy.1 - xy.2 = u}, + (p a / Fintype.card G) * (p a / Fintype.card G) + +/-- Within-class differences all have the same mass, namely collision +mass divided by the size of the common translation group. -/ +theorem same_class_difference_mass {A : Type*} [Fintype A] (p : A → ℝ) (u : G) : + sameClassDifferenceMass p u = collisionMass p / (Fintype.card G : ℝ) := by + have hc : (Fintype.card G : ℝ) ≠ 0 := by exact_mod_cast Fintype.card_ne_zero + unfold sameClassDifferenceMass collisionMass + rw [Finset.sum_div] + apply Finset.sum_congr rfl + intro a _ + simp only [Finset.sum_const, Finset.card_univ, difference_fiber_card, nsmul_eq_mul] + field_simp + +/-- Summing the nonzero within-class differences gives exactly the factor +`collisionMass p * (1 - 1 / #G)` used in the nullity argument. -/ +theorem nonzero_same_class_difference_mass {A : Type*} [Fintype A] (p : A → ℝ) : + (∑ u ∈ (Finset.univ : Finset G).erase 0, sameClassDifferenceMass p u) = + collisionMass p * (1 - 1 / (Fintype.card G : ℝ)) := by + simp_rw [same_class_difference_mass] + have hc : 0 < Fintype.card G := Fintype.card_pos + have hc0 : (Fintype.card G : ℝ) ≠ 0 := by exact_mod_cast Nat.ne_of_gt hc + simp only [Finset.sum_const, Finset.card_erase_of_mem (Finset.mem_univ (0 : G)), + Finset.card_univ, nsmul_eq_mul] + rw [Nat.cast_sub (by omega : 1 ≤ Fintype.card G)] + push_cast + field_simp + +/-- The low-nullity nonzero collision estimate, with the class and +translation-space cardinality assumptions displayed explicitly. -/ +theorem low_nullity_nonzero_mass_lower_bound {A : Type*} [Fintype A] + (p : A → ℝ) (hp : ∑ a, p a = 1) (r j : ℕ) + (hclasses : Fintype.card A ≤ 2 ^ r) (hgroup : Fintype.card G = 2 ^ j) : + 1 / (2 : ℝ) ^ r * (1 - 1 / (2 : ℝ) ^ j) ≤ + ∑ u ∈ (Finset.univ : Finset G).erase 0, sameClassDifferenceMass p u := by + rw [nonzero_same_class_difference_mass, hgroup] + push_cast + apply mul_le_mul_of_nonneg_right (inverse_two_pow_le_collision p hp r hclasses) + have hpow : (1 : ℝ) ≤ 2 ^ j := one_le_pow₀ (by norm_num) + have hpos : (0 : ℝ) < 2 ^ j := by positivity + have hinv : 1 / (2 : ℝ) ^ j ≤ 1 := (div_le_iff₀ hpos).2 (by simpa using hpow) + linarith + +end Differences + +section RoundBounds + +/-- A numerical survival recurrence gives the usual geometric tail. +The recurrence is an explicit hypothesis, not a proved law of the algorithm. -/ +theorem survival_le_geometric (s : ℕ → ℝ) (p : ℝ) (hp : p ≤ 1) + (hzero : s 0 ≤ 1) (hstep : ∀ k, s (k + 1) ≤ (1 - p) * s k) (k : ℕ) : + s k ≤ (1 - p) ^ k := by + induction k with + | zero => simpa using hzero + | succ k ih => + calc + s (k + 1) ≤ (1 - p) * s k := hstep k + _ ≤ (1 - p) * (1 - p) ^ k := + mul_le_mul_of_nonneg_left ih (sub_nonneg.mpr hp) + _ = (1 - p) ^ (k + 1) := by rw [pow_succ]; ring + +/-- A finite sum of survival terms is bounded by the corresponding finite +geometric sum, written in closed form. -/ +theorem finite_survival_sum_le (s : ℕ → ℝ) (p : ℝ) (hp0 : 0 < p) (hp1 : p ≤ 1) + (hzero : s 0 ≤ 1) (hstep : ∀ k, s (k + 1) ≤ (1 - p) * s k) (n : ℕ) : + (∑ k ∈ Finset.range n, s k) ≤ (1 - (1 - p) ^ n) / p := by + induction n with + | zero => simp + | succ n ih => + rw [Finset.sum_range_succ] + have hn := survival_le_geometric s p hp1 hzero hstep n + calc + _ ≤ (1 - (1 - p) ^ n) / p + (1 - p) ^ n := add_le_add ih hn + _ = (1 - (1 - p) ^ (n + 1)) / p := by + rw [pow_succ] + field_simp + ring + +/-- Thus every finite truncation of the tail sum is at most `1/p`. +Connecting this to a random variable's expectation is a separate step. -/ +theorem finite_survival_sum_le_inverse (s : ℕ → ℝ) (p : ℝ) + (hp0 : 0 < p) (hp1 : p ≤ 1) (hzero : s 0 ≤ 1) + (hstep : ∀ k, s (k + 1) ≤ (1 - p) * s k) (n : ℕ) : + (∑ k ∈ Finset.range n, s k) ≤ 1 / p := by + apply (finite_survival_sum_le s p hp0 hp1 hzero hstep n).trans + apply div_le_div_of_nonneg_right _ (le_of_lt hp0) + have hpow : 0 ≤ (1 - p) ^ n := pow_nonneg (sub_nonneg.mpr hp1) _ + linarith + +/-- The success parameter for a positive codimension `j`. -/ +def progressProbability (j : ℕ) : ℝ := (1 - (1 / 2 : ℝ) ^ j) / 2 + +/-- Every positive level has progress parameter at least one quarter. -/ +theorem progress_probability_ge_quarter (j : ℕ) (hj : 0 < j) : + (1 / 4 : ℝ) ≤ progressProbability j := by + obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (Nat.ne_of_gt hj) + have hpow : (1 / 2 : ℝ) ^ k ≤ 1 := pow_le_one₀ (by norm_num) (by norm_num) + unfold progressProbability + rw [pow_succ] + nlinarith + +/-- A strengthened finite reciprocal-sum estimate. This is an arithmetic +bound, not an expectation or stopping-time theorem. -/ +theorem reciprocal_sum_le (n : ℕ) : + (∑ k ∈ Finset.range n, 2 / (1 - (1 / 2 : ℝ) ^ (k + 1))) ≤ + 2 * n + 4 - 4 * (1 / 2 : ℝ) ^ n := by + induction n with + | zero => norm_num + | succ n ih => + rw [Finset.sum_range_succ] + have hpow0 : 0 ≤ (1 / 2 : ℝ) ^ n := by positivity + have hpow1 : (1 / 2 : ℝ) ^ n ≤ 1 := pow_le_one₀ (by norm_num) (by norm_num) + have hden : 0 < 1 - (1 / 2 : ℝ) ^ (n + 1) := by rw [pow_succ]; nlinarith + have hterm : 2 / (1 - (1 / 2 : ℝ) ^ (n + 1)) ≤ + 2 + 4 * (1 / 2 : ℝ) ^ (n + 1) := by + apply (div_le_iff₀ hden).2 + rw [pow_succ] + nlinarith [mul_nonneg hpow0 (sub_nonneg.mpr hpow1)] + push_cast + rw [pow_succ] at hterm ⊢ + linarith + +/-- The paper's strict numerical bound on the sum of reciprocal progress +parameters. The connection to expected waiting times is not assumed here. -/ +theorem reciprocal_sum_lt_two_n_add_four (n : ℕ) : + (∑ k ∈ Finset.range n, 2 / (1 - (1 / 2 : ℝ) ^ (k + 1))) < 2 * n + 4 := by + have h := reciprocal_sum_le n + have hp : 0 < (1 / 2 : ℝ) ^ n := by positivity + linarith + +/-- Scaling the same finite bound gives the low-nullity arithmetic bound. -/ +theorem scaled_reciprocal_sum_lt (r n : ℕ) : + (2 : ℝ) ^ r * (∑ k ∈ Finset.range n, 2 / (1 - (1 / 2 : ℝ) ^ (k + 1))) < + (2 : ℝ) ^ r * (2 * n + 4) := by + exact mul_lt_mul_of_pos_left (reciprocal_sum_lt_two_n_add_four n) (by positivity) + +end RoundBounds + +end LeanPool.SingleCopyStabilizer.FiniteProbability diff --git a/LeanPool/SingleCopyStabilizer/GeometricDomination.lean b/LeanPool/SingleCopyStabilizer/GeometricDomination.lean new file mode 100644 index 0000000000..94f485d91e --- /dev/null +++ b/LeanPool/SingleCopyStabilizer/GeometricDomination.lean @@ -0,0 +1,214 @@ +/- +Copyright (c) 2026 Antonio Anna Mele. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Antonio Anna Mele +-/ +module + +public import LeanPool.SingleCopyStabilizer.AdaptiveProcess +public import Mathlib.Tactic.FieldSimp + + +/-! +# Geometric-product tail bounds for finite adaptive processes + +Per-state, history-dependent strict-progress bounds imply the same +exponential upper-tail product as independent geometric waiting times. The +proof is direct: derive a one-step contraction of a killed product potential +and iterate it over the finite probability tree. No independent waiting-time +coupling or final tail bound is assumed. +-/ + +@[expose] public section + +noncomputable section +open scoped BigOperators + +namespace LeanPool.SingleCopyStabilizer.GeometricDomination + +/-- The geometric moment-generating factor, in the parameterization +`q = 1/(1-λ)`. -/ +def geometricFactor (p : ℕ → ℝ) (lambda : ℝ) (j : ℕ) : ℝ := + (1 - lambda / p j)⁻¹ + +/-- Product over the positive ranks up to and including `r`. -/ +def productPotential (p : ℕ → ℝ) (lambda : ℝ) (r : ℕ) : ℝ := + ∏ j ∈ Finset.range r, geometricFactor p lambda (j + 1) + +/-- Set the potential to zero at the terminal rank. -/ +def killedPotential (p : ℕ → ℝ) (lambda : ℝ) (r : ℕ) : ℝ := + if r = 0 then 0 else productPotential p lambda r + +variable (p : ℕ → ℝ) (lambda : ℝ) + +@[simp] theorem productPotential_zero : productPotential p lambda 0 = 1 := by + simp [productPotential] + +@[simp] theorem killedPotential_zero : killedPotential p lambda 0 = 0 := by + simp [killedPotential] + +theorem productPotential_succ (r : ℕ) : + productPotential p lambda (r + 1) = + productPotential p lambda r * geometricFactor p lambda (r + 1) := by + simp [productPotential, Finset.prod_range_succ] + +variable (hlambda : 0 ≤ lambda) (hrate : ∀ j, 0 < j → lambda < p j) +include hlambda hrate + +theorem factor_denominator_pos (j : ℕ) (hj : 0 < j) : 0 < 1 - lambda / p j := by + have hp : 0 < p j := lt_of_le_of_lt hlambda (hrate j hj) + have hdiv : lambda / p j < 1 := (div_lt_iff₀ hp).2 (by simpa using hrate j hj) + linarith + +theorem one_le_geometricFactor (j : ℕ) (hj : 0 < j) : + 1 ≤ geometricFactor p lambda j := by + have hp : 0 < p j := lt_of_le_of_lt hlambda (hrate j hj) + have hden := factor_denominator_pos p lambda hlambda hrate j hj + unfold geometricFactor + rw [inv_eq_one_div] + apply (le_div_iff₀ hden).2 + have hdiv : 0 ≤ lambda / p j := div_nonneg hlambda (le_of_lt hp) + linarith + +theorem one_le_productPotential (r : ℕ) : 1 ≤ productPotential p lambda r := by + induction r with + | zero => simp + | succ r ih => + rw [productPotential_succ] + have hf := one_le_geometricFactor p lambda hlambda hrate (r + 1) (by omega) + nlinarith + +theorem productPotential_nonneg (r : ℕ) : 0 ≤ productPotential p lambda r := + le_trans (by norm_num) (one_le_productPotential p lambda hlambda hrate r) + +theorem productPotential_mono : Monotone (productPotential p lambda) := by + apply monotone_nat_of_le_succ + intro r + rw [productPotential_succ] + have hg := productPotential_nonneg p lambda hlambda hrate r + have hf := one_le_geometricFactor p lambda hlambda hrate (r + 1) (by omega) + nlinarith + +theorem killedPotential_nonneg (r : ℕ) : 0 ≤ killedPotential p lambda r := by + unfold killedPotential + split_ifs + · exact le_rfl + · exact productPotential_nonneg p lambda hlambda hrate r + +theorem killedPotential_le_productPotential {a b : ℕ} (hab : a ≤ b) : + killedPotential p lambda a ≤ productPotential p lambda b := by + unfold killedPotential + split_ifs + · exact productPotential_nonneg p lambda hlambda hrate b + · exact productPotential_mono p lambda hlambda hrate hab + +/-- The defining product has exactly the one-step recurrence of a geometric +waiting-time generating function at each positive rank. -/ +theorem productPotential_recurrence (r : ℕ) : + (1 - p (r + 1)) * productPotential p lambda (r + 1) + + p (r + 1) * productPotential p lambda r = + (1 - lambda) * productPotential p lambda (r + 1) := by + have hp : p (r + 1) ≠ 0 := ne_of_gt (lt_of_le_of_lt hlambda (hrate _ (by omega))) + have hden : 1 - lambda / p (r + 1) ≠ 0 := + ne_of_gt (factor_denominator_pos p lambda hlambda hrate _ (by omega)) + have hsub : p (r + 1) - lambda ≠ 0 := ne_of_gt (sub_pos.mpr (hrate _ (by omega))) + rw [productPotential_succ] + unfold geometricFactor + field_simp [hsub] + ring + +variable {S Ω : Type*} [Fintype Ω] + +/-- History-conditioned progress gives contraction of the product +potential at every state of the finite tree. -/ +theorem product_potential_drift (P : AdaptiveProcess.RankedProcess S Ω) + (hprogress : ∀ s, 0 < P.rank s → p (P.rank s) ≤ P.progressMass s) (s : S) : + (∑ o, P.weight s o * killedPotential p lambda (P.rank (P.next s o))) ≤ + (1 - lambda) * killedPotential p lambda (P.rank s) := by + cases hs : P.rank s with + | zero => + have hnext : ∀ o, P.rank (P.next s o) = 0 := fun o => by + have h := P.rank_mono s o + omega + simp [hnext] + | succ r => + have hpoint (o : Ω) : + P.weight s o * killedPotential p lambda (P.rank (P.next s o)) ≤ + P.weight s o * productPotential p lambda (r + 1) - + (if P.rank (P.next s o) < P.rank s then P.weight s o else 0) * + (productPotential p lambda (r + 1) - productPotential p lambda r) := by + split_ifs with hlt + · have hr : P.rank (P.next s o) ≤ r := by omega + have hh := mul_le_mul_of_nonneg_left + (killedPotential_le_productPotential p lambda hlambda hrate hr) (P.weight_nonneg s o) + linarith + · have hr : P.rank (P.next s o) ≤ r + 1 := by + simpa [hs] using P.rank_mono s o + simpa using mul_le_mul_of_nonneg_left + (killedPotential_le_productPotential p lambda hlambda hrate hr) (P.weight_nonneg s o) + have hdiff : 0 ≤ productPotential p lambda (r + 1) - productPotential p lambda r := + sub_nonneg.mpr (productPotential_mono p lambda hlambda hrate (by omega)) + have hpr : p (r + 1) ≤ P.progressMass s := by + simpa [hs] using hprogress s (by omega) + calc + _ ≤ ∑ o, (P.weight s o * productPotential p lambda (r + 1) - + (if P.rank (P.next s o) < P.rank s then P.weight s o else 0) * + (productPotential p lambda (r + 1) - productPotential p lambda r)) := + Finset.sum_le_sum fun o _ => hpoint o + _ = productPotential p lambda (r + 1) - P.progressMass s * + (productPotential p lambda (r + 1) - productPotential p lambda r) := by + simp only [Finset.sum_sub_distrib, ← Finset.sum_mul, P.weight_sum, one_mul, + AdaptiveProcess.RankedProcess.progressMass] + _ ≤ productPotential p lambda (r + 1) - p (r + 1) * + (productPotential p lambda (r + 1) - productPotential p lambda r) := by + exact sub_le_sub_left (mul_le_mul_of_nonneg_right hpr hdiff) _ + _ = (1 - p (r + 1)) * productPotential p lambda (r + 1) + + p (r + 1) * productPotential p lambda r := by ring + _ = (1 - lambda) * productPotential p lambda (r + 1) := + productPotential_recurrence p lambda hlambda hrate r + _ = (1 - lambda) * killedPotential p lambda (r + 1) := by + simp [killedPotential] + +/-- The product-geometric tail inequality for a fully adaptive finite tree. +Only local kernel/progress hypotheses are used. -/ +theorem failure_probability_le_product (P : AdaptiveProcess.RankedProcess S Ω) + (hlambda1 : lambda ≤ 1) + (hprogress : ∀ s, 0 < P.rank s → p (P.rank s) ≤ P.progressMass s) + (t : ℕ) (s : S) : + P.failureProbability t s ≤ productPotential p lambda (P.rank s) * (1 - lambda) ^ t := by + have hq : 0 ≤ 1 - lambda := sub_nonneg.mpr hlambda1 + have hmain (t : ℕ) (s : S) : + P.failureProbability t s ≤ (1 - lambda) ^ t * killedPotential p lambda (P.rank s) := by + induction t generalizing s with + | zero => + by_cases hs : P.rank s = 0 + · simp [AdaptiveProcess.RankedProcess.failureProbability, killedPotential, hs] + · simpa [AdaptiveProcess.RankedProcess.failureProbability, killedPotential, hs] using + one_le_productPotential p lambda hlambda hrate (P.rank s) + | succ t ih => + calc + P.failureProbability (t + 1) s = + ∑ o, P.weight s o * P.failureProbability t (P.next s o) := rfl + _ ≤ ∑ o, P.weight s o * ((1 - lambda) ^ t * + killedPotential p lambda (P.rank (P.next s o))) := + Finset.sum_le_sum fun o _ => mul_le_mul_of_nonneg_left (ih _) (P.weight_nonneg s o) + _ = (1 - lambda) ^ t * ∑ o, + P.weight s o * killedPotential p lambda (P.rank (P.next s o)) := by + rw [Finset.mul_sum] + apply Finset.sum_congr rfl + intro o _ + ring + _ ≤ (1 - lambda) ^ t * ((1 - lambda) * killedPotential p lambda (P.rank s)) := + mul_le_mul_of_nonneg_left + (product_potential_drift p lambda hlambda hrate P hprogress s) (pow_nonneg hq t) + _ = (1 - lambda) ^ (t + 1) * killedPotential p lambda (P.rank s) := by + rw [pow_succ] + ring + calc + _ ≤ (1 - lambda) ^ t * killedPotential p lambda (P.rank s) := hmain t s + _ ≤ (1 - lambda) ^ t * productPotential p lambda (P.rank s) := + mul_le_mul_of_nonneg_left + (killedPotential_le_productPotential p lambda hlambda hrate (le_refl _)) (pow_nonneg hq t) + _ = _ := by ring + +end LeanPool.SingleCopyStabilizer.GeometricDomination diff --git a/LeanPool/SingleCopyStabilizer/GeometricTailBounds.lean b/LeanPool/SingleCopyStabilizer/GeometricTailBounds.lean new file mode 100644 index 0000000000..dcab3d2416 --- /dev/null +++ b/LeanPool/SingleCopyStabilizer/GeometricTailBounds.lean @@ -0,0 +1,250 @@ +/- +Copyright (c) 2026 Antonio Anna Mele. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Antonio Anna Mele +-/ +module + +public import LeanPool.SingleCopyStabilizer.FiniteProbability +public import Mathlib.Analysis.SpecialFunctions.Log.Basic +public import Mathlib.Analysis.Real.Sqrt +public import Mathlib.Tactic.FieldSimp +public import Mathlib.Tactic.Linarith +public import Mathlib.Tactic.Positivity +public import Mathlib.Tactic.Ring + + +/-! +# Scalar Chernoff bounds for geometric-product potentials + +These finite-product inequalities are independent of a stochastic model. +`GeometricDomination` supplies the adaptive-process domination needed to +interpret the final bound as a failure probability. +-/ + +@[expose] public section + +noncomputable section + +namespace LeanPool.SingleCopyStabilizer.GeometricTailBounds + +open Finset + +/-- A quadratic upper bound for a geometric-series factor. -/ +theorem reciprocal_one_sub_le_quadratic (x : ℝ) (_hx : 0 ≤ x) (hxhalf : x ≤ 1 / 2) : + (1 - x)⁻¹ ≤ 1 + x + 2 * x ^ 2 := by + have hden : 0 < 1 - x := by linarith + rw [← one_div] + apply (div_le_iff₀ hden).2 + have hproduct := mul_nonneg (sq_nonneg x) (show 0 ≤ 1 - 2 * x by linarith) + nlinarith + +/-- The same reciprocal factor is bounded by a quadratic exponential. -/ +theorem reciprocal_one_sub_le_exp (x : ℝ) (hx : 0 ≤ x) (hxhalf : x ≤ 1 / 2) : + (1 - x)⁻¹ ≤ Real.exp (x + 2 * x ^ 2) := by + calc + _ ≤ 1 + x + 2 * x ^ 2 := reciprocal_one_sub_le_quadratic x hx hxhalf + _ ≤ Real.exp (x + 2 * x ^ 2) := by + have := Real.add_one_le_exp (x + 2 * x ^ 2) + linarith + +/-- Each geometric PGF factor has an exponential bound controlled by `1/p`. -/ +theorem geometric_factor_le_exp (p lam : ℝ) (hp : (1 / 4 : ℝ) ≤ p) + (hlam : 0 ≤ lam) (hlammax : lam ≤ 1 / 8) : + (1 - lam / p)⁻¹ ≤ Real.exp ((lam + 8 * lam ^ 2) / p) := by + have hpPos : 0 < p := by linarith + have hx : 0 ≤ lam / p := div_nonneg hlam hpPos.le + have hxhalf : lam / p ≤ 1 / 2 := by + apply (div_le_iff₀ hpPos).2 + linarith + have hexp : lam / p + 2 * (lam / p) ^ 2 ≤ (lam + 8 * lam ^ 2) / p := by + have hinv : 1 / p ≤ 4 := by + apply (div_le_iff₀ hpPos).2 + linarith + have hsq : (1 / p) ^ 2 ≤ 4 / p := by + have hmul := mul_le_mul_of_nonneg_right hinv + (show 0 ≤ 1 / p by positivity) + convert hmul using 1 <;> ring + have hmul := mul_le_mul_of_nonneg_left hsq (show 0 ≤ 2 * lam ^ 2 by positivity) + have hmuladd := add_le_add_left hmul (lam / p) + convert hmuladd using 1 <;> ring + exact (reciprocal_one_sub_le_exp _ hx hxhalf).trans (Real.exp_le_exp.mpr hexp) + +/-- The product of the geometric factors is bounded using their reciprocal sum. -/ +theorem product_le_exp {α : Type*} (indices : Finset α) (p : α → ℝ) (lam M : ℝ) + (hp : ∀ i ∈ indices, (1 / 4 : ℝ) ≤ p i) + (hlam : 0 ≤ lam) (hlammax : lam ≤ 1 / 8) + (hmean : (∑ i ∈ indices, 1 / p i) ≤ M) : + (∏ i ∈ indices, (1 - lam / p i)⁻¹) ≤ Real.exp ((lam + 8 * lam ^ 2) * M) := by + have hprod : (∏ i ∈ indices, (1 - lam / p i)⁻¹) ≤ + ∏ i ∈ indices, Real.exp ((lam + 8 * lam ^ 2) / p i) := by + apply Finset.prod_le_prod₀ + · intro i hi + have hpPos : 0 < p i := by have := hp i hi; linarith + have hratio : lam / p i ≤ 1 / 2 := by + apply (div_le_iff₀ hpPos).2 + have := hp i hi + linarith + exact inv_nonneg.mpr (by linarith) + · intro i hi + exact geometric_factor_le_exp _ _ (hp i hi) hlam hlammax + calc + _ ≤ ∏ i ∈ indices, Real.exp ((lam + 8 * lam ^ 2) / p i) := hprod + _ = Real.exp ((lam + 8 * lam ^ 2) * (∑ i ∈ indices, 1 / p i)) := by + rw [← Real.exp_sum, Finset.mul_sum] + congr 1 + apply Finset.sum_congr rfl + intro i _ + ring + _ ≤ Real.exp ((lam + 8 * lam ^ 2) * M) := by + apply Real.exp_le_exp.mpr + exact mul_le_mul_of_nonneg_left hmean (by positivity) + +/-- The Bernoulli decay term is at most the corresponding exponential. -/ +theorem decay_le_exp (lam : ℝ) (T : ℕ) (hlammax : lam ≤ 1) : + (1 - lam) ^ T ≤ Real.exp (-lam * (T : ℝ)) := by + have hpow := pow_le_pow_left₀ (show 0 ≤ 1 - lam by linarith) + (Real.one_sub_le_exp_neg lam) T + calc + _ ≤ Real.exp (-lam) ^ T := hpow + _ = Real.exp (-lam * (T : ℝ)) := by rw [← Real.exp_nat_mul]; congr 1; ring + +/-- A finite-product Chernoff bound before choosing the exponential parameter. -/ +theorem product_decay_le_exp {α : Type*} (indices : Finset α) (p : α → ℝ) + (lam M : ℝ) (T : ℕ) (hp : ∀ i ∈ indices, (1 / 4 : ℝ) ≤ p i) + (hlam : 0 ≤ lam) (hlammax : lam ≤ 1 / 8) + (hmean : (∑ i ∈ indices, 1 / p i) ≤ M) : + (∏ i ∈ indices, (1 - lam / p i)⁻¹) * (1 - lam) ^ T ≤ + Real.exp ((lam + 8 * lam ^ 2) * M - lam * (T : ℝ)) := by + calc + _ ≤ Real.exp ((lam + 8 * lam ^ 2) * M) * Real.exp (-lam * (T : ℝ)) := by + apply mul_le_mul (product_le_exp indices p lam M hp hlam hlammax hmean) + (decay_le_exp lam T (by linarith)) + · exact pow_nonneg (by linarith) _ + · exact (Real.exp_pos _).le + _ = _ := by rw [← Real.exp_add]; congr 1; ring + +/-- Parameter used for a deviation `s` above the reciprocal-sum bound `M`. -/ +def chosenTilt (M s : ℝ) : ℝ := s / (16 * (M + s)) + +theorem chosenTilt_bounds (M s : ℝ) (hM : 0 < M) (hs : 0 ≤ s) : + 0 ≤ chosenTilt M s ∧ chosenTilt M s ≤ 1 / 16 := by + have hden : 0 < 16 * (M + s) := by positivity + constructor + · exact div_nonneg hs hden.le + · apply (div_le_iff₀ hden).2 + linarith + +/-- The chosen tilt is strictly below every permitted progress rate. -/ +theorem chosenTilt_lt_rate (M s p : ℝ) (hM : 0 < M) (hs : 0 ≤ s) + (hp : (1 / 4 : ℝ) ≤ p) : chosenTilt M s < p := by + have := (chosenTilt_bounds M s hM hs).2 + linarith + +/-- The chosen tilt gives a quadratic-over-linear deviation exponent. -/ +theorem chosenTilt_exponent (M s T : ℝ) (hM : 0 < M) (hs : 0 ≤ s) + (hT : M + s ≤ T) : + (chosenTilt M s + 8 * (chosenTilt M s) ^ 2) * M - chosenTilt M s * T ≤ + -(s ^ 2 / (32 * (M + s))) := by + have hden : 0 < M + s := by linarith + have hlam := (chosenTilt_bounds M s hM hs).1 + have htime := mul_le_mul_of_nonneg_left hT hlam + have hlocal : (chosenTilt M s + 8 * (chosenTilt M s) ^ 2) * M - + chosenTilt M s * (M + s) + s ^ 2 / (32 * (M + s)) = + -(s ^ 3 / (32 * (M + s) ^ 2)) := by + unfold chosenTilt + field_simp + ring + have hnonneg : 0 ≤ s ^ 3 / (32 * (M + s) ^ 2) := by positivity + linarith + +/-- Finite geometric-product Chernoff bound with leading term `M`. -/ +theorem sharp_tail_bound {α : Type*} (indices : Finset α) (p : α → ℝ) + (M s : ℝ) (T : ℕ) (hM : 0 < M) (hs : 0 ≤ s) + (hp : ∀ i ∈ indices, (1 / 4 : ℝ) ≤ p i) + (hmean : (∑ i ∈ indices, 1 / p i) ≤ M) (hT : M + s ≤ (T : ℝ)) : + (∏ i ∈ indices, (1 - chosenTilt M s / p i)⁻¹) * (1 - chosenTilt M s) ^ T ≤ + Real.exp (-(s ^ 2 / (32 * (M + s)))) := by + obtain ⟨hlam, hlammax⟩ := chosenTilt_bounds M s hM hs + exact (product_decay_le_exp indices p _ M T hp hlam (by linarith) hmean).trans + (Real.exp_le_exp.mpr (chosenTilt_exponent M s T hM hs hT)) + +/-- An explicit deviation of order `sqrt(M L) + L`. -/ +def confidenceDeviation (M L : ℝ) : ℝ := 8 * Real.sqrt (M * L) + 64 * L + +theorem confidenceDeviation_nonneg (M L : ℝ) (_hM : 0 ≤ M) (hL : 0 ≤ L) : + 0 ≤ confidenceDeviation M L := by + unfold confidenceDeviation + positivity + +/-- The explicit deviation makes the quadratic-over-linear exponent at least `L`. -/ +theorem confidenceDeviation_exponent (M L : ℝ) (hM : 0 < M) (hL : 0 ≤ L) : + L ≤ (confidenceDeviation M L) ^ 2 / (32 * (M + confidenceDeviation M L)) := by + have hs := confidenceDeviation_nonneg M L hM.le hL + apply (le_div_iff₀ (show 0 < 32 * (M + confidenceDeviation M L) by positivity)).2 + have hroot := Real.sqrt_nonneg (M * L) + have hsquare := Real.sq_sqrt (mul_nonneg hM.le hL) + have hproduct := mul_nonneg hL hroot + unfold confidenceDeviation + nlinarith [sq_nonneg L, mul_nonneg hM.le hL] + +/-- A square-root-plus-linear budget achieves tail `exp(-L)`. -/ +theorem confidence_exp_bound {α : Type*} (indices : Finset α) (p : α → ℝ) + (M L : ℝ) (T : ℕ) (hM : 0 < M) (hL : 0 ≤ L) + (hp : ∀ i ∈ indices, (1 / 4 : ℝ) ≤ p i) + (hmean : (∑ i ∈ indices, 1 / p i) ≤ M) + (hT : M + confidenceDeviation M L ≤ (T : ℝ)) : + (∏ i ∈ indices, (1 - chosenTilt M (confidenceDeviation M L) / p i)⁻¹) * + (1 - chosenTilt M (confidenceDeviation M L)) ^ T ≤ Real.exp (-L) := by + apply (sharp_tail_bound indices p M _ T hM + (confidenceDeviation_nonneg M L hM.le hL) hp hmean hT).trans + exact Real.exp_le_exp.mpr (neg_le_neg (confidenceDeviation_exponent M L hM hL)) + +/-- The numerical confidence guarantee with `L = log(1/δ)`. -/ +theorem confidence_tail_bound {α : Type*} (indices : Finset α) (p : α → ℝ) + (M δ : ℝ) (T : ℕ) (hM : 0 < M) (hδ : 0 < δ) (hδmax : δ ≤ 1) + (hp : ∀ i ∈ indices, (1 / 4 : ℝ) ≤ p i) + (hmean : (∑ i ∈ indices, 1 / p i) ≤ M) + (hT : M + confidenceDeviation M (Real.log (1 / δ)) ≤ (T : ℝ)) : + (∏ i ∈ indices, (1 - chosenTilt M (confidenceDeviation M (Real.log (1 / δ))) / p i)⁻¹) * + (1 - chosenTilt M (confidenceDeviation M (Real.log (1 / δ)))) ^ T ≤ δ := by + have hlog : 0 ≤ Real.log (1 / δ) := by + apply Real.log_nonneg + apply (le_div_iff₀ hδ).2 + simpa using hδmax + calc + _ ≤ Real.exp (-Real.log (1 / δ)) := + confidence_exp_bound indices p M _ T hM hlog hp hmean hT + _ = δ := by rw [Real.exp_neg, Real.exp_log (by positivity)]; simp + +/-- A natural-number budget with leading term `M`. -/ +def confidenceBudget (M δ : ℝ) : ℕ := + ⌈M + confidenceDeviation M (Real.log (1 / δ))⌉₊ + +theorem confidenceBudget_sufficient {α : Type*} (indices : Finset α) (p : α → ℝ) + (M δ : ℝ) (hM : 0 < M) (hδ : 0 < δ) (hδmax : δ ≤ 1) + (hp : ∀ i ∈ indices, (1 / 4 : ℝ) ≤ p i) + (hmean : (∑ i ∈ indices, 1 / p i) ≤ M) : + (∏ i ∈ indices, (1 - chosenTilt M (confidenceDeviation M (Real.log (1 / δ))) / p i)⁻¹) * + (1 - chosenTilt M (confidenceDeviation M (Real.log (1 / δ)))) ^ + confidenceBudget M δ ≤ δ := by + apply confidence_tail_bound indices p M δ _ hM hδ hδmax hp hmean + exact Nat.le_ceil _ + +/-- The exact learner's reciprocal progress sum is at most `2n + 4`, even +when its current rank `r` is smaller than the qubit count `n`. -/ +theorem exact_rate_sum_bound (r n : ℕ) (hrn : r ≤ n) : + (∑ j ∈ Finset.range r, + 1 / FiniteProbability.progressProbability (j + 1)) ≤ 2 * (n : ℝ) + 4 := by + have hsum := FiniteProbability.reciprocal_sum_lt_two_n_add_four r + have hrnReal : (r : ℝ) ≤ n := by exact_mod_cast hrn + have hid : (∑ j ∈ Finset.range r, + 1 / FiniteProbability.progressProbability (j + 1)) = + ∑ j ∈ Finset.range r, 2 / (1 - (1 / 2 : ℝ) ^ (j + 1)) := by + apply Finset.sum_congr rfl + intro j _ + simp [FiniteProbability.progressProbability] + rw [hid] + linarith + +end LeanPool.SingleCopyStabilizer.GeometricTailBounds diff --git a/LeanPool/SingleCopyStabilizer/HadamardCoefficient.lean b/LeanPool/SingleCopyStabilizer/HadamardCoefficient.lean new file mode 100644 index 0000000000..16a52abb19 --- /dev/null +++ b/LeanPool/SingleCopyStabilizer/HadamardCoefficient.lean @@ -0,0 +1,31 @@ +/- +Copyright (c) 2026 Antonio Anna Mele. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Antonio Anna Mele +-/ +module + +public import Mathlib.Basic.Complex.Basic +public import Mathlib.Analysis.Real.Sqrt + +/-! The normalization coefficient for arbitrary-qubit Hadamard actions. -/ + +@[expose] public section + +noncomputable section +namespace LeanPool.SingleCopyStabilizer.QubitGates + +/-- The positive real coefficient `1 / √2`, regarded as a complex number. -/ +def hadamardCoefficient : ℂ := (Real.sqrt (1 / 2 : ℝ) : ℂ) + +lemma hadamardCoefficient_mul : + hadamardCoefficient * hadamardCoefficient = (1 / 2 : ℂ) := by + unfold hadamardCoefficient + rw [← Complex.ofReal_mul, Real.mul_self_sqrt (by norm_num : (0 : ℝ) ≤ 1 / 2)] + norm_num + +@[simp] lemma hadamardCoefficient_star : + star hadamardCoefficient = hadamardCoefficient := by + simp [hadamardCoefficient] + +end LeanPool.SingleCopyStabilizer.QubitGates diff --git a/LeanPool/SingleCopyStabilizer/Imports.lean b/LeanPool/SingleCopyStabilizer/Imports.lean new file mode 100644 index 0000000000..b94cfae133 --- /dev/null +++ b/LeanPool/SingleCopyStabilizer/Imports.lean @@ -0,0 +1,32 @@ +/- +Copyright (c) 2026 Lean Pool contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lean Pool contributors +-/ +module -- shake: keep-all --deprecated_module: ignore + +-- Generated project imports; run `lake exe mk_all`. +public import LeanPool.SingleCopyStabilizer +public import LeanPool.SingleCopyStabilizer.AdaptiveProcess +public import LeanPool.SingleCopyStabilizer.CNOTAction +public import LeanPool.SingleCopyStabilizer.Circuit +public import LeanPool.SingleCopyStabilizer.CliffordAction +public import LeanPool.SingleCopyStabilizer.ExactLearning +public import LeanPool.SingleCopyStabilizer.ExactLearningTheorem +public import LeanPool.SingleCopyStabilizer.ExactResources +public import LeanPool.SingleCopyStabilizer.FiniteProbability +public import LeanPool.SingleCopyStabilizer.GeometricDomination +public import LeanPool.SingleCopyStabilizer.GeometricTailBounds +public import LeanPool.SingleCopyStabilizer.HadamardCoefficient +public import LeanPool.SingleCopyStabilizer.InstructionSemantics +public import LeanPool.SingleCopyStabilizer.Measurement +public import LeanPool.SingleCopyStabilizer.OutputCorrectness +public import LeanPool.SingleCopyStabilizer.PhysicalExactLearning +public import LeanPool.SingleCopyStabilizer.PhysicalSampling +public import LeanPool.SingleCopyStabilizer.Projection +public import LeanPool.SingleCopyStabilizer.QuantumRound +public import LeanPool.SingleCopyStabilizer.Round +public import LeanPool.SingleCopyStabilizer.SharpExactLearning +public import LeanPool.SingleCopyStabilizer.StabilizerState +public import LeanPool.SingleCopyStabilizer.Symplectic +public import LeanPool.SingleCopyStabilizer.Transcript diff --git a/LeanPool/SingleCopyStabilizer/InstructionSemantics.lean b/LeanPool/SingleCopyStabilizer/InstructionSemantics.lean new file mode 100644 index 0000000000..c817c910be --- /dev/null +++ b/LeanPool/SingleCopyStabilizer/InstructionSemantics.lean @@ -0,0 +1,211 @@ +/- +Copyright (c) 2026 Antonio Anna Mele. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Antonio Anna Mele +-/ +module + +public import LeanPool.SingleCopyStabilizer.ExactResources +public import LeanPool.SingleCopyStabilizer.Circuit + + +/-! +# Elementary gate semantics of the recorded learning circuit + +The instruction lists counted in `ExactResources` denote exactly the +complex-linear Clifford operations in `Circuit`. In particular the counted +individual CNOTs implement the simultaneous target-mask operation. +-/ + +@[expose] public section + +noncomputable section + + +namespace LeanPool.SingleCopyStabilizer.InstructionSemantics + +open Measurement CNOTAction CliffordAction Circuit ExactResources + +variable {ι : Type*} [Fintype ι] [DecidableEq ι] + +/-- A CNOT's control and target must be distinct. -/ +def WellFormed : Instruction ι → Prop + | .cnot i j => i ≠ j + | .phase _ => True + | .hadamard _ => True + +/-- Elementary physical gate interpretation. A malformed self-target CNOT is +totalized as the identity; generated instruction lists never use that case. -/ +def instructionEquiv : Instruction ι → (Amplitude ι ≃ₗ[ℂ] Amplitude ι) + | .cnot i j => if h : j = i then LinearEquiv.refl ℂ _ + else cnotEquiv i (Pi.single j 1) (by simp [Ne.symm h]) + | .phase i => localPhaseLinearEquiv i + | .hadamard i => localHadamardLinearEquiv i + +omit [Fintype ι] in +theorem instructionEquiv_cnot_of_ne (i j : ι) (h : j ≠ i) : + instructionEquiv (.cnot i j) = + cnotEquiv i (Pi.single j 1) (by simp [Ne.symm h]) := by + classical + simp [instructionEquiv, h] + +/-- Chronological composition of elementary instructions. -/ +def instructionsEquiv : List (Instruction ι) → (Amplitude ι ≃ₗ[ℂ] Amplitude ι) + | [] => LinearEquiv.refl ℂ _ + | g :: gs => (instructionEquiv g).trans (instructionsEquiv gs) + +omit [Fintype ι] in +@[simp] theorem instructionsEquiv_nil : + instructionsEquiv ([] : List (Instruction ι)) = LinearEquiv.refl ℂ _ := rfl + +omit [Fintype ι] in +@[simp] theorem instructionsEquiv_cons (g : Instruction ι) (gs : List (Instruction ι)) : + instructionsEquiv (g :: gs) = (instructionEquiv g).trans (instructionsEquiv gs) := rfl + +omit [Fintype ι] in +theorem instructionsEquiv_append (xs ys : List (Instruction ι)) : + instructionsEquiv (xs ++ ys) = (instructionsEquiv xs).trans (instructionsEquiv ys) := by + classical + induction xs with + | nil => rfl + | cons g gs ih => + ext ψ x + simp only [List.cons_append, instructionsEquiv_cons, ih, LinearEquiv.trans_apply] + +omit [DecidableEq ι] [Fintype ι] in +/-- CNOT masks sharing a control add under composition. -/ +theorem cnotEquiv_trans (i : ι) (w v : Bits ι) (hw : w i = 0) (hv : v i = 0) : + (cnotEquiv i w hw).trans (cnotEquiv i v hv) = + cnotEquiv i (w + v) (by simp [hw, hv]) := by + classical + ext ψ x + change ψ ((x + x i • v) + (x + x i • v) i • w) = ψ (x + x i • (w + v)) + congr 1 + ext j + simp only [Pi.add_apply, Pi.smul_apply, smul_eq_mul, hv, mul_zero, add_zero] + ring + +omit [DecidableEq ι] [Fintype ι] in +@[simp] theorem cnotEquiv_zero (i : ι) : + cnotEquiv i (0 : Bits ι) (by simp) = LinearEquiv.refl ℂ _ := by + classical + ext ψ x + change ψ (x + x i • (0 : Bits ι)) = ψ x + simp + +/-- Mask obtained from a list of CNOT targets, counting repeated targets +modulo two. -/ +def targetMask (targets : List ι) : Bits ι := + (targets.map (fun j => (Pi.single j 1 : Bits ι))).sum + +omit [Fintype ι] in +theorem targetMask_control_zero (i : ι) (targets : List ι) (hi : i ∉ targets) : + targetMask targets i = 0 := by + classical + induction targets with + | nil => simp [targetMask] + | cons j js ih => + have hij : i ≠ j := by + intro h + exact hi (by simp [h]) + have hin : i ∉ js := by intro h; exact hi (List.mem_cons_of_mem j h) + simpa [targetMask, hij] using ih hin + +omit [Fintype ι] in +/-- A list of single-target CNOTs realizes its simultaneous target mask. -/ +theorem instructionsEquiv_cnots (i : ι) (targets : List ι) (hi : i ∉ targets) : + instructionsEquiv (targets.map (Instruction.cnot i)) = + cnotEquiv i (targetMask targets) (targetMask_control_zero i targets hi) := by + classical + induction targets with + | nil => simp [targetMask] + | cons j js ih => + have hji : j ≠ i := by + intro h + subst j + exact hi (by simp) + have hin : i ∉ js := by intro h; exact hi (List.mem_cons_of_mem j h) + rw [List.map_cons, instructionsEquiv_cons, instructionEquiv_cnot_of_ne i j hji, + ih hin, cnotEquiv_trans] + rfl + +theorem pivot_not_mem_targets (u : Bits ι) (i : ι) : i ∉ cnotTargets u i := by + simp [cnotTargets] + +theorem roundInstructions_wellFormed (outcome : RoundOutcome ι) + (g : Instruction ι) (hg : g ∈ roundInstructions outcome) : WellFormed g := by + by_cases hu : outcome.1 = 0 + · simp [roundInstructions, hu] at hg + · simp only [roundInstructions, dite_eq_right hu, List.mem_append] at hg + rcases hg with (hg | hg) | hg + · obtain ⟨j, hj, rfl⟩ := List.mem_map.mp hg + have ht : j ∈ cnotTargets outcome.1 (binaryPivot outcome.1 hu) := by simpa using hj + exact Ne.symm (Finset.mem_filter.mp ht).2.1 + · by_cases hb : outcome.2 = 0 + · simp [hb] at hg + · simp only [hb, ite_false, List.mem_singleton] at hg + subst g + trivial + · simp only [List.mem_singleton] at hg + subst g + trivial + +/-- For a pivot bit equal to one, the elementary target list is exactly the +paper's mask `u - eᵢ`. -/ +theorem cnotTargets_mask (u : Bits ι) (i : ι) (hu : u i = 1) : + targetMask (cnotTargets u i).toList = u - Pi.single i 1 := by + unfold targetMask + rw [Finset.sum_map_toList] + ext j + rw [Finset.sum_apply] + by_cases hji : j = i + · subst j + simp [cnotTargets, hu] + · have hui : u j = 0 ∨ u j = 1 := CliffordAction.bit_eq_zero_or_one (u j) + rcases hui with hj | hj + · simp [cnotTargets, Pi.single_apply, hji, hj] + · simp [cnotTargets, Pi.single_apply, hji, hj] + +theorem instructionsEquiv_cnotTargets (u : Bits ι) (i : ι) (hu : u i = 1) : + instructionsEquiv ((cnotTargets u i).toList.map (Instruction.cnot i)) = + cnotEquiv i (u - Pi.single i 1) (by simp [hu]) := by + rw [instructionsEquiv_cnots i _ (by simpa using pivot_not_mem_targets u i)] + congr 1 + exact cnotTargets_mask u i hu + +/-- The counted elementary instructions implement exactly one physical +learning round, including its zero-difference branch. -/ +theorem roundInstructions_denote (outcome : RoundOutcome ι) : + instructionsEquiv (roundInstructions outcome) = roundEquiv outcome.1 outcome.2 := by + by_cases hu : outcome.1 = 0 + · simp [roundInstructions, roundEquiv, hu] + · simp only [roundInstructions, dite_eq_right hu, instructionsEquiv_append] + rw [instructionsEquiv_cnotTargets _ _ (binaryPivot_spec _ hu)] + ext ψ x + by_cases hb : outcome.2 = 0 <;> + simp [roundEquiv, hu, correctionEquiv, hb, instructionsEquiv, instructionEquiv] + +/-- The complete counted elementary circuit implements exactly the same +operation as the recorded outcome circuit used by the decoder. -/ +theorem circuitInstructions_denote (outcomes : List (RoundOutcome ι)) : + instructionsEquiv (circuitInstructions outcomes) = circuitEquiv outcomes := by + induction outcomes with + | nil => rfl + | cons outcome outcomes ih => + change instructionsEquiv (roundInstructions outcome ++ circuitInstructions outcomes) = _ + rw [instructionsEquiv_append, roundInstructions_denote, ih] + rfl + +theorem circuitInstructions_wellFormed (outcomes : List (RoundOutcome ι)) + (g : Instruction ι) (hg : g ∈ circuitInstructions outcomes) : WellFormed g := by + obtain ⟨outcome, _, hg⟩ := List.mem_flatMap.mp hg + exact roundInstructions_wellFormed outcome g hg + +/-- The learned amplitude is exactly the inverse of the counted elementary +instruction circuit, applied to the final computational basis string. -/ +theorem decode_eq_inverse_instructions (outcomes : List (RoundOutcome ι)) (z : Bits ι) : + decode outcomes z = (instructionsEquiv (circuitInstructions outcomes)).symm (basis z) := by + rw [circuitInstructions_denote] + rfl + +end LeanPool.SingleCopyStabilizer.InstructionSemantics diff --git a/LeanPool/SingleCopyStabilizer/Measurement.lean b/LeanPool/SingleCopyStabilizer/Measurement.lean new file mode 100644 index 0000000000..4e4e989e8c --- /dev/null +++ b/LeanPool/SingleCopyStabilizer/Measurement.lean @@ -0,0 +1,339 @@ +/- +Copyright (c) 2026 Antonio Anna Mele. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Antonio Anna Mele +-/ +module + +public import Mathlib.Basic.Complex.Basic +public import Mathlib.Data.ZMod.Basic +public import Mathlib.LinearAlgebra.Matrix.DotProduct +public import Mathlib.Probability.Distributions.Uniform +public import Mathlib.Tactic.Abel +public import Mathlib.Tactic.FieldSimp +public import Mathlib.Tactic.NormNum +public import Mathlib.Tactic.Ring + + +/-! +# Amplitudes, Pauli eigenvectors, and computational measurement weights + +An amplitude is a complex function on binary strings. Computational outcome +weights are defined by the Born rule `Complex.normSq`; normalization is the +finite sum of those weights. The Pauli action is the explicit action of XᵘZᵛ +on amplitudes, not an assumed measurement-distribution property. +-/ + +@[expose] public section + + +noncomputable section + +namespace LeanPool.SingleCopyStabilizer.Measurement + +open scoped BigOperators + +/-- Computational-basis strings indexed by qubit sites. -/ +abbrev Bits (ι : Type*) := ι → ZMod 2 +/-- Complex amplitudes on the computational basis. -/ +abbrev Amplitude (ι : Type*) := Bits ι → ℂ + +/-- The binary character `(-1)^a`, without choosing integer representatives. -/ +def paritySign (a : ZMod 2) : ℂ := if a = 0 then 1 else -1 + +@[simp] theorem paritySign_normSq (a : ZMod 2) : + Complex.normSq (paritySign a) = 1 := by + by_cases ha : a = 0 <;> simp [paritySign, ha] + +theorem paritySign_injective : Function.Injective paritySign := by + intro a b h + have bits : ∀ x : ZMod 2, x = 0 ∨ x = 1 := by decide + rcases bits a with rfl | rfl <;> rcases bits b with rfl | rfl <;> + norm_num [paritySign] at * + +variable {ι : Type*} [Fintype ι] [DecidableEq ι] + +/-- Born probability weight of a computational-basis outcome. -/ +def bornWeight (ψ : Amplitude ι) (x : Bits ι) : ℝ := Complex.normSq (ψ x) + +/-- Normalization of the finite Born weights to total mass one. -/ +def IsNormalized (ψ : Amplitude ι) : Prop := ∑ x, bornWeight ψ x = 1 + +omit [DecidableEq ι] [Fintype ι] in +theorem bornWeight_nonneg (ψ : Amplitude ι) (x : Bits ι) : + 0 ≤ bornWeight ψ x := Complex.normSq_nonneg _ + +omit [DecidableEq ι] [Fintype ι] in +@[simp] theorem bornWeight_pos (ψ : Amplitude ι) (x : Bits ι) : + 0 < bornWeight ψ x ↔ ψ x ≠ 0 := Complex.normSq_pos + +omit [DecidableEq ι] [Fintype ι] in +@[simp] theorem bornWeight_eq_zero (ψ : Amplitude ι) (x : Bits ι) : + bornWeight ψ x = 0 ↔ ψ x = 0 := Complex.normSq_eq_zero + +/-- Normalized amplitudes determine a mathlib probability mass function. -/ +def bornPMF (ψ : Amplitude ι) (hψ : IsNormalized ψ) : PMF (Bits ι) := + PMF.ofFintype (fun x => ENNReal.ofReal (bornWeight ψ x)) (by + rw [← ENNReal.ofReal_sum_of_nonneg (fun x _ => bornWeight_nonneg ψ x)] + rw [hψ] + exact ENNReal.ofReal_one) + +@[simp] theorem bornPMF_apply (ψ : Amplitude ι) (hψ : IsNormalized ψ) + (x : Bits ι) : bornPMF ψ hψ x = ENNReal.ofReal (bornWeight ψ x) := rfl + +/-- `(Xᵘ Zᵛ ψ)(x) = (-1)^(v·(x-u)) ψ(x-u)`, in the conventional +operator order. The source basis vector `x-u` is first phased, then shifted. -/ +def pauliAction (u v : Bits ι) (ψ : Amplitude ι) (x : Bits ι) : ℂ := + paritySign (v ⬝ᵥ (x - u)) * ψ (x - u) + +/-- The explicit action is complex-linear. -/ +def pauliOperator (u v : Bits ι) : Amplitude ι →ₗ[ℂ] Amplitude ι where + toFun := pauliAction u v + map_add' ψ φ := by + ext x + simp [pauliAction, mul_add] + map_smul' c ψ := by + ext x + simp [pauliAction] + ring + +/-- The eigenvector premise is a pointwise equality of explicitly defined +linear-operator amplitudes. -/ +def IsPauliEigenvector (ψ : Amplitude ι) (u v : Bits ι) (ζ : ℂ) : Prop := + ∀ x, pauliAction u v ψ x = ζ * ψ x + +theorem pauliAction_norm_preserving (u v : Bits ι) (ψ : Amplitude ι) : + (∑ x, bornWeight (pauliAction u v ψ) x) = ∑ x, bornWeight ψ x := by + simp only [bornWeight, pauliAction, Complex.normSq_mul, paritySign_normSq, one_mul] + exact Fintype.sum_equiv (Equiv.subRight u) _ _ (fun _ => rfl) + +theorem pauliAction_preserves_normalization (u v : Bits ι) (ψ : Amplitude ι) + (hψ : IsNormalized ψ) : IsNormalized (pauliAction u v ψ) := by + unfold IsNormalized + rw [pauliAction_norm_preserving] + exact hψ + +/-- A normalized eigenvector of this explicit Pauli operator necessarily has +a unit-modulus eigenvalue. No unit-modulus assumption is required. -/ +theorem eigenvalue_normSq_eq_one (ψ : Amplitude ι) (hψ : IsNormalized ψ) + (u v : Bits ι) (ζ : ℂ) (heig : IsPauliEigenvector ψ u v ζ) : + Complex.normSq ζ = 1 := by + have h := pauliAction_norm_preserving u v ψ + simp only [bornWeight] at h + have heq : pauliAction u v ψ = fun x => ζ * ψ x := funext heig + rw [heq] at h + simp only [Complex.normSq_mul] at h + rw [← Finset.mul_sum] at h + change Complex.normSq ζ * (∑ x, bornWeight ψ x) = ∑ x, bornWeight ψ x at h + rw [hψ, mul_one] at h + exact h + +/-- Stabilizer X labels act as translation symmetries of the computational +probabilities. This follows from the amplitude equation by taking norm squares. -/ +theorem eigenvector_bornWeight_translation (ψ : Amplitude ι) (hψ : IsNormalized ψ) + (u v : Bits ι) (ζ : ℂ) (heig : IsPauliEigenvector ψ u v ζ) + (x : Bits ι) : bornWeight ψ (x + u) = bornWeight ψ x := by + have h := congrArg Complex.normSq (heig (x + u)) + have hζ := eigenvalue_normSq_eq_one ψ hψ u v ζ heig + simpa [pauliAction, Complex.normSq_mul, hζ, bornWeight] using h.symm + +omit [DecidableEq ι] in +/-- At a nonzero amplitude of a diagonal Pauli eigenvector, the parity +character is forced to equal the eigenvalue. -/ +theorem diagonal_eigenvalue_at_nonzero (ψ : Amplitude ι) (s : Bits ι) (ζ : ℂ) + (heig : IsPauliEigenvector ψ 0 s ζ) (x : Bits ι) (hx : ψ x ≠ 0) : + paritySign (s ⬝ᵥ x) = ζ := by + classical + have h := heig x + simp only [pauliAction, sub_zero] at h + exact mul_right_cancel₀ hx h + +omit [DecidableEq ι] in +/-- Two outcomes in the amplitude support of a diagonal eigenvector have +the same parity, so their difference is orthogonal to its Z label. -/ +theorem diagonal_eigenvector_difference (ψ : Amplitude ι) (s : Bits ι) (ζ : ℂ) + (heig : IsPauliEigenvector ψ 0 s ζ) (x y : Bits ι) + (hx : ψ x ≠ 0) (hy : ψ y ≠ 0) : s ⬝ᵥ (x - y) = 0 := by + classical + have hxζ := diagonal_eigenvalue_at_nonzero ψ s ζ heig x hx + have hyζ := diagonal_eigenvalue_at_nonzero ψ s ζ heig y hy + have hxy : s ⬝ᵥ x = s ⬝ᵥ y := paritySign_injective (hxζ.trans hyζ.symm) + rw [dotProduct_sub, hxy, sub_self] + +/-- The orthogonal complement written directly in binary dot products. -/ +def orthogonalSet (D : Set (Bits ι)) : Set (Bits ι) := + {u | ∀ s ∈ D, s ⬝ᵥ u = 0} + +/-- The diagonal annihilator is an additive subgroup, without needing to +assume that the supplied collection D is itself a subspace. -/ +def orthogonalSubgroup (D : Set (Bits ι)) : AddSubgroup (Bits ι) where + carrier := orthogonalSet D + zero_mem' := by intro s _; simp + add_mem' hu hv := by + intro s hs + rw [dotProduct_add, hu s hs, hv s hs, add_zero] + neg_mem' hu := by + intro s hs + simpa only [dotProduct_neg, hu s hs] using (neg_zero : -(0 : ZMod 2) = 0) + +omit [DecidableEq ι] in +@[simp] theorem mem_orthogonalSubgroup (D : Set (Bits ι)) (u : Bits ι) : + u ∈ orthogonalSubgroup D ↔ u ∈ orthogonalSet D := Iff.rfl + +omit [DecidableEq ι] in +/-- Every computational difference lies in the annihilator of all diagonal +stabilizers, even when the state has positive stabilizer nullity. -/ +theorem supported_difference_orthogonal (ψ : Amplitude ι) (D : Set (Bits ι)) + (hD : ∀ s ∈ D, ∃ ζ, IsPauliEigenvector ψ 0 s ζ) + (x y : Bits ι) (hx : ψ x ≠ 0) (hy : ψ y ≠ 0) : + x - y ∈ orthogonalSet D := by + classical + intro s hs + obtain ⟨ζ, heig⟩ := hD s hs + exact diagonal_eigenvector_difference ψ s ζ heig x y hx hy + +omit [DecidableEq ι] in +/-- The same guarantee stated in terms of positive-probability outcomes. -/ +theorem positive_probability_difference_orthogonal (ψ : Amplitude ι) + (D : Set (Bits ι)) (hD : ∀ s ∈ D, ∃ ζ, IsPauliEigenvector ψ 0 s ζ) + (x y : Bits ι) (hx : 0 < bornWeight ψ x) (hy : 0 < bornWeight ψ y) : + x - y ∈ orthogonalSet D := + supported_difference_orthogonal ψ D hD x y + ((bornWeight_pos ψ x).mp hx) ((bornWeight_pos ψ y).mp hy) + +omit [DecidableEq ι] in +/-- Choosing any supported basepoint places the entire amplitude support in +one affine coset of the diagonal annihilator. -/ +theorem support_in_affine_annihilator (ψ : Amplitude ι) (D : Set (Bits ι)) + (hD : ∀ s ∈ D, ∃ ζ, IsPauliEigenvector ψ 0 s ζ) + (z : Bits ι) (hz : ψ z ≠ 0) : + ∀ x, ψ x ≠ 0 → x - z ∈ orthogonalSet D := by + classical + intro x hx + exact supported_difference_orthogonal ψ D hD x z hx hz + +/-- A collection of actual Pauli eigenlabels gives probability invariance +under every translation in their X projection. -/ +theorem bornWeight_invariant_of_eigenlabels (ψ : Amplitude ι) + (hψ : IsNormalized ψ) (V : Set (Bits ι)) + (hV : ∀ u ∈ V, ∃ v ζ, IsPauliEigenvector ψ u v ζ) : + ∀ u ∈ V, ∀ x, bornWeight ψ (x + u) = bornWeight ψ x := by + intro u hu x + obtain ⟨v, ζ, heig⟩ := hV u hu + exact eigenvector_bornWeight_translation ψ hψ u v ζ heig x + +/-- The finite affine coset `z + V`, expressed by subtraction. -/ +def affineCoset (V : AddSubgroup (Bits ι)) (z : Bits ι) : Finset (Bits ι) := by + classical + exact Finset.univ.filter (fun x => x - z ∈ V) + +@[simp] theorem mem_affineCoset (V : AddSubgroup (Bits ι)) (z x : Bits ι) : + x ∈ affineCoset V z ↔ x - z ∈ V := by + classical + simp [affineCoset] + +theorem affineCoset_card (V : AddSubgroup (Bits ι)) (z : Bits ι) : + (affineCoset V z).card = Nat.card V := by + classical + let e : V ≃ ↥(affineCoset V z) := { + toFun := fun u => ⟨z + u, by + apply (mem_affineCoset V z _).mpr + convert u.property using 1 + abel⟩ + invFun := fun x => ⟨x - z, (mem_affineCoset V z x).mp x.property⟩ + left_inv := by intro u; apply Subtype.ext; dsimp; abel + right_inv := by intro x; apply Subtype.ext; dsimp; abel } + simpa only [Nat.card_eq_fintype_card, Fintype.card_coe] using (Fintype.card_congr e).symm + +/-- Invariance under all translations in V makes weights constant on every +affine V-coset, even if different cosets have different masses. -/ +theorem bornWeight_constant_on_affineCoset (ψ : Amplitude ι) + (V : AddSubgroup (Bits ι)) + (hinv : ∀ u ∈ V, ∀ x, bornWeight ψ (x + u) = bornWeight ψ x) + (z x : Bits ι) (hx : x ∈ affineCoset V z) : + bornWeight ψ x = bornWeight ψ z := by + have h := hinv (x - z) ((mem_affineCoset V z x).mp hx) z + have heq : z + (x - z) = x := by abel + simpa only [heq] using h + +/-- If the support is confined to one coset and every translation in its +direction space preserves probabilities, normalization forces the uniform +distribution on that coset. This is a derived Born-weight statement. -/ +theorem bornWeight_uniform_affineCoset (ψ : Amplitude ι) (hψ : IsNormalized ψ) + (V : AddSubgroup (Bits ι)) (z : Bits ι) + (hsupp : ∀ x, ψ x ≠ 0 → x - z ∈ V) + (hinv : ∀ u ∈ V, ∀ x, bornWeight ψ (x + u) = bornWeight ψ x) + (x : Bits ι) (hx : x ∈ affineCoset V z) : + bornWeight ψ x = 1 / (Nat.card V : ℝ) := by + classical + have hsum : (∑ y ∈ affineCoset V z, bornWeight ψ y) = 1 := by + calc + (∑ y ∈ affineCoset V z, bornWeight ψ y) = ∑ y, bornWeight ψ y := by + apply Finset.sum_subset (Finset.subset_univ _) + intro y _ hy + apply (bornWeight_eq_zero ψ y).mpr + by_contra hny + exact hy ((mem_affineCoset V z y).mpr (hsupp y hny)) + _ = 1 := hψ + have hconst : (∑ y ∈ affineCoset V z, bornWeight ψ y) = + (Nat.card V : ℝ) * bornWeight ψ z := by + calc + (∑ y ∈ affineCoset V z, bornWeight ψ y) = + ∑ _y ∈ affineCoset V z, bornWeight ψ z := by + apply Finset.sum_congr rfl + intro y hy + exact bornWeight_constant_on_affineCoset ψ V hinv z y hy + _ = _ := by simp [affineCoset_card, nsmul_eq_mul] + have hc : (Nat.card V : ℝ) ≠ 0 := by + simp only [Nat.card_eq_fintype_card] + exact_mod_cast Fintype.card_ne_zero + rw [bornWeight_constant_on_affineCoset ψ V hinv z x hx] + apply (eq_div_iff hc).mpr + rw [mul_comm, ← hconst, hsum] + +/-- The complete distribution, including its zero weights outside the coset. -/ +theorem bornWeight_uniform_affineCoset_ite (ψ : Amplitude ι) (hψ : IsNormalized ψ) + (V : AddSubgroup (Bits ι)) (z : Bits ι) + (hsupp : ∀ x, ψ x ≠ 0 → x - z ∈ V) + (hinv : ∀ u ∈ V, ∀ x, bornWeight ψ (x + u) = bornWeight ψ x) + (x : Bits ι) : + bornWeight ψ x = if x ∈ affineCoset V z then 1 / (Nat.card V : ℝ) else 0 := by + classical + by_cases hx : x ∈ affineCoset V z + · rw [ite_eq_left hx] + exact bornWeight_uniform_affineCoset ψ hψ V z hsupp hinv x hx + · rw [ite_eq_right hx] + apply (bornWeight_eq_zero ψ x).mpr + by_contra hnx + exact hx ((mem_affineCoset V z x).mpr (hsupp x hnx)) + +theorem normalized_has_nonzero_amplitude (ψ : Amplitude ι) (hψ : IsNormalized ψ) : + ∃ z, ψ z ≠ 0 := by + by_contra! hzero + have hsum : (∑ x, bornWeight ψ x) = 0 := by simp [bornWeight, hzero] + rw [hψ] at hsum + norm_num at hsum + +/-- Operational uniform-support consequence of a complete collection of +Pauli eigenlabels. Diagonal eigenlabels confine the support, and a Pauli +eigenlabel above every direction in their annihilator forces uniformity. +The latter existence premise is the algebraic X-projection theorem for a +maximal stabilizer space; no probability-uniformity hypothesis is assumed. -/ +theorem uniform_bornWeight_of_complete_eigenlabels (ψ : Amplitude ι) + (hψ : IsNormalized ψ) (D : Set (Bits ι)) + (hD : ∀ s ∈ D, ∃ ζ, IsPauliEigenvector ψ 0 s ζ) + (hX : ∀ u ∈ orthogonalSubgroup D, ∃ v ζ, IsPauliEigenvector ψ u v ζ) : + ∃ z, ∀ x, bornWeight ψ x = + if x ∈ affineCoset (orthogonalSubgroup D) z then + 1 / (Nat.card (orthogonalSubgroup D) : ℝ) else 0 := by + classical + obtain ⟨z, hz⟩ := normalized_has_nonzero_amplitude ψ hψ + refine ⟨z, ?_⟩ + intro x + apply bornWeight_uniform_affineCoset_ite ψ hψ (orthogonalSubgroup D) z + · exact support_in_affine_annihilator ψ D hD z hz + · intro u hu y + obtain ⟨v, ζ, heig⟩ := hX u hu + exact eigenvector_bornWeight_translation ψ hψ u v ζ heig y + +end LeanPool.SingleCopyStabilizer.Measurement diff --git a/LeanPool/SingleCopyStabilizer/OutputCorrectness.lean b/LeanPool/SingleCopyStabilizer/OutputCorrectness.lean new file mode 100644 index 0000000000..e05740955d --- /dev/null +++ b/LeanPool/SingleCopyStabilizer/OutputCorrectness.lean @@ -0,0 +1,231 @@ +/- +Copyright (c) 2026 Antonio Anna Mele. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Antonio Anna Mele +-/ +module + +public import LeanPool.SingleCopyStabilizer.Circuit +public import LeanPool.SingleCopyStabilizer.QuantumRound +public import LeanPool.SingleCopyStabilizer.PhysicalSampling +public import LeanPool.SingleCopyStabilizer.PhysicalExactLearning + + +/-! Exact state reconstruction from the adaptive experiment's actual output. +Correctness identifies amplitudes up to a unit-modulus global scalar. -/ + +@[expose] public section + +noncomputable section + + +namespace LeanPool.SingleCopyStabilizer.OutputCorrectness + +open Measurement +open scoped BigOperators + +variable {ι : Type*} [Fintype ι] [DecidableEq ι] + +/-- Equality of pure states up to a physically irrelevant global phase. -/ +def SameRay (ψ φ : Amplitude ι) : Prop := + ∃ c : ℂ, Complex.normSq c = 1 ∧ ψ = c • φ + +omit [DecidableEq ι] [Fintype ι] in +theorem sameRay_refl (ψ : Amplitude ι) : SameRay ψ ψ := by + classical + exact ⟨1, by simp, by simp⟩ + +omit [DecidableEq ι] [Fintype ι] in +/-- Reversing a linear gate transports exactly the same global phase. -/ +theorem sameRay_inverse_iff (U : Amplitude ι ≃ₗ[ℂ] Amplitude ι) + (ψ φ : Amplitude ι) : SameRay ψ (U.symm φ) ↔ SameRay (U ψ) φ := by + classical + constructor + · rintro ⟨c, hc, h⟩ + refine ⟨c, hc, ?_⟩ + simpa only [map_smul, LinearEquiv.apply_symm_apply] using congrArg U h + · rintro ⟨c, hc, h⟩ + refine ⟨c, hc, ?_⟩ + apply U.injective + simpa only [map_smul, LinearEquiv.apply_symm_apply] using h + +theorem roundEquiv_apply (u : Bits ι) (b : ZMod 2) (ψ : Amplitude ι) : + Circuit.roundEquiv u b ψ = QuantumRound.applyRoundAmplitude u b ψ := + QuantumRound.roundEquiv_apply_eq_applyRoundAmplitude u b ψ + +/-- The actual adaptive learner's returned amplitude. The terminal experiment +reads one computational outcome. Each recursive step performs two fresh-copy +Born measurements and the correction coin, then reverses the recorded round +on the recursively decoded result. -/ +def outputPMF : ℕ → PureStabilizerState ι → PMF (Amplitude ι) + | 0, S => (bornPMF S.amplitude S.normalized).map Circuit.basis + | t + 1, S => (PhysicalSampling.outcomePMF S).bind fun o => + (outputPMF t (QuantumRound.quantumRound S o)).map (Circuit.roundEquiv o.1 o.2).symm + +/-- Finite classical output: the chronological round records and one final +computational-basis string. No unknown amplitudes are included in the output. -/ +abbrev Description (ι : Type*) := List (Circuit.Outcome ι) × Bits ι + +/-- The same physical experiment retaining its classical circuit description. -/ +def descriptionPMF : ℕ → PureStabilizerState ι → PMF (Description ι) + | 0, S => (bornPMF S.amplitude S.normalized).map fun z => ([], z) + | t + 1, S => (PhysicalSampling.outcomePMF S).bind fun o => + (descriptionPMF t (QuantumRound.quantumRound S o)).map fun d => (o :: d.1, d.2) + +/-- Interpreting the returned finite description gives exactly the amplitude +distribution in `outputPMF`. -/ +theorem descriptionPMF_decode (t : ℕ) (S : PureStabilizerState ι) : + (descriptionPMF t S).map (fun d => Circuit.decode d.1 d.2) = outputPMF t S := by + classical + induction t generalizing S with + | zero => simp [descriptionPMF, outputPMF, PMF.map_comp, Function.comp_def] + | succ t ih => + rw [descriptionPMF, PMF.map_bind, outputPMF] + congr 1 + funext o + rw [← ih, PMF.map_comp, PMF.map_comp] + congr 1 + +/-- Every classical description denotes a normalized pure state. -/ +theorem description_normalized (d : Description ι) : + IsNormalized (Circuit.decode d.1 d.2) := Circuit.decode_normalized d.1 d.2 + +/-- The learner's output distribution is supported on normalized amplitudes. -/ +theorem outputPMF_normalized (t : ℕ) (S : PureStabilizerState ι) + (ψ : Amplitude ι) (hψ : ψ ∈ (outputPMF t S).support) : IsNormalized ψ := by + classical + rw [← descriptionPMF_decode, PMF.support_map] at hψ + obtain ⟨d, _, rfl⟩ := hψ + exact description_normalized d + +open Classical in +/-- Actual probability that the output fails to represent the input state. +The Boolean pushforward avoids introducing a measure on amplitude space. -/ +def outputFailure (t : ℕ) (S : PureStabilizerState ι) : ENNReal := + ((outputPMF t S).map fun φ => decide (SameRay S.amplitude φ)) false + +/-- At full diagonal rank the single final Born readout reconstructs the +current input amplitude up to global phase with probability one. -/ +theorem outputFailure_zero_of_rank_zero (S : PureStabilizerState ι) + (hrank : ExactLearning.rank (PhysicalSampling.labels S) = 0) : + outputFailure 0 S = 0 := by + classical + have hfull := (ExactLearning.rank_zero_iff_full_diagonal + (PhysicalSampling.labels S)).mp hrank + obtain ⟨z, c, hc, hamp⟩ := full_diagonal_basis_amplitude S.amplitude S.normalized + S.labels S.eigenlabels hfull + have hray : SameRay S.amplitude (Circuit.basis z) := by + refine ⟨c, hc, ?_⟩ + simpa only [Circuit.smul_basis] using hamp + have hpmf : bornPMF S.amplitude S.normalized = PMF.pure z := by + ext x + by_cases hx : x = z + · subst x + simp [bornPMF_apply, bornWeight, hamp, hc, PMF.pure_apply] + · simp [bornPMF_apply, bornWeight, hamp, hx, PMF.pure_apply] + simp [outputFailure, outputPMF, hpmf, PMF.pure_map, hray] + +/-- The output error is the Born-weighted mean of the errors of later rounds. +Reversing a recorded Clifford cannot create a reconstruction error. -/ +theorem outputFailure_succ (t : ℕ) (S : PureStabilizerState ι) : + outputFailure (t + 1) S = ∑ o : ExactLearning.Outcome ι, + PhysicalSampling.outcomePMF S o * outputFailure t (QuantumRound.quantumRound S o) := by + classical + unfold outputFailure + rw [outputPMF, PMF.map_bind, PMF.bind_apply, tsum_fintype] + apply Finset.sum_congr rfl + intro o _ + congr 1 + rw [PMF.map_comp] + congr 2 + funext φ + simp only [Function.comp_apply, sameRay_inverse_iff, roundEquiv_apply, + QuantumRound.quantumRound_amplitude] + rfl + +/-- The probability of returning the wrong state is at most the probability +of incomplete diagonal compression in the actual physical experiment. -/ +theorem outputFailure_le_compression (t : ℕ) (S : PureStabilizerState ι) : + outputFailure t S ≤ ENNReal.ofReal (PhysicalExactLearning.failureProbability t S) := by + classical + induction t generalizing S with + | zero => + by_cases hrank : ExactLearning.rank (PhysicalSampling.labels S) = 0 + · simp [PhysicalExactLearning.failureProbability, hrank, + outputFailure_zero_of_rank_zero S hrank] + · simp only [PhysicalExactLearning.failureProbability, ite_eq_right hrank, + ENNReal.ofReal_one] + exact PMF.coe_le_one _ _ + | succ t ih => + rw [outputFailure_succ, PhysicalExactLearning.failureProbability, + ENNReal.ofReal_sum_of_nonneg (fun o _ => mul_nonneg ENNReal.toReal_nonneg + (PhysicalExactLearning.failureProbability_nonneg t (QuantumRound.quantumRound S o)))] + apply Finset.sum_le_sum + intro o _ + calc + _ ≤ PhysicalSampling.outcomePMF S o * ENNReal.ofReal + (PhysicalExactLearning.failureProbability t (QuantumRound.quantumRound S o)) := + mul_le_mul_right (ih (QuantumRound.quantumRound S o)) _ + _ = _ := by + rw [ENNReal.ofReal_mul ENNReal.toReal_nonneg, + ENNReal.ofReal_toReal (PMF.apply_ne_top _ _)] + +/-- The actual learner returns the exact input pure state up to global phase, +except with probability at most δ, at the proved leading-2n round budget. -/ +theorem exact_learning_failure_probability (S : PureStabilizerState ι) + (δ : ℝ) (hδ : 0 < δ) (hδmax : δ ≤ 1) : + outputFailure (SharpExactLearning.roundBudget (Fintype.card ι) δ) S ≤ ENNReal.ofReal δ := by + classical + exact (outputFailure_le_compression _ S).trans (ENNReal.ofReal_le_ofReal + (PhysicalExactLearning.compression_failure_probability S δ hδ hδmax)) + +theorem exact_learning_failure_probability_after_budget (S : PureStabilizerState ι) + (δ : ℝ) (hδ : 0 < δ) (hδmax : δ ≤ 1) (T : ℕ) + (hT : SharpExactLearning.roundBudget (Fintype.card ι) δ ≤ T) : + outputFailure T S ≤ ENNReal.ofReal δ := by + classical + exact (outputFailure_le_compression T S).trans (ENNReal.ofReal_le_ofReal + (PhysicalExactLearning.compression_failure_probability_after_budget S δ hδ hδmax T hT)) + +open Classical in +/-- The same correctness guarantee stated directly for the finite classical +description that the learner returns. -/ +theorem description_failure_probability (S : PureStabilizerState ι) + (δ : ℝ) (hδ : 0 < δ) (hδmax : δ ≤ 1) : + ((descriptionPMF (SharpExactLearning.roundBudget (Fintype.card ι) δ) S).map + fun d => decide (SameRay S.amplitude (Circuit.decode d.1 d.2))) false ≤ ENNReal.ofReal δ := by + classical + have h := exact_learning_failure_probability S δ hδ hδmax + unfold outputFailure at h + rw [← descriptionPMF_decode, PMF.map_comp] at h + exact h + +/-- For a Boolean correctness experiment, the success and failure +probabilities sum to one. -/ +theorem bool_success_probability_ge (p : PMF Bool) (δ : ℝ) (hδ : 0 ≤ δ) + (hfailure : p false ≤ ENNReal.ofReal δ) : 1 - δ ≤ (p true).toReal := by + classical + have hsum : p true + p false = 1 := by + have h := p.tsum_coe + rw [tsum_fintype] at h + simpa only [Fintype.sum_bool] using h + have hreal : (p true).toReal + (p false).toReal = 1 := by + rw [← ENNReal.toReal_add (p.apply_ne_top true) (p.apply_ne_top false), hsum] + simp + have hfailreal := ENNReal.toReal_mono ENNReal.ofReal_ne_top hfailure + rw [ENNReal.toReal_ofReal hδ] at hfailreal + linarith + +open Classical in +/-- Direct real-valued success guarantee for the returned classical circuit +description: it exactly represents the input pure state with probability +at least `1-δ`. -/ +theorem description_success_probability (S : PureStabilizerState ι) + (δ : ℝ) (hδ : 0 < δ) (hδmax : δ ≤ 1) : + 1 - δ ≤ (((descriptionPMF (SharpExactLearning.roundBudget (Fintype.card ι) δ) S).map + fun d => decide (SameRay S.amplitude (Circuit.decode d.1 d.2))) true).toReal := by + classical + apply bool_success_probability_ge _ δ hδ.le + exact description_failure_probability S δ hδ hδmax + +end LeanPool.SingleCopyStabilizer.OutputCorrectness diff --git a/LeanPool/SingleCopyStabilizer/PhysicalExactLearning.lean b/LeanPool/SingleCopyStabilizer/PhysicalExactLearning.lean new file mode 100644 index 0000000000..7123fc6cc1 --- /dev/null +++ b/LeanPool/SingleCopyStabilizer/PhysicalExactLearning.lean @@ -0,0 +1,87 @@ +/- +Copyright (c) 2026 Antonio Anna Mele. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Antonio Anna Mele +-/ +module + +public import LeanPool.SingleCopyStabilizer.QuantumRound +public import LeanPool.SingleCopyStabilizer.PhysicalSampling +public import LeanPool.SingleCopyStabilizer.SharpExactLearning + + +/-! The actual amplitude experiment realizes the verified label process. +Zero-probability observations are handled without consulting the unknown +stabilizer labels in the physical algorithm. -/ + +@[expose] public section + +noncomputable section + +namespace LeanPool.SingleCopyStabilizer.PhysicalExactLearning + +open Measurement PhysicalSampling QuantumRound +open scoped BigOperators + +variable {ι : Type*} [Fintype ι] [DecidableEq ι] + +/-- On every possible observation, the physical and algebraic updates agree. -/ +theorem label_next_of_supported (S : PureStabilizerState ι) + (o : ExactLearning.Outcome ι) (hu : o.1 ∈ xProjection S.labels) : + labels (quantumRound S o) = ExactLearning.next (labels S) o := by + apply Subtype.ext + change binaryRound S.labels o.1 o.2 = safeBinaryRound S.labels o.1 o.2 + exact (safeBinaryRound_of_mem S.labels o.1 o.2 hu).symm + +/-- Failure to reach full diagonal rank, evaluated on the actual Born +branching experiment with concrete CNOT and H/HS amplitude updates. -/ +def failureProbability : ℕ → PureStabilizerState ι → ℝ + | 0, S => if ExactLearning.rank (labels S) = 0 then 0 else 1 + | t + 1, S => ∑ o : ExactLearning.Outcome ι, + (outcomePMF S o).toReal * failureProbability t (quantumRound S o) + +/-- The finite tree probabilities coincide, with all sampling and physical +gate hypotheses discharged. -/ +theorem failureProbability_eq_labelProcess (t : ℕ) (S : PureStabilizerState ι) : + failureProbability t S = ExactLearning.process.failureProbability t (labels S) := by + classical + induction t generalizing S with + | zero => rfl + | succ t ih => + change (∑ o : ExactLearning.Outcome ι, + (outcomePMF S o).toReal * failureProbability t (quantumRound S o)) = + ∑ o : ExactLearning.Outcome ι, ExactLearning.weight (labels S) o * + ExactLearning.process.failureProbability t (ExactLearning.next (labels S) o) + apply Finset.sum_congr rfl + intro o _ + rw [outcomePMF_toReal, ih] + by_cases hu : o.1 ∈ xProjection S.labels + · rw [label_next_of_supported S o hu] + · simp [ExactLearning.weight, labels, hu] + +theorem failureProbability_nonneg (t : ℕ) (S : PureStabilizerState ι) : + 0 ≤ failureProbability t S := by + rw [failureProbability_eq_labelProcess] + exact ExactLearning.process.failure_probability_nonneg t (labels S) + +theorem failureProbability_le_one (t : ℕ) (S : PureStabilizerState ι) : + failureProbability t S ≤ 1 := by + rw [failureProbability_eq_labelProcess] + exact ExactLearning.process.failure_probability_le_one t (labels S) + +/-- Physical adaptive compression with a leading `2n` round budget. -/ +theorem compression_failure_probability (S : PureStabilizerState ι) + (δ : ℝ) (hδ : 0 < δ) (hδmax : δ ≤ 1) : + failureProbability (SharpExactLearning.roundBudget (Fintype.card ι) δ) S ≤ δ := by + rw [failureProbability_eq_labelProcess] + exact SharpExactLearning.compression_failure_probability (labels S) δ hδ hδmax + +theorem compression_failure_probability_after_budget (S : PureStabilizerState ι) + (δ : ℝ) (hδ : 0 < δ) (hδmax : δ ≤ 1) (T : ℕ) + (hT : SharpExactLearning.roundBudget (Fintype.card ι) δ ≤ T) : + failureProbability T S ≤ δ := by + rw [failureProbability_eq_labelProcess] + exact SharpExactLearning.compression_failure_probability_after_budget + (labels S) δ hδ hδmax T hT + +end LeanPool.SingleCopyStabilizer.PhysicalExactLearning diff --git a/LeanPool/SingleCopyStabilizer/PhysicalSampling.lean b/LeanPool/SingleCopyStabilizer/PhysicalSampling.lean new file mode 100644 index 0000000000..d3d7f27b2a --- /dev/null +++ b/LeanPool/SingleCopyStabilizer/PhysicalSampling.lean @@ -0,0 +1,79 @@ +/- +Copyright (c) 2026 Antonio Anna Mele. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Antonio Anna Mele +-/ +module + +public import LeanPool.SingleCopyStabilizer.StabilizerState +public import LeanPool.SingleCopyStabilizer.ExactLearning + + +/-! The exact round's actual two-copy Born measurements and independent +correction bit induce precisely the finite kernel used in the tail proof. -/ + +@[expose] public section + +noncomputable section + +namespace LeanPool.SingleCopyStabilizer.PhysicalSampling + +open Measurement +open scoped BigOperators + +variable {ι : Type*} [Fintype ι] [DecidableEq ι] + +/-- The Lagrangian label state underlying a physical stabilizer state. -/ +def labels (S : PureStabilizerState ι) : ExactLearning.State ι := + ⟨S.labels, S.isotropic, S.maximal⟩ + +/-- Two independent fresh computational outcomes, their difference, then +an independent fair correction bit. -/ +def outcomePMF (S : PureStabilizerState ι) : PMF (ExactLearning.Outcome ι) := + (bornDifferencePMF S.amplitude S.normalized).bind fun u => + (PMF.uniformOfFintype (ZMod 2)).map fun b => (u, b) + +omit [DecidableEq ι] in +theorem correction_map_apply (u : Bits ι) (o : ExactLearning.Outcome ι) : + ((PMF.uniformOfFintype (ZMod 2)).map fun b => (u, b)) o = + if u = o.1 then (1 / 2 : ENNReal) else 0 := by + classical + rcases o with ⟨x, c⟩ + by_cases hu : u = x + · subst u + simp [PMF.map_apply, tsum_fintype, PMF.uniformOfFintype_apply] + · simp [PMF.map_apply, tsum_fintype, hu, Ne.symm hu] + +theorem outcomePMF_apply (S : PureStabilizerState ι) (o : ExactLearning.Outcome ι) : + outcomePMF S o = bornDifferencePMF S.amplitude S.normalized o.1 / 2 := by + classical + rw [outcomePMF, PMF.bind_apply, tsum_fintype] + simp_rw [correction_map_apply] + simp [mul_ite, div_eq_mul_inv] + +/-- The label process's kernel is derived from the physical sampling PMF. -/ +theorem outcomePMF_eq_kernel (S : PureStabilizerState ι) (o : ExactLearning.Outcome ι) : + outcomePMF S o = ENNReal.ofReal (ExactLearning.weight (labels S) o) := by + classical + rw [outcomePMF_apply, S.bornDifferencePMF_uniform] + unfold ExactLearning.weight labels + dsimp only + by_cases hu : o.1 ∈ xProjection S.labels + · rw [ite_eq_left hu, ite_eq_left hu] + rw [Nat.card_eq_fintype_card] + rw [← ENNReal.ofReal_ofNat (n := 2), ← ENNReal.ofReal_div_of_pos (by norm_num : (0:ℝ) < 2)] + congr 1 + ring + · simp [hu] + +theorem outcomePMF_toReal (S : PureStabilizerState ι) (o : ExactLearning.Outcome ι) : + (outcomePMF S o).toReal = ExactLearning.weight (labels S) o := by + rw [outcomePMF_eq_kernel, ENNReal.toReal_ofReal (ExactLearning.weight_nonneg _ _)] + +theorem outcomePMF_zero_of_not_mem (S : PureStabilizerState ι) + (o : ExactLearning.Outcome ι) (hu : o.1 ∉ xProjection S.labels) : + outcomePMF S o = 0 := by + rw [outcomePMF_eq_kernel] + simp [ExactLearning.weight, labels, hu] + +end LeanPool.SingleCopyStabilizer.PhysicalSampling diff --git a/LeanPool/SingleCopyStabilizer/Projection.lean b/LeanPool/SingleCopyStabilizer/Projection.lean new file mode 100644 index 0000000000..2b7e7758a5 --- /dev/null +++ b/LeanPool/SingleCopyStabilizer/Projection.lean @@ -0,0 +1,192 @@ +/- +Copyright (c) 2026 Antonio Anna Mele. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Antonio Anna Mele +-/ +module + +public import LeanPool.SingleCopyStabilizer.Symplectic +public import Mathlib.LinearAlgebra.Matrix.ToLin +public import Mathlib.LinearAlgebra.BilinearForm.Orthogonal + + +/-! Rank-nullity and the X-projection / diagonal-orthogonal identity. -/ + +@[expose] public section + + +namespace LeanPool.SingleCopyStabilizer + +variable {𝕜 : Type*} [Field 𝕜] {ι : Type*} [Fintype ι] [DecidableEq ι] + +/-- The coordinate dot product regarded as a bilinear form. -/ +def dotForm : LinearMap.BilinForm 𝕜 (Vec 𝕜 ι) := dotProductBilin 𝕜 𝕜 + +omit [DecidableEq ι] in +theorem dotForm_nondegenerate : (dotForm (𝕜 := 𝕜) (ι := ι)).Nondegenerate := by + classical + constructor + · intro x hx + funext i + simpa [dotForm] using hx (Pi.single i 1) + · intro x hx + funext i + simpa [dotForm] using hx (Pi.single i 1) + +omit [DecidableEq ι] in +theorem dotForm_refl : (dotForm (𝕜 := 𝕜) (ι := ι)).IsRefl := by + classical + intro x y hxy + change y ⬝ᵥ x = 0 + rw [dotProduct_comm] + exact hxy +/-- The annihilator of a subspace under the coordinate dot product. -/ +def dotOrthogonal (D : Submodule 𝕜 (Vec 𝕜 ι)) : Submodule 𝕜 (Vec 𝕜 ι) := + dotForm.orthogonal D + +omit [DecidableEq ι] in +@[simp] theorem mem_dotOrthogonal (D : Submodule 𝕜 (Vec 𝕜 ι)) (x : Vec 𝕜 ι) : + x ∈ dotOrthogonal D ↔ ∀ s ∈ D, x ⬝ᵥ s = 0 := by + classical + change (∀ s ∈ D, s ⬝ᵥ x = 0) ↔ _ + simp only [dotProduct_comm] + +omit [DecidableEq ι] in +theorem finrank_dotOrthogonal (D : Submodule 𝕜 (Vec 𝕜 ι)) : + Module.finrank 𝕜 (dotOrthogonal D) = Fintype.card ι - Module.finrank 𝕜 D := by + classical + rw [dotOrthogonal, LinearMap.BilinForm.finrank_orthogonal + dotForm_nondegenerate] + simp +/-- The X-coordinate image of a space of Pauli labels. -/ +def xProjection (L : Submodule 𝕜 (Label 𝕜 ι)) : Submodule 𝕜 (Vec 𝕜 ι) := + L.map (LinearMap.fst 𝕜 (Vec 𝕜 ι) (Vec 𝕜 ι)) + +omit [DecidableEq ι] [Fintype ι] in +@[simp] theorem mem_xProjection (L : Submodule 𝕜 (Label 𝕜 ι)) (x : Vec 𝕜 ι) : + x ∈ xProjection L ↔ ∃ z, (x, z) ∈ L := by + classical + constructor + · rintro ⟨⟨y,z⟩, hyz, h⟩ + exact ⟨z, by simpa using h ▸ hyz⟩ + · rintro ⟨z, hz⟩ + exact ⟨(x, z), hz, rfl⟩ +/-- The X projection with domain restricted to a given label space. -/ +def xRestricted (L : Submodule 𝕜 (Label 𝕜 ι)) : L →ₗ[𝕜] Vec 𝕜 ι := + (LinearMap.fst 𝕜 (Vec 𝕜 ι) (Vec 𝕜 ι)).domRestrict L + +/-- Identify diagonal labels with the kernel of the restricted X projection. -/ +def diagonalKernelEquiv (L : Submodule 𝕜 (Label 𝕜 ι)) : + diagonalSpace L ≃ₗ[𝕜] LinearMap.ker (xRestricted L) where + toFun z := ⟨⟨(0,z),z.property⟩,rfl⟩ + invFun a := ⟨a.val.val.2, by + have hx : a.val.val.1 = 0 := a.property + change (0, a.val.val.2) ∈ L + rw [← hx] + exact a.val.property⟩ + left_inv _ := rfl + right_inv a := by + apply Subtype.ext + apply Subtype.ext + apply Prod.ext + · exact a.property.symm + · rfl + map_add' a b := by + apply Subtype.ext + apply Subtype.ext + simp + map_smul' c z := by + apply Subtype.ext + apply Subtype.ext + simp + +omit [DecidableEq ι] [Fintype ι] in +/-- Rank-nullity with the diagonal kernel explicitly identified. -/ +theorem finrank_xProjection_add_diagonal [Finite ι] (L : Submodule 𝕜 (Label 𝕜 ι)) : + Module.finrank 𝕜 (xProjection L) + Module.finrank 𝕜 (diagonalSpace L) = + Module.finrank 𝕜 L := by + let := Fintype.ofFinite ι + classical + have h := (xRestricted L).finrank_range_add_finrank_ker + rw [← (diagonalKernelEquiv L).finrank_eq] at h + have hr : LinearMap.range (xRestricted L) = xProjection L := by + ext x + constructor + · rintro ⟨a, rfl⟩ + exact ⟨a.val, a.property, rfl⟩ + · rintro ⟨a, ha, rfl⟩ + exact ⟨⟨a,ha⟩, rfl⟩ + rw [hr] at h + exact h + +omit [DecidableEq ι] in +theorem xProjection_le_orthogonal (L : Submodule 𝕜 (Label 𝕜 ι)) + (hL : IsIsotropic L) : xProjection L ≤ dotOrthogonal (diagonalSpace L) := by + classical + intro x hx + obtain ⟨z, hz⟩ := (mem_xProjection L x).mp hx + rw [mem_dotOrthogonal] + intro s hs + exact x_orthogonal_diagonal hL hz hs + +omit [DecidableEq ι] in +/-- For a Lagrangian label space, the X projection is exactly the orthogonal +complement of the diagonal labels. -/ +theorem lagrangian_xProjection_eq (L : Submodule 𝕜 (Label 𝕜 ι)) + (hL : IsIsotropic L) (hdim : Module.finrank 𝕜 L = Fintype.card ι) : + xProjection L = dotOrthogonal (diagonalSpace L) := by + classical + apply Submodule.eq_of_le_of_finrank_eq (xProjection_le_orthogonal L hL) + have h := finrank_xProjection_add_diagonal L + rw [finrank_dotOrthogonal] + omega + +omit [DecidableEq ι] in +/-- The general dimension identity underlying the nullity argument. -/ +theorem low_nullity_projection_codimension + (L : Submodule 𝕜 (Label 𝕜 ι)) (r : ℕ) + (hdim : Module.finrank 𝕜 L + r = Fintype.card ι) : + Module.finrank 𝕜 (xProjection L) + r = + Module.finrank 𝕜 (dotOrthogonal (diagonalSpace L)) := by + classical + have h := finrank_xProjection_add_diagonal L + rw [finrank_dotOrthogonal] + omega + +omit [DecidableEq ι] in +/-- Isotropy bounds stabilizer dimension by the number of sites. -/ +theorem isotropic_finrank_le (L : Submodule 𝕜 (Label 𝕜 ι)) (hL : IsIsotropic L) : + Module.finrank 𝕜 L ≤ Fintype.card ι := by + classical + have h := finrank_xProjection_add_diagonal L + have hle := Submodule.finrank_mono (xProjection_le_orthogonal L hL) + rw [finrank_dotOrthogonal] at hle + have hD : Module.finrank 𝕜 (diagonalSpace L) ≤ Fintype.card ι := by + simpa using (diagonalSpace L).finrank_le + omega + +omit [DecidableEq ι] [Fintype ι] in +/-- When diagonal dimension reaches total stabilizer dimension, every +stabilizer is diagonal. This applies to the low-nullity stopping criterion. -/ +theorem all_diagonal_of_max_dimension [Finite ι] (L : Submodule 𝕜 (Label 𝕜 ι)) + (hdim : Module.finrank 𝕜 (diagonalSpace L) = Module.finrank 𝕜 L) : + ∀ a ∈ L, a.1 = 0 := by + let := Fintype.ofFinite ι + classical + have h := finrank_xProjection_add_diagonal L + have hzero : Module.finrank 𝕜 (xProjection L) = 0 := by omega + have hbot := Submodule.finrank_eq_zero.mp hzero + intro a ha + have hx : a.1 ∈ xProjection L := (mem_xProjection L a.1).mpr ⟨a.2, ha⟩ + simpa [hbot] using hx + +omit [DecidableEq ι] in +/-- Full diagonal dimension means all diagonal labels are present. -/ +theorem diagonalSpace_eq_top_of_full_dimension (L : Submodule 𝕜 (Label 𝕜 ι)) + (hdim : Module.finrank 𝕜 (diagonalSpace L) = Fintype.card ι) : + diagonalSpace L = ⊤ := by + classical + apply Submodule.eq_top_of_finrank_eq + simpa using hdim + +end LeanPool.SingleCopyStabilizer diff --git a/LeanPool/SingleCopyStabilizer/QuantumRound.lean b/LeanPool/SingleCopyStabilizer/QuantumRound.lean new file mode 100644 index 0000000000..8924e48e43 --- /dev/null +++ b/LeanPool/SingleCopyStabilizer/QuantumRound.lean @@ -0,0 +1,187 @@ +/- +Copyright (c) 2026 Antonio Anna Mele. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Antonio Anna Mele +-/ +module + +public import LeanPool.SingleCopyStabilizer.StabilizerState +public import LeanPool.SingleCopyStabilizer.CNOTAction +public import LeanPool.SingleCopyStabilizer.CliffordAction +public import LeanPool.SingleCopyStabilizer.ExactLearning +public import LeanPool.SingleCopyStabilizer.Circuit + + +/-! +# A physical adaptive round on stabilizer amplitudes + +The round is the actual CNOT basis permutation, followed by H or HS at +the chosen pivot. Its label-space action is proved to be `binaryRound`. +No membership oracle is used to define the amplitude action. +-/ + +@[expose] public section + +noncomputable section + + +namespace LeanPool.SingleCopyStabilizer.QuantumRound + +open Measurement CliffordAction +open scoped CharTwo + +variable {ι : Type*} [Fintype ι] [DecidableEq ι] + +/-- Apply H for correction bit zero, and HS for correction bit one. -/ +def correctionAmplitude (i : ι) (b : ZMod 2) (ψ : Amplitude ι) : Amplitude ι := + localHadamard i (if b = 0 then ψ else localPhase i ψ) + +theorem correctionAmplitude_normalized (i : ι) (b : ZMod 2) + (ψ : Amplitude ι) (hψ : IsNormalized ψ) : + IsNormalized (correctionAmplitude i b ψ) := by + classical + apply localHadamard_normalized + split_ifs + · exact hψ + · exact localPhase_normalized i ψ hψ + +omit [Fintype ι] in +theorem localCorrection_zero (i : ι) (u v : Bits ι) : + localCorrection i (0 : ZMod 2) (u, v) = + (hadamardXLabel i u v, hadamardZLabel i u v) := by + classical + simp [localCorrection, hadamardXLabel, hadamardZLabel] + +omit [Fintype ι] in +theorem localCorrection_one (i : ι) (u v : Bits ι) : + localCorrection i (1 : ZMod 2) (u, v) = + (hadamardXLabel i u (phaseZLabel i u v), + hadamardZLabel i u (phaseZLabel i u v)) := by + classical + apply Prod.ext + · simp [localCorrection, hadamardXLabel, phaseZLabel] + · funext j + by_cases hj : j = i + · subst j + simp [localCorrection, hadamardZLabel] + · simp [localCorrection, hadamardZLabel, phaseZLabel, hj] + +/-- Actual H/HS eigenvector covariance yields the correction's label action; +the output eigenvalue includes the physically relevant phase factors. -/ +theorem correctionAmplitude_eigenvector (i : ι) (b : ZMod 2) + (ψ : Amplitude ι) (u v : Bits ι) (ζ : ℂ) + (heig : IsPauliEigenvector ψ u v ζ) : + ∃ η, IsPauliEigenvector (correctionAmplitude i b ψ) + (localCorrection i b (u, v)).1 (localCorrection i b (u, v)).2 η := by + classical + rcases bit_eq_zero_or_one b with hb | hb + · subst b + rw [localCorrection_zero] + refine ⟨paritySign (u i * v i) * ζ, ?_⟩ + simpa [correctionAmplitude] using localHadamard_eigenvector i ψ u v ζ heig + · subst b + rw [localCorrection_one] + refine ⟨paritySign (u i * phaseZLabel i u v i) * + (star (phaseBit (u i)) * ζ), ?_⟩ + simpa [correctionAmplitude] using + localHadamard_eigenvector i (localPhase i ψ) u (phaseZLabel i u v) + (star (phaseBit (u i)) * ζ) (localPhase_eigenvector i ψ u v ζ heig) + +/-- The physical round depends only on its observed difference and random bit. +When the observed difference is zero, the state is left unchanged. -/ +def applyRoundAmplitude (u : BinaryVec ι) (b : ZMod 2) + (ψ : Amplitude ι) : Amplitude ι := + if hu : u = 0 then ψ else + let i := binaryPivot u hu + correctionAmplitude i b + (CNOTAction.applyCNOTs i (u - Pi.single i 1) + (by simp [i, binaryPivot_spec u hu]) ψ) + +@[simp] theorem applyRoundAmplitude_zero (b : ZMod 2) (ψ : Amplitude ι) : + applyRoundAmplitude 0 b ψ = ψ := by + classical + simp [applyRoundAmplitude] + +theorem applyRoundAmplitude_of_ne (u : BinaryVec ι) (b : ZMod 2) + (ψ : Amplitude ι) (hu : u ≠ 0) : + applyRoundAmplitude u b ψ = correctionAmplitude (binaryPivot u hu) b + (CNOTAction.applyCNOTs (binaryPivot u hu) (u - Pi.single (binaryPivot u hu) 1) + (by simp [binaryPivot_spec u hu]) ψ) := by + classical + simp [applyRoundAmplitude, hu] + +/-- The amplitude round is exactly the recorded complex-linear circuit round. -/ +theorem roundEquiv_apply_eq_applyRoundAmplitude (u : BinaryVec ι) (b : ZMod 2) + (ψ : Amplitude ι) : Circuit.roundEquiv u b ψ = applyRoundAmplitude u b ψ := by + classical + by_cases hu : u = 0 + · subst u + simp + · rw [Circuit.roundEquiv_apply_of_ne u b hu, + applyRoundAmplitude_of_ne u b ψ hu, Circuit.correctionEquiv_apply] + rfl + +theorem applyRoundAmplitude_normalized (u : BinaryVec ι) (b : ZMod 2) + (ψ : Amplitude ι) (hψ : IsNormalized ψ) : + IsNormalized (applyRoundAmplitude u b ψ) := by + classical + by_cases hu : u = 0 + · subst u + simpa using hψ + · rw [applyRoundAmplitude_of_ne u b ψ hu] + apply correctionAmplitude_normalized + exact CNOTAction.normalized _ _ _ ψ hψ + +/-- Composition of the concrete CNOT and H/HS covariance theorems transports +every eigenlabel through the paper's algebraic adaptive update. -/ +theorem adaptiveUpdate_eigenvector (i : ι) (u : BinaryVec ι) (b : ZMod 2) + (hu : u i = 1) (ψ : Amplitude ι) (a : Label (ZMod 2) ι) (ζ : ℂ) + (heig : IsPauliEigenvector ψ a.1 a.2 ζ) : + ∃ η, IsPauliEigenvector + (correctionAmplitude i b (CNOTAction.applyCNOTs i (u - Pi.single i 1) + (by simp [hu]) ψ)) + (adaptiveUpdate i u b a).1 (adaptiveUpdate i u b a).2 η := by + classical + exact correctionAmplitude_eigenvector i b _ _ _ ζ + (CNOTAction.transports_eigenvector i (u - Pi.single i 1) (by simp [hu]) + ψ a.1 a.2 ζ heig) + +/-- The physical gate round implements the full unsigned label-space update, +including arbitrary outcomes with zero probability. -/ +theorem applyRoundAmplitude_eigenlabels (u : BinaryVec ι) (b : ZMod 2) + (ψ : Amplitude ι) (L : BinarySpace ι) (heig : HasEigenlabels ψ L) : + HasEigenlabels (applyRoundAmplitude u b ψ) (binaryRound L u b) := by + classical + by_cases hu : u = 0 + · subst u + simpa using heig + · rw [applyRoundAmplitude_of_ne u b ψ hu, binaryRound_of_ne L u b hu] + rintro _ ⟨a, ha, rfl⟩ + obtain ⟨ζ, hζ⟩ := heig a ha + exact adaptiveUpdate_eigenvector (binaryPivot u hu) u b + (binaryPivot_spec u hu) ψ a ζ hζ + +/-- An actual normalized pure stabilizer state after the physical round. -/ +def quantumRound (S : PureStabilizerState ι) (o : ExactLearning.Outcome ι) : + PureStabilizerState ι where + amplitude := applyRoundAmplitude o.1 o.2 S.amplitude + normalized := applyRoundAmplitude_normalized o.1 o.2 S.amplitude S.normalized + labels := binaryRound S.labels o.1 o.2 + isotropic := binaryRound_isotropic S.labels S.isotropic o.1 o.2 + maximal := (binaryRound_finrank S.labels o.1 o.2).trans S.maximal + eigenlabels := applyRoundAmplitude_eigenlabels o.1 o.2 S.amplitude S.labels S.eigenlabels + +@[simp] theorem quantumRound_labels (S : PureStabilizerState ι) + (o : ExactLearning.Outcome ι) : + (quantumRound S o).labels = binaryRound S.labels o.1 o.2 := rfl + +@[simp] theorem quantumRound_amplitude (S : PureStabilizerState ι) + (o : ExactLearning.Outcome ι) : + (quantumRound S o).amplitude = applyRoundAmplitude o.1 o.2 S.amplitude := rfl + +theorem quantumRound_amplitude_eq_roundEquiv (S : PureStabilizerState ι) + (o : ExactLearning.Outcome ι) : + (quantumRound S o).amplitude = Circuit.roundEquiv o.1 o.2 S.amplitude := + (roundEquiv_apply_eq_applyRoundAmplitude o.1 o.2 S.amplitude).symm + +end LeanPool.SingleCopyStabilizer.QuantumRound diff --git a/LeanPool/SingleCopyStabilizer/Round.lean b/LeanPool/SingleCopyStabilizer/Round.lean new file mode 100644 index 0000000000..d7007ac724 --- /dev/null +++ b/LeanPool/SingleCopyStabilizer/Round.lean @@ -0,0 +1,149 @@ +/- +Copyright (c) 2026 Antonio Anna Mele. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Antonio Anna Mele +-/ +module + +public import LeanPool.SingleCopyStabilizer.Projection + + +/-! A complete unsigned-label update for one binary round, including the +zero-difference branch and a deterministic pivot choice. -/ + +@[expose] public section + +noncomputable section + + +namespace LeanPool.SingleCopyStabilizer + +variable {ι : Type*} [Fintype ι] [DecidableEq ι] + +/-- Unsigned X or Z labels of a binary qubit register. -/ +abbrev BinaryVec (ι : Type*) := Vec (ZMod 2) ι +/-- Binary linear spaces of paired Pauli labels. -/ +abbrev BinarySpace (ι : Type*) := Submodule (ZMod 2) (Label (ZMod 2) ι) + +theorem bit_eq_one_of_ne_zero (a : ZMod 2) (ha : a ≠ 0) : a = 1 := by + -- There are only two residues modulo two. + revert a + decide + +omit [DecidableEq ι] [Fintype ι] in +theorem exists_binary_pivot (u : BinaryVec ι) (hu : u ≠ 0) : ∃ i, u i = 1 := by + classical + have h : ∃ i, u i ≠ 0 := by + by_contra! h + exact hu (funext h) + obtain ⟨i, hi⟩ := h + exact ⟨i, bit_eq_one_of_ne_zero (u i) hi⟩ +/-- Select a coordinate equal to one in a nonzero binary vector. -/ +def binaryPivot (u : BinaryVec ι) (hu : u ≠ 0) : ι := + Classical.choose (exists_binary_pivot u hu) + +omit [Fintype ι] [DecidableEq ι] in +theorem binaryPivot_spec (u : BinaryVec ι) (hu : u ≠ 0) : u (binaryPivot u hu) = 1 := + Classical.choose_spec (exists_binary_pivot u hu) + +/-- The observed shear and local correction acting on a binary label space. -/ +def binaryRound (L : BinarySpace ι) (u : BinaryVec ι) (b : ZMod 2) : BinarySpace ι := by + classical + exact if hu : u = 0 then L else updatedSpace L (binaryPivot u hu) u b + +@[simp] theorem binaryRound_zero (L : BinarySpace ι) (b : ZMod 2) : + binaryRound L 0 b = L := by + classical + exact dite_eq_left rfl + +theorem binaryRound_of_ne (L : BinarySpace ι) (u : BinaryVec ι) (b : ZMod 2) + (hu : u ≠ 0) : binaryRound L u b = updatedSpace L (binaryPivot u hu) u b := by + classical + exact dite_eq_right hu + +theorem binaryRound_isotropic (L : BinarySpace ι) (hL : IsIsotropic L) + (u : BinaryVec ι) (b : ZMod 2) : IsIsotropic (binaryRound L u b) := by + by_cases hu : u = 0 + · subst u + simpa using hL + · rw [binaryRound_of_ne L u b hu] + exact updatedSpace_isotropic L hL _ u b (binaryPivot_spec u hu) + +theorem binaryRound_finrank (L : BinarySpace ι) (u : BinaryVec ι) (b : ZMod 2) : + Module.finrank (ZMod 2) (binaryRound L u b) = Module.finrank (ZMod 2) L := by + by_cases hu : u = 0 + · subst u + rw [binaryRound_zero] + · rw [binaryRound_of_ne L u b hu] + exact updatedSpace_finrank L _ u b (binaryPivot_spec u hu) + +/-- All computationally allowed differences preserve the diagonal dimension, +including those which are not stabilizer X labels in the low-nullity setting. -/ +theorem binaryRound_diagonal_mono (L : BinarySpace ι) (u : BinaryVec ι) (b : ZMod 2) + (hu : u ∈ dotOrthogonal (diagonalSpace L)) : + Module.finrank (ZMod 2) (diagonalSpace L) ≤ + Module.finrank (ZMod 2) (diagonalSpace (binaryRound L u b)) := by + by_cases hzero : u = 0 + · subst u + rw [binaryRound_zero] + · rw [binaryRound_of_ne L u b hzero] + exact diagonal_finrank_monotone L u _ b (binaryPivot_spec u hzero) + ((mem_dotOrthogonal _ _).mp hu) + +/-- Every nonzero stabilizer X label has at least one successful correction. -/ +theorem binaryRound_exists_progress (L : BinarySpace ι) (hL : IsIsotropic L) + (u : BinaryVec ι) (hu : u ∈ xProjection L) (hzero : u ≠ 0) : + ∃ b : ZMod 2, Module.finrank (ZMod 2) (diagonalSpace L) < + Module.finrank (ZMod 2) (diagonalSpace (binaryRound L u b)) := by + obtain ⟨v, hv⟩ := (mem_xProjection L u).mp hu + obtain ⟨b, hb⟩ := exists_diagonal_finrank_progress L hL u v (binaryPivot u hzero) + (binaryPivot_spec u hzero) hv + refine ⟨b, ?_⟩ + rw [binaryRound_of_ne L u b hzero] + exact hb + +/-- Totalize sampling from the X projection by leaving the label space +unchanged on labels outside that projection. This is used for exact learning; +those labels can have positive probability for states of positive nullity. -/ +def safeBinaryRound (L : BinarySpace ι) (u : BinaryVec ι) (b : ZMod 2) : BinarySpace ι := by + classical + exact if u ∈ xProjection L then binaryRound L u b else L + +theorem safeBinaryRound_of_mem (L : BinarySpace ι) (u : BinaryVec ι) (b : ZMod 2) + (hu : u ∈ xProjection L) : safeBinaryRound L u b = binaryRound L u b := by + classical + exact ite_eq_left hu + +theorem safeBinaryRound_of_not_mem (L : BinarySpace ι) (u : BinaryVec ι) (b : ZMod 2) + (hu : u ∉ xProjection L) : safeBinaryRound L u b = L := by + classical + exact ite_eq_right hu + +theorem safeBinaryRound_isotropic (L : BinarySpace ι) (hL : IsIsotropic L) + (u : BinaryVec ι) (b : ZMod 2) : IsIsotropic (safeBinaryRound L u b) := by + classical + by_cases hu : u ∈ xProjection L + · rw [safeBinaryRound_of_mem L u b hu] + exact binaryRound_isotropic L hL u b + · rw [safeBinaryRound_of_not_mem L u b hu] + exact hL + +theorem safeBinaryRound_finrank (L : BinarySpace ι) (u : BinaryVec ι) (b : ZMod 2) : + Module.finrank (ZMod 2) (safeBinaryRound L u b) = Module.finrank (ZMod 2) L := by + classical + by_cases hu : u ∈ xProjection L + · rw [safeBinaryRound_of_mem L u b hu] + exact binaryRound_finrank L u b + · rw [safeBinaryRound_of_not_mem L u b hu] + +theorem safeBinaryRound_diagonal_mono (L : BinarySpace ι) (hL : IsIsotropic L) + (u : BinaryVec ι) (b : ZMod 2) : + Module.finrank (ZMod 2) (diagonalSpace L) ≤ + Module.finrank (ZMod 2) (diagonalSpace (safeBinaryRound L u b)) := by + classical + by_cases hu : u ∈ xProjection L + · rw [safeBinaryRound_of_mem L u b hu] + exact binaryRound_diagonal_mono L u b (xProjection_le_orthogonal L hL hu) + · rw [safeBinaryRound_of_not_mem L u b hu] + +end LeanPool.SingleCopyStabilizer diff --git a/LeanPool/SingleCopyStabilizer/SharpExactLearning.lean b/LeanPool/SingleCopyStabilizer/SharpExactLearning.lean new file mode 100644 index 0000000000..516bbb8fee --- /dev/null +++ b/LeanPool/SingleCopyStabilizer/SharpExactLearning.lean @@ -0,0 +1,162 @@ +/- +Copyright (c) 2026 Antonio Anna Mele. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Antonio Anna Mele +-/ +module + +public import LeanPool.SingleCopyStabilizer.ExactLearning +public import LeanPool.SingleCopyStabilizer.GeometricTailBounds +public import LeanPool.SingleCopyStabilizer.GeometricDomination + + +/-! +# Exact label compression with a sharp leading round count + +The numerical budget has leading term `2n` rounds and `4n` copies. The tail +bound is for the explicit uniform-X-label process in `ExactLearning`; the +connection of that process to Born-rule circuit execution is proved separately. +-/ + +@[expose] public section + +noncomputable section + +namespace LeanPool.SingleCopyStabilizer.SharpExactLearning + +open GeometricTailBounds + +/-- The reciprocal progress-rate bound for `n` qubits. -/ +def meanBound (n : ℕ) : ℝ := 2 * (n : ℝ) + 4 + +/-- Explicit round budget preserving the leading coefficient two. -/ +def roundBudget (n : ℕ) (δ : ℝ) : ℕ := confidenceBudget (meanBound n) δ + +/-- Two fresh copies per round, followed by one final computational readout. -/ +def copyBudget (n : ℕ) (δ : ℝ) : ℕ := 2 * roundBudget n δ + 1 + +theorem meanBound_pos (n : ℕ) : 0 < meanBound n := by + unfold meanBound + positivity + +/-- Expanded round budget with no hidden asymptotic constants. -/ +theorem roundBudget_formula (n : ℕ) (δ : ℝ) : + roundBudget n δ = + ⌈2 * (n : ℝ) + 4 + 8 * Real.sqrt ((2 * (n : ℝ) + 4) * Real.log (1 / δ)) + + 64 * Real.log (1 / δ)⌉₊ := by + unfold roundBudget confidenceBudget confidenceDeviation meanBound + congr 1 + ring + +/-- The logarithmic confidence parameter is nonnegative on the intended range. -/ +theorem confidence_log_nonneg (δ : ℝ) (hδ : 0 < δ) (hδmax : δ ≤ 1) : + 0 ≤ Real.log (1 / δ) := by + apply Real.log_nonneg + apply (le_div_iff₀ hδ).2 + simpa using hδmax + +/-- Rounding adds less than one round to the explicit real-valued budget. -/ +theorem roundBudget_upper (n : ℕ) (δ : ℝ) (hδ : 0 < δ) (hδmax : δ ≤ 1) : + (roundBudget n δ : ℝ) < + 2 * (n : ℝ) + 5 + 8 * Real.sqrt ((2 * (n : ℝ) + 4) * Real.log (1 / δ)) + + 64 * Real.log (1 / δ) := by + have hM := meanBound_pos n + have hlog := confidence_log_nonneg δ hδ hδmax + have hdev := confidenceDeviation_nonneg (meanBound n) _ hM.le hlog + have hceil := Nat.ceil_lt_add_one + (show 0 ≤ meanBound n + confidenceDeviation (meanBound n) (Real.log (1 / δ)) by linarith) + change (roundBudget n δ : ℝ) < _ at hceil + dsimp [confidenceDeviation, meanBound] at hceil + linarith + +/-- The resulting copy budget has leading coefficient four. -/ +theorem copyBudget_upper (n : ℕ) (δ : ℝ) (hδ : 0 < δ) (hδmax : δ ≤ 1) : + (copyBudget n δ : ℝ) < + 4 * (n : ℝ) + 11 + 16 * Real.sqrt ((2 * (n : ℝ) + 4) * Real.log (1 / δ)) + + 128 * Real.log (1 / δ) := by + have := roundBudget_upper n δ hδ hδmax + simp only [copyBudget, Nat.cast_add, Nat.cast_mul, Nat.cast_ofNat, Nat.cast_one] + linarith + +/-- An explicit universal-constant copy bound, valid for at least one qubit. +The constant is conservative; `copyBudget_upper` retains the sharper leading +coefficient four and square-root confidence term. -/ +theorem copyBudget_linear (n : ℕ) (hn : 1 ≤ n) (δ : ℝ) + (hδ : 0 < δ) (hδmax : δ ≤ 1) : + (copyBudget n δ : ℝ) < 136 * ((n : ℝ) + Real.log (1 / δ)) := by + have hnreal : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn + have hlog := confidence_log_nonneg δ hδ hδmax + have hsqrt : Real.sqrt ((2 * (n : ℝ) + 4) * Real.log (1 / δ)) ≤ + ((2 * (n : ℝ) + 4) + Real.log (1 / δ)) / 2 := by + apply Real.sqrt_le_iff.mpr + constructor + · positivity + · nlinarith [sq_nonneg ((2 * (n : ℝ) + 4) - Real.log (1 / δ))] + have hbudget := copyBudget_upper n δ hδ hδmax + linarith + +variable {ι : Type*} [Fintype ι] [DecidableEq ι] + +omit [DecidableEq ι] in +/-- The exact process's rank is bounded by the number of qubits. -/ +theorem rank_le_qubit_count (s : ExactLearning.State ι) : + ExactLearning.rank s ≤ Fintype.card ι := Nat.sub_le _ _ + +/-- Every needed progress-rate estimate is proved for the exact process. -/ +theorem exact_progress_parameter (s : ExactLearning.State ι) : + FiniteProbability.progressProbability (ExactLearning.rank s) ≤ + ExactLearning.process.progressMass s := + ExactLearning.progress_mass_ge_rank_parameter s + +omit [DecidableEq ι] in +/-- The reciprocal-sum hypothesis is discharged for every exact-process state. -/ +theorem exact_process_mean_bound (s : ExactLearning.State ι) : + (∑ j ∈ Finset.range (ExactLearning.rank s), + 1 / FiniteProbability.progressProbability (j + 1)) ≤ meanBound (Fintype.card ι) := + exact_rate_sum_bound _ _ (rank_le_qubit_count s) + +/-- The explicit exact-learning label process succeeds with confidence +`1-δ` at every round count at least the sharp-leading-term budget. All +progress-rate and reciprocal-sum hypotheses are proved, not assumed. -/ +theorem compression_failure_probability_after_budget (s : ExactLearning.State ι) + (δ : ℝ) (hδ : 0 < δ) (hδmax : δ ≤ 1) (T : ℕ) + (hT : roundBudget (Fintype.card ι) δ ≤ T) : + ExactLearning.process.failureProbability T s ≤ δ := by + let M : ℝ := meanBound (Fintype.card ι) + let L : ℝ := Real.log (1 / δ) + let deviation : ℝ := confidenceDeviation M L + let lambda : ℝ := chosenTilt M deviation + have hM : 0 < M := meanBound_pos _ + have hL : 0 ≤ L := confidence_log_nonneg δ hδ hδmax + have hdev : 0 ≤ deviation := confidenceDeviation_nonneg M L hM.le hL + obtain ⟨hlambda, hlambdamax⟩ := chosenTilt_bounds M deviation hM hdev + have hrate : ∀ j, 0 < j → lambda < FiniteProbability.progressProbability j := by + intro j hj + exact chosenTilt_lt_rate M deviation _ hM hdev + (FiniteProbability.progress_probability_ge_quarter j hj) + have hdom := GeometricDomination.failure_probability_le_product + FiniteProbability.progressProbability lambda hlambda hrate ExactLearning.process + (show lambda ≤ 1 by dsimp [lambda]; linarith) + (fun state _ => exact_progress_parameter state) T s + have htime : M + confidenceDeviation M (Real.log (1 / δ)) ≤ (T : ℝ) := by + have hceil : M + confidenceDeviation M (Real.log (1 / δ)) ≤ + (roundBudget (Fintype.card ι) δ : ℝ) := Nat.le_ceil _ + have hTreal : (roundBudget (Fintype.card ι) δ : ℝ) ≤ T := by exact_mod_cast hT + exact hceil.trans hTreal + have htail : GeometricDomination.productPotential FiniteProbability.progressProbability + lambda (ExactLearning.rank s) * (1 - lambda) ^ T ≤ δ := by + simpa only [GeometricDomination.productPotential, GeometricDomination.geometricFactor] using + confidence_tail_bound (Finset.range (ExactLearning.rank s)) + (fun j => FiniteProbability.progressProbability (j + 1)) M δ T hM hδ hδmax + (fun j _ => FiniteProbability.progress_probability_ge_quarter (j + 1) (by omega)) + (exact_process_mean_bound s) htime + exact hdom.trans htail + +/-- Exact label compression in `ceil(2n+4+8√((2n+4)log(1/δ))+64log(1/δ))` +rounds, with failure probability at most `δ`. -/ +theorem compression_failure_probability (s : ExactLearning.State ι) + (δ : ℝ) (hδ : 0 < δ) (hδmax : δ ≤ 1) : + ExactLearning.process.failureProbability (roundBudget (Fintype.card ι) δ) s ≤ δ := + compression_failure_probability_after_budget s δ hδ hδmax _ le_rfl + +end LeanPool.SingleCopyStabilizer.SharpExactLearning diff --git a/LeanPool/SingleCopyStabilizer/StabilizerState.lean b/LeanPool/SingleCopyStabilizer/StabilizerState.lean new file mode 100644 index 0000000000..2b28bcf05f --- /dev/null +++ b/LeanPool/SingleCopyStabilizer/StabilizerState.lean @@ -0,0 +1,304 @@ +/- +Copyright (c) 2026 Antonio Anna Mele. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Antonio Anna Mele +-/ +module + +public import LeanPool.SingleCopyStabilizer.Measurement +public import LeanPool.SingleCopyStabilizer.Projection + + +/-! +# Stabilizer label spaces imply the operational computational distribution + +This file joins finite-dimensional symplectic algebra to the explicit complex +amplitude Pauli action. The public state premises are normalization, actual +Pauli eigenvector equations, isotropy, and maximal label-space dimension. +Uniform measurement distributions are conclusions, not premises. +-/ + +@[expose] public section + + +noncomputable section + +namespace LeanPool.SingleCopyStabilizer + +attribute [local instance] Classical.propDecidable + +open Measurement +open scoped BigOperators + +variable {ι : Type*} [Fintype ι] [DecidableEq ι] + +/-- Every label in L represents an actual Pauli eigenvector equation for ψ. -/ +def HasEigenlabels (ψ : Amplitude ι) (L : Submodule (ZMod 2) (Label (ZMod 2) ι)) : Prop := + ∀ a ∈ L, ∃ ζ, IsPauliEigenvector ψ a.1 a.2 ζ + +/-- A normalized amplitude together with its maximal isotropic eigenlabel +space. Eigenvalue phases remain existential and are not discarded from the +underlying quantum equations. -/ +structure PureStabilizerState (ι : Type*) [Fintype ι] [DecidableEq ι] where + /-- The actual pure-state amplitudes. -/ + amplitude : Amplitude ι + normalized : IsNormalized amplitude + /-- The maximal isotropic space of actual Pauli eigenlabels. -/ + labels : Submodule (ZMod 2) (Label (ZMod 2) ι) + isotropic : IsIsotropic labels + maximal : Module.finrank (ZMod 2) labels = Fintype.card ι + eigenlabels : HasEigenlabels amplitude labels + +omit [DecidableEq ι] in +theorem measurement_orthogonalSubgroup_eq (D : Submodule (ZMod 2) (Bits ι)) : + orthogonalSubgroup (D : Set (Bits ι)) = (dotOrthogonal D).toAddSubgroup := by + classical + ext u + change u ∈ orthogonalSet (D : Set (Bits ι)) ↔ u ∈ dotOrthogonal D + rw [mem_dotOrthogonal] + change (∀ s ∈ D, s ⬝ᵥ u = 0) ↔ (∀ s ∈ D, u ⬝ᵥ s = 0) + simp only [dotProduct_comm] + +omit [DecidableEq ι] in +theorem eigenlabels_diagonal (ψ : Amplitude ι) + (L : Submodule (ZMod 2) (Label (ZMod 2) ι)) (heig : HasEigenlabels ψ L) : + ∀ s ∈ (diagonalSpace L : Set (Bits ι)), ∃ ζ, IsPauliEigenvector ψ 0 s ζ := by + classical + intro s hs + exact heig (0, s) hs + +omit [DecidableEq ι] in +/-- Supported outcome differences annihilate diagonal labels for any +eigenlabel space, without a maximality or stabilizer-state promise. -/ +theorem eigenlabels_supported_difference (ψ : Amplitude ι) + (L : Submodule (ZMod 2) (Label (ZMod 2) ι)) (heig : HasEigenlabels ψ L) + (x y : Bits ι) (hx : ψ x ≠ 0) (hy : ψ y ≠ 0) : + x - y ∈ dotOrthogonal (diagonalSpace L) := by + classical + have h := supported_difference_orthogonal ψ (diagonalSpace L : Set (Bits ι)) + (eigenlabels_diagonal ψ L heig) x y hx hy + rw [mem_dotOrthogonal] + intro s hs + rw [dotProduct_comm] + exact h s hs + +omit [DecidableEq ι] in +/-- For maximal isotropic eigenlabels the geometric X-projection theorem +turns every supported difference into an actual stabilizer X direction. -/ +theorem stabilizer_supported_difference (ψ : Amplitude ι) + (L : Submodule (ZMod 2) (Label (ZMod 2) ι)) (heig : HasEigenlabels ψ L) + (hiso : IsIsotropic L) (hdim : Module.finrank (ZMod 2) L = Fintype.card ι) + (x y : Bits ι) (hx : ψ x ≠ 0) (hy : ψ y ≠ 0) : + ∃ v, (x - y, v) ∈ L := by + classical + apply (mem_xProjection L (x - y)).mp + rw [lagrangian_xProjection_eq L hiso hdim] + exact eigenlabels_supported_difference ψ L heig x y hx hy + +/-- The paper's affine uniform-support theorem, now derived from actual +amplitude eigenvector equations and maximal isotropic label-space dimension. -/ +theorem stabilizer_uniform_bornWeight (ψ : Amplitude ι) (hnorm : IsNormalized ψ) + (L : Submodule (ZMod 2) (Label (ZMod 2) ι)) (heig : HasEigenlabels ψ L) + (hiso : IsIsotropic L) (hdim : Module.finrank (ZMod 2) L = Fintype.card ι) : + ∃ z, ∀ x, bornWeight ψ x = + if x ∈ affineCoset (xProjection L).toAddSubgroup z then + 1 / (Nat.card (xProjection L) : ℝ) else 0 := by + classical + have heq : orthogonalSubgroup (diagonalSpace L : Set (Bits ι)) = + (xProjection L).toAddSubgroup := by + rw [measurement_orthogonalSubgroup_eq, lagrangian_xProjection_eq L hiso hdim] + have hX : ∀ u ∈ orthogonalSubgroup (diagonalSpace L : Set (Bits ι)), + ∃ v ζ, IsPauliEigenvector ψ u v ζ := by + intro u hu + rw [heq] at hu + obtain ⟨v, huv⟩ := (mem_xProjection L u).mp hu + obtain ⟨ζ, hζ⟩ := heig (u, v) huv + exact ⟨v, ζ, hζ⟩ + have h := uniform_bornWeight_of_complete_eigenlabels ψ hnorm + (diagonalSpace L : Set (Bits ι)) (eigenlabels_diagonal ψ L heig) hX + have hcard : Nat.card (xProjection L).toAddSubgroup = Nat.card (xProjection L) := + Nat.card_congr { + toFun := fun x => ⟨x.1, x.2⟩ + invFun := fun x => ⟨x.1, x.2⟩ + left_inv := fun _ => rfl + right_inv := fun _ => rfl } + simpa only [heq, hcard] using h + +theorem PureStabilizerState.uniform_bornWeight (S : PureStabilizerState ι) : + ∃ z, ∀ x, bornWeight S.amplitude x = + if x ∈ affineCoset (xProjection S.labels).toAddSubgroup z then + 1 / (Nat.card (xProjection S.labels) : ℝ) else 0 := + stabilizer_uniform_bornWeight S.amplitude S.normalized S.labels S.eigenlabels + S.isotropic S.maximal + +omit [DecidableEq ι] in +/-- Full diagonal dimension forces any two supported outcomes to coincide. -/ +theorem full_diagonal_support_unique (ψ : Amplitude ι) + (L : Submodule (ZMod 2) (Label (ZMod 2) ι)) (heig : HasEigenlabels ψ L) + (hfull : Module.finrank (ZMod 2) (diagonalSpace L) = Fintype.card ι) + (x y : Bits ι) (hx : ψ x ≠ 0) (hy : ψ y ≠ 0) : x = y := by + classical + have h := eigenlabels_supported_difference ψ L heig x y hx hy + have htop := diagonalSpace_eq_top_of_full_dimension L hfull + rw [mem_dotOrthogonal, htop] at h + have hzero : x - y = 0 := by + funext i + simpa using h (Pi.single i 1) (by simp) + exact sub_eq_zero.mp hzero + +/-- The termination readout is a point mass when diagonal rank is full. +This theorem needs neither isotropy nor maximality beyond the stated full +diagonal-rank condition. -/ +theorem full_diagonal_bornWeight_point_mass (ψ : Amplitude ι) (hnorm : IsNormalized ψ) + (L : Submodule (ZMod 2) (Label (ZMod 2) ι)) (heig : HasEigenlabels ψ L) + (hfull : Module.finrank (ZMod 2) (diagonalSpace L) = Fintype.card ι) : + ∃ z, ∀ x, bornWeight ψ x = if x = z then 1 else 0 := by + obtain ⟨z, hz⟩ := normalized_has_nonzero_amplitude ψ hnorm + have hzero : ∀ x, x ≠ z → ψ x = 0 := by + intro x hx + by_contra hnx + exact hx (full_diagonal_support_unique ψ L heig hfull x z hnx hz) + have hmass : bornWeight ψ z = 1 := by + calc + bornWeight ψ z = ∑ x, bornWeight ψ x := by + symm + apply Finset.sum_eq_single z + · intro x _ hx + exact (bornWeight_eq_zero ψ x).mpr (hzero x hx) + · simp + _ = 1 := hnorm + refine ⟨z, ?_⟩ + intro x + by_cases hx : x = z + · simpa [hx] using hmass + · simp [hx, bornWeight, hzero x hx] + +/-- Full diagonal rank identifies the amplitude with a basis vector times +a unit-modulus scalar, making the global-phase qualification explicit. -/ +theorem full_diagonal_basis_amplitude (ψ : Amplitude ι) (hnorm : IsNormalized ψ) + (L : Submodule (ZMod 2) (Label (ZMod 2) ι)) (heig : HasEigenlabels ψ L) + (hfull : Module.finrank (ZMod 2) (diagonalSpace L) = Fintype.card ι) : + ∃ z c, Complex.normSq c = 1 ∧ ψ = fun x => if x = z then c else 0 := by + obtain ⟨z, hp⟩ := full_diagonal_bornWeight_point_mass ψ hnorm L heig hfull + refine ⟨z, ψ z, ?_, ?_⟩ + · simpa [bornWeight] using hp z + · funext x + by_cases hx : x = z + · simp [hx] + · have hzero : bornWeight ψ x = 0 := by simpa [hx] using hp x + simp [hx, (bornWeight_eq_zero ψ x).mp hzero] + +/-- Two independent fresh computational measurements followed by subtraction. +The second distribution is constant in the first outcome, so this is an +independent product experiment expressed with mathlib's PMF bind/map. -/ +def bornDifferencePMF (ψ : Amplitude ι) (hnorm : IsNormalized ψ) : PMF (Bits ι) := + (bornPMF ψ hnorm).bind (fun x => PMF.map (fun y => x - y) (bornPMF ψ hnorm)) + +omit [DecidableEq ι] [Fintype ι] in +theorem pmf_map_sub_left_apply (p : PMF (Bits ι)) (x u : Bits ι) : + PMF.map (fun y => x - y) p u = p (x - u) := by + classical + rw [PMF.map_apply, tsum_eq_single (x - u)] + · simp + · intro y hy + apply ite_eq_right + intro heq + have hxy : x - u = y := by rw [heq]; simp + exact hy hxy.symm + +/-- The PMF subtraction pushforward equals the usual finite convolution +formula, derived from bind and map rather than assumed. -/ +theorem bornDifferencePMF_apply (ψ : Amplitude ι) (hnorm : IsNormalized ψ) + (u : Bits ι) : + bornDifferencePMF ψ hnorm u = + ENNReal.ofReal (∑ x, bornWeight ψ x * bornWeight ψ (x - u)) := by + classical + calc + bornDifferencePMF ψ hnorm u = + ∑ x, ENNReal.ofReal (bornWeight ψ x) * + ENNReal.ofReal (bornWeight ψ (x - u)) := by + simp only [bornDifferencePMF, PMF.bind_apply, pmf_map_sub_left_apply, + tsum_fintype, bornPMF_apply] + _ = ENNReal.ofReal (∑ x, bornWeight ψ x * bornWeight ψ (x - u)) := by + rw [ENNReal.ofReal_sum_of_nonneg + (fun x _ => mul_nonneg (bornWeight_nonneg ψ x) (bornWeight_nonneg ψ (x - u)))] + apply Finset.sum_congr rfl + intro x _ + exact (ENNReal.ofReal_mul (bornWeight_nonneg ψ x)).symm + +/-- Finite convolution of one uniform affine distribution removes its affine +offset and gives the uniform distribution on its direction subgroup. -/ +theorem uniform_affine_difference_mass (ψ : Amplitude ι) + (V : AddSubgroup (Bits ι)) (z : Bits ι) + (hp : ∀ x, bornWeight ψ x = + if x ∈ affineCoset V z then 1 / (Nat.card V : ℝ) else 0) + (u : Bits ι) : + (∑ x, bornWeight ψ x * bornWeight ψ (x - u)) = + if u ∈ V then 1 / (Nat.card V : ℝ) else 0 := by + classical + have hc : (Nat.card V : ℝ) ≠ 0 := by + simp only [Nat.card_eq_fintype_card] + exact_mod_cast Fintype.card_ne_zero + by_cases hu : u ∈ V + · rw [ite_eq_left hu] + have hshift (x : Bits ι) : x - u ∈ affineCoset V z ↔ x ∈ affineCoset V z := by + rw [mem_affineCoset, mem_affineCoset] + constructor + · intro hx + have h := V.add_mem hx hu + convert h using 1; abel + · intro hx + have h := V.sub_mem hx hu + convert h using 1; abel + have hprod (x : Bits ι) : bornWeight ψ x * bornWeight ψ (x - u) = + if x ∈ affineCoset V z then (1 / (Nat.card V : ℝ)) ^ 2 else 0 := by + rw [hp x, hp (x - u)] + simp only [hshift x] + split_ifs <;> ring + calc + (∑ x, bornWeight ψ x * bornWeight ψ (x - u)) = + ∑ x ∈ affineCoset V z, (1 / (Nat.card V : ℝ)) ^ 2 := by + simp_rw [hprod] + rw [← Finset.sum_filter] + congr 1 + ext y + simp only [Finset.mem_filter, Finset.mem_univ, true_and] + _ = (Nat.card V : ℝ) * (1 / (Nat.card V : ℝ)) ^ 2 := by + simp [affineCoset_card, nsmul_eq_mul] + _ = 1 / (Nat.card V : ℝ) := by field_simp + · rw [ite_eq_right hu] + apply Finset.sum_eq_zero + intro x _ + by_cases hx : x ∈ affineCoset V z + · have hy : x - u ∉ affineCoset V z := by + intro hy + apply hu + have h := V.sub_mem ((mem_affineCoset V z x).mp hx) + ((mem_affineCoset V z (x - u)).mp hy) + convert h using 1; abel + rw [hp x, hp (x - u), ite_eq_left hx, ite_eq_right hy, mul_zero] + · rw [hp x, ite_eq_right hx, zero_mul] + +/-- Actual independent Born-measurement differences of a stabilizer state +have the uniform PMF on its X projection. The only assumptions are the +quantum eigenvector equations and maximal isotropic label-space structure. -/ +theorem stabilizer_bornDifferencePMF_uniform (ψ : Amplitude ι) + (hnorm : IsNormalized ψ) (L : Submodule (ZMod 2) (Label (ZMod 2) ι)) + (heig : HasEigenlabels ψ L) (hiso : IsIsotropic L) + (hdim : Module.finrank (ZMod 2) L = Fintype.card ι) (u : Bits ι) : + bornDifferencePMF ψ hnorm u = if u ∈ xProjection L then + ENNReal.ofReal (1 / (Nat.card (xProjection L) : ℝ)) else 0 := by + classical + obtain ⟨z, hp⟩ := stabilizer_uniform_bornWeight ψ hnorm L heig hiso hdim + rw [bornDifferencePMF_apply, + uniform_affine_difference_mass ψ (xProjection L).toAddSubgroup z hp u] + split_ifs <;> simp_all + +theorem PureStabilizerState.bornDifferencePMF_uniform (S : PureStabilizerState ι) + (u : Bits ι) : bornDifferencePMF S.amplitude S.normalized u = + if u ∈ xProjection S.labels then + ENNReal.ofReal (1 / (Nat.card (xProjection S.labels) : ℝ)) else 0 := + stabilizer_bornDifferencePMF_uniform S.amplitude S.normalized S.labels + S.eigenlabels S.isotropic S.maximal u + +end LeanPool.SingleCopyStabilizer diff --git a/LeanPool/SingleCopyStabilizer/Symplectic.lean b/LeanPool/SingleCopyStabilizer/Symplectic.lean new file mode 100644 index 0000000000..78bc8db9a9 --- /dev/null +++ b/LeanPool/SingleCopyStabilizer/Symplectic.lean @@ -0,0 +1,303 @@ +/- +Copyright (c) 2026 Antonio Anna Mele. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Antonio Anna Mele +-/ +module + +public import Mathlib.Algebra.Field.ZMod +public import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas +public import Mathlib.Data.Matrix.Mul +public import Mathlib.Data.ZMod.Basic +public import Mathlib.Tactic.Abel +public import Mathlib.Tactic.Ring + + + +/-! +# The algebraic adaptive update + +The supporting linear algebra is stated over a field and is specialized to +qubits (`ZMod 2`) in `Round.lean`. These are statements about unsigned Pauli +labels. The qudit extension is outside this formalization. The identification +with unitary conjugation is proved in the physical gate modules. +-/ + +@[expose] public section + +namespace LeanPool.SingleCopyStabilizer + +variable {𝕜 : Type*} [Field 𝕜] {ι : Type*} [Fintype ι] [DecidableEq ι] + +/-- Coordinate vectors indexed by the register sites. -/ +abbrev Vec (𝕜 : Type*) (ι : Type*) := ι → 𝕜 +/-- Pauli labels paired into X and Z coordinate vectors. -/ +abbrev Label (𝕜 : Type*) (ι : Type*) := Vec 𝕜 ι × Vec 𝕜 ι + +/-- The alternating X-Z pairing controlling Pauli commutation. -/ +def symplectic (a b : Label 𝕜 ι) : 𝕜 := + a.1 ⬝ᵥ b.2 - a.2 ⬝ᵥ b.1 + +/-- Pairwise vanishing of the symplectic pairing on a label space. -/ +def IsIsotropic (L : Submodule 𝕜 (Label 𝕜 ι)) : Prop := + ∀ a ∈ L, ∀ b ∈ L, symplectic a b = 0 + +/-- Z labels whose paired X coordinate is zero in the label space. -/ +def diagonalSpace (L : Submodule 𝕜 (Label 𝕜 ι)) : Submodule 𝕜 (Vec 𝕜 ι) where + carrier := {s | (0, s) ∈ L} + zero_mem' := L.zero_mem + add_mem' ha hb := by simpa using L.add_mem ha hb + smul_mem' c _ ha := by simpa using L.smul_mem c ha + +omit [DecidableEq ι] [Fintype ι] in +@[simp] theorem mem_diagonalSpace (L : Submodule 𝕜 (Label 𝕜 ι)) (s : Vec 𝕜 ι) : + s ∈ diagonalSpace L ↔ (0, s) ∈ L := Iff.rfl + +omit [DecidableEq ι] in +/-- Commuting with a diagonal stabilizer forces orthogonality of the X label. -/ +theorem x_orthogonal_diagonal {L : Submodule 𝕜 (Label 𝕜 ι)} + (hL : IsIsotropic L) {x z s : Vec 𝕜 ι} + (hxz : (x, z) ∈ L) (hs : s ∈ diagonalSpace L) : x ⬝ᵥ s = 0 := by + classical + simpa [symplectic] using hL (x, z) hxz (0, s) hs + +/-- X-coordinate action of a simultaneous controlled-SUM shear. -/ +def shearX (i : ι) (w x : Vec 𝕜 ι) : Vec 𝕜 ι := x - x i • w + +/-- Contragradient action on Z coordinates. -/ +def shearZ (i : ι) (w z : Vec 𝕜 ι) : Vec 𝕜 ι := + z + (w ⬝ᵥ z) • (Pi.single i 1 : Vec 𝕜 ι) + +omit [DecidableEq ι] [Fintype ι] in +@[simp] theorem shearX_pivot (i : ι) {w : Vec 𝕜 ι} (hw : w i = 0) + (x : Vec 𝕜 ι) : shearX i w x i = x i := by + classical + simp [shearX, hw] + +@[simp] theorem shearZ_pivot (i : ι) (w z : Vec 𝕜 ι) : + shearZ i w z i = z i + w ⬝ᵥ z := by simp [shearZ] + +/-- The two shear actions preserve the X-Z pairing. -/ +theorem shear_pairing (i : ι) {w : Vec 𝕜 ι} (hw : w i = 0) + (x z : Vec 𝕜 ι) : shearX i w x ⬝ᵥ shearZ i w z = x ⬝ᵥ z := by + simp [shearX, shearZ, dotProduct_add, sub_dotProduct, hw] + ring + +/-- The invertible dual shear when the target mask vanishes at the pivot. -/ +def shearZEquiv (i : ι) (w : Vec 𝕜 ι) (hw : w i = 0) : + Vec 𝕜 ι ≃ₗ[𝕜] Vec 𝕜 ι where + toFun := shearZ i w + invFun z := z - (w ⬝ᵥ z) • (Pi.single i 1 : Vec 𝕜 ι) + left_inv z := by + simp [shearZ, dotProduct_add, hw] + right_inv z := by + simp [shearZ, dotProduct_sub, hw] + map_add' x y := by + simp [shearZ, dotProduct_add, add_smul] + abel + map_smul' c x := by + simp [shearZ, smul_add, smul_smul] + +omit [Fintype ι] in +/-- A normalized sample is concentrated on the chosen pivot. -/ +theorem pivot_concentrates {u : Vec 𝕜 ι} {i : ι} (hu : u i = 1) : + shearX i (u - (Pi.single i 1 : Vec 𝕜 ι)) u = (Pi.single i 1 : Vec 𝕜 ι) := by + classical + simp [shearX, hu] + +/-- Orthogonality is exactly what makes the transformed old Z label vanish at the pivot. -/ +theorem pivot_diagonal_zero {u s : Vec 𝕜 ι} {i : ι} + (horth : u ⬝ᵥ s = 0) : shearZ i (u - (Pi.single i 1 : Vec 𝕜 ι)) s i = 0 := by + simp [shearZ, sub_dotProduct, horth] + +/-- A local Fourier/phase correction, with determinant one over any field. -/ +def localCorrection (i : ι) (b : 𝕜) (a : Label 𝕜 ι) : Label 𝕜 ι := + (Function.update a.1 i (a.2 i + b * a.1 i), + Function.update a.2 i (-a.1 i)) + +omit [Fintype ι] in +theorem localCorrection_old_diagonal {s : Vec 𝕜 ι} {i : ι} (hs : s i = 0) + (b : 𝕜) : localCorrection i b (0, s) = (0, s) := by + classical + ext j <;> by_cases hj : j = i <;> simp [localCorrection, hj, hs] + +omit [Fintype ι] in +theorem localCorrection_new_diagonal (i : ι) (z : Vec 𝕜 ι) : + localCorrection i (-z i) ((Pi.single i 1 : Vec 𝕜 ι), z) = + (0, Function.update z i (-1)) := by + classical + apply Prod.ext + · funext j + by_cases hj : j = i <;> simp [localCorrection, hj] + · simp [localCorrection] +/-- Compose the pivot shear with its local Fourier and phase correction. -/ +def adaptiveUpdate (i : ι) (u : Vec 𝕜 ι) (b : 𝕜) (a : Label 𝕜 ι) : + Label 𝕜 ι := + localCorrection i b (shearX i (u - (Pi.single i 1 : Vec 𝕜 ι)) a.1, + shearZ i (u - (Pi.single i 1 : Vec 𝕜 ι)) a.2) + +theorem adaptiveUpdate_preserves_diagonal {u s : Vec 𝕜 ι} {i : ι} + (horth : u ⬝ᵥ s = 0) (b : 𝕜) : + adaptiveUpdate i u b (0, s) = (0, shearZ i (u - (Pi.single i 1 : Vec 𝕜 ι)) s) := by + simp only [adaptiveUpdate, shearX, Pi.zero_apply, zero_smul, sub_zero] + exact localCorrection_old_diagonal (pivot_diagonal_zero horth) b + +theorem adaptiveUpdate_creates_diagonal {u v : Vec 𝕜 ι} {i : ι} (hu : u i = 1) : + adaptiveUpdate i u (-(shearZ i (u - (Pi.single i 1 : Vec 𝕜 ι)) v) i) (u, v) = + (0, Function.update (shearZ i (u - (Pi.single i 1 : Vec 𝕜 ι)) v) i (-1)) := by + simp only [adaptiveUpdate, pivot_concentrates hu] + exact localCorrection_new_diagonal i _ + +/-- The linear map implementing the observed symplectic update. -/ +def adaptiveUpdateMap (i : ι) (u : Vec 𝕜 ι) (b : 𝕜) : + Label 𝕜 ι →ₗ[𝕜] Label 𝕜 ι where + toFun := adaptiveUpdate i u b + map_add' a c := by + ext j <;> by_cases hj : j = i <;> + simp [adaptiveUpdate, localCorrection, shearX, shearZ, hj, + dotProduct_add, add_smul] <;> ring + map_smul' c a := by + ext j <;> by_cases hj : j = i <;> + simp [adaptiveUpdate, localCorrection, shearX, shearZ, hj] <;> ring + +omit [DecidableEq ι] in +theorem symplectic_eq_sum (a c : Label 𝕜 ι) : + symplectic a c = ∑ j, (a.1 j * c.2 j - a.2 j * c.1 j) := by + classical + simp [symplectic, dotProduct, Finset.sum_sub_distrib] + +theorem localCorrection_symplectic (i : ι) (b : 𝕜) (a c : Label 𝕜 ι) : + symplectic (localCorrection i b a) (localCorrection i b c) = symplectic a c := by + simp only [symplectic_eq_sum] + apply Finset.sum_congr rfl + intro j _ + by_cases hj : j = i + · simp [localCorrection, hj] + ring + · simp [localCorrection, hj] + +theorem adaptiveUpdate_symplectic (i : ι) (u : Vec 𝕜 ι) (b : 𝕜) + (hu : u i = 1) (a c : Label 𝕜 ι) : + symplectic (adaptiveUpdate i u b a) (adaptiveUpdate i u b c) = symplectic a c := by + have hw : (u - (Pi.single i 1 : Vec 𝕜 ι)) i = 0 := by simp [hu] + rw [adaptiveUpdate, adaptiveUpdate, localCorrection_symplectic] + unfold symplectic + dsimp only + rw [shear_pairing i hw] + rw [dotProduct_comm (shearZ _ _ _), shear_pairing i hw, dotProduct_comm c.1 a.2] + +omit [DecidableEq ι] in +theorem symplectic_nondegenerate (a : Label 𝕜 ι) + (h : ∀ c, symplectic a c = 0) : a = 0 := by + classical + apply Prod.ext + · funext i + simpa [symplectic] using h (0, Pi.single i 1) + · funext i + simpa [symplectic] using h (Pi.single i 1, 0) + +theorem adaptiveUpdate_injective (i : ι) (u : Vec 𝕜 ι) (b : 𝕜) (hu : u i = 1) : + Function.Injective (adaptiveUpdateMap i u b) := by + apply LinearMap.ker_eq_bot.mp + apply LinearMap.ker_eq_bot'.mpr + intro a ha + apply symplectic_nondegenerate a + intro c + rw [← adaptiveUpdate_symplectic i u b hu] + change symplectic ((adaptiveUpdateMap i u b) a) _ = 0 + rw [ha] + simp [symplectic] + +/-- The image label space after the observed adaptive update. -/ +def updatedSpace (L : Submodule 𝕜 (Label 𝕜 ι)) (i : ι) + (u : Vec 𝕜 ι) (b : 𝕜) : Submodule 𝕜 (Label 𝕜 ι) := + L.map (adaptiveUpdateMap i u b) + +theorem updatedSpace_isotropic (L : Submodule 𝕜 (Label 𝕜 ι)) (hL : IsIsotropic L) + (i : ι) (u : Vec 𝕜 ι) (b : 𝕜) (hu : u i = 1) : + IsIsotropic (updatedSpace L i u b) := by + rintro _ ⟨a, ha, rfl⟩ _ ⟨c, hc, rfl⟩ + change symplectic (adaptiveUpdate i u b a) (adaptiveUpdate i u b c) = 0 + rw [adaptiveUpdate_symplectic i u b hu] + exact hL a ha c hc + +theorem updatedSpace_finrank (L : Submodule 𝕜 (Label 𝕜 ι)) + (i : ι) (u : Vec 𝕜 ι) (b : 𝕜) (hu : u i = 1) : + Module.finrank 𝕜 (updatedSpace L i u b) = Module.finrank 𝕜 L := by + exact (Submodule.equivMapOfInjective (adaptiveUpdateMap i u b) + (adaptiveUpdate_injective i u b hu) L).finrank_eq.symm + +/-- Every choice of the local correction does not decrease diagonal dimension. +Only orthogonality is needed, not membership of the sample in the X projection; +this distinction is essential to the low-nullity proof. -/ +theorem diagonal_finrank_monotone + (L : Submodule 𝕜 (Label 𝕜 ι)) (u : Vec 𝕜 ι) (i : ι) (b : 𝕜) + (hu : u i = 1) (horth : ∀ s ∈ diagonalSpace L, u ⬝ᵥ s = 0) : + Module.finrank 𝕜 (diagonalSpace L) ≤ + Module.finrank 𝕜 (diagonalSpace (updatedSpace L i u b)) := by + let e := shearZEquiv i (u - (Pi.single i 1 : Vec 𝕜 ι)) (by simp [hu]) + have hle : (diagonalSpace L).map e.toLinearMap ≤ + diagonalSpace (updatedSpace L i u b) := by + rintro s ⟨t, ht, rfl⟩ + exact ⟨(0, t), ht, adaptiveUpdate_preserves_diagonal (horth t ht) b⟩ + have hdim := Submodule.finrank_mono hle + simpa only [LinearEquiv.finrank_map_eq] using hdim + +omit [Fintype ι] in +/-- The newly created diagonal label is outside the span of all old labels, +because the entire old subspace vanishes at the pivot. -/ +theorem new_diagonal_independent {D : Submodule 𝕜 (Vec 𝕜 ι)} {i : ι} + (hD : ∀ s ∈ D, s i = 0) (z : Vec 𝕜 ι) : + Function.update z i (-1) ∉ D := by + classical + intro hz + have h := hD _ hz + simp at h + +/-- Exact algebraic content of the increase in diagonal-stabilizer dimension. +`L'` can be any submodule containing the updated labels; no dimension increase +is assumed. The result is deduced from the explicit fresh pivot coordinate. -/ +theorem diagonal_finrank_strict_progress + (L L' : Submodule 𝕜 (Label 𝕜 ι)) (u v : Vec 𝕜 ι) (i : ι) + (hu : u i = 1) (huv : (u, v) ∈ L) + (horth : ∀ s ∈ diagonalSpace L, u ⬝ᵥ s = 0) + (hupdate : ∀ a ∈ L, + adaptiveUpdate i u (-(shearZ i (u - (Pi.single i 1 : Vec 𝕜 ι)) v) i) a ∈ L') : + Module.finrank 𝕜 (diagonalSpace L) < Module.finrank 𝕜 (diagonalSpace L') := by + let e := shearZEquiv i (u - (Pi.single i 1 : Vec 𝕜 ι)) (by simp [hu]) + let D := (diagonalSpace L).map e.toLinearMap + have hle : D ≤ diagonalSpace L' := by + rintro s ⟨t, ht, rfl⟩ + have h := hupdate (0, t) ht + rw [adaptiveUpdate_preserves_diagonal (horth t ht)] at h + exact h + have hzero : ∀ s ∈ D, s i = 0 := by + rintro s ⟨t, ht, rfl⟩ + exact pivot_diagonal_zero (horth t ht) + let z := Function.update (shearZ i (u - (Pi.single i 1 : Vec 𝕜 ι)) v) i (-1) + have hz : z ∈ diagonalSpace L' := by + have h := hupdate (u, v) huv + rw [adaptiveUpdate_creates_diagonal hu] at h + exact h + have hn : z ∉ D := new_diagonal_independent hzero _ + have hlt : D < diagonalSpace L' := lt_of_le_of_ne hle (by + intro heq + exact hn (heq.symm ▸ hz)) + have hdim := Submodule.finrank_lt_finrank_of_lt hlt + simpa only [D, LinearEquiv.finrank_map_eq] using hdim + +/-- For an isotropic space and a genuine nonzero stabilizer X label, +there exists a local slope which strictly increases diagonal dimension. -/ +theorem exists_diagonal_finrank_progress + (L : Submodule 𝕜 (Label 𝕜 ι)) (hL : IsIsotropic L) + (u v : Vec 𝕜 ι) (i : ι) (hu : u i = 1) (huv : (u, v) ∈ L) : + ∃ b : 𝕜, Module.finrank 𝕜 (diagonalSpace L) < + Module.finrank 𝕜 (diagonalSpace (updatedSpace L i u b)) := by + refine ⟨-(shearZ i (u - (Pi.single i 1 : Vec 𝕜 ι)) v) i, ?_⟩ + apply diagonal_finrank_strict_progress L _ u v i hu huv + · intro s hs + exact x_orthogonal_diagonal hL huv hs + · intro a ha + exact ⟨a, ha, rfl⟩ + +end LeanPool.SingleCopyStabilizer diff --git a/LeanPool/SingleCopyStabilizer/Transcript.lean b/LeanPool/SingleCopyStabilizer/Transcript.lean new file mode 100644 index 0000000000..9657d3467e --- /dev/null +++ b/LeanPool/SingleCopyStabilizer/Transcript.lean @@ -0,0 +1,108 @@ +/- +Copyright (c) 2026 Antonio Anna Mele. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Antonio Anna Mele +-/ +module + +public import LeanPool.SingleCopyStabilizer.OutputCorrectness +public import LeanPool.SingleCopyStabilizer.ExactResources + + +/-! +# Finite classical exact-learning transcripts + +Every possible returned description contains exactly the prescribed number +of round records. The copy and gate bounds therefore apply to the actual +classical output distribution, rather than an unrelated arbitrary list. +-/ + +@[expose] public section + +noncomputable section + +namespace LeanPool.SingleCopyStabilizer.Transcript + +open Measurement OutputCorrectness +variable {ι : Type*} [Fintype ι] [DecidableEq ι] + +/-- The physical experiment retaining its circuit record and final readout. -/ +abbrev transcriptPMF (T : ℕ) (S : PureStabilizerState ι) : PMF (Description ι) := + descriptionPMF T S + +/-- Its decoded interpretation is exactly the proved output-state law. -/ +theorem transcriptPMF_decode (T : ℕ) (S : PureStabilizerState ι) : + (transcriptPMF T S).map (fun d => Circuit.decode d.1 d.2) = outputPMF T S := + descriptionPMF_decode T S + +/-- Every possible transcript records exactly one outcome per scheduled round, +including zero differences that append no quantum gates. -/ +theorem supported_length (T : ℕ) (S : PureStabilizerState ι) (d : Description ι) + (hd : d ∈ (transcriptPMF T S).support) : d.1.length = T := by + classical + induction T generalizing S d with + | zero => + change d ∈ (descriptionPMF 0 S).support at hd + rw [descriptionPMF, PMF.mem_support_map_iff] at hd + obtain ⟨z, _, rfl⟩ := hd + rfl + | succ T ih => + change d ∈ (descriptionPMF (T + 1) S).support at hd + rw [descriptionPMF, PMF.mem_support_bind_iff] at hd + obtain ⟨o, _, hd⟩ := hd + rw [PMF.mem_support_map_iff] at hd + obtain ⟨e, he, rfl⟩ := hd + simpa using congrArg Nat.succ (ih (QuantumRound.quantumRound S o) e he) + +/-- Histories of the wrong length have exactly zero output probability. -/ +theorem zero_of_length_ne (T : ℕ) (S : PureStabilizerState ι) (d : Description ι) + (hlen : d.1.length ≠ T) : transcriptPMF T S d = 0 := by + classical + by_contra hne + exact hlen (supported_length T S d ((PMF.mem_support_iff _ _).mpr hne)) + +/-- The returned finite description corresponds to exactly `2T+1` consumed +input copies, for every possible run and independently of success. -/ +theorem supported_copy_count (T : ℕ) (S : PureStabilizerState ι) (d : Description ι) + (hd : d ∈ (transcriptPMF T S).support) : + ExactResources.protocolCopyCount d.1 = 2 * T + 1 := + ExactResources.protocolCopyCount_eq d.1 T (supported_length T S d hd) + +/-- At most `(n+1)T` elementary instructions describe the final circuit. -/ +theorem supported_circuit_gate_count (T : ℕ) (S : PureStabilizerState ι) + (d : Description ι) (hd : d ∈ (transcriptPMF T S).support) : + ExactResources.listCircuitGateCount d.1 ≤ (Fintype.card ι + 1) * T := by + classical + simpa only [supported_length T S d hd] using ExactResources.listCircuitGateCount_le d.1 + +/-- All gates used on the fresh copies and final readout total at most +`(n+1)T²`, for every supported classical output description. -/ +theorem supported_protocol_gate_cost (T : ℕ) (S : PureStabilizerState ι) + (d : Description ι) (hd : d ∈ (transcriptPMF T S).support) : + ExactResources.protocolGateCost d.1 ≤ (Fintype.card ι + 1) * T ^ 2 := by + classical + simpa only [supported_length T S d hd] using ExactResources.protocolGateCost_le d.1 + +theorem supported_protocol_gate_cost_two_n (T : ℕ) (S : PureStabilizerState ι) + (d : Description ι) (hd : d ∈ (transcriptPMF T S).support) + (hn : 1 ≤ Fintype.card ι) : + ExactResources.protocolGateCost d.1 ≤ 2 * Fintype.card ι * T ^ 2 := by + classical + simpa only [supported_length T S d hd] using + ExactResources.protocolGateCost_le_two_n d.1 hn + +open Classical in +/-- Correctness stated directly on the recorded finite output, with any +round count at least the proved confidence budget. -/ +theorem failure_probability_after_budget (S : PureStabilizerState ι) + (δ : ℝ) (hδ : 0 < δ) (hδmax : δ ≤ 1) (T : ℕ) + (hT : SharpExactLearning.roundBudget (Fintype.card ι) δ ≤ T) : + ((transcriptPMF T S).map fun d => + decide (SameRay S.amplitude (Circuit.decode d.1 d.2))) false ≤ ENNReal.ofReal δ := by + classical + have h := exact_learning_failure_probability_after_budget S δ hδ hδmax T hT + unfold outputFailure at h + rw [← transcriptPMF_decode, PMF.map_comp] at h + exact h + +end LeanPool.SingleCopyStabilizer.Transcript diff --git a/LeanPool/projects/single-copy-stabilizer-learning.yaml b/LeanPool/projects/single-copy-stabilizer-learning.yaml new file mode 100644 index 0000000000..eef86f62ed --- /dev/null +++ b/LeanPool/projects/single-copy-stabilizer-learning.yaml @@ -0,0 +1,34 @@ +slug: single-copy-stabilizer-learning +title: Exact adaptive single-copy stabilizer learning +summary: Exact recovery of pure qubit stabilizer states from adaptive single-copy measurements, with + explicit confidence, copy and elementary gate upper bounds. +branch: quantum information +entry_module: LeanPool.SingleCopyStabilizer +authors: +- Antonio Anna Mele +source: + arxiv: '2610.02031' + github_repo: AntMele/single-copy-stabilizer-learning-lean +license: MIT +status: verified +provenance: AI +main_declarations: +- LeanPool.SingleCopyStabilizer.ExactLearningTheorem.exact_learning +main_results: +- declaration: LeanPool.SingleCopyStabilizer.ExactLearningTheorem.exact_learning + informal: For every normalized pure qubit stabilizer state and failure parameter 0 < delta <= 1, + the physical learner returns a finite circuit and readout that decode to the input up to global + phase with probability at least 1 - delta. Every supported execution uses exactly 2T + 1 copies + and at most (n + 1)T^2 elementary gate applications at the stated round budget T. +- declaration: LeanPool.SingleCopyStabilizer.ExactLearningTheorem.exact_learning_copy_bound_linear + informal: For n >= 1, every supported output at the confidence budget consumes fewer than 136(n + + log(1 / delta)) input copies. +tags: +- quantum-computing +- stabilizer-states +- quantum-learning +- probability +msc: +- 81P68 +- 68Q32 +- 81P45