Documentation

CslibFrontier.Computability.PolyTime.CSP.Edge.Solver.Walk

Native binary-position walk operations #

Finite operations on the existing EdgeAugmenting.WalkCode. Public positions and original names stay binary; prefix counts and scope/constraint coordinates use list-funded unary work encodings. Out-of-range binary lookups saturate at actual list lengths. No operation expands a binary position or name into an unbounded unary loop.

source
def Cslib.Complexity.CSP.EdgeSolver.NativeWalk.edges (w : EdgeAugmenting.WalkCode) :
List ℕ

Both binary global positions of each step, in traversal order.

Instances For
    source
    def Cslib.Complexity.CSP.EdgeSolver.NativeWalk.flip (bits : List Bool) (positions : List ℕ) :
    List Bool

    Flip a binary-position set in an actual finite buffer. Duplicate positions flip once.

    Instances For
      source
      def Cslib.Complexity.CSP.EdgeSolver.NativeWalk.take (w : EdgeAugmenting.WalkCode) (n : ℕ) :
      EdgeAugmenting.WalkCode

      Keep the first actual n steps. The work prefix count is unary.

      Instances For
        source
        def Cslib.Complexity.CSP.EdgeSolver.NativeWalk.drop (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (w : EdgeAugmenting.WalkCode) (n : ℕ) :
        EdgeAugmenting.WalkCode

        Remove n actual steps, starting at the preceding prefix's actual endpoint.

        Instances For
          source
          def Cslib.Complexity.CSP.EdgeSolver.NativeWalk.reverse (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (w : EdgeAugmenting.WalkCode) :
          EdgeAugmenting.WalkCode

          Reverse actual step order and swap the two positional ports in each step.

          Instances For
            source
            def Cslib.Complexity.CSP.EdgeSolver.NativeWalk.snoc (w : EdgeAugmenting.WalkCode) (a b : ℕ) :
            EdgeAugmenting.WalkCode

            Append one actual incidence pair to a code.

            Instances For
              source
              def Cslib.Complexity.CSP.EdgeSolver.NativeWalk.internal (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (w : EdgeAugmenting.WalkCode) :
              List ℕ

              Original binary variable names selected by a cycle, with duplicates erased.

              Instances For
                source
                def Cslib.Complexity.CSP.EdgeSolver.NativeWalk.inputArm (w : EdgeAugmenting.WalkCode) (step input output : ℕ) :
                EdgeAugmenting.WalkCode

                Native prefix arm at one actual step.

                Instances For
                  source
                  def Cslib.Complexity.CSP.EdgeSolver.NativeWalk.outputArm (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (w : EdgeAugmenting.WalkCode) (step input output : ℕ) :
                  EdgeAugmenting.WalkCode

                  Native reversed-suffix arm at one actual step.

                  Instances For
                    source
                    theorem Cslib.Complexity.CSP.EdgeSolver.NativeWalk.computableInPolyTime_port :
                    Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Logic.PL.CSP Logic.PL.CSP.Table ℕ × ℕ) => EdgeAugmenting.recordAt p.1 p.2) (Turing.MultiTapeTM.encPair (encCSP encTable Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encNat) EdgeAugmenting.encRecord

                    Binary port lookup scans the actual occurrence list.

                    source
                    theorem Cslib.Complexity.CSP.EdgeSolver.NativeWalk.computableInPolyTime_portWith {α : Type} {e : α ↪ List Bool} {F : α → Logic.PL.CSP Logic.PL.CSP.Table ℕ} {index : α → ℕ} (hF : Turing.MultiTapeTM.ComputableInPolyTime F e (encCSP encTable Turing.MultiTapeTM.encNat)) (hi : Turing.MultiTapeTM.ComputableInPolyTime index e Turing.MultiTapeTM.encNat) :
                    Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => EdgeAugmenting.recordAt (F a) (index a)) e EdgeAugmenting.encRecord

                    Composition with captured binary-position walk inputs.

                    source
                    theorem Cslib.Complexity.CSP.EdgeSolver.NativeWalk.computableInPolyTime_start :
                    Turing.MultiTapeTM.ComputableInPolyTime EdgeAugmenting.WalkCode.start EdgeAugmenting.encWalkCode Turing.MultiTapeTM.encNat

                    Native access to the existing binary walk-code representation.

                    source
                    theorem Cslib.Complexity.CSP.EdgeSolver.NativeWalk.computableInPolyTime_steps :
                    Turing.MultiTapeTM.ComputableInPolyTime EdgeAugmenting.WalkCode.steps EdgeAugmenting.encWalkCode (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat))

                    Native access to the existing binary walk-code representation.

                    source
                    theorem Cslib.Complexity.CSP.EdgeSolver.NativeWalk.computableInPolyTime_mk :
                    Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List (ℕ × ℕ)) => { start := p.1, steps := p.2 }) EdgeAugmenting.encWalkCodeFields EdgeAugmenting.encWalkCode

                    Native access to the existing binary walk-code representation.

                    source
                    theorem Cslib.Complexity.CSP.EdgeSolver.NativeWalk.computableInPolyTime_findIdxWith {α β : Type} {e : α ↪ List Bool} {eb : β ↪ List Bool} {xs : α → List β} {pred : α → β → Bool} (hx : Turing.MultiTapeTM.ComputableInPolyTime xs e (Turing.MultiTapeTM.encList eb)) (hp : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : α × β) => pred p.1 p.2) (Turing.MultiTapeTM.encPair e eb) Turing.MultiTapeTM.encBool) :
                    Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => List.findIdx (pred a) (xs a)) e Turing.MultiTapeTM.encUnary

                    A predicate's first matching position is a unary, list-funded scan. The Boolean map and existing idxOf machine implement findIdx exactly, including its length default.

                    source
                    theorem Cslib.Complexity.CSP.EdgeSolver.NativeWalk.computableInPolyTime_flip :
                    Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List ℕ) => flip p.1 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool)

                    Binary-position flips scan the actual buffer, including on huge malformed indices.

                    source
                    theorem Cslib.Complexity.CSP.EdgeSolver.NativeWalk.computableInPolyTime_edges :
                    Turing.MultiTapeTM.ComputableInPolyTime edges EdgeAugmenting.encWalkCode (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

                    Extracting binary step positions is native polynomial-time.

                    source
                    theorem Cslib.Complexity.CSP.EdgeSolver.NativeWalk.computableInPolyTime_finish :
                    Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Logic.PL.CSP Logic.PL.CSP.Table ℕ × EdgeAugmenting.WalkCode) => EdgeAugmenting.finish { body := p.1, labels := [], comparison := [], excluded := 0 } p.2) (Turing.MultiTapeTM.encPair (encCSP encTable Turing.MultiTapeTM.encNat) EdgeAugmenting.encWalkCode) Turing.MultiTapeTM.encNat

                    Endpoint lookup retains original binary names.

                    source
                    theorem Cslib.Complexity.CSP.EdgeSolver.NativeWalk.computableInPolyTime_internal :
                    Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Logic.PL.CSP Logic.PL.CSP.Table ℕ × EdgeAugmenting.WalkCode) => internal p.1 p.2) (Turing.MultiTapeTM.encPair (encCSP encTable Turing.MultiTapeTM.encNat) EdgeAugmenting.encWalkCode) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

                    Binary-name internal-variable enumeration is native polynomial-time on every raw code.

                    source
                    theorem Cslib.Complexity.CSP.EdgeSolver.NativeWalk.computableInPolyTime_take :
                    Turing.MultiTapeTM.ComputableInPolyTime (fun (p : EdgeAugmenting.WalkCode × ℕ) => take p.1 p.2) (Turing.MultiTapeTM.encPair EdgeAugmenting.encWalkCode Turing.MultiTapeTM.encUnary) EdgeAugmenting.encWalkCode

                    Native prefix extraction uses a unary, list-funded number of actual steps.

                    source
                    theorem Cslib.Complexity.CSP.EdgeSolver.NativeWalk.computableInPolyTime_takeWith {α : Type} {e : α ↪ List Bool} {w : α → EdgeAugmenting.WalkCode} {n : α → ℕ} (hw : Turing.MultiTapeTM.ComputableInPolyTime w e EdgeAugmenting.encWalkCode) (hn : Turing.MultiTapeTM.ComputableInPolyTime n e Turing.MultiTapeTM.encUnary) :
                    Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => take (w a) (n a)) e EdgeAugmenting.encWalkCode

                    Composition with captured binary-position walk inputs.

                    source
                    theorem Cslib.Complexity.CSP.EdgeSolver.NativeWalk.computableInPolyTime_reverse :
                    Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Logic.PL.CSP Logic.PL.CSP.Table ℕ × EdgeAugmenting.WalkCode) => reverse p.1 p.2) (Turing.MultiTapeTM.encPair (encCSP encTable Turing.MultiTapeTM.encNat) EdgeAugmenting.encWalkCode) EdgeAugmenting.encWalkCode

                    Native reversal preserves binary positions and original start/end names.

                    source
                    theorem Cslib.Complexity.CSP.EdgeSolver.NativeWalk.computableInPolyTime_finishWith {α : Type} {e : α ↪ List Bool} {F : α → Logic.PL.CSP Logic.PL.CSP.Table ℕ} {w : α → EdgeAugmenting.WalkCode} (hF : Turing.MultiTapeTM.ComputableInPolyTime F e (encCSP encTable Turing.MultiTapeTM.encNat)) (hw : Turing.MultiTapeTM.ComputableInPolyTime w e EdgeAugmenting.encWalkCode) :
                    Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => EdgeAugmenting.finish { body := F a, labels := [], comparison := [], excluded := 0 } (w a)) e Turing.MultiTapeTM.encNat

                    Compose endpoint lookup on a computed body and binary-position walk.

                    source
                    theorem Cslib.Complexity.CSP.EdgeSolver.NativeWalk.computableInPolyTime_drop :
                    Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (Logic.PL.CSP Logic.PL.CSP.Table ℕ × EdgeAugmenting.WalkCode) × ℕ) => drop p.1.1 p.1.2 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (encCSP encTable Turing.MultiTapeTM.encNat) EdgeAugmenting.encWalkCode) Turing.MultiTapeTM.encUnary) EdgeAugmenting.encWalkCode

                    Native suffix extraction is funded by a unary number of actual steps.

                    source
                    theorem Cslib.Complexity.CSP.EdgeSolver.NativeWalk.computableInPolyTime_dropWith {α : Type} {e : α ↪ List Bool} {F : α → Logic.PL.CSP Logic.PL.CSP.Table ℕ} {w : α → EdgeAugmenting.WalkCode} {n : α → ℕ} (hF : Turing.MultiTapeTM.ComputableInPolyTime F e (encCSP encTable Turing.MultiTapeTM.encNat)) (hw : Turing.MultiTapeTM.ComputableInPolyTime w e EdgeAugmenting.encWalkCode) (hn : Turing.MultiTapeTM.ComputableInPolyTime n e Turing.MultiTapeTM.encUnary) :
                    Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => drop (F a) (w a) (n a)) e EdgeAugmenting.encWalkCode

                    Compose suffix extraction on a computed problem, walk and unary prefix length.

                    source
                    theorem Cslib.Complexity.CSP.EdgeSolver.NativeWalk.computableInPolyTime_reverseWith {α : Type} {e : α ↪ List Bool} {F : α → Logic.PL.CSP Logic.PL.CSP.Table ℕ} {w : α → EdgeAugmenting.WalkCode} (hF : Turing.MultiTapeTM.ComputableInPolyTime F e (encCSP encTable Turing.MultiTapeTM.encNat)) (hw : Turing.MultiTapeTM.ComputableInPolyTime w e EdgeAugmenting.encWalkCode) :
                    Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => reverse (F a) (w a)) e EdgeAugmenting.encWalkCode

                    Compose reversal while retaining all original binary names and positions.

                    source
                    theorem Cslib.Complexity.CSP.EdgeSolver.NativeWalk.computableInPolyTime_snocWith {α : Type} {e : α ↪ List Bool} {w : α → EdgeAugmenting.WalkCode} {a b : α → ℕ} (hw : Turing.MultiTapeTM.ComputableInPolyTime w e EdgeAugmenting.encWalkCode) (ha : Turing.MultiTapeTM.ComputableInPolyTime a e Turing.MultiTapeTM.encNat) (hb : Turing.MultiTapeTM.ComputableInPolyTime b e Turing.MultiTapeTM.encNat) :
                    Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => snoc (w x) (a x) (b x)) e EdgeAugmenting.encWalkCode

                    Append a pair of binary global positions to a computed walk.

                    source
                    theorem Cslib.Complexity.CSP.EdgeSolver.NativeWalk.computableInPolyTime_inputArmWith {α : Type} {e : α ↪ List Bool} {w : α → EdgeAugmenting.WalkCode} {step a b : α → ℕ} (hw : Turing.MultiTapeTM.ComputableInPolyTime w e EdgeAugmenting.encWalkCode) (hs : Turing.MultiTapeTM.ComputableInPolyTime step e Turing.MultiTapeTM.encUnary) (ha : Turing.MultiTapeTM.ComputableInPolyTime a e Turing.MultiTapeTM.encNat) (hb : Turing.MultiTapeTM.ComputableInPolyTime b e Turing.MultiTapeTM.encNat) :
                    Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => inputArm (w x) (step x) (a x) (b x)) e EdgeAugmenting.encWalkCode

                    Native prefix-arm construction uses a unary cycle-step position and binary port positions.

                    source
                    theorem Cslib.Complexity.CSP.EdgeSolver.NativeWalk.computableInPolyTime_outputArmWith {α : Type} {e : α ↪ List Bool} {F : α → Logic.PL.CSP Logic.PL.CSP.Table ℕ} {w : α → EdgeAugmenting.WalkCode} {step a b : α → ℕ} (hF : Turing.MultiTapeTM.ComputableInPolyTime F e (encCSP encTable Turing.MultiTapeTM.encNat)) (hw : Turing.MultiTapeTM.ComputableInPolyTime w e EdgeAugmenting.encWalkCode) (hs : Turing.MultiTapeTM.ComputableInPolyTime step e Turing.MultiTapeTM.encUnary) (ha : Turing.MultiTapeTM.ComputableInPolyTime a e Turing.MultiTapeTM.encNat) (hb : Turing.MultiTapeTM.ComputableInPolyTime b e Turing.MultiTapeTM.encNat) :
                    Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => outputArm (F x) (w x) (step x) (a x) (b x)) e EdgeAugmenting.encWalkCode

                    Native reversed-suffix arms have the same unary/binary coordinate convention.

                    source
                    theorem Cslib.Complexity.CSP.EdgeSolver.NativeWalk.take_code {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (w : F.Walk) (n : ℕ) :
                    take (EdgeAugmenting.code w) n = EdgeAugmenting.code (w.take n)

                    Prefix extraction preserves every actual incidence position exactly.

                    source
                    theorem Cslib.Complexity.CSP.EdgeSolver.NativeWalk.reverse_code {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (w : F.Walk) :
                    reverse F (EdgeAugmenting.code w) = EdgeAugmenting.code w.reverse

                    Native reversal has exactly the source's traversal and starting variable.

                    source
                    theorem Cslib.Complexity.CSP.EdgeSolver.NativeWalk.drop_code {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (w : F.Walk) (n : ℕ) :
                    drop F (EdgeAugmenting.code w) n = EdgeAugmenting.code (w.drop n)

                    Native suffix extraction has the exact preceding-prefix endpoint and actual suffix.

                    source
                    theorem Cslib.Complexity.CSP.EdgeSolver.NativeWalk.snoc_code {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (w : F.Walk) (a b : F.Occurrence) :
                    snoc (EdgeAugmenting.code w) (EdgeAugmenting.occurrenceIndex a) (EdgeAugmenting.occurrenceIndex b) = EdgeAugmenting.code (w.snoc a b)

                    Appending an actual positional pair preserves its exact binary occurrence positions.

                    source
                    theorem Cslib.Complexity.CSP.EdgeSolver.NativeWalk.flip_eq (bits : List Bool) (positions : List ℕ) :
                    flip bits positions = EdgeAugmenting.flip bits positions

                    The raw flip has exactly the existing mathematical set-flip behavior.

                    source
                    theorem Cslib.Complexity.CSP.EdgeSolver.NativeWalk.edges_code {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (w : F.Walk) :
                    edges (EdgeAugmenting.code w) = List.map EdgeAugmenting.occurrenceIndex w.edges

                    Actual walk-code edges retain exactly the original incidence-list positions.

                    source
                    theorem Cslib.Complexity.CSP.EdgeSolver.NativeWalk.internal_code {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (w : F.Walk) :
                    internal F (EdgeAugmenting.code w) = Logic.PL.CSP.Blossom.internal w

                    Native selected names are exactly the source's actual internal variables, with the same duplicate-retention convention.

                    source
                    theorem Cslib.Complexity.CSP.EdgeSolver.NativeWalk.flip_buffer {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (f : F.OccurrenceLabeling Bool) (s : List F.Occurrence) :
                    flip (List.map f F.incidenceList) (List.map EdgeAugmenting.occurrenceIndex s) = List.map (BitString.flipOn s.toFinset f) F.incidenceList

                    Materialized set flips agree exactly with the original occurrence-labeling operation, for every finite positional set, including duplicate positions.

                    source
                    theorem Cslib.Complexity.CSP.EdgeSolver.NativeWalk.flip_code {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (f : F.OccurrenceLabeling Bool) (w : F.Walk) :
                    flip (List.map f F.incidenceList) (edges (EdgeAugmenting.code w)) = List.map (w.flip f) F.incidenceList

                    Flipping a materialized actual walk is exact, with no model or validity premises.

                    source
                    theorem Cslib.Complexity.CSP.EdgeSolver.NativeWalk.computableInPolyTime_flipWith {α : Type} {e : α ↪ List Bool} {bits : α → List Bool} {positions : α → List ℕ} (hb : Turing.MultiTapeTM.ComputableInPolyTime bits e (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool)) (hp : Turing.MultiTapeTM.ComputableInPolyTime positions e (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) :
                    Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => flip (bits a) (positions a)) e (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool)

                    Compose the native finite operation with computed inputs, charging their full encodings.

                    source
                    theorem Cslib.Complexity.CSP.EdgeSolver.NativeWalk.computableInPolyTime_edgesWith {α : Type} {e : α ↪ List Bool} {w : α → EdgeAugmenting.WalkCode} (hw : Turing.MultiTapeTM.ComputableInPolyTime w e EdgeAugmenting.encWalkCode) :
                    Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => edges (w a)) e (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

                    Compose the native finite operation with computed inputs, charging their full encodings.

                    source
                    theorem Cslib.Complexity.CSP.EdgeSolver.NativeWalk.computableInPolyTime_internalWith {α : Type} {e : α ↪ List Bool} {F : α → Logic.PL.CSP Logic.PL.CSP.Table ℕ} {w : α → EdgeAugmenting.WalkCode} (hF : Turing.MultiTapeTM.ComputableInPolyTime F e (encCSP encTable Turing.MultiTapeTM.encNat)) (hw : Turing.MultiTapeTM.ComputableInPolyTime w e EdgeAugmenting.encWalkCode) :
                    Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => internal (F a) (w a)) e (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

                    Compose the native finite operation with computed inputs, charging their full encodings.