Proof of `Formal forward and reverse rows of a unary mixer test` (6th statement)
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 tester term is constant along the free Z block. The point input changes affinely by its direction matrix, and the indexed row map is linear. Combining these facts with the concrete mixer expansion gives the claimed affine substitution with an explicitly fixed linear part.