Proof of `Joint channel law and its independent-column density` (3rd statement)
groundedproofs/Lax342547Proofs/ChannelDensity.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 raw mass is constant on each injective Gram orbit and its total mass is at most one. Independent columns give that orbit mass at least 2^(-h²-2), so the density on every orbit is at most 2^(h²+2).