Proof of `Clique number equals the maximum number of accepting random choices` (2nd statement)
groundedproofs/Lax253009Proofs/ConsistencyGraph.lean · lax-253009
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
Choose one accepting local view for each accepting random choice. All the chosen views extend the given proof, so they are pairwise compatible.