Heisenberg naturality for the r_R pairing (Lemma 5.6), and the traced-row re-export

The dévissage χ-layer needs two traced ingredients over the Roe complex:

• the traced Stokes rows prop_5_8_left_R/prop_5_8_right_R (⟦lem:stokes⟧) — the chain identities B^R(d⁰a, y) = ⟨a, L^{A^∨}(y)⟩ making the χ-maps well-defined. These are ticket R25's (GQ2/Roe/TrivialSelfDual.lean), landed with trivialSelfDual_R; this file re-exports them (public import), never re-proving them;
• Lemma 5.6 (⟦lem-heisnatural⟧), the coefficient-naturality square of the traced pairing B^R_{A'}(f∗x, y') = B^R_A(x, f^∨ y'), needed by the χ¹/δ-square rungs. R20 tagged lemma_5_6 pure-(A); its wild half (Marking.map_wildValue) is in fact word-coupled, but the port is verbatim — the only change is the final simp swapping mixedB/Marking.map_wildValue for mixedB_R/Marking.map_wildValueR. R25 does not need it (the trivial module has no coefficient maps), so R26a provides it here (mechanical clone, docs/orchestration/roe-r20-recon.md).

theorem GQ2.FoxH.lemma_5_6_R {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] {A' : Type u_3} [AddCommGroup A'] [DistribMulAction C A'] [Finite A] [Finite A'] [Finite C] (f : A →+ A') (hf : ∀ (g : C) (a : A), f (g • a) = g • f a) (t : Marking C) (x : Fin 4 → A) (y' : Fin 4 → ElemDual A') : mixedB_R t (fun (i : Fin 4) => f (x i)) y' = mixedB_R t x fun (i : Fin 4) => AddMonoidHom.comp (y' i) f

Lemma 5.6 (strict coefficient naturality) for the Roe pairing (R-clone of lemma_5_6, GQ2/FoxHeisenberg/Traced.lean): B^R_{A'}(f∗x, y') = B^R_A(x, f^∨ y'). Verbatim port — only the final simp swaps mixedB/Marking.map_wildValue for mixedB_R/Marking.map_wildValueR.