Coordinate Wise Special Sound of mk Witness

theorem coordinateWiseSpecialSound_of_mkWitness    (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))    (V : Verifier oSpec StmtIn (StmtIn × CarrierCom × (Fin (2 ^ r) → C)) (pSpec CarrierCom C r))    (hpure : ∀ s tr, V.verify s tr = pure (s, tr.messages ⟨0, rfl⟩, tr.challenges ⟨1, rfl⟩))    (relIn : Set (StmtIn × WitIn))    (relOut : Set ((StmtIn × CarrierCom × (Fin (2 ^ r) → C)) × WitOut))    (mkWitness : StmtIn → CarrierCom → (Fin (2 ^ r + 1) → (Fin (2 ^ r) → C)) →      (Fin (2 ^ r + 1) → WitOut) → WitIn)    (hmk : ∀ stmtIn v (fam : Fin (2 ^ r + 1) → (Fin (2 ^ r) → C)) (resp : Fin (2 ^ r + 1) → WitOut),      (∀ j, ((stmtIn, v, fam j), resp j) ∈ relOut) →      (∃ e, StarAt fam e) →      (stmtIn, mkWitness stmtIn v fam resp) ∈ relIn) :    V.coordinateWiseSpecialSound init impl      (foldStructure (CarrierCom := CarrierCom) (C := C) (r := r)) relIn relOut := by  classical  refine ⟨treeExtractor relOut mkWitness, ?_⟩  intro stmtIn tree hStruct hAcc  obtain ⟨v, challenges, rfl⟩ := tree_shape tree  have harity := (foldStructure_arity (CarrierCom := CarrierCom) (C := C) (r := r)).symm  -- each branch's guard fires: per-branch membership in `relOut.language`  have hmem : ∀ j : Fin (2 ^ r + 1),      ∃ w, ((stmtIn, v, challenges (Fin.cast harity j)), w) ∈ relOut := by    intro j    have h := branch_relOut_language init impl V hpure relOut stmtIn v challenges hAcc      (Fin.cast harity j)    exact (Set.mem_language_iff relOut _).1 h  -- the sibling family is special sound, hence has a star center  have hfam := (nodeOk_iff_family challenges).1 hStruct.1  have hstar : ∃ e, StarAt      (fun j : Fin (2 ^ r + 1) => challenges (Fin.cast harity j)) e :=    exists_starAt (le_refl 2) (by omega) _ hfam  -- each chosen response satisfies the relation (the extractor's guards fire)  have hbranch : ∀ j : Fin (2 ^ r + 1),      ((stmtIn, v, challenges (Fin.cast harity j)),        if h : ∃ w, ((stmtIn, v, challenges (Fin.cast harity j)), w) ∈ relOut          then h.choose else Classical.ofNonempty) ∈ relOut := by    intro j    rw [dif_pos (hmem j)]    exact (hmem j).choose_spec  -- the extractor computes definitionally on the recovered star tree; `exact` closes by defeq  exact hmk stmtIn v _ _ hbranch hstar