Proof of `Cut profiles and the constant kernel`
groundedproofs/Lax342547Proofs/CutProfiles.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
Equality in the coordinate for each tag pair forces the sums of the two representative values to be constant. Subspace closure puts the constant in every tag's allowed space. Conversely a constant tuple contributes twice the same value to each cut, hence zero.