FS001R · theorem body

four_square_descent_double_pair_identity

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

Multiplication by the two-square norm 1²+1² gives a fully explicit paired four-square doubling identity.

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 a b c d v x. (a = b + 2 * v \/ b = a + 2 * v) -> (c = d + 2 * x \/ d = c + 2 * x) -> (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)))

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 a b c d v x. (a = b + 2 * v \/ b = a + 2 * v) -> (c = d + 2 * x \/ d = c + 2 * x) -> (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)))

Proof neighborhood

Direct theorem prerequisites

FS000I four_square_two_square_factor_identity zero_add · Stable closed mul_one · Stable closed

Direct theorem dependents

FS001S four_square_descent_even_multiplier_paired_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

48 script commands · 15 reading checkpoints · 6 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 (1)
four square two square factor identity
01Fix variables and assumptionsL1–8

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro d
  5. L5
    intro v
  6. L6
    intro x
  7. L7
    intro hfirst
  8. L8
    intro hsecond
02Establish hidentityL9–18

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

  1. L9
    have hidentity : (a * a + b * b + c * c + d * d) * (1 * 1 + 1 * 1) = (((a * 1 + b * 1) * (a * 1 + b * 1) + (2 * v) * (2 * v)) + ((c * 1 + d * 1) * (c * 1 + d * 1) + (2 * x) * (2 * x)))
  2. L10
    specialize four_square_two_square_factor_identity a
  3. L11
    specialize four_square_two_square_factor_identity b
  4. L12
    specialize four_square_two_square_factor_identity c
  5. L13
    specialize four_square_two_square_factor_identity d
  6. L14
    specialize four_square_two_square_factor_identity 1
  7. L15
    specialize four_square_two_square_factor_identity 1
  8. L16
    specialize four_square_two_square_factor_identity (2 * v)
  9. L17
    specialize four_square_two_square_factor_identity (2 * x)
  10. L18
    apply four_square_two_square_factor_identity
03Separate the logical casesL19–20

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

  1. L19
    cases hfirst
  2. L20
    left
04Calculate and transport equalitiesL21–21

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

  1. L21
    simp [zero_add]
05Separate the logical casesL22–22

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

  1. L22
    right
06Calculate and transport equalitiesL23–23

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

  1. L23
    simp [zero_add]
07Separate the logical casesL24–25

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

  1. L24
    cases hsecond
  2. L25
    left
08Calculate and transport equalitiesL26–26

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

  1. L26
    simp [zero_add]
09Separate the logical casesL27–27

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

  1. L27
    right
10Calculate and transport equalitiesL28–28

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

  1. L28
    simp [zero_add]
11Establish htwoL29–31

Establish this local claim before using it. It is not an additional assumption.

  1. L29
    have htwo : 1 * 1 + 1 * 1 = 2
  2. L30
    norm_num
  3. L31
    rewrite htwo at hidentity
12Establish haoneL32–35

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

  1. L32
    have haone : a * 1 = a
  2. L33
    apply mul_one
  3. L34
    rewrite haone at hidentity
  4. L35
    rewrite haone at hidentity
13Establish hboneL36–39

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

  1. L36
    have hbone : b * 1 = b
  2. L37
    apply mul_one
  3. L38
    rewrite hbone at hidentity
  4. L39
    rewrite hbone at hidentity
14Establish hconeL40–43

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

  1. L40
    have hcone : c * 1 = c
  2. L41
    apply mul_one
  3. L42
    rewrite hcone at hidentity
  4. L43
    rewrite hcone at hidentity
15Establish hdoneL44–48

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

  1. L44
    have hdone : d * 1 = d
  2. L45
    apply mul_one
  3. L46
    rewrite hdone at hidentity
  4. L47
    rewrite hdone at hidentity
  5. L48
    exact hidentity

Library-wide reading audit

Original defined command ledger · 48 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro v
  6. 0006intro x
  7. 0007intro hfirst
  8. 0008intro hsecond
  9. 0009have hidentity : (a * a + b * b + c * c + d * d) * (1 * 1 + 1 * 1) = (((a * 1 + b * 1) * (a * 1 + b * 1) + (2 * v) * (2 * v)) + ((c * 1 + d * 1) * (c * 1 + d * 1) + (2 * x) * (2 * x)))
  10. 0010specialize four_square_two_square_factor_identity a
  11. 0011specialize four_square_two_square_factor_identity b
  12. 0012specialize four_square_two_square_factor_identity c
  13. 0013specialize four_square_two_square_factor_identity d
  14. 0014specialize four_square_two_square_factor_identity 1
  15. 0015specialize four_square_two_square_factor_identity 1
  16. 0016specialize four_square_two_square_factor_identity (2 * v)
  17. 0017specialize four_square_two_square_factor_identity (2 * x)
  18. 0018apply four_square_two_square_factor_identity
  19. 0019cases hfirst
  20. 0020left
  21. 0021simp [zero_add]
  22. 0022right
  23. 0023simp [zero_add]
  24. 0024cases hsecond
  25. 0025left
  26. 0026simp [zero_add]
  27. 0027right
  28. 0028simp [zero_add]
  29. 0029have htwo : 1 * 1 + 1 * 1 = 2
  30. 0030norm_num
  31. 0031rewrite htwo at hidentity
  32. 0032have haone : a * 1 = a
  33. 0033apply mul_one
  34. 0034rewrite haone at hidentity
  35. 0035rewrite haone at hidentity
  36. 0036have hbone : b * 1 = b
  37. 0037apply mul_one
  38. 0038rewrite hbone at hidentity
  39. 0039rewrite hbone at hidentity
  40. 0040have hcone : c * 1 = c
  41. 0041apply mul_one
  42. 0042rewrite hcone at hidentity
  43. 0043rewrite hcone at hidentity
  44. 0044have hdone : d * 1 = d
  45. 0045apply mul_one
  46. 0046rewrite hdone at hidentity
  47. 0047rewrite hdone at hidentity
  48. 0048exact hidentity