Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

The consistency graph of accepting local views

Lax253009.ConsistencyGraph · concepts/Lax253009/ConsistencyGraph.lean · lax-253009

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    There is a vertex for each pair consisting of a random choice and an accepting local view. Two vertices are adjacent when their random choices differ and their partial assignments agree wherever both are defined. This is the consistency graph used in the PCP-to-clique reduction.

    Excluding edges between vertices with the same random choice ensures that a clique contains at most one accepting view for each choice, even when the supplied lists contain overlapping views.

    Concept map
    2 concepts; 8 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax253009.LocalTests
    2import Mathlib.Combinatorics.SimpleGraph.Clique
    3import Mathlib.Data.Fintype.Sigma
    4
    5/-!
    6---
    7title: The consistency graph of accepting local views
    8type: definition
    9---
    10There is a vertex for each pair consisting of a random choice and an
    11accepting local view. Two vertices are adjacent when their random choices
    12differ and their partial assignments agree wherever both are defined.
    13This is the consistency graph used in the PCP-to-clique reduction.
    14
    15Excluding edges between vertices with the same random choice ensures that
    16a clique contains at most one accepting view for each choice, even when
    17the supplied lists contain overlapping views.
    18-/
    19
    20namespace Lax253009.ConsistencyGraph
    21
    22open LocalTests
    23
    24abbrev Vertex {r m : ℕ} (C : System r m) :=
    25 (seed : Fin r) × {a // a ∈ C.accepting seed}
    26
    27def graph {r m : ℕ} (C : System r m) : SimpleGraph (Vertex C) where
    28 Adj u v := u.1 ≠ v.1 ∧ Compatible u.2.1 v.2.1
    29 symm := ⟨fun _ _ h ↦ ⟨Ne.symm h.1,
    30 fun i x y hx hy ↦ (h.2 i y x hy hx).symm⟩⟩
    31 loopless := ⟨fun _ h ↦ h.1 rfl⟩
    32
    33end Lax253009.ConsistencyGraph
    34
    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…