FS0040 · theorem body

four_square_parity_even_multiplier_halving

Alpha v34 checked-use · independently kernel and Lean verified; 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.

Statement with defined notation

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)

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

none

In local proof propositions

PD0009 Even PD0010 Odd
Exact expanded first-order 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)

Proof neighborhood

Direct theorem prerequisites

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 theorem dependents

FS0041 four_square_parity_represented_double_halving FS0042 four_square_parity_represented_additive_double_halving

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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
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: Even(a)Even(b)Odd(a)Odd(b)Even(c)Even(d)Odd(c)Odd(d)Original native command in the exact edition
  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 defined 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 : (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)))
    Exact native replay linehave 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