The first is volume. Sixty units at fifteen a term is four terms, and no amount of planning moves that: it is the pigeonhole principle, since you cannot fit more than cap times terms of anything into terms of size cap. The second is order. Chemistry 1A comes before 1B, which comes before Organic 1, which comes before Organic 2, and a chain of four courses occupies four separate terms even if all four together are a light load. These two bounds are independent. A student can be well under the unit cap and still be held for four terms by a single chain, and the advisor who only counts units will not see it coming.
Erika/Nursing.lean
Six areas, twenty-one units, two terms.
The nursing prerequisite set has exactly six areas: English, anatomy and physiology, microbiology, mathematics, psychology and communications. Their units add to twenty-one, from three each for the smaller areas up to five for anatomy and physiology. At a full-time fifteen units a term that is two terms. At twelve units it is still two. At three units a term it is seven. Those are ceiling divisions, proved by decide rather than worked out on a napkin, which matters because the floor and the ceiling disagree here and only one of them is the number of terms a student actually sits.
Erika/Units.lean
Quarter students are not imagining it.
A quarter unit is two thirds of a semester unit. Five quarter units of anatomy and physiology arrive as ten thirds of a semester unit, which is 3.33 and change, and a five-unit requirement is not met. That is not an unlucky rounding, it is the conversion working as designed, and it is provable in general: for any positive number of quarter units the semester figure is strictly smaller. Doing the arithmetic in exact rationals rather than floating point means the round trip back to quarter units returns the original number exactly, so a converted transcript can be checked rather than trusted.
Erika/GPA.lean · Erika/ScienceGPA.lean
Straight Bs clear the bar, and that is a theorem.
A grade point average is quality points over units, which means a single heavy course can move it more than two light ones. The corpus proves the average is bounded by the largest grade in the list, that it never goes negative, and the fact a student most wants to hear: if every prerequisite grade is a B or better, the prerequisite average is at least 2.5. Science GPA is computed the same way over a filtered list, because programs that separate science coursework are asking a different question about the same transcript.
Erika/Shortfall.lean · Erika/Equivalency.lean
What is missing, and the smallest thing that fixes it.
A shortfall is what a requirement asks minus what a student has, floored at zero. The corpus proves the shortfall is zero exactly when the requirement is met, that adding coursework never increases it, and that there is a minimal amount of remediation which closes it, so nobody is advised to take more than they need. Articulation is a map between course codes, and broadening the map can only help: a wider articulation satisfies at least as much as a narrower one, never less.
Formal statements
theorem
Erika.Schedule.completion_lower_bound
For cap > 0, if total ≤ numTerms * cap then total / cap ≤ numTerms. Volume alone sets a floor on terms.
Erika/Schedule.lean:20
theorem
Erika.Schedule.prereq_chain_forces_terms
In a plan respecting prerequisites, the i-th course of a chain sits in term i or later. A four-course chain needs four terms.
Erika/Schedule.lean:72
theorem
Erika.Nursing.nursing_total_units
3 + 5 + 4 + 3 + 3 + 3 = 21. The six prerequisite areas total twenty-one units.
Erika/Nursing.lean:60
theorem
Erika.Nursing.nursing_fulltime_terms
(21 + 15 - 1) / 15 = 2. At fifteen units a term the prerequisites take two terms.
Erika/Nursing.lean:69
theorem
Erika.Units.five_quarter_is_ten_thirds
Five quarter units convert to exactly 10/3 semester units. A five-unit requirement is not met.
Erika/Units.lean:80
theorem
Erika.Nursing.quarter_always_fewer
For n > 0, quarterToSemester n < n. Converting from quarters always yields strictly fewer units.
Erika/Nursing.lean:111
theorem
Erika.Nursing.b_grades_meet_threshold
If every prerequisite grade is at least 3.0, the prerequisite GPA is at least 2.5.
Erika/Nursing.lean:120
theorem
Erika.DegreePlan.ge_area_count
Fintype.card GEArea = 7. The general-education pattern has seven areas.
Erika/DegreePlan.lean:36
Two questions students ask constantly.
How long is this going to take, and do my old units count. Both have exact answers once the rule is fixed, and the arithmetic is the part that should never be in doubt.
Three receipts hold this site up. Everything else is the college’s word.
A conjunction identity for an admission record, a lower bound for prerequisite chains, and an exact rational unit conversion. Each is pinned to a file, a line, and a commit. Transcript review, degree planning, equivalency, and admission remain with the college.
Three conditions gate a nursing prerequisite record: areas covered, GPA clear, units sufficient. All three or none, with no partial credit and no compensating between them. Returns which of the three a course list meets, the computed GPA, and the exact shortfall in each area that misses. Which conditions are in force this year is the college's answer.
{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.
A quarter unit is two thirds of a semester unit. Five quarter units of anatomy and physiology come to exactly ten thirds, which does not meet a five-unit requirement. Computed in exact rationals, so the round trip back to quarter units is the identity rather than nearly the identity, and boundary cases resolve the same way twice.