Documentation

CslibFrontier.Computability.PolyTime.CSP.Edge.Solver.Step

Native machine certificate for one solver stack step #

Compile the existing finite stack operation to the native machine calculus. The intermediate case-analysis expression is proved equal on every raw state; no model, width or runtime certificate is supplied as an input. This representation bookkeeping is original.

source
@[reducible, inline]
abbrev Cslib.Complexity.CSP.EdgeSolver.Program.encEventArgs :
EdgeForest.Input × EdgeForest.MeetingCode ↪ List Bool

Complete original input is framed, followed by the native meeting code.

Instances For
    source
    theorem Cslib.Complexity.CSP.EdgeSolver.Program.computableInPolyTime_push :
    Turing.MultiTapeTM.ComputableInPolyTime (fun (p : EdgeForest.Input × EdgeForest.MeetingCode) => push p.1 p.2) encEventArgs (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encPair encFrame EdgeForest.encInput))

    Native preparation, honest whole-instance contraction and reference construction, on every raw meeting and finite buffer. No hidden contraction or preparation provider is assumed.

    source
    theorem Cslib.Complexity.CSP.EdgeSolver.Program.computableInPolyTime_augment :
    Turing.MultiTapeTM.ComputableInPolyTime (fun (p : EdgeForest.Input × EdgeForest.MeetingCode) => augment p.1 p.2) encEventArgs (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool))

    Native construction and flip of the actual chronological augmenting walk.

    source
    theorem Cslib.Complexity.CSP.EdgeSolver.Program.computableInPolyTime_lift :
    Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Frame × List Bool) => lift p.1 p.2) (Turing.MultiTapeTM.encPair encFrame (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool)) (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool))

    Native arbitrary-comparison lifting from a stored prepared parent frame.

    source
    theorem Cslib.Complexity.CSP.EdgeSolver.Program.computableInPolyTime_step :
    Turing.MultiTapeTM.ComputableInPolyTime step encState encState

    One complete finite stack step is ordinary native polynomial-time on every encoded state, including malformed widths, huge binary names, arbitrary stacks and invalid meeting buffers.