ParetoOptimal

ProofRun is an executable review desk for software optimization claims. It helps ML and performance engineers reject invalid gains and give another reviewer reproducible evidence for an adoption decision. The Decision Room combines three separate questions: is an arithmetic rewrite equivalent under exact algebra, does it preserve machine-number results, and does an implementation preserve its contract while improving measured performance? Python egglog extracts a smaller expression; binary64 experiments expose the limits of its assumptions. Meta Muse Spark then guides cosine-retrieval investigations through real local tests. Python completes mandatory coverage and computes the verdict. In our recorded October 29 live review, a deliberately defective cache appeared 187.29 times faster but returned incorrect results and was rejected. The normalized index passed seven correctness experiments with matching benchmark outputs and measured 1.41 times faster on that local workload. A separate 25-case arithmetic experiment found two rounding mismatches and three nonfinite outcomes, despite exact symbolic equivalence. Engineers can register a trusted local Python implementation and dataset, inspect inputs and failures, export the decision packet, and replay supported findings. Import inspects evidence without executing it. Replay checks correctness and recorded timing consistency, without another model call or a claim to reproduce historical latency. The distinctive approach connects symbolic assumptions, adaptive experiments, measured behavior, and a portable review record. These are finite local findings, not universal correctness or production-savings claims.