FS001R

four_square_descent_double_pair_identity

Alpha v34 independently verified · alpha_closed; checked-use authorized; 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.

Exact expanded first-order arithmetic 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)))

Constructive proof overview

Generated structural guide

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

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

FS000I four_square_two_square_factor_identity zero_add Stable theorem; checked-use authorized mul_one Stable theorem; checked-use authorized

Direct dependents

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

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.

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 exact 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