Interval scheduling with commitment: hardness, selection and compact attack certificates

We study interval scheduling with commitment: cancellations may affect the entire labelled input, recovery adds at most p unused nonfailed requests, and every surviving initial commitment must remain. We consolidate strong NP-completeness for two cancellations and every fixed positive p with exact unit-weight selection for an input cancellation budget and two additions, together with complementary tractable regimes. For unit weights and both budgets supplied as input, we give a polynomial supplied-schedule evaluator and an exact polynomial-size mixed-integer formulation based on a selection-independent attack-certificate graph. The formulation retains one common initial selection; it does not establish polynomial-time integer selection or LP integrality. Established interval packing, interdiction, dynamic-programming and network-potential ingredients are credited, and the relation to general binary bilevel formulations is made explicit. Bounded exhaustive comparisons support implementation correctness on the recorded finite cases, without a practical-speed claim. Formal verification covers only the explicitly listed Lean targets under pinned definitions, axioms and checker trust; unresolved obligations are identified separately. This research preprint has not received external human peer review. Substantial use of AI in derivation, drafting and internal review is disclosed. Bibliographic corpus and version gaps remain, and exhaustive originality is not certified. Version 7.0 consolidates the intervening local drafts; versions 2–6 were not separate public deposits. The files include the 57-page manuscript, matching LaTeX sources, recorded numerical evidence, frozen accepted Lean sources and replay reports, a SHA-256 manifest and reproduction instructions. Formal-verification cutoff: 1 November 2026 00:06:21 UTC (31 October in Chile). The accepted Lean 4.35.0 dependency batch contains 13 modules and 92 targets, including the two inherited coverage targets. The complete functional evaluator and complexity bounds remain pending as formal certificates; the selection algorithms, hardness reduction and compact MILP are outside this accepted scope. Comments and corrections are welcome.