D4.4c: q-square refinement
ProvedFiniteMagmaE677.period_four_swapped_s_q_square_refinementWrite and let for an exact first-return cycle of length . Let a finite magma satisfy E677 and carry the swapped-S one-step packet with and . Put .
Then is outside the six named points, , , and . Moreover, the full five-way one-step classification admits the following refinement, preserving each original packet and branch payload. If both lie on , either occupies a third distinct phase there with the oriented phase-product identity, or starts a disjoint cycle. If starts a new cycle and lies on or , then lies on , lies on , or starts a cycle disjoint from both. Every contact keeps the identity in its corresponding ordered phase form; phases on are strictly positive, and same-cycle phases of are distinct. The two branches in which escapes retain their original full payloads.
The conclusion supplies both the q-square seed facts and this complete refined outcome. It does not establish recursive renewal or a fixer at .
import Definitions.Def_FiniteMagmaE677_sswap_renewal import Mathlib universe u open FiniteMagmaE677
theorem FiniteMagmaE677.period_four_swapped_s_q_square_refinement
{α : Type u} [Fintype α] (op : α → α → α) (h : FiniteMagmaE677.E677 op)
(x c1 c2 c3 q s t : α)
(first : FirstReturn.D4FirstReturn op x c1 c2 c3 t 0)
(pump : SSwap.Pump op x c1 c2 c3 q s t
(op q (op q x)) (op q (op q (op q x))) first) :
SSwap.QSquareSeed op x c1 c2 c3 q s (op q (op q x)) (op q (op q (op q x))) ∧
SSwap.QSquareOutcome op x c1 c2 c3 q s t
(op q (op q x)) (op q (op q (op q x))) first := by sorry