Erdős Problem 633

Reference:

• erdosproblems.com/633
• [So09] Soifer, Alexander, How Does One Cut a Triangle? I
• [So09c] Soifer, Alexander, Is there anything beyond the solution?

def Erdos633.IsCuttable (n : ℕ) (T : Affine.Triangle ℝ (EuclideanSpace ℝ (Fin 2))) : Prop

A triangle is n-cuttable if it can be decomposed into n congruent triangles.

Equations

• One or more equations did not get rendered due to their size.

theorem Erdos633.IsCuttable.ne_zero {n : ℕ} {T : Affine.Triangle ℝ (EuclideanSpace ℝ (Fin 2))} (hT : IsCuttable n T) : n ≠ 0

A triangle isn't cuttable into zero triangles.

theorem Erdos633.IsCuttable.sq {n : ℕ} {T : Affine.Triangle ℝ (EuclideanSpace ℝ (Fin 2))} (hn : n ≠ 0) : IsCuttable (n ^ 2) T

Every triangle is cuttable into any non-zero square number of congruent triangles.

theorem Erdos633.IsCuttable.of_isSquare {n : ℕ} {T : Affine.Triangle ℝ (EuclideanSpace ℝ (Fin 2))} (hn₀ : n ≠ 0) (hn : IsSquare n) : IsCuttable n T

Every triangle is cuttable into any non-zero square number of congruent triangles.

theorem Erdos633.isCuttable_iff_isSquare_of_linearIndependent {n : ℕ} {T : Affine.Triangle ℝ (EuclideanSpace ℝ (Fin 2))} (hTsides : LinearIndependent ℤ ![dist (T.points 0) (T.points 1), dist (T.points 1) (T.points 2), dist (T.points 2) (T.points 0)]) (hTangles : LinearIndependent ℤ ![EuclideanGeometry.angle (T.points 0) (T.points 1) (T.points 2), EuclideanGeometry.angle (T.points 1) (T.points 2) (T.points 0), EuclideanGeometry.angle (T.points 2) (T.points 0) (T.points 1)]) : IsCuttable n T ↔ n ≠ 0 ∧ IsSquare n

A triangle whose side lengths and angles are integrally independent is cuttable only into a non-zero square number of congruent triangles. This is proved in [So09c].

theorem Erdos633.erdos_633 {T : Affine.Triangle ℝ (EuclideanSpace ℝ (Fin 2))} : T ∈ sorry ↔ ∀ (n : ℕ), IsCuttable n T → IsSquare n

Which triangles can only be decomposed into a square number of congruent triangles?

def Erdos633.IsSimiliCuttable (n : ℕ) (T : Affine.Triangle ℝ (EuclideanSpace ℝ (Fin 2))) : Prop

A triangle is n-simili-cuttable if it can be decomposed into n similar triangles.

Equations

• One or more equations did not get rendered due to their size.

theorem Erdos633.IsSimiliCuttable.ne_zero {n : ℕ} {T : Affine.Triangle ℝ (EuclideanSpace ℝ (Fin 2))} (hT : IsSimiliCuttable n T) : n ≠ 0

A triangle isn't simili-cuttable into zero triangles.

theorem Erdos633.IsSimiliCuttable.of_ne_zero_two_three_five {n : ℕ} {T : Affine.Triangle ℝ (EuclideanSpace ℝ (Fin 2))} (hn₀ : n ≠ 0) (hn₂ : n ≠ 2) (hn₃ : n ≠ 3) (hn₅ : n ≠ 5) : IsSimiliCuttable n T

Every triangle is simili-cuttable into any number of similar triangles, except 0, 2, 3, 5. This is proved in [So09].

theorem Erdos633.exists_isSimiliCuttable_iff_ne_zero_two_three_five : ∃ (T : Affine.Triangle ℝ (EuclideanSpace ℝ (Fin 2))), ∀ (n : ℕ), IsSimiliCuttable n T ↔ n ≠ 0 ∧ n ≠ 2 ∧ n ≠ 3 ∧ n ≠ 5

There exists a triangle which isn't simili-cuttable into 0, 2, 3, 5 parts. This is proved in [So09].