FS001S

four_square_descent_even_multiplier_paired_halving

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

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

Constructive proof overview

Generated structural guide

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

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

FS001R four_square_descent_double_pair_identity FS001C four_square_descent_scaled_norm_quotient mul_one Stable theorem; checked-use authorized add_assoc Stable theorem; checked-use authorized succ_ne_zero Stable theorem; checked-use authorized

Direct dependents

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

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.

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