If every term holds at most cap units, then n terms hold at most n times cap. Turn that around and the number of terms is at least the total divided by the cap. Sixty units at fifteen a term is four terms. At twelve it is five, at nine it is six, at six it is ten, and at three it is twenty. Each of those is a separate proved statement rather than a formula anyone has to trust, and the arithmetic is integer division, so the direction of rounding is decided rather than assumed.
Erika/Nursing.lean
Floor and ceiling are not the same advice.
Twenty-one units at fifteen a term is 1.4 terms. Floor says one. A student sits two. The corpus keeps these apart deliberately: the floor value is a valid lower bound, and the ceiling is the number of terms actually needed. Rounding the wrong way here tells a nursing applicant they finish a term earlier than they do, which is the kind of small error that costs somebody a year.
Erika/Schedule.lean
Order beats volume more often than people expect.
A plan respects prerequisites when every course lands strictly after everything it depends on. Follow a chain through such a plan and each step must go at least one term further out, so the i-th course of a chain is in term i or later. The bound falls out by induction and it does not care about unit loads at all. When the chain bound exceeds the volume bound, adding units per term changes nothing, and the only remedies are summer terms, testing out, or an articulated equivalent from somewhere else.
Course sequences change. The arithmetic does not.
Which courses chain, and what the cap is this year, come from the current catalog and a counselor. What the numbers do once you have them is settled here.
The previous eight-term schedule and its optimality badge were retired. Their course graph and units were not generated from a versioned official catalog, so a theorem about an assumed graph could not certify that plan.
What the theorem actually says
A conditional lower bound, not a planner
Prerequisite-chain term lower bound
Erika.Schedule.prereq_chain_forces_terms
{n k : ℕ} (s : TermPlan n) {prereqs : Fin n → Fin n → Prop} (hresp : s.respectsPrereqs prereqs) (chain : Fin (k + 1) → Fin n) (hchain : ∀ (i : ℕ) (hi : i < k), prereqs (chain ⟨i, by omega⟩) (chain ⟨i + 1, by omega⟩)) : ∀ (i : ℕ) (hi : i ≤ k), i ≤ s.assign (chain ⟨i, by omega⟩)
Order costs time independently of volume. In any plan that respects prerequisites, the i-th course of a chain lands in term i or later, so a four-course chemistry chain occupies four terms however light the load. Returns the term count implied by a course list's unit total and the separate floor implied by its longest chain.
The theorem does not discover COC prerequisites, generate a schedule, prove unit-cap compliance, or establish fastest graduation. Its sibling in the same file, completion_lower_bound at Erika/Schedule.lean:20, bounds terms by total units over cap, and combined_bound at Erika/Schedule.lean:102 joins the two. A future planner needs a dated catalog snapshot, official equivalency rules, validation by program staff, and a receipt binding the runtime graph to that snapshot.