refactor(proofs): remove codegen fiction, name the scheduling-math source (#321 foundation)

[avrabe]

Foundation toward #321 — does NOT close it. REQ-PROOF-SCHED-SPEC-SOURCE-001 (verified). The real generator that closes #321 is filed as REQ-PROOF-SCHED-CODEGEN-001 (proposed); #321 stays OPEN.

What the investigation found

A reflection probe (lake env lean over the elaborated Exprs) established that true generation is blocked this cycle:

• ceilDiv/interference/rtaStep reflect cleanly (flat arithmetic Expr trees).
• totalInterference compiles to List.brecOn/List.below — not a naive Expr walk.
• the driver compute_response_time is a hand-written loop, not a syntactic image of iterN.

And critically: the existing Codegen.lean emits hardcoded Rust strings, so a byte-diff gate over it would only enforce .rs == Codegen-strings (both hand-written, neither read from the proofs) — theory↔code drift stays representable. That's generation cosplay; shipping it as #321 progress would be a #294/#331-class over-claim. Not done.

What this PR does (honest, verifiable)

1. Corrects a false verification claim (claim-verification skill). scheduling_verified.rs claimed "generated by lake exe codegen — DO NOT EDIT" while its own top lines documented a hand-edit (div_ceil) and the generator only ever emitted 5 of the 12 functions it ships. The header now states the truth: hand-written to mirror the Lean defs, bound to them by the named property tests (ceil_div_matches_lean_definition, compute_response_time_matches_lean_spec, the jittered/blocking spec tests) that run in the CI Test gate — the executed oracle for the Rust↔Lean correspondence.
2. Removes the footgun. Deletes proofs/Codegen.lean + its codegen lakefile exe. The documented lake exe codegen > scheduling_verified.rs would have silently deleted the 7 hand-added jittered/blocking/ISR functions.
3. Keeps RTACore.lean — the combinational defs as a mathlib-free named single source the future generator will consume; RTA.lean proves the theorems over it.
4. rivet: two REQs (foundation verified + generator proposed); fixes REQ-PROOF-SCHED-002's now-stale "existing RTA extraction" reference.

Verification

• scheduling_verified property tests: 15/15 (the Rust↔Lean binding oracle) — logic unchanged, header is doc-only.
• RTACore.lean builds mathlib-free locally (357ms). The full RTA.lean proof re-verify (theorems now typecheck against the relocated RTACore defs) is the CI lake build gate — the key thing to watch, since the def relocation is mechanical but only CI has mathlib.

Scope honesty

This removes a live footgun and a false "generated" claim, and names the spec source. It does not make the Rust generated from the proofs — #321's actual ask — which stays open as REQ-PROOF-SCHED-CODEGEN-001.

🤖 Generated with Claude Code

[github-actions]

Rivet verification gate

✅ 20/20 passed

	count
Passed	20
Failed	0
Skipped (no steps)	0

Filter: (and (= type "feature") (or (has-tag "v093") (has-tag "v0100")))

Failed artifacts

(none)

_{Updated automatically by tools/post_verification_comment.py. Source of truth: artifacts/verification.yaml.}

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!