Transport of the liveness lower bound through word encodings

Apply OpenAI's matching_recognition_degree to the product of crossing diagrams for each encoded letter. The encoding can have arbitrary, even varying, lengths. No explicit deterministic simulation is needed and no state factor is lost.

theorem Complexity.FiniteAutomaton.Machine.encoded_liveness_rank_bound {H Alpha Q : Type} [Fintype H] [Fintype Q] (M : Machine Alpha Q) (code : BRel H → List Alpha) (hM : ∀ (w : List (BRel H)), M.Accepts false (List.flatMap code w) ↔ BRel.Live w) (x y : H) (hxy : x ≠ y) : rankLoss (Fintype.card H) ≤ 4 * (Fintype.card Q + 1) ^ 2

theorem Complexity.FiniteAutomaton.encoded_oneWayLiveness_lower_bound_proof {Alpha : Type} (h : ℕ) (hh : 2 ≤ h) (code : Alphabet h → List Alpha) (positive : Bool) (s : ℕ) (D : DMachine Alpha s) (hD : ∀ (w : List (Alphabet h)), D.Accepts positive (List.flatMap code w) ↔ w ∈ oneWayLiveness h) : 2 ^ ((h - 2) / 31) ≤ 4 * (s + if positive = true then 2 else 1) ^ 2