IMO 2024 P6
Google DeepMind IMO 2024
IMO 2024 P1IMO 2024 P2IMO 2024 P4IMO 2024 P6
IMO 2024 P6
Let \mathbb{Q} be the set of rational numbers. A function f : \mathbb{Q} \to \mathbb{Q} is called aquaesulian if
the following property holds: for every x, y \in \mathbb{Q},
f(x + f(y)) = f(x) + y \qquad\text{or}\qquad f(f(x) + y) = x + f(y).
Show that there exists an integer c such that for any aquaesulian function f there are at most
c different rational numbers of the form f(r) + f(-r) for some rational number r, and find the
smallest possible value of c.
Solution: c=2
open Polynomial
theorem imo_2024_p6
(IsAquaesulian : (ℚ → ℚ) → Prop)
(IsAquaesulian_def : ∀ f, IsAquaesulian f ↔
∀ x y, f (x + f y) = f x + y ∨ f (f x + y) = x + f y) :
IsLeast {(c : ℤ) | ∀ f, IsAquaesulian f → {(f r + f (-r)) | (r : ℚ)}.Finite ∧
{(f r + f (-r)) | (r : ℚ)}.ncard ≤ c} 2 := by
IsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y⊢ IsLeast
{c | ∀ (f : ℚ → ℚ), IsAquaesulian f → {x | ∃ r, f r + f (-r) = x}.Finite ∧ ↑{x | ∃ r, f r + f (-r) = x}.ncard ≤ c} 2
exists@?_
refine_1IsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y⊢ 2 ∈ {c | ∀ (f : ℚ → ℚ), IsAquaesulian f → {x | ∃ r, f r + f (-r) = x}.Finite ∧ ↑{x | ∃ r, f r + f (-r) = x}.ncard ≤ c}
refine_2IsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y⊢ 2 ∈
lowerBounds
{c | ∀ (f : ℚ → ℚ), IsAquaesulian f → {x | ∃ r, f r + f (-r) = x}.Finite ∧ ↑{x | ∃ r, f r + f (-r) = x}.ncard ≤ c}
·
refine_1IsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y⊢ 2 ∈ {c | ∀ (f : ℚ → ℚ), IsAquaesulian f → {x | ∃ r, f r + f (-r) = x}.Finite ∧ ↑{x | ∃ r, f r + f (-r) = x}.ncard ≤ c} /- Let f be an aquaesulian function with f(0) = 0.
We claim that f(x) + f(-x) takes on at most two distinct values. -/
useλu b=>if j:u 0=0then by_contra λc=>?_ else ?_
refine_1.refine_1IsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yu:ℚ → ℚb:IsAquaesulian uj:u 0 = 0c:¬({x | ∃ r, u r + u (-r) = x}.Finite ∧ ↑{x | ∃ r, u r + u (-r) = x}.ncard ≤ 2)⊢ False
refine_1.refine_2IsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yu:ℚ → ℚb:IsAquaesulian uj:¬u 0 = 0⊢ {x | ∃ r, u r + u (-r) = x}.Finite ∧ ↑{x | ∃ r, u r + u (-r) = x}.ncard ≤ 2
·
refine_1.refine_1IsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yu:ℚ → ℚb:IsAquaesulian uj:u 0 = 0c:¬({x | ∃ r, u r + u (-r) = x}.Finite ∧ ↑{x | ∃ r, u r + u (-r) = x}.ncard ≤ 2)⊢ False -- If f(x) + f(-x) = 0 for all x, we are done.
suffices:({J|∃k,u k+u (-k)= J}) ⊆{0}
refine_1.refine_1IsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yu:ℚ → ℚb:IsAquaesulian uj:u 0 = 0c:¬({x | ∃ r, u r + u (-r) = x}.Finite ∧ ↑{x | ∃ r, u r + u (-r) = x}.ncard ≤ 2)this:{J | ∃ k, u k + u (-k) = J} ⊆ {0}⊢ False
thisIsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yu:ℚ → ℚb:IsAquaesulian uj:u 0 = 0c:¬({x | ∃ r, u r + u (-r) = x}.Finite ∧ ↑{x | ∃ r, u r + u (-r) = x}.ncard ≤ 2)⊢ {J | ∃ k, u k + u (-k) = J} ⊆ {0}
·
refine_1.refine_1IsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yu:ℚ → ℚb:IsAquaesulian uj:u 0 = 0c:¬({x | ∃ r, u r + u (-r) = x}.Finite ∧ ↑{x | ∃ r, u r + u (-r) = x}.ncard ≤ 2)this:{J | ∃ k, u k + u (-k) = J} ⊆ {0}⊢ False simp_all[this.antisymm]
All goals completed! 🐙
-- Otherwise, take a, k such that f(a) + f(-a) = k ≠ 0.
rintro - ⟨a, rfl⟩
this.introIsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yu:ℚ → ℚb:IsAquaesulian uj:u 0 = 0c:¬({x | ∃ r, u r + u (-r) = x}.Finite ∧ ↑{x | ∃ r, u r + u (-r) = x}.ncard ≤ 2)a:ℚ⊢ u a + u (-a) ∈ {0}
contrapose! c
this.introIsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yu:ℚ → ℚb:IsAquaesulian uj:u 0 = 0a:ℚc:u a + u (-a) ∉ {0}⊢ {x | ∃ r, u r + u (-r) = x}.Finite ∧ ↑{x | ∃ r, u r + u (-r) = x}.ncard ≤ 2
simp_all
this.introIsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yu:ℚ → ℚa:ℚb:∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u yj:u 0 = 0c:¬u a + u (-a) = 0⊢ {x | ∃ r, u r + u (-r) = x}.Finite ∧ {x | ∃ r, u r + u (-r) = x}.ncard ≤ 2
-- If we can show that f(x) + f(-x) = 0 or k for all x, then we are done.
suffices:{U|∃examples6, (u) ‹ℚ› +u ( -‹_›)= U} ⊆{0,(u (a : Rat)+ (u<|@@↑(( (-a ))))) } ..
this.introIsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yu:ℚ → ℚa:ℚb:∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u yj:u 0 = 0c:¬u a + u (-a) = 0this:{U | ∃ examples6, u examples6 + u (-examples6) = U} ⊆ {0, u a + u (-a)}⊢ {x | ∃ r, u r + u (-r) = x}.Finite ∧ {x | ∃ r, u r + u (-r) = x}.ncard ≤ 2
thisIsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yu:ℚ → ℚa:ℚb:∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u yj:u 0 = 0c:¬u a + u (-a) = 0⊢ {U | ∃ examples6, u examples6 + u (-examples6) = U} ⊆ {0, u a + u (-a)}
·
this.introIsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yu:ℚ → ℚa:ℚb:∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u yj:u 0 = 0c:¬u a + u (-a) = 0this:{U | ∃ examples6, u examples6 + u (-examples6) = U} ⊆ {0, u a + u (-a)}⊢ {x | ∃ r, u r + u (-r) = x}.Finite ∧ {x | ∃ r, u r + u (-r) = x}.ncard ≤ 2 use ( Set.toFinite ( _) ).subset ↑@@this , (Set.ncard_le_ncard$ (((this )) ) ).trans (Set.ncard_pair$ Ne.symm (↑ ( (c)) ) ).le
All goals completed! 🐙
-- We now proceed to show that f(x) + f(-x) = 0 or k for all x.
rintro-⟨hz, rfl⟩
this.introIsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yu:ℚ → ℚa:ℚb:∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u yj:u 0 = 0c:¬u a + u (-a) = 0hz:ℚ⊢ u hz + u (-hz) ∈ {0, u a + u (-a)}
-- We have f(x + f(a)) = f(x) + a or f(f(x) + a) = x + f(a).
induction b @hz a
this.intro.inlIsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yu:ℚ → ℚa:ℚb:∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u yj:u 0 = 0c:¬u a + u (-a) = 0hz:ℚh✝:u (hz + u a) = u hz + a⊢ u hz + u (-hz) ∈ {0, u a + u (-a)}
this.intro.inrIsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yu:ℚ → ℚa:ℚb:∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u yj:u 0 = 0c:¬u a + u (-a) = 0hz:ℚh✝:u (u hz + a) = hz + u a⊢ u hz + u (-hz) ∈ {0, u a + u (-a)}
·
this.intro.inlIsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yu:ℚ → ℚa:ℚb:∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u yj:u 0 = 0c:¬u a + u (-a) = 0hz:ℚh✝:u (hz + u a) = u hz + a⊢ u hz + u (-hz) ∈ {0, u a + u (-a)} -- Step "f.": First, consider the case where f(x + f(a)) = f(x) + a.
/- Step "i.": We have f(-a + f(x + f(a))) = f(-a) + (x + f(a))
or f(f(-a) + (x + f(a))) = -a + f(x + f(a)). -/
have:=b (-a)$ hz+u a
this.intro.inlIsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yu:ℚ → ℚa:ℚb:∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u yj:u 0 = 0c:¬u a + u (-a) = 0hz:ℚh✝:u (hz + u a) = u hz + athis:u (-a + u (hz + u a)) = u (-a) + (hz + u a) ∨ u (u (-a) + (hz + u a)) = -a + u (hz + u a)⊢ u hz + u (-hz) ∈ {0, u a + u (-a)}
/- Step "ii.": We have f(x + f(x)) = f(x) + x or f(f(x) + x) = x + f(x).
This simplifies to just f(x + f(x)) = x + f(x).
-/
have:=b hz hz
this.intro.inlIsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yu:ℚ → ℚa:ℚb:∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u yj:u 0 = 0c:¬u a + u (-a) = 0hz:ℚh✝:u (hz + u a) = u hz + athis✝:u (-a + u (hz + u a)) = u (-a) + (hz + u a) ∨ u (u (-a) + (hz + u a)) = -a + u (hz + u a)this:u (hz + u hz) = u hz + hz ∨ u (u hz + hz) = hz + u hz⊢ u hz + u (-hz) ∈ {0, u a + u (-a)}
/- Step "iii.": Substituting step “f.” into step “i.” and simplifying
gives f(f(x)) = x + f(a) + f(-a) or f(x + f(a) + f(-a)) = f(x). -/
simp_all[add_comm]
this.intro.inlIsAquaesulian:(ℚ → ℚ) → Propu:ℚ → ℚa:ℚhz:ℚIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f yb:∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u yj:u 0 = 0c:¬u a + u (-a) = 0h✝:u (hz + u a) = a + u hzthis✝:u (u hz) = hz + u a + u (-a) ∨ u (hz + u a + u (-a)) = u hzthis:u (hz + u hz) = hz + u hz⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
/- Step "iiii.": We have f(-x + f(x + f(x))) = f(-x) + x + f(x) or
f(f(-x) + x + f(x)) = -x + f(x + f(x)). -/
have:=b (-hz) (hz+u ↑(hz))
this.intro.inlIsAquaesulian:(ℚ → ℚ) → Propu:ℚ → ℚa:ℚhz:ℚIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f yb:∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u yj:u 0 = 0c:¬u a + u (-a) = 0h✝:u (hz + u a) = a + u hzthis✝¹:u (u hz) = hz + u a + u (-a) ∨ u (hz + u a + u (-a)) = u hzthis✝:u (hz + u hz) = hz + u hzthis:u (-hz + u (hz + u hz)) = hz + u hz + u (-hz) ∨ u (hz + u hz + u (-hz)) = -hz + u (hz + u hz)⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
/- Substituting step “ii.” into step “iv.”, we have
f(f(x)) = x + f(-x) + f(x) or f(x + f(-x) + f(x)) = f(x). -/
simp_all[ add_assoc, C]
this.intro.inlIsAquaesulian:(ℚ → ℚ) → Propu:ℚ → ℚa:ℚhz:ℚIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f yb:∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u yj:u 0 = 0c:¬u a + u (-a) = 0h✝:u (hz + u a) = a + u hzthis✝¹:u (u hz) = hz + (u a + u (-a)) ∨ u (hz + (u a + u (-a))) = u hzthis✝:u (hz + u hz) = hz + u hzthis:u (u hz) = hz + (u hz + u (-hz)) ∨ u (hz + (u hz + u (-hz))) = u hz⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
induction this
this.intro.inl.inlIsAquaesulian:(ℚ → ℚ) → Propu:ℚ → ℚa:ℚhz:ℚIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f yb:∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u yj:u 0 = 0c:¬u a + u (-a) = 0h✝¹:u (hz + u a) = a + u hzthis✝:u (u hz) = hz + (u a + u (-a)) ∨ u (hz + (u a + u (-a))) = u hzthis:u (hz + u hz) = hz + u hzh✝:u (u hz) = hz + (u hz + u (-hz))⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
this.intro.inl.inrIsAquaesulian:(ℚ → ℚ) → Propu:ℚ → ℚa:ℚhz:ℚIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f yb:∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u yj:u 0 = 0c:¬u a + u (-a) = 0h✝¹:u (hz + u a) = a + u hzthis✝:u (u hz) = hz + (u a + u (-a)) ∨ u (hz + (u a + u (-a))) = u hzthis:u (hz + u hz) = hz + u hzh✝:u (hz + (u hz + u (-hz))) = u hz⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
·
this.intro.inl.inlIsAquaesulian:(ℚ → ℚ) → Propu:ℚ → ℚa:ℚhz:ℚIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f yb:∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u yj:u 0 = 0c:¬u a + u (-a) = 0h✝¹:u (hz + u a) = a + u hzthis✝:u (u hz) = hz + (u a + u (-a)) ∨ u (hz + (u a + u (-a))) = u hzthis:u (hz + u hz) = hz + u hzh✝:u (u hz) = hz + (u hz + u (-hz))⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a) -- Step "vi.": First, consider the case where f(f(x)) = x + f(-x) + f(x).
/- Step "vi.1" In this case, step “iii.” simplifies to
f(-x) + f(x) = f(a) + f(-a)
or f(x + f(a) + f(-a)) = f(x). In the first case we are done,
so we focus only on the second case. -/
simp_all
this.intro.inl.inlIsAquaesulian:(ℚ → ℚ) → Propu:ℚ → ℚa:ℚhz:ℚIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f yb:∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u yj:u 0 = 0c:¬u a + u (-a) = 0h✝¹:u (hz + u a) = a + u hzthis✝:u hz + u (-hz) = u a + u (-a) ∨ u (hz + (u a + u (-a))) = u hzthis:u (hz + u hz) = hz + u hzh✝:u (u hz) = hz + (u hz + u (-hz))⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
/- Step "vi.2": We have
f(x + f(x + f(a) + f(-a))) = f(x) + x + (f(a) + f(-a)) or
f(f(x) + x + f(a) + f(-a)) = x + f(x + f(a) + f(-a)). -/
have:=b hz (hz+(u a+u (-a)))
this.intro.inl.inlIsAquaesulian:(ℚ → ℚ) → Propu:ℚ → ℚa:ℚhz:ℚIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f yb:∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u yj:u 0 = 0c:¬u a + u (-a) = 0h✝¹:u (hz + u a) = a + u hzthis✝¹:u hz + u (-hz) = u a + u (-a) ∨ u (hz + (u a + u (-a))) = u hzthis✝:u (hz + u hz) = hz + u hzh✝:u (u hz) = hz + (u hz + u (-hz))this:u (hz + u (hz + (u a + u (-a)))) = hz + (u a + u (-a)) + u hz ∨
u (hz + (u a + u (-a)) + u hz) = hz + u (hz + (u a + u (-a)))⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
/- Step "vi.3": We have
f(x + f(a) + f(-a) + f(x + f(a) + f(-a)))
= x + f(a) + f(-a) + f(x + f(a) + f(-a)). -/
have:=b (hz+(u a+u (-a)))$ hz+(u a+u (-a))
this.intro.inl.inlIsAquaesulian:(ℚ → ℚ) → Propu:ℚ → ℚa:ℚhz:ℚIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f yb:∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u yj:u 0 = 0c:¬u a + u (-a) = 0h✝¹:u (hz + u a) = a + u hzthis✝²:u hz + u (-hz) = u a + u (-a) ∨ u (hz + (u a + u (-a))) = u hzthis✝¹:u (hz + u hz) = hz + u hzh✝:u (u hz) = hz + (u hz + u (-hz))this✝:u (hz + u (hz + (u a + u (-a)))) = hz + (u a + u (-a)) + u hz ∨
u (hz + (u a + u (-a)) + u hz) = hz + u (hz + (u a + u (-a)))this:u (hz + (u a + u (-a)) + u (hz + (u a + u (-a)))) = hz + (u a + u (-a)) + u (hz + (u a + u (-a))) ∨
u (hz + (u a + u (-a)) + u (hz + (u a + u (-a)))) = hz + (u a + u (-a)) + u (hz + (u a + u (-a)))⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
/- Step "vi.4": Substituting step “vi.1.” into step “vi.2” gives
f(x +f(x))=f(x)+x+(f(a)+f(-a)) or f(f(x)+x+f(a)+f(-a))=x+f(x).
Step "vi.5" Substituting step “vi.1.” into step “vi.3.” gives
f(x+f(a)+f(-a)+f(x))=x+f(a)+f(-a)+f(x).
Substituting step “vi.5.” into step “vi.4.” and simplifying gives
f(x +f(x))=f(x)+x+(f(a)+f(-a)) or f(a)+f(-a)=0.
The former case simplifies via step “ii.” to f(a)+f(-a)=0,
so in both cases we have a contradiction. -/
use .inr$ by_contra$ by
IsAquaesulian:(ℚ → ℚ) → Propu:ℚ → ℚa:ℚhz:ℚIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f yb:∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u yj:u 0 = 0c:¬u a + u (-a) = 0h✝¹:u (hz + u a) = a + u hzthis✝²:u hz + u (-hz) = u a + u (-a) ∨ u (hz + (u a + u (-a))) = u hzthis✝¹:u (hz + u hz) = hz + u hzh✝:u (u hz) = hz + (u hz + u (-hz))this✝:u (hz + u (hz + (u a + u (-a)))) = hz + (u a + u (-a)) + u hz ∨
u (hz + (u a + u (-a)) + u hz) = hz + u (hz + (u a + u (-a)))this:u (hz + (u a + u (-a)) + u (hz + (u a + u (-a)))) = hz + (u a + u (-a)) + u (hz + (u a + u (-a))) ∨
u (hz + (u a + u (-a)) + u (hz + (u a + u (-a)))) = hz + (u a + u (-a)) + u (hz + (u a + u (-a)))⊢ ¬u hz + u (-hz) = u a + u (-a) → False Try these:
• aesop
• simp_all only [or_self, imp_false, Decidable.not_not]hint
All goals completed! 🐙
-- Step "vii." Now, consider the case where f(x + f(-x) + f(x)) = f(x).
/- Step "vii.1": We have f(x + f(x + f(-x) + f(x))) = f(x) + x + f(-x) + f(x)
or f(f(x) + x + f(-x) + f(x)) = x + f(x + f(-x) + f(x)). -/
have:=b hz$ hz+(u hz+u (-hz))
this.intro.inl.inrIsAquaesulian:(ℚ → ℚ) → Propu:ℚ → ℚa:ℚhz:ℚIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f yb:∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u yj:u 0 = 0c:¬u a + u (-a) = 0h✝¹:u (hz + u a) = a + u hzthis✝¹:u (u hz) = hz + (u a + u (-a)) ∨ u (hz + (u a + u (-a))) = u hzthis✝:u (hz + u hz) = hz + u hzh✝:u (hz + (u hz + u (-hz))) = u hzthis:u (hz + u (hz + (u hz + u (-hz)))) = hz + (u hz + u (-hz)) + u hz ∨
u (hz + (u hz + u (-hz)) + u hz) = hz + u (hz + (u hz + u (-hz)))⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
/- Step "vii.2": We have f(f(x + f(-x) + f(x)) + x + f(-x) + f(x)) =
x + f(-x) + f(x) + f(x + f(-x) + f(x)).
Step "vii.3": Substituting step “vii.” into step “vii.2.” gives
f(f(x)+x+f(-x)+f(x))= x+f(-x)+f(x)+f(x).
Substituting step “vii.” into step “1.” gives
f(x+f(x))=f(x)+x+f(-x)+f(x) or
f(f(x)+x+f(-x)+f(x))=x+f(x).
In the first case we can substitute in step “ii.” and
simplify to f(-x)+f(x)=0 as desired.
In the second case we can substitute in step “vii.3” to
obtain f(-x)+f(x)=0 again as desired. -/
cases b (hz+(u hz+u (-hz)))$ hz+(u hz+u (-hz))with|_=>
this.intro.inl.inr.inrIsAquaesulian:(ℚ → ℚ) → Propu:ℚ → ℚa:ℚhz:ℚIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f yb:∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u yj:u 0 = 0c:¬u a + u (-a) = 0h✝²:u (hz + u a) = a + u hzthis✝¹:u (u hz) = hz + (u a + u (-a)) ∨ u (hz + (u a + u (-a))) = u hzthis✝:u (hz + u hz) = hz + u hzh✝¹:u (hz + (u hz + u (-hz))) = u hzthis:u (hz + u (hz + (u hz + u (-hz)))) = hz + (u hz + u (-hz)) + u hz ∨
u (hz + (u hz + u (-hz)) + u hz) = hz + u (hz + (u hz + u (-hz)))h✝:u (hz + (u hz + u (-hz)) + u (hz + (u hz + u (-hz)))) = hz + (u hz + u (-hz)) + u (hz + (u hz + u (-hz)))⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)Try these:
• simp_all only [add_left_inj, self_eq_add_right, add_right_eq_self, or_self, add_zero, true_or]Try these:
• simp_all only [add_left_inj, self_eq_add_right, add_right_eq_self, or_self, add_zero, true_or]hint
All goals completed! 🐙
-- Step "g.": Now, consider the case where  f(f(x) + a) = x + f(a).
/- Step "i.": We have f(-x + f(f(x) + a)) = f(-x) + (f(x) + a) or
f(f(-x) + f(x) + a) = -x + f(f(x) + a). -/
have:=b (-hz) (u hz+a)
this.intro.inrIsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yu:ℚ → ℚa:ℚb:∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u yj:u 0 = 0c:¬u a + u (-a) = 0hz:ℚh✝:u (u hz + a) = hz + u athis:u (-hz + u (u hz + a)) = u (-hz) + (u hz + a) ∨ u (u (-hz) + (u hz + a)) = -hz + u (u hz + a)⊢ u hz + u (-hz) ∈ {0, u a + u (-a)}
have:=b$ -a
this.intro.inrIsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yu:ℚ → ℚa:ℚb:∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u yj:u 0 = 0c:¬u a + u (-a) = 0hz:ℚh✝:u (u hz + a) = hz + u athis✝:u (-hz + u (u hz + a)) = u (-hz) + (u hz + a) ∨ u (u (-hz) + (u hz + a)) = -hz + u (u hz + a)this:∀ (y : ℚ), u (-a + u y) = u (-a) + y ∨ u (u (-a) + y) = -a + u y⊢ u hz + u (-hz) ∈ {0, u a + u (-a)}
/- Step "ii." We have f(-a + f(f(x) + a)) = f(-a) + (f(x) + a) or
f(f(-a) + (f(x) + a)) = -a + f(f(x) + a). -/
specialize this (u hz+a)
this.intro.inrIsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yu:ℚ → ℚa:ℚb:∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u yj:u 0 = 0c:¬u a + u (-a) = 0hz:ℚh✝:u (u hz + a) = hz + u athis✝:u (-hz + u (u hz + a)) = u (-hz) + (u hz + a) ∨ u (u (-hz) + (u hz + a)) = -hz + u (u hz + a)this:u (-a + u (u hz + a)) = u (-a) + (u hz + a) ∨ u (u (-a) + (u hz + a)) = -a + u (u hz + a)⊢ u hz + u (-hz) ∈ {0, u a + u (-a)}
/- Step "iii.": Substituting step “g.” into step “i.” gives
f(f(a)) = f(-x) + (f(x) + a) or f(f(-x) + f(x) + a) = f(a).
Step "iv.": Substituting step “g.” into step “ii.” gives
f(-a + x + f(a)) = f(-a) + f(x) + a or
f(f(-a) + f(x) + a) = -a + x + f(a). -/
simp_all[ ←add_assoc]
this.intro.inrIsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yu:ℚ → ℚa:ℚb:∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u yj:u 0 = 0c:¬u a + u (-a) = 0hz:ℚh✝:u (u hz + a) = hz + u athis✝:u (u a) = u (-hz) + u hz + a ∨ u (u (-hz) + u hz + a) = u athis:u (-a + hz + u a) = u (-a) + u hz + a ∨ u (u (-a) + u hz + a) = -a + hz + u a⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
have:=b 0
this.intro.inrIsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yu:ℚ → ℚa:ℚb:∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u yj:u 0 = 0c:¬u a + u (-a) = 0hz:ℚh✝:u (u hz + a) = hz + u athis✝¹:u (u a) = u (-hz) + u hz + a ∨ u (u (-hz) + u hz + a) = u athis✝:u (-a + hz + u a) = u (-a) + u hz + a ∨ u (u (-a) + u hz + a) = -a + hz + u athis:∀ (y : ℚ), u (0 + u y) = u 0 + y ∨ u (u 0 + y) = 0 + u y⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
have:=b
this.intro.inrIsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yu:ℚ → ℚa:ℚb:∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u yj:u 0 = 0c:¬u a + u (-a) = 0hz:ℚh✝:u (u hz + a) = hz + u athis✝²:u (u a) = u (-hz) + u hz + a ∨ u (u (-hz) + u hz + a) = u athis✝¹:u (-a + hz + u a) = u (-a) + u hz + a ∨ u (u (-a) + u hz + a) = -a + hz + u athis✝:∀ (y : ℚ), u (0 + u y) = u 0 + y ∨ u (u 0 + y) = 0 + u ythis:∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u y⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
-- Step "v.": We have f(a + f(a)) = a + f(a).
specialize b a a
this.intro.inrIsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yu:ℚ → ℚa:ℚj:u 0 = 0c:¬u a + u (-a) = 0hz:ℚh✝:u (u hz + a) = hz + u athis✝²:u (u a) = u (-hz) + u hz + a ∨ u (u (-hz) + u hz + a) = u athis✝¹:u (-a + hz + u a) = u (-a) + u hz + a ∨ u (u (-a) + u hz + a) = -a + hz + u athis✝:∀ (y : ℚ), u (0 + u y) = u 0 + y ∨ u (u 0 + y) = 0 + u ythis:∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u yb:u (a + u a) = u a + a ∨ u (u a + a) = a + u a⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
simp_all[add_comm]
this.intro.inrIsAquaesulian:(ℚ → ℚ) → Propu:ℚ → ℚa:ℚhz:ℚIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f yj:u 0 = 0c:¬u a + u (-a) = 0h✝:u (a + u hz) = hz + u athis✝¹:u (u a) = a + (u hz + u (-hz)) ∨ u (a + (u hz + u (-hz))) = u athis✝:u (u a + (hz + -a)) = a + (u hz + u (-a)) ∨ u (a + (u hz + u (-a))) = u a + (hz + -a)this:∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u yb:u (a + u a) = a + u a⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
/- Step "vi.": We have f(-a + f(a + f(a))) = f(-a) + a + f(a) or
f(f(-a) + a + f(a)) = -a + f(a + f(a)). -/
have:=(this<| -a) (↑a + (((u a))): (↑_ :((( _) ) ) )) ..
this.intro.inrIsAquaesulian:(ℚ → ℚ) → Propu:ℚ → ℚa:ℚhz:ℚIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f yj:u 0 = 0c:¬u a + u (-a) = 0h✝:u (a + u hz) = hz + u athis✝²:u (u a) = a + (u hz + u (-hz)) ∨ u (a + (u hz + u (-hz))) = u athis✝¹:u (u a + (hz + -a)) = a + (u hz + u (-a)) ∨ u (a + (u hz + u (-a))) = u a + (hz + -a)this✝:∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u yb:u (a + u a) = a + u athis:u (-a + u (a + u a)) = a + u a + u (-a) ∨ u (a + u a + u (-a)) = -a + u (a + u a)⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
/- Step "vii.": Substituting step “v.” into step “vi.” and simplifying gives
f(f(a)) = a + f(a) + f(-a) or f(a + f(a) + f(-a)) = f(a). -/
simp_all[add_assoc]
this.intro.inrIsAquaesulian:(ℚ → ℚ) → Propu:ℚ → ℚa:ℚhz:ℚIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f yj:u 0 = 0c:¬u a + u (-a) = 0h✝:u (a + u hz) = hz + u athis✝²:u (u a) = a + (u hz + u (-hz)) ∨ u (a + (u hz + u (-hz))) = u athis✝¹:u (u a + (hz + -a)) = a + (u hz + u (-a)) ∨ u (a + (u hz + u (-a))) = u a + (hz + -a)this✝:∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u yb:u (a + u a) = a + u athis:u (u a) = a + (u a + u (-a)) ∨ u (a + (u a + u (-a))) = u a⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
cases this
this.intro.inr.inlIsAquaesulian:(ℚ → ℚ) → Propu:ℚ → ℚa:ℚhz:ℚIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f yj:u 0 = 0c:¬u a + u (-a) = 0h✝¹:u (a + u hz) = hz + u athis✝¹:u (u a) = a + (u hz + u (-hz)) ∨ u (a + (u hz + u (-hz))) = u athis✝:u (u a + (hz + -a)) = a + (u hz + u (-a)) ∨ u (a + (u hz + u (-a))) = u a + (hz + -a)this:∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u yb:u (a + u a) = a + u ah✝:u (u a) = a + (u a + u (-a))⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
this.intro.inr.inrIsAquaesulian:(ℚ → ℚ) → Propu:ℚ → ℚa:ℚhz:ℚIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f yj:u 0 = 0c:¬u a + u (-a) = 0h✝¹:u (a + u hz) = hz + u athis✝¹:u (u a) = a + (u hz + u (-hz)) ∨ u (a + (u hz + u (-hz))) = u athis✝:u (u a + (hz + -a)) = a + (u hz + u (-a)) ∨ u (a + (u hz + u (-a))) = u a + (hz + -a)this:∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u yb:u (a + u a) = a + u ah✝:u (a + (u a + u (-a))) = u a⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
·
this.intro.inr.inlIsAquaesulian:(ℚ → ℚ) → Propu:ℚ → ℚa:ℚhz:ℚIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f yj:u 0 = 0c:¬u a + u (-a) = 0h✝¹:u (a + u hz) = hz + u athis✝¹:u (u a) = a + (u hz + u (-hz)) ∨ u (a + (u hz + u (-hz))) = u athis✝:u (u a + (hz + -a)) = a + (u hz + u (-a)) ∨ u (a + (u hz + u (-a))) = u a + (hz + -a)this:∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u yb:u (a + u a) = a + u ah✝:u (u a) = a + (u a + u (-a))⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a) -- Step "viii.": First, consider the case where f(f(a)) = a + f(a) + f(-a).
/- Step "viii.1": In this case, step “iii.” simplifies to
f(a) + f(-a) = f(-x) + f(x) or f(f(-x) + f(x) + a) = f(a).
In the first case we are done, so we focus only on the second case. -/
simp_all
this.intro.inr.inlIsAquaesulian:(ℚ → ℚ) → Propu:ℚ → ℚa:ℚhz:ℚIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f yj:u 0 = 0c:¬u a + u (-a) = 0h✝¹:u (a + u hz) = hz + u athis✝¹:u a + u (-a) = u hz + u (-hz) ∨ u (a + (u hz + u (-hz))) = u athis✝:u (u a + (hz + -a)) = a + (u hz + u (-a)) ∨ u (a + (u hz + u (-a))) = u a + (hz + -a)this:∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u yb:u (a + u a) = a + u ah✝:u (u a) = a + (u a + u (-a))⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
contrapose! IsAquaesulian_def
this.intro.inr.inlIsAquaesulian:(ℚ → ℚ) → Propu:ℚ → ℚa:ℚhz:ℚj:u 0 = 0c:¬u a + u (-a) = 0h✝¹:u (a + u hz) = hz + u athis✝¹:u a + u (-a) = u hz + u (-hz) ∨ u (a + (u hz + u (-hz))) = u athis✝:u (u a + (hz + -a)) = a + (u hz + u (-a)) ∨ u (a + (u hz + u (-a))) = u a + (hz + -a)this:∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u yb:u (a + u a) = a + u ah✝:u (u a) = a + (u a + u (-a))IsAquaesulian_def:u hz + u (-hz) ≠ 0 ∧ u hz + u (-hz) ≠ u a + u (-a)⊢ ∃ f,
(IsAquaesulian f ∧ ∃ x y, f (x + f y) ≠ y + f x ∧ f (y + f x) ≠ x + f y) ∨
¬IsAquaesulian f ∧ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f y
simp_all
this.intro.inr.inlIsAquaesulian:(ℚ → ℚ) → Propu:ℚ → ℚa:ℚhz:ℚj:u 0 = 0c:¬u a + u (-a) = 0h✝¹:u (a + u hz) = hz + u athis✝¹:u a + u (-a) = u hz + u (-hz) ∨ u (a + (u hz + u (-hz))) = u athis✝:u (u a + (hz + -a)) = a + (u hz + u (-a)) ∨ u (a + (u hz + u (-a))) = u a + (hz + -a)this:∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u yb:u (a + u a) = a + u ah✝:u (u a) = a + (u a + u (-a))IsAquaesulian_def:¬u hz + u (-hz) = 0 ∧ ¬u hz + u (-hz) = u a + u (-a)⊢ ∃ f,
(IsAquaesulian f ∧ ∃ x y, ¬f (x + f y) = y + f x ∧ ¬f (y + f x) = x + f y) ∨
¬IsAquaesulian f ∧ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f y
exfalso
this.intro.inr.inlIsAquaesulian:(ℚ → ℚ) → Propu:ℚ → ℚa:ℚhz:ℚj:u 0 = 0c:¬u a + u (-a) = 0h✝¹:u (a + u hz) = hz + u athis✝¹:u a + u (-a) = u hz + u (-hz) ∨ u (a + (u hz + u (-hz))) = u athis✝:u (u a + (hz + -a)) = a + (u hz + u (-a)) ∨ u (a + (u hz + u (-a))) = u a + (hz + -a)this:∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u yb:u (a + u a) = a + u ah✝:u (u a) = a + (u a + u (-a))IsAquaesulian_def:¬u hz + u (-hz) = 0 ∧ ¬u hz + u (-hz) = u a + u (-a)⊢ False
/- Step "viii.2": We have
f(a + f(a + (f(x) + f(-x)))) = a + (f(x) + f(-x)) + f(a) or
f(a + (f(x) + f(-x)) + f(a)) = a + f(a + (f(x) + f(-x))). -/
have:=this a (a+(u hz+u ( -hz)))
this.intro.inr.inlIsAquaesulian:(ℚ → ℚ) → Propu:ℚ → ℚa:ℚhz:ℚj:u 0 = 0c:¬u a + u (-a) = 0h✝¹:u (a + u hz) = hz + u athis✝²:u a + u (-a) = u hz + u (-hz) ∨ u (a + (u hz + u (-hz))) = u athis✝¹:u (u a + (hz + -a)) = a + (u hz + u (-a)) ∨ u (a + (u hz + u (-a))) = u a + (hz + -a)this✝:∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u yb:u (a + u a) = a + u ah✝:u (u a) = a + (u a + u (-a))IsAquaesulian_def:¬u hz + u (-hz) = 0 ∧ ¬u hz + u (-hz) = u a + u (-a)this:u (a + u (a + (u hz + u (-hz)))) = a + (u hz + u (-hz)) + u a ∨
u (a + (u hz + u (-hz)) + u a) = a + u (a + (u hz + u (-hz)))⊢ False
simp_all[Ne.symm,Bool]
this.intro.inr.inlIsAquaesulian:(ℚ → ℚ) → Propu:ℚ → ℚa:ℚhz:ℚj:u 0 = 0c:¬u a + u (-a) = 0h✝¹:u (a + u hz) = hz + u athis✝²:u (a + (u hz + u (-hz))) = u athis✝¹:u (u a + (hz + -a)) = a + (u hz + u (-a)) ∨ u (a + (u hz + u (-a))) = u a + (hz + -a)this✝:∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u yb:u (a + u a) = a + u ah✝:u (u a) = a + (u a + u (-a))IsAquaesulian_def:¬u hz + u (-hz) = 0 ∧ ¬u hz + u (-hz) = u a + u (-a)this:u (a + (u hz + u (-hz)) + u a) = a + u a⊢ False
/- Step "viii.3": We have
f(a + f(x) + f(-x) + f(a + f(x) + f(-x))) =
a + f(x) + f(-x) + f(a + f(x) + f(-x)). -/
have:=‹∀congr_arg G,_› (a+(u hz+u (-hz)))$ a+(u ↑hz+u ↑( -hz) )
this.intro.inr.inlIsAquaesulian:(ℚ → ℚ) → Propu:ℚ → ℚa:ℚhz:ℚj:u 0 = 0c:¬u a + u (-a) = 0h✝¹:u (a + u hz) = hz + u athis✝³:u (a + (u hz + u (-hz))) = u athis✝²:u (u a + (hz + -a)) = a + (u hz + u (-a)) ∨ u (a + (u hz + u (-a))) = u a + (hz + -a)this✝¹:∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u yb:u (a + u a) = a + u ah✝:u (u a) = a + (u a + u (-a))IsAquaesulian_def:¬u hz + u (-hz) = 0 ∧ ¬u hz + u (-hz) = u a + u (-a)this✝:u (a + (u hz + u (-hz)) + u a) = a + u athis:u (a + (u hz + u (-hz)) + u (a + (u hz + u (-hz)))) = a + (u hz + u (-hz)) + u (a + (u hz + u (-hz))) ∨
u (a + (u hz + u (-hz)) + u (a + (u hz + u (-hz)))) = a + (u hz + u (-hz)) + u (a + (u hz + u (-hz)))⊢ False
/- Step "viii.4": Substituting step “viii.1” into step “viii.3” gives
f(a + f(x) + f(-x) + f(a))=a + f(x) + f(-x) + f(a).
The result follows by casework on step “viii.2”; In the first case,
substituting in step “viii.1” followed by step “v.” gives
f(x) + f(-x) = 0 as desired, and in the second case,
substituting in step “viiii.4” followed by step “viii.1” gives
f(x) + f(-x) = 0 again as desired.
-/
simp_all
All goals completed! 🐙
-- Step "ix.": Now, consider the case where f(a + f(a) + f(-a)) = f(a).
/- Step "ix.1.": We have f(a + f(a + f(a) + f(-a))) = f(a) + a + f(a) + f(-a)
or f(f(a) + a + f(a) + f(-a)) = a + f(a + f(a) + f(-a)). -/
have:=this a (a +(u a+u (-a)))
this.intro.inr.inrIsAquaesulian:(ℚ → ℚ) → Propu:ℚ → ℚa:ℚhz:ℚIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f yj:u 0 = 0c:¬u a + u (-a) = 0h✝¹:u (a + u hz) = hz + u athis✝²:u (u a) = a + (u hz + u (-hz)) ∨ u (a + (u hz + u (-hz))) = u athis✝¹:u (u a + (hz + -a)) = a + (u hz + u (-a)) ∨ u (a + (u hz + u (-a))) = u a + (hz + -a)this✝:∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u yb:u (a + u a) = a + u ah✝:u (a + (u a + u (-a))) = u athis:u (a + u (a + (u a + u (-a)))) = a + (u a + u (-a)) + u a ∨ u (a + (u a + u (-a)) + u a) = a + u (a + (u a + u (-a)))⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
/- Step "ix.2.": We have
f(a + f(a) + f(-a) + f(a + f(a) + f(-a)))
= a + f(a) + f(-a) + f(a + f(a) + f(-a)).
Step "ix.3.": Substituting step “ix.” into step “ix.2” gives
f(a + f(a) + f(-a) +f(a)) = a + f(a) + f(-a) + f(a).
The result follows by casework on step “ix.1.”: In the first case,
we can substitute in step “ix.” followed by step “v.” to get f(a)+f(-a)=0,
and in the second case we can substitute in step “ix.3.”
followed by step “ix.” to get f(a)+f(-a)=0 again.
Either way, this contradicts our assumption about a. -/
cases‹forall Jd S,_› (a+(u a+u (-a))) ( a + (u a +u ↑(-a)))with| _ =>
this.intro.inr.inr.inrIsAquaesulian:(ℚ → ℚ) → Propu:ℚ → ℚa:ℚhz:ℚIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f yj:u 0 = 0c:¬u a + u (-a) = 0h✝²:u (a + u hz) = hz + u athis✝²:u (u a) = a + (u hz + u (-hz)) ∨ u (a + (u hz + u (-hz))) = u athis✝¹:u (u a + (hz + -a)) = a + (u hz + u (-a)) ∨ u (a + (u hz + u (-a))) = u a + (hz + -a)this✝:∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u yb:u (a + u a) = a + u ah✝¹:u (a + (u a + u (-a))) = u athis:u (a + u (a + (u a + u (-a)))) = a + (u a + u (-a)) + u a ∨ u (a + (u a + u (-a)) + u a) = a + u (a + (u a + u (-a)))h✝:u (a + (u a + u (-a)) + u (a + (u a + u (-a)))) = a + (u a + u (-a)) + u (a + (u a + u (-a)))⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)Try these:
• simp_all only [add_left_inj, self_eq_add_right, false_or]Try these:
• simp_all only [add_left_inj, self_eq_add_right, false_or]hint
All goals completed! 🐙
/- Now let f be an aquaesulian function with f(0) ≠ 0.
We will derive a contradiction. -/
simp_all
refine_1.refine_2IsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yu:ℚ → ℚb:∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u yj:¬u 0 = 0⊢ {x | ∃ r, u r + u (-r) = x}.Finite ∧ {x | ∃ r, u r + u (-r) = x}.ncard ≤ 2
/- We have:
P(0, 0) -> f(f(0)) = f(0),
P(f(0), f(0)) -> f(f(0) + f(f(0))) = f(0) + f(f(0)) ->
f(2f(0)) = 2f(0),
P(0, f(0)) -> f(f(f(0))) = 2f(0) or f(2f(0)) = f(f(0)) ->
f(0) = 2f(0) or f(2f(0)) = f(0) -> f(0) = 2f(0) or 2f(0) = f(0),
so f(0) = 0 as desired. -/
cases b 0 0with|_=>
refine_1.refine_2.inrIsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yu:ℚ → ℚb:∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u yj:¬u 0 = 0h✝:u (u 0 + 0) = 0 + u 0⊢ {x | ∃ r, u r + u (-r) = x}.Finite ∧ {x | ∃ r, u r + u (-r) = x}.ncard ≤ 2exact absurd (b 0$ (0+(1 *(@(u ↑.((0) )))))^ 01: ↑ ((_)) ) (id$ (by
IsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yu:ℚ → ℚb:∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u yj:¬u 0 = 0h✝:u (u 0 + 0) = 0 + u 0⊢ ¬(u (0 + u ((0 + 1 * u 0) ^ 1)) = u 0 + (0 + 1 * u 0) ^ 1 ∨ u (u 0 + (0 + 1 * u 0) ^ 1) = 0 + u ((0 + 1 * u 0) ^ 1))(cases ( b (u 0) ( (u 0)))with|_ =>
inrIsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yu:ℚ → ℚb:∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u yj:¬u 0 = 0h✝¹:u (u 0 + 0) = 0 + u 0h✝:u (u (u 0) + u 0) = u 0 + u (u 0)⊢ ¬(u (0 + u ((0 + 1 * u 0) ^ 1)) = u 0 + (0 + 1 * u 0) ^ 1 ∨ u (u 0 + (0 + 1 * u 0) ^ 1) = 0 + u ((0 + 1 * u 0) ^ 1)) continuity
All goals completed! 🐙)))
rintro K V
refine_2IsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yK:ℤV:K ∈ {c | ∀ (f : ℚ → ℚ), IsAquaesulian f → {x | ∃ r, f r + f (-r) = x}.Finite ∧ ↑{x | ∃ r, f r + f (-r) = x}.ncard ≤ c}⊢ 2 ≤ K
-- Now let f(x) = -x + 2⌈x⌉. We claim that f is aquaesulian.
specialize V $ λ N=>-N+2 *Int.ceil N
refine_2IsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yK:ℤV:(IsAquaesulian fun N => -N + 2 * ↑⌈N⌉) →
{x | ∃ r, -r + 2 * ↑⌈r⌉ + (- -r + 2 * ↑⌈-r⌉) = x}.Finite ∧
↑{x | ∃ r, -r + 2 * ↑⌈r⌉ + (- -r + 2 * ↑⌈-r⌉) = x}.ncard ≤ K⊢ 2 ≤ K
specialize( V $ (IsAquaesulian_def _).mpr _)
refine_2IsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yK:ℤV:(IsAquaesulian fun N => -N + 2 * ↑⌈N⌉) →
{x | ∃ r, -r + 2 * ↑⌈r⌉ + (- -r + 2 * ↑⌈-r⌉) = x}.Finite ∧
↑{x | ∃ r, -r + 2 * ↑⌈r⌉ + (- -r + 2 * ↑⌈-r⌉) = x}.ncard ≤ K⊢ ∀ (x y : ℚ),
-(x + (-y + 2 * ↑⌈y⌉)) + 2 * ↑⌈x + (-y + 2 * ↑⌈y⌉)⌉ = -x + 2 * ↑⌈x⌉ + y ∨
-(-x + 2 * ↑⌈x⌉ + y) + 2 * ↑⌈-x + 2 * ↑⌈x⌉ + y⌉ = x + (-y + 2 * ↑⌈y⌉)
refine_2IsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yK:ℤV:{x | ∃ r, -r + 2 * ↑⌈r⌉ + (- -r + 2 * ↑⌈-r⌉) = x}.Finite ∧ ↑{x | ∃ r, -r + 2 * ↑⌈r⌉ + (- -r + 2 * ↑⌈-r⌉) = x}.ncard ≤ K⊢ 2 ≤ K
·
refine_2IsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yK:ℤV:(IsAquaesulian fun N => -N + 2 * ↑⌈N⌉) →
{x | ∃ r, -r + 2 * ↑⌈r⌉ + (- -r + 2 * ↑⌈-r⌉) = x}.Finite ∧
↑{x | ∃ r, -r + 2 * ↑⌈r⌉ + (- -r + 2 * ↑⌈-r⌉) = x}.ncard ≤ K⊢ ∀ (x y : ℚ),
-(x + (-y + 2 * ↑⌈y⌉)) + 2 * ↑⌈x + (-y + 2 * ↑⌈y⌉)⌉ = -x + 2 * ↑⌈x⌉ + y ∨
-(-x + 2 * ↑⌈x⌉ + y) + 2 * ↑⌈-x + 2 * ↑⌈x⌉ + y⌉ = x + (-y + 2 * ↑⌈y⌉) simp_rw [ ←eq_sub_iff_add_eq'
refine_2IsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yK:ℤV:(IsAquaesulian fun N => -N + 2 * ↑⌈N⌉) →
{x | ∃ r, -r + 2 * ↑⌈r⌉ + (- -r + 2 * ↑⌈-r⌉) = x}.Finite ∧
↑{x | ∃ r, -r + 2 * ↑⌈r⌉ + (- -r + 2 * ↑⌈-r⌉) = x}.ncard ≤ K⊢ ∀ (x y : ℚ),
2 * ↑⌈x + (-y + 2 * ↑⌈y⌉)⌉ = -x + 2 * ↑⌈x⌉ + y - -(x + (-y + 2 * ↑⌈y⌉)) ∨
2 * ↑⌈-x + 2 * ↑⌈x⌉ + y⌉ = x + (-y + 2 * ↑⌈y⌉) - -(-x + 2 * ↑⌈x⌉ + y)]
/- The functional equation simplifies to
⌈x - y + ⌈y⌉ * 2⌉ * 2 = ⌈y⌉ * 2 + ⌈x⌉ * 2 or
⌈-x + y + ⌈x⌉ * 2⌉ * 2 = ⌈y⌉ * 2 + ⌈x⌉ * 2. -/
Try this: ring_nfring
refine_2IsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yK:ℤV:(IsAquaesulian fun N => -N + 2 * ↑⌈N⌉) →
{x | ∃ r, -r + 2 * ↑⌈r⌉ + (- -r + 2 * ↑⌈-r⌉) = x}.Finite ∧
↑{x | ∃ r, -r + 2 * ↑⌈r⌉ + (- -r + 2 * ↑⌈-r⌉) = x}.ncard ≤ K⊢ ∀ (x y : ℚ), ↑⌈x - y + ↑⌈y⌉ * 2⌉ * 2 = ↑⌈y⌉ * 2 + ↑⌈x⌉ * 2 ∨ ↑⌈-x + y + ↑⌈x⌉ * 2⌉ * 2 = ↑⌈y⌉ * 2 + ↑⌈x⌉ * 2
use mod_cast@?_
refine_2IsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yK:ℤV:(IsAquaesulian fun N => -N + 2 * ↑⌈N⌉) →
{x | ∃ r, -r + 2 * ↑⌈r⌉ + (- -r + 2 * ↑⌈-r⌉) = x}.Finite ∧
↑{x | ∃ r, -r + 2 * ↑⌈r⌉ + (- -r + 2 * ↑⌈-r⌉) = x}.ncard ≤ K⊢ ∀ (x y : ℚ), ⌈x - y + ↑(⌈y⌉ * 2)⌉ * 2 = ⌈y⌉ * 2 + ⌈x⌉ * 2 ∨ ⌈-x + y + ↑(⌈x⌉ * 2)⌉ * 2 = ⌈y⌉ * 2 + ⌈x⌉ * 2
/- Which is equivalent to:
(A) ⌈y⌉ + ⌈x⌉ - 1 < x - y + ⌈y⌉ * 2 ≤ ⌈y⌉ + ⌈x⌉ or
(B) ⌈y⌉ + ⌈x⌉ - 1 < -x + y + ⌈x⌉ * 2 ≤ ⌈y⌉ + ⌈x⌉ -/
norm_num[<-add_mul,Int.ceil_eq_iff]
refine_2IsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yK:ℤV:(IsAquaesulian fun N => -N + 2 * ↑⌈N⌉) →
{x | ∃ r, -r + 2 * ↑⌈r⌉ + (- -r + 2 * ↑⌈-r⌉) = x}.Finite ∧
↑{x | ∃ r, -r + 2 * ↑⌈r⌉ + (- -r + 2 * ↑⌈-r⌉) = x}.ncard ≤ K⊢ ∀ (x y : ℚ),
↑⌈y⌉ + ↑⌈x⌉ - 1 < x - y + ↑⌈y⌉ * 2 ∧ x - y + ↑⌈y⌉ * 2 ≤ ↑⌈y⌉ + ↑⌈x⌉ ∨
↑⌈y⌉ + ↑⌈x⌉ - 1 < -x + y + ↑⌈x⌉ * 2 ∧ -x + y + ↑⌈x⌉ * 2 ≤ ↑⌈y⌉ + ↑⌈x⌉
useλc K=>(em _).imp (⟨by
IsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y⊢ IsLeast
{c | ∀ (f : ℚ → ℚ), IsAquaesulian f → {x | ∃ r, f r + f (-r) = x}.Finite ∧ ↑{x | ∃ r, f r + f (-r) = x}.ncard ≤ c} 2 linarith[Int.ceil_lt_add_one c,Int.le_ceil K],.⟩) (by
IsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y⊢ IsLeast
{c | ∀ (f : ℚ → ℚ), IsAquaesulian f → {x | ∃ r, f r + f (-r) = x}.Finite ∧ ↑{x | ∃ r, f r + f (-r) = x}.ncard ≤ c} 2 repeat use by
IsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y⊢ IsLeast
{c | ∀ (f : ℚ → ℚ), IsAquaesulian f → {x | ∃ r, f r + f (-r) = x}.Finite ∧ ↑{x | ∃ r, f r + f (-r) = x}.ncard ≤ c} 2 linarith[.,Int.le_ceil c,or,Int.ceil_lt_add_one$ K])
/- If x - y + ⌈y⌉ * 2 ≤ ⌈y⌉ + ⌈x⌉ then we have the desired result (A)
since ⌈y⌉ < y + 1.
Otherwise, we have ⌈y⌉ + ⌈x⌉ < x - y + ⌈y⌉ * 2 which we negate and
add ⌈x⌉ * 2 + ⌈y⌉ * 2 to get -x + y + ⌈x⌉ * 2 < ⌈y⌉ + ⌈x⌉,
from which we get the desired result (B) since ⌈x⌉ < x + 1. -/
simp_all[Int.ceil_neg, ←add_assoc]
refine_2IsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yK:ℤV:{x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.Finite ∧ ↑{x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.ncard ≤ K⊢ 2 ≤ K
suffices:2<=V.1.toFinset.card
refine_2IsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yK:ℤV:{x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.Finite ∧ ↑{x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.ncard ≤ Kthis:2 ≤ ⋯.toFinset.card⊢ 2 ≤ K
thisIsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yK:ℤV:{x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.Finite ∧ ↑{x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.ncard ≤ K⊢ 2 ≤ ⋯.toFinset.card
·
refine_2IsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yK:ℤV:{x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.Finite ∧ ↑{x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.ncard ≤ Kthis:2 ≤ ⋯.toFinset.card⊢ 2 ≤ K let M:=V.1.toFinset
refine_2IsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yK:ℤV:{x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.Finite ∧ ↑{x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.ncard ≤ Kthis:2 ≤ ⋯.toFinset.cardM:Finset ℚ := ⋯.toFinset⊢ 2 ≤ K
norm_num[this,V.2.trans',(Set.ext$ by
IsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yK:ℤV:{x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.Finite ∧ ↑{x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.ncard ≤ Kthis:2 ≤ ⋯.toFinset.cardM:Finset ℚ := ⋯.toFinset⊢ ∀ (x : ℚ), x ∈ {x | ∃ t, 2 * ↑⌈t⌉ + -(2 * ↑⌊t⌋) = x} ↔ x ∈ ↑M simp_all[M]
All goals completed! 🐙 : {x :Rat|∃t:Rat, (↑2 ) * ( ⌈ t ⌉:(ℚ ) ) .. + (- (2 *⌊(t)⌋)) = ↑x} = M)]
/- Finally, we have f(-1) + f(1) = 0 and f(1/2) = f(-1/2) = 2
as two distinct values of f. Thus, c = 2 is tight as desired. -/
use Finset.one_lt_card.2$ by
IsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yK:ℤV:{x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.Finite ∧ ↑{x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.ncard ≤ K⊢ ∃ a ∈ ⋯.toFinset, ∃ b ∈ ⋯.toFinset, a ≠ b exists@0,V.1.mem_toFinset.2 (by
IsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yK:ℤV:{x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.Finite ∧ ↑{x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.ncard ≤ K⊢ 0 ∈ {x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x} exists-1
All goals completed! 🐙),2,V.1.mem_toFinset.2 (by
IsAquaesulian:(ℚ → ℚ) → PropIsAquaesulian_def:∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f yK:ℤV:{x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.Finite ∧ ↑{x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.ncard ≤ K⊢ 2 ∈ {x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x} exists 1/2
All goals completed! 🐙)
The following command shows which axioms the proof relies upon:
'imo_2024_p6' depends on axioms: [propext, Classical.choice, Quot.sound]#print axioms imo_2024_p6
'imo_2024_p6' depends on axioms: [propext, Classical.choice, Quot.sound]
These are the standard built in axioms.