一些随意普通的闲聊 » 讨论
一些中欧和东欧国家的中学数学竞赛题

import Mathlib.Data.Rat.Defs

import Mathlib.Data.Rat.Lemmas

import Mathlib.Tactic



/-- 

对于任意正有理数 q，均可表示为 (a^2 + b^3) / (c^5 + d^7) 的形式，

其中 a, b, c, d 均为正整数。

-/

theorem rational_sum_powers_representation (q : ℚ) (hq : 0 < q) :

  ∃ a b c d : ℕ,

    0 < a ∧ 0 < b ∧ 0 < c ∧ 0 < d ∧

    q = (a^2 + b^3 : ℚ) / (c^5 + d^7 : ℚ) := by

  -- =========================

  -- 1. 准备工作：提取分子分母

  -- =========================

  let m : ℕ := q.num.natAbs

  let n : ℕ := q.den



  -- 证明 m 和 n 均为正数 (因为 q > 0)

  have hm : 0 < m := Int.natAbs_pos.mpr (Rat.num_pos.mpr hq).ne'

  have hn : 0 < n := q.den_pos



  -- =========================

  -- 2. 构造解 (Witnesses)

  -- =========================

  /- 

    数学构造思路:

    我们需要 (a^2 + b^3) / (c^5 + d^7) = m / n

    

    策略:

    1. 令 a = k^3, b = k^2，则 a^2 + b^3 = k^6 + k^6 = 2 * k^6

    2. 令 c = l^7, d = l^5，则 c^5 + d^7 = l^35 + l^35 = 2 * l^35

    3. 此时分式变为 (2 * k^6) / (2 * l^35) = k^6 / l^35

    4. 我们需要 k^6 / l^35 = m / n

    

    凑指数:

    取 k = m^6 * n^29

    取 l = m^1 * n^5

    

    验证:

    k^6  = m^36 * n^174

    l^35 = m^35 * n^175

    k^6 / l^35 = (m^36 * n^174) / (m^35 * n^175) = m / n  (成立)

  -/

  let k := m^6 * n^29

  let l := m^1 * n^5

  let a := k^3

  let b := k^2

  let c := l^7

  let d := l^5



  -- 证明构造出的数均为正数

  have hk : 0 < k := by dsimp [k]; positivity

  have hl : 0 < l := by dsimp [l]; positivity

  have ha : 0 < a := by dsimp [a]; positivity

  have hb : 0 < b := by dsimp [b]; positivity

  have hc : 0 < c := by dsimp [c]; positivity

  have hd : 0 < d := by dsimp [d]; positivity



  -- 提供解

  use a, b, c, d

  refine ⟨ha, hb, hc, hd, ?_⟩



  -- =========================

  -- 3. 证明核心等式

  -- =========================

  

  -- 步骤 A: 将 q 转化为 m/n 的形式

  have hq_eq : q = (m : ℚ) / (n : ℚ) := by

    -- 证明 q.num 等于整数 m

    have h_num : q.num = (m : ℤ) := by

      dsimp [m] -- 展开 m 的定义以便访问 natAbs 结构

      rw [← Int.abs_eq_natAbs] -- 使用 |z| = natAbs z

      rw [abs_of_pos (Rat.num_pos.mpr hq)] -- 因为 q>0，所以 |num| = num



    -- 在 q 处重写定义 (q = num/den)

    nth_rw 1 [← Rat.num_div_den q]

    rw [h_num]

    rfl



  rw [hq_eq]



  -- 步骤 B: 消除分母，转化为乘法等式

  -- 证明构造的分母不为 0 (除法有意义的前提)

  have h_denom_ne_zero : (c : ℚ)^5 + (d : ℚ)^7 ≠ 0 := by

    norm_cast -- 将有理数不等式转化为自然数不等式

    positivity



  -- 应用定理: a/b = c/d ↔ a*d = b*c

  -- 需要保证两个分母 (n 和 c^5+d^7) 均不为 0

  rw [div_eq_div_iff (by exact_mod_cast hn.ne') h_denom_ne_zero]



  -- 步骤 C: 纯代数计算

  -- 1. 展开所有 let 定义

  dsimp [a, b, c, d, k, l]

  -- 2. norm_cast: 将所有有理数(ℚ)运算强制转换为自然数(ℕ)运算

  --    这是最关键的一步，使得问题变成了纯粹的自然数多项式验证

  norm_cast

  -- 3. ring: 自动验证环上的代数恒等式

  ring