Documentation

CslibFrontier.Computability.PolyTime.Graph.RotationSystem.Recognition.Recovery

Native bounded candidate recovery #

All raw labels are binary. Unary iteration counts come only from actual endpoint fibers and vertex lists. Split queries are temporary; loop states contain orders and one candidate block, never systems or query history. Successful candidates use the existing certificate checker.

source
@[reducible, inline]
abbrev Cslib.Complexity.Graph.RotationRecognition.encWordInput :
FixedRotationInput × ℕ ↪ List Bool

Framed fixed/free input followed by the binary current vertex.

Instances For
    source
    @[reducible, inline]
    abbrev Cslib.Complexity.Graph.RotationRecognition.encBlockInput :
    (FixedRotationInput × ℕ) × List ℕ ↪ List Bool

    Framed input/vertex pair followed by a framed binary dart block.

    Instances For
      source
      @[reducible, inline]
      abbrev Cslib.Complexity.Graph.RotationRecognition.encAdvanceInput :
      (FixedRotationInput × ℕ) × Option (List ℕ) ↪ List Bool

      Framed input/vertex pair followed by an optional framed binary dart block.

      Instances For
        source
        theorem Cslib.Complexity.Graph.RotationRecognition.split_polyTime :
        Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (FixedRotationInput × ℕ) × List ℕ) => split p.1.1 p.1.2 p.2) encBlockInput encFixedRotationInput

        The split is a native list construction even on malformed raw labels and blocks.

        source
        theorem Cslib.Complexity.Graph.RotationRecognition.remaining_polyTime :
        Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (FixedRotationInput × ℕ) × List ℕ) => remaining p.1.1 p.1.2 p.2) encBlockInput (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

        Only actual unused fiber darts are scanned as candidates.

        source
        theorem Cslib.Complexity.Graph.RotationRecognition.nextCandidate_polyTime :
        Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (FixedRotationInput × ℕ) × List ℕ) => nextCandidate p.1.1 p.1.2 p.2) encBlockInput (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encNat)

        First-candidate search actually calls the concrete native XOR query on each ephemeral split.

        source
        theorem Cslib.Complexity.Graph.RotationRecognition.advance_polyTime :
        Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (FixedRotationInput × ℕ) × Option (List ℕ)) => advance p.1.1 p.1.2 p.2) encAdvanceInput (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))

        A block step has native time independent of query feasibility or input validity.

        source
        theorem Cslib.Complexity.Graph.RotationRecognition.recoverWord_polyTime :
        Turing.MultiTapeTM.ComputableInPolyTime (fun (p : FixedRotationInput × ℕ) => recoverWord p.1 p.2) encWordInput (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))

        Bounded word recovery is native polynomial-time on all raw input/vertex pairs. The loop stores only one optional block and adds at most one bounded dart per iteration.

        source
        theorem Cslib.Complexity.Graph.RotationRecognition.prescribe_polyTime :
        Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (FixedRotationInput × ℕ) × List ℕ) => prescribe p.1.1 p.1.2 p.2) encBlockInput encFixedRotationInput

        Replacement of a complete order is native; supplied vertex labels stay binary.

        source
        theorem Cslib.Complexity.Graph.RotationRecognition.completeVertex_polyTime :
        Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Option FixedRotationInput × ℕ) => completeVertex p.1 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encOption encFixedRotationInput) Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encOption encFixedRotationInput)

        A complete-vertex step uses only the current optional state and a binary vertex.

        source
        theorem Cslib.Complexity.Graph.RotationRecognition.recoverOrders_polyTime :
        Turing.MultiTapeTM.ComputableInPolyTime recoverOrders encFixedRotationInput (Turing.MultiTapeTM.encOption encFixedRotationInput)

        Native outer recovery stores only original-graph orders. The prefix bound is proved from the actual implementation, with no resource-provider premise.

        source
        theorem Cslib.Complexity.Graph.RotationRecognition.nextInWord_polyTime :
        Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List ℕ × ℕ) => nextInWord p.1 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encNat

        Native cyclic successor lookup, with unary word position and binary word entries.

        source
        theorem Cslib.Complexity.Graph.RotationRecognition.certificate_polyTime :
        Turing.MultiTapeTM.ComputableInPolyTime certificate encFixedRotationInput encRotationCertificate

        Assemble one binary successor per original dart using saturating binary endpoint lookup.

        source
        @[reducible, inline]
        abbrev Cslib.Complexity.Graph.RotationRecognition.encFixedCertificate :
        FixedRotationInput × RotationCertificate ↪ List Bool

        Framed fixed/free input followed by an existing binary successor certificate.

        Instances For
          source
          theorem Cslib.Complexity.Graph.RotationRecognition.verifyFixed_polyTime :
          Turing.MultiTapeTM.ComputableInPolyTime (fun (p : FixedRotationInput × RotationCertificate) => verifyFixed p.1 p.2) encFixedCertificate Turing.MultiTapeTM.encBool

          The supplied complete-word guard is native on all raw words and successor tables.

          source
          theorem Cslib.Complexity.Graph.RotationRecognition.recover_polyTime :
          Turing.MultiTapeTM.ComputableInPolyTime recover encFixedRotationInput (Turing.MultiTapeTM.encOption encRotationCertificate)

          The complete concrete candidate driver has native polynomial time on every raw input. Its sound guard uses the existing numerical checker; completeness remains separate.

          source
          theorem Cslib.Complexity.Graph.RotationRecognition.freePrefix_polyTime :
          Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Graph × ℕ) => freePrefix p.1 p.2) (Turing.MultiTapeTM.encPair encGraph Turing.MultiTapeTM.encNat) encFixedRotationInput

          Fixing the full orders after a free vertex prefix scans the listed graph only. Its raw binary cutoff is compared with labels, never converted into a unary scan bound.

          source
          theorem Cslib.Complexity.Graph.RotationRecognition.ofCSP_polyTime {Rel V : Type} [DecidableEq V] (encRel : Rel ↪ List Bool) (encV : V ↪ List Bool) :
          Turing.MultiTapeTM.ComputableInPolyTime ofCSP (encCSP encRel encV) encFixedRotationInput

          Original CSP scopes compile through the existing dense incidence graph. Binary source names are compared as bit strings; relation semantics and declared arity fund no scans.

          source
          theorem Cslib.Complexity.Graph.RotationRecognition.recoverCSP_polyTime {Rel V : Type} [DecidableEq V] (encRel : Rel ↪ List Bool) (encV : V ↪ List Bool) :
          Turing.MultiTapeTM.ComputableInPolyTime recoverCSP (encCSP encRel encV) (Turing.MultiTapeTM.encOption encRotationCertificate)

          Bare original CSP recovery is a native polynomial-time program using the concrete XOR solver and the existing original-position certificate checker, on every raw encoded CSP.