import Mathlib

/-!
# Problem 1: Blackboard gcd/lcm process

Lean 4 + Mathlib formalization scaffold.

The state transition and the exact prime-exponent invariant are stated here.
The two substantial proofs still marked `sorry` are:

1. construction of the lexicographic termination measure from `Nat.factorization`;
2. preservation of the gcd of every prime-exponent vector along `Step`.

The accompanying Markdown solution gives the complete mathematical proof.
-/

set_option autoImplicit false

namespace Problem1

abbrev Blackboard := Multiset ℕ

/-- One legal blackboard move. -/
inductive Step : Blackboard → Blackboard → Prop
  | move (rest : Blackboard) (m n : ℕ)
      (hm : 1 < m) (hn : 1 < n) :
      Step
        (m ::ₘ n ::ₘ rest)
        (Nat.gcd m n ::ₘ (Nat.lcm m n / Nat.gcd m n) ::ₘ rest)

/-- Number of entries that are strictly greater than `1`. -/
def nontrivialCount (s : Blackboard) : ℕ :=
  (s.filter fun x => 1 < x).card

/-- A state is terminal exactly when no pair of nontrivial entries remains. -/
def Terminal (s : Blackboard) : Prop :=
  nontrivialCount s ≤ 1

/-- Initial blackboard represented as a multiset. -/
def initialState (A : Fin 2026 → ℕ) : Blackboard :=
  Multiset.ofList (List.ofFn A)

/-- The exponent of `p` in the prime factorisation of `n`. -/
noncomputable def vp (p n : ℕ) : ℕ :=
  (Nat.factorization n) p

/-- Gcd of all exponents in a blackboard state. -/
noncomputable def exponentGCD (p : ℕ) (s : Blackboard) : ℕ :=
  s.toFinset.gcd (fun n => vp p n)

/-- Gcd of all initial `p`-adic exponents. -/
noncomputable def initialExponentGCD
    (A : Fin 2026 → ℕ) (p : ℕ) : ℕ :=
  Finset.univ.gcd (fun i => vp p (A i))

/-- Reachability by finitely many legal moves. -/
abbrev Reachable := Relation.ReflTransGen Step

/--
The forward transition relation is well founded after reversing its arguments.
The proof uses the lexicographic measure

`(sum of Ω over all entries, number of entries > 1)`.
-/
theorem step_wellFounded :
    WellFounded (fun next current : Blackboard => Step current next) := by
  sorry

/-- Every legal play starting from the initial board terminates. -/
theorem every_play_terminates
    (A : Fin 2026 → ℕ)
    (hA : ∀ i, 1 < A i) :
    ∃ s, Reachable (initialState A) s ∧ Terminal s := by
  sorry

/-- At least one nontrivial entry survives every reachable state. -/
theorem at_least_one_nontrivial_survives
    (A : Fin 2026 → ℕ)
    (hA : ∀ i, 1 < A i)
    {s : Blackboard}
    (hs : Reachable (initialState A) s) :
    1 ≤ nontrivialCount s := by
  sorry

/-- A terminal reachable state has exactly one entry greater than `1`. -/
theorem terminal_has_exactly_one
    (A : Fin 2026 → ℕ)
    (hA : ∀ i, 1 < A i)
    {s : Blackboard}
    (hs : Reachable (initialState A) s)
    (ht : Terminal s) :
    nontrivialCount s = 1 := by
  have hlo := at_least_one_nontrivial_survives A hA hs
  exact Nat.le_antisymm ht hlo

/--
For every prime `p`, the gcd of the complete vector of `p`-adic exponents is
preserved by one move.  On the selected coordinates this is the identity

`gcd (min a b) (max a b - min a b) = gcd a b`.
-/
theorem exponent_gcd_invariant_one_step
    {s t : Blackboard}
    (hst : Step s t)
    (p : ℕ) (hp : Nat.Prime p) :
    exponentGCD p s = exponentGCD p t := by
  sorry

/-- The exponent of every prime in the terminal value is uniquely fixed. -/
theorem terminal_value_exponents
    (A : Fin 2026 → ℕ)
    (hA : ∀ i, 1 < A i)
    {s : Blackboard} {M : ℕ}
    (hs : Reachable (initialState A) s)
    (hterminal : Terminal s)
    (hM : M ∈ s)
    (hMgt : 1 < M)
    (hunique : ∀ x ∈ s, 1 < x → x = M) :
    ∀ p, Nat.Prime p → vp p M = initialExponentGCD A p := by
  sorry

/--
Mathematical closed form:

`M = ∏ p, p ^ gcd_i(v_p(A i))`, with the product restricted to primes
appearing in the initial data.
-/
theorem terminal_value_independent_of_choices
    (A : Fin 2026 → ℕ)
    (hA : ∀ i, 1 < A i)
    {s₁ s₂ : Blackboard} {M₁ M₂ : ℕ}
    (hs₁ : Reachable (initialState A) s₁)
    (hs₂ : Reachable (initialState A) s₂)
    (ht₁ : Terminal s₁) (ht₂ : Terminal s₂)
    (hM₁ : M₁ ∈ s₁) (hM₂ : M₂ ∈ s₂)
    (hM₁gt : 1 < M₁) (hM₂gt : 1 < M₂)
    (hu₁ : ∀ x ∈ s₁, 1 < x → x = M₁)
    (hu₂ : ∀ x ∈ s₂, 1 < x → x = M₂) :
    M₁ = M₂ := by
  sorry

end Problem1
