Documentation

Complexity.Computability.PCP.Encoded.Amplification.Enumeration

Complete enumeration for executable amplification #

Constructive finite enumerations supply the walk labels, assignment-tester slots, coins, and queries of an amplification round. The enumerations are fixed with the degree and alphabet; the graph is runtime input, and the construction certificate charges all materialized tables. The fixed enumerations can be enormous, so this interface asserts polynomial time in the graph encoding rather than practical running time at arbitrary fixed parameters.

Main definitions #

Main results #

References #

source
def Cslib.PCP.Encoded.Graph.amplifyEnumerated {C α D : Type} [FinEnum α] [FinEnum D] (eval : C → α → α → Bool) (fallback : C) (rotate : ℕ × ℕ × D → ℕ × D) (T q : ℕ) [NeZero q] (g : Graph C) :
Graph (Bool × (Fin 6 → Bool) → Bool × (Fin 6 → Bool) → Bool)

An amplification round with complete constructive enumerations for every finite parameter.

Instances For
    source
    theorem Cslib.PCP.Encoded.Graph.isPolyTime_amplifyEnumerated {C α D : Type} [FinEnum α] [FinEnum D] {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] :
    Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : Input) => amplifyEnumerated eval fallback rotate T q (graph x)) input (encoding (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)))

    A certified graph expression feeds the round without finite enumeration proof obligations.

    source
    @[simp]
    theorem Cslib.PCP.Encoded.Graph.vertices_amplifyEnumerated {C α D : Type} [FinEnum α] [FinEnum D] (eval : C → α → α → Bool) (fallback : C) (rotate : ℕ × ℕ × D → ℕ × D) (T q : ℕ) [NeZero q] (g : Graph C) :
    (amplifyEnumerated eval fallback rotate T q g).vertices = (2 * g.edges.length + 2 * g.edges.length * Fintype.card (PowerLabel D T q)) * Fintype.card (SelectedComposeSlot (PowerAlphabet D α T))

    The output vertex count uses the cardinalities of the complete finite enumerations.

    source
    @[simp]
    theorem Cslib.PCP.Encoded.Graph.length_edges_amplifyEnumerated {C α D : Type} [FinEnum α] [FinEnum D] (eval : C → α → α → Bool) (fallback : C) (rotate : ℕ × ℕ × D → ℕ × D) (T q : ℕ) [NeZero q] (g : Graph C) :
    (amplifyEnumerated eval fallback rotate T q g).edges.length = 2 * g.edges.length * Fintype.card (PowerLabel D T q) * Fintype.card (Fin 5 × HadamardTester.Rand (PowerAlphabet D α T)) * Fintype.card (Fin 6)

    Every walk, coin, and query contributes exactly one edge per original half-edge.

    source
    theorem Cslib.PCP.Encoded.Graph.wellFormed_amplifyEnumerated {C α D : Type} [FinEnum α] [FinEnum D] (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] :
    (amplifyEnumerated eval fallback rotate T q g).WellFormed

    The complete round produces valid endpoint indices, even for malformed input graphs.

    source
    theorem Cslib.PCP.Encoded.Graph.div_le_unsatVal_amplifyEnumerated {C α D : Type} [FinEnum α] [FinEnum D] (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 α] :
    ((g.regularPreprocess eval fallback family).power T q).toConstraintGraph.unsatVal / 840 ≤ ((amplifyEnumerated eval fallback rotate T q g).toGraph id).unsatVal

    The complete round retains the tester's 1/840 fraction of the powered value.

    source
    theorem Cslib.PCP.Encoded.Graph.le_unsatVal_amplifyEnumerated {C α D : Type} [FinEnum α] [FinEnum D] (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 α] [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) ≤ ((amplifyEnumerated eval fallback rotate T q g).toGraph id).unsatVal

    Constructive enumeration discharges all completeness hypotheses of the quantitative bound.

    source
    theorem Cslib.PCP.Encoded.Graph.min_le_unsatVal_amplifyEnumerated {C α D : Type} [FinEnum α] [FinEnum D] (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 α] [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) γ ≤ ((amplifyEnumerated eval fallback rotate T q g).toGraph id).unsatVal

    A killing rate with sufficient gain doubles the value up to the fixed threshold.

    source
    theorem Cslib.PCP.Encoded.Graph.satisfiable_amplifyEnumerated_iff {C α D : Type} [FinEnum α] [FinEnum D] (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 α] [Nonempty D] (μ : ℝ) (hgap : ∀ (n : ℕ), (family n).spectralExpansion ≤ μ) (hμ : μ < 1) (hT : 1 ≤ T) (hq : 2 ≤ q) :
    ((amplifyEnumerated eval fallback rotate T q g).toGraph id).Satisfiable ↔ (g.toGraph eval).Satisfiable

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