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.ParallelStrassenChapter 26 Internal Parallel-Algorithm Index
This internal import index keeps the original source layout stable. Readers should use the canonical Section 26.2 and Section 26.3 pages, which present parallel matrix multiplication and parallel merge sort separately. Parallel Strassen remains an explicitly labeled 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
the numerical P-ADD and P-MATMUL cost extensions. Actual matrix executions
have dimension 2^k; no arbitrary-dimension padding/unpadding interface
is constructed by the all-input bounds. 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.