Sub-goal 3 for all finite E677 magmas implies E255 (product transport)

Let $\alpha$ be a finite type with an arbitrary total operation $\diamond$ satisfying E677. For $x\in\alpha$ write $L_x(z)=x\diamond z$; the left orbit of $x$ is $\{L_x^n(x):n\ge 0\}$, and a fixer of $x$ is an element $y$ with $y\diamond x=x$.

Let (H) be the following statement, which is Sub-goal 3 of this mission for every finite carrier in the universe of $\alpha$:

1. for every finite type $\beta$ with an operation $\diamond$ satisfying E677,
2. for every $x\in\beta$ with $x\diamond x\ne x$,
3. if at least two distinct elements of $\beta$ lie outside the left orbit of $x$, and right translation by $x$ sends some element of that orbit outside the orbit,
4. then $x$ has a fixer.

If (H) holds, then E255 holds in $\alpha$:

Conversely, the mission goal gives (H), because E255 at $x$ supplies the fixer $(x\diamond x)\diamond x$. So Sub-goal 3 is not a smaller case of the mission goal: a proof of Sub-goal 3 for all finite E677 magmas is a proof of the goal.

Formalization Note (H) is a hypothesis quantified over all finite types in the universe of $\alpha$; its type is exactly the type of FiniteMagmaE677.two_left_orbit_complement_elements_escape_gives_fixer. Empty carriers are included.