Case Study: Building a Provably Complete Stamp-Maker with Strong Induction

DataField.Dev

Case Study: Building a Provably Complete Stamp-Maker with Strong Induction

"It is not enough for code to work on the cases you tried; it must work on the cases you didn't."

Executive Summary

A shipping service needs to make up exact postage from a fixed set of stamp denominations. The product question sounds simple — "which amounts can we cover?" — but it hides a classic discrete-math result: the Frobenius / postage-stamp problem. In this build-focused case study you'll construct, from scratch, a small make_postage engine for 4- and 5-cent stamps, and — crucially — you'll build it hand in hand with a strong-induction proof that it succeeds for every amount from 12 cents upward. The proof is not an afterthought bolted onto finished code; it drives the construction, and in particular it tells you exactly how many base cases you must hard-check and why the recursive reduction is "subtract one stamp and recurse." This is the build counterpart to Case Study 1: there we certified an existing evaluator; here the theorem and the implementation grow together, and the proof is the design spec. The engine becomes the make_postage and recursive_seq pieces of the Toolkit's recurrences.py.

Skills applied

Turning a vague product requirement into a precise "for all $n \ge n_0$" statement.
Discovering the threshold $n_0$ empirically (computation) and then proving it (strong induction).
Counting base cases by the reach of the inductive step — and feeling why the count is what it is.
Building a constructive function whose recursion mirrors the proof's reduction.
Extending a proved result to new denominations and recognizing the general pattern (Frobenius).

Background

The scenario

The fulfillment team stocks only two stamp denominations: 4 cents and 5 cents. Orders need exact postage. A junior engineer ships this:

def make_postage_v0(n):
    """Try to make n cents from 4- and 5-cent stamps. (First attempt.)"""
    fours = n // 4
    if 4 * fours == n:
        return (fours, 0)
    return None

print(make_postage_v0(8), make_postage_v0(13))
# Expected output:
# (2, 0) None

It "works" — it makes $8 = 2 \times 4$. But it reports None for $13$, even though $13 = 4 + 4 + 5$ is obviously makeable. The bug is that v0 only ever tries zero 5-cent stamps. The deeper problem is that nobody on the team can answer the product manager's actual question: "For which amounts is exact postage even possible, and can we promise it always works above some threshold?" That is not a coding question you can settle by testing — it is a theorem, and the implementation should be built to match it.

💡 Intuition: With only 4s and 5s you can clearly make $4, 5, 8, 9, 10, 12, 13, \dots$ — but small amounts like $1, 2, 3, 6, 7, 11$ are impossible. Somewhere the impossibilities stop and every amount becomes makeable. Finding that "somewhere," and proving nothing breaks above it, is the whole job. This is the postage problem previewed in the chapter's Project Checkpoint.

Why this matters

"It works on the inputs I tried" is precisely the failure mode this book warns against (theme two and theme four). A stamp-maker that silently fails on some amount in production is a shipping outage. More broadly, the makeable-from-fixed-denominations question is the Frobenius coin problem, and it shows up in compilers (instruction selection), number theory, and operations research. Strong induction is the natural proof tool because the reduction "use one 4-cent stamp, then make $n - 4$" reaches back to a case that is four steps down — not the immediately previous one — which is the §7.1 cue for "this needs the strong hypothesis, and it needs several base cases."

🔗 Connection. The reduction-by-4 here is the same shape as the divide-and-conquer reductions of Chapter 18 and the power_fast reduction-by-half from Chapter 6's case study: the recursive call doesn't land on $n - 1$. Whenever it doesn't, reach for strong induction and count base cases by the jump.

Phase 1: Find the threshold empirically (compute first)

Before proving anything, look. We write a brute-force checker — try every count of 5-cent stamps and see if the remainder is divisible by 4 — and scan small amounts to find where impossibility ends:

def can_make(n):
    """True if n cents is exactly makeable from 4- and 5-cent stamps."""
    for fives in range(n // 5 + 1):
        if (n - 5 * fives) % 4 == 0:
            return True
    return False

print([n for n in range(0, 20) if not can_make(n)])   # the IMPOSSIBLE amounts
print([can_make(n) for n in range(12, 20)])           # 12..19, all makeable?
# Expected output:
# [1, 2, 3, 6, 7, 11]
# [True, True, True, True, True, True, True, True]

The impossible amounts are $\{1, 2, 3, 6, 7, 11\}$ — and the largest is 11. From $12$ onward, every amount we checked is makeable. That makes the conjecture sharp:

Conjecture. Every integer amount $n \ge 12$ is exactly makeable from 4-cent and 5-cent stamps, and $11$ is the largest amount that is not.

⚠️ Common Pitfall: mistaking the scan for the proof. The scan checked $12$ through $19$ — eight amounts. That is evidence, not a guarantee for the infinitely many amounts beyond $19$. The whole point of theme four: the computation found the threshold; only a strong-induction proof can promise it holds forever. Do not let eight Trues end the investigation.

🔄 Check Your Understanding The number $11$ is the largest impossible amount. Verify by hand that $11$ truly cannot be made, and that $12, 13, 14, 15$ each can.

Answer

$11$: zero 5s needs $11/4$ (no); one 5 leaves $6$, not a multiple of 4 (no); two 5s leave $1$ (no). So $11$ is impossible. $12 = 3\times4$; $13 = 2\times4 + 1\times5$; $14 = 1\times4 + 2\times5$; $15 = 3\times5$. All four are makeable — exactly the four consecutive successes the next phase needs.

Phase 2: Design the proof — and let it dictate the base cases

Here is the build discipline that this chapter is really about: we design the inductive step first, and the step tells us how many base cases the code must hard-code.

The natural reduction is: to make $n$, use one 4-cent stamp and then make $n - 4$. If we already know $n - 4$ is makeable, we slap on a 4-cent stamp and we're done. In symbols, the step proves $P(n)$ from $P(n - 4)$ — it reaches four cases back.

By the §7.1 rule ("the number of base cases equals how far back the step reaches"), a reduction by 4 requires four consecutive base cases. We choose the four smallest amounts in range: $12, 13, 14, 15$. Why exactly these four? Because the step, applied at $n = 16, 17, 18, 19, \dots$, reduces to $12, 13, 14, 15, \dots$ — so every amount $\ge 16$ bottoms out at one of the four base cases after finitely many subtractions of 4. If we checked only three (say $12, 13, 14$), the step at $n = 15$ would reduce to $P(11)$ — which is false — and the chain would never reach $15$ legitimately.

💡 Intuition: Picture four parallel ladders, one starting at each of $12, 13, 14, 15$. Adding a 4-cent stamp is climbing one rung. Every amount $\ge 12$ sits on exactly one ladder ($n \equiv 0, 1, 2, 3 \pmod 4$ shifted into range), and the four base cases are the four ladders' bottom rungs. Miss a bottom rung and one whole ladder is unsupported.

🚪 Threshold Concept. This is the single skill the chapter is built around: the structure of the recursive reduction dictates the number of base cases. Reduction by 1 → one base case (ordinary induction). Reduction by 4 → four base cases. Reduction to two predecessors (Fibonacci) → two. Once you internalize "count base cases by the jump," strong-induction proofs stop silently breaking.

🧩 Productive Struggle. Before Phase 3, predict: if the stamps were 4 and 6 cents instead of 4 and 5, would the reduction-by-4 step still work? (Try to make $13$ and $15$ from 4s and 6s.) Hold your answer for Discussion Question 4.

Phase 3: Build the constructive engine to match the proof

Now we build a function whose recursion is the proof's reduction. We want it to return the actual counts (fours, fives), not just a yes/no — a constructive proof yields a constructive algorithm. Two implementations, both worth seeing:

def make_postage(n):
    """Return (fours, fives) summing to n cents, or None if impossible.
    Provable by strong induction: succeeds for every n >= 12."""
    for fives in range(n // 5 + 1):
        rest = n - 5 * fives
        if rest % 4 == 0:
            return (rest // 4, fives)
    return None

print(make_postage(12), make_postage(23), make_postage(11))
# Expected output:
# (3, 0) (2, 3) None

This direct version searches over the number of 5-cent stamps. It returns None exactly on the six impossible amounts $\{1, 2, 3, 6, 7, 11\}$ and a valid pair everywhere else. For $23$: try $fives = 3$, $rest = 23 - 15 = 8 = 2\times4$, giving (2, 3) — i.e. $23 = 8 + 15$. ✓

The recursive version makes the proof's structure visible — it literally implements "add a 4-cent stamp to a solution for $n - 4$," bottoming out at the four base cases:

def make_postage_rec(n, _base={12: (3, 0), 13: (2, 1), 14: (1, 2), 15: (0, 3)}):
    """Strong-induction-shaped: reduce by one 4-cent stamp down to a base case."""
    if n in _base:                       # the FOUR hard-checked base cases
        return _base[n]
    if n < 12:
        return None                      # below threshold: may be impossible
    fours, fives = make_postage_rec(n - 4)   # strong hypothesis: n-4 is solved
    return (fours + 1, fives)             # ...add one 4-cent stamp

print(make_postage_rec(12), make_postage_rec(23), make_postage_rec(20))
# Expected output:
# (3, 0) (2, 3) (5, 0)

Hand-trace these — this is exactly the "never run code, derive by hand" discipline (theme four), and the trace doubles as a walk through the proof's reduction:

$12$ is a base case, returning (3, 0) directly — that is $12 = 3\times4$. ✓
$23$ is not a base case and $\ge 12$, so reduce by 4: $23 \to 19 \to 15$. Now $15$ is a base case, (0, 3). Climbing back up, each return adds one 4-cent stamp: $19 \to (1, 3)$, then $23 \to (2, 3)$ — that is $23 = 2\times4 + 3\times5 = 8 + 15$. ✓
$20$ reduces $20 \to 16 \to 12$; $12$ is the base case (3, 0); climbing up, $16 \to (4, 0)$ then $20 \to (5, 0)$ — that is $20 = 5\times4$. ✓

Notice the recursive version and the searching make_postage can return different but equally valid representations of the same amount (both happen to agree on these three). That ambiguity is harmless for the existence claim "$n$ is makeable"; Discussion Question 3 asks what it would take to pin down a single canonical answer. The reference implementation in code/exercise-solutions.py uses the searching make_postage, whose outputs are simplest to hand-verify; the recursive version is shown here to expose the proof's shape.

Phase 4: The proof (now the code's spec, made rigorous)

With the design fixed, the proof is short — it is the blueprint the code was built from.

The strategy first. Four base cases ($12$–$15$), one for each residue mod 4 shifted into range; then a step that makes $n$ by adding a 4-cent stamp to a solution for $n - 4$. The strong hypothesis supplies $P(n-4)$, which exists and is true precisely because $n - 4 \ge 12$ once $n \ge 16$.

Claim. For every integer $n \ge 12$, there exist non-negative integers $a, b$ with $n = 4a + 5b$.

Proof (strong induction on $n$). Let $P(n)$ be "$n = 4a + 5b$ for some integers $a, b \ge 0$."

Base cases ($n = 12, 13, 14, 15$). Exhibit a representation for each: $$12 = 4\cdot 3 + 5\cdot 0, \quad 13 = 4\cdot 2 + 5\cdot 1, \quad 14 = 4\cdot 1 + 5\cdot 2, \quad 15 = 4\cdot 0 + 5\cdot 3.$$ So $P(12), P(13), P(14), P(15)$ all hold.

Strong inductive step. Fix $k \ge 15$ and assume $P(12), P(13), \dots, P(k)$ all hold; we prove $P(k+1)$. Since $k + 1 \ge 16$, we have $(k + 1) - 4 = k - 3 \ge 12$, so $k - 3$ is one of the indices covered by the hypothesis, and $P(k-3)$ holds: write $k - 3 = 4a + 5b$ with $a, b \ge 0$. Then $$k + 1 = (k - 3) + 4 = (4a + 5b) + 4 = 4(a + 1) + 5b,$$ which is a representation of $k + 1$ with non-negative coefficients $a + 1$ and $b$. So $P(k+1)$ holds. By strong induction, $P(n)$ holds for all $n \ge 12$. $\blacksquare$

Two things to notice, both the heart of the chapter. First, the step used the hypothesis at $k - 3$, which is not the immediately preceding case $k$ — that is why ordinary induction would not serve. Second, the step is only valid once $k - 3 \ge 12$, i.e. $k + 1 \ge 16$; the four amounts $12, 13, 14, 15$ lie below where the step takes over and so had to be checked by hand. Four base cases, because the step reaches four back. That is the whole moral.

🐛 Find the Error. A teammate "simplifies" the proof to use only one base case, $n = 12$, claiming "the step covers everything else." Where does their argument fail, and on which amount does the gap show?

Answer

With only $P(12)$ proved, the step (reduce by 4) at $n = 13$ would need $P(9)$, at $n = 14$ would need $P(10)$, and at $n = 15$ would need $P(11)$ — none of which is established (and $P(11)$ is outright false, since $11$ is unmakeable). The chain reaches $16, 20, 24, \dots$ (the $n \equiv 0 \bmod 4$ ladder) but never $13, 14, 15$ or anything on their ladders. The gap shows immediately at $13$. You need all four bottom rungs.

Discussion Questions

The empirical scan (Phase 1) and the proof (Phase 4) play different roles. State precisely what the scan established and what the proof added — and why neither alone is sufficient for a production promise.
We chose to reduce by four (add a 4-cent stamp). Could the proof instead reduce by five (add a 5-cent stamp)? How many base cases would that version need, and which ones? Is one version "better"?
The recursive make_postage_rec and the searching make_postage can return different valid representations of the same amount. Is that a bug? What would it take to specify a canonical answer (e.g., the one using the fewest stamps), and would the proof change?
(From the Productive Struggle.) With 4- and 6-cent stamps, the reduce-by-4 step still works, but the set of makeable amounts is different — only even amounts are makeable at all. Explain why, using a divisibility/$\gcd$ argument, and state the new threshold above which every even amount is makeable.
The largest impossible amount for $\{4, 5\}$ is $11 = 4\cdot 5 - 4 - 5$. This is the Frobenius number $g(4, 5)$. Look up the formula $g(a, b) = ab - a - b$ for coprime $a, b$ and verify it for $\{3, 7\}$ and $\{5, 8\}$. Why does the formula require $a$ and $b$ to be coprime?

Your Turn: Extensions

Option A (generalize the denominations, build + prove). Write make_postage_general(n, coins) for an arbitrary tuple of coprime denominations, and for the specific case $\{3, 5\}$ prove by strong induction that every $n \ge 8$ is makeable. State the number of base cases (the step reduces by 3) and verify your threshold against the Frobenius formula.
Option B (the Toolkit's generic evaluator). Recall recursive_seq(step, base, n) from the Project Checkpoint. Use it to tabulate the "smallest number of stamps to make $n$" as a recurrence $m(n) = 1 + \min(m(n-4), m(n-5))$ for $n \ge 12$ with appropriate base values, and explain why this recurrence's step (a min over two predecessors) is itself strong-induction-shaped.
Option C (test then prove, your own denominations). Pick two coprime denominations of your choice, scan for the impossible amounts and the threshold in code, conjecture the threshold, then write the strong-induction proof with the correct number of base cases. Confirm the threshold matches $ab - a - b + 1$.

Key Takeaways

The proof is the design spec. We fixed the inductive step first; it dictated the reduction the code performs and the base cases it must hard-check. Build the proof and the program together.
Count base cases by the reach of the step. Reduce-by-4 ⟹ four base cases ($12, 13, 14, 15$); each covers one residue class mod 4. Three would leave a whole ladder (and the false $P(11)$) unsupported.
Computation finds the threshold; proof guarantees it. The scan revealed $11$ as the last impossible amount; only strong induction promises every amount from $12$ up works, forever.
A constructive proof yields a constructive algorithm. Because the step builds a representation of $n$ from one of $n - 4$, the function returns the actual stamp counts, not just a yes/no.
Hand-tracing is how you verify expected output. We derived every (fours, fives) by walking the recursion on paper — the same "never run code, reason it through" discipline this book insists on, and the trace doubled as a tour of the proof's reduction.