Formal: Python/native classifier accuracy — both paths, vs CPython signal semantics

[emeryberger]

Closes the classifier-accuracy gap (HANDOFF §7 step 5) and adds the per-thread comparison. sorry-free, standard axioms only; full lake build green (8576 jobs); 17 modules / 142 theorems.

Accuracy can't be a bare theorem — which branch is right depends on where the program truly was when the timer fired, observable only through CPython's signal-delivery semantics. So this module makes that an explicit hypothesis and proves exact correctness relative to it.

The hypothesis — SigDeliverySound

CPython delivers a signal only at a bytecode boundary, so a timer firing inside a C call is deferred until the call returns, leaving f_lasti at the CALL opcode. Hence atCall = true ↔ truly in a C call. A CPython-runtime + synchronous-stamping property — stated, not proved. It is the honest residual.

Theorems

• worker_classifier_correct — the worker-thread bytecode classifier (_update_thread_stats, :458) charges native exactly the in-call samples under the hypothesis. Exact, not approximate.
• main_branchA_correct — the main-thread branch A (:256-275) is exact too.
• main_worker_agree / main_worker_both_exact — the comparison you asked for: in the shared regime (use_call_attribution true), the two paths make byte-for-byte the same Python/native decision, so one correctness proof covers both call sites.
• deferral_route_iff + deferral_formula_exact / deferral_formula_zero_when_no_excess — the paths diverge exactly in virtual-time, non-thread-sampled mode, where only the main thread has a virtual timer to measure deferral; that route is exact when native time shows up as timer-deferral (and the code's documented blind spot otherwise).
• misclassified_when_unsound / missed_when_unsound — if the hypothesis fails, the two-sided error is pinned down (false positive → native charged for Python; false negative → the reverse), quantifying what SigDeliverySound buys.

Docs

STATUS.md (classifier accuracy row ⚠️→✅-conditional; SigDeliverySound as the residual ⚠️), README §17 + roundup + boundary, HANDOFF module table + step 5 updated.

Formal-only; no production code touched.