Imports
import CLRSLean.FourthEdition.Chapter_26.Section_26_1_Multithreading_Model
import CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.S1_CostModel
import CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.S2_Recurrences
import CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.S3_AllInputBounds
import CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMatrix.Definitions
import CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMatrix.Correctness
import CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMatrix.Costs
import CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMerge
import CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMergeSort
import CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelStrassen
26.2–26.3. Multithreaded Algorithms (Historical 2_4 Compatibility)
The historical 2_4 module name is retained for compatibility. Its main
text now covers §§26.2–26.3: parallel-recurrence definitions and all-input
analysis for P-MATMUL, P-MERGE, and P-MERGE-SORT. The historical parallel
Strassen names are imported separately from an explicitly labeled Chapter 26
extension.
Main results
The imported modules provide an executable value/work/span layer for attaching
costs directly to algorithm results, executable and proved-correct P-ADD and
P-MATMUL algorithms, exact equalities between their recorded costs and their
execution recurrences, monotonicity and adjacent-power sandwiches for all four
matrix costs, power-of-two solutions, and all-input Theta results for
P-ADD and executable P-MATMUL. The earlier idealized P-MATMUL recurrence
retains its all-input upper bounds. The imports also provide monotonicity,
adjacent-power sandwiches, and all-input Theta results for P-MERGE and
P-MERGE-SORT. The compatibility extension retains the corresponding Strassen
recurrence results without presenting them as Chapter 26 main text. The
executable binary lower bound used by P-MERGE additionally has a complete
duplicate-sensitive partition theorem and logarithmic work/span bounds.
CLRS.Chapter27.MergeSplit and
CLRS.Chapter27.pMerge implement the actual midpoint/binary-search
P-MERGE control structure, and CLRS.Chapter27.pMerge_correct proves its
sortedness, permutation, and exact-length specification. The pointwise
CLRS.Chapter27.pMerge_work_lower and
CLRS.Chapter27.pMerge_work_upper theorems prove its actual execution
has linear work. The theorem CLRS.Chapter27.pMerge_span_upper proves
the universal quadratic-logarithmic span upper bound, and sorted interleaved
power-of-two inputs attain the matching bound through
CLRS.Chapter27.pMerge_interleaved_span_lower.
CLRS.Chapter27.pMergeSort executes the textbook midpoint split,
parallel recursive sorting, and sequential P-MERGE phase;
CLRS.Chapter27.pMergeSort_correct proves sortedness, permutation, and
exact output length for every input. The exact step equations
CLRS.Chapter27.pMergeSort_work_step_eq and
CLRS.Chapter27.pMergeSort_span_step_eq connect its carried costs to the
recursion. The pointwise pair CLRS.Chapter27.pMergeSort_work_lower and
CLRS.Chapter27.pMergeSort_work_upper proves executable Θ(n log n) work;
CLRS.Chapter27.pMergeSort_span_upper gives the universal cubic-log span
bound, while CLRS.Chapter27.pMergeSort_worstFamily_span_lower gives the
matching recursive witness family.
Completion boundary
The executable P-MERGE-SORT cost gap is closed, and the parallel-Strassen compatibility extension has been isolated from the main-text recurrence modules. No represented Chapter 26 main-text core proof obligation remains.