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.
Exact expanded first-order arithmetic 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 n. (exists fsl_a_fslf_natural fsl_b_fslf_natural fsl_c_fslf_natural fsl_d_fslf_natural. (n) = fsl_a_fslf_natural * fsl_a_fslf_natural + fsl_b_fslf_natural * fsl_b_fslf_natural + fsl_c_fslf_natural * fsl_c_fslf_natural + fsl_d_fslf_natural * fsl_d_fslf_natural)Constructive proof overview
Generated structural guide
Universal Lagrange follows constructively from exactly one visible remaining hypothesis: representation of each odd signed centered quaternion quotient.
The unchanged tactic script uses 2 declared prerequisites and contains 4 exact native proof lines.
dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged
Proof neighborhood
Direct dependencies
Direct dependents
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This dependency-curried candidate body does not grant checked theorem use or Stable membership.
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
Original exact command ledger · 4 lines
- 0001
intro hsigned - 0002
apply four_square_lagrange_from_all_primes - 0003
apply four_square_prime_from_odd_signed_quaternion - 0004
exact hsigned