FS001T · theorem body

four_square_descent_even_multiplier_matching_parity_halving

Alpha v34 checked-use · independently kernel and Lean verified; not Stable

Any represented even multiplier with two constructively matching-parity coordinate pairs has a fully checked four-square half representation.

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

∀ p. ∀ a. ∀ b. ∀ c. ∀ d. p · 2 = a · a + b · b + c · c + d · d → Even(a) ∧ Even(b) ∨ Odd(a) ∧ Odd(b) → Even(c) ∧ Even(d) ∨ Odd(c) ∧ Odd(d) → ∃ x. ∃ y. ∃ z. ∃ n. p = x · x + y · y + z · z + n · n

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

PD0009 Even PD0010 Odd

In local proof propositions

PD0009 Even
Exact expanded first-order statement
forall p a b c d. p * 2 = a * a + b * b + c * c + d * d -> ((((exists fsd_even_first_halve_first. a = 2 * fsd_even_first_halve_first) /\ (exists fsd_even_second_halve_first. b = 2 * fsd_even_second_halve_first)) \/ ((exists fsd_odd_first_halve_first. a = 2 * fsd_odd_first_halve_first + 1) /\ (exists fsd_odd_second_halve_first. b = 2 * fsd_odd_second_halve_first + 1)))) -> ((((exists fsd_even_first_halve_second. c = 2 * fsd_even_first_halve_second) /\ (exists fsd_even_second_halve_second. d = 2 * fsd_even_second_halve_second)) \/ ((exists fsd_odd_first_halve_second. c = 2 * fsd_odd_first_halve_second + 1) /\ (exists fsd_odd_second_halve_second. d = 2 * fsd_odd_second_halve_second + 1)))) -> (exists fsl_a_even_matching fsl_b_even_matching fsl_c_even_matching fsl_d_even_matching. (p) = fsl_a_even_matching * fsl_a_even_matching + fsl_b_even_matching * fsl_b_even_matching + fsl_c_even_matching * fsl_c_even_matching + fsl_d_even_matching * fsl_d_even_matching)

Proof neighborhood

Direct theorem prerequisites

FS001P four_square_descent_matching_parity_sum_even FS001Q four_square_descent_matching_parity_absolute_even FS001S four_square_descent_even_multiplier_paired_halving

Direct theorem dependents

FS0040 four_square_parity_even_multiplier_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

43 script commands · 11 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.

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 (3)
four square descent matching parity sum evenfour square descent matching parity absolute evenfour square descent even multiplier paired halving
01Fix variables and assumptionsL1–8

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

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro d
  6. L6
    intro hnorm
  7. L7
    intro hfirst
  8. L8
    intro hsecond
02Establish hsumfirstL9–13

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square descent matching parity sum even.

  1. L9
    have hsumfirst : Even(a + b)Definitions: Even(a + b)Original native command in the exact edition
  2. L10
    specialize four_square_descent_matching_parity_sum_even a
  3. L11
    specialize four_square_descent_matching_parity_sum_even b
  4. L12
    apply four_square_descent_matching_parity_sum_even
  5. L13
    exact hfirst
03Separate the logical casesL14–14

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

  1. L14
    cases hsumfirst
04Establish hgapfirstL15–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square descent matching parity absolute even.

  1. L15
    have hgapfirst : exists v. ((a = b + 2 * v) \/ (b = a + 2 * v))
  2. L16
    specialize four_square_descent_matching_parity_absolute_even a
  3. L17
    specialize four_square_descent_matching_parity_absolute_even b
  4. L18
    apply four_square_descent_matching_parity_absolute_even
  5. L19
    exact hfirst
05Separate the logical casesL20–20

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

  1. L20
    cases hgapfirst
06Establish hsumsecondL21–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square descent matching parity sum even.

  1. L21
    have hsumsecond : Even(c + d)Definitions: Even(c + d)Original native command in the exact edition
  2. L22
    apply four_square_descent_matching_parity_sum_even
  3. L23
    exact hsecond
07Separate the logical casesL24–24

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

  1. L24
    cases hsumsecond
08Establish hgapsecondL25–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square descent matching parity absolute even.

  1. L25
    have hgapsecond : exists z. ((c = d + 2 * z) \/ (d = c + 2 * z))
  2. L26
    apply four_square_descent_matching_parity_absolute_even
  3. L27
    exact hsecond
09Separate the logical casesL28–28

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

  1. L28
    cases hgapsecond
10Use earlier factsL29–38

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

  1. L29
    specialize four_square_descent_even_multiplier_paired_halving p
  2. L30
    specialize four_square_descent_even_multiplier_paired_halving a
  3. L31
    specialize four_square_descent_even_multiplier_paired_halving b
  4. L32
    specialize four_square_descent_even_multiplier_paired_halving c
  5. L33
    specialize four_square_descent_even_multiplier_paired_halving d
  6. L34
    specialize four_square_descent_even_multiplier_paired_halving x
  7. L35
    specialize four_square_descent_even_multiplier_paired_halving x1
  8. L36
    specialize four_square_descent_even_multiplier_paired_halving x2
  9. L37
    specialize four_square_descent_even_multiplier_paired_halving x3
  10. L38
    apply four_square_descent_even_multiplier_paired_halving
11Use earlier factsL39–43

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

  1. L39
    exact hnorm
  2. L40
    exact hsumfirst_witness
  3. L41
    exact hgapfirst_witness
  4. L42
    exact hsumsecond_witness
  5. L43
    exact hgapsecond_witness

Library-wide reading audit

Original defined command ledger · 43 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro b
  4. 0004intro c
  5. 0005intro d
  6. 0006intro hnorm
  7. 0007intro hfirst
  8. 0008intro hsecond
  9. 0009have hsumfirst : Even(a + b)
    Exact native replay linehave hsumfirst : exists u. a + b = 2 * u
  10. 0010specialize four_square_descent_matching_parity_sum_even a
  11. 0011specialize four_square_descent_matching_parity_sum_even b
  12. 0012apply four_square_descent_matching_parity_sum_even
  13. 0013exact hfirst
  14. 0014cases hsumfirst
  15. 0015have hgapfirst : exists v. ((a = b + 2 * v) \/ (b = a + 2 * v))
  16. 0016specialize four_square_descent_matching_parity_absolute_even a
  17. 0017specialize four_square_descent_matching_parity_absolute_even b
  18. 0018apply four_square_descent_matching_parity_absolute_even
  19. 0019exact hfirst
  20. 0020cases hgapfirst
  21. 0021have hsumsecond : Even(c + d)
    Exact native replay linehave hsumsecond : exists w. c + d = 2 * w
  22. 0022apply four_square_descent_matching_parity_sum_even
  23. 0023exact hsecond
  24. 0024cases hsumsecond
  25. 0025have hgapsecond : exists z. ((c = d + 2 * z) \/ (d = c + 2 * z))
  26. 0026apply four_square_descent_matching_parity_absolute_even
  27. 0027exact hsecond
  28. 0028cases hgapsecond
  29. 0029specialize four_square_descent_even_multiplier_paired_halving p
  30. 0030specialize four_square_descent_even_multiplier_paired_halving a
  31. 0031specialize four_square_descent_even_multiplier_paired_halving b
  32. 0032specialize four_square_descent_even_multiplier_paired_halving c
  33. 0033specialize four_square_descent_even_multiplier_paired_halving d
  34. 0034specialize four_square_descent_even_multiplier_paired_halving x
  35. 0035specialize four_square_descent_even_multiplier_paired_halving x1
  36. 0036specialize four_square_descent_even_multiplier_paired_halving x2
  37. 0037specialize four_square_descent_even_multiplier_paired_halving x3
  38. 0038apply four_square_descent_even_multiplier_paired_halving
  39. 0039exact hnorm
  40. 0040exact hsumfirst_witness
  41. 0041exact hgapfirst_witness
  42. 0042exact hsumsecond_witness
  43. 0043exact hgapsecond_witness