FS001S · theorem body

four_square_descent_even_multiplier_paired_halving

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

An actually represented double p·2 descends unconditionally to p when its four coordinates are supplied as two matching-parity pairs.

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 p a b c d u v w x. p * 2 = a * a + b * b + c * c + d * d -> a + b = 2 * u -> (a = b + 2 * v \/ b = a + 2 * v) -> c + d = 2 * w -> (c = d + 2 * x \/ d = c + 2 * x) -> (exists fsl_a_even_paired fsl_b_even_paired fsl_c_even_paired fsl_d_even_paired. (p) = fsl_a_even_paired * fsl_a_even_paired + fsl_b_even_paired * fsl_b_even_paired + fsl_c_even_paired * fsl_c_even_paired + fsl_d_even_paired * fsl_d_even_paired)

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

none
Exact expanded first-order statement
forall p a b c d u v w x. p * 2 = a * a + b * b + c * c + d * d -> a + b = 2 * u -> (a = b + 2 * v \/ b = a + 2 * v) -> c + d = 2 * w -> (c = d + 2 * x \/ d = c + 2 * x) -> (exists fsl_a_even_paired fsl_b_even_paired fsl_c_even_paired fsl_d_even_paired. (p) = fsl_a_even_paired * fsl_a_even_paired + fsl_b_even_paired * fsl_b_even_paired + fsl_c_even_paired * fsl_c_even_paired + fsl_d_even_paired * fsl_d_even_paired)

Proof neighborhood

Direct theorem prerequisites

FS001R four_square_descent_double_pair_identity FS001C four_square_descent_scaled_norm_quotient mul_one · Stable closed add_assoc · Stable closed succ_ne_zero · Stable closed

Direct theorem dependents

FS001T four_square_descent_even_multiplier_matching_parity_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

57 script commands · 10 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.

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 (2)
four square descent double pair identityfour square descent scaled norm quotient
01Fix variables and assumptionsL1–10

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 u
  7. L7
    intro v
  8. L8
    intro w
  9. L9
    intro x
  10. L10
    intro hnorm
02Fix variables and assumptionsL11–14

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

  1. L11
    intro hsumfirst
  2. L12
    intro hgapfirst
  3. L13
    intro hsumsecond
  4. L14
    intro hgapsecond
03Establish hidentityL15–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square descent double pair identity.

  1. L15
    have hidentity : (a * a + b * b + c * c + d * d) * 2 = (((a + b) * (a + b) + (2 * v) * (2 * v)) + ((c + d) * (c + d) + (2 * x) * (2 * x)))
  2. L16
    specialize four_square_descent_double_pair_identity a
  3. L17
    specialize four_square_descent_double_pair_identity b
  4. L18
    specialize four_square_descent_double_pair_identity c
  5. L19
    specialize four_square_descent_double_pair_identity d
  6. L20
    specialize four_square_descent_double_pair_identity v
  7. L21
    specialize four_square_descent_double_pair_identity x
  8. L22
    apply four_square_descent_double_pair_identity
  9. L23
    exact hgapfirst
  10. L24
    exact hgapsecond
04Calculate and transport equalitiesL25–28

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

  1. L25
    rewrite hsumfirst at hidentity
  2. L26
    rewrite hsumfirst at hidentity
  3. L27
    rewrite hsumsecond at hidentity
  4. L28
    rewrite hsumsecond at hidentity
05Establish hscaledL29–37

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul one.

  1. L29
    have hscaled : (p * 2) * (2 * 1) = (2 * u) * (2 * u) + (2 * v) * (2 * v) + (2 * w) * (2 * w) + (2 * x) * (2 * x)
  2. L30
    trans (a * a + b * b + c * c + d * d) * 2
  3. L31
    congr
  4. L32
    exact hnorm
  5. L33
    apply mul_one
  6. L34
    trans (((2 * u) * (2 * u) + (2 * v) * (2 * v)) + ((2 * w) * (2 * w) + (2 * x) * (2 * x)))
  7. L35
    exact hidentity
  8. L36
    symm
  9. L37
    apply add_assoc
06Construct an explicit witnessL38–41

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

  1. L38
    exists u
  2. L39
    exists v
  3. L40
    exists w
  4. L41
    exists x
07Calculate and transport equalitiesL42–43

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

  1. L42
    trans p * 1
  2. L43
    symm
08Use earlier factsL44–52

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

  1. L44
    apply mul_one
  2. L45
    specialize four_square_descent_scaled_norm_quotient p
  3. L46
    specialize four_square_descent_scaled_norm_quotient 2
  4. L47
    specialize four_square_descent_scaled_norm_quotient 1
  5. L48
    specialize four_square_descent_scaled_norm_quotient u
  6. L49
    specialize four_square_descent_scaled_norm_quotient v
  7. L50
    specialize four_square_descent_scaled_norm_quotient w
  8. L51
    specialize four_square_descent_scaled_norm_quotient x
  9. L52
    apply four_square_descent_scaled_norm_quotient
09Fix variables and assumptionsL53–53

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

  1. L53
    intro hzero
10Use earlier factsL54–57

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

  1. L54
    specialize succ_ne_zero 1
  2. L55
    apply succ_ne_zero
  3. L56
    exact hzero
  4. L57
    exact hscaled

Library-wide reading audit

Original defined command ledger · 57 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro b
  4. 0004intro c
  5. 0005intro d
  6. 0006intro u
  7. 0007intro v
  8. 0008intro w
  9. 0009intro x
  10. 0010intro hnorm
  11. 0011intro hsumfirst
  12. 0012intro hgapfirst
  13. 0013intro hsumsecond
  14. 0014intro hgapsecond
  15. 0015have hidentity : (a * a + b * b + c * c + d * d) * 2 = (((a + b) * (a + b) + (2 * v) * (2 * v)) + ((c + d) * (c + d) + (2 * x) * (2 * x)))
  16. 0016specialize four_square_descent_double_pair_identity a
  17. 0017specialize four_square_descent_double_pair_identity b
  18. 0018specialize four_square_descent_double_pair_identity c
  19. 0019specialize four_square_descent_double_pair_identity d
  20. 0020specialize four_square_descent_double_pair_identity v
  21. 0021specialize four_square_descent_double_pair_identity x
  22. 0022apply four_square_descent_double_pair_identity
  23. 0023exact hgapfirst
  24. 0024exact hgapsecond
  25. 0025rewrite hsumfirst at hidentity
  26. 0026rewrite hsumfirst at hidentity
  27. 0027rewrite hsumsecond at hidentity
  28. 0028rewrite hsumsecond at hidentity
  29. 0029have hscaled : (p * 2) * (2 * 1) = (2 * u) * (2 * u) + (2 * v) * (2 * v) + (2 * w) * (2 * w) + (2 * x) * (2 * x)
  30. 0030trans (a * a + b * b + c * c + d * d) * 2
  31. 0031congr
  32. 0032exact hnorm
  33. 0033apply mul_one
  34. 0034trans (((2 * u) * (2 * u) + (2 * v) * (2 * v)) + ((2 * w) * (2 * w) + (2 * x) * (2 * x)))
  35. 0035exact hidentity
  36. 0036symm
  37. 0037apply add_assoc
  38. 0038exists u
  39. 0039exists v
  40. 0040exists w
  41. 0041exists x
  42. 0042trans p * 1
  43. 0043symm
  44. 0044apply mul_one
  45. 0045specialize four_square_descent_scaled_norm_quotient p
  46. 0046specialize four_square_descent_scaled_norm_quotient 2
  47. 0047specialize four_square_descent_scaled_norm_quotient 1
  48. 0048specialize four_square_descent_scaled_norm_quotient u
  49. 0049specialize four_square_descent_scaled_norm_quotient v
  50. 0050specialize four_square_descent_scaled_norm_quotient w
  51. 0051specialize four_square_descent_scaled_norm_quotient x
  52. 0052apply four_square_descent_scaled_norm_quotient
  53. 0053intro hzero
  54. 0054specialize succ_ne_zero 1
  55. 0055apply succ_ne_zero
  56. 0056exact hzero
  57. 0057exact hscaled