Proof of `Uniform mixing forms chosen simultaneously before any unit law` (2nd statement)
groundedproofs/Lax342547Proofs/UniformMixers.lean · lax-342547
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
The unary and indexed-binary bad events share the same matrix-family probability space. Their sum is at most (C_unary+C_binary)/2^n<1 above the stated threshold. Choose a family outside their union, then choose sharp matrices outside their own bad event. Restriction to the always retained blocks supplies every flavor's binary bound for these choices.