Lax Lean Archive

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

Proof of `Standard words into high-multiplicity words` (4th statement)

groundedproofs/Lax434175Proofs/HighMultiplicityTransfer.lean · lax-434175

What this proof establishes

thm✓Lax434175.HighMultiplicity (4th 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

Every instance written by the image has the processing times of the lift; the parameter of P∣∣CmaxP||Cmax is computed by the map followed by the parameter of P∣HM∣CmaxP|HM|Cmax, which FPT computes in polynomial time.