TS0017 · theorem body

negative_one_congruent_square_norm_multiple

Alpha v34 checked-use · independently kernel and Lean verified; 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.

Statement with defined notation

∀ p. ∀ r. ∀ x. ∀ y. Dvd(p,r · r + 1) → ModEq(p,r · x · (r · x),y · y) → Dvd(p,x · x + y · y)

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

PD0003 Dvd PD0008 ModEq

In local proof propositions

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

Proof neighborhood

Direct theorem prerequisites

TS0014 negative_one_scaled_square_congruent_zero mod_eq_refl · Stable closed mod_eq_add · Stable closed mod_eq_symm · Stable closed mod_eq_trans · Stable closed add_comm · Stable closed TS0011 balanced_zero_congruence_implies_multiple

Direct theorem dependents

TS0018 negative_one_linear_congruence_norm_multiple TS0019 negative_one_opposite_linear_congruence_norm_multiple

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

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.

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)
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 : ModEq(p,r · x · (r · x) + x · x,0)Definitions: ModEq(p,r · x · (r · x) + x · x,0)Original native command in the exact edition
  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 : ModEq(p,x · x,x · x)Definitions: ModEq(p,x · x,x · x)Original native command in the exact edition
  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 : ModEq(p,r · x · (r · x) + x · x,y · y + x · x)Definitions: ModEq(p,r · x · (r · x) + x · x,y · y + x · x)Original native command in the exact edition
  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 : ModEq(p,y · y + x · x,r · x · (r · x) + x · x)Definitions: ModEq(p,y · y + x · x,r · x · (r · x) + x · x)Original native command in the exact edition
  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 : ModEq(p,y · y + x · x,0)Definitions: ModEq(p,y · y + x · x,0)Original native command in the exact edition
  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 defined 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 : ModEq(p,r · x · (r · x) + x · x,0)
    Exact native replay linehave 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 : ModEq(p,x · x,x · x)
    Exact native replay linehave 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 : ModEq(p,r · x · (r · x) + x · x,y · y + x · x)
    Exact native replay linehave 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 : ModEq(p,y · y + x · x,r · x · (r · x) + x · x)
    Exact native replay linehave 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 : ModEq(p,y · y + x · x,0)
    Exact native replay linehave 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