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
  a query in $S$ was made.›
definition ‹Pfind' = (norm (Snd (id_cblinfun - selfbutter (ket empty)) *_V run_B))²›


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
  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:
  an adversary does not terminate, we get an additional term in the Pfind.›
definition "P_nonterm = (norm run_B_count)² - (norm run_B)²"

text ‹The One-Way-to-Hiding Lemma for pure states.
 : The difference of two games where we may change queries on a set $S$ in game $B$ can
  bounded by the fining event ‹Pfind'›.
  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$
  $\mid 0\rangle$.›
lemma pure_o2h: ‹(norm ((run_A ⊗_s ket empty) - run_B))² ≤ (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
      ―‹Equation (16)›

― ‹The operation $N'$ connects the results of the game $A$ and the counting game $B_{count}$.›

  define N':: "('mem × nat) update" where 
    "N' = (id_cblinfun ⊗_o (∑i<d+1. butterfly (ket 0) (ket i))) o_CL 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_CL (UA i ⊗_o id_cblinfun) = (UA i ⊗_o id_cblinfun) o_CL N'" for i
    unfolding N'_def by (simp add: Proj_ket_set_def comp_tensor_op)
      ―‹‹N'› commutes with ‹UA››

  have N'_UqueryH: "N' o_CL (X_for_C;Y_for_C) (Uquery H) = (X_for_C;Y_for_C) (Uquery H) o_CL N'"
    unfolding UqueryH_tensor_id_cblinfunC by (simp add: N'_def Proj_ket_set_def comp_tensor_op)
      ―‹‹N'› commutes with the oracle queries›

  have N'_B_count: "N' o_CL 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  
    ―‹‹N' U_S' = N'››

  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
      ―‹the initial state of ‹B_count› is invariant under ‹N'››

  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_CL 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_CL (X_for_C;Y_for_C) (Uquery H) o_CL 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_CL (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_CL UA (Suc n) ⊗_o id_cblinfun o_CL (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)
      ―‹‹N'› does not touch the second part of the memory and ‹run_B_count› and ‹run_A›
 do the same on ‹'mem››

  then have N'_run_B_count_run_A: "N' *_V run_B_count = run_A ⊗_s ket 0"
    by (simp add: N'_tensor_ket)
      ― ‹Relation between $A$ and $B_{count}$›


  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
    ―‹Equation (17)›
    ― ‹Representation of $A$ in terms of parts of states in $B_{count}$›

  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
      ―‹Equation (18)›


  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
    ―‹Equation (19)›
    ― ‹Relating the games $B$ and $B_{count}$.›

― ‹Now, we argue about the probabilits of the find event and the outcome states.›

  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))²"
    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))²"  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
    ―‹Equation (20)›

  have eq20':"norm (Ψs' 0)^2 = norm (run_B)^2 - Pfind'" unfolding eq19 using eq20 by auto
      ―‹Analog to Equation (20)›

  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
    ―‹Part of Equation (21)›

  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
    ―‹Part of Equation (21)›

― ‹Finally, we can subsume all our findings and prove the O2H Lemma.›

  show ?thesis 
  proof -
    have "(norm (run_A ⊗_s ket empty - run_B))² =
          (norm (run_B - run_A ⊗_s ket empty))²" 
      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))))²"
    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)))² +
      (norm (∑l∈has_bits {0..<d}. ΨsB l ⊗_s ket (list_to_l l)))²"
    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))² +
      (∑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))² + 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