module
public import Mathlib.Tactic
public import Mathlib.Algebra.Order.Floor.Semiring
public import Mathlib.Analysis.SpecialFunctions.Pow.Real
public section
/-!
# International Mathematical Olympiad 1976, Problem 3
A rectangular box can be completely filled with unit cubes. If one places
as many cubes as possible, each with volume 2, in the box, with their edges
parallel to the edges of the box, one can fill exactly 40% of the box.
Determine the possible dimensions of the box.
# Formalization
The box has integer dimensions `a ≤ b ≤ c`. A cube of volume `2` has side
length `k = ∛2` (the real cube root of two). A placement of such cubes in the
box, with edges parallel to the edges of the box, is formalized as a finite set
`P` of corner positions satisfying `IsPacking a b c P`: every cube lies inside
the box and distinct cubes have disjoint interiors (`NonOverlapping`).
The maximal number of cubes that fit is
`maxNumCubes a b c = ⌊a / k⌋₊ * ⌊b / k⌋₊ * ⌊c / k⌋₊`: along an edge of
integer length `n` exactly `⌊n / k⌋₊` cubes fit. The maximality is proved
formally rather than asserted: `packing_card_le` shows that no packing has more
cubes (the map sending a cube at `(x, y, z)` to the triple
`(⌊x / k⌋₊, ⌊y / k⌋₊, ⌊z / k⌋₊)` is injective on a packing), and
`exists_packing` shows that the grid arrangement attains the bound.
The "exactly 40%" condition is stated explicitly as
`2 * P.card = 40 / 100 * (a * b * c)` for a maximal packing `P`: the total
volume of the cubes is 40% of the box volume. Since a maximal packing has
`P.card = maxNumCubes a b c`, this is equivalent to
`a * b * c = 5 * (⌊a / k⌋₊ * ⌊b / k⌋₊ * ⌊c / k⌋₊)`, which is the form used
by the integer-arithmetic core of the proof.
-/
namespace Imo1976P3
/-- The side length of a cube of volume 2: the real cube root of 2. -/
noncomputable def k : ℝ := (2 : ℝ) ^ (3 : ℝ)⁻¹
/-- A placement of a cube of side `k` in the `a × b × c` box: the cube is the
closed box `[p.1, p.1 + k] × [p.2.1, p.2.1 + k] × [p.2.2, p.2.2 + k]`, and it
must be contained in `[0, a] × [0, b] × [0, c]`. -/
noncomputable abbrev CubeInBox (a b c : ℕ) (p : ℝ × ℝ × ℝ) : Prop :=
0 ≤ p.1 ∧ p.1 + k ≤ a ∧ 0 ≤ p.2.1 ∧ p.2.1 + k ≤ b ∧ 0 ≤ p.2.2 ∧ p.2.2 + k ≤ c
/-- Two cubes of side `k` placed at `p` and `q` do not overlap: their interiors
are disjoint, i.e. they are separated along at least one axis. -/
noncomputable abbrev NonOverlapping (p q : ℝ × ℝ × ℝ) : Prop :=
p.1 + k ≤ q.1 ∨ q.1 + k ≤ p.1 ∨
p.2.1 + k ≤ q.2.1 ∨ q.2.1 + k ≤ p.2.1 ∨
p.2.2 + k ≤ q.2.2 ∨ q.2.2 + k ≤ p.2.2
/-- A packing of the `a × b × c` box by cubes of volume 2 (side `k = ∛2`), with
edges parallel to the edges of the box: a finite set of cube positions inside
the box, pairwise non-overlapping. -/
structure IsPacking (a b c : ℕ) (P : Finset (ℝ × ℝ × ℝ)) : Prop where
inBox : ∀ p ∈ P, CubeInBox a b c p
nonOverlapping : ∀ p ∈ P, ∀ q ∈ P, p ≠ q → NonOverlapping p q
/-- The maximal number of cubes of volume 2 that can be placed in the
`a × b × c` box with edges parallel to the edges of the box: along an edge of
integer length `n` exactly `⌊n / k⌋₊` cubes fit. That this is indeed the
maximum is proved in `packing_card_le` (upper bound) and `exists_packing`
(the grid arrangement attains it). -/
noncomputable def maxNumCubes (a b c : ℕ) : ℕ :=
⌊(a : ℝ) / k⌋₊ * ⌊(b : ℝ) / k⌋₊ * ⌊(c : ℝ) / k⌋₊
/- determine -/ abbrev solution_set : Set (ℕ × ℕ × ℕ) := sorry
theorem imo1976_p3 (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
(hab : a ≤ b) (hbc : b ≤ c) :
⟨a, b, c⟩ ∈ solution_set ↔
∃ P : Finset (ℝ × ℝ × ℝ), IsPacking a b c P ∧
(∀ P' : Finset (ℝ × ℝ × ℝ), IsPacking a b c P' → P'.card ≤ P.card) ∧
(2 : ℝ) * P.card = 40 / 100 * (a * b * c : ℝ) := sorry
end Imo1976P3
This problem has a complete formalized solution.