Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Statement with defined notation
∀ n. ∀ a. ∀ b. ∀ c. ∀ d. n · 2 = a · a + b · b + c · c + d · d → (Even(a) ∧ Even(b) ∨ Odd(a) ∧ Odd(b)) ∧ (Even(c) ∧ Even(d) ∨ Odd(c) ∧ Odd(d)) ∨ ((Even(a) ∧ Even(c) ∨ Odd(a) ∧ Odd(c)) ∧ (Even(b) ∧ Even(d) ∨ Odd(b) ∧ Odd(d)) ∨ (Even(a) ∧ Even(d) ∨ Odd(a) ∧ Odd(d)) ∧ (Even(b) ∧ Even(c) ∨ Odd(b) ∧ Odd(c)))Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.
Definitions used by this theorem
In the theorem statement
In local proof propositions
none
Exact expanded first-order statement
forall n a b c d. n * 2 = a * a + b * b + c * c + d * d -> (((((((exists fsd_even_first_fsps_norm_selection_ab. a = 2 * fsd_even_first_fsps_norm_selection_ab) /\ (exists fsd_even_second_fsps_norm_selection_ab. b = 2 * fsd_even_second_fsps_norm_selection_ab)) \/ ((exists fsd_odd_first_fsps_norm_selection_ab. a = 2 * fsd_odd_first_fsps_norm_selection_ab + 1) /\ (exists fsd_odd_second_fsps_norm_selection_ab. b = 2 * fsd_odd_second_fsps_norm_selection_ab + 1)))) /\ ((((exists fsd_even_first_fsps_norm_selection_cd. c = 2 * fsd_even_first_fsps_norm_selection_cd) /\ (exists fsd_even_second_fsps_norm_selection_cd. d = 2 * fsd_even_second_fsps_norm_selection_cd)) \/ ((exists fsd_odd_first_fsps_norm_selection_cd. c = 2 * fsd_odd_first_fsps_norm_selection_cd + 1) /\ (exists fsd_odd_second_fsps_norm_selection_cd. d = 2 * fsd_odd_second_fsps_norm_selection_cd + 1))))) \/ (((((((exists fsd_even_first_fsps_norm_selection_crossed_ac. a = 2 * fsd_even_first_fsps_norm_selection_crossed_ac) /\ (exists fsd_even_second_fsps_norm_selection_crossed_ac. c = 2 * fsd_even_second_fsps_norm_selection_crossed_ac)) \/ ((exists fsd_odd_first_fsps_norm_selection_crossed_ac. a = 2 * fsd_odd_first_fsps_norm_selection_crossed_ac + 1) /\ (exists fsd_odd_second_fsps_norm_selection_crossed_ac. c = 2 * fsd_odd_second_fsps_norm_selection_crossed_ac + 1)))) /\ ((((exists fsd_even_first_fsps_norm_selection_crossed_bd. b = 2 * fsd_even_first_fsps_norm_selection_crossed_bd) /\ (exists fsd_even_second_fsps_norm_selection_crossed_bd. d = 2 * fsd_even_second_fsps_norm_selection_crossed_bd)) \/ ((exists fsd_odd_first_fsps_norm_selection_crossed_bd. b = 2 * fsd_odd_first_fsps_norm_selection_crossed_bd + 1) /\ (exists fsd_odd_second_fsps_norm_selection_crossed_bd. d = 2 * fsd_odd_second_fsps_norm_selection_crossed_bd + 1))))) \/ (((((exists fsd_even_first_fsps_norm_selection_crossed_ad. a = 2 * fsd_even_first_fsps_norm_selection_crossed_ad) /\ (exists fsd_even_second_fsps_norm_selection_crossed_ad. d = 2 * fsd_even_second_fsps_norm_selection_crossed_ad)) \/ ((exists fsd_odd_first_fsps_norm_selection_crossed_ad. a = 2 * fsd_odd_first_fsps_norm_selection_crossed_ad + 1) /\ (exists fsd_odd_second_fsps_norm_selection_crossed_ad. d = 2 * fsd_odd_second_fsps_norm_selection_crossed_ad + 1)))) /\ ((((exists fsd_even_first_fsps_norm_selection_crossed_bc. b = 2 * fsd_even_first_fsps_norm_selection_crossed_bc) /\ (exists fsd_even_second_fsps_norm_selection_crossed_bc. c = 2 * fsd_even_second_fsps_norm_selection_crossed_bc)) \/ ((exists fsd_odd_first_fsps_norm_selection_crossed_bc. b = 2 * fsd_odd_first_fsps_norm_selection_crossed_bc + 1) /\ (exists fsd_odd_second_fsps_norm_selection_crossed_bc. c = 2 * fsd_odd_second_fsps_norm_selection_crossed_bc + 1)))))))))Proof neighborhood
Direct theorem prerequisites
FS003U four_square_parity_even_norm_coordinate_sum FS003W four_square_parity_even_coordinate_pair_selectionDirect theorem dependents
Definition-aware tactic body
Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.