FS000T

four_square_branch_odd_represented_strict_step

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

A proper odd prime multiplier descends constructively once its one explicitly centered signed quaternion quotient is represented.

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_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 p k h. ((~(p = 1) /\ forall frm_prime_left_fsbr_prime frm_prime_right_fsbr_prime. p = frm_prime_left_fsbr_prime * frm_prime_right_fsbr_prime -> frm_prime_left_fsbr_prime = 1 \/ frm_prime_right_fsbr_prime = 1)) -> ~(k = 0) -> ~(k = 1) -> (exists gap. gap + S k = p) -> k = 2 * h + 1 -> (exists fsl_a_fsbr_multiple fsl_b_fsbr_multiple fsl_c_fsbr_multiple fsl_d_fsbr_multiple. (p * k) = fsl_a_fsbr_multiple * fsl_a_fsbr_multiple + fsl_b_fsbr_multiple * fsl_b_fsbr_multiple + fsl_c_fsbr_multiple * fsl_c_fsbr_multiple + fsl_d_fsbr_multiple * fsl_d_fsbr_multiple) -> (exists r. (~(r = 0) /\ ((exists gap. gap + S r = k) /\ (exists fsl_a_fsbr_smaller fsl_b_fsbr_smaller fsl_c_fsbr_smaller fsl_d_fsbr_smaller. (p * r) = fsl_a_fsbr_smaller * fsl_a_fsbr_smaller + fsl_b_fsbr_smaller * fsl_b_fsbr_smaller + fsl_c_fsbr_smaller * fsl_c_fsbr_smaller + fsl_d_fsbr_smaller * fsl_d_fsbr_smaller))))

Constructive proof overview

Generated structural guide

A proper odd prime multiplier descends constructively once its one explicitly centered signed quaternion quotient is represented.

The unchanged tactic script uses 3 declared prerequisites and contains 92 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

FS001N four_square_descent_centered_four_remainders_exist FS005D four_square_signed_centered_norm_quotient_exists FS0024 four_square_descent_odd_centered_strict_step

Direct dependents

FS000U four_square_bounded_strict_descent_from_odd_signed_quaternion

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

92 script commands · 12 reading checkpoints · 2 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 (3)
four square descent centered four remainders existfour square signed centered norm quotient existsfour square descent odd centered strict step

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro hsigned
  2. L2
    intro p
  3. L3
    intro k
  4. L4
    intro h
  5. L5
    intro hprime
  6. L6
    intro hnonzero
  7. L7
    intro hnonunit
  8. L8
    intro hproper
  9. L9
    intro hodd
  10. L10
    intro hrepresented
02Separate the logical casesL11–14

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L11
    cases hrepresented
  2. L12
    cases hrepresented_witness
  3. L13
    cases hrepresented_witness_witness
  4. L14
    cases hrepresented_witness_witness_witness
03Establish hcentersL15–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square descent centered four remainders exist.

  1. L15
    have hcenters : ∃ e. ∃ f. ∃ g. ∃ j. Le(e + e,k) ∧ ((∃ y. x = k · y + e) ∨ Dvd(k,x + e)) ∧ (Le(f + f,k) ∧ ((∃ y. x1 = k · y + f) ∨ Dvd(k,x1 + f)) ∧ (Le(g + g,k) ∧ ((∃ y. x2 = k · y + g) ∨ Dvd(k,x2 + g)) ∧ (Le(j + j,k) ∧ ((∃ y. x3 = k · y + j) ∨ Dvd(k,x3 + j)))))Definitions: LeDvd
  2. L16
    specialize four_square_descent_centered_four_remainders_exist k
  3. L17
    specialize four_square_descent_centered_four_remainders_exist x
  4. L18
    specialize four_square_descent_centered_four_remainders_exist x1
  5. L19
    specialize four_square_descent_centered_four_remainders_exist x2
  6. L20
    specialize four_square_descent_centered_four_remainders_exist x3
  7. L21
    apply four_square_descent_centered_four_remainders_exist
  8. L22
    exact hnonzero
04Separate the logical casesL23–29

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L23
    cases hcenters
  2. L24
    cases hcenters_witness
  3. L25
    cases hcenters_witness_witness
  4. L26
    cases hcenters_witness_witness_witness
  5. L27
    cases hcenters_witness_witness_witness_witness
  6. L28
    cases hcenters_witness_witness_witness_witness_right
  7. L29
    cases hcenters_witness_witness_witness_witness_right_right
05Establish hquotientL30–39

Establish this local claim before using it. It is not an additional assumption.

  1. L30
    have hquotient : exists r. k * r = x4 * x4 + x5 * x5 + x6 * x6 + x7 * x7
  2. L31
    specialize four_square_signed_centered_norm_quotient_exists p
  3. L32
    specialize four_square_signed_centered_norm_quotient_exists k
  4. L33
    specialize four_square_signed_centered_norm_quotient_exists x
  5. L34
    specialize four_square_signed_centered_norm_quotient_exists x1
  6. L35
    specialize four_square_signed_centered_norm_quotient_exists x2
  7. L36
    specialize four_square_signed_centered_norm_quotient_exists x3
  8. L37
    specialize four_square_signed_centered_norm_quotient_exists x4
  9. L38
    specialize four_square_signed_centered_norm_quotient_exists x5
  10. L39
    specialize four_square_signed_centered_norm_quotient_exists x6
06Use earlier factsL40–46

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

  1. L40
    specialize four_square_signed_centered_norm_quotient_exists x7
  2. L41
    apply four_square_signed_centered_norm_quotient_exists
  3. L42
    exact hrepresented_witness_witness_witness_witness
  4. L43
    exact hcenters_witness_witness_witness_witness_left
  5. L44
    exact hcenters_witness_witness_witness_witness_right_left
  6. L45
    exact hcenters_witness_witness_witness_witness_right_right_left
  7. L46
    exact hcenters_witness_witness_witness_witness_right_right_right
07Separate the logical casesL47–47

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L47
    cases hquotient
08Use earlier factsL48–57

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

  1. L48
    specialize four_square_descent_odd_centered_strict_step p
  2. L49
    specialize four_square_descent_odd_centered_strict_step k
  3. L50
    specialize four_square_descent_odd_centered_strict_step h
  4. L51
    specialize four_square_descent_odd_centered_strict_step x8
  5. L52
    specialize four_square_descent_odd_centered_strict_step x
  6. L53
    specialize four_square_descent_odd_centered_strict_step x1
  7. L54
    specialize four_square_descent_odd_centered_strict_step x2
  8. L55
    specialize four_square_descent_odd_centered_strict_step x3
  9. L56
    specialize four_square_descent_odd_centered_strict_step x4
  10. L57
    specialize four_square_descent_odd_centered_strict_step x5
09Use earlier factsL58–67

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

  1. L58
    specialize four_square_descent_odd_centered_strict_step x6
  2. L59
    specialize four_square_descent_odd_centered_strict_step x7
  3. L60
    apply four_square_descent_odd_centered_strict_step
  4. L61
    exact hprime
  5. L62
    exact hnonzero
  6. L63
    exact hnonunit
  7. L64
    exact hproper
  8. L65
    exact hodd
  9. L66
    exact hrepresented_witness_witness_witness_witness
  10. L67
    exact hcenters_witness_witness_witness_witness_left
10Use earlier factsL68–77

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

  1. L68
    exact hcenters_witness_witness_witness_witness_right_left
  2. L69
    exact hcenters_witness_witness_witness_witness_right_right_left
  3. L70
    exact hcenters_witness_witness_witness_witness_right_right_right
  4. L71
    exact hquotient_witness
  5. L72
    specialize hsigned p
  6. L73
    specialize hsigned k
  7. L74
    specialize hsigned h
  8. L75
    specialize hsigned x
  9. L76
    specialize hsigned x1
  10. L77
    specialize hsigned x2
11Use earlier factsL78–87

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

  1. L78
    specialize hsigned x3
  2. L79
    specialize hsigned x4
  3. L80
    specialize hsigned x5
  4. L81
    specialize hsigned x6
  5. L82
    specialize hsigned x7
  6. L83
    specialize hsigned x8
  7. L84
    apply hsigned
  8. L85
    exact hnonzero
  9. L86
    exact hodd
  10. L87
    exact hrepresented_witness_witness_witness_witness
12Use earlier factsL88–92

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

  1. L88
    exact hcenters_witness_witness_witness_witness_left
  2. L89
    exact hcenters_witness_witness_witness_witness_right_left
  3. L90
    exact hcenters_witness_witness_witness_witness_right_right_left
  4. L91
    exact hcenters_witness_witness_witness_witness_right_right_right
  5. L92
    exact hquotient_witness

Library-wide reading audit

Original exact command ledger · 92 lines
  1. 0001intro hsigned
  2. 0002intro p
  3. 0003intro k
  4. 0004intro h
  5. 0005intro hprime
  6. 0006intro hnonzero
  7. 0007intro hnonunit
  8. 0008intro hproper
  9. 0009intro hodd
  10. 0010intro hrepresented
  11. 0011cases hrepresented
  12. 0012cases hrepresented_witness
  13. 0013cases hrepresented_witness_witness
  14. 0014cases hrepresented_witness_witness_witness
  15. 0015have hcenters : exists e f g j. ((((exists fsd_center_bound_branch_a. fsd_center_bound_branch_a + (e + e) = k) /\ ((exists fsd_center_lower_branch_a. x = k * fsd_center_lower_branch_a + e) \/ (exists fsd_center_upper_branch_a. x + e = k * fsd_center_upper_branch_a)))) /\ ((((exists fsd_center_bound_branch_b. fsd_center_bound_branch_b + (f + f) = k) /\ ((exists fsd_center_lower_branch_b. x1 = k * fsd_center_lower_branch_b + f) \/ (exists fsd_center_upper_branch_b. x1 + f = k * fsd_center_upper_branch_b)))) /\ ((((exists fsd_center_bound_branch_c. fsd_center_bound_branch_c + (g + g) = k) /\ ((exists fsd_center_lower_branch_c. x2 = k * fsd_center_lower_branch_c + g) \/ (exists fsd_center_upper_branch_c. x2 + g = k * fsd_center_upper_branch_c)))) /\ (((exists fsd_center_bound_branch_d. fsd_center_bound_branch_d + (j + j) = k) /\ ((exists fsd_center_lower_branch_d. x3 = k * fsd_center_lower_branch_d + j) \/ (exists fsd_center_upper_branch_d. x3 + j = k * fsd_center_upper_branch_d)))))))
  16. 0016specialize four_square_descent_centered_four_remainders_exist k
  17. 0017specialize four_square_descent_centered_four_remainders_exist x
  18. 0018specialize four_square_descent_centered_four_remainders_exist x1
  19. 0019specialize four_square_descent_centered_four_remainders_exist x2
  20. 0020specialize four_square_descent_centered_four_remainders_exist x3
  21. 0021apply four_square_descent_centered_four_remainders_exist
  22. 0022exact hnonzero
  23. 0023cases hcenters
  24. 0024cases hcenters_witness
  25. 0025cases hcenters_witness_witness
  26. 0026cases hcenters_witness_witness_witness
  27. 0027cases hcenters_witness_witness_witness_witness
  28. 0028cases hcenters_witness_witness_witness_witness_right
  29. 0029cases hcenters_witness_witness_witness_witness_right_right
  30. 0030have hquotient : exists r. k * r = x4 * x4 + x5 * x5 + x6 * x6 + x7 * x7
  31. 0031specialize four_square_signed_centered_norm_quotient_exists p
  32. 0032specialize four_square_signed_centered_norm_quotient_exists k
  33. 0033specialize four_square_signed_centered_norm_quotient_exists x
  34. 0034specialize four_square_signed_centered_norm_quotient_exists x1
  35. 0035specialize four_square_signed_centered_norm_quotient_exists x2
  36. 0036specialize four_square_signed_centered_norm_quotient_exists x3
  37. 0037specialize four_square_signed_centered_norm_quotient_exists x4
  38. 0038specialize four_square_signed_centered_norm_quotient_exists x5
  39. 0039specialize four_square_signed_centered_norm_quotient_exists x6
  40. 0040specialize four_square_signed_centered_norm_quotient_exists x7
  41. 0041apply four_square_signed_centered_norm_quotient_exists
  42. 0042exact hrepresented_witness_witness_witness_witness
  43. 0043exact hcenters_witness_witness_witness_witness_left
  44. 0044exact hcenters_witness_witness_witness_witness_right_left
  45. 0045exact hcenters_witness_witness_witness_witness_right_right_left
  46. 0046exact hcenters_witness_witness_witness_witness_right_right_right
  47. 0047cases hquotient
  48. 0048specialize four_square_descent_odd_centered_strict_step p
  49. 0049specialize four_square_descent_odd_centered_strict_step k
  50. 0050specialize four_square_descent_odd_centered_strict_step h
  51. 0051specialize four_square_descent_odd_centered_strict_step x8
  52. 0052specialize four_square_descent_odd_centered_strict_step x
  53. 0053specialize four_square_descent_odd_centered_strict_step x1
  54. 0054specialize four_square_descent_odd_centered_strict_step x2
  55. 0055specialize four_square_descent_odd_centered_strict_step x3
  56. 0056specialize four_square_descent_odd_centered_strict_step x4
  57. 0057specialize four_square_descent_odd_centered_strict_step x5
  58. 0058specialize four_square_descent_odd_centered_strict_step x6
  59. 0059specialize four_square_descent_odd_centered_strict_step x7
  60. 0060apply four_square_descent_odd_centered_strict_step
  61. 0061exact hprime
  62. 0062exact hnonzero
  63. 0063exact hnonunit
  64. 0064exact hproper
  65. 0065exact hodd
  66. 0066exact hrepresented_witness_witness_witness_witness
  67. 0067exact hcenters_witness_witness_witness_witness_left
  68. 0068exact hcenters_witness_witness_witness_witness_right_left
  69. 0069exact hcenters_witness_witness_witness_witness_right_right_left
  70. 0070exact hcenters_witness_witness_witness_witness_right_right_right
  71. 0071exact hquotient_witness
  72. 0072specialize hsigned p
  73. 0073specialize hsigned k
  74. 0074specialize hsigned h
  75. 0075specialize hsigned x
  76. 0076specialize hsigned x1
  77. 0077specialize hsigned x2
  78. 0078specialize hsigned x3
  79. 0079specialize hsigned x4
  80. 0080specialize hsigned x5
  81. 0081specialize hsigned x6
  82. 0082specialize hsigned x7
  83. 0083specialize hsigned x8
  84. 0084apply hsigned
  85. 0085exact hnonzero
  86. 0086exact hodd
  87. 0087exact hrepresented_witness_witness_witness_witness
  88. 0088exact hcenters_witness_witness_witness_witness_left
  89. 0089exact hcenters_witness_witness_witness_witness_right_left
  90. 0090exact hcenters_witness_witness_witness_witness_right_right_left
  91. 0091exact hcenters_witness_witness_witness_witness_right_right_right
  92. 0092exact hquotient_witness