Proof of `Bounded allowed derivatives preserving the actual linearized response` (1st statement)
groundedproofs/Lax342547Proofs/BoundedDerivatives.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
Observe an allowed channel vector only through its pairings with the baseline image. This observation factors through the baseline dual map. A section onto its image therefore gives a projection inside the same allowed value space with rank at most the baseline rank.