Chapter 4. Divide-and-Conquer

Chapter 4 has several good Lean targets. The current first pass contains both an algorithmic specification for the maximum-subarray problem and the recurrence proof infrastructure used by later divide-and-conquer analyses. Sections 4.3 and 4.4 provide the proof-method infrastructure used by the Master-method file and by future divide-and-conquer runtime proofs.

• Section 4.1 - The maximum-subarray problem: proved for the current functional correctness model. The file proves that the candidate enumerator contains exactly the nonempty contiguous subarrays, and that maxSubarray returns a candidate with maximum sum. It also proves that maxCrossingSubarray returns a maximum-sum candidate among all candidates crossing a split. Finally, subarray_append_left_or_right_or_crossing and subarray_append_optimal_of_cases provide the proof interface for the recursive combine step, and maxSubarrayDivideStep_correct proves the executable combine step itself. The recursive layer is captured by maxSubarrayDivideTree_correct for explicit split trees and maxSubarrayDivideFuel_correct for a fuelled midpoint splitter. The remaining refinement target is runtime/RAM-cost analysis.

• Section 4.2 - Strassen's algorithm for matrix multiplication: proved for 2 by 2 block algebra. The file proves CLRS.Chapter04.strassen2x2_correct: Strassen's seven products reconstruct ordinary 2 by 2 block matrix multiplication over an arbitrary ring.

• Section 4.3 - The substitution method: proved for one-step recurrence bounds. The file proves upper-bound, lower-bound, sandwich, linear, and geometric substitution templates.

• Section 4.4 - The recursion-tree method: proved for additive finite level expansions. The file proves exact unrolling into level-cost sums and envelope bounds for the resulting finite sums.

• Section 4.5 - The master method: proved for exact-power recurrences. The file proves the normalized recurrence expansion and three Master-style exact-power criteria for bounded, constant, and tail-dominated normalized forcing.

• Section 4.6 - Proof of the master theorem: partial. The file proves floor/ceiling all-input recurrence interfaces, extracts exact-power recurrences from those models, and proves a compiler-clean transfer bridge from exact-power O, Ω, and Θ bounds to all natural inputs under monotone cost and explicit power-sandwich hypotheses. It also proves the adjacent-power Nat.log interval and a direct allInput_bigTheta_of_powerStep theorem that discharges those sandwich hypotheses from monotone comparison scales with eventual one-step control. The discrete criticalPowerScale and criticalPowerLogScale and tailDominatedScale wrappers now turn exact-power T(b^i) = Θ(a^i), T(b^i) = Θ((i+1)a^i), and tail-dominated bounds into all-input bounds, and Section 4.6 packages the floor/ceiling recurrence forms of exact-power Master cases 1, 2, and 3 for these discrete scales. It also proves the natural-exponent comparison layer for a = b^p, exposing case-1 results as Θ(n^p) and case-2 results as Θ((⌊log_b n⌋+1)n^p). A real-log bridge CLRS.­Chapter04.­criticalPowerScale_isBigTheta_realLogScale now connects the discrete scale a^(⌊log_b n⌋) to the textbook scale n^(log_b a) for all a ≥ 1 and b > 1, and the named exact/floor/ceiling case-1 wrappers now expose CLRS-facing Θ(n^(log_b a)) bounds directly. A second bridge proves the discrete case-2 scale is Θ(n^(log_b a) log n), and the named exact/floor/ ceiling case-2 wrappers expose that textbook scale directly. The remaining Master gap is a textbook-facing case-3 comparison scale.