Tensions in Practice: Case checking in tension with a shared explanation¶
A small exact divisibility proof
For every odd integer n, n² − 1 is divisible by 8. One proof checks all four possible odd remainders after division by 8. Another writes n = 2k + 1 and notices that k and k + 1 are adjacent, so one is even. Both establish the same claim. The comparison separates a complete case certificate from a compact reason shared by every case.
Check local obligations
Reduce the claim to an explicitly exhaustive set of manageable cases.
Expose the common reason
Show one relationship that explains why all cases work.
Why these aims pull against each other
Case splitting can make checking routine while expanding bookkeeping and hiding a unifying relation; a common argument needs a suitable insight.
Choose an arrangement to see what changes and what remains difficult.
Arrows express the declared relations, not measured effect sizes. Examples and quantities are illustrative.
What this choice protects
What it costs
When it fits
Compare the arrangements
Check all odd remainders
Reduce the claim to remainders 1, 3, 5 and 7 and check each.
- What it protects
- The finite obligations and their arithmetic are explicit.
- What it costs
- Coverage and the reduction to remainders must also be proved; checking examples alone would not suffice.
- When it fits
- The case set is warranted exhaustive and checking its branches is manageable.
Illustration note: The paired boxes save space but still display all four remainders and their corresponding values.
Use adjacent integers
Expand the square of 2k + 1 and use the even factor in k(k + 1).
- What it protects
- The same reason handles every odd integer at once.
- What it costs
- Finding and understanding the useful factorization takes algebraic insight.
- When it fits
- The audience can follow the factorization and the adjacent-integer argument.
Illustration note: This is an alternative proof, not a claim that exhaustive cases are inferior or incorrect.
What this illustration does—and does not—establish
The source supplies the stated tension; the selected arrangements are bounded editorial illustrations. Costs and conditions remain part of the comparison.
- The variable n ranges over all odd integers, not only 1, 3, 5 and 7.
- A multiple of 8 has an integer quotient on division by 8; no empirical sample is involved.
- The visual does not replace the coverage and algebra written in the description.
Source entries
Proof by Cases
This source passage supplies the contextual tension. The concrete arrangements and schematic examples are editorial illustrations, not measured findings.
Mechanical Checking versus Explanatory Insight
T2 — Mechanical Checking versus Explanatory Insight. A computer can verify thousands of branches while leaving the reason for the common conclusion hard to see. Diagnostic: Distinguish the correctness certificate from the higher-level explanation or invariant.
The source operation
Proof by cases converts a global claim into local obligations. A declared universe is divided into case conditions whose union covers every admissible possibility; the same proposition is then derived under each condition. Once those conditional derivations and the coverage claim are valid, the temporary case assumptions can be discharged and the proposition follows over the entire universe.