TS0017

negative_one_congruent_square_norm_multiple

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

A root of minus one and either matching linear square yield an actual divisible two-square norm.

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 r x y. (exists ftcn_factor_root. (r * r + 1) = (p) * ftcn_factor_root) -> (exists ftcn_left_squared ftcn_right_squared. ((r * x) * (r * x)) + (p) * ftcn_left_squared = (y * y) + (p) * ftcn_right_squared) -> (exists ftcn_factor_norm. (x * x + y * y) = (p) * ftcn_factor_norm)

Constructive proof overview

Generated structural guide

A root of minus one and either matching linear square yield an actual divisible two-square norm.

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

TS0014 negative_one_scaled_square_congruent_zero mod_eq_refl Stable theorem; checked-use authorized mod_eq_add Stable theorem; checked-use authorized mod_eq_symm Stable theorem; checked-use authorized mod_eq_trans Stable theorem; checked-use authorized add_comm Stable theorem; checked-use authorized TS0011 balanced_zero_congruence_implies_multiple

Direct dependents

TS0018 negative_one_linear_congruence_norm_multiple TS0019 negative_one_opposite_linear_congruence_norm_multiple

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

46 script commands · 7 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 (2)
negative one scaled square congruent zerobalanced zero congruence implies multiple
01Fix variables and assumptionsL1–6

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

  1. L1
    intro p
  2. L2
    intro r
  3. L3
    intro x
  4. L4
    intro y
  5. L5
    intro hroot
  6. L6
    intro hsquare
02Establish hzeroL7–12

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply negative one scaled square congruent zero.

  1. L7
    have hzero : exists ftcn_left_norm_root ftcn_right_norm_root. ((r * x) * (r * x) + x * x) + (p) * ftcn_left_norm_root = (0) + (p) * ftcn_right_norm_root
  2. L8
    specialize negative_one_scaled_square_congruent_zero p
  3. L9
    specialize negative_one_scaled_square_congruent_zero r
  4. L10
    specialize negative_one_scaled_square_congruent_zero x
  5. L11
    apply negative_one_scaled_square_congruent_zero
  6. L12
    exact hroot
03Establish hsameL13–16

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

  1. L13
    have hsame : exists ftcn_left_norm_same ftcn_right_norm_same. (x * x) + (p) * ftcn_left_norm_same = (x * x) + (p) * ftcn_right_norm_same
  2. L14
    specialize mod_eq_refl p
  3. L15
    specialize mod_eq_refl (x * x)
  4. L16
    exact mod_eq_refl
04Establish haddL17–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq add.

  1. L17
    have hadd : exists ftcn_left_norm_added ftcn_right_norm_added. ((r * x) * (r * x) + x * x) + (p) * ftcn_left_norm_added = (y * y + x * x) + (p) * ftcn_right_norm_added
  2. L18
    specialize mod_eq_add p
  3. L19
    specialize mod_eq_add ((r * x) * (r * x))
  4. L20
    specialize mod_eq_add (y * y)
  5. L21
    specialize mod_eq_add (x * x)
  6. L22
    specialize mod_eq_add (x * x)
  7. L23
    apply mod_eq_add
  8. L24
    exact hsquare
  9. L25
    exact hsame
05Establish hreverseL26–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq symm.

  1. L26
    have hreverse : exists ftcn_left_norm_reverse ftcn_right_norm_reverse. (y * y + x * x) + (p) * ftcn_left_norm_reverse = ((r * x) * (r * x) + x * x) + (p) * ftcn_right_norm_reverse
  2. L27
    specialize mod_eq_symm p
  3. L28
    specialize mod_eq_symm ((r * x) * (r * x) + x * x)
  4. L29
    specialize mod_eq_symm (y * y + x * x)
  5. L30
    apply mod_eq_symm
  6. L31
    exact hadd
06Establish hnormL32–39

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq trans.

  1. L32
    have hnorm : exists ftcn_left_norm_zero ftcn_right_norm_zero. (y * y + x * x) + (p) * ftcn_left_norm_zero = (0) + (p) * ftcn_right_norm_zero
  2. L33
    specialize mod_eq_trans p
  3. L34
    specialize mod_eq_trans (y * y + x * x)
  4. L35
    specialize mod_eq_trans ((r * x) * (r * x) + x * x)
  5. L36
    specialize mod_eq_trans 0
  6. L37
    apply mod_eq_trans
  7. L38
    exact hreverse
  8. L39
    exact hzero
07Establish horderL40–46

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

  1. L40
    have horder : y * y + x * x = x * x + y * y
  2. L41
    apply add_comm
  3. L42
    rewrite horder at hnorm
  4. L43
    specialize balanced_zero_congruence_implies_multiple p
  5. L44
    specialize balanced_zero_congruence_implies_multiple (x * x + y * y)
  6. L45
    apply balanced_zero_congruence_implies_multiple
  7. L46
    exact hnorm

Library-wide reading audit

Original exact command ledger · 46 lines
  1. 0001intro p
  2. 0002intro r
  3. 0003intro x
  4. 0004intro y
  5. 0005intro hroot
  6. 0006intro hsquare
  7. 0007have hzero : exists ftcn_left_norm_root ftcn_right_norm_root. ((r * x) * (r * x) + x * x) + (p) * ftcn_left_norm_root = (0) + (p) * ftcn_right_norm_root
  8. 0008specialize negative_one_scaled_square_congruent_zero p
  9. 0009specialize negative_one_scaled_square_congruent_zero r
  10. 0010specialize negative_one_scaled_square_congruent_zero x
  11. 0011apply negative_one_scaled_square_congruent_zero
  12. 0012exact hroot
  13. 0013have hsame : exists ftcn_left_norm_same ftcn_right_norm_same. (x * x) + (p) * ftcn_left_norm_same = (x * x) + (p) * ftcn_right_norm_same
  14. 0014specialize mod_eq_refl p
  15. 0015specialize mod_eq_refl (x * x)
  16. 0016exact mod_eq_refl
  17. 0017have hadd : exists ftcn_left_norm_added ftcn_right_norm_added. ((r * x) * (r * x) + x * x) + (p) * ftcn_left_norm_added = (y * y + x * x) + (p) * ftcn_right_norm_added
  18. 0018specialize mod_eq_add p
  19. 0019specialize mod_eq_add ((r * x) * (r * x))
  20. 0020specialize mod_eq_add (y * y)
  21. 0021specialize mod_eq_add (x * x)
  22. 0022specialize mod_eq_add (x * x)
  23. 0023apply mod_eq_add
  24. 0024exact hsquare
  25. 0025exact hsame
  26. 0026have hreverse : exists ftcn_left_norm_reverse ftcn_right_norm_reverse. (y * y + x * x) + (p) * ftcn_left_norm_reverse = ((r * x) * (r * x) + x * x) + (p) * ftcn_right_norm_reverse
  27. 0027specialize mod_eq_symm p
  28. 0028specialize mod_eq_symm ((r * x) * (r * x) + x * x)
  29. 0029specialize mod_eq_symm (y * y + x * x)
  30. 0030apply mod_eq_symm
  31. 0031exact hadd
  32. 0032have hnorm : exists ftcn_left_norm_zero ftcn_right_norm_zero. (y * y + x * x) + (p) * ftcn_left_norm_zero = (0) + (p) * ftcn_right_norm_zero
  33. 0033specialize mod_eq_trans p
  34. 0034specialize mod_eq_trans (y * y + x * x)
  35. 0035specialize mod_eq_trans ((r * x) * (r * x) + x * x)
  36. 0036specialize mod_eq_trans 0
  37. 0037apply mod_eq_trans
  38. 0038exact hreverse
  39. 0039exact hzero
  40. 0040have horder : y * y + x * x = x * x + y * y
  41. 0041apply add_comm
  42. 0042rewrite horder at hnorm
  43. 0043specialize balanced_zero_congruence_implies_multiple p
  44. 0044specialize balanced_zero_congruence_implies_multiple (x * x + y * y)
  45. 0045apply balanced_zero_congruence_implies_multiple
  46. 0046exact hnorm