We isolate and formalize a d=6 exact-base branch in finite E677 magmas. In the branch considered here, a distinguished element x has left orbit c₀ = x, c₁ = x ◇ x, c₂ = x ◇ c₁,. . . , c₅ = x ◇ c₄, together with an outsider element A satisfying the exact-base rows A ◇ A = c₁, A ◇ x = c₃, c₃ ◇ c₃ = c₁. Under the d=6 gap-1 context hypotheses, these rows force c₄ ◇ x = x, and therefore ( (x ◇ x) ◇ x) ◇ x = x. The Lean formalization exposes this result through D6ExactBasePacket. fixer in lean/E677/D6Publication. lean. The theorem is independent of the large gap-1 dispatcher and verifies with only standard Lean axioms (propext, Classical. choice, Quot. sound).
Adam McKenna (Fri,) studied this question.