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
(∀ x. ∀ y. ∀ z. ∀ n. ∀ m. ∀ k. ∀ i. ∀ j. ∀ u. ∀ v. ∀ w. ∀ x0. ¬y = 0 → y = 2 · z + 1 → x · y = n · n + m · m + k · k + i · i → Le(j + j,y) ∧ ((∃ x1. n = y · x1 + j) ∨ Dvd(y,n + j)) → Le(u + u,y) ∧ ((∃ x1. m = y · x1 + u) ∨ Dvd(y,m + u)) → Le(v + v,y) ∧ ((∃ x1. k = y · x1 + v) ∨ Dvd(y,k + v)) → Le(w + w,y) ∧ ((∃ x1. i = y · x1 + w) ∨ Dvd(y,i + w)) → y · x0 = j · j + u · u + v · v + w · w → ∃ x1. ∃ x2. ∃ x3. ∃ x4. x · x0 = x1 · x1 + x2 · x2 + x3 · x3 + x4 · x4) → ∀ x. Prime(x) → ∃ y. ∃ z. ∃ n. ∃ m. x = y · y + z · z + n · n + m · mEvery 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 fsbr_modulus_final fsbr_multiplier_final fsbr_half_final fsbr_coordinate_final_0 fsbr_coordinate_final_1 fsbr_coordinate_final_2 fsbr_coordinate_final_3 fsbr_center_final_0 fsbr_center_final_1 fsbr_center_final_2 fsbr_center_final_3 fsbr_quotient_final. ~(fsbr_multiplier_final = 0) -> fsbr_multiplier_final = 2 * fsbr_half_final + 1 -> fsbr_modulus_final * fsbr_multiplier_final = fsbr_coordinate_final_0 * fsbr_coordinate_final_0 + fsbr_coordinate_final_1 * fsbr_coordinate_final_1 + fsbr_coordinate_final_2 * fsbr_coordinate_final_2 + fsbr_coordinate_final_3 * fsbr_coordinate_final_3 -> (((exists fsd_center_bound_final_0. fsd_center_bound_final_0 + (fsbr_center_final_0 + fsbr_center_final_0) = fsbr_multiplier_final) /\ ((exists fsd_center_lower_final_0. fsbr_coordinate_final_0 = fsbr_multiplier_final * fsd_center_lower_final_0 + fsbr_center_final_0) \/ (exists fsd_center_upper_final_0. fsbr_coordinate_final_0 + fsbr_center_final_0 = fsbr_multiplier_final * fsd_center_upper_final_0)))) -> (((exists fsd_center_bound_final_1. fsd_center_bound_final_1 + (fsbr_center_final_1 + fsbr_center_final_1) = fsbr_multiplier_final) /\ ((exists fsd_center_lower_final_1. fsbr_coordinate_final_1 = fsbr_multiplier_final * fsd_center_lower_final_1 + fsbr_center_final_1) \/ (exists fsd_center_upper_final_1. fsbr_coordinate_final_1 + fsbr_center_final_1 = fsbr_multiplier_final * fsd_center_upper_final_1)))) -> (((exists fsd_center_bound_final_2. fsd_center_bound_final_2 + (fsbr_center_final_2 + fsbr_center_final_2) = fsbr_multiplier_final) /\ ((exists fsd_center_lower_final_2. fsbr_coordinate_final_2 = fsbr_multiplier_final * fsd_center_lower_final_2 + fsbr_center_final_2) \/ (exists fsd_center_upper_final_2. fsbr_coordinate_final_2 + fsbr_center_final_2 = fsbr_multiplier_final * fsd_center_upper_final_2)))) -> (((exists fsd_center_bound_final_3. fsd_center_bound_final_3 + (fsbr_center_final_3 + fsbr_center_final_3) = fsbr_multiplier_final) /\ ((exists fsd_center_lower_final_3. fsbr_coordinate_final_3 = fsbr_multiplier_final * fsd_center_lower_final_3 + fsbr_center_final_3) \/ (exists fsd_center_upper_final_3. fsbr_coordinate_final_3 + fsbr_center_final_3 = fsbr_multiplier_final * fsd_center_upper_final_3)))) -> fsbr_multiplier_final * fsbr_quotient_final = fsbr_center_final_0 * fsbr_center_final_0 + fsbr_center_final_1 * fsbr_center_final_1 + fsbr_center_final_2 * fsbr_center_final_2 + fsbr_center_final_3 * fsbr_center_final_3 -> (exists fsl_a_fsbr_signed_final fsl_b_fsbr_signed_final fsl_c_fsbr_signed_final fsl_d_fsbr_signed_final. (fsbr_modulus_final * fsbr_quotient_final) = fsl_a_fsbr_signed_final * fsl_a_fsbr_signed_final + fsl_b_fsbr_signed_final * fsl_b_fsbr_signed_final + fsl_c_fsbr_signed_final * fsl_c_fsbr_signed_final + fsl_d_fsbr_signed_final * fsl_d_fsbr_signed_final)) -> forall p. ((~(p = 1) /\ forall frm_prime_left_fslf_prime frm_prime_right_fslf_prime. p = frm_prime_left_fslf_prime * frm_prime_right_fslf_prime -> frm_prime_left_fslf_prime = 1 \/ frm_prime_right_fslf_prime = 1)) -> (exists fsl_a_fslf_prime fsl_b_fslf_prime fsl_c_fslf_prime fsl_d_fslf_prime. (p) = fsl_a_fslf_prime * fsl_a_fslf_prime + fsl_b_fslf_prime * fsl_b_fslf_prime + fsl_c_fslf_prime * fsl_c_fslf_prime + fsl_d_fslf_prime * fsl_d_fslf_prime)Proof neighborhood
Direct theorem prerequisites
FS000U four_square_bounded_strict_descent_from_odd_signed_quaternion FS0035 four_square_prime_from_bounded_strict_descentDirect 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.
Named ingredients (2)
01Fix variables and assumptionsL1–1
Work with arbitrary variables or the premises of the current implication.
- L1
intro hsigned