Proof of `Concrete cut-space testers and the ordered mixer form` (1st statement)
groundedproofs/Lax342547Proofs/ConcreteCut.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
Ordinary testers vanish on the common moment space. Shared testers are summed over an even number of tags. The checked cut-kernel theorem gives representative independence, and quotient descent constructs the actual linear functionals on the image of the restricted cut map.