Executable rotation within a vertex cloud

Cloud rotation enumerates the incident half-edges, finds the current one, calls a uniformly certified numerical rotation algorithm, and reads the resulting half-edge. It retains the return edge label. The correctness theorem identifies it with the existing mathematical cloud graph whenever the supplied rotation algorithm realizes its family on Fin n.

Main definitions

• Cslib.PCP.Encoded.Graph.cloudRotation: the executable cloud rotation.
• Cslib.PCP.Encoded.Graph.cloudFamily: the mathematical family transported to the clouds.

Main results

• Cslib.PCP.Encoded.Graph.isPolyTime_cloudRotation: a uniform certificate charging the full graph, enumeration, search, rotation, and result lookup.
• Cslib.PCP.Encoded.Graph.cloudRotation_eq: exact agreement with the transported rotation, including its return label.

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.cloudRotation {C D : Type} (fallback : C) (rotate : ℕ × ℕ × D → ℕ × D) (g : Graph C) (p : (ℕ × Bool) × D) : (ℕ × Bool) × D

Rotate within the current endpoint's cloud using its ordered half-edge enumeration. An out-of-range answer retains the input half-edge.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_cloudRotation {C D Input : Type} {input : Input ↪ List Bool} {enc : C ↪ List Bool} {labelEncoding : D ↪ List Bool} {graph : Input → Graph C} {halfEdge : Input → (ℕ × Bool) × D} {rotate : ℕ × ℕ × D → ℕ × D} (hgraph : Turing.MultiTapeTM.ComputableTidilyInPolyTime graph input (encoding enc)) (hhalfEdge : Turing.MultiTapeTM.ComputableTidilyInPolyTime halfEdge input (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool) 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) => cloudRotation fallback rotate (graph x) (halfEdge x)) input (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool) labelEncoding)

The polynomial-time hypothesis on the numerical rotation is joint in the cloud size, vertex and label. A separate machine for each size is insufficient.

def Cslib.PCP.Encoded.Graph.cloudFamily {C α D : Type} (g : Graph C) (eval : C → α → α → Bool) (fallback : C) (family : (n : ℕ) → RotationMap (Fin n) D) (vertex : ℕ) : RotationMap ((g.toGraph eval).Cloud vertex) D

Transport a numbered graph family to the explicitly enumerated mathematical clouds.

theorem Cslib.PCP.Encoded.Graph.cloudRotation_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)) (vertex : ℕ) (p : (g.toGraph eval).Cloud vertex) (d : D) : cloudRotation fallback rotate g ((↑(↑p).1, (↑p).2), d) = have next := (g.cloudFamily eval fallback family vertex).rot (p, d); ((↑(↑next.1).1, (↑next.1).2), next.2)

Exact agreement of the numerical program with the transported rotation on a cloud. The equality includes the return edge label, not only the neighboring half-edge.