sgl_power_uniform

import Definitions.Def_sgl_power_all

/-!
# One machine for all inputs

`power_exists` fixes the seed's size before choosing the machine, which reads
as though the machine were built for one input length.  It is not — nothing in
the construction counts to `N`; the machine rewinds and multiplies whatever
run is there — but a scheduler must be one machine for every input, so the
quantifiers have to say so.  The induction is the same; only the machine is
chosen once, outside the `N`.
-/

namespace SipserGacsLautemann

variable {tapes : Nat}

/-- **One machine for every degree and every input.** -/
theorem power_uniform (s a b : Fin tapes) (hsa : s ≠ a) (hsb : s ≠ b)
    (hab : a ≠ b) :
    ∀ d : Nat, ∃ (S : Type) (_ : Fintype S) (M : TypedMachine tapes S),
      ∀ N : Nat, ∃ cost : Nat,
        cost ≤ 50 * (N + 2) ^ (d + 1) ∧ PowerSpec s a b N d M cost := by
  intro d
  induction d with
  | zero =>
      refine ⟨_, inferInstance, _, fun N => ⟨_, ?_, powerSpec_zero s a b hsa hsb hab N⟩⟩
      rw [pow_one]
      omega
  | succ d ih =>
      obtain ⟨S, inst, M, hM⟩ := ih
      letI := inst
      refine ⟨_, inferInstance,
        M.andThen fun _ => (rewindRun (pTape a b d)).andThen fun _ =>
          (multiply (pTape a b d) s (pOther a b d)).andThen fun _ =>
            moveUpTo (pTape a b d) 1 HeadMove.right,
        fun N => ?_⟩
      obtain ⟨cost, hb, hP⟩ := hM N
      refine ⟨_, ?_, powerSpec_step s a b hsa hsb hab N d M cost hP⟩
      set ℓ := (N + 1) ^ d with hℓ
      have hℓ1 : 1 ≤ ℓ := Nat.one_le_pow d (N + 1) (by omega)
      have hK : (ℓ - 1) * ((N + 1) * 5 + 4 + 1 + ((N + 1) * 4 + 3 + 1 + 1)
          + 1 + (1 + 1 + 1) + 1) =
          ℓ * ((N + 1) * 5 + 4 + 1 + ((N + 1) * 4 + 3 + 1 + 1)
            + 1 + (1 + 1 + 1) + 1)
          - ((N + 1) * 5 + 4 + 1 + ((N + 1) * 4 + 3 + 1 + 1)
            + 1 + (1 + 1 + 1) + 1) := Nat.sub_one_mul _ _
      have hKle : ℓ * ((N + 1) * 5 + 4 + 1 + ((N + 1) * 4 + 3 + 1 + 1)
          + 1 + (1 + 1 + 1) + 1) ≤ ℓ * (36 * (N + 2)) :=
        Nat.mul_le_mul_left ℓ (by omega)
      have hK2 : (N + 1) * 5 + 4 + 1 + ((N + 1) * 4 + 3 + 1 + 1)
          + 1 + (1 + 1 + 1) + 1 ≤
          ℓ * ((N + 1) * 5 + 4 + 1 + ((N + 1) * 4 + 3 + 1 + 1)
            + 1 + (1 + 1 + 1) + 1) :=
        Nat.le_mul_of_pos_left _ (by omega)
      have h4ℓ : 4 * ℓ ≤ 4 * (ℓ * (N + 2)) := by
        have : ℓ ≤ ℓ * (N + 2) := Nat.le_mul_of_pos_right ℓ (by omega)
        omega
      have hℓP : ℓ * (N + 2) ≤ (N + 2) ^ d * (N + 2) :=
        Nat.mul_le_mul_right (N + 2)
          (by rw [hℓ]; exact Nat.pow_le_pow_left (by omega) d)
      have hpow1 : (N + 2) ^ d * (N + 2) = (N + 2) ^ (d + 1) := by
        rw [pow_succ]
      have hpow2 : (N + 2) ^ (d + 1) * (N + 2) = (N + 2) ^ (d + 1 + 1) :=
        (pow_succ (N + 2) (d + 1)).symm
      have hmono : (N + 2) ^ (d + 1) * 2 ≤ (N + 2) ^ (d + 1) * (N + 2) :=
        Nat.mul_le_mul_left _ (by omega)
      have hge1 : 1 ≤ (N + 2) ^ (d + 1) := Nat.one_le_pow _ _ (by omega)
      have hmul36 : ℓ * (36 * (N + 2)) = 36 * (ℓ * (N + 2)) := by ring
      omega

end SipserGacsLautemann