A concrete executable gap amplifier

Use the certified arithmetic expander, complete constructive enumerations, and fixed numerical parameters to iterate the normalized amplification round. The program has no unimplemented expander or enumeration premise. Its asymptotic polynomial-time certificate charges the complete encoded tables, while its enormous fixed parameters prevent practical execution.

Main definitions

• Cslib.PCP.Encoded.Graph.arithmeticAmplify: logarithmically many concrete amplification rounds.

Main results

• Cslib.PCP.Encoded.Graph.isPolyTime_arithmeticAmplify: the complete construction certificate.
• Cslib.PCP.Encoded.Graph.satisfiable_arithmeticAmplify_iff: preservation of satisfiability.
• Cslib.PCP.Encoded.Graph.gap_le_unsatVal_arithmeticAmplify: an unconditional fixed soundness gap.

References

• I. Dinur, The PCP theorem by gap amplification
• O. Reingold, S. Vadhan, A. Wigderson, Entropy waves, the zig-zag graph product, and new constant-degree expanders

@[instance_reducible]

def Cslib.PCP.Encoded.Graph.instFinEnumZMod257 : FinEnum (ZMod 257)

Concrete enumeration of the arithmetic expander's fixed field.

@[irreducible]

def Cslib.PCP.Encoded.Graph.arithmeticAmplify (g : Graph (Bool × (Fin 6 → Bool) → Bool × (Fin 6 → Bool) → Bool)) : Graph (Bool × (Fin 6 → Bool) → Bool × (Fin 6 → Bool) → Bool)

Complete normalized rounds with fixed arithmetic expanders and fixed numerical parameters.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_arithmeticAmplify {Input : Type} {input : Input ↪ List Bool} {graph : Input → Graph (Bool × (Fin 6 → Bool) → Bool × (Fin 6 → Bool) → Bool)} (hgraph : Turing.MultiTapeTM.ComputableTidilyInPolyTime graph input (encoding (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)))) (hwellFormed : ∀ (x : Input), (graph x).WellFormed) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : Input) => (graph x).arithmeticAmplify) input (encoding (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)))

The concrete amplifier is polynomial-time in any efficiently computed well-formed input.

theorem Cslib.PCP.Encoded.Graph.wellFormed_arithmeticAmplify {g : Graph (Bool × (Fin 6 → Bool) → Bool × (Fin 6 → Bool) → Bool)} (hg : g.WellFormed) : g.arithmeticAmplify.WellFormed

Valid endpoint indices are preserved, including when the program performs no rounds.

theorem Cslib.PCP.Encoded.Graph.satisfiable_arithmeticAmplify_iff (g : Graph (Bool × (Fin 6 → Bool) → Bool × (Fin 6 → Bool) → Bool)) : (g.arithmeticAmplify.toGraph id).Satisfiable ↔ (g.toGraph id).Satisfiable

The fully specified arithmetic construction preserves satisfiability.

theorem Cslib.PCP.Encoded.Graph.gap_le_unsatVal_arithmeticAmplify {g : Graph (Bool × (Fin 6 → Bool) → Bool × (Fin 6 → Bool) → Bool)} (hunsat : ¬(g.toGraph id).Satisfiable) : ConstraintGraph.Amplification.Arithmetic.gap ≤ (g.arithmeticAmplify.toGraph id).unsatVal

Every unsatisfiable graph reaches the fixed positive gap after logarithmically many rounds.