E206:Erdős Problem #206 “Can one give an explicit irrational whose best Egyptian underapproximations are not eventually greedy?”

import Erdos206Explicit

/-!
Submission wrapper for Jig's canonical statement. The existential witnesses are
the concrete real and executable rational approximation function defined in
`StageRecurrence.lean`; they are not chosen nonconstructively here.
-/

namespace Submissions.Erdos206ExplicitWitness.Coleski

open scoped BigOperators

noncomputable def egyptianSum (S : Finset ℕ) : ℝ :=
  S.sum (fun m => (1 : ℝ) / m)

def ValidEgyptian (S : Finset ℕ) : Prop :=

import StageRecurrence

/-!
# Explicit-example supplement to Erdős #206

This is not a new proof of Kovač's almost-everywhere theorem. The specified
number `ExplicitEgyptian.explicitNumber` is the limit of the concrete executable
rational recurrence in StageRecurrence.lean. The final statement includes its
positive irrationality, failure of eventual greediness under the original
strict/distinct-denominator convention, and a certified approximation modulus.
-/

namespace ExplicitEgyptian

theorem erdos206_explicit_resolution :
    (1/4:ℝ) < explicitNumber ∧ explicitNumber < 1/2 ∧

import RationalOptimizer
import Density
import StepBounds
import NestedIntervals

namespace ExplicitEgyptian

open Erdos206 Erdos206.EgyptianFractions

/-- All data fields are rational or natural; invariant fields are erased proofs. -/
structure IntervalState where
  lower : ℚ
  upper : ℚ
  level : ℕ
  quarter_le : 1/4 ≤ lower
  lower_lt_upper : lower < upper

import PriorErdos206

namespace ExplicitEgyptian

def qsum (S : Finset ℕ) : ℚ := ∑ a ∈ S, 1 / (a : ℚ)

def base (n L : ℕ) (z : ℚ) : Finset ℕ :=
  (Finset.range n).image (fun k => L + ⌈(n : ℚ) / z⌉₊ + k + 1)

theorem base_card (n L : ℕ) (z : ℚ) : (base n L z).card = n := by
  unfold base
  rw [Finset.card_image_of_injective _ (by
    intro a b h; dsimp at h; omega : Function.Injective (fun k => L + ⌈(n : ℚ) / z⌉₊ + k + 1))]
  exact Finset.card_range n

theorem base_above (n L : ℕ) (z : ℚ) : ∀ a ∈ base n L z, L < a := by

import PriorErdos206

namespace ExplicitEgyptian

open Erdos206.EgyptianFractions

theorem best_sum_above_of_bound (L z : ℝ) (hL : 0 < L) (hLz : L < z)
    (hz : z < 1) (t : ℕ) (ht : 2 ≤ t)
    (hbound : 1 / (z - L) < (t : ℝ))
    (S : Finset ℕ) (hS : IsBestNTerm S t z) :
    L < egyptianSum S := by
  have htpos : (0 : ℝ) < t := by exact_mod_cast (show 0 < t by omega)
  have hdelta : 0 < z - L := sub_pos.mpr hLz
  have h1 : harmonicNumber 1 = 1 := by norm_num [harmonicNumber]
  have hH : 1 ≤ harmonicNumber t := by
    rw [← h1]

import LocalObstruction

/-! Executable rational interval updates for the #206 explicit-example supplement. -/

namespace Erdos206.EgyptianFractions

def badLowerQ (i : ℕ) : ℚ :=
  1 / (i+1:ℕ) + 1 / (i*(i+1)/2+1:ℕ)

def badUpperQ (i : ℕ) : ℚ :=
  1 / (i:ℚ) + 1 / (i*(i+1)+4:ℕ)

@[simp] theorem badLowerQ_cast (i : ℕ) : (badLowerQ i : ℝ) = badLower i := by
  simp [badLowerQ, badLower]

@[simp] theorem badUpperQ_cast (i : ℕ) : (badUpperQ i : ℝ) = badUpper i := by

import Mathlib

namespace Erdos206

open Set Filter

/-- Rational stage data only; computation of these sequences belongs to the recurrence. -/
structure RationalNestedData where
  lower : ℕ → ℚ
  upper : ℕ → ℚ
  approx : ℕ → ℚ
  lower_le_upper : ∀ n, lower n ≤ upper n
  lower_mono : Monotone lower
  upper_anti : Antitone upper
  width_le : ∀ n, (upper n - lower n : ℚ) ≤ (1 / 2 : ℚ) ^ n
  approx_lt_lower : ∀ n, approx n < lower n

/- leanprover/lean4:v4.33.0  mathlib v4.33.0 -/
/- Original license: Apache 2.0. Note: This file has been modified. -/
/-
This is a Lean formalization of a solution to Erdős Problem 206.
https://www.erdosproblems.com/forum/thread/206

Informal authors:
- Vjekoslav Kovač

Formal authors:
- Aristotle
- Matteo Del Vecchio

URLs:
- https://www.erdosproblems.com/forum/thread/206#post-5989
- https://gist.githubusercontent.com/madeve-unipi/0920783513a1a00af4a14660852df60e/raw/522569070c2ec

import PriorErdos206

/-!
Local obstruction for the explicit-example supplement to Erdős #206.
Uses the definitions and the competitor lemma formalized by Matteo Del Vecchio
and Aristotle for Vjekoslav Kovač's proof; see PriorErdos206.lean for credits.
-/

namespace Erdos206.EgyptianFractions

open Finset

lemma prefix_sum_succ (m : ℕ → ℕ) (hm : StrictMono m) (t : ℕ) :
    egyptianSum (image m (range (t+1))) =
      egyptianSum (image m (range t)) + 1 / (m t : ℝ) := by
  simp [egyptianSum, Finset.sum_image, hm.injective.eq_iff, Finset.sum_range_succ]