`Compfiles/Usa2016P4.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

15 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2016 P4

Find all functions f : ℝ → ℝ such that for all x, y ∈ ℝ: (f(x)+xy) · f(x-3y) + (f(y)+xy) · f(3x-y) = (f(x+y))^2

Imports (3)

Imported by 1 file

Compfiles.lean

def Usa2016P4.f_good line 26 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: Eq, HAdd.hAdd, HMul.hMul, HSub.hSub, OfNat.ofNat, HPow.hPow, Nat
14 instances, coercions and auxiliary constants left out.
theorem Usa2016P4.f_zero line 33 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Usa2016P4.f_good, Eq, OfNat.ofNat
Proof uses: Eq.mp, HPow.hPow, Nat, congrArg, propext, sq_eq_zero_iff, eq_zero_of_mul_eq_self_left, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Nat.cast_one, Bool, Bool.false, HAdd.hAdd, HMul.hMul, Eq.symm, two_mul, pow_two, HSub.hSub and 6 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem Usa2016P4.f_t_even line 40 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Usa2016P4.f_good, Ne, OfNat.ofNat, Eq, Neg.neg
Proof uses: Or, Eq.mp, HMul.hMul, congrArg, propext, mul_eq_mul_left_iff, HPow.hPow, Nat, pow_two, HAdd.hAdd, HSub.hSub, congr, Eq.trans, MulZeroClass.zero_mul, add_zero, zero_sub, congrFun', MulZeroClass.mul_zero, zero_add, Usa2016P4.f_zero and 2 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma Usa2016P4.f_even_zero line 55 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Usa2016P4.f_good, Eq, OfNat.ofNat, Neg.neg
Proof uses: Or, Eq.mp, HMul.hMul, congrArg, propext, mul_eq_mul_left_iff, HPow.hPow, Nat, pow_two, HAdd.hAdd, HSub.hSub, congr, Eq.trans, mul_neg, MulZeroClass.zero_mul, neg_zero, add_zero, sub_neg_eq_add, zero_add, congrFun' and 5 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
theorem Usa2016P4.f_even line 71 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Usa2016P4.f_good, Eq, Neg.neg
Proof uses: dite, OfNat.ofNat, Usa2016P4.f_even_zero, Eq.mpr, id, congrArg, Eq.refl, Not, Usa2016P4.f_t_even
5 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem Usa2016P4.f_half_zero line 78 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Usa2016P4.f_good, Eq, OfNat.ofNat, HDiv.hDiv, Nat
Proof uses: eq_zero_of_pow_eq_zero, Eq.symm, HPow.hPow, Eq.mp, HMul.hMul, Inv.inv, congrArg, div_eq_mul_inv, HAdd.hAdd, congr, Eq.trans, congrFun', one_div, MulZeroClass.mul_zero, add_mul, mul_rotate, Nat.rawCast, NNRat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.add_congr and 79 more
100 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma Usa2016P4.eq_2 line 95 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Usa2016P4.f_good, Or, Eq, HSub.hSub, HAdd.hAdd, Neg.neg, HMul.hMul, OfNat.ofNat, Nat, HPow.hPow
Proof uses: Eq.mpr, id, congrArg, Eq.symm, mul_sub_right_distrib, add_mul, of_eq_true, Eq.trans, True, congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl and 68 more
103 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
theorem Usa2016P4.hf_opts line 110 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Usa2016P4.f_good, Or, Eq, HPow.hPow, Nat, OfNat.ofNat
Proof uses: HSub.hSub, HAdd.hAdd, Neg.neg, HMul.hMul, Usa2016P4.eq_2, dite, Or.inr, Not, Or.inl, Eq.mp, congrArg, propext, sub_eq_zero, Eq.trans, False, congrFun', false_or, Eq.symm, mul_sub, two_mul and 43 more
97 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
lemma Usa2016P4.eq_3 line 134 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Usa2016P4.f_good, Eq, HMul.hMul, HAdd.hAdd, OfNat.ofNat, Nat, HPow.hPow
Proof uses: Eq.mp, congrArg, add_comm, Eq.symm, add_mul, mul_rotate, congrFun', Eq.trans, congr, MulZeroClass.mul_zero, MulZeroClass.zero_mul, zero_add, add_zero, Usa2016P4.f_zero, HSub.hSub, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf', Mathlib.Tactic.Ring.cast_pos and 57 more
73 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
theorem Usa2016P4.f_two_zero line 144 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Usa2016P4.f_good, Eq, OfNat.ofNat, HMul.hMul, Nat
Proof uses: HAdd.hAdd, HPow.hPow, Usa2016P4.eq_3, Or, Eq.mp, Eq.trans, congrArg, congrFun', zero_pow, of_eq_true, Not, False, True, not_false_eq_true, implies_congr, eq_true, Eq.refl, dite, Eq.mpr, id and 44 more
92 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
theorem Usa2016P4.f_ge_zero line 174 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Usa2016P4.f_good, GE.ge, OfNat.ofNat
Proof uses: Or, Eq, HPow.hPow, Nat, Usa2016P4.hf_opts, Eq.mpr, id, congrArg, sq_nonneg, le_refl
29 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem Usa2016P4.ha_zero if a ≠ 0 and f a = 0 then wlog a > 0 line 184 source
Source comment
if a ≠ 0 and f a = 0 then wlog a > 0

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Usa2016P4.f_good, Iff, Exists, And, Ne, OfNat.ofNat, Eq, GT.gt
Proof uses: Iff.intro, Neg.neg, Usa2016P4.f_even_zero, dite, Exists.intro, And.intro, Not, LT.lt, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul, HPow.hPow, Nat and 42 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
```
theorem ha_zero (f: ℝ→ℝ) (hf : f_good f) :
    ∀(_:ℝ), ((∃a, a ≠ 0 ∧ f a = 0)↔ ∃ a > 0, f a = 0) := by
…
```
Mentions: f, Usa2016P4.f_good
theorem Usa2016P4.f_eq_zero_if_not_sq The main part, proving that if there is some nonzero a such that f a = 0 then we must have f b = 0 for all b line 210 source
Source comment
The main part, proving that if there is some nonzero a such that f a = 0 then we must have f b = 0 for all b

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Usa2016P4.f_good, Exists, And, Ne, OfNat.ofNat, Eq
Proof uses: dite, Eq.mpr, id, congrArg, Usa2016P4.f_zero, Not, LT.lt, Or, Classical.em, Iff, GT.gt, Usa2016P4.ha_zero, Eq.mp, propext, HDiv.hDiv, div_pos, HMul.hMul, Nat, HPow.hPow, Int and 209 more
184 instances, coercions and auxiliary constants left out.

Tactic trace: 135 steps
Open to load the checked before-and-after goal states.
```
theorem f_eq_zero_if_not_sq (f: ℝ→ℝ) (hf : f_good f) :
    ∀(b:ℝ),(∃a, a≠0 ∧ f a = 0) → f b = 0 := by
…
```
Mentions: f, Usa2016P4.f_good
determine Usa2016P4.solution_set line 338 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Real
Proof uses: Insert.insert, OfNat.ofNat, Singleton.singleton, HPow.hPow, Nat
9 instances, coercions and auxiliary constants left out.
problem Usa2016P4.usa2016_p4 line 340 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Iff, Membership.mem, Set, Usa2016P4.solution_set, Usa2016P4.f_good
Proof uses: Iff.intro, Eq, OfNat.ofNat, Singleton.singleton, HPow.hPow, Nat, HAdd.hAdd, HMul.hMul, HSub.hSub, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', zero_add, MulZeroClass.mul_zero, add_zero, zero_pow, Not and 131 more
123 instances, coercions and auxiliary constants left out.

Tactic trace: 52 steps
Open to load the checked before-and-after goal states.