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 the executable maximum-subarray and Strassen runtime proofs.

• Section 4.1 - The maximum-subarray problem: proved for functional correctness and the executable abstract control-step runtime. 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 executable midpoint layer uses maxPrefixLinear_result_correct, maxSuffixLinear_result_correct, and maxCrossingSubarrayLinear_result_correct to avoid exhaustive search at recursive nodes. maxSubarrayDivideCosted_result erases the attached cost, maxSubarrayDivideCosted_correct proves the returned candidate, the costed prefix/suffix/crossing executions prove their exact linear scan counts, and maxSubarrayDivideCosted_cost_eq plus maxSubarrayDivideCost_unfold connect the measured run to its actual mixed floor/ceiling recurrence. Finally, maxSubarrayDivideCost_isBigTheta_nlogn proves the all-input Theta(n log n) bound. The remaining refinement target is a lower-level list-allocation/integer-operation/RAM cost model.

• Section 4.2 - Strassen's algorithm for matrix multiplication: proved for 2 by 2 block algebra, the recursive algorithm, and runtime. The file proves CLRS.Chapter04.strassen2x2_correct: Strassen's seven products reconstruct ordinary 2 by 2 block matrix multiplication over an arbitrary ring. It then packages this into the recursive algorithm CLRS.Chapter04.strassenRec on depth-indexed power-of-two squares CLRS.Chapter04.SqMat, with a scalar base case, and proves CLRS.Chapter04.strassenRec_correct that it computes the true matrix product at every depth. CLRS.Chapter04.strassenRec_padOne shows that zero-padding an input into the next power-of-two block preserves the top-left product. Finally CLRS.Chapter04.strassen_runtime_bigTheta proves the CLRS runtime: the recurrence T(n) = 7 T(⌊n/2⌋) + n² is Θ(n^(log₂ 7)), discharged through the Chapter 4 Master-theorem case-1 wrapper.

• 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, plus a polylog case-2 extension (CLRS.Chapter04.master_case2_polylog_forcing): polynomial normalized forcing c·j^k ≤ forcing ≤ C·j^k gives T(b^i) = Θ((i+1)^(k+1)·a^i), i.e. the standard f(n) = Θ(n^(log_b a)·log^k n) textbook case.

• 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 (including the polylog criticalPowerLogPolylogScale) 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 case-3 regularity bridge connects the discrete tail-dominated scale to the textbook forcing function. The remaining chapter work is lower-level representation and RAM refinement, not recursive Strassen, maximum-subarray algorithm-level runtime, or a missing Master case.