Theory Pure_O2H
theory Pure_O2H
imports Run_Pure_B
Run_Pure_B_count
begin
unbundle cblinfun_syntax
unbundle lattice_syntax
unbundle register_syntax
context pure_o2h
begin
text ‹The probability that the find event occurs. That is the event that the adversary $B$ notices
that a query in $S$ was made.›
definition ‹Pfind' = (norm (Snd (id_cblinfun - selfbutter (ket empty)) *⇩V run_B))⇧2›
text ‹What happens only to the first part of the memory when executing ‹B› or ‹B_count› is the same.
This is recorded in ‹Φ›. The second registers only serve as counting registers.›
definition Φs where
"Φs n = run_pure_adv n (λi. UA i) (λ_. not_S_embed S) init X Y H"
text ‹We ensure that the $\Phi s$ is the same as the left part of $\Psi_{count}$
(ie.\ ‹run_B_count›) with right part $\mid 0 \rangle$.›
lemma Ψs_run_B_count_upto_eq_Φs:
assumes "i<d+1"
shows "Ψs 0 (run_B_count_upto i) = Φs i"
using le0 proof (induction i rule: Nat.dec_induct)
case base
then show ?case unfolding run_B_count_upto_def init_B_count_def Φs_def
by (auto simp add: tensor_op_ell2 tensor_ell2_ket Ψs_def)
next
case (step n)
then have "n<d" using assms by auto
have "Ψs 0 (run_B_count_upto (Suc n)) = UA (Suc n) *⇩V (X;Y) (Uquery H) *⇩V
Ψs 0 (U_S' S *⇩V Proj_ket_set {..<n+1} *⇩V
run_pure_adv n (λi. UA i ⊗⇩o id_cblinfun) (λ_. U_S' S) init_B_count X_for_C Y_for_C H)"
using run_B_count_projection
by (auto simp add: Ψs_id_cblinfun UqueryH_tensor_id_cblinfunC run_B_count_upto_def)
also have "… = UA (Suc n) *⇩V (X;Y) (Uquery H) *⇩V
(not_S_embed S *⇩V tensor_ell2_right (ket 0)* *⇩V
run_pure_adv n (λi. UA i ⊗⇩o id_cblinfun) (λ_. U_S' S) init_B_count X_for_C Y_for_C H)"
using Ψs_U_S'_Proj_ket_upto[OF ‹n<d›]
by (metis (no_types, lifting) Ψs_def cblinfun_apply_cblinfun_compose)
also have "… = UA (Suc n) *⇩V (X;Y) (Uquery H) *⇩V
not_S_embed S *⇩V run_pure_adv n UA (λ_. not_S_embed S) init X Y H"
using step by (simp add: Φs_def Ψs_def run_B_count_upto_def)
finally show ?case unfolding Φs_def by auto
qed
text ‹Analogously, $\Phi s$ is the same as the left part of $\Psi_{right}$ (ie.\ ‹run_B›) with
right part $\mid embed\ 0\rangle$.›
lemma Ψs_run_B_upto_eq_Φs:
assumes "i≤d"
shows "Ψs empty (run_B_upto i) = Φs i"
using le0 proof (induction i rule: Nat.dec_induct)
case base
then show ?case unfolding run_B_upto_def init_B_def Φs_def
by (auto simp add: tensor_op_ell2 tensor_ell2_ket Ψs_def)
next
case (step n)
then have "n<d" using assms by auto
have "Ψs empty (run_B_upto (Suc n)) = UA (Suc n) *⇩V (X;Y) (Uquery H) *⇩V
Ψs empty ((US S n) *⇩V Proj_ket_upto (has_bits_upto n) *⇩V run_B_upto n)"
by (subst run_B_upto_I, subst run_B_projection[OF ‹n<d›])
(auto simp add: Ψs_id_cblinfun UqueryH_tensor_id_cblinfunB)
also have "… = UA (Suc n) *⇩V (X;Y) (Uquery H) *⇩V
(not_S_embed S *⇩V tensor_ell2_right (ket empty)* *⇩V run_B_upto n)"
using Ψs_US_Proj_ket_upto[OF ‹n<d›]
by (metis (no_types, lifting) Ψs_def cblinfun_apply_cblinfun_compose)
also have "… = UA (Suc n) *⇩V (X;Y) (Uquery H) *⇩V
not_S_embed S *⇩V run_pure_adv n UA (λ_. not_S_embed S) init X Y H"
using step by (simp add: Φs_def Ψs_def run_B_upto_def init_B_count_def init_B_def)
finally show ?case unfolding Φs_def by auto
qed
text ‹For the version of o2h with ‹norm UA ≤ 1›, we need to introduce the following error term:
when an adversary does not terminate, we get an additional term in the Pfind.›
definition "P_nonterm = (norm run_B_count)⇧2 - (norm run_B)⇧2"
text ‹The One-Way-to-Hiding Lemma for pure states.
Intuition: The difference of two games where we may change queries on a set $S$ in game $B$ can
be bounded by the fining event ‹Pfind'›.
Proof idea: We introduce an intermediate game $B_{count}$ and show first equivalence between
$A$ and the left part of $B_{count}$ in $\mid 0\rangle$ and then equivalence of $B_{count}$ and $B$
in $\mid 0\rangle$.›
lemma pure_o2h: ‹(norm ((run_A ⊗⇩s ket empty) - run_B))⇧2 ≤ (d+1) * Pfind' + d * P_nonterm›
proof -
define Ψs' where "Ψs' = (λi::nat. Ψs i run_B_count)"
have eq16: "run_B_count = (∑i<d+1. Ψs' i ⊗⇩s (ket i))"
using run_B_count_split Ψs'_def by auto
define N':: "('mem × nat) update" where
"N' = (id_cblinfun ⊗⇩o (∑i<d+1. butterfly (ket 0) (ket i))) o⇩C⇩L Proj_ket_set {..<d+1}"
have *: "sum (Rep_ell2 (ket c)) {..<d + 1} *⇩C ket 0 = ket 0" if "c<d+1" for c
by (metis lessThan_iff proj_classical_set_elem sum_butterfly_ket0 sum_butterfly_ket0' that)
have N'_ket: "N' (ket (x,c)) = ket (x,0)" if "c<d+1" for x c
unfolding N'_def Proj_ket_set_def
apply (subst tensor_ell2_ket[symmetric], subst comp_tensor_op, subst tensor_op_ell2)
apply (subst (2) cblinfun_apply_cblinfun_compose, subst sum_butterfly_ket0')
apply (subst *[OF that])
by (auto simp add: tensor_ell2_ket[symmetric])
have N'_tensor_ket: "N' *⇩V y ⊗⇩s ket c = y ⊗⇩s ket 0" if "c<d+1" for c y unfolding N'_def
proof (subst cblinfun_apply_cblinfun_compose, subst Proj_ket_set_vec)
show "c ∈ {..<d + 1}" using that by auto
then show "(id_cblinfun ⊗⇩o (∑i<d + 1. butterfly (ket 0) (ket i))) *⇩V y ⊗⇩s ket c = y ⊗⇩s ket 0"
by (subst tensor_op_ell2, subst sum_butterfly_ket0) auto
qed
have N'_UA: "N' o⇩C⇩L (UA i ⊗⇩o id_cblinfun) = (UA i ⊗⇩o id_cblinfun) o⇩C⇩L N'" for i
unfolding N'_def by (simp add: Proj_ket_set_def comp_tensor_op)
have N'_UqueryH: "N' o⇩C⇩L (X_for_C;Y_for_C) (Uquery H) = (X_for_C;Y_for_C) (Uquery H) o⇩C⇩L N'"
unfolding UqueryH_tensor_id_cblinfunC by (simp add: N'_def Proj_ket_set_def comp_tensor_op)
have N'_B_count: "N' o⇩C⇩L U_S' S = N'"
proof (unfold N'_def, intro equal_ket, safe, goal_cases)
case (1 a b)
show ?case proof (cases "b<d+1")
case True
obtain y where y: "Uc *⇩V ket b = ket y" "y<d+1"
using True Uc_ket_range_valid by auto
have proj_y:"proj_classical_set {..<Suc d} *⇩V ket y = ket y" using ‹y<d+1›
by (metis Suc_eq_plus1 lessThan_iff proj_classical_set_elem)
have proj_b:"proj_classical_set {..<Suc d} *⇩V ket b = ket b" using True
by (metis Suc_eq_plus1 lessThan_iff proj_classical_set_elem)
have butter_y: "(∑i<d+1. butterfly (ket 0) (ket i)) *⇩V ket y = ket 0"
using sum_butterfly_ket0 y(2) by blast
have butter_b: "(∑i<d+1. butterfly (ket 0) (ket i)) *⇩V ket b = ket 0"
using sum_butterfly_ket0 True by blast
have "(S_embed S *⇩V ket a) ⊗⇩s (∑i<d+1. butterfly (ket 0) (ket i)) *⇩V ket y +
(not_S_embed S *⇩V ket a) ⊗⇩s (∑i<d+1. butterfly (ket 0) (ket i)) *⇩V ket b =
ket a ⊗⇩s (∑i<d+1. butterfly (ket 0) (ket i)) *⇩V ket b"
unfolding butter_y butter_b by (metis S_embed_not_S_embed_add tensor_ell2_add1)
then show ?thesis using y proj_y proj_b
by(auto simp add: tensor_op_ell2 tensor_op_ket cblinfun.add_right
U_S'_ket_split sum_butterfly_ket0 tensor_ell2_add1[symmetric] Proj_ket_set_def)
next
case False
then show ?thesis
by (metis (no_types, lifting) S_embed_not_S_embed_add U_S'_ket_split Uc_ket_greater
lift_cblinfun_comp(4) not_less_eq semiring_norm(174) tensor_ell2_add1 tensor_ell2_ket)
qed
qed
have "0<d+1" using d_gr_0 by auto
have N'_init_B_count: "N' *⇩V init_B_count = init_B_count"
unfolding init_B_count_def using N'_def N'_tensor_ket[OF ‹0<d+1›] by blast
have N'_run_B_count_upto_N'_run_A: "N' *⇩V run_B_count_upto n =
N' *⇩V (run_pure_adv n UA (λ_. id_cblinfun) init X Y H ⊗⇩s ket (0))" for n
unfolding run_B_count_upto_def run_A_def
proof (induction n)
case 0
have "N' *⇩V U_S' S *⇩V (UA 0 ⊗⇩o id_cblinfun) *⇩V init_B_count =
(UA 0 ⊗⇩o id_cblinfun o⇩C⇩L N') *⇩V init_B_count"
by (auto simp add: cblinfun_apply_cblinfun_compose[symmetric] N'_B_count
N'_init_B_count N'_UA cblinfun_compose_assoc[symmetric]
simp del: cblinfun_apply_cblinfun_compose)
also have "… = (UA 0 ⊗⇩o id_cblinfun) *⇩V init_B_count" using N'_init_B_count by auto
finally show ?case by (auto simp add: N'_UA N'_tensor_ket tensor_op_ell2 init_B_count_def)
next
case (Suc n)
let ?run_pure_adv_B_count_d =
"run_pure_adv n (λi. UA i ⊗⇩o id_cblinfun) (λ_. U_S' S) init_B_count X_for_C Y_for_C H"
let ?run_pure_adv_A_d = "run_pure_adv n UA (λ_. id_cblinfun) init X Y H"
have "N' *⇩V run_pure_adv (n+1) (λi. UA i ⊗⇩o id_cblinfun) (λ_. U_S' S)
init_B_count X_for_C Y_for_C H =
(UA (Suc n) ⊗⇩o id_cblinfun o⇩C⇩L (X_for_C;Y_for_C) (Uquery H) o⇩C⇩L N') *⇩V ?run_pure_adv_B_count_d"
using N'_B_count N'_UA N'_UqueryH
by (auto simp add: cblinfun_apply_cblinfun_compose[symmetric]
cblinfun_compose_assoc[symmetric] simp del: cblinfun_apply_cblinfun_compose)
(auto simp add: cblinfun_compose_assoc)
also have "… = (UA (Suc n) ⊗⇩o id_cblinfun o⇩C⇩L (X_for_C;Y_for_C) (Uquery H)) *⇩V
N' *⇩V ?run_pure_adv_A_d ⊗⇩s ket 0"
by (simp add: Suc.IH)
also have "… = (N' o⇩C⇩L UA (Suc n) ⊗⇩o id_cblinfun o⇩C⇩L (X_for_C;Y_for_C) (Uquery H)) *⇩V
?run_pure_adv_A_d ⊗⇩s ket 0"
using N'_B_count N'_UA N'_UqueryH
by (auto simp add: cblinfun_apply_cblinfun_compose[symmetric]
cblinfun_compose_assoc[symmetric] simp del: cblinfun_apply_cblinfun_compose)
(auto simp add: cblinfun_compose_assoc)
finally show ?case
by (auto simp add: UqueryH_tensor_id_cblinfunC tensor_op_ell2 nth_append)
qed
have N'_run_B_count_N'_run_A: "N' *⇩V run_B_count = N' *⇩V (run_A ⊗⇩s ket (0))"
unfolding run_B_count_altdef by (subst N'_run_B_count_upto_N'_run_A)
(auto simp add: run_A_def)
then have N'_run_B_count_run_A: "N' *⇩V run_B_count = run_A ⊗⇩s ket 0"
by (simp add: N'_tensor_ket)
have "(∑i<d+1. Ψs' i ⊗⇩s ket (0::nat)) = N' *⇩V run_B_count" unfolding eq16
by (subst cblinfun.sum_right, intro sum.cong) (auto simp add: N'_tensor_ket)
moreover have "N' *⇩V run_B_count = run_A ⊗⇩s ket (0::nat)"
unfolding N'_run_B_count_N'_run_A by (auto simp add: N'_tensor_ket)
ultimately have Ψs'_run_A:
"(∑i<d+1. Ψs' i ⊗⇩s ket (0::nat)) = run_A ⊗⇩s ket (0)" by auto
have eq17: "run_A = (∑i<d+1. Ψs' i)"
proof -
have "run_A = (tensor_ell2_right (ket 0))* *⇩V (run_A ⊗⇩s ket (0::nat))" by auto
also have "… = (∑i<d+1. Ψs' i)"
unfolding Ψs'_run_A[symmetric]
by (subst tensor_ell2_sum_left[symmetric], subst tensor_ell2_right_adj_apply, auto)
finally show ?thesis by blast
qed
define ΨsB where "ΨsB = (λi::bool list. Ψs (list_to_l i) run_B)"
have eq18: "run_B = (∑l∈len_d_lists. ΨsB l ⊗⇩s ket (list_to_l l))"
by (subst run_B_split, unfold ΨsB_def) auto
have ΨsB_Φs: "ΨsB empty_list = Φs d" by (simp add: ΨsB_def Ψs_run_B_upto_eq_Φs run_B_altdef)
have eq19: "Ψs' 0 = ΨsB empty_list"
proof -
have "Ψs' 0 = Ψs 0 (run_B_count_upto d)" unfolding Ψs'_def run_B_count_altdef by auto
also have "… = Φs d" by (simp add: Ψs_run_B_count_upto_eq_Φs)
also have "… = ΨsB empty_list" unfolding ΨsB_Φs by auto
finally show ?thesis by blast
qed
have eq20:"norm (ΨsB empty_list)^2 = (norm run_B)^2 - Pfind'"
proof -
have "norm (ΨsB empty_list)^2 = (norm (Φs d))^2" unfolding ΨsB_def run_B_altdef
by (auto simp add: Ψs_run_B_upto_eq_Φs)
also have "… = (norm run_B)^2 - (norm (run_B - Φs d ⊗⇩s ket empty))⇧2"
proof -
have norm_B: "Re (run_B ∙⇩C run_B) = (norm run_B)^2"
unfolding power2_norm_eq_cinner[symmetric] norm_run_B by auto
have cinner_B_Ψ: "(run_B) ∙⇩C (Φs d ⊗⇩s ket empty) = (Φs d) ∙⇩C (Φs d)"
proof -
have "list_to_l x = empty ⟹ x∈len_d_lists ⟹ x=empty_list" for x
using inj_list_to_l inj_onD by fastforce
then have **: "ΨsB empty_list ∙⇩C ΨsB empty_list = sum ((λl. ΨsB l ∙⇩C ΨsB empty_list *
(ket (list_to_l l) ∙⇩C ket empty))) len_d_lists"
by (subst sum.remove[OF finite_len_d_lists empty_list_len_d]) (auto intro!: sum.neutral)
show ?thesis unfolding eq18 ΨsB_Φs[symmetric] unfolding **
by (auto simp add: cinner_sum_left)
qed
have "(norm (Φs d))^2 + (norm (run_B - Φs d ⊗⇩s ket empty))^2 =
Re (Φs d ∙⇩C Φs d + (run_B - Φs d ⊗⇩s ket empty) ∙⇩C (run_B - Φs d ⊗⇩s ket empty))"
unfolding power2_norm_eq_cinner' by auto
also have "… = Re (2 * (Φs d ∙⇩C Φs d) + run_B ∙⇩C run_B - (run_B) ∙⇩C (Φs d ⊗⇩s ket empty) -
(Φs d ⊗⇩s ket empty) ∙⇩C (run_B))"
by (auto simp add: algebra_simps norm_B)
also have "… = (norm run_B)^2" by (subst (3)cinner_commute, unfold cinner_B_Ψ)
(auto simp add: norm_B)
finally have "(norm (Φs d))^2 + (norm (run_B - Φs d ⊗⇩s ket empty))^2 = (norm run_B)^2" by auto
then show ?thesis by auto
qed
also have "… = (norm run_B)^2 - (norm (run_B - (tensor_ell2_right (ket empty)* *⇩V run_B)
⊗⇩s ket empty))⇧2" unfolding run_B_def
by (subst Ψs_run_B_upto_eq_Φs[symmetric])(auto simp add: Ψs_def run_B_upto_def)
also have "… = (norm run_B)^2 - Pfind'" unfolding Pfind'_def
by (auto simp add: Snd_def tensor_op_right_minus cblinfun.diff_left
id_cblinfun_selfbutter_tensor_ell2_right)
finally show ?thesis by auto
qed
have eq20':"norm (Ψs' 0)^2 = norm (run_B)^2 - Pfind'" unfolding eq19 using eq20 by auto
have sum_to_1': "(∑i<d+1. norm (Ψs' i)^2) = (norm run_B_count)^2"
proof -
have "(∑i<d+1. norm (Ψs' i)^2) =
(∑i<d+1. norm ((Ψs' i) ⊗⇩s ket (i::nat))^2)"
by (intro sum.cong, auto simp add: norm_tensor_ell2)
also have "… = norm (∑i<d+1. (Ψs' i) ⊗⇩s ket (i::nat))^2"
by (rule pythagorean_theorem_sum[symmetric], auto)
also have "… = norm (run_B_count)^2" unfolding eq16 by auto
finally show ?thesis by auto
qed
then have eq21': "(∑i=1..<d+1. norm (Ψs' i)^2) = Pfind' + P_nonterm"
proof -
have "(∑i<d+1. norm (Ψs' i)^2) =
norm (Ψs' 0)^2 + (∑i=1..<d+1. norm (Ψs' i)^2)"
unfolding atLeast0AtMost lessThan_atLeast0
by (subst sum.atLeast_Suc_lessThan[OF ‹0<d+1›]) auto
then show ?thesis using eq20' sum_to_1' unfolding P_nonterm_def by linarith
qed
have sum_to_1:"(∑l∈len_d_lists. norm (ΨsB l)^2) = (norm run_B)^2"
proof -
have "(∑l∈len_d_lists. norm (ΨsB l)^2) =
(∑l∈len_d_lists. norm ((ΨsB l) ⊗⇩s ket (list_to_l l))^2)"
by (intro sum.cong, auto simp add: norm_tensor_ell2)
also have "… = norm (∑l∈len_d_lists. ΨsB l ⊗⇩s ket (list_to_l l))^2"
proof -
have "a ≠ a' ⟹ a∈len_d_lists ⟹ a'∈len_d_lists ⟹ list_to_l a ≠ (list_to_l a')"
for a a' by (meson inj_list_to_l inj_onD)
then show ?thesis by (subst pythagorean_theorem_sum) auto
qed
also have "… = norm (run_B)^2" unfolding eq18 by auto
finally show ?thesis by auto
qed
then have eq21: "(∑l∈has_bits {0..<d}. norm (ΨsB l)^2) = Pfind'"
proof -
have "(∑l∈len_d_lists. norm (ΨsB l)^2) =
norm (ΨsB empty_list)^2 + (∑l∈has_bits {0..<d}. norm (ΨsB l)^2)"
by (subst sum.remove[of _ empty_list], unfold len_d_empty_has_bits) auto
then show ?thesis using eq20 sum_to_1 unfolding P_nonterm_def by auto
qed
show ?thesis
proof -
have "(norm (run_A ⊗⇩s ket empty - run_B))⇧2 =
(norm (run_B - run_A ⊗⇩s ket empty))⇧2"
by (subst norm_minus_cancel[symmetric], auto)
also have "… = (norm ((ΨsB empty_list - run_A) ⊗⇩s ket empty +
(∑l∈has_bits {0..<d}. ΨsB l ⊗⇩s ket (list_to_l l))))⇧2"
proof -
have *: "(ΨsB empty_list - run_A) ⊗⇩s ket empty =
ΨsB empty_list ⊗⇩s ket empty - run_A ⊗⇩s ket empty"
using tensor_ell2_diff1 by blast
show ?thesis unfolding eq18
by (subst sum.remove[of _ empty_list], unfold * len_d_empty_has_bits)
(auto simp add: algebra_simps)
qed
also have "… = (norm ((ΨsB empty_list - run_A) ⊗⇩s ket (empty)))⇧2 +
(norm (∑l∈has_bits {0..<d}. ΨsB l ⊗⇩s ket (list_to_l l)))⇧2"
proof -
have l: "(if empty = list_to_l l then 1 else 0) = 0" if "l ∈ has_bits {0..<d}" for l
using that by (metis DiffE empty_iff has_bits_empty len_d_empty_has_bits has_bits_not_empty)
then have *: "(∑l∈has_bits {0..<d}.
(ΨsB empty_list - run_A) ∙⇩C ΨsB l * (if empty = list_to_l l then 1 else 0)) = 0"
by (smt (verit, best) class_semiring.add.finprod_all1 semiring_norm(64))
have "(∑l∈has_bits {0..<d} ∩ {l. empty = list_to_l l}.
(ΨsB empty_list - run_A) ∙⇩C ΨsB l) = 0" by (subst sum.inter_restrict, simp)
(subst (2) *[symmetric], intro sum.cong, auto)
then have "is_orthogonal ((ΨsB empty_list - run_A) ⊗⇩s ket empty)
(∑l∈has_bits {0..<d}. ΨsB l ⊗⇩s ket (list_to_l l))"
by (auto simp add: cinner_sum_right cinner_ket)
then show ?thesis by (rule pythagorean_theorem)
qed
also have "… = (norm ((ΨsB empty_list - run_A) ⊗⇩s ket empty))⇧2 +
(∑l∈has_bits {0..<d}. norm (ΨsB l)^2)"
proof -
have "a ≠ a' ⟹ a∈has_bits {0..<d} ⟹ a'∈has_bits {0..<d} ⟹
list_to_l a ≠ list_to_l a'" for a a'
by (metis DiffE inj_list_to_l inj_onD len_d_empty_has_bits)
then show ?thesis
by (subst pythagorean_theorem_sum) (auto simp add: norm_tensor_ell2)
qed
also have "… = (norm ((ΨsB empty_list - run_A) ⊗⇩s ket empty))⇧2 + Pfind'"
using eq21 by auto
also have "… = norm (∑i=1..<d+1. Ψs' i)^2 + Pfind'"
proof -
have *: "Ψs' 0 - (∑i<d+1. Ψs' i) = - (∑i=1..<d+1. Ψs' i)"
unfolding lessThan_atLeast0
by (subst sum.atLeast_Suc_lessThan[OF ‹0<d+1›]) auto
have **: "norm ((Ψs' 0 - (∑i<d+1. Ψs' i)) ⊗⇩s ket empty) =
norm (∑i = 1..<d+1. Ψs' i)"
unfolding * by (simp add: norm_tensor_ell2)
show ?thesis unfolding eq17 eq19[symmetric] ** by auto
qed
also have "… ≤ (∑i=1..<d+1. norm (Ψs' i))^2 + Pfind'"
using eq20 eq21'
by (smt (verit) power_mono[OF norm_sum norm_ge_zero] sum.cong)
also have "… ≤ d * (∑i=1..<d+1. norm (Ψs' i)^2) + Pfind'"
by (subst add_le_cancel_right)
(use arith_quad_mean_ineq[of "{1..<d+1}" "(λi. norm (Ψs' i))"] in ‹auto›)
also have "… = (d+1) * Pfind' + d * P_nonterm"
unfolding eq21' by (simp add: algebra_simps)
finally show ?thesis by linarith
qed
qed
lemma pure_o2h_sqrt: ‹norm ((run_A ⊗⇩s ket empty) - run_B) ≤ sqrt ((d+1) * Pfind' + d * P_nonterm)›
using pure_o2h real_le_rsqrt by blast
lemma error_term_pos:
"(d+1) * Pfind' + d * P_nonterm ≥ 0"
using pure_o2h by (smt (verit, best) power2_diff sum_squares_bound)
end
unbundle no cblinfun_syntax
unbundle no lattice_syntax
unbundle no register_syntax
end