Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Proof of `The running times of FF(1,m)||ΣwjZj` (2nd statement)

groundedproofs/Lax434175Proofs/JitTimes.lean · lax-434175

What this proof establishes

thm✓Lax434175.JitFlowShopTimes (2nd statement)

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

The profile sweep of Theorem 3 of lax-496464 after the word map: the word has at most m−1m - 1 second-stage machines and the same largest processing time, so its main term is at most 4Wmmqaxn4 W m^q_max n.