Structural packet forced by a cross-boundary collision with one element outside the left orbit

Proved supporting lemma for the one-element left-orbit-complement branch of the finite E677 → E255 problem.

Let $(\alpha,\diamond)$ be a finite magma satisfying E677: for all $p,q\in\alpha$,

Fix $x\in\alpha$ and let $O_x=\{L_x^n(x):n\ge 0\}$ be its orbit under the left translation $L_x(z)=x\diamond z$. Assume:

1. $x$ has no fixer, that is, no $y$ satisfies $y\diamond x=x$;
2. exactly one element $A$ lies outside $O_x$;
3. some $c\in O_x$ collides with $A$ under right translation by $x$: $c\diamond x=A\diamond x$.

Write $d=A\diamond x$, $b=A\diamond A$, $u=c\diamond d$, and $v=A\diamond u$. The lemma asserts the following structural packet.

• $d\in O_x$, $d\ne x$, $d\ne A$.
• $b\in O_x$, $b\ne x$, $b\ne d$, $b\ne A$.
• The outsider is fixed by $L_x$ and satisfies $A\diamond d=A$ and $b\diamond A=x$:

• The collision transports along the backward recurrence: $u\diamond c=b$.
• $u\in O_x$ and $u\ne d$.
• $v\in O_x$, $v\ne A$, $v\ne b$.
• If $v=d$, then $u=x$, and the two predecessor identities

hold; together with $c\diamond x=d$ (the collision) and $c\diamond d=u=x$, this says $L_c$ exchanges $x$ and $d$.

The lemma isolates the points and separations that any argument about the cross-boundary collision must handle, and it splits the situation into the branch $v=d$ and the branch $v\ne d$. It does not conclude the open successor-propagation statement $(x\diamond c)\diamond x=A\diamond x$, and it does not produce a fixer. Its conclusions are sound constraints for finite-model or SAT searches inside this branch.

Formalization Note Orbit membership is the predicate InLeftOrbit, the no-fixer hypothesis is the negation of HasFixerAt, and uniqueness of the outsider is stated as: every element outside the orbit equals $A$. The derived points are written out as terms rather than introduced by let binders.