Cma H3Expected Loss le query Bounds

theorem cmaH3ExpectedLoss_le_queryBounds    (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel)    (hr : GenerableRelation Stmt Wit rel)    (ζ_zk β : ℝ≥0∞)    {α : Type}    (A : OracleComp (cmaSpec M Commit Chal Resp Stmt) α)    {qS qH : ℕ}    (h_qS : OracleComp.IsQueryBoundP A      (cmaH3Costly (M := M) (Commit := Commit) (Chal := Chal)        (Resp := Resp) (Stmt := Stmt)) qS)    (h_qH : OracleComp.IsQueryBoundP A      (IsHashQuery (M := M) (Commit := Commit) (Chal := Chal)        (Resp := Resp) (Stmt := Stmt)) qH) :    cmaH3ExpectedLoss M Commit Chal σ hr ζ_zk β A qS ≤      (qS : ℝ≥0∞) * ζ_zk + (qS : ℝ≥0∞) * ((qS : ℝ≥0∞) + qH) * β := by  change expectedQuerySlack (cmaReal M Commit Chal σ hr)    (cmaH3Costly (M := M) (Commit := Commit) (Chal := Chal)      (Resp := Resp) (Stmt := Stmt))    (fun s : CmaData M Commit Chal Stmt Wit ↦ ζ_zk + QueryCache.enncard s.2.1 * β)    A qS (cmaDataInit M Commit Chal Stmt Wit, false) ≤ _  simpa [cmaDataInit, add_assoc] using    expectedQuerySlack_resource_le      (impl := cmaReal M Commit Chal σ hr)      (chargedQuery := cmaH3Costly (M := M) (Commit := Commit) (Chal := Chal)        (Resp := Resp) (Stmt := Stmt))      (growthQuery := IsHashQuery (M := M) (Commit := Commit) (Chal := Chal)        (Resp := Resp) (Stmt := Stmt))      (R := fun s : CmaData M Commit Chal Stmt Wit => QueryCache.enncard s.2.1)      (ζ := ζ_zk) (β := β)      (h_growth := by        intro t p _ htg z hz        simpa [htg] using cmaReal_roCacheCount_step_le M Commit Chal σ hr t p z hz)      (h_free := by        intro t p _ hnotCostly hnotHash z hz        simpa [hnotCostly, hnotHash] using          cmaReal_roCacheCount_step_le M Commit Chal σ hr t p z hz)      (oa := A) (qS := qS) (qH := qH)      (h_qS := h_qS) (h_qH := h_qH)      (s := cmaDataInit M Commit Chal Stmt Wit)