Executable degree reduction

The executable construction uses every half-edge as a vertex. Each has one original edge-link and one cloud-link for every label of a fixed enumerated graph family. Original constraints retain their orientation; cloud-links use equality. The program is polynomial-time given one uniform certificate for the numerical cloud rotation.

Main definitions

• Cslib.PCP.Encoded.Graph.halfEdgeNumber: number the half-edges by consecutive naturals.
• Cslib.PCP.Encoded.Graph.degreeReduce: the executable edge-list transformation.
• Cslib.PCP.Encoded.Graph.degreeReduceEval: interpret original and equality constraints.

Main results

• Cslib.PCP.Encoded.Graph.isPolyTime_degreeReduce: the entire transformation is polynomial-time.
• Cslib.PCP.Encoded.Graph.toGraph_degreeReduce: exact agreement with degree reduction.
• Cslib.PCP.Encoded.Graph.le_unsatVal_degreeReduce: the retained constraint-violation gap.

References

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

def Cslib.PCP.Encoded.Graph.halfEdgeNumber (p : ℕ × Bool) : ℕ

Consecutive vertex identifiers for the two ends of each numbered edge.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_halfEdgeNumber : Turing.MultiTapeTM.ComputableTidilyInPolyTime halfEdgeNumber (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool) Turing.MultiTapeTM.encUnary

Numbering half-edges uses only unary arithmetic.

theorem Cslib.PCP.Encoded.Graph.halfEdgeNumber_injective : Function.Injective halfEdgeNumber

Numbering does not identify the two ends of a loop or distinct parallel edges.

theorem Cslib.PCP.Encoded.Graph.halfEdgeNumber_lt {p : ℕ × Bool} {edges : ℕ} (hp : p.1 < edges) : halfEdgeNumber p < 2 * edges

Existing half-edges receive identifiers below twice the number of edges.

def Cslib.PCP.Encoded.Graph.degreeReduceDarts {C D : Type} (g : Graph C) (labels : List D) : List ((ℕ × Bool) × Option D)

Edge-link labels are none; cloud-link labels are some d.

def Cslib.PCP.Encoded.Graph.degreeReduceEdge {C D : Type} (fallback : C) (rotate : ℕ × ℕ × D → ℕ × D) (g : Graph C) (dart : (ℕ × Bool) × Option D) : Edge (Option (Bool × C))

The constraint descriptor is none for equality or some (reverse, original) for an original edge constraint, with its argument order retained.

def Cslib.PCP.Encoded.Graph.degreeReduce {C D : Type} (fallback : C) (rotate : ℕ × ℕ × D → ℕ × D) (labels : List D) (g : Graph C) : Graph (Option (Bool × C))

Construct the entire degree-reduced graph as ordinary enumeration followed by mapping.

def Cslib.PCP.Encoded.Graph.degreeReduceEval {C α : Type} [DecidableEq α] (eval : C → α → α → Bool) (constraint : Option (Bool × C)) (a b : α) : Bool

Evaluate an original oriented constraint or a cloud equality constraint.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_degreeReduceDarts {C D Input : Type} {input : Input ↪ List Bool} {enc : C ↪ List Bool} {labelEncoding : D ↪ List Bool} {graph : Input → Graph C} (hgraph : Turing.MultiTapeTM.ComputableTidilyInPolyTime graph input (encoding enc)) (labels : List D) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : Input) => (graph x).degreeReduceDarts labels) input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool) (Turing.MultiTapeTM.encOption labelEncoding)))

Enumerating all darts of degree reduction charges the full output list.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_degreeReduceEdge {C D Input : Type} {input : Input ↪ List Bool} {enc : C ↪ List Bool} {labelEncoding : D ↪ List Bool} {graph : Input → Graph C} {dart : Input → (ℕ × Bool) × Option D} {rotate : ℕ × ℕ × D → ℕ × D} (hgraph : Turing.MultiTapeTM.ComputableTidilyInPolyTime graph input (encoding enc)) (hdart : Turing.MultiTapeTM.ComputableTidilyInPolyTime dart input (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool) (Turing.MultiTapeTM.encOption labelEncoding))) (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)) (fallback : C) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : Input) => degreeReduceEdge fallback rotate (graph x) (dart x)) input (Edge.encoding (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBool enc)))

Every output edge is computed uniformly in the input graph and dart.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_degreeReduce {C D : Type} {enc : C ↪ List Bool} {labelEncoding : D ↪ List Bool} (fallback : C) (labels : List D) (rotate : ℕ × ℕ × D → ℕ × D) (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)) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (degreeReduce fallback rotate labels) (encoding enc) (encoding (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBool enc)))

The whole edge-list construction is uniformly polynomial-time, including all cloud scans, searches, rotation calls, copying, and storage of the resulting graph.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_degreeReduceEval {C α : Type} {enc : C ↪ List Bool} [DecidableEq α] {alphabet : α ↪ List Bool} {eval : C → α → α → Bool} (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) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : Option (Bool × C) × α × α) => degreeReduceEval eval p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBool enc)) (Turing.MultiTapeTM.encPair alphabet alphabet)) Turing.MultiTapeTM.encBool

Constraint evaluation remains polynomial-time, with equality implemented by comparison of encoded labels.

theorem Cslib.PCP.Encoded.Graph.length_edges_degreeReduce {C D : Type} (fallback : C) (rotate : ℕ × ℕ × D → ℕ × D) (labels : List D) (g : Graph C) : (degreeReduce fallback rotate labels g).edges.length = 2 * g.edges.length * (1 + labels.length)

A degree-reduced edge list has the expected number of darts.

@[simp]

theorem Cslib.PCP.Encoded.Graph.mem_degreeReduceDarts_iff {C D : Type} (g : Graph C) (labels : List D) (p : (ℕ × Bool) × Option D) : p ∈ g.degreeReduceDarts labels ↔ p.1.1 < g.edges.length ∧ (p.2 = none ∨ ∃ d ∈ labels, p.2 = some d)

Every enumerated dart comes from an existing original edge and a listed label.

theorem Cslib.PCP.Encoded.Graph.nodup_degreeReduceDarts {C D : Type} (g : Graph C) (labels : List D) (hlabels : labels.Nodup) : (g.degreeReduceDarts labels).Nodup

Enumerating distinct labels gives one occurrence of every dart.

def Cslib.PCP.Encoded.Graph.numberDart {D : Type} {edges : ℕ} (p : (Fin edges × Bool) × (Unit ⊕ D)) : (ℕ × Bool) × Option D

Forget the finite index proofs in a mathematical degree-reduction dart.

def Cslib.PCP.Encoded.Graph.degreeReduceEnumeration {C D : Type} [DecidableEq D] (g : Graph C) (fallback : C) (rotate : ℕ × ℕ × D → ℕ × D) (labels : List D) (hlabels : labels.Nodup) (hmem : ∀ (d : D), d ∈ labels) : (degreeReduce fallback rotate labels g).edges.Enumeration fun (p : (Fin g.edges.length × Bool) × (Unit ⊕ D)) => degreeReduceEdge fallback rotate g (numberDart p)

The ordered output occurrences are indexed by the mathematical degree-reduction darts. The original edge precedes the cloud edges at each half-edge.

@[simp]

theorem Cslib.PCP.Encoded.Graph.src_degreeReduceEdge {C D : Type} (fallback : C) (rotate : ℕ × ℕ × D → ℕ × D) (g : Graph C) (p : (ℕ × Bool) × Option D) : (degreeReduceEdge fallback rotate g p).src = halfEdgeNumber p.1

The computed source is the numbered source half-edge.

theorem Cslib.PCP.Encoded.Graph.toGraph_degreeReduce {C α D : Type} (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)) [DecidableEq α] [DecidableEq D] (labels : List D) (hlabels : labels.Nodup) (hmem : ∀ (d : D), d ∈ labels) : (degreeReduce fallback rotate labels g).toGraph (degreeReduceEval eval) = (((g.toGraph eval).degreeReduce (g.cloudFamily eval fallback family)).toConstraintGraph.map fun (p : Fin g.edges.length × Bool) => halfEdgeNumber (↑p.1, p.2)).comap ⇑(g.degreeReduceEnumeration fallback rotate labels hlabels hmem).equiv

The complete edge-list program is the existing degree reduction, with explicitly numbered vertices and the proved enumeration of its darts.

theorem Cslib.PCP.Encoded.Graph.wellFormed_degreeReduce {C D : Type} (g : Graph C) (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)) (labels : List D) : (degreeReduce fallback rotate labels g).WellFormed

Every generated endpoint is in the output vertex range. The original graph's declared vertex bound is irrelevant, because its edges themselves index the new vertices.

theorem Cslib.PCP.Encoded.Graph.halfEdgeNumber_fin_injective (edges : ℕ) : Function.Injective fun (p : Fin edges × Bool) => halfEdgeNumber (↑p.1, p.2)

Restricting half-edge numbering to existing edges is still injective.

theorem Cslib.PCP.Encoded.Graph.unsatVal_degreeReduce {C α D : Type} (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)) [DecidableEq α] [Nonempty α] [Fintype D] (labels : List D) (hlabels : labels.Nodup) (hmem : ∀ (d : D), d ∈ labels) : ((degreeReduce fallback rotate labels g).toGraph (degreeReduceEval eval)).unsatVal = ((g.toGraph eval).degreeReduce (g.cloudFamily eval fallback family)).toConstraintGraph.unsatVal

The executable output has exactly the value of the mathematical degree reduction.

theorem Cslib.PCP.Encoded.Graph.satisfiable_degreeReduce_iff {C α D : Type} (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)) [DecidableEq α] [Nonempty α] (labels : List D) (hlabels : labels.Nodup) (hmem : ∀ (d : D), d ∈ labels) : ((degreeReduce fallback rotate labels g).toGraph (degreeReduceEval eval)).Satisfiable ↔ ((g.toGraph eval).degreeReduce (g.cloudFamily eval fallback family)).toConstraintGraph.Satisfiable

The executable output has exactly the satisfiability of the mathematical degree reduction.

theorem Cslib.PCP.Encoded.Graph.le_unsatVal_degreeReduce {C α D : Type} (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)) [DecidableEq α] [Nonempty α] [Fintype D] (labels : List D) (hlabels : labels.Nodup) (hmem : ∀ (d : D), d ∈ labels) (μ : ℝ) (hgap : ∀ (n : ℕ), (family n).spectralExpansion ≤ μ) : min 1 ((1 - μ) * ↑(Fintype.card D)) / (2 * (1 + ↑(Fintype.card D))) * (g.toGraph eval).unsatVal ≤ ((degreeReduce fallback rotate labels g).toGraph (degreeReduceEval eval)).unsatVal

The uniform spectral bound transfers through the computed cloud enumeration, so the existing Dinur degree-reduction gap estimate applies to the executable graph.

theorem Cslib.PCP.Encoded.Graph.one_add_card_mul_unsatVal_degreeReduce_le {C α D : Type} (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)) [DecidableEq α] [Nonempty α] [Fintype D] (labels : List D) (hlabels : labels.Nodup) (hmem : ∀ (d : D), d ∈ labels) : (1 + ↑(Fintype.card D)) * ((degreeReduce fallback rotate labels g).toGraph (degreeReduceEval eval)).unsatVal ≤ (g.toGraph eval).unsatVal

Degree reduction does not increase the number of violations after normalizing by its degree.