Proof of `Graphs sampled from a hole relation`
groundedproofs/Lax342547Proofs/SampledGraph.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
Three independent sample positions would produce three pairwise holes. This argument does not require the sampled raw vertices to be distinct.