Showcase / sq-add-sq-eq-three-mul-sq-s3

div_three_descends_sq_add_sq_eq_three_mul_sq

proved

difficulty 1

Proved by @cgbarlow. Kernel-verified at Gate A; no human in the correctness path.

Original target

The goal record the swarm was asked to discharge — the source of truth for this proof's identity and difficulty.

sq-add-sq-eq-three-mul-sq-s3AISP goal record →Lean statement →

Effort & telemetry

Difficulty: 1
Runs: 1
Successes: 1
Provider attempts: 2

Statement

The Lean statement the swarm proved, kernel-verified at Gate A.

goals/sq-add-sq-eq-three-mul-sq-s3.lean

import Mathlib

theorem div_three_descends_sq_add_sq_eq_three_mul_sq (x y z : ℤ) (h : x ^ 2 + y ^ 2 = 3 * z ^ 2) (hnonzero : x ≠ 0 ∨ y ≠ 0 ∨ z ≠ 0) : ∃ x1 y1 z1 : ℤ, x1 ^ 2 + y1 ^ 2 = 3 * z1 ^ 2 ∧ Int.natAbs x1 + Int.natAbs y1 + Int.natAbs z1 < Int.natAbs x + Int.natAbs y + Int.natAbs z := by
  sorry