Yoneda reflection for a finite mesh presentation

theorem MagnitudeConjecture.MeshCategory.RightMeshData.yoneda_reflected_relation {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hP : T.FiniteContravariantRepresentables) (z : { z : Q // z ∉ T.projective }) (x : Q) (h : T.incomingCoefficientFiniteModule hP ↑z ⟶ T.contravariantRepresentableFiniteModule hP x) (hh : CategoryTheory.CategoryStruct.comp (T.translationMapFinite hP z) h = 0) : let Y := CategoryTheory.linearYoneda k T.VertexCategory; ∑ a : IncomingArrow ↑z, CategoryTheory.CategoryStruct.comp (CategoryTheory.InducedCategory.homMk (T.incomingArrowHom ⟨T.tau z, (T.arrowEquiv z a.fst) a.snd⟩)) (Y.preimage (CategoryTheory.CategoryStruct.comp (T.incomingSummandInclusionFinite hP (↑z) a) h).hom.hom) = 0

Reflect the translation relation before specializing the mesh data to an algebra's standard form.