Documentation

CslibFrontier.Computability.PolyTime.Graph.RotationSystem

Native polynomial-time rotation-certificate verification #

Binary table lookup uses the existing saturating binary-index implementation. Orbit clocks are unary and computed from the edge-list length. Every intermediate iterate is a table entry or zero, whose encoded length is bounded by the encoded table; this remains true on malformed input. No certificate validity premise appears in the native resource theorem.

Main results #

source
theorem Cslib.Complexity.Graph.RotationCertificate.computableInPolyTime_successor :
Turing.MultiTapeTM.ComputableInPolyTime successor encRotationCertificate (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

Reading the supplied binary successor table is a projection of its structure encoding.

source
theorem Cslib.Complexity.Graph.RotationCertificate.incidenceVertices_polyTime :
Turing.MultiTapeTM.ComputableInPolyTime incidenceVertices encGraph (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

Enumerating listed endpoint occurrences is native polynomial-time on every raw graph.

source
@[reducible, inline]
abbrev Cslib.Complexity.Graph.RotationCertificate.encRotationWalk :
(List ℕ × ℕ) × ℕ ↪ List Bool

The table and unary iteration count are paired and framed before the binary start index.

Instances For
    source
    theorem Cslib.Complexity.Graph.RotationCertificate.computableInPolyTime_walk :
    Turing.MultiTapeTM.ComputableInPolyTime (fun (x : (List ℕ × ℕ) × ℕ) => walk x.1.1 x.1.2 x.2) encRotationWalk Turing.MultiTapeTM.encNat

    Iterating a binary-indexed successor table has a native polynomial-time implementation for a unary number of steps, including invalid and oversized table indices.

    source
    @[reducible, inline]
    abbrev Cslib.Complexity.Graph.RotationCertificate.encRotationOrbit :
    (ℕ × List ℕ) × ℕ × ℕ ↪ List Bool

    Orbit input: unary dart count, binary successor list, then two binary dart indices. Each left part is framed by its enclosing pair.

    Instances For
      source
      theorem Cslib.Complexity.Graph.RotationCertificate.computableInPolyTime_orbitBool :
      Turing.MultiTapeTM.ComputableInPolyTime (fun (x : (ℕ × List ℕ) × ℕ × ℕ) => orbitBool x.1.1 x.1.2 x.2.1 x.2.2) encRotationOrbit Turing.MultiTapeTM.encBool

      Bounded orbit membership is native polynomial-time on all tables.

      source
      theorem Cslib.Complexity.Graph.RotationCertificate.orbitBool_polyTime {α : Type} {enc : α ↪ List Bool} {n i j : α → ℕ} {table : α → List ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n enc Turing.MultiTapeTM.encUnary) (ht : Turing.MultiTapeTM.ComputableInPolyTime table enc (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (hi : Turing.MultiTapeTM.ComputableInPolyTime i enc Turing.MultiTapeTM.encNat) (hj : Turing.MultiTapeTM.ComputableInPolyTime j enc Turing.MultiTapeTM.encNat) :
      Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => orbitBool (n x) (table x) (i x) (j x)) enc Turing.MultiTapeTM.encBool

      Bounded orbit scanning composes native table, binary endpoint and unary clock computations. The clock is explicit; the runtime certificate applies to every raw table and index, without a graph, permutation or certificate-validity premise.

      source
      theorem Cslib.Complexity.Graph.RotationCertificate.range_binary :
      Turing.MultiTapeTM.ComputableInPolyTime List.range Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

      A unary-funded range can be enumerated with binary-encoded entries in polynomial time.

      source
      theorem Cslib.Complexity.Graph.RotationCertificate.computableInPolyTime_verifyRotation :
      Turing.MultiTapeTM.ComputableInPolyTime (fun (x : Graph × RotationCertificate) => verifyRotation x.1 x.2) encGraphRotationCertificate Turing.MultiTapeTM.encBool

      Every part of rotation validation runs natively in polynomial time in the graph and table encodings, without an assumed checker, recognizer, or well-formedness hypothesis.

      source
      theorem Cslib.Complexity.Graph.RotationCertificate.computableInPolyTime_componentVertices :
      Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Graph × ℕ) => componentVertices p.1 p.2) (Turing.MultiTapeTM.encPair encGraph Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

      Breadth-first expansion is native polynomial-time; the accumulated list grows by at most one copy of the declared vertex list per iteration, including on malformed graphs.

      source
      theorem Cslib.Complexity.Graph.RotationCertificate.faceTable_polyTime :
      Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Graph × RotationCertificate) => faceTable p.1 p.2) encGraphRotationCertificate (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

      Construct the inverse-successor face table by bounded scans of actual graph darts. Runtime is native polynomial time on all raw graphs and certificates, including oversized binary successors; no validity or endpoint-declaration premise is used.

      source
      theorem Cslib.Complexity.Graph.RotationCertificate.computableInPolyTime_verifyEuler :
      Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Graph × RotationCertificate) => verifyEuler p.1 p.2) encGraphRotationCertificate Turing.MultiTapeTM.encBool

      Componentwise Euler verification is native polynomial-time in the actual encoded graph and successor table. No connectivity, permutation, or index-bound premise is required.

      source
      theorem Cslib.Complexity.Graph.RotationCertificate.computableInPolyTime_verifyGenusZero :
      Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Graph × RotationCertificate) => verifyGenusZero p.1 p.2) encGraphRotationCertificate Turing.MultiTapeTM.encBool

      The full finite supplied-certificate verifier has a native polynomial-time certificate.