siddhartha-gadgil/leanaide/bounding-extremal

Skill: Bounding, Monotonicity, and Extremal Objects

Pre-condition: Apply this skill when the proof is driven by inequalities, monotone sequences, squeeze arguments, maxima/minima, shortest or longest objects, or optimal choices.

Goal: Control the target by ordered comparison or choose an extremal object and show it must satisfy the desired property.

Instructions:

1. Identify the Order: Specify the partial order, metric size, degree, cardinality, norm, or energy being compared.
2. Bounding Route: Find lower and upper bounds, comparison objects, or a squeeze configuration.
3. Monotonicity Route: Prove the relevant function or sequence is increasing/decreasing and combine with boundedness or endpoint values.
4. Extremal Route: Choose a maximal or minimal object and prove failure of the target would allow an improvement.
5. Close the Argument: Translate the comparison or extremality contradiction into the desired statement.

Common Failure Modes:

• Assuming an extremum exists without compactness, finiteness, completeness, or Zorn-type justification.
• Missing strictness in an improvement argument.
• Using bounds that are too weak to force the target.