FS001N

four_square_descent_centered_four_remainders_exist

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

Every four-coordinate natural quaternion admits four independent constructively chosen centered signed remainders.

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 k a b c d. ~(k = 0) -> exists e f g h. ((((exists fsd_center_bound_four_0. fsd_center_bound_four_0 + (e + e) = k) /\ ((exists fsd_center_lower_four_0. a = k * fsd_center_lower_four_0 + e) \/ (exists fsd_center_upper_four_0. a + e = k * fsd_center_upper_four_0)))) /\ ((((exists fsd_center_bound_four_1. fsd_center_bound_four_1 + (f + f) = k) /\ ((exists fsd_center_lower_four_1. b = k * fsd_center_lower_four_1 + f) \/ (exists fsd_center_upper_four_1. b + f = k * fsd_center_upper_four_1)))) /\ ((((exists fsd_center_bound_four_2. fsd_center_bound_four_2 + (g + g) = k) /\ ((exists fsd_center_lower_four_2. c = k * fsd_center_lower_four_2 + g) \/ (exists fsd_center_upper_four_2. c + g = k * fsd_center_upper_four_2)))) /\ (((exists fsd_center_bound_four_3. fsd_center_bound_four_3 + (h + h) = k) /\ ((exists fsd_center_lower_four_3. d = k * fsd_center_lower_four_3 + h) \/ (exists fsd_center_upper_four_3. d + h = k * fsd_center_upper_four_3)))))))

Constructive proof overview

Generated structural guide

Every four-coordinate natural quaternion admits four independent constructively chosen centered signed remainders.

The unchanged tactic script uses 1 declared prerequisite and contains 35 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

FS001M four_square_descent_centered_signed_remainder_exists

Direct dependents

FS000T four_square_branch_odd_represented_strict_step

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

35 script commands · 13 reading checkpoints · 4 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 (1)
four square descent centered signed remainder exists
01Fix variables and assumptionsL1–6

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

  1. L1
    intro k
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro d
  6. L6
    intro hnonzero
02Establish haL7–11

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

  1. L7
    have ha : exists e. (((exists fsd_center_bound_four_a. fsd_center_bound_four_a + (e + e) = k) /\ ((exists fsd_center_lower_four_a. a = k * fsd_center_lower_four_a + e) \/ (exists fsd_center_upper_four_a. a + e = k * fsd_center_upper_four_a))))
  2. L8
    specialize four_square_descent_centered_signed_remainder_exists k
  3. L9
    specialize four_square_descent_centered_signed_remainder_exists a
  4. L10
    apply four_square_descent_centered_signed_remainder_exists
  5. L11
    exact hnonzero
03Establish hbL12–14

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

  1. L12
    have hb : exists f. (((exists fsd_center_bound_four_b. fsd_center_bound_four_b + (f + f) = k) /\ ((exists fsd_center_lower_four_b. b = k * fsd_center_lower_four_b + f) \/ (exists fsd_center_upper_four_b. b + f = k * fsd_center_upper_four_b))))
  2. L13
    apply four_square_descent_centered_signed_remainder_exists
  3. L14
    exact hnonzero
04Establish hcL15–17

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

  1. L15
    have hc : exists g. (((exists fsd_center_bound_four_c. fsd_center_bound_four_c + (g + g) = k) /\ ((exists fsd_center_lower_four_c. c = k * fsd_center_lower_four_c + g) \/ (exists fsd_center_upper_four_c. c + g = k * fsd_center_upper_four_c))))
  2. L16
    apply four_square_descent_centered_signed_remainder_exists
  3. L17
    exact hnonzero
05Establish hdL18–20

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

  1. L18
    have hd : exists h. (((exists fsd_center_bound_four_d. fsd_center_bound_four_d + (h + h) = k) /\ ((exists fsd_center_lower_four_d. d = k * fsd_center_lower_four_d + h) \/ (exists fsd_center_upper_four_d. d + h = k * fsd_center_upper_four_d))))
  2. L19
    apply four_square_descent_centered_signed_remainder_exists
  3. L20
    exact hnonzero
06Separate the logical casesL21–24

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

  1. L21
    cases ha
  2. L22
    cases hb
  3. L23
    cases hc
  4. L24
    cases hd
07Construct an explicit witnessL25–28

Supply the displayed value, then prove that it has the required property.

  1. L25
    exists x
  2. L26
    exists x1
  3. L27
    exists x2
  4. L28
    exists x3
08Separate the logical casesL29–29

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

  1. L29
    split
09Use earlier factsL30–30

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

  1. L30
    exact ha_witness
10Separate the logical casesL31–31

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

  1. L31
    split
11Use earlier factsL32–32

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

  1. L32
    exact hb_witness
12Separate the logical casesL33–33

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

  1. L33
    split
13Use earlier factsL34–35

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

  1. L34
    exact hc_witness
  2. L35
    exact hd_witness

Library-wide reading audit

Original exact command ledger · 35 lines
  1. 0001intro k
  2. 0002intro a
  3. 0003intro b
  4. 0004intro c
  5. 0005intro d
  6. 0006intro hnonzero
  7. 0007have ha : exists e. (((exists fsd_center_bound_four_a. fsd_center_bound_four_a + (e + e) = k) /\ ((exists fsd_center_lower_four_a. a = k * fsd_center_lower_four_a + e) \/ (exists fsd_center_upper_four_a. a + e = k * fsd_center_upper_four_a))))
  8. 0008specialize four_square_descent_centered_signed_remainder_exists k
  9. 0009specialize four_square_descent_centered_signed_remainder_exists a
  10. 0010apply four_square_descent_centered_signed_remainder_exists
  11. 0011exact hnonzero
  12. 0012have hb : exists f. (((exists fsd_center_bound_four_b. fsd_center_bound_four_b + (f + f) = k) /\ ((exists fsd_center_lower_four_b. b = k * fsd_center_lower_four_b + f) \/ (exists fsd_center_upper_four_b. b + f = k * fsd_center_upper_four_b))))
  13. 0013apply four_square_descent_centered_signed_remainder_exists
  14. 0014exact hnonzero
  15. 0015have hc : exists g. (((exists fsd_center_bound_four_c. fsd_center_bound_four_c + (g + g) = k) /\ ((exists fsd_center_lower_four_c. c = k * fsd_center_lower_four_c + g) \/ (exists fsd_center_upper_four_c. c + g = k * fsd_center_upper_four_c))))
  16. 0016apply four_square_descent_centered_signed_remainder_exists
  17. 0017exact hnonzero
  18. 0018have hd : exists h. (((exists fsd_center_bound_four_d. fsd_center_bound_four_d + (h + h) = k) /\ ((exists fsd_center_lower_four_d. d = k * fsd_center_lower_four_d + h) \/ (exists fsd_center_upper_four_d. d + h = k * fsd_center_upper_four_d))))
  19. 0019apply four_square_descent_centered_signed_remainder_exists
  20. 0020exact hnonzero
  21. 0021cases ha
  22. 0022cases hb
  23. 0023cases hc
  24. 0024cases hd
  25. 0025exists x
  26. 0026exists x1
  27. 0027exists x2
  28. 0028exists x3
  29. 0029split
  30. 0030exact ha_witness
  31. 0031split
  32. 0032exact hb_witness
  33. 0033split
  34. 0034exact hc_witness
  35. 0035exact hd_witness