Documentation

CslibFrontier.Computability.PolyTime.CSP.CyclicDifference.Native

Native supplied-rotation cyclic-difference compilation #

All certificates cover every raw typed input under the original framed CSP/certificate encoding. Fixed finite relation lookups may depend on the language, including exponentially large static truth tables. No computability assumption on a solver, recognizer, or arbitrary semantic function is used. Natural source labels and external certificate indices remain binary throughout.

source
@[reducible, inline]
abbrev Cslib.Complexity.CSP.CyclicCompiler.encParityChain :
ℕ × List ℕ ↪ List Bool

Unary fresh offset followed by a framed list of binary boundary names.

Instances For
    source
    theorem Cslib.Complexity.CSP.CyclicCompiler.computableInPolyTime_parityChain :
    Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List ℕ) => Logic.PL.CSP.Table.parityChain p.1 p.2) encParityChain (encCSP encTable Turing.MultiTapeTM.encNat)

    Native construction of the actual chain, including empty and malformed boundary lists.

    source
    theorem Cslib.Complexity.CSP.CyclicCompiler.computableInPolyTime_body {Rel : Type} [Finite Rel] (encRel : Rel ↪ List Bool) (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) :
    Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Logic.PL.CSP Rel ℕ × Graph.RotationCertificate) => body arity sem p.1 p.2) (encCSPRotationCertificate encRel Turing.MultiTapeTM.encNat) (encCSP encTable Turing.MultiTapeTM.encNat)

    The complete body is native polynomial time on every raw CSP/certificate pair. Fixed finite language preprocessing is a constant of this theorem, rather than a uniform algorithm on relation descriptions. All white-face construction cost is charged to actual input lists.

    source
    theorem Cslib.Complexity.CSP.CyclicCompiler.computableInPolyTime_compile {Rel : Type} [Finite Rel] (encRel : Rel ↪ List Bool) (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) :
    Turing.MultiTapeTM.ComputableInPolyTime (compile arity sem) (encCSPRotationCertificate encRel Turing.MultiTapeTM.encNat) (encCSP encTable Turing.MultiTapeTM.encNat)

    Total ordinary native polynomial-time compiler under the original framed input and explicit-table output encodings. No input-validity, positivity, semantic, or runtime premise appears: malformed arities/rotations and huge binary names/indices are included.

    source
    theorem Cslib.Complexity.CSP.CyclicCompiler.polyBounded_length_compile {Rel : Type} [Finite Rel] (encRel : Rel ↪ List Bool) (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) :
    Turing.MultiTapeTM.PolyBounded (fun (p : Logic.PL.CSP Rel ℕ × Graph.RotationCertificate) => ((encCSPRotationCertificate encRel Turing.MultiTapeTM.encNat) p).length) fun (p : Logic.PL.CSP Rel ℕ × Graph.RotationCertificate) => ((encCSP encTable Turing.MultiTapeTM.encNat) (compile arity sem p)).length

    Full framed output length is polynomial in full framed input length, including all explicit table rows, binary arities, dense auxiliary names and pair/list framing.