Documentation

CslibFrontier.Computability.PolyTime.CSP.Edge.Solver.LiftingPolyTime

Native certificates for finite lifting operations #

All working scope/constraint coordinates and prefix lengths are unary and list-funded. Original names and global walk positions remain binary. Malformed binary positions are looked up with bounded native scans; none is expanded into an unbounded unary traversal.

source
@[reducible, inline]
abbrev Cslib.Complexity.CSP.EdgeSolver.NativeLifting.encLiftResult :
Option (List Bool) ↪ List Bool

Optional lifted occurrence buffer: none is empty; some bits starts with true, then concatenates the framed one-bit Boolean encodings in buffer order.

Instances For
    source
    @[reducible, inline]
    abbrev Cslib.Complexity.CSP.EdgeSolver.NativeLifting.encRestoreWalkArgs :
    EdgeForest.Input × List ℕ × ℕ × EdgeAugmenting.WalkCode ↪ List Bool

    Original input, selected names and binary fallback are framed, followed by the complete binary-position walk to restore.

    Instances For
      source
      theorem Cslib.Complexity.CSP.EdgeSolver.NativeLifting.computableInPolyTime_restoreWalk :
      Turing.MultiTapeTM.ComputableInPolyTime (fun (p : EdgeForest.Input × List ℕ × ℕ × EdgeAugmenting.WalkCode) => restoreWalk p.1 p.2.1 p.2.2.1 p.2.2.2) encRestoreWalkArgs EdgeAugmenting.encWalkCode

      Finite surviving-port restoration is ordinary native polynomial-time on every raw input.

      source
      @[reducible, inline]
      abbrev Cslib.Complexity.CSP.EdgeSolver.NativeLifting.encPrefixArgs :
      EdgeForest.Input × EdgeAugmenting.WalkCode × EdgeAugmenting.WalkCode ↪ List Bool

      Framed original input and cycle, followed by the complete binary-position outside walk.

      Instances For
        source
        theorem Cslib.Complexity.CSP.EdgeSolver.NativeLifting.computableInPolyTime_liftPrefix :
        Turing.MultiTapeTM.ComputableInPolyTime (fun (p : EdgeForest.Input × EdgeAugmenting.WalkCode × EdgeAugmenting.WalkCode) => liftPrefix p.1 p.2.1 p.2.2) encPrefixArgs encLiftResult

        The shortest outside prefix and actual-arm scan are ordinary native polynomial-time. The certificate covers all raw buffers and codes, without semantic or width assumptions.

        source
        theorem Cslib.Complexity.CSP.EdgeSolver.NativeLifting.computableInPolyTime_liftWalk :
        Turing.MultiTapeTM.ComputableInPolyTime (fun (p : EdgeForest.Input × EdgeAugmenting.WalkCode × EdgeAugmenting.WalkCode) => liftWalk p.1 p.2.1 p.2.2) encPrefixArgs encLiftResult

        The two connector cases of whole-instance walk lifting are native polynomial-time on every raw code and buffer. Original binary names and positions retain their bit lengths.

        source
        @[reducible, inline]
        abbrev Cslib.Complexity.CSP.EdgeSolver.NativeLifting.encComparisonArgs :
        EdgeForest.Input × EdgeAugmenting.WalkCode × List Bool ↪ List Bool

        Original input is framed, then the cycle is framed, then the improving comparison's actual Boolean buffer is framed. All original names and walk positions remain binary.

        Instances For
          source
          theorem Cslib.Complexity.CSP.EdgeSolver.NativeLifting.computableInPolyTime_liftComparison :
          Turing.MultiTapeTM.ComputableInPolyTime (fun (p : EdgeForest.Input × EdgeAugmenting.WalkCode × List Bool) => liftComparison p.1 p.2.1 p.2.2) encComparisonArgs encLiftResult

          Native augmentation and arbitrary outside-comparison lifting supply the full machine certificate on all raw data, including malformed widths and huge binary names.