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. ∀ y. Prime(x) → ¬y = 0 → ¬y = 1 → Lt(y,x) → (∃ z. ∃ n. ∃ m. ∃ k. x · y = z · z + n · n + m · m + k · k) → ∃ z. ¬z = 0 ∧ (Lt(z,y) ∧ (∃ n. ∃ m. ∃ k. ∃ i. x · z = n · n + m · m + k · k + i · i))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
Exact expanded first-order statement
(forall fsbr_modulus_branch fsbr_multiplier_branch fsbr_half_branch fsbr_coordinate_branch_0 fsbr_coordinate_branch_1 fsbr_coordinate_branch_2 fsbr_coordinate_branch_3 fsbr_center_branch_0 fsbr_center_branch_1 fsbr_center_branch_2 fsbr_center_branch_3 fsbr_quotient_branch. ~(fsbr_multiplier_branch = 0) -> fsbr_multiplier_branch = 2 * fsbr_half_branch + 1 -> fsbr_modulus_branch * fsbr_multiplier_branch = fsbr_coordinate_branch_0 * fsbr_coordinate_branch_0 + fsbr_coordinate_branch_1 * fsbr_coordinate_branch_1 + fsbr_coordinate_branch_2 * fsbr_coordinate_branch_2 + fsbr_coordinate_branch_3 * fsbr_coordinate_branch_3 -> (((exists fsd_center_bound_branch_0. fsd_center_bound_branch_0 + (fsbr_center_branch_0 + fsbr_center_branch_0) = fsbr_multiplier_branch) /\ ((exists fsd_center_lower_branch_0. fsbr_coordinate_branch_0 = fsbr_multiplier_branch * fsd_center_lower_branch_0 + fsbr_center_branch_0) \/ (exists fsd_center_upper_branch_0. fsbr_coordinate_branch_0 + fsbr_center_branch_0 = fsbr_multiplier_branch * fsd_center_upper_branch_0)))) -> (((exists fsd_center_bound_branch_1. fsd_center_bound_branch_1 + (fsbr_center_branch_1 + fsbr_center_branch_1) = fsbr_multiplier_branch) /\ ((exists fsd_center_lower_branch_1. fsbr_coordinate_branch_1 = fsbr_multiplier_branch * fsd_center_lower_branch_1 + fsbr_center_branch_1) \/ (exists fsd_center_upper_branch_1. fsbr_coordinate_branch_1 + fsbr_center_branch_1 = fsbr_multiplier_branch * fsd_center_upper_branch_1)))) -> (((exists fsd_center_bound_branch_2. fsd_center_bound_branch_2 + (fsbr_center_branch_2 + fsbr_center_branch_2) = fsbr_multiplier_branch) /\ ((exists fsd_center_lower_branch_2. fsbr_coordinate_branch_2 = fsbr_multiplier_branch * fsd_center_lower_branch_2 + fsbr_center_branch_2) \/ (exists fsd_center_upper_branch_2. fsbr_coordinate_branch_2 + fsbr_center_branch_2 = fsbr_multiplier_branch * fsd_center_upper_branch_2)))) -> (((exists fsd_center_bound_branch_3. fsd_center_bound_branch_3 + (fsbr_center_branch_3 + fsbr_center_branch_3) = fsbr_multiplier_branch) /\ ((exists fsd_center_lower_branch_3. fsbr_coordinate_branch_3 = fsbr_multiplier_branch * fsd_center_lower_branch_3 + fsbr_center_branch_3) \/ (exists fsd_center_upper_branch_3. fsbr_coordinate_branch_3 + fsbr_center_branch_3 = fsbr_multiplier_branch * fsd_center_upper_branch_3)))) -> fsbr_multiplier_branch * fsbr_quotient_branch = fsbr_center_branch_0 * fsbr_center_branch_0 + fsbr_center_branch_1 * fsbr_center_branch_1 + fsbr_center_branch_2 * fsbr_center_branch_2 + fsbr_center_branch_3 * fsbr_center_branch_3 -> (exists fsl_a_fsbr_signed_branch fsl_b_fsbr_signed_branch fsl_c_fsbr_signed_branch fsl_d_fsbr_signed_branch. (fsbr_modulus_branch * fsbr_quotient_branch) = fsl_a_fsbr_signed_branch * fsl_a_fsbr_signed_branch + fsl_b_fsbr_signed_branch * fsl_b_fsbr_signed_branch + fsl_c_fsbr_signed_branch * fsl_c_fsbr_signed_branch + fsl_d_fsbr_signed_branch * fsl_d_fsbr_signed_branch)) -> (forall fslb_bounded_prime_branch fslb_bounded_multiplier_branch. ((~(fslb_bounded_prime_branch = 1) /\ forall frm_prime_left_fslb_bounded_prime_branch frm_prime_right_fslb_bounded_prime_branch. fslb_bounded_prime_branch = frm_prime_left_fslb_bounded_prime_branch * frm_prime_right_fslb_bounded_prime_branch -> frm_prime_left_fslb_bounded_prime_branch = 1 \/ frm_prime_right_fslb_bounded_prime_branch = 1)) -> ~(fslb_bounded_multiplier_branch = 0) -> ~(fslb_bounded_multiplier_branch = 1) -> (exists fslb_bounded_upper_gap_branch. fslb_bounded_upper_gap_branch + S fslb_bounded_multiplier_branch = fslb_bounded_prime_branch) -> (exists fsl_a_fslb_bounded_source_branch fsl_b_fslb_bounded_source_branch fsl_c_fslb_bounded_source_branch fsl_d_fslb_bounded_source_branch. (fslb_bounded_prime_branch * fslb_bounded_multiplier_branch) = fsl_a_fslb_bounded_source_branch * fsl_a_fslb_bounded_source_branch + fsl_b_fslb_bounded_source_branch * fsl_b_fslb_bounded_source_branch + fsl_c_fslb_bounded_source_branch * fsl_c_fslb_bounded_source_branch + fsl_d_fslb_bounded_source_branch * fsl_d_fslb_bounded_source_branch) -> exists fslb_bounded_smaller_branch. (~(fslb_bounded_smaller_branch = 0) /\ ((exists fslb_bounded_lower_gap_branch. fslb_bounded_lower_gap_branch + S fslb_bounded_smaller_branch = fslb_bounded_multiplier_branch) /\ (exists fsl_a_fslb_bounded_target_branch fsl_b_fslb_bounded_target_branch fsl_c_fslb_bounded_target_branch fsl_d_fslb_bounded_target_branch. (fslb_bounded_prime_branch * fslb_bounded_smaller_branch) = fsl_a_fslb_bounded_target_branch * fsl_a_fslb_bounded_target_branch + fsl_b_fslb_bounded_target_branch * fsl_b_fslb_bounded_target_branch + fsl_c_fslb_bounded_target_branch * fsl_c_fslb_bounded_target_branch + fsl_d_fslb_bounded_target_branch * fsl_d_fslb_bounded_target_branch))))Proof neighborhood
Direct theorem prerequisites
parity_cases · Stable closed
FS000S four_square_branch_even_represented_strict_step FS000T four_square_branch_odd_represented_strict_stepDirect 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–8
02Establish hparityL9–11
03Separate the logical casesL12–13
04Use earlier factsL14–20
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L14
specialize four_square_branch_even_represented_strict_step p - L15
specialize four_square_branch_even_represented_strict_step k - L16
specialize four_square_branch_even_represented_strict_step x - L17
apply four_square_branch_even_represented_strict_step - L18
exact hnonzero - L19
exact hparity_witness_left - L20
exact hrepresented
05Establish hoddstepL21–30
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square branch odd represented strict step.
- L21
have hoddstep : ∀ q. ∀ j. ∀ t. Prime(q) → ¬j = 0 → ¬j = 1 → Lt(j,q) → j = 2 · t + 1 → (∃ x. ∃ y. ∃ z. ∃ n. q · j = x · x + y · y + z · z + n · n) → ∃ x. ¬x = 0 ∧ (Lt(x,j) ∧ (∃ y. ∃ z. ∃ n. ∃ m. q · x = y · y + z · z + n · n + m · m))Definitions: Prime(q)Lt(j,q)Lt(x,j)Original native command in the exact edition - L22
apply four_square_branch_odd_represented_strict_step - L23
exact hsigned - L24
specialize hoddstep p - L25
specialize hoddstep k - L26
specialize hoddstep x - L27
apply hoddstep - L28
exact hprime - L29
exact hnonzero - L30
exact hnonunit
Original defined command ledger · 33 lines
- 0001
intro hsigned - 0002
intro p - 0003
intro k - 0004
intro hprime - 0005
intro hnonzero - 0006
intro hnonunit - 0007
intro hproper - 0008
intro hrepresented - 0009
have hparity : exists h. k = 2 * h \/ k = 2 * h + 1 - 0010
specialize parity_cases k - 0011
exact parity_cases - 0012
cases hparity - 0013
cases hparity_witness - 0014
specialize four_square_branch_even_represented_strict_step p - 0015
specialize four_square_branch_even_represented_strict_step k - 0016
specialize four_square_branch_even_represented_strict_step x - 0017
apply four_square_branch_even_represented_strict_step - 0018
exact hnonzero - 0019
exact hparity_witness_left - 0020
exact hrepresented - 0021
have hoddstep : ∀ q. ∀ j. ∀ t. Prime(q) → ¬j = 0 → ¬j = 1 → Lt(j,q) → j = 2 · t + 1 → (∃ x. ∃ y. ∃ z. ∃ n. q · j = x · x + y · y + z · z + n · n) → ∃ x. ¬x = 0 ∧ (Lt(x,j) ∧ (∃ y. ∃ z. ∃ n. ∃ m. q · x = y · y + z · z + n · n + m · m))Exact native replay line
have hoddstep : forall q j t. ((~(q = 1) /\ forall frm_prime_left_fsbr_local_prime frm_prime_right_fsbr_local_prime. q = frm_prime_left_fsbr_local_prime * frm_prime_right_fsbr_local_prime -> frm_prime_left_fsbr_local_prime = 1 \/ frm_prime_right_fsbr_local_prime = 1)) -> ~(j = 0) -> ~(j = 1) -> (exists gap. gap + S j = q) -> j = 2 * t + 1 -> (exists fsl_a_fsbr_local_source fsl_b_fsbr_local_source fsl_c_fsbr_local_source fsl_d_fsbr_local_source. (q * j) = fsl_a_fsbr_local_source * fsl_a_fsbr_local_source + fsl_b_fsbr_local_source * fsl_b_fsbr_local_source + fsl_c_fsbr_local_source * fsl_c_fsbr_local_source + fsl_d_fsbr_local_source * fsl_d_fsbr_local_source) -> exists r. (~(r = 0) /\ ((exists gap. gap + S r = j) /\ (exists fsl_a_fsbr_local_result fsl_b_fsbr_local_result fsl_c_fsbr_local_result fsl_d_fsbr_local_result. (q * r) = fsl_a_fsbr_local_result * fsl_a_fsbr_local_result + fsl_b_fsbr_local_result * fsl_b_fsbr_local_result + fsl_c_fsbr_local_result * fsl_c_fsbr_local_result + fsl_d_fsbr_local_result * fsl_d_fsbr_local_result))) - 0022
apply four_square_branch_odd_represented_strict_step - 0023
exact hsigned - 0024
specialize hoddstep p - 0025
specialize hoddstep k - 0026
specialize hoddstep x - 0027
apply hoddstep - 0028
exact hprime - 0029
exact hnonzero - 0030
exact hnonunit - 0031
exact hproper - 0032
exact hparity_witness_right - 0033
exact hrepresented