`Compfiles/Imo2026P5.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 3305 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

18 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2026, Problem 5

Let ℝ_{>0} be the set of positive real numbers. Determine all functions f : ℝ_{>0} → ℝ_{>0} such that

√((x² + f(y)²)/2) ≥ (f(x) + y)/2 ≥ √(x·f(y))

for every x, y ∈ ℝ_{>0}.

Statement formalization adapted from AxiomMath/IMO2026; proof adapted from Humanfia's Kimi-K3 solutions (https://github.com/humanfia/imo2026).

Imports (4)

Imported by 1 file

Compfiles.lean

abbrev Imo2026P5.PositiveReal The subtype of positive real numbers, representing \mathbb{R}_{>0} line 39 source
Source documentation
The subtype of positive real numbers, representing \mathbb{R}_{>0}.

standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: Subtype, Real, LT.lt, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
```
abbrev PositiveReal : Type := {x : ℝ // 0 < x}
```
def Imo2026P5.IsAdmissible The two-sided inequality defining admissible functions on positive real numbers line 42 source
Source documentation
The two-sided inequality defining admissible functions on positive real numbers.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2026P5.PositiveReal
Proof uses: And, LE.le, Real, HDiv.hDiv, HAdd.hAdd, LT.lt, OfNat.ofNat, Real.sqrt, HPow.hPow, Nat, HMul.hMul
20 instances, coercions and auxiliary constants left out.
```
def IsAdmissible (f : PositiveReal → PositiveReal) : Prop :=
…
```
Mentions: f, Imo2026P5.PositiveReal
def Imo2026P5.fdef The defect f x - x of a function on the positive reals line 50 source
Source documentation
The defect f x - x of a function on the positive reals.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2026P5.PositiveReal, Real
Proof uses: HSub.hSub, LT.lt, OfNat.ofNat
6 instances, coercions and auxiliary constants left out.
```
def fdef (f : PositiveReal → PositiveReal) (x : PositiveReal) : ℝ := (f x : ℝ) - (x : ℝ)
```
Mentions: f, Imo2026P5.PositiveReal
lemma Imo2026P5.fdef_eq line 52 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2026P5.PositiveReal, Eq, Real, Imo2026P5.fdef, HSub.hSub, LT.lt, OfNat.ofNat
Proof uses: rfl
6 instances, coercions and auxiliary constants left out.
lemma Imo2026P5.pval line 55 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Eq, Subtype.mk
Proof uses: rfl
8 instances, coercions and auxiliary constants left out.
lemma Imo2026P5.hB Squared form of the right inequality: 4 x f(y) ≤ (f(x) + y)^2 line 58 source
Source documentation
Squared form of the right inequality: 4 x f(y) ≤ (f(x) + y)^2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2026P5.PositiveReal, Imo2026P5.IsAdmissible, LE.le, Real, HMul.hMul, OfNat.ofNat, Nat, LT.lt, HPow.hPow, HAdd.hAdd
Proof uses: le_of_lt, Subtype.property, Real.sqrt, HDiv.hDiv, And.right, pow_le_pow_left₀, Real.sqrt_nonneg, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, Ring and 83 more
107 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma hB (f : PositiveReal → PositiveReal) (h : IsAdmissible f) (x y : PositiveReal) :
    4 * (x : ℝ) * (f y : ℝ) ≤ ((f x : ℝ) + (y : ℝ)) ^ 2 := by
…
```
Mentions: f, Imo2026P5.PositiveReal, h, Imo2026P5.IsAdmissible
lemma Imo2026P5.hA Squared form of the left inequality: (f(x) + y)^2 ≤ 2 (x^2 + f(y)^2) line 68 source
Source documentation
Squared form of the left inequality: (f(x) + y)^2 ≤ 2 (x^2 + f(y)^2).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2026P5.PositiveReal, Imo2026P5.IsAdmissible, LE.le, Real, HPow.hPow, Nat, HAdd.hAdd, LT.lt, OfNat.ofNat, HMul.hMul
Proof uses: le_of_lt, Subtype.property, HDiv.hDiv, Real.sqrt, And.left, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr and 92 more
122 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma hA (f : PositiveReal → PositiveReal) (h : IsAdmissible f) (x y : PositiveReal) :
    ((f x : ℝ) + (y : ℝ)) ^ 2 ≤ 2 * ((x : ℝ) ^ 2 + (f y : ℝ) ^ 2) := by
…
```
Mentions: f, Imo2026P5.PositiveReal, h, Imo2026P5.IsAdmissible
lemma Imo2026P5.fcomp Iterating f twice shifts by the defect: f(f(y)) = 2 f(y) - y line 81 source
Source documentation
Iterating f twice shifts by the defect: f(f(y)) = 2 f(y) - y.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2026P5.PositiveReal, Imo2026P5.IsAdmissible, Eq, Real, LT.lt, OfNat.ofNat, HSub.hSub, HMul.hMul, Nat
Proof uses: Subtype.property, LE.le, HPow.hPow, HAdd.hAdd, Imo2026P5.hB, Imo2026P5.hA, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.mul_congr and 79 more
93 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma fcomp (f : PositiveReal → PositiveReal) (h : IsAdmissible f) (y : PositiveReal) :
    (f (f y) : ℝ) = 2 * (f y : ℝ) - (y : ℝ) := by
…
```
Mentions: f, Imo2026P5.PositiveReal, h, Imo2026P5.IsAdmissible
lemma Imo2026P5.orbit The orbit of f is an arithmetic progression with difference fdef f y line 95 source
Source documentation
The orbit of f is an arithmetic progression with difference fdef f y.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2026P5.PositiveReal, Imo2026P5.IsAdmissible, Nat, Eq, Real, LT.lt, OfNat.ofNat, Nat.iterate, HAdd.hAdd, HMul.hMul, HSub.hSub
Proof uses: And, Nat.recAux, And.intro, Eq.mpr, id, congrArg, Function.iterate_zero_apply, of_eq_true, Eq.trans, True, congrFun', CharP.cast_eq_zero, MulZeroClass.zero_mul, add_zero, eq_self, Function.iterate_one, Nat.cast_one, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast and 53 more
74 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
lemma orbit (f : PositiveReal → PositiveReal) (h : IsAdmissible f) (y : PositiveReal)
    (n : ℕ) :
    (f^[n] y : ℝ) = (y : ℝ) + (n : ℝ) * ((f y : ℝ) - (y : ℝ)) := by
…
```
Mentions: f, Imo2026P5.PositiveReal, h, Imo2026P5.IsAdmissible
lemma Imo2026P5.g_nonneg The defect is nonnegative: f y ≥ y line 123 source
Source documentation
The defect is nonnegative: f y ≥ y.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2026P5.PositiveReal, Imo2026P5.IsAdmissible, LE.le, Real, OfNat.ofNat, HSub.hSub, LT.lt
Proof uses: Decidable.byContradiction, Not, Eq, rfl, Eq.mp, congrArg, Neg.neg, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, HAdd.hAdd, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul, HPow.hPow, Nat, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat and 56 more
85 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma g_nonneg (f : PositiveReal → PositiveReal) (h : IsAdmissible f) (y : PositiveReal) :
    (0 : ℝ) ≤ (f y : ℝ) - (y : ℝ) := by
…
```
Mentions: f, Imo2026P5.PositiveReal, h, Imo2026P5.IsAdmissible
lemma Imo2026P5.cross Cross inequality on orbit points, with p = fdef f b, q = fdef f a line 137 source
Source documentation
Cross inequality on orbit points, with p = fdef f b, q = fdef f a.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2026P5.PositiveReal, Imo2026P5.IsAdmissible, Nat, LE.le, Real, HMul.hMul, OfNat.ofNat, LT.lt, Nat.iterate, HSub.hSub, HPow.hPow
Proof uses: HAdd.hAdd, Imo2026P5.hB, Eq, Eq.symm, Nat.succ, Function.iterate_succ_apply', Imo2026P5.orbit, Eq.mpr, id, congrArg, congr, congrFun', Eq.trans, Nat.cast_add, Nat.cast_one, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Int.rawCast, inferInstance, Ring and 66 more
87 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma cross (f : PositiveReal → PositiveReal) (h : IsAdmissible f) (a b : PositiveReal)
    (m n : ℕ) :
    4 * (f^[m] b : ℝ) * (((f a : ℝ) - (a : ℝ)) - ((f b : ℝ) - (b : ℝ))) ≤
      ((f^[m] b : ℝ) - (f^[n] a : ℝ) - ((f b : ℝ) - (b : ℝ))) ^ 2 := by
…
```
Mentions: f, Imo2026P5.PositiveReal, h, Imo2026P5.IsAdmissible
lemma Imo2026P5.absurd_lt Two positive defect values cannot be strictly ordered line 164 source
Source documentation
Two positive defect values cannot be strictly ordered.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2026P5.PositiveReal, Imo2026P5.IsAdmissible, LT.lt, Real, OfNat.ofNat, HSub.hSub, False
Proof uses: Eq, rfl, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul, HPow.hPow, Nat, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.sub_congr and 149 more
137 instances, coercions and auxiliary constants left out.

Tactic trace: 53 steps
Open to load the checked before-and-after goal states.
```
lemma absurd_lt (f : PositiveReal → PositiveReal) (h : IsAdmissible f) (a b : PositiveReal)
    (ha : (0 : ℝ) < (f a : ℝ) - (a : ℝ)) (hb : (0 : ℝ) < (f b : ℝ) - (b : ℝ))
    (hlt : (f b : ℝ) - (b : ℝ) < (f a : ℝ) - (a : ℝ)) : False := by
…
```
Mentions: f, Imo2026P5.PositiveReal, h, Imo2026P5.IsAdmissible
lemma Imo2026P5.eq_of_pos All positive values of the defect coincide line 217 source
Source documentation
All positive values of the defect coincide.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2026P5.PositiveReal, Imo2026P5.IsAdmissible, LT.lt, Real, OfNat.ofNat, HSub.hSub, Eq
Proof uses: Or, lt_trichotomy, False.elim, Imo2026P5.absurd_lt
17 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma eq_of_pos (f : PositiveReal → PositiveReal) (h : IsAdmissible f) (a b : PositiveReal)
    (ha : (0 : ℝ) < (f a : ℝ) - (a : ℝ)) (hb : (0 : ℝ) < (f b : ℝ) - (b : ℝ)) :
    (f a : ℝ) - (a : ℝ) = (f b : ℝ) - (b : ℝ) := by
…
```
Mentions: f, Imo2026P5.PositiveReal, h, Imo2026P5.IsAdmissible
lemma Imo2026P5.ball Near a zero of the defect, the defect vanishes line 226 source
Source documentation
Near a zero of the defect, the defect vanishes.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2026P5.PositiveReal, Imo2026P5.IsAdmissible, LT.lt, Real, OfNat.ofNat, Imo2026P5.fdef, Or, Eq, abs, HSub.hSub, Real.sqrt, HMul.hMul, Nat
Proof uses: LE.le, Imo2026P5.g_nonneg, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.Common.sub_congr and 86 more
116 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
```
lemma ball (f : PositiveReal → PositiveReal) (h : IsAdmissible f) (a : PositiveReal)
    (ha : (0 : ℝ) < fdef f a)
    (hdval : ∀ x : PositiveReal, fdef f x = 0 ∨ fdef f x = fdef f a)
    (t x : PositiveReal) (ht : fdef f t = 0)
    (hclose : |(x : ℝ) - (t : ℝ)| < Real.sqrt (2 * fdef f a * (t : ℝ))) :
    fdef f x = 0 := by
…
```
Mentions: f, Imo2026P5.PositiveReal, h, Imo2026P5.IsAdmissible, Imo2026P5.fdef
lemma Imo2026P5.ascend Everything strictly above a zero of the defect is a zero line 266 source
Source documentation
Everything strictly above a zero of the defect is a zero.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2026P5.PositiveReal, Imo2026P5.IsAdmissible, LT.lt, Real, OfNat.ofNat, Imo2026P5.fdef, Or, Eq
Proof uses: rfl, Eq.mp, congrArg, Subtype.property, HMul.hMul, Nat, mul_pos, two_pos, HDiv.hDiv, Real.sqrt, Real.sqrt_pos_of_pos, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, HAdd.hAdd, Neg.neg, HSub.hSub, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo and 126 more
120 instances, coercions and auxiliary constants left out.

Tactic trace: 63 steps
Open to load the checked before-and-after goal states.
```
lemma ascend (f : PositiveReal → PositiveReal) (h : IsAdmissible f) (a : PositiveReal)
    (ha : (0 : ℝ) < fdef f a)
    (hdval : ∀ x : PositiveReal, fdef f x = 0 ∨ fdef f x = fdef f a)
    (t : PositiveReal) (ht : fdef f t = 0) (x : PositiveReal) (htx : (t : ℝ) < (x : ℝ)) :
    fdef f x = 0 := by
…
```
Mentions: f, Imo2026P5.PositiveReal, h, Imo2026P5.IsAdmissible, Imo2026P5.fdef
lemma Imo2026P5.zero_contra A zero of the defect cannot coexist with a positive value line 344 source
Source documentation
A zero of the defect cannot coexist with a positive value.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2026P5.PositiveReal, Imo2026P5.IsAdmissible, LT.lt, Real, OfNat.ofNat, Imo2026P5.fdef, Or, Eq, False
Proof uses: rfl, Eq.mp, congrArg, Subtype.property, And, LE.le, HMul.hMul, Nat, Exists, dite, Exists.intro, And.intro, Not, HAdd.hAdd, Nat.floor, HDiv.hDiv, HSub.hSub, div_nonneg, Iff.mpr, sub_nonneg and 136 more
150 instances, coercions and auxiliary constants left out.

Tactic trace: 81 steps
Open to load the checked before-and-after goal states.
```
lemma zero_contra (f : PositiveReal → PositiveReal) (h : IsAdmissible f) (a : PositiveReal)
    (ha : (0 : ℝ) < fdef f a)
    (hdval : ∀ x : PositiveReal, fdef f x = 0 ∨ fdef f x = fdef f a)
    (b : PositiveReal) (hb : fdef f b = 0) : False := by
…
```
Mentions: f, Imo2026P5.PositiveReal, h, Imo2026P5.IsAdmissible, Imo2026P5.fdef
determine Imo2026P5.answer line 430 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Imo2026P5.PositiveReal
Proof uses: Set.ofPred, Exists, Real, And, LE.le, OfNat.ofNat, Eq, LT.lt, HAdd.hAdd
7 instances, coercions and auxiliary constants left out.
problem Imo2026P5.imo2026_p5 The admissible functions are exactly the translations f(x) = x + c with a nonnegative constant c line 436 source
Source documentation
The admissible functions are exactly the translations f(x) = x + c with a nonnegative constant c.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2026P5.PositiveReal, Iff, Imo2026P5.IsAdmissible, Membership.mem, Set, Imo2026P5.answer
Proof uses: id, Iff.intro, Exists, Real, And, LE.le, OfNat.ofNat, Eq, LT.lt, HAdd.hAdd, dite, Imo2026P5.fdef, Classical.propDecidable, Or, HSub.hSub, Imo2026P5.g_nonneg, Eq.mpr, congrArg, Imo2026P5.fdef_eq, eq_or_lt_of_le and 136 more
120 instances, coercions and auxiliary constants left out.

Tactic trace: 74 steps
Open to load the checked before-and-after goal states.
```
problem imo2026_p5 (f : PositiveReal → PositiveReal) :
    IsAdmissible f ↔ f ∈ answer := by
…
```
Mentions: f, Imo2026P5.PositiveReal, Imo2026P5.IsAdmissible, Imo2026P5.answer