Proof of `Uniform mixing forms chosen simultaneously before any unit law` (3rd 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
All factors in the paper's displayed A are natural numbers, so 4⌈A⌉ is 40(K+1)p_*(g²+5). This exceeds the profile-count slope. Taking J to be 101(s₀+K²+1) gives the paper's strict mixer-budget inequality.