Proof of `The finite simultaneous unary mixer estimate` (5th statement)
groundedproofs/Lax342547Proofs/UnaryMixers.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
Substitute the proved coordinate count. The numerator is C times 2^(a n), with C independent of n and a the displayed profile-count slope. The denominator exponent is at least (a+1)n. For n≥C, the elementary inequality n<2^n makes the resulting bound strictly below one.