Proof of `Baseline contractions on the selected atoms` (2nd 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
The frozen contraction equals the actual one. The positionwise matched keys identify its tensor with the opposite matched atom's tensor. On that endpoint self-contraction is zero; on the other endpoint it is the matched atom's own-unit contraction.