FS003M

four_square_prime_from_odd_signed_quaternion

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

The actual bounded modular prime seed, complete even branch, centered odd bounds, and terminating descent reduce representation of every prime to the single signed odd quaternion identity.

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 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)

Constructive proof overview

Generated structural guide

The actual bounded modular prime seed, complete even branch, centered odd bounds, and terminating descent reduce representation of every prime to the single signed odd quaternion identity.

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

FS000U four_square_bounded_strict_descent_from_odd_signed_quaternion FS0035 four_square_prime_from_bounded_strict_descent

Direct dependents

FS003N four_square_lagrange_from_odd_signed_quaternion FS003O four_square_prime_representation

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

4 script commands · 2 reading checkpoints · 0 local claims

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)
four square bounded strict descent from odd signed quaternionfour square prime from bounded strict descent
01Fix variables and assumptionsL1–1

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro hsigned
02Use earlier factsL2–4

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L2
    apply four_square_prime_from_bounded_strict_descent
  2. L3
    apply four_square_bounded_strict_descent_from_odd_signed_quaternion
  3. L4
    exact hsigned

Library-wide reading audit

Original exact command ledger · 4 lines
  1. 0001intro hsigned
  2. 0002apply four_square_prime_from_bounded_strict_descent
  3. 0003apply four_square_bounded_strict_descent_from_odd_signed_quaternion
  4. 0004exact hsigned