FS0040

four_square_parity_even_multiplier_halving

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

Every represented even natural n·2 has an actual four-square representation of n, with no coordinate-parity premise.

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 n a b c d. n * 2 = a * a + b * b + c * c + d * d -> (exists fsl_a_fsps_half fsl_b_fsps_half fsl_c_fsps_half fsl_d_fsps_half. (n) = fsl_a_fsps_half * fsl_a_fsps_half + fsl_b_fsps_half * fsl_b_fsps_half + fsl_c_fsps_half * fsl_c_fsps_half + fsl_d_fsps_half * fsl_d_fsps_half)

Constructive proof overview

Generated structural guide

Every represented even natural n·2 has an actual four-square representation of n, with no coordinate-parity premise.

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

FS003X four_square_parity_even_norm_pair_selection FS003Y four_square_parity_swap_middle_coordinates FS003Z four_square_parity_swap_outer_coordinates FS001T four_square_descent_even_multiplier_matching_parity_halving

Direct dependents

FS0041 four_square_parity_represented_double_halving FS0042 four_square_parity_represented_additive_double_halving

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

46 script commands · 12 reading checkpoints · 1 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 (4)
four square parity even norm pair selectionfour square parity swap middle coordinatesfour square parity swap outer coordinatesfour square descent even multiplier matching parity halving

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–6

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

  1. L1
    intro n
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro d
  6. L6
    intro hnorm
02Establish hpairsL7–10

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square parity even norm pair selection.

  1. L7
    have hpairs : (Even(a) ∧ Even(b) ∨ Odd(a) ∧ Odd(b)) ∧ (Even(c) ∧ Even(d) ∨ Odd(c) ∧ Odd(d)) ∨ ((Even(a) ∧ Even(c) ∨ Odd(a) ∧ Odd(c)) ∧ (Even(b) ∧ Even(d) ∨ Odd(b) ∧ Odd(d)) ∨ (Even(a) ∧ Even(d) ∨ Odd(a) ∧ Odd(d)) ∧ (Even(b) ∧ Even(c) ∨ Odd(b) ∧ Odd(c)))Definitions: EvenOdd
  2. L8
    specialize four_square_parity_even_norm_pair_selection n
  3. L9
    apply four_square_parity_even_norm_pair_selection
  4. L10
    exact hnorm
03Separate the logical casesL11–12

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

  1. L11
    cases hpairs
  2. L12
    cases hpairs_left
04Use earlier factsL13–21

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

  1. L13
    specialize four_square_descent_even_multiplier_matching_parity_halving n
  2. L14
    specialize four_square_descent_even_multiplier_matching_parity_halving a
  3. L15
    specialize four_square_descent_even_multiplier_matching_parity_halving b
  4. L16
    specialize four_square_descent_even_multiplier_matching_parity_halving c
  5. L17
    specialize four_square_descent_even_multiplier_matching_parity_halving d
  6. L18
    apply four_square_descent_even_multiplier_matching_parity_halving
  7. L19
    exact hnorm
  8. L20
    exact hpairs_left_left
  9. L21
    exact hpairs_left_right
05Separate the logical casesL22–23

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

  1. L22
    cases hpairs_right
  2. L23
    cases hpairs_right_left
06Use earlier factsL24–29

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

  1. L24
    specialize four_square_descent_even_multiplier_matching_parity_halving n
  2. L25
    specialize four_square_descent_even_multiplier_matching_parity_halving a
  3. L26
    specialize four_square_descent_even_multiplier_matching_parity_halving c
  4. L27
    specialize four_square_descent_even_multiplier_matching_parity_halving b
  5. L28
    specialize four_square_descent_even_multiplier_matching_parity_halving d
  6. L29
    apply four_square_descent_even_multiplier_matching_parity_halving
07Calculate and transport equalitiesL30–30

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L30
    trans a * a + b * b + c * c + d * d
08Use earlier factsL31–34

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

  1. L31
    exact hnorm
  2. L32
    apply four_square_parity_swap_middle_coordinates
  3. L33
    exact hpairs_right_left_left
  4. L34
    exact hpairs_right_left_right
09Separate the logical casesL35–35

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

  1. L35
    cases hpairs_right_right
10Use earlier factsL36–41

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

  1. L36
    specialize four_square_descent_even_multiplier_matching_parity_halving n
  2. L37
    specialize four_square_descent_even_multiplier_matching_parity_halving a
  3. L38
    specialize four_square_descent_even_multiplier_matching_parity_halving d
  4. L39
    specialize four_square_descent_even_multiplier_matching_parity_halving b
  5. L40
    specialize four_square_descent_even_multiplier_matching_parity_halving c
  6. L41
    apply four_square_descent_even_multiplier_matching_parity_halving
11Calculate and transport equalitiesL42–42

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L42
    trans a * a + b * b + c * c + d * d
12Use earlier factsL43–46

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

  1. L43
    exact hnorm
  2. L44
    apply four_square_parity_swap_outer_coordinates
  3. L45
    exact hpairs_right_right_left
  4. L46
    exact hpairs_right_right_right

Library-wide reading audit

Original exact command ledger · 46 lines
  1. 0001intro n
  2. 0002intro a
  3. 0003intro b
  4. 0004intro c
  5. 0005intro d
  6. 0006intro hnorm
  7. 0007have hpairs : ((((((exists fsd_even_first_fsps_half_pairs_ab. a = 2 * fsd_even_first_fsps_half_pairs_ab) /\ (exists fsd_even_second_fsps_half_pairs_ab. b = 2 * fsd_even_second_fsps_half_pairs_ab)) \/ ((exists fsd_odd_first_fsps_half_pairs_ab. a = 2 * fsd_odd_first_fsps_half_pairs_ab + 1) /\ (exists fsd_odd_second_fsps_half_pairs_ab. b = 2 * fsd_odd_second_fsps_half_pairs_ab + 1)))) /\ ((((exists fsd_even_first_fsps_half_pairs_cd. c = 2 * fsd_even_first_fsps_half_pairs_cd) /\ (exists fsd_even_second_fsps_half_pairs_cd. d = 2 * fsd_even_second_fsps_half_pairs_cd)) \/ ((exists fsd_odd_first_fsps_half_pairs_cd. c = 2 * fsd_odd_first_fsps_half_pairs_cd + 1) /\ (exists fsd_odd_second_fsps_half_pairs_cd. d = 2 * fsd_odd_second_fsps_half_pairs_cd + 1))))) \/ (((((((exists fsd_even_first_fsps_half_pairs_crossed_ac. a = 2 * fsd_even_first_fsps_half_pairs_crossed_ac) /\ (exists fsd_even_second_fsps_half_pairs_crossed_ac. c = 2 * fsd_even_second_fsps_half_pairs_crossed_ac)) \/ ((exists fsd_odd_first_fsps_half_pairs_crossed_ac. a = 2 * fsd_odd_first_fsps_half_pairs_crossed_ac + 1) /\ (exists fsd_odd_second_fsps_half_pairs_crossed_ac. c = 2 * fsd_odd_second_fsps_half_pairs_crossed_ac + 1)))) /\ ((((exists fsd_even_first_fsps_half_pairs_crossed_bd. b = 2 * fsd_even_first_fsps_half_pairs_crossed_bd) /\ (exists fsd_even_second_fsps_half_pairs_crossed_bd. d = 2 * fsd_even_second_fsps_half_pairs_crossed_bd)) \/ ((exists fsd_odd_first_fsps_half_pairs_crossed_bd. b = 2 * fsd_odd_first_fsps_half_pairs_crossed_bd + 1) /\ (exists fsd_odd_second_fsps_half_pairs_crossed_bd. d = 2 * fsd_odd_second_fsps_half_pairs_crossed_bd + 1))))) \/ (((((exists fsd_even_first_fsps_half_pairs_crossed_ad. a = 2 * fsd_even_first_fsps_half_pairs_crossed_ad) /\ (exists fsd_even_second_fsps_half_pairs_crossed_ad. d = 2 * fsd_even_second_fsps_half_pairs_crossed_ad)) \/ ((exists fsd_odd_first_fsps_half_pairs_crossed_ad. a = 2 * fsd_odd_first_fsps_half_pairs_crossed_ad + 1) /\ (exists fsd_odd_second_fsps_half_pairs_crossed_ad. d = 2 * fsd_odd_second_fsps_half_pairs_crossed_ad + 1)))) /\ ((((exists fsd_even_first_fsps_half_pairs_crossed_bc. b = 2 * fsd_even_first_fsps_half_pairs_crossed_bc) /\ (exists fsd_even_second_fsps_half_pairs_crossed_bc. c = 2 * fsd_even_second_fsps_half_pairs_crossed_bc)) \/ ((exists fsd_odd_first_fsps_half_pairs_crossed_bc. b = 2 * fsd_odd_first_fsps_half_pairs_crossed_bc + 1) /\ (exists fsd_odd_second_fsps_half_pairs_crossed_bc. c = 2 * fsd_odd_second_fsps_half_pairs_crossed_bc + 1))))))))
  8. 0008specialize four_square_parity_even_norm_pair_selection n
  9. 0009apply four_square_parity_even_norm_pair_selection
  10. 0010exact hnorm
  11. 0011cases hpairs
  12. 0012cases hpairs_left
  13. 0013specialize four_square_descent_even_multiplier_matching_parity_halving n
  14. 0014specialize four_square_descent_even_multiplier_matching_parity_halving a
  15. 0015specialize four_square_descent_even_multiplier_matching_parity_halving b
  16. 0016specialize four_square_descent_even_multiplier_matching_parity_halving c
  17. 0017specialize four_square_descent_even_multiplier_matching_parity_halving d
  18. 0018apply four_square_descent_even_multiplier_matching_parity_halving
  19. 0019exact hnorm
  20. 0020exact hpairs_left_left
  21. 0021exact hpairs_left_right
  22. 0022cases hpairs_right
  23. 0023cases hpairs_right_left
  24. 0024specialize four_square_descent_even_multiplier_matching_parity_halving n
  25. 0025specialize four_square_descent_even_multiplier_matching_parity_halving a
  26. 0026specialize four_square_descent_even_multiplier_matching_parity_halving c
  27. 0027specialize four_square_descent_even_multiplier_matching_parity_halving b
  28. 0028specialize four_square_descent_even_multiplier_matching_parity_halving d
  29. 0029apply four_square_descent_even_multiplier_matching_parity_halving
  30. 0030trans a * a + b * b + c * c + d * d
  31. 0031exact hnorm
  32. 0032apply four_square_parity_swap_middle_coordinates
  33. 0033exact hpairs_right_left_left
  34. 0034exact hpairs_right_left_right
  35. 0035cases hpairs_right_right
  36. 0036specialize four_square_descent_even_multiplier_matching_parity_halving n
  37. 0037specialize four_square_descent_even_multiplier_matching_parity_halving a
  38. 0038specialize four_square_descent_even_multiplier_matching_parity_halving d
  39. 0039specialize four_square_descent_even_multiplier_matching_parity_halving b
  40. 0040specialize four_square_descent_even_multiplier_matching_parity_halving c
  41. 0041apply four_square_descent_even_multiplier_matching_parity_halving
  42. 0042trans a * a + b * b + c * c + d * d
  43. 0043exact hnorm
  44. 0044apply four_square_parity_swap_outer_coordinates
  45. 0045exact hpairs_right_right_left
  46. 0046exact hpairs_right_right_right