The rational hitting-list generator is in canonical FP

This transfers OpenAI's finite-machine runtime theorem to complexitylib's canonical string-function class. Input true^n ++ [false] ++ true^s produces the exact encoded hittingList n s for positive n,s; every malformed input produces the empty string. A five-state format check supplies totality.

The source result and encoding are credited in Complexitylib.RationalHitting. This theorem concerns list generation. Polynomial bit complexity for evaluating rational formulas on the list remains a separate obligation.

theorem Complexity.RationalHitting.inputDFA_accepts_iff {w : List Bool} : w ∈ inputDFA.accepts ↔ ∃ (n : ℕ) (s : ℕ), 1 ≤ n ∧ 1 ≤ s ∧ w = binaryInput n s

The accepted inputs are exactly two positive unary parameters and a separator.

theorem Complexity.RationalHitting.hittingGenerator_binaryInput (n s : ℕ) (hn : 1 ≤ n) (hs : 1 ≤ s) : hittingGenerator (binaryInput n s) = encodeOutput (hittingList n s)

The generator returns the source's complete encoding on literal positive unary input.

theorem Complexity.RationalHitting.hittingGenerator_eq_nil {w : List Bool} (hw : ¬∃ (n : ℕ) (s : ℕ), 1 ≤ n ∧ 1 ≤ s ∧ w = binaryInput n s) : hittingGenerator w = []

Every malformed binary string produces empty output.

theorem Complexity.RationalHitting.hittingGenerator_mem_FP : hittingGenerator ∈ FP

The total hitting-list generator has polynomial time in the canonical machine model.