Executable powering after preprocessing

Every half-edge and supplied killed walk gives one edge. Its endpoint is computed by the same rotation program as its constraint; the complete Boolean truth table is charged by the output encoding. The input graph and its original constraints may be arbitrarily large. Walk length, killing rate, degree and alphabet are fixed parameters of this transformation.

Main definitions

• Cslib.PCP.Encoded.Graph.powerPreprocess: construct the complete powered graph.

Main results

• Cslib.PCP.Encoded.Graph.isPolyTime_powerPreprocess: uniform machine-backed construction.
• Cslib.PCP.Encoded.Graph.length_edges_powerPreprocess: exact edge count.

References

• I. Dinur, The PCP theorem by gap amplification
• J. Radhakrishnan, Gap amplification in PCPs using lazy random walks

@[reducible, inline]

abbrev Cslib.PCP.Encoded.Graph.PowerLabel (D : Type) (T q : ℕ) : Type

Killed-walk labels on the preprocessed regular graph.

@[reducible, inline]

abbrev Cslib.PCP.Encoded.Graph.PowerAlphabet (D α : Type) (T : ℕ) : Type

Each powered vertex holds an opinion about every walk of length at most T.

def Cslib.PCP.Encoded.Graph.powerPreprocessEdge {C α D : Type} [DecidableEq α] (eval : C → α → α → Bool) (fallback : C) (rotate : ℕ × ℕ × D → ℕ × D) (T q : ℕ) [NeZero q] (g : Graph C) (dart : (ℕ × Bool) × PowerLabel D T q) : Edge (PowerAlphabet D α T → PowerAlphabet D α T → Bool)

Construct one powered edge and its complete Boolean relation.

def Cslib.PCP.Encoded.Graph.powerPreprocess {C α D : Type} [DecidableEq α] (eval : C → α → α → Bool) (fallback : C) (rotate : ℕ × ℕ × D → ℕ × D) (T q : ℕ) [NeZero q] (walks : List (PowerLabel D T q)) (g : Graph C) : Graph (PowerAlphabet D α T → PowerAlphabet D α T → Bool)

Enumerate every half-edge and supplied killed walk, computing endpoints and constraints.

@[simp]

theorem Cslib.PCP.Encoded.Graph.vertices_powerPreprocess {C α D : Type} [DecidableEq α] (eval : C → α → α → Bool) (fallback : C) (rotate : ℕ × ℕ × D → ℕ × D) (T q : ℕ) [NeZero q] (walks : List (PowerLabel D T q)) (g : Graph C) : (powerPreprocess eval fallback rotate T q walks g).vertices = 2 * g.edges.length

Powering retains the preprocessed half-edge vertices.

@[simp]

theorem Cslib.PCP.Encoded.Graph.length_edges_powerPreprocess {C α D : Type} [DecidableEq α] (eval : C → α → α → Bool) (fallback : C) (rotate : ℕ × ℕ × D → ℕ × D) (T q : ℕ) [NeZero q] (walks : List (PowerLabel D T q)) (g : Graph C) : (powerPreprocess eval fallback rotate T q walks g).edges.length = 2 * g.edges.length * walks.length

Every original half-edge contributes one edge per supplied killed walk.

def Cslib.PCP.Encoded.Graph.powerPreprocessEnumeration {C α D : Type} [DecidableEq α] [DecidableEq D] (g : Graph C) (eval : C → α → α → Bool) (fallback : C) (rotate : ℕ × ℕ × D → ℕ × D) (T q : ℕ) [NeZero q] (walks : List (PowerLabel D T q)) (hwalks : walks.Nodup) (hmem : ∀ (d : PowerLabel D T q), d ∈ walks) : (powerPreprocess eval fallback rotate T q walks g).edges.Enumeration fun (dart : (Fin g.edges.length × Bool) × PowerLabel D T q) => powerPreprocessEdge eval fallback rotate T q g ((↑dart.1.1, dart.1.2), dart.2)

The ordered output occurrences are indexed by the mathematical killed-walk darts. Mapping darts to stored edges preserves multiplicities, including equal constraints.

theorem Cslib.PCP.Encoded.Graph.toGraph_powerPreprocess {C α D : Type} [DecidableEq α] (g : Graph C) (eval : C → α → α → Bool) (fallback : C) (family : (n : ℕ) → RotationMap (Fin n) D) (rotate : ℕ × ℕ × D → ℕ × D) (hrotate : ∀ (n : ℕ) (v : Fin n) (d : D), rotate (n, ↑v, d) = (↑((family n).rot (v, d)).1, ((family n).rot (v, d)).2)) (T q : ℕ) [NeZero q] [DecidableEq D] (walks : List (PowerLabel D T q)) (hwalks : walks.Nodup) (hmem : ∀ (d : PowerLabel D T q), d ∈ walks) : (powerPreprocess eval fallback rotate T q walks g).toGraph id = (((g.regularPreprocess eval fallback family).power T q).toConstraintGraph.map fun (v : Fin g.edges.length × Bool) => halfEdgeNumber (↑v.1, v.2)).comap ⇑(g.powerPreprocessEnumeration eval fallback rotate T q walks hwalks hmem).equiv

The full executable graph is the mathematical power, with exact vertex and edge numbering.

theorem Cslib.PCP.Encoded.Graph.wellFormed_powerPreprocess {C α D : Type} [DecidableEq α] (g : Graph C) (eval : C → α → α → Bool) (fallback : C) (family : (n : ℕ) → RotationMap (Fin n) D) (rotate : ℕ × ℕ × D → ℕ × D) (hrotate : ∀ (n : ℕ) (v : Fin n) (d : D), rotate (n, ↑v, d) = (↑((family n).rot (v, d)).1, ((family n).rot (v, d)).2)) (T q : ℕ) [NeZero q] (walks : List (PowerLabel D T q)) : (powerPreprocess eval fallback rotate T q walks g).WellFormed

Every destination is a numbered half-edge; malformed original vertex bounds are irrelevant.

theorem Cslib.PCP.Encoded.Graph.unsatVal_powerPreprocess {C α D : Type} [DecidableEq α] (g : Graph C) (eval : C → α → α → Bool) (fallback : C) (family : (n : ℕ) → RotationMap (Fin n) D) (rotate : ℕ × ℕ × D → ℕ × D) (hrotate : ∀ (n : ℕ) (v : Fin n) (d : D), rotate (n, ↑v, d) = (↑((family n).rot (v, d)).1, ((family n).rot (v, d)).2)) (T q : ℕ) [NeZero q] [Nonempty α] [Fintype D] (walks : List (PowerLabel D T q)) (hwalks : walks.Nodup) (hmem : ∀ (d : PowerLabel D T q), d ∈ walks) : ((powerPreprocess eval fallback rotate T q walks g).toGraph id).unsatVal = ((g.regularPreprocess eval fallback family).power T q).toConstraintGraph.unsatVal

Exact numbering preserves the unsatisfied fraction of the complete powered graph.

theorem Cslib.PCP.Encoded.Graph.satisfiable_powerPreprocess_iff {C α D : Type} [DecidableEq α] (g : Graph C) (eval : C → α → α → Bool) (fallback : C) (family : (n : ℕ) → RotationMap (Fin n) D) (rotate : ℕ × ℕ × D → ℕ × D) (hrotate : ∀ (n : ℕ) (v : Fin n) (d : D), rotate (n, ↑v, d) = (↑((family n).rot (v, d)).1, ((family n).rot (v, d)).2)) (T q : ℕ) [NeZero q] [Nonempty α] (walks : List (PowerLabel D T q)) (hwalks : walks.Nodup) (hmem : ∀ (d : PowerLabel D T q), d ∈ walks) : ((powerPreprocess eval fallback rotate T q walks g).toGraph id).Satisfiable ↔ ((g.regularPreprocess eval fallback family).power T q).toConstraintGraph.Satisfiable

Exact numbering preserves satisfiability of the complete powered graph.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_powerPreprocess {C α D : Type} [DecidableEq α] {enc : C ↪ List Bool} {alphabet : α ↪ List Bool} {labelEncoding : D ↪ List Bool} [Finite D] [Finite α] {Input : Type} {input : Input ↪ List Bool} {graph : Input → Graph C} {eval : C → α → α → Bool} {rotate : ℕ × ℕ × D → ℕ × D} (hgraph : Turing.MultiTapeTM.ComputableTidilyInPolyTime graph input (encoding enc)) (hrotate : Turing.MultiTapeTM.ComputableTidilyInPolyTime rotate (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary labelEncoding)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary labelEncoding)) (heval : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : C × α × α) => eval p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair enc (Turing.MultiTapeTM.encPair alphabet alphabet)) Turing.MultiTapeTM.encBool) (fallback : C) (T q : ℕ) [NeZero q] (walks : List (PowerLabel D T q)) {output : (PowerAlphabet D α T → PowerAlphabet D α T → Bool) ↪ List Bool} : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : Input) => powerPreprocess eval fallback rotate T q walks (graph x)) input (encoding output)

The output descriptor encoding is arbitrary and fixed. Finite-table conversion hides the internal enumeration, so matching an ordinary graph expression never unfolds that enumeration.