Documentation

Complexity.Computability.PCP.Encoded.Amplification

Executable amplification rounds #

A round follows the preprocessed graph's rotations, constructs every supplied powered edge and its Boolean table, then applies the assignment tester and tabulates its output. The output uses the fixed answer alphabet, so it has the same representation as the next round's input.

The degree, alphabet, walk length, killing rate, slot numbering and finite lists are fixed. All claims are uniform in the runtime graph, and the construction certificate charges the complete intermediate and output tables. Exact interpretations require complete duplicate-free lists.

Main definitions #

Main results #

References #

source
def Cslib.PCP.Encoded.Graph.amplify {C α D : Type} [Fintype α] [DecidableEq α] [Fintype D] [DecidableEq D] {width : ℕ} (eval : C → α → α → Bool) (fallback : C) (rotate : ℕ × ℕ × D → ℕ × D) (T q : ℕ) [NeZero q] (walks : List (PowerLabel D T q)) (number : SelectedComposeSlot (PowerAlphabet D α T) ≃ Fin width) (coins : List (Fin 5 × HadamardTester.Rand (PowerAlphabet D α T))) (queries : List (Fin 6)) (g : Graph C) :
Graph (Bool × (Fin 6 → Bool) → Bool × (Fin 6 → Bool) → Bool)

A normalized amplification round. Each stage materializes the next stage's input graph.

Instances For
    source
    theorem Cslib.PCP.Encoded.Graph.isPolyTime_amplify {C α D : Type} [Fintype α] [DecidableEq α] [Fintype D] [DecidableEq D] {width : ℕ} {Input : Type} {input : Input ↪ List Bool} {enc : C ↪ List Bool} {alphabet : α ↪ List Bool} {labelEncoding : D ↪ 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)) (number : SelectedComposeSlot (PowerAlphabet D α T) ≃ Fin width) (coins : List (Fin 5 × HadamardTester.Rand (PowerAlphabet D α T))) (queries : List (Fin 6)) :
    Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : Input) => amplify eval fallback rotate T q walks number coins queries (graph x)) input (encoding (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)))

    Any certified graph expression can feed a round, with all internal finite encodings hidden.

    source
    @[simp]
    theorem Cslib.PCP.Encoded.Graph.vertices_amplify {C α D : Type} [Fintype α] [DecidableEq α] [Fintype D] [DecidableEq D] {width : ℕ} (eval : C → α → α → Bool) (fallback : C) (rotate : ℕ × ℕ × D → ℕ × D) (T q : ℕ) [NeZero q] (walks : List (PowerLabel D T q)) (number : SelectedComposeSlot (PowerAlphabet D α T) ≃ Fin width) (coins : List (Fin 5 × HadamardTester.Rand (PowerAlphabet D α T))) (queries : List (Fin 6)) (g : Graph C) :
    (amplify eval fallback rotate T q walks number coins queries g).vertices = (2 * g.edges.length + 2 * g.edges.length * walks.length) * width

    The declared output vertex count is linear in the number of original edges.

    source
    @[simp]
    theorem Cslib.PCP.Encoded.Graph.length_edges_amplify {C α D : Type} [Fintype α] [DecidableEq α] [Fintype D] [DecidableEq D] {width : ℕ} (eval : C → α → α → Bool) (fallback : C) (rotate : ℕ × ℕ × D → ℕ × D) (T q : ℕ) [NeZero q] (walks : List (PowerLabel D T q)) (number : SelectedComposeSlot (PowerAlphabet D α T) ≃ Fin width) (coins : List (Fin 5 × HadamardTester.Rand (PowerAlphabet D α T))) (queries : List (Fin 6)) (g : Graph C) :
    (amplify eval fallback rotate T q walks number coins queries g).edges.length = 2 * g.edges.length * walks.length * coins.length * queries.length

    Every original half-edge contributes one edge for each walk, coin and query triple.

    source
    theorem Cslib.PCP.Encoded.Graph.wellFormed_amplify {C α D : Type} [Fintype α] [DecidableEq α] [Fintype D] [DecidableEq D] {width : ℕ} (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)) (number : SelectedComposeSlot (PowerAlphabet D α T) ≃ Fin width) (coins : List (Fin 5 × HadamardTester.Rand (PowerAlphabet D α T))) (queries : List (Fin 6)) :
    (amplify eval fallback rotate T q walks number coins queries g).WellFormed

    Every generated endpoint lies in the declared range, independently of the input bounds.

    source
    theorem Cslib.PCP.Encoded.Graph.div_le_unsatVal_amplify {C α D : Type} [Fintype α] [DecidableEq α] [Fintype D] [DecidableEq D] {width : ℕ} (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)) (number : SelectedComposeSlot (PowerAlphabet D α T) ≃ Fin width) (coins : List (Fin 5 × HadamardTester.Rand (PowerAlphabet D α T))) (queries : List (Fin 6)) [Nonempty α] (hwalks : walks.Nodup) (hmemWalks : ∀ (d : PowerLabel D T q), d ∈ walks) (hcoins : coins.Nodup) (hqueries : queries.Nodup) (hmemCoins : ∀ (ω : Fin 5 × HadamardTester.Rand (PowerAlphabet D α T)), ω ∈ coins) (hmemQueries : ∀ (i : Fin 6), i ∈ queries) :
    ((g.regularPreprocess eval fallback family).power T q).toConstraintGraph.unsatVal / 840 ≤ ((amplify eval fallback rotate T q walks number coins queries g).toGraph id).unsatVal

    The executable round retains the assignment tester's 1/840 fraction of the powered gap.

    source
    theorem Cslib.PCP.Encoded.Graph.le_unsatVal_amplify {C α D : Type} [Fintype α] [DecidableEq α] [Fintype D] [DecidableEq D] {width : ℕ} (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)) (number : SelectedComposeSlot (PowerAlphabet D α T) ≃ Fin width) (coins : List (Fin 5 × HadamardTester.Rand (PowerAlphabet D α T))) (queries : List (Fin 6)) [Nonempty α] (hwalks : walks.Nodup) (hmemWalks : ∀ (d : PowerLabel D T q), d ∈ walks) (hcoins : coins.Nodup) (hqueries : queries.Nodup) (hmemCoins : ∀ (ω : Fin 5 × HadamardTester.Rand (PowerAlphabet D α T)), ω ∈ coins) (hmemQueries : ∀ (i : Fin 6), i ∈ queries) [Nonempty D] (μ : ℝ) (hgap : ∀ (n : ℕ), (family n).spectralExpansion ≤ μ) (hμ : μ < 1) (hq : 2 ≤ q) (hT : T = 4 * Fintype.card α * (q - 1)) :
    (↑q - 1) / ConstraintGraph.Amplification.denominator 840 (Fintype.card α) (Fintype.card D) μ * min (ConstraintGraph.Amplification.retention (Fintype.card D) μ * (g.toGraph eval).unsatVal) (1 / ↑T ^ 2) ≤ ((amplify eval fallback rotate T q walks number coins queries g).toGraph id).unsatVal

    The complete executable round inherits the mathematical amplification bound, using the explicit cloud numberings selected by its preprocessing program.

    source
    theorem Cslib.PCP.Encoded.Graph.min_le_unsatVal_amplify {C α D : Type} [Fintype α] [DecidableEq α] [Fintype D] [DecidableEq D] {width : ℕ} (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)) (number : SelectedComposeSlot (PowerAlphabet D α T) ≃ Fin width) (coins : List (Fin 5 × HadamardTester.Rand (PowerAlphabet D α T))) (queries : List (Fin 6)) [Nonempty α] (hwalks : walks.Nodup) (hmemWalks : ∀ (d : PowerLabel D T q), d ∈ walks) (hcoins : coins.Nodup) (hqueries : queries.Nodup) (hmemCoins : ∀ (ω : Fin 5 × HadamardTester.Rand (PowerAlphabet D α T)), ω ∈ coins) (hmemQueries : ∀ (i : Fin 6), i ∈ queries) [Nonempty D] (μ : ℝ) (hgap : ∀ (n : ℕ), (family n).spectralExpansion ≤ μ) (hμ : μ < 1) (hq : 2 ≤ q) (hT : T = 4 * Fintype.card α * (q - 1)) {γ : ℝ} (hγ : 0 ≤ γ) (hgain : 2 ≤ ConstraintGraph.Amplification.gain 840 (Fintype.card α) (Fintype.card D) T q μ γ) :
    min (2 * (g.toGraph eval).unsatVal) γ ≤ ((amplify eval fallback rotate T q walks number coins queries g).toGraph id).unsatVal

    A killing rate with sufficient gain doubles the value up to the fixed threshold. The pre-composition bound is shared with the mathematical amplification proof.

    source
    theorem Cslib.PCP.Encoded.Graph.satisfiable_amplify_iff {C α D : Type} [Fintype α] [DecidableEq α] [Fintype D] [DecidableEq D] {width : ℕ} (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)) (number : SelectedComposeSlot (PowerAlphabet D α T) ≃ Fin width) (coins : List (Fin 5 × HadamardTester.Rand (PowerAlphabet D α T))) (queries : List (Fin 6)) [Nonempty α] (hwalks : walks.Nodup) (hmemWalks : ∀ (d : PowerLabel D T q), d ∈ walks) (hcoins : coins.Nodup) (hqueries : queries.Nodup) (hmemCoins : ∀ (ω : Fin 5 × HadamardTester.Rand (PowerAlphabet D α T)), ω ∈ coins) (hmemQueries : ∀ (i : Fin 6), i ∈ queries) [Nonempty D] (μ : ℝ) (hgap : ∀ (n : ℕ), (family n).spectralExpansion ≤ μ) (hμ : μ < 1) (hT : 1 ≤ T) (hq : 2 ≤ q) :
    ((amplify eval fallback rotate T q walks number coins queries g).toGraph id).Satisfiable ↔ (g.toGraph eval).Satisfiable

    A complete round preserves satisfiability whenever the expander family has a spectral gap.