One witness, both engines — RelatedBinOp ⇒ RArrow

The two relatedness engines register a realized binary operation under two different keys: the Related engine takes a RelatedBinOp enc op bop square (Base/Related.lean, consumed by rcongr/param_cc/param_solve), the Param engine takes a curried RArrow witness (Translate/ParamTranslate.lean, consumed by the term translator ⟦·⟧ and registered with @[param]). They carry the same content: over the encoding graph R a b := enc a = b, the square enc (op a b) = bop (enc a) (enc b) unfolds to ∀ a a', R a a' → ∀ b b', R b b' → R (op a b) (bop a' b'), which is exactly RArrow R (RArrow R R) op bop.

This file makes that a single source of truth: register the RelatedBinOp square once, and derive the Param-engine witness from it with no second proof. It is the RelatedBinOp companion of ParamNormCast.paramWitOfCastHom (which does the same for a @[norm_cast] move lemma), closing the loop so a realized operation is proved once and consumed by every tactic surface.

@[reducible, inline]

abbrev Transfer.Param.encRel {A α : Type} (enc : A → α) : A → α → Prop

The encoding graph of enc as a bare-Prop relation.

Equations

• Transfer.Param.encRel enc a b = (enc a = b)

theorem Transfer.Param.paramWitnessOfRelatedBinOp {A α : Type} (enc : A → α) (op : A → A → A) (bop : α → α → α) [h : RelatedBinOp enc op bop] : RArrow (encRel enc) (RArrow (encRel enc) (encRel enc)) op bop

Single source of truth. A RelatedBinOp enc op bop square is the curried Param binary witness RArrow (encRel enc) (RArrow (encRel enc) (encRel enc)) op bop. Register the square once (for the Related engine); this derives the Param-engine witness — no re-proof. The @[param]-registered form is a one-line := paramWitnessOfRelatedBinOp enc op bop.