Proof of `Baseline contractions on the selected atoms` (1st statement)
groundedproofs/Lax342547Proofs/FrozenValues.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
In each incident component both primal key directions are frozen. Thus both channel evaluation vectors are unchanged. Their dot product is the outer-product contraction of that atom; other components vanish.