Unique Crystal Components

Reference: arxiv/1601.03081 The Biharmonic mean by Marco Abrate, Stefano Barbero, Umberto Cerruti, Nadir Murru

def IsCrystalWithComponents (n a b : ℕ) : Prop

An odd number $n$ is called a crystal if $n = ab$, with $a, b > 1$ and $B(a, b) ∈ ℕ$, where $B(a, b) := ((a + b)^2 + (a b + 1)^2) / (2 (a + 1) (b + 1))$.

Equations

• IsCrystalWithComponents n a b = (Odd n ∧ 1 < a ∧ 1 < b ∧ n = a * b ∧ 2 * (a + 1) * (b + 1) ∣ (a + b) ^ 2 + (a * b + 1) ^ 2)

theorem crystals_components_unique (n a b c d : ℕ) (hab : IsCrystalWithComponents n a b) (hcd : IsCrystalWithComponents n c d) : {a, b} = {c, d}

If $n = ab$ is a crystal, then there are no other pairs of positive integers $c, d > 1$, different from the couple $a, b$, such that $n = cd$ and $B(c, d) ∈ ℕ$, i.e., the components of the crystals are unique.