Nma to hard relation bound

theorem nma_to_hard_relation_bound    [DecidableEq M] [DecidableEq Commit]    [SampleableType Wit] [SampleableType Chal]    (hss : σ.SpeciallySound)    (hss_nf : ∀ ω₁ p₁ ω₂ p₂, Pr[⊥ | σ.extract ω₁ p₁ ω₂ p₂] = 0)    [Fintype Chal] [Inhabited Chal]    (nmaAdv : SignatureAlg.managedRoNmaAdv      (FiatShamir (m := OracleComp (unifSpec + (M × Commit →ₒ Chal))) σ hr M))    (qH : ℕ) :    ∃ reduction : Stmt → ProbComp Wit,      (Fork.advantage σ hr M nmaAdv qH *          (Fork.advantage σ hr M nmaAdv qH / (qH + 1 : ENNReal) -            challengeSpaceInv Chal)) ≤        Pr[= true | hardRelationExp hr reduction] := by  classical  refine ⟨nmaReduction σ hr M nmaAdv qH, ?_⟩  set acc : Stmt → ENNReal := fun pk =>    Pr[ fun x => (Fork.forkPoint (M := M) (Commit := Commit) (Resp := Resp)      (Chal := Chal) qH x).isSome | Fork.runTrace σ hr M nmaAdv pk] with hacc_def  have hAdv_eq_tsum :      Fork.advantage σ hr M nmaAdv qH =        ∑' pkw : Stmt × Wit, Pr[= pkw | hr.gen] * acc pkw.1 := by    simp only [Fork.advantage, Fork.exp, ← probEvent_eq_eq_probOutput,      probEvent_simulateQ_unifChalImpl, probEvent_bind_eq_tsum, bind_pure_comp,      probEvent_map, Function.comp_def, probEvent_liftComp, acc]  have hRHS_eq_tsum :      Pr[= true | hardRelationExp hr (nmaReduction σ hr M nmaAdv qH)] =        ∑' pkw : Stmt × Wit, Pr[= pkw | hr.gen] *          Pr[ fun w : Wit => rel pkw.1 w = true |            nmaReduction σ hr M nmaAdv qH pkw.1] := by    simp only [hardRelationExp, ← probEvent_eq_eq_probOutput, bind_pure_comp,      probEvent_bind_eq_tsum, probEvent_map, Function.comp_def]  -- The replay-forking bound feeds the per-`pk` witness-extraction bound.  have hPerPkFinal : ∀ pk : Stmt,      acc pk * (acc pk / (qH + 1 : ENNReal) - challengeSpaceInv Chal) ≤        Pr[ fun w : Wit => rel pk w = true |          nmaReduction σ hr M nmaAdv qH pk] := fun pk =>    (Fork.replayForkingBound (σ := σ) (hr := hr) (M := M) nmaAdv qH pk        (P_out := forkSupportInvariant σ M qH pk)        (hP := fun h => forkSupportInvariant_of_mem_replayFirstRun σ hr M nmaAdv qH pk h)        (hreach := Fork.runTrace_forkPoint_CfReachable          (σ := σ) (hr := hr) (M := M) nmaAdv qH pk)).trans      (perPk_extraction_bound σ hr M nmaAdv qH hss hss_nf pk)  rw [hAdv_eq_tsum, hRHS_eq_tsum]  exact OracleComp.EvalDist.marginalized_jensen_forking_bound (mx := hr.gen)    (acc := fun pkw => acc pkw.1)    (B := fun pkw => Pr[ fun w : Wit => rel pkw.1 w = true |      nmaReduction σ hr M nmaAdv qH pkw.1])    (q := (qH : ENNReal) + 1) (hinv := challengeSpaceInv Chal)    challengeSpaceInv_ne_top (fun _ => probEvent_le_one) (fun pkw => hPerPkFinal pkw.1)