Rotation and constraint programs for preprocessing

The edge-list construction and random-walk algorithms use the same numbered half-edges. These programs expose the complete rotation, including the return label, without rebuilding the preprocessed edge list for each call. Cloud search, numerical family rotation, constraint lookup and every copied runtime graph are charged by the joint certificates.

Main definitions

• Cslib.PCP.Encoded.Graph.preprocessRotation: rotate on a numbered half-edge.
• Cslib.PCP.Encoded.Graph.preprocessRelation: evaluate the constraint on a dart.

Main results

• Cslib.PCP.Encoded.Graph.preprocessRotation_eq: exact mathematical rotation and return label.
• Cslib.PCP.Encoded.Graph.preprocessRelation_eq_true: exact mathematical constraint.
• Cslib.PCP.Encoded.Graph.isPolyTime_preprocessRotation: uniform joint rotation certificate.
• Cslib.PCP.Encoded.Graph.isPolyTime_preprocessRelation: uniform evaluation certificate.

References

• I. Dinur, The PCP theorem by gap amplification

@[reducible, inline]

abbrev Cslib.PCP.Encoded.Graph.PreprocessLabel (D : Type) : Type

Original-edge, cloud, global-family and self-loop labels.

def Cslib.PCP.Encoded.Graph.halfEdgeOfNumber (n : ℕ) : ℕ × Bool

Decode a numbered half-edge into its edge index and endpoint bit.

@[simp]

theorem Cslib.PCP.Encoded.Graph.halfEdgeOfNumber_halfEdgeNumber (p : ℕ × Bool) : halfEdgeOfNumber (halfEdgeNumber p) = p

Numbering retains both the edge identity and its endpoint.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_halfEdgeOfNumber : Turing.MultiTapeTM.ComputableTidilyInPolyTime halfEdgeOfNumber Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool)

Dividing by two and reading the low bit are polynomial-time in the unary vertex name.

def Cslib.PCP.Encoded.Graph.preprocessRotation {C D : Type} (fallback : C) (rotate : ℕ × ℕ × D → ℕ × D) (g : Graph C) (p : (ℕ × Bool) × PreprocessLabel D) : (ℕ × Bool) × PreprocessLabel D

Rotate on one of the four kinds of preprocessed darts, retaining its return label.

def Cslib.PCP.Encoded.Graph.preprocessRelation {C α D : Type} [DecidableEq α] (eval : C → α → α → Bool) (fallback : C) (g : Graph C) (p : (ℕ × Bool) × PreprocessLabel D) (a b : α) : Bool

Original edges retain their orientation, cloud edges check equality, and new edges accept.

theorem Cslib.PCP.Encoded.Graph.preprocessRotation_eq {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)) (v : Fin g.edges.length × Bool) (d : PreprocessLabel D) : preprocessRotation fallback rotate g ((↑v.1, v.2), d) = have next := (g.regularPreprocess eval fallback family).graph.rot (v, d); ((↑next.1.1, next.1.2), next.2)

Exact agreement on the existing half-edges needs no claim about malformed vertex names.

theorem Cslib.PCP.Encoded.Graph.preprocessRelation_eq_true {C α D : Type} [DecidableEq α] (g : Graph C) (eval : C → α → α → Bool) (fallback : C) (family : (n : ℕ) → RotationMap (Fin n) D) (v : Fin g.edges.length × Bool) (d : PreprocessLabel D) (a b : α) : preprocessRelation eval fallback g ((↑v.1, v.2), d) a b = true ↔ (g.regularPreprocess eval fallback family).rel (v, d) a b

The executable constraint is the existing mathematical preprocessing constraint.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_preprocessRotation {C D : Type} {enc : C ↪ List Bool} {labelEncoding : D ↪ List Bool} {dartEncoding : PreprocessLabel D ↪ List Bool} [Finite D] {Input : Type} {input : Input ↪ List Bool} {graph : Input → Graph C} {dart : Input → (ℕ × Bool) × PreprocessLabel 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) dartEncoding)) (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) => preprocessRotation fallback rotate (graph x) (dart x)) input (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool) dartEncoding)

Computed graph and dart arguments determine their encodings before composition.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_preprocessRelation {C α D : Type} {enc : C ↪ List Bool} {dartEncoding : PreprocessLabel D ↪ List Bool} [Finite D] [DecidableEq α] {Input : Type} {input : Input ↪ List Bool} {alphabet : α ↪ List Bool} {graph : Input → Graph C} {dart : Input → (ℕ × Bool) × PreprocessLabel D} {left right : Input → α} {eval : C → α → α → Bool} (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) dartEncoding)) (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) (hleft : Turing.MultiTapeTM.ComputableTidilyInPolyTime left input alphabet) (hright : Turing.MultiTapeTM.ComputableTidilyInPolyTime right input alphabet) (fallback : C) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : Input) => preprocessRelation eval fallback (graph x) (dart x) (left x) (right x)) input Turing.MultiTapeTM.encBool

Computed constraints and labels use the same evaluator under any fixed label encoding.