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. Prime(x) → ¬y = 0 → ¬y = 1 → (∃ 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))) → ∀ 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
Exact expanded first-order statement
(forall fsd_prime_bridge fsd_multiplier_bridge. ((~(fsd_prime_bridge = 1) /\ forall frm_prime_left_fsd_bridge_prime frm_prime_right_fsd_bridge_prime. fsd_prime_bridge = frm_prime_left_fsd_bridge_prime * frm_prime_right_fsd_bridge_prime -> frm_prime_left_fsd_bridge_prime = 1 \/ frm_prime_right_fsd_bridge_prime = 1)) -> ~(fsd_multiplier_bridge = 0) -> ~(fsd_multiplier_bridge = 1) -> (exists fsl_a_fsd_bridge_source fsl_b_fsd_bridge_source fsl_c_fsd_bridge_source fsl_d_fsd_bridge_source. (fsd_prime_bridge * fsd_multiplier_bridge) = fsl_a_fsd_bridge_source * fsl_a_fsd_bridge_source + fsl_b_fsd_bridge_source * fsl_b_fsd_bridge_source + fsl_c_fsd_bridge_source * fsl_c_fsd_bridge_source + fsl_d_fsd_bridge_source * fsl_d_fsd_bridge_source) -> exists fsd_smaller_bridge. (~(fsd_smaller_bridge = 0) /\ ((exists fsd_gap_bridge. fsd_gap_bridge + S fsd_smaller_bridge = fsd_multiplier_bridge) /\ (exists fsl_a_fsd_bridge_target fsl_b_fsd_bridge_target fsl_c_fsd_bridge_target fsl_d_fsd_bridge_target. (fsd_prime_bridge * fsd_smaller_bridge) = fsl_a_fsd_bridge_target * fsl_a_fsd_bridge_target + fsl_b_fsd_bridge_target * fsl_b_fsd_bridge_target + fsl_c_fsd_bridge_target * fsl_c_fsd_bridge_target + fsl_d_fsd_bridge_target * fsl_d_fsd_bridge_target)))) -> forall p. ((~(p = 1) /\ forall frm_prime_left_fslb_prime frm_prime_right_fslb_prime. p = frm_prime_left_fslb_prime * frm_prime_right_fslb_prime -> frm_prime_left_fslb_prime = 1 \/ frm_prime_right_fslb_prime = 1)) -> (exists fsl_a_fslb_prime_result fsl_b_fslb_prime_result fsl_c_fslb_prime_result fsl_d_fslb_prime_result. (p) = fsl_a_fslb_prime_result * fsl_a_fslb_prime_result + fsl_b_fslb_prime_result * fsl_b_fslb_prime_result + fsl_c_fslb_prime_result * fsl_c_fslb_prime_result + fsl_d_fslb_prime_result * fsl_d_fslb_prime_result)Proof neighborhood
Direct theorem prerequisites
Direct 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–3
02Establish hseedL4–7
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square prime modular seed.
- L4
have hseed : ∃ a. ∃ b. Dvd(p,a · a + b · b + 1)Definitions: Dvd(p,a · a + b · b + 1)Original native command in the exact edition - L5
specialize four_square_prime_modular_seed p - L6
apply four_square_prime_modular_seed - L7
exact hprime
03Separate the logical casesL8–10
04Establish hdescentL11–20
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square descent prime from modular seed and step.
- L11
have hdescent : ∀ q. ∀ a. ∀ b. ∀ k. Prime(q) → a · a + b · b + 1 = q · k → ∃ x. ∃ y. ∃ z. ∃ n. q = x · x + y · y + z · z + n · nDefinitions: Prime(q)Original native command in the exact edition - L12
apply four_square_descent_prime_from_modular_seed_and_step - L13
exact hstep - L14
specialize hdescent p - L15
specialize hdescent x - L16
specialize hdescent x1 - L17
specialize hdescent x2 - L18
apply hdescent - L19
exact hprime - L20
exact hseed_witness_witness_witness
Original defined command ledger · 20 lines
- 0001
intro hstep - 0002
intro p - 0003
intro hprime - 0004
have hseed : ∃ a. ∃ b. Dvd(p,a · a + b · b + 1)Exact native replay line
have hseed : exists a b k. a * a + b * b + 1 = p * k - 0005
specialize four_square_prime_modular_seed p - 0006
apply four_square_prime_modular_seed - 0007
exact hprime - 0008
cases hseed - 0009
cases hseed_witness - 0010
cases hseed_witness_witness - 0011
have hdescent : ∀ q. ∀ a. ∀ b. ∀ k. Prime(q) → a · a + b · b + 1 = q · k → ∃ x. ∃ y. ∃ z. ∃ n. q = x · x + y · y + z · z + n · nExact native replay line
have hdescent : forall q a b k. ((~(q = 1) /\ forall frm_prime_left_fslb_local_prime frm_prime_right_fslb_local_prime. q = frm_prime_left_fslb_local_prime * frm_prime_right_fslb_local_prime -> frm_prime_left_fslb_local_prime = 1 \/ frm_prime_right_fslb_local_prime = 1)) -> a * a + b * b + 1 = q * k -> (exists fsl_a_fslb_local_result fsl_b_fslb_local_result fsl_c_fslb_local_result fsl_d_fslb_local_result. (q) = fsl_a_fslb_local_result * fsl_a_fslb_local_result + fsl_b_fslb_local_result * fsl_b_fslb_local_result + fsl_c_fslb_local_result * fsl_c_fslb_local_result + fsl_d_fslb_local_result * fsl_d_fslb_local_result) - 0012
apply four_square_descent_prime_from_modular_seed_and_step - 0013
exact hstep - 0014
specialize hdescent p - 0015
specialize hdescent x - 0016
specialize hdescent x1 - 0017
specialize hdescent x2 - 0018
apply hdescent - 0019
exact hprime - 0020
exact hseed_witness_witness_witness