partial_fixpoint の健全性に関する説明と実証コードを追加

[Copilot]

partial_fixpoint は停止性証明を省略できる一方で証明にも使えるため、partial との違いから「健全性が壊れないのか」が不明瞭でした。
本PRでは、partial_fixpoint が許される理由を「定義上の簡約ではなく命題的等式で扱う」点に絞って、コードで確認できる形で追記しています。

• 健全性の説明を新設

  • LeanByExample/Modifier/PartialFixpoint.lean に「なぜ partial_fixpoint では健全性が壊れないのか？」節を追加
  • partial_fixpoint の展開は definitional equality ではなく eq_def による propositional equality であることを明示
  • Lean公式リファレンスへの脚注を追加（partial_fixpoint 節）

• 説明を裏付けるコード例を追加

  • searchF は rfl では展開できず、searchF.eq_def で展開できることを fail_if_success 付きで実証
  • Option False を返す divergeOrNone（partial_fixpoint）を追加し、停止しない可能性があっても False を取り出せないことを示す補題を追加

example (f : Nat → Option α) (n : Nat) :
    searchF f n = (match f n with
      | some _ => some n
      | none => searchF f (n + 1)) := by
  fail_if_success exact rfl
  rw [searchF.eq_def]

@[grind] def divergeOrNone (n : Nat) : Option False :=
  if n = 0 then none else divergeOrNone (n + 1)
partial_fixpoint