D4.4b: one-step q-seed pump
ProvedFiniteMagmaE677.period_four_swapped_s_q_fixer_one_stepe677magmaperiod-fourrenewal
Write and let for an exact first-return cycle of length . Let a finite magma satisfy E677, with an exact first-return cycle at and the swapped-S cycle-renewal packet. Assume and . Put and .
There is a one-step packet retaining the renewal input and canonical q/s equations. It records freshness of both outside the six named points, , , , and , together with all five cycle-location alternatives:
- Both lie on , at distinct phases.
- lies on and starts a disjoint cycle.
- starts a new cycle and lies on .
- starts a new cycle and lies at a strictly positive phase of .
- starts a new cycle and starts a cycle disjoint from both .
Contact phases carry their exact equations and bounds; escaping seeds carry exact first-return data. This asserts one step, without an iteration or termination conclusion.
Preamble
import Definitions.Def_FiniteMagmaE677_sswap_renewal import Mathlib universe u open FiniteMagmaE677
Formal statement
theorem FiniteMagmaE677.period_four_swapped_s_q_fixer_one_step
{α : 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)
(input : SSwap.CycleRenewal op x c1 c2 c3 q s t first)
(q_eq : q = op c2 x) (s_eq : s = op c3 q) :
SSwap.Pump op x c1 c2 c3 q s t (op q (op q x)) (op q (op q (op q x))) first := by sorrySource
Adam McKenna, The Missing Pair (private repository), revision f9945b937be61f4ca48eb6cafdcfa07ba7a7f78c, lean/E677/Spine/Piece1D4SSwapQFixerPump.lean, line 87. The accepted proof on this platform is the public record.