The Kibble–Zurek Speed Limit Theorem: Finite-Time Critical Crossing as a Thermodynamic Speed Limit

Paper supported by machine-verified Lean 4. The Kibble–Zurek Speed Limit Theorem (KZSLT) recasts the finite-time crossing of a second-order critical point as a thermodynamic speed limit with a universality-class exponent. Its content: (i) a product-form speed-limit equivalent to an explicit power-law bound; (ii) criticality cushions haste — for exponent α∈(0,1) the critical penalty is milder than the analytic exponent 1; (iii) a first-order optimal crossing tempo that recovers the Run-060 Tempo Theorem exactly at α=1; (iv) a minimal wall-time that diverges at criticality (critical slowing down); (v) a two-sided, Intelligence-Bound-floored defect residual; and (vi) crossing efficiency equal to cos²Θ via Cauchy–Schwarz. KZSLT is the critical/continuous member of the finite-time transition taxonomy and generalizes and contains the Run-060 Tempo Theorem. This version (1.0.0) deposits the clean analytic core (8 theorems) together with the corrected symmetry-breaking tempo penalty ρ(u,α)=(u^−α+αu)/(1+α), α∈(0,1) — a machine-verified re-proof (8 theorems) that repairs a swapped-term error in the original finding's boxed penalty and establishes strict convexity, a unique optimal tempo at u=1, and the symmetry-breaking sign law ρ<ρ_swap iff u>1 (slow crossings penalized strictly less than the swapped form predicts). Derived from the Viridis Intelligence-Bound canon; concept DOI 10.5281/zenodo.19317982.