Iterating executable amplification rounds

Normalized constraint tables keep the alphabet and representation fixed across rounds. A fixed round multiplies the sum of vertices and edges by a constant and creates well-formed endpoints; every stored constraint has the same bounded table encoding. The existing iteration calculus therefore certifies a logarithmic number of complete rounds, charging all intermediate states.

The parameters and finite enumeration lists are fixed before the runtime graph. Construction certificates need no completeness assumption on those lists; gap and satisfiability claims do.

Main definitions

• Cslib.PCP.Encoded.Graph.amplifyIter: repeated normalized amplification.

Main results

• Cslib.PCP.Encoded.Graph.isPolyTime_amplifyIter_clog: a certificate for logarithmically many rounds, including their full intermediate and output table encodings.
• Cslib.PCP.Encoded.Graph.satisfiable_amplifyIter_iff: complete rounds preserve satisfiability.
• Cslib.PCP.Encoded.Graph.gap_le_unsatVal_amplifyIter_clog: logarithmically many complete rounds give a fixed positive gap on every unsatisfiable input.

References

• I. Dinur, The PCP theorem by gap amplification

@[irreducible]

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

Iterate the same normalized round over its fixed answer alphabet. Irreducibility keeps failed certificate search from unfolding the complete loop; clients use its resource and semantic contracts, or unfold the definition explicitly when reasoning about the program.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_amplifyIter_clog {D : Type} [Fintype D] [DecidableEq D] {width : ℕ} {Input : Type} {input : Input ↪ List Bool} {graph : Input → Graph (Bool × (Fin 6 → Bool) → Bool × (Fin 6 → Bool) → Bool)} {labelEncoding : D ↪ List Bool} (hgraph : Turing.MultiTapeTM.ComputableTidilyInPolyTime graph input (encoding (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)))) (hwellFormed : ∀ (x : Input), (graph x).WellFormed) (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)) (hcost : Turing.MultiTapeTM.ComputableTidilyInPolyTime rotate (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary labelEncoding)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary labelEncoding)) (fallback : Bool × (Fin 6 → Bool) → Bool × (Fin 6 → Bool) → Bool) (T q : ℕ) [NeZero q] (walks : List (PowerLabel D T q)) (number : SelectedComposeSlot (PowerAlphabet D (Bool × (Fin 6 → Bool)) T) ≃ Fin width) (coins : List (Fin 5 × HadamardTester.Rand (PowerAlphabet D (Bool × (Fin 6 → Bool)) T))) (queries : List (Fin 6)) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : Input) => amplifyIter fallback rotate T q walks number coins queries (Nat.clog 2 (graph x).edges.length) (graph x)) input (encoding (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)))

A logarithmic number of normalized rounds has polynomial cost in the original input encoding. Well-formed endpoints and the full table bound supply the loop's size invariant.

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

Every complete round preserves satisfiability, hence so does their iteration.

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

The complete rounds double the value until the fixed threshold is reached.

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

Enough complete rounds turn every unsatisfiable input into a graph above the fixed gap.

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

The logarithmic program has a constant soundness gap on every unsatisfiable input.