Proof of `Holes are symmetric, loopless, and triangle-free`
groundedproofs/Lax342547Proofs/HoleTriangleFree.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
Symmetry exchanges the witnesses. Injectivity rules out loops. Evaluating the functional equations on the other witnesses around a triangle cancels the symmetric bilinear terms and contradicts the three parity equations.