Proof of `Rank control for the frozen baseline on primal inputs` (1st statement)
groundedproofs/Lax342547Proofs/BaselineRank.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
Choose the independent frozen/table splittings, and precompose both with primal-preserving retractions onto table plus keys. This keeps all baseline agreements while bounding its primal channel rank by the table-primal dimension, number of key directions, and opposite pin rank.