putnam_2023_a6: fix vacuous strategy-validity condition (Lean) and free-variable typo (Isabelle)

[AaronY77]

Fixes #365.

• Lean: IsValidStrategy s ↔ ∀ g, g.length > 0 → s g ∈ g forces Bob to repeat a chosen number, so no legal game of length ≥ 2 conforms and every valid strategy wins vacuously. The new condition requires, on every legal unfinished history, an unused number in 1..n:

  (IsValidStrategy : ℕ → (List ℕ → ℕ) → Prop)
  (IsValidStrategy_def : ∀ n s, IsValidStrategy n s ↔
    ∀ g : List ℕ, g.Nodup → (∀ i ∈ g, i ∈ Icc 1 n) → g.length < n →
      s g ∈ Icc 1 n ∧ s g ∉ g)

  and IsWinningFor_def uses IsValidStrategy n s. Range and freshness are both needed (missing range was the Fix misformalizations #285 exploit). The statement elaborates on Lean v4.35.0 + current Mathlib; we have not proved the fixed theorem.
• Isabelle: IsValidGame G → IsValidGame g in IsValidGame_def (the free G made the assumptions contradictory). The Isabelle version still has no strategy-validity condition (see putnam_2023_a6 (Lean, Isabelle): statement is vacuous — "valid strategy" requires Bob to pick an already-chosen number #365); not changed here because we could not machine-check an Isabelle edit.