Proof of `Joint distribution of the unary mixer row matrix` (4th statement)
groundedproofs/Lax342547Proofs/UnaryRowLaw.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
Factor each actual symmetric profile component through its rank. The always-retained free block gives injective direction columns. If any non-Z fixing fails the unary rank bound, the common row map must have corank at least s₀+1. The single row-corank event therefore controls all fixings at once, without a union over their values or over flavors.