Native polynomial-time chronological forest search

Certificates use ordinary ComputableInPolyTime, realized by the library's native multitape machines. Work positions are unary, original names binary, and output global positions binary. The bounds charge actual encoded records and all list/option framing.

theorem Cslib.Complexity.CSP.EdgeForest.poly_binaryIndex {α : Type} {e : α ↪ List Bool} {F : α → Logic.PL.CSP Logic.PL.CSP.Table ℕ} {o : α → EdgeAugmenting.Record} (hF : Turing.MultiTapeTM.ComputableInPolyTime F e (encCSP encTable Turing.MultiTapeTM.encNat)) (ho : Turing.MultiTapeTM.ComputableInPolyTime o e EdgeAugmenting.encRecord) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => List.idxOf (o x) (F x).occurrences) e Turing.MultiTapeTM.encNat

Compute an occurrence record's binary output position by scanning the actual occurrence list; an absent record returns the actual list length, also encoded in binary.

theorem Cslib.Complexity.CSP.EdgeForest.computableInPolyTime_run : Turing.MultiTapeTM.ComputableInPolyTime run encInput (Turing.MultiTapeTM.encOption encResultCode)

Uniform ordinary native polynomial time on every raw explicit-table CSP and finite buffer. No implementation, runtime, semantic or invariant premise is supplied to this certificate.