Theory Multitape_Alphabet_Enlargement.AlphabetEnlargement_Acceptance

theory AlphabetEnlargement_Acceptance
  imports AlphabetEnlargement_ForwardStage
begin

subsection ‹Acceptance correspondence and step-count engine›

subsubsection ‹Acceptance correspondence and initial setup›

text ‹Acceptance correspondence: ‹M› accepts iff ‹M'›'s
  state equals the canonical ‹M'›-accept config
  ‹(t_tm M, init_stage le_M)›.  Direct from
  ‹ae_simulates_def›'s XOR-style halt-arm disjunct (which pins
  down ‹(off, buf, dest, idx) = init_stage le_M› exactly when
  ‹qM' ∈ {t_tm M, r_tm M}›) plus the ‹q›-correspondence
  conjunct.›

lemma ae_simulates_accept_iff:
  fixes M :: "('q, 'a) mttm"
    and cM :: "('a, 'q) mt_config"
    and c' :: "('c :: enum ⇒ 'a,
                'q × ('a, 'c) ae_stage) mt_config"
  assumes vM:  "valid_mttm M"
      and sim: "ae_simulates M cM c'"
    shows "(mt_state cM = t_tm M)
            ⟷ (mt_state c' = (t_tm M, init_stage (le_tm M)))"
proof -
  obtain qM' ofs buf dest idx where
      state_comp: "mt_state c' = (qM', ofs, buf, dest, idx)"
    by (cases "mt_state c'")
  have sim_body:
      "((idx = SS1 ∧ qM' ∉ {t_tm M, r_tm M})
          ∨ (qM' ∈ {t_tm M, r_tm M}
               ∧ (ofs, buf, dest, idx) = init_stage (le_tm M)))
       ∧ mt_state cM = qM'
       ∧ (∀k<k_tm M. ae_tape_correspondence (le_tm M)
                 (mt_tape cM k) (mt_tape c' k))
       ∧ (idx = SS1
            ⟶ (∀k<k_tm M. mt_pos cM k = ae_decode_pos (mt_pos c' k) (ofs k)))
       ∧ ae_tape_in_gamma_block M c'"
    using sim state_comp unfolding ae_simulates_def by simp
  have disj:
      "(idx = SS1 ∧ qM' ∉ {t_tm M, r_tm M})
        ∨ (qM' ∈ {t_tm M, r_tm M}
             ∧ (ofs, buf, dest, idx) = init_stage (le_tm M))"
    using sim_body by simp
  have qM_eq: "mt_state cM = qM'" using sim_body by simp
  show ?thesis
  proof
    assume hyp: "mt_state cM = t_tm M"
    hence qM'_eq_t: "qM' = t_tm M" using qM_eq by simp
    hence q_in_halt: "qM' ∈ {t_tm M, r_tm M}" by simp
    have shape: "(ofs, buf, dest, idx) = init_stage (le_tm M)"
      using disj q_in_halt by auto
    show "mt_state c' = (t_tm M, init_stage (le_tm M))"
      using state_comp qM'_eq_t shape by simp
  next
    assume "mt_state c' = (t_tm M, init_stage (le_tm M))"
    hence "qM' = t_tm M" using state_comp by simp
    thus "mt_state cM = t_tm M" using qM_eq by simp
  qed
qed

text ‹Initial setup: post-validation, the simulation holds
  between ‹M›'s initial config on ‹u› and ‹M'›'s
  post-validation config on ‹encode_input (bl_tm M) u›.
  Combines ‹ae_validation_post_state_canonical› with the
  encoder's correctness.›

lemma ae_init_config_simulates_post_validation:
  fixes M :: "('q, 'a) mttm"
    and u :: "'a list"
  assumes vM: "valid_mttm M"
      and u_sub: "set u ⊆ Sigma_tm M"
      and le_neq_bl: "le_tm M ≠ bl_tm M"
  obtains n :: nat and c' where
      "(ae_init_config M (encode_input (bl_tm M) u), c')
            ∈ mttm_step (alphabet_enlarge_delta M) ^^ n"
    and "ae_simulates M
            (init_config_mttm M u)
            (c' :: ('c :: enum ⇒ 'a,
                    'q × ('a, 'c) ae_stage) mt_config)"
    and "ae_buffer_in_gamma_block M c'"
    and "∀kk<k_tm M. mt_tape c' kk 0 = LE_block (le_tm M)"
    and "∀i<n. ∀d :: ('c :: enum ⇒ 'a,
                          'q × ('a, 'c) ae_stage) mt_config.
            (ae_init_config M (encode_input (bl_tm M) u), d)
                ∈ mttm_step (alphabet_enlarge_delta M) ^^ i
              ⟶ snd (snd (snd (snd (mt_state d))))
                    ∈ {VFwd, VFwdPad, VRet}"
proof -
  obtain n c' where
      A: "(ae_init_config M (encode_input (bl_tm M) u), c')
            ∈ mttm_step (alphabet_enlarge_delta M) ^^ n"
    and B: "ae_simulates M
              (init_config_mttm M u)
              (c' :: ('c ⇒ 'a,
                      'q × ('a, 'c) ae_stage) mt_config)"
    and C: "ae_buffer_in_gamma_block M c'"
    and D: "∀kk<k_tm M. mt_tape c' kk 0 = LE_block (le_tm M)"
    and E: "∀i<n. ∀d :: ('c ⇒ 'a,
                            'q × ('a, 'c) ae_stage) mt_config.
              (ae_init_config M (encode_input (bl_tm M) u), d)
                  ∈ mttm_step (alphabet_enlarge_delta M) ^^ i
                ⟶ snd (snd (snd (snd (mt_state d))))
                      ∈ {VFwd, VFwdPad, VRet}"
    by (rule ae_validation_post_state_canonical[OF vM u_sub le_neq_bl])
  show ?thesis using A B C D E by (rule that)
qed

subsubsection ‹Step-count machinery and chunked simulation engine›

text ‹Step-counting lemmas: validation phase bounded by
  ‹2 ⋅ n + f⇩v›; simulation phase bounded by
  ‹8 ⋅ ⌈T(c ⋅ n) / c⌉›.›

text ‹This is the general-input form of the validation-phase
  step count: for any well-formed AE-input ‹w›, the
  validation phase completes in ‹O(|w|)› steps and lands
  either at the canonical SS1 configuration or in the reject
  state.  It is not invoked by the headline time theorem
  ‹alphabet_enlarge_time› below — for canonical
  encoder-image inputs that the base machine accepts, the
  narrower form ‹ae_validation_well_formed_to_SS1› in
  theory ‹AlphabetEnlargement_ValidationBound› gives the exact step
  count ‹2 ⋅ |w| + 4› with SS1 as the only outcome,
  which is what the linear-speedup proof needs.  The general
  form is retained as a structural completeness result
  describing the AE machine's runtime behaviour on
  non-canonical or rejected inputs — of potential use for
  downstream consumers that reason about reject paths, and for
  the nondeterministic-reverse research thread.›

lemma ae_validation_phase_step_count:
  fixes M :: "('q, 'a) mttm"
    and w :: "(('c :: enum) ⇒ 'a) list"
  assumes vM: "valid_mttm M"
      and w_sub: "set w ⊆ gamma_block (Sigma_tm M ∪ {bl_tm M})"
      and s_neq_t: "s_tm M ≠ t_tm M"
      and s_neq_r: "s_tm M ≠ r_tm M"
      and le_neq_bl: "le_tm M ≠ bl_tm M"
  obtains f⇩v :: nat and n :: nat and c' where
      "n ≤ 2 * length w + f⇩v"
    and "(ae_init_config M w, c')
            ∈ mttm_step (alphabet_enlarge_delta M) ^^ n"
    and "case mt_state c' of (qM', _, _, _, idx) ⇒
            idx = SS1 ∨ qM' = r_tm M"
proof -
  obtain f⇩v n c' where
      A: "n ≤ 2 * length w + f⇩v"
    and B: "(ae_init_config M w, c')
              ∈ mttm_step (alphabet_enlarge_delta M) ^^ n"
    and C: "case mt_state c' of (qM', _, _, _, idx) ⇒
              idx = SS1 ∨ qM' = r_tm M"
    using ae_validation_steps_bound[OF vM w_sub s_neq_t s_neq_r le_neq_bl]
    by metis
  show ?thesis using A B C by (rule that)
qed

text ‹Chunked-induction engine for the simulation-phase
  step count.  Given a specific (finite) accepting ‹M›-path
  of length ‹n› from a reachable ‹cM› with a paired SS1
  M'-config ‹c'› satisfying the invariants ‹buf_gamma›,
  ‹le_anchor›, exhibit a corresponding accepting ‹M'›-path
  of length at most ‹8 ⋅ ⌈n / c⌉›.

  Proof structure (when discharged): induction on the M-path
  length ‹n›, taking the next chunk of up to
  ‹c = card (UNIV :: 'c set)› M-steps per stage and
  invoking ‹ae_simulates_forward_stage_general›.  The
  invariant ‹buf_gamma c'_j ∧ le_anchor c'_j› is
  preserved by ‹forward_stage_general›'s output
  conjuncts (just strengthened in the previous commit).  The
  M-side ‹no_le_per_tape› hypothesis for the per-tape
  unified forward stage is discharged from
  ‹valid_reach_LE_only_pos0_mttm› on the substrate,
  threaded through ‹reach_M›.

  Wrapped by ‹ae_simulation_phase_step_count› below to
  produce the named-bound ‹obtains›-form.›

lemma ae_simulation_phase_chunked:
  fixes M :: "('q, 'a) mttm"
    and w :: "'a list"
    and cM cM_final :: "('a, 'q) mt_config"
    and c' :: "('c :: enum ⇒ 'a,
                'q × ('a, 'c) ae_stage) mt_config"
    and n :: nat
  assumes vM:         "valid_mttm M"
      and lu:         "le_unique M"
      and w_sub:      "set w ⊆ Sigma_tm M"
      and le_neq_bl:  "le_tm M ≠ bl_tm M"
      and s_neq_t:    "s_tm M ≠ t_tm M"
      and s_neq_r:    "s_tm M ≠ r_tm M"
      and reach_M:    "(init_config_mttm M w, cM)
                          ∈ (mttm_step (delta_tm M))⇧*"
      and trace:      "(cM, cM_final) ∈ (mttm_step (delta_tm M))^^n"
      and accept:     "mt_state cM_final = t_tm M"
      and sim:        "ae_simulates M cM c'"
      and buf_gamma:  "ae_buffer_in_gamma_block M c'"
      and le_anchor:  "∀kk<k_tm M. mt_tape c' kk 0 = LE_block (le_tm M)"
  shows "∃m c''. m ≤ 8 * ((n + card (UNIV :: 'c set) - 1)
                            div card (UNIV :: 'c set))
              ∧ (c', c'') ∈ (mttm_step (alphabet_enlarge_delta M))^^m
              ∧ mt_state c'' = (t_tm M, init_stage (le_tm M))"
  using reach_M trace accept sim buf_gamma le_anchor
proof (induction n arbitrary: cM cM_final c' rule: less_induct)
  case (less n)
  ― ‹Strong-induction case for path-length ‹n›.  The hypotheses
      ‹reach_M›, ‹trace›, ‹accept›, ‹sim›, ‹buf_gamma›,
      ‹le_anchor› have been re-quantified over ‹cM›,
      ‹cM_final›, ‹c'› by the induction; ‹less.prems›
      restates them for this ‹n›, and ‹less.IH› gives the
      conclusion for every strictly smaller ‹n'› (with its
      own fresh ‹cM'›, ‹cM_final'›, ‹c''›).›
  show ?case
  proof (cases n)
    case 0
    ― ‹Base case: ‹n = 0› means ‹cM = cM_final› (length-0
        trace), so ‹mt_state cM = t_tm M› by ‹accept›.
        ‹ae_simulates_accept_iff› then forces
        ‹mt_state c' = (t_tm M, init_stage (le_tm M))›.
        Witness: ‹m = 0›, ‹c'' = c'›.›
    have trace_zero: "(cM, cM_final) ∈ (mttm_step (delta_tm M))^^0"
      using less.prems(2) ‹n = 0› by simp
    have cM_eq: "cM_final = cM"
      using trace_zero by simp
    have mt_cM: "mt_state cM = t_tm M"
      using less.prems(3) cM_eq by simp
    have state_c': "mt_state c' = (t_tm M, init_stage (le_tm M))"
      using ae_simulates_accept_iff[OF vM less.prems(4)] mt_cM by simp
    have run_zero:
        "(c', c') ∈ (mttm_step (alphabet_enlarge_delta M))^^0"
      by simp
    have bound_zero:
        "(0 :: nat) ≤ 8 * ((n + card (UNIV :: 'c set) - 1)
                             div card (UNIV :: 'c set))"
      by simp
    show ?thesis
      using bound_zero run_zero state_c' by blast
  next
    case (Suc n_minus_1)
    ― ‹Inductive case: ‹n > 0›.  Select the chunk size
        ‹k_chunk ≤ c›: the earliest halt index in
        ‹[1..min n c]›, or ‹c› if no halt in that range.
        Split the trace as ‹cM →k_chunk cM_k →(n - k_chunk)
        cM_final›; apply ‹forward_stage_general› to get an
        M'-witness for the first chunk; apply ‹less.IH›
        on ‹n - k_chunk < n› for the remaining trace.›
    ― ‹Substep A: extract the first M-step from the
        non-empty trace and derive ‹cM›'s status
        (non-halt, in Q) from ‹mttm_step_src›.›
    have trace_Suc: "(cM, cM_final)
                       ∈ mttm_step (delta_tm M) ^^ Suc n_minus_1"
      using less.prems(2) Suc by simp
    obtain cM_1 where
        step_first: "(cM, cM_1) ∈ mttm_step (delta_tm M)"
      and rest_trace: "(cM_1, cM_final)
                          ∈ mttm_step (delta_tm M) ^^ n_minus_1"
      using relpow_Suc_D2[OF trace_Suc] by blast
    have cM_in_Q:  "mt_state cM ∈ Q_tm M"
      using mttm_step_src_in_Q[OF vM step_first] .
    have cM_neq_t: "mt_state cM ≠ t_tm M"
      using mttm_step_src_neq_t[OF vM step_first] .
    have cM_neq_r: "mt_state cM ≠ r_tm M"
      using mttm_step_src_neq_r[OF vM step_first] .
    ― ‹Substep B: name the alphabet-grouping size ‹c› and
        define the chunk size as ‹k_chunk = min n c›.  Since
        the universal-form ‹prefix_nhalt› hypothesis has been
        retired from ‹forward_stage_general› (the AE-chain
        audit found it was dead weight propagated through every
        layer without being used substantively), the chunk just
        needs to satisfy ‹end_or_halt›, which holds via
        ‹k_chunk = n = halt› when ‹n ≤ c›, or via
        ‹k_chunk = c› when ‹n > c›.›
    define c where "c ≡ card (UNIV :: 'c set)"
    have c_pos: "0 < c"
    proof -
      have "(c_first :: 'c) ∈ UNIV" by simp
      thus ?thesis unfolding c_def by (simp add: card_gt_0_iff)
    qed
    define k_chunk where "k_chunk ≡ min n c"
    have k_chunk_pos:  "0 < k_chunk"
      using c_pos Suc unfolding k_chunk_def by simp
    have k_chunk_le_n: "k_chunk ≤ n"
      unfolding k_chunk_def by simp
    have k_chunk_le_c: "k_chunk ≤ c"
      unfolding k_chunk_def by simp
    have k_chunk_lt_n_or_eq_n: "k_chunk < n ∨ k_chunk = n"
      using k_chunk_le_n by linarith
    ― ‹Substep C: split the M-trace at ‹k_chunk›.  Since
        ‹k_chunk ≤ n›, ‹k_chunk + (n - k_chunk) = n›;
        ‹relpow_add› turns ‹rel ^^ n› into the composition
        ‹rel ^^ k_chunk O rel ^^ (n - k_chunk)›, which a single
        unpacking exposes ‹cM_k›.›
    have trace_split_rel:
        "(cM, cM_final) ∈ (mttm_step (delta_tm M) ^^ k_chunk)
                           O (mttm_step (delta_tm M) ^^ (n - k_chunk))"
    proof -
      have sum_eq: "k_chunk + (n - k_chunk) = n"
        using k_chunk_le_n by simp
      have "(cM, cM_final) ∈ mttm_step (delta_tm M)
                                ^^ (k_chunk + (n - k_chunk))"
        using less.prems(2) sum_eq by simp
      thus ?thesis by (simp add: relpow_add)
    qed
    obtain cM_k where
        chunk_trace: "(cM, cM_k) ∈ mttm_step (delta_tm M) ^^ k_chunk"
      and rest_after_chunk:
          "(cM_k, cM_final) ∈ mttm_step (delta_tm M) ^^ (n - k_chunk)"
      using trace_split_rel by auto
    ― ‹Substep E: ‹end_or_halt›.  Two cases:
          - ‹k_chunk = n›: ‹n ≤ c›, ‹cM_k = cM_final›
            (from length-zero remaining trace), state is ‹t_tm M›
            by ‹accept›.  Second disjunct fires.
          - ‹k_chunk < n›: ‹n > c›, so ‹min n c = c›, i.e.,
            ‹k_chunk = c›.  First disjunct fires.›
    have end_or_halt:
        "k_chunk = c ∨ mt_state cM_k ∈ {t_tm M, r_tm M}"
    proof (cases "k_chunk = n")
      case True
      hence "n - k_chunk = 0" by simp
      hence "cM_k = cM_final"
        using rest_after_chunk by simp
      hence "mt_state cM_k = t_tm M"
        using less.prems(3) by simp
      thus ?thesis by simp
    next
      case False
      hence "k_chunk < n" using k_chunk_le_n by linarith
      hence "min n c < n" unfolding k_chunk_def by simp
      hence "c < n" by linarith
      hence "min n c = c" by simp
      hence "k_chunk = c" unfolding k_chunk_def by simp
      thus ?thesis by simp
    qed
    ― ‹Substep F: derive ‹no_le_per_tape› for ‹cM› from
        substrate reachability.  Each disjunct of
        ‹no_le_per_tape› asserts that an ‹M›-tape cell at some
        positive index is not the left-end marker.  The substrate
        lemma ‹valid_reach_LE_only_pos0_mttm› exactly delivers
        this for every cell index ‹p ≠ 0› along a reachable
        trace from ‹init_config_mttm M w›; the three disjuncts'
        cell indices (‹(mt_pos c' kk - 2) * c + 1 + i› and
        ‹Suc i› twice) are all syntactically positive, so the
        ‹p ≠ 0› obligation is discharged by ‹by simp›.›
    have reach_cM: "(init_config_mttm M w, cM)
                       ∈ (mttm_step (delta_tm M))⇧*"
      using less.prems(1) .
    have no_le_per_tape:
        "∀kk. (mt_pos c' kk ≥ 2
                ⟶ (∀i. i < 3 * c
                          ⟶ mt_tape cM kk
                                ((mt_pos c' kk - 2) * c + 1 + i)
                              ≠ le_tm M))
             ∧ (mt_pos c' kk = 1
                  ⟶ (∀i. i < 2 * c
                            ⟶ mt_tape cM kk (Suc i) ≠ le_tm M))
             ∧ (mt_pos c' kk = 0
                  ⟶ (∀i. i < c
                            ⟶ mt_tape cM kk (Suc i) ≠ le_tm M))"
    proof (intro allI conjI impI allI impI)
      fix kk :: nat and i :: nat
      assume "2 ≤ mt_pos c' kk" and "i < 3 * c"
      have idx_nz: "(mt_pos c' kk - 2) * c + 1 + i ≠ 0" by simp
      show "mt_tape cM kk ((mt_pos c' kk - 2) * c + 1 + i) ≠ le_tm M"
        using valid_reach_LE_only_pos0_mttm
                [OF vM lu w_sub reach_cM idx_nz le_neq_bl[symmetric]] .
    next
      fix kk :: nat and i :: nat
      assume "mt_pos c' kk = 1" and "i < 2 * c"
      have idx_nz: "Suc i ≠ 0" by simp
      show "mt_tape cM kk (Suc i) ≠ le_tm M"
        using valid_reach_LE_only_pos0_mttm
                [OF vM lu w_sub reach_cM idx_nz le_neq_bl[symmetric]] .
    next
      fix kk :: nat and i :: nat
      assume "mt_pos c' kk = 0" and "i < c"
      have idx_nz: "Suc i ≠ 0" by simp
      show "mt_tape cM kk (Suc i) ≠ le_tm M"
        using valid_reach_LE_only_pos0_mttm
                [OF vM lu w_sub reach_cM idx_nz le_neq_bl[symmetric]] .
    qed
    ― ‹Substep G: invoke ‹forward_stage_general› on the
        first chunk ‹cM →k_chunk cM_k› to obtain an
        M'-witness ‹c8› of length 8 satisfying the invariants
        needed to recurse on the remaining trace.  All twelve
        hypotheses are now in hand: ‹vM›, ‹sim› (from
        ‹less.prems›), ‹cM› in ‹Q› + non-halt (substep A),
        ‹buf_gamma› + ‹le_anchor› (from ‹less.prems›),
        ‹k_chunk_le_c› (substep B), ‹chunk_trace› (substep
        C), ‹end_or_halt› (substep E), ‹le_neq_bl› (outer
        assume), ‹no_le_per_tape› (substep F).  Uses
        ‹obtain ... by (rule ...)› as the ‹obtains›-elim
        pattern (automation diverges on ‹obtains› rules
        with multiple output conjuncts).›
    have k_chunk_le_card: "k_chunk ≤ card (UNIV :: 'c set)"
      using k_chunk_le_c unfolding c_def .
    have end_or_halt_card:
        "k_chunk = card (UNIV :: 'c set)
          ∨ mt_state cM_k ∈ {t_tm M, r_tm M}"
      using end_or_halt unfolding c_def .
    have no_le_per_tape_card:
        "∀kk. (mt_pos c' kk ≥ 2
                ⟶ (∀i. i < 3 * card (UNIV :: 'c set)
                          ⟶ mt_tape cM kk
                                ((mt_pos c' kk - 2) * card (UNIV :: 'c set) + 1 + i)
                              ≠ le_tm M))
             ∧ (mt_pos c' kk = 1
                  ⟶ (∀i. i < 2 * card (UNIV :: 'c set)
                            ⟶ mt_tape cM kk (Suc i) ≠ le_tm M))
             ∧ (mt_pos c' kk = 0
                  ⟶ (∀i. i < card (UNIV :: 'c set)
                            ⟶ mt_tape cM kk (Suc i) ≠ le_tm M))"
      using no_le_per_tape unfolding c_def .
    obtain c8 where
        chain8: "(c', c8) ∈ mttm_step (alphabet_enlarge_delta M) ^^ 8"
      and sim_c8: "ae_simulates M cM_k c8"
      and buf_gamma_c8: "ae_buffer_in_gamma_block M c8"
      and le_anchor_c8: "∀kk<k_tm M. mt_tape c8 kk 0 = LE_block (le_tm M)"
      by (rule ae_simulates_forward_stage_general
                 [OF vM lu less.prems(4) cM_in_Q cM_neq_t cM_neq_r
                     less.prems(5) k_chunk_le_card chunk_trace
                     end_or_halt_card less.prems(6) le_neq_bl
                     no_le_per_tape_card])
    ― ‹Substep H: extend the substrate-reachability of ‹cM›
        to ‹cM_k›.  Composes ‹reach_cM› (an ‹rtrancl›
        certificate) with ‹chunk_trace› (a ‹relpow›
        certificate of length ‹k_chunk›) by lifting the
        ‹relpow› to ‹rtrancl› via ‹relpow_imp_rtrancl›,
        then composing via ‹rtrancl_trans›.  Needed because
        the IH recursion requires the substrate-reachability of
        the recursion's starting M-config (here, ‹cM_k›).›
    have chunk_in_rtrancl: "(cM, cM_k) ∈ (mttm_step (delta_tm M))⇧*"
      using chunk_trace by (rule relpow_imp_rtrancl)
    have reach_cM_k: "(init_config_mttm M w, cM_k)
                         ∈ (mttm_step (delta_tm M))⇧*"
      using reach_cM chunk_in_rtrancl by (rule rtrancl_trans)
    ― ‹Substep I: apply ‹less.IH› for the remaining trace
        ‹cM_k →(n - k_chunk) cM_final›.  Recursion is on
        ‹n - k_chunk < n› (which holds because
        ‹k_chunk ≥ 1› and ‹n ≥ 1›); the re-quantified
        hypotheses are ‹reach_cM_k› (substep H),
        ‹rest_after_chunk› (substep C),
        ‹less.prems(3)› (accept), ‹sim_c8›, ‹buf_gamma_c8›,
        ‹le_anchor_c8› (substep G).  Yields the recursion-arm
        witness ‹(m_rec, c'')›: an M'-path of length ‹m_rec›
        from ‹c8› ending in canonical halt, with ‹m_rec›
        bounded by ‹8 ⋅ ⌈(n - k_chunk) / c⌉›.›
    have n_minus_lt_n: "n - k_chunk < n"
      using k_chunk_pos Suc by linarith
    obtain m_rec c'' where
        bound_rec: "m_rec ≤ 8 * ((n - k_chunk + card (UNIV :: 'c set) - 1)
                                   div card (UNIV :: 'c set))"
      and chain_rec: "(c8, c'') ∈ (mttm_step (alphabet_enlarge_delta M))^^m_rec"
      and state_c'': "mt_state c'' = (t_tm M, init_stage (le_tm M))"
      using less.IH[OF n_minus_lt_n reach_cM_k rest_after_chunk
                       less.prems(3) sim_c8 buf_gamma_c8 le_anchor_c8]
      by blast
    ― ‹Substep J: compose the 8-step forward chunk ‹chain8›
        with the recursion-arm ‹chain_rec› via ‹relpow_add›:
        ‹rel ^^ 8 O rel ^^ m_rec = rel ^^ (8 + m_rec)›.›
    have chain_compose:
        "(c', c'') ∈ (mttm_step (alphabet_enlarge_delta M))^^(8 + m_rec)"
      using chain8 chain_rec by (auto simp: relpow_add)
    ― ‹Substep K: arithmetic bound ‹8 + m_rec ≤ 8 ⋅ ⌈n/c⌉›.
        Case-split mirroring substep E's:
          - ‹k_chunk = n›: ‹n - k_chunk = 0› so ‹m_rec = 0›
            (IH base case yields zero-bound on a zero-length
            trace); and ‹n ≥ 1› gives ‹⌈n/c⌉ ≥ 1›, so the
            target ‹8 ≤ 8 ⋅ 1› holds.
          - ‹k_chunk \<ne> n›: substep E forces ‹k_chunk = c›
            (and ‹c < n›); the IH bound becomes
            ‹m_rec ≤ 8 ⋅ ⌈(n-1)/c⌉›, and the identity
            ‹⌈n/c⌉ = ⌈(n-1)/c⌉ + 1› (which holds for
            ‹n ≥ 1, c ≥ 1›) gives the target with equality.›
    have n_pos: "0 < n" using Suc by simp
    have bound_compose:
        "8 + m_rec
          ≤ 8 * ((n + card (UNIV :: 'c set) - 1)
                    div card (UNIV :: 'c set))"
    proof (cases "k_chunk = n")
      case True
      have m_rec_zero: "m_rec = 0"
      proof -
        have "n - k_chunk = 0" using True by simp
        hence "(n - k_chunk + card (UNIV :: 'c set) - 1)
                  div card (UNIV :: 'c set) = 0"
          using c_pos[unfolded c_def] by simp
        thus ?thesis using bound_rec by simp
      qed
      have one_le_ceil:
          "1 ≤ (n + card (UNIV :: 'c set) - 1)
                  div card (UNIV :: 'c set)"
      proof -
        have "card (UNIV :: 'c set) ≤ n + card (UNIV :: 'c set) - 1"
          using n_pos by simp
        hence "card (UNIV :: 'c set) div card (UNIV :: 'c set)
                ≤ (n + card (UNIV :: 'c set) - 1)
                    div card (UNIV :: 'c set)"
          using div_le_mono by blast
        thus ?thesis using c_pos[unfolded c_def] by simp
      qed
      show ?thesis using m_rec_zero one_le_ceil by simp
    next
      case False
      have k_chunk_eq_c: "k_chunk = c"
      proof -
        have "k_chunk < n" using k_chunk_le_n False by linarith
        hence "min n c < n" unfolding k_chunk_def by simp
        hence "c < n" by linarith
        hence "min n c = c" by simp
        thus ?thesis unfolding k_chunk_def by simp
      qed
      have n_gt_c: "c < n"
        using False k_chunk_le_n k_chunk_eq_c by linarith
      have n_minus_eq: "n - k_chunk + c - 1 = n - 1"
        using k_chunk_eq_c n_gt_c by simp
      have rec_bound:
          "m_rec ≤ 8 * ((n - 1) div card (UNIV :: 'c set))"
        using bound_rec n_minus_eq unfolding c_def by simp
      have ceil_step:
          "(n + card (UNIV :: 'c set) - 1)
              div card (UNIV :: 'c set)
            = (n - 1) div card (UNIV :: 'c set) + 1"
      proof -
        have c_nz: "card (UNIV :: 'c set) ≠ 0"
          using c_pos unfolding c_def by simp
        have sum_eq: "n + card (UNIV :: 'c set) - 1
                       = (n - 1) + card (UNIV :: 'c set)"
          using n_pos by simp
        have div_step:
            "((n - 1) + card (UNIV :: 'c set))
                div card (UNIV :: 'c set)
              = (n - 1) div card (UNIV :: 'c set) + 1"
          using div_add_self2[OF c_nz] .
        show ?thesis using sum_eq div_step by simp
      qed
      have "8 + m_rec
              ≤ 8 + 8 * ((n - 1) div card (UNIV :: 'c set))"
        using rec_bound by simp
      also have "… = 8 * ((n - 1) div card (UNIV :: 'c set) + 1)"
        by simp
      also have "… = 8 * ((n + card (UNIV :: 'c set) - 1)
                            div card (UNIV :: 'c set))"
        using ceil_step by simp
      finally show ?thesis .
    qed
    ― ‹Final assembly: witnesses ‹(8 + m_rec, c'')› satisfy
        the bound ‹(8 + m_rec) ≤ 8 ⋅ ⌈n/c⌉›, the chain
        ‹(c', c'') ∈ alphabet_enlarge_delta^^(8 + m_rec)›, and
        the canonical halt state ‹(t_tm M, init_stage le_M)›.›
    show ?thesis
      using bound_compose chain_compose state_c'' by blast
  qed
qed

text ‹Simulation-phase step count under weak acceptance.  If
  ‹M› accepts ‹u› within time ‹T (length u)› (an accepting
  ‹M›-path of length at most ‹T (length u)› from
  ‹init_config_mttm M u› to a config in state ‹t_tm M›),
  then from any simulation-paired SS1 config ‹c'› there is an
  accepting ‹M'›-path of length at most ‹8 * ⌈T(length u) / c⌉›
  ending at ‹(t_tm M, init_stage (le_tm M))›.

  Under the weak time-bounded acceptance convention
  (‹accepts_in_time_mttm›).  Hypothesis
  ‹accepts_in_time_mttm M u (T (length u))› replaces the
  universal-path-bound ‹upperb_time_mttm M T›; conclusion drops
  the ‹r_tm›-arm (under weak acceptance, "reject" just means
  "no accepting path"; no canonical ‹r_tm› config is tracked
  explicitly).  Thin
  wrapper around ‹ae_simulation_phase_chunked›: unpacks
  the weak-acceptance witness, lifts the tight bound
  ‹(n0 + c - 1) div c› to the ‹T (length u)› bound
  via monotonicity of division, and adapts to the
  ‹obtains›-form.›

lemma ae_simulation_phase_step_count:
  fixes M :: "('q, 'a) mttm"
    and T :: "nat ⇒ nat"
    and u :: "'a list"
    and c' :: "('c :: enum ⇒ 'a,
                'q × ('a, 'c) ae_stage) mt_config"
  assumes vM:         "valid_mttm M"
      and lu:         "le_unique M"
      and m_accepts:  "accepts_in_time_mttm M u (T (length u))"
      and u_sub:      "set u ⊆ Sigma_tm M"
      and sim:        "ae_simulates M (init_config_mttm M u) c'"
      and buf_gamma_c': "ae_buffer_in_gamma_block M c'"
      and le_anchor_c': "∀kk<k_tm M. mt_tape c' kk 0 = LE_block (le_tm M)"
      and s_neq_t:    "s_tm M ≠ t_tm M"
      and s_neq_r:    "s_tm M ≠ r_tm M"
      and le_neq_bl:  "le_tm M ≠ bl_tm M"
  obtains n_steps :: nat and c'' where
      "n_steps ≤ 8 * ((T (length u) + card (UNIV :: 'c set) - 1)
                       div card (UNIV :: 'c set))"
    and "(c', c'') ∈ mttm_step (alphabet_enlarge_delta M) ^^ n_steps"
    and "mt_state c'' = (t_tm M, init_stage (le_tm M))"
proof -
  ― ‹Step 1: unpack the weak-acceptance witness — the specific
      accepting ‹M›-path of length ‹n0 ≤ T (length u)›
      from ‹init_config_mttm M u› to a config in state ‹t_tm M›.›
  from m_accepts obtain n0 cM_n0 where
      n0_bd:  "n0 ≤ T (length u)"
    and n0_run: "(init_config_mttm M u, cM_n0)
                    ∈ mttm_step (delta_tm M) ^^ n0"
    and n0_acc: "mt_state cM_n0 = t_tm M"
    unfolding accepts_in_time_mttm_def by blast
  ― ‹Step 2: invoke the chunked-induction helper.  Reachability
      of the starting M-config (‹init_config_mttm M u›) from
      itself is reflexive.  The helper returns an M'-witness path
      with the tight bound ‹8 ⋅ ⌈n0/c⌉›; the wrapper relaxes
      this to ‹8 ⋅ ⌈T(|u|)/c⌉› via monotonicity of
      ‹(_ + c - 1) div c› in the dividend.›
  have init_reach:
      "(init_config_mttm M u, init_config_mttm M u)
          ∈ (mttm_step (delta_tm M))⇧*"
    by simp
  obtain n_steps c'' where
      tight_bound: "n_steps ≤ 8 * ((n0 + card (UNIV :: 'c set) - 1)
                                       div card (UNIV :: 'c set))"
    and run:   "(c', c'') ∈ mttm_step (alphabet_enlarge_delta M) ^^ n_steps"
    and halt:  "mt_state c'' = (t_tm M, init_stage (le_tm M))"
    using ae_simulation_phase_chunked[OF vM lu u_sub le_neq_bl s_neq_t s_neq_r
                                          init_reach n0_run n0_acc sim
                                          buf_gamma_c' le_anchor_c']
    by blast
  ― ‹Step 3: arithmetic — relax the tight ‹n0›-bound to the
      loose ‹T(|u|)›-bound using ‹n0 ≤ T (length u)› and
      monotonicity of ‹div› on the dividend.›
  have div_mono:
      "(n0 + card (UNIV :: 'c set) - 1) div card (UNIV :: 'c set)
         ≤ (T (length u) + card (UNIV :: 'c set) - 1)
              div card (UNIV :: 'c set)"
    using n0_bd by (intro div_le_mono add_le_mono) auto
  have loose_bound:
      "n_steps ≤ 8 * ((T (length u) + card (UNIV :: 'c set) - 1)
                       div card (UNIV :: 'c set))"
    using tight_bound div_mono by linarith
  show ?thesis
  proof (rule that)
    show "n_steps ≤ 8 * ((T (length u) + card (UNIV :: 'c set) - 1)
                            div card (UNIV :: 'c set))"
      using loose_bound .
    show "(c', c'') ∈ mttm_step (alphabet_enlarge_delta M) ^^ n_steps"
      using run .
    show "mt_state c'' = (t_tm M, init_stage (le_tm M))"
      using halt .
  qed
qed

end