Documentation

CslibFrontier.Computability.PolyTime.CSP.Edge.Solver.AncestryPolyTime

Native chronological ancestry compiler certificates #

The backwards scan stores one actual parent pair and one unary copy timestamp per selected expansion. A native-computable envelope of all possible parent records bounds full framed storage on every raw log, including huge binary positions and names. This bookkeeping is original and assumes no forest invariant or externally supplied resource certificate.

source
@[reducible, inline]
abbrev Cslib.Complexity.CSP.EdgeSolver.NativeForest.encTraceArgs :
Logic.PL.CSP Logic.PL.CSP.Table ℕ × List EdgeForest.ExpansionCode × TraceCode ↪ List Bool

Body and log are framed, followed by an arbitrary initial backwards-scan suffix.

Instances For
    source
    theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.computableInPolyTime_trace :
    Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Logic.PL.CSP Logic.PL.CSP.Table ℕ × List EdgeForest.ExpansionCode × TraceCode) => trace p.1 p.2.1 p.2.2) encTraceArgs encTraceCode

    A backwards chronological scan is native polynomial-time on all raw logs and suffixes. Every intermediate code is bounded by the full encoded parent-record envelope.

    source
    @[reducible, inline]
    abbrev Cslib.Complexity.CSP.EdgeSolver.NativeForest.encAncestryArgs :
    Logic.PL.CSP Logic.PL.CSP.Table ℕ × List EdgeForest.ExpansionCode × ℕ ↪ List Bool

    Body and expansion log are framed, followed by the queried binary original name.

    Instances For
      source
      theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.computableInPolyTime_ancestry :
      Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Logic.PL.CSP Logic.PL.CSP.Table ℕ × List EdgeForest.ExpansionCode × ℕ) => ancestry p.1 p.2.1 p.2.2) encAncestryArgs encTraceCode

      Native root-path reconstruction on every raw expansion log.

      source
      @[reducible, inline]
      abbrev Cslib.Complexity.CSP.EdgeSolver.NativeForest.encMeetingArgs :
      Logic.PL.CSP Logic.PL.CSP.Table ℕ × EdgeForest.MeetingCode ↪ List Bool

      The original body is framed, followed by the complete binary-position meeting code.

      Instances For
        source
        theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.computableInPolyTime_meetingWalk :
        Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Logic.PL.CSP Logic.PL.CSP.Table ℕ × EdgeForest.MeetingCode) => meetingWalk p.1 p.2) encMeetingArgs EdgeAugmenting.encWalkCode

        Candidate augmentation compilation is native polynomial-time on all raw meetings.

        source
        theorem Cslib.Complexity.CSP.EdgeSolver.NativeForest.computableInPolyTime_blossom :
        Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Logic.PL.CSP Logic.PL.CSP.Table ℕ × EdgeForest.MeetingCode) => blossom p.1 p.2) encMeetingArgs (Turing.MultiTapeTM.encOption encBlossomCode)

        Both timestamped LCA cases are native polynomial-time on every raw meeting. In particular, copy times are not original constraint names and binary labels never fund a unary traversal.