Amplification with specified expanders

Dinur's preprocessing, powering and composition argument applies to any fixed expander degree and any fixed spectral bound below one. This file keeps those parameters in the interface, so that changing the construction does not require rebuilding the argument around numerical constants. The default composition uses the selected six-query tester; its numerical powering bounds accept any positive composition loss. The transformation is mathematical: an executable realization must additionally implement the graph representation and certify each transformation.

Main definitions

• Cslib.PCP.ConstraintGraph.amplifyWith: preprocessing with supplied rotations, followed by powering and composition.
• Cslib.PCP.ConstraintGraph.Amplification.retention: the value retained by preprocessing.
• Cslib.PCP.ConstraintGraph.Amplification.gain: the gain at a supplied soundness threshold.
• Cslib.PCP.ConstraintGraph.Amplification.denominator: the denominator in the gain obtained by powering and composition.
• Cslib.PCP.ConstraintGraph.Amplification.amplifier: a gap amplifier with supplied rotations.

Main results

• Cslib.PCP.ConstraintGraph.satisfiable_amplifyWith_iff: preservation of satisfiability.
• Cslib.PCP.ConstraintGraph.le_unsatVal_amplifyWith: quantitative soundness for arbitrary degree.
• Cslib.PCP.ConstraintGraph.Amplification.card_vertices and Cslib.PCP.ConstraintGraph.Amplification.card_edges: exact output sizes.
• Cslib.PCP.ConstraintGraph.min_le_unsatVal_amplifyWith: doubling up to a fixed threshold.
• Cslib.PCP.ConstraintGraph.Amplification.exists_killRate: suitable fixed parameters exist.

References

• I. Dinur, The PCP theorem by gap amplification
• I. Dinur, The PCP theorem by gap amplification, ECCC TR05-046, revision 1

@[reducible, inline]

abbrev Cslib.PCP.ConstraintGraph.Amplification.Dart (D : Type u_1) (E : Type u_2) (T q : ℕ) : Type (max u_1 u_2)

The darts after powering, for a preprocessing family with label type D.

@[reducible, inline]

abbrev Cslib.PCP.ConstraintGraph.Amplification.Vertex (D : Type u_1) (E : Type u_2) (α : Type u_3) (T q : ℕ) : Type (max (max (max u_1 u_3) u_2 u_1) u_2)

The vertices after composition.

@[reducible, inline]

abbrev Cslib.PCP.ConstraintGraph.Amplification.Edge (D : Type u_1) (E : Type u_2) (α : Type u_3) (T q : ℕ) : Type (max (max u_1 u_3) u_2 u_1)

The edges after composition.

@[instance_reducible]

instance Cslib.PCP.ConstraintGraph.Amplification.instFintypeVertexOfDecidableEq {D : Type u_1} {E : Type u_2} {α : Type u_3} [Fintype D] [DecidableEq D] [Fintype E] [Fintype α] [DecidableEq α] {T q : ℕ} : Fintype (Vertex D E α T q)

@[instance_reducible]

instance Cslib.PCP.ConstraintGraph.Amplification.instFintypeEdgeOfDecidableEq {D : Type u_1} {E : Type u_2} {α : Type u_3} [Fintype D] [DecidableEq D] [Fintype E] [Fintype α] [DecidableEq α] {T q : ℕ} : Fintype (Edge D E α T q)

noncomputable def Cslib.PCP.ConstraintGraph.Amplification.retention (d : ℕ) (μ : ℝ) : ℝ

The fraction of value retained by preprocessing with degree d and spectral bound μ.

noncomputable def Cslib.PCP.ConstraintGraph.Amplification.gain (loss : ℝ) (K d T q : ℕ) (μ γ : ℝ) : ℝ

The gain after preprocessing, powering and composition with loss loss, at threshold γ. The powering threshold is retention d μ * γ / 2, so gain at least two suffices for doubling.

noncomputable def Cslib.PCP.ConstraintGraph.Amplification.denominator (loss : ℝ) (K d : ℕ) (μ : ℝ) : ℝ

The denominator of the gain from powering and composition with loss loss, for an alphabet of size K.

theorem Cslib.PCP.ConstraintGraph.Amplification.retention_pos {d : ℕ} {μ : ℝ} (hd : 0 < d) (hμ : μ < 1) : 0 < retention d μ

A positive expander degree and a spectral bound below one give positive retention.

theorem Cslib.PCP.ConstraintGraph.Amplification.retention_le_one (d : ℕ) (μ : ℝ) : retention d μ ≤ 1

Preprocessing retains at most the original value.

theorem Cslib.PCP.ConstraintGraph.Amplification.denominator_pos {loss : ℝ} {K d : ℕ} {μ : ℝ} (hloss : 0 < loss) (hK : 0 < K) (hd : 0 < d) (hμ : μ < 1) : 0 < denominator loss K d μ

Positive composition loss, a nonempty alphabet and an expander family give a positive denominator.

theorem Cslib.PCP.ConstraintGraph.Amplification.exists_killRate {loss : ℝ} {K d : ℕ} {μ : ℝ} (hloss : 0 < loss) (hK : 0 < K) (hd : 0 < d) (hμ : μ < 1) : ∃ (q : ℕ), 2 ≤ q ∧ 2 / retention d μ ≤ (↑q - 1) / denominator loss K d μ

Every fixed positive composition loss, degree and spectral gap admit a fixed killing rate sufficient to double the value. Clients may instead supply concrete parameters.

def Cslib.PCP.ConstraintGraph.Amplification.alphabetCard (d K T : ℕ) : ℕ

The number of labels in the powered alphabet.

def Cslib.PCP.ConstraintGraph.Amplification.vertexFactor (d K T q : ℕ) : ℕ

The number of output vertices per input edge.

def Cslib.PCP.ConstraintGraph.Amplification.edgeFactor (d K T q : ℕ) : ℕ

The number of output edges per input edge.

theorem Cslib.PCP.ConstraintGraph.Amplification.card_walkLabels {D : Type u_1} {α : Type u_3} [Fintype D] [DecidableEq D] [Fintype α] (T : ℕ) : Fintype.card (WalkLabels (PreprocessLabel D) T → α) = alphabetCard (Fintype.card D) (Fintype.card α) T

The powered alphabet depends only on the original alphabet, the degree and the walk length.

theorem Cslib.PCP.ConstraintGraph.Amplification.card_dart {D : Type u_1} {E : Type u_2} [Fintype D] [Fintype E] (T q : ℕ) : Fintype.card (Dart D E T q) = 2 * ((2 * Fintype.card D + 2) * q) ^ T * Fintype.card E

The number of darts presented to composition.

theorem Cslib.PCP.ConstraintGraph.Amplification.card_vertices {D : Type u_1} {E : Type u_2} {α : Type u_3} [Fintype D] [DecidableEq D] [Fintype E] [Fintype α] (T q : ℕ) [DecidableEq α] : Fintype.card (Vertex D E α T q) = vertexFactor (Fintype.card D) (Fintype.card α) T q * Fintype.card E

Each input edge gives a fixed number of output vertices.

theorem Cslib.PCP.ConstraintGraph.Amplification.card_edges {D : Type u_1} {E : Type u_2} {α : Type u_3} [Fintype D] [DecidableEq D] [Fintype E] [Fintype α] (T q : ℕ) [DecidableEq α] : Fintype.card (Edge D E α T q) = edgeFactor (Fintype.card D) (Fintype.card α) T q * Fintype.card E

Each input edge gives a fixed number of output edges.

noncomputable def Cslib.PCP.ConstraintGraph.amplifyWith {V : Type u_1} {E : Type u} {α : Type u_2} {D : Type u_3} [Fintype E] [DecidableEq V] [Fintype D] [DecidableEq D] (G : ConstraintGraph V E α) {μ : ℝ} (X : G.PreprocessExpanders D μ) (T q : ℕ) [NeZero q] [Fintype α] [DecidableEq α] : ConstraintGraph (Amplification.Vertex D E α T q) (Amplification.Edge D E α T q) (Bool × (Fin 6 → Bool))

An amplification round with supplied cloud and half-edge rotations: preprocess, power, then compose with the selected six-query tester.

theorem Cslib.PCP.ConstraintGraph.satisfiable_amplifyWith_iff {V : Type u_1} {E : Type u} {α : Type u_2} {D : Type u_3} [Fintype E] [DecidableEq V] [Fintype D] [DecidableEq D] (G : ConstraintGraph V E α) {μ : ℝ} (X : G.PreprocessExpanders D μ) [Fintype α] [DecidableEq α] [Nonempty α] [Nonempty D] {T q : ℕ} [NeZero q] (hμ : μ < 1) (hT : 1 ≤ T) (hq : 2 ≤ q) : (G.amplifyWith X T q).Satisfiable ↔ G.Satisfiable

An amplification round preserves satisfiability when the supplied family has a spectral gap.

theorem Cslib.PCP.ConstraintGraph.le_div_unsatVal_power_preprocessWith {V : Type u_1} {E : Type u} {α : Type u_2} {D : Type u_3} [Fintype E] [DecidableEq V] [Fintype D] (G : ConstraintGraph V E α) {μ : ℝ} (X : G.PreprocessExpanders D μ) [Fintype α] [Nonempty α] [Nonempty D] {T q : ℕ} [NeZero q] (loss : ℝ) (hloss : 0 < loss) (hμ : μ < 1) (hq : 2 ≤ q) (hT : T = 4 * Fintype.card α * (q - 1)) : (↑q - 1) / Amplification.denominator loss (Fintype.card α) (Fintype.card D) μ * min (Amplification.retention (Fintype.card D) μ * G.unsatVal) (1 / ↑T ^ 2) ≤ ((G.preprocessWith X).power T q).toConstraintGraph.unsatVal / loss

Preprocessing and powering supply the quantitative gap used by composition. Dividing by the supplied positive loss makes this bound independent of the chosen assignment tester.

theorem Cslib.PCP.ConstraintGraph.le_unsatVal_amplifyWith {V : Type u_1} {E : Type u} {α : Type u_2} {D : Type u_3} [Fintype E] [DecidableEq V] [Fintype D] [DecidableEq D] (G : ConstraintGraph V E α) {μ : ℝ} (X : G.PreprocessExpanders D μ) [Fintype α] [DecidableEq α] [Nonempty α] [Nonempty D] {T q : ℕ} [NeZero q] (hμ : μ < 1) (hq : 2 ≤ q) (hT : T = 4 * Fintype.card α * (q - 1)) : (↑q - 1) / Amplification.denominator 840 (Fintype.card α) (Fintype.card D) μ * min (Amplification.retention (Fintype.card D) μ * G.unsatVal) (1 / ↑T ^ 2) ≤ (G.amplifyWith X T q).unsatVal

Quantitative amplification with arbitrary fixed degree and spectral gap. The loss from preprocessing is retention; powering and composition supply the factor linear in q.

theorem Cslib.PCP.ConstraintGraph.min_le_div_unsatVal_power_preprocessWith {V : Type u_1} {E : Type u} {α : Type u_2} {D : Type u_3} [Fintype E] [DecidableEq V] [Fintype D] (G : ConstraintGraph V E α) {μ : ℝ} (X : G.PreprocessExpanders D μ) [Fintype α] [Nonempty α] [Nonempty D] {T q : ℕ} [NeZero q] (loss : ℝ) (hloss : 0 < loss) (hμ : μ < 1) (hq : 2 ≤ q) (hT : T = 4 * Fintype.card α * (q - 1)) {γ : ℝ} (hγ : 0 ≤ γ) (hgain : 2 ≤ Amplification.gain loss (Fintype.card α) (Fintype.card D) T q μ γ) : min (2 * G.unsatVal) γ ≤ ((G.preprocessWith X).power T q).toConstraintGraph.unsatVal / loss

Preprocessing and powering double the value up to γ, after division by the composition loss, whenever the scalar gain at that threshold is at least two.

theorem Cslib.PCP.ConstraintGraph.min_le_unsatVal_amplifyWith {V : Type u_1} {E : Type u} {α : Type u_2} {D : Type u_3} [Fintype E] [DecidableEq V] [Fintype D] [DecidableEq D] (G : ConstraintGraph V E α) {μ : ℝ} (X : G.PreprocessExpanders D μ) [Fintype α] [DecidableEq α] [Nonempty α] [Nonempty D] {T q : ℕ} [NeZero q] (hμ : μ < 1) (hq : 2 ≤ q) (hT : T = 4 * Fintype.card α * (q - 1)) {γ : ℝ} (hγ : 0 ≤ γ) (hgain : 2 ≤ Amplification.gain 840 (Fintype.card α) (Fintype.card D) T q μ γ) : min (2 * G.unsatVal) γ ≤ (G.amplifyWith X T q).unsatVal

A scalar gain of at least two doubles the value up to the supplied threshold.

noncomputable def Cslib.PCP.ConstraintGraph.Amplification.round {D : Type} [Fintype D] [DecidableEq D] {μ : ℝ} (X : (G : FinConstraintGraph (Bool × (Fin 6 → Bool))) → G.graph.PreprocessExpanders D μ) (T q : ℕ) [NeZero q] (G : FinConstraintGraph (Bool × (Fin 6 → Bool))) : FinConstraintGraph (Bool × (Fin 6 → Bool))

The amplification round on bundled finite graphs. Supplying rotations separately for each input permits executable clients to retain their own cloud and vertex numberings.

noncomputable def Cslib.PCP.ConstraintGraph.Amplification.amplifier {D : Type} [Fintype D] [DecidableEq D] {μ : ℝ} (X : (G : FinConstraintGraph (Bool × (Fin 6 → Bool))) → G.graph.PreprocessExpanders D μ) [Nonempty D] (T q : ℕ) [NeZero q] (hμ : μ < 1) (hq : 2 ≤ q) (hT : T = 4 * Fintype.card (Bool × (Fin 6 → Bool)) * (q - 1)) {γ : ℝ} (hγ : 0 < γ) (hγ₁ : γ ≤ 1) (hgain : 2 ≤ gain 840 (Fintype.card (Bool × (Fin 6 → Bool))) (Fintype.card D) T q μ γ) : Amplifier (Bool × (Fin 6 → Bool))

A supplied expander construction and parameters with enough gain give an amplifier. The result is mathematical; the encoded implementation and running time need separate certificates.