Native list-funded parity-chain construction

The actual recursive chain has an equivalent bounded map implementation. Every iteration count and auxiliary offset is unary and funded by the supplied boundary list. Scope names and the output use binary naturals. Only the four constant tables of widths zero through three occur; no exponentially large white-face table is constructed.

def Cslib.Complexity.CSP.CyclicCompiler.smallEvenTable (n : ℕ) : Logic.PL.CSP.Table

Constant-size parity lookup, with a total width-three fallback.

def Cslib.Complexity.CSP.CyclicCompiler.chainScope (fresh first : ℕ) (rest : List ℕ) (i : ℕ) : List ℕ

Scope of one chain cell. The row index and fresh offset are internally unary.

theorem Cslib.Complexity.CSP.CyclicCompiler.parityChainTail_eq_map (fresh first : ℕ) (rest : List ℕ) : Logic.PL.CSP.Table.parityChainTail fresh first rest = List.map (fun (i : ℕ) => (smallEvenTable (min 3 (rest.length + 1)), chainScope fresh first rest i)) (List.range (max 1 (rest.length - 1)))

Exact bounded-map implementation of the recursive chain tail.

@[reducible, inline]

abbrev Cslib.Complexity.CSP.CyclicCompiler.encParityTail : ℕ × ℕ × List ℕ ↪ List Bool

Framed unary fresh offset, framed binary first name and binary remaining scope.

theorem Cslib.Complexity.CSP.CyclicCompiler.computableInPolyTime_parityChainTail : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × ℕ × List ℕ) => Logic.PL.CSP.Table.parityChainTail p.1 p.2.1 p.2.2) encParityTail (encCSP encTable Turing.MultiTapeTM.encNat)

Ordinary native polynomial-time construction of an arbitrary long parity chain tail.