even better more structured throughput scheduling

plot adjustments
validation adjustments

docs/compiler/scheduling-implementation.md

@@ -136,12 +136,10 @@ remain approximations, not extra inferred memory traffic.
 
 [`PipelineScheduling.cpp`](../../src/PIM/Dialect/Spatial/Passes/Transforms/MergeComputeNodes/Scheduling/PipelineScheduling.cpp) caches a per-template
 adjustment between physical execution cost and nominal volume priority, scaling
-it by chunk lanes. The original partitioning and packing candidate uses nominal
-priorities; transposes count as bulk moves there. The memory-aware candidate
-uses execution estimates for partitioning, retaining the existing core-budget
-and packing heuristics. Final
-selection evaluates bounded alternatives after physical placement, retaining
-the original candidate when the combined resource estimates worsen. PEFT,
+it by chunk lanes. Initialization uses nominal priorities; transposes count as
+bulk moves there. One joint prefix/resource DP constructs the initial partition.
+Bounded beam refinement changes partitions and their core allocations together.
+Queue-aware Spatial evaluation scores every admitted physical placement. PEFT,
 final schedule evaluation, and reported per-core demand use physical estimates.
 These quantities must not be substituted for measured simulator periods.
 
@@ -220,7 +218,7 @@ Consumed prefixes, capacities, and compaction indices cannot affect future timin
 An idle controller's past completion cannot delay future arrivals.
 These normalizations require causal, monotonic transitions, which the proof checks.
 
-Proof construction uses at most 256 generations and 16 MiB of snapshot storage.
+Proof construction uses at most 1024 generations and 64 MiB of snapshot storage.
 Each checkpoint scans events, dependencies, and remaining tokens, then orders a copy of the pending frontier.
 Exact comparisons use bounded history; hashes only filter comparisons.
 Unproved recurrence remains explicit and cannot guide multi-candidate selection.