TS0024 · theorem body

prime_divisible_two_square_norm_unit_coordinate_yields_negative_one_root

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

A prime dividing a²+b² but not b supplies an explicit modular root of minus one through the modular inverse of b.

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. ∀ n. ∀ a. ∀ b. p = S n → Prime(p) → Dvd(p,a · a + b · b) → ¬Dvd(p,b) → QRes(p,n)

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 PD0004 Prime PD0021 QRes

In local proof propositions

PD0003 Dvd PD0008 ModEq PD0031 BalancedInverse
Exact expanded first-order statement
forall p n a b. p = S n -> ((~(p = 1) /\ forall frm_prime_left_ftsc_prime frm_prime_right_ftsc_prime. p = frm_prime_left_ftsc_prime * frm_prime_right_ftsc_prime -> frm_prime_left_ftsc_prime = 1 \/ frm_prime_right_ftsc_prime = 1)) -> (exists ftcn_factor_ftsc_norm. (a * a + b * b) = (p) * ftcn_factor_ftsc_norm) -> ~(exists ftcn_factor_ftsc_unit_coordinate. (b) = (p) * ftcn_factor_ftsc_unit_coordinate) -> (exists qr_x_ftsc_predecessor. exists qr_u_ftsc_predecessor qr_v_ftsc_predecessor. qr_x_ftsc_predecessor * qr_x_ftsc_predecessor + p * qr_u_ftsc_predecessor = n + p * qr_v_ftsc_predecessor)

Proof neighborhood

Direct theorem prerequisites

prime_mod_inverse · Stable closed TS0012 multiple_implies_balanced_zero_congruence mod_eq_mul · Stable closed one_mul · Stable closed mod_eq_mul_right · Stable closed TS0022 two_square_scaled_norm_identity mul_zero_left · Stable closed mod_eq_refl · Stable closed mod_eq_add · Stable closed mod_eq_symm · Stable closed mod_eq_trans · Stable closed TS0011 balanced_zero_congruence_implies_multiple TS0023 negative_one_norm_multiple_yields_predecessor_residue

Direct theorem dependents

TS0026 three_mod_four_prime_norm_divisor_forces_second_coordinate

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

88 script commands · 19 reading checkpoints · 10 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 (4)
multiple implies balanced zero congruencetwo square scaled norm identitybalanced zero congruence implies multiplenegative one norm multiple yields predecessor residue
01Fix variables and assumptionsL1–8

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro a
  4. L4
    intro b
  5. L5
    intro hpredecessor
  6. L6
    intro hprime
  7. L7
    intro hnorm
  8. L8
    intro hunit
02Establish hinverseL9–14

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

  1. L9
    have hinverse : ∃ z. BalancedInverse(p,b,z)Definitions: BalancedInverse(p,b,z)Original native command in the exact edition
  2. L10
    specialize prime_mod_inverse p
  3. L11
    specialize prime_mod_inverse b
  4. L12
    apply prime_mod_inverse
  5. L13
    exact hprime
  6. L14
    exact hunit
03Separate the logical casesL15–17

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

  1. L15
    cases hinverse
  2. L16
    cases hinverse_witness
  3. L17
    cases hinverse_witness_witness
04Establish hinverse_modL18–18

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

  1. L18
    have hinverse_mod : BalancedInverse(p,b,x)Definitions: BalancedInverse(p,b,x)Original native command in the exact edition
05Construct an explicit witnessL19–20

Supply the displayed value, then prove that it has the required property.

  1. L19
    exists x1
  2. L20
    exists x2
06Use earlier factsL21–21

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L21
    exact hinverse_witness_witness_witness
07Establish hinverse_square_rawL22–31

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

  1. L22
    have hinverse_square_raw : ModEq(p,b · x · (b · x),1 · 1)Definitions: ModEq(p,b · x · (b · x),1 · 1)Original native command in the exact edition
  2. L23
    specialize mod_eq_mul p
  3. L24
    specialize mod_eq_mul (b * x)
  4. L25
    specialize mod_eq_mul 1
  5. L26
    specialize mod_eq_mul (b * x)
  6. L27
    specialize mod_eq_mul 1
  7. L28
    apply mod_eq_mul
  8. L29
    exact hinverse_mod
  9. L30
    exact hinverse_mod
  10. L31
    specialize one_mul 1
08Calculate and transport equalitiesL32–32

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

  1. L32
    rewrite one_mul at hinverse_square_raw
09Establish hnorm_modL33–37

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply multiple implies balanced zero congruence.

  1. L33
    have hnorm_mod : ModEq(p,a · a + b · b,0)Definitions: ModEq(p,a · a + b · b,0)Original native command in the exact edition
  2. L34
    specialize multiple_implies_balanced_zero_congruence p
  3. L35
    specialize multiple_implies_balanced_zero_congruence (a * a + b * b)
  4. L36
    apply multiple_implies_balanced_zero_congruence
  5. L37
    exact hnorm
10Establish hscaledL38–47

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

  1. L38
    have hscaled : ModEq(p,(a · a + b · b) · (x · x),0 · (x · x))Definitions: ModEq(p,(a · a + b · b) · (x · x),0 · (x · x))Original native command in the exact edition
  2. L39
    specialize mod_eq_mul_right p
  3. L40
    specialize mod_eq_mul_right (a * a + b * b)
  4. L41
    specialize mod_eq_mul_right 0
  5. L42
    specialize mod_eq_mul_right (x * x)
  6. L43
    apply mod_eq_mul_right
  7. L44
    exact hnorm_mod
  8. L45
    specialize two_square_scaled_norm_identity a
  9. L46
    specialize two_square_scaled_norm_identity b
  10. L47
    specialize two_square_scaled_norm_identity x
11Calculate and transport equalitiesL48–48

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

  1. L48
    rewrite two_square_scaled_norm_identity at hscaled
12Use earlier factsL49–49

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L49
    specialize mul_zero_left (x * x)
13Calculate and transport equalitiesL50–50

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

  1. L50
    rewrite mul_zero_left at hscaled
14Establish hselfL51–54

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

  1. L51
    have hself : ModEq(p,a · x · (a · x),a · x · (a · x))Definitions: ModEq(p,a · x · (a · x),a · x · (a · x))Original native command in the exact edition
  2. L52
    specialize mod_eq_refl p
  3. L53
    specialize mod_eq_refl ((a * x) * (a * x))
  4. L54
    exact mod_eq_refl
15Establish hreplaceL55–63

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

  1. L55
    have hreplace : ModEq(p,a · x · (a · x) + b · x · (b · x),a · x · (a · x) + 1)Definitions: ModEq(p,a · x · (a · x) + b · x · (b · x),a · x · (a · x) + 1)Original native command in the exact edition
  2. L56
    specialize mod_eq_add p
  3. L57
    specialize mod_eq_add ((a * x) * (a * x))
  4. L58
    specialize mod_eq_add ((a * x) * (a * x))
  5. L59
    specialize mod_eq_add ((b * x) * (b * x))
  6. L60
    specialize mod_eq_add 1
  7. L61
    apply mod_eq_add
  8. L62
    exact hself
  9. L63
    exact hinverse_square_raw
16Establish hreverseL64–69

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

  1. L64
    have hreverse : ModEq(p,a · x · (a · x) + 1,a · x · (a · x) + b · x · (b · x))Definitions: ModEq(p,a · x · (a · x) + 1,a · x · (a · x) + b · x · (b · x))Original native command in the exact edition
  2. L65
    specialize mod_eq_symm p
  3. L66
    specialize mod_eq_symm ((a * x) * (a * x) + (b * x) * (b * x))
  4. L67
    specialize mod_eq_symm ((a * x) * (a * x) + 1)
  5. L68
    apply mod_eq_symm
  6. L69
    exact hreplace
17Establish hroot_modL70–77

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

  1. L70
    have hroot_mod : ModEq(p,a · x · (a · x) + 1,0)Definitions: ModEq(p,a · x · (a · x) + 1,0)Original native command in the exact edition
  2. L71
    specialize mod_eq_trans p
  3. L72
    specialize mod_eq_trans ((a * x) * (a * x) + 1)
  4. L73
    specialize mod_eq_trans ((a * x) * (a * x) + (b * x) * (b * x))
  5. L74
    specialize mod_eq_trans 0
  6. L75
    apply mod_eq_trans
  7. L76
    exact hreverse
  8. L77
    exact hscaled
18Establish hroot_multipleL78–87

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply balanced zero congruence implies multiple.

  1. L78
    have hroot_multiple : Dvd(p,a · x · (a · x) + 1)Definitions: Dvd(p,a · x · (a · x) + 1)Original native command in the exact edition
  2. L79
    specialize balanced_zero_congruence_implies_multiple p
  3. L80
    specialize balanced_zero_congruence_implies_multiple ((a * x) * (a * x) + 1)
  4. L81
    apply balanced_zero_congruence_implies_multiple
  5. L82
    exact hroot_mod
  6. L83
    specialize negative_one_norm_multiple_yields_predecessor_residue p
  7. L84
    specialize negative_one_norm_multiple_yields_predecessor_residue n
  8. L85
    specialize negative_one_norm_multiple_yields_predecessor_residue (a * x)
  9. L86
    apply negative_one_norm_multiple_yields_predecessor_residue
  10. L87
    exact hpredecessor
19Use earlier factsL88–88

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L88
    exact hroot_multiple

Library-wide reading audit

Original defined command ledger · 88 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro a
  4. 0004intro b
  5. 0005intro hpredecessor
  6. 0006intro hprime
  7. 0007intro hnorm
  8. 0008intro hunit
  9. 0009have hinverse : ∃ z. BalancedInverse(p,b,z)
    Exact native replay linehave hinverse : exists z u v. b * z + p * u = 1 + p * v
  10. 0010specialize prime_mod_inverse p
  11. 0011specialize prime_mod_inverse b
  12. 0012apply prime_mod_inverse
  13. 0013exact hprime
  14. 0014exact hunit
  15. 0015cases hinverse
  16. 0016cases hinverse_witness
  17. 0017cases hinverse_witness_witness
  18. 0018have hinverse_mod : BalancedInverse(p,b,x)
    Exact native replay linehave hinverse_mod : exists ftcn_left_ftsc_inverse ftcn_right_ftsc_inverse. (b * x) + (p) * ftcn_left_ftsc_inverse = (1) + (p) * ftcn_right_ftsc_inverse
  19. 0019exists x1
  20. 0020exists x2
  21. 0021exact hinverse_witness_witness_witness
  22. 0022have hinverse_square_raw : ModEq(p,b · x · (b · x),1 · 1)
    Exact native replay linehave hinverse_square_raw : exists ftcn_left_ftsc_inverse_square_raw ftcn_right_ftsc_inverse_square_raw. ((b * x) * (b * x)) + (p) * ftcn_left_ftsc_inverse_square_raw = (1 * 1) + (p) * ftcn_right_ftsc_inverse_square_raw
  23. 0023specialize mod_eq_mul p
  24. 0024specialize mod_eq_mul (b * x)
  25. 0025specialize mod_eq_mul 1
  26. 0026specialize mod_eq_mul (b * x)
  27. 0027specialize mod_eq_mul 1
  28. 0028apply mod_eq_mul
  29. 0029exact hinverse_mod
  30. 0030exact hinverse_mod
  31. 0031specialize one_mul 1
  32. 0032rewrite one_mul at hinverse_square_raw
  33. 0033have hnorm_mod : ModEq(p,a · a + b · b,0)
    Exact native replay linehave hnorm_mod : exists ftcn_left_ftsc_norm_zero ftcn_right_ftsc_norm_zero. (a * a + b * b) + (p) * ftcn_left_ftsc_norm_zero = (0) + (p) * ftcn_right_ftsc_norm_zero
  34. 0034specialize multiple_implies_balanced_zero_congruence p
  35. 0035specialize multiple_implies_balanced_zero_congruence (a * a + b * b)
  36. 0036apply multiple_implies_balanced_zero_congruence
  37. 0037exact hnorm
  38. 0038have hscaled : ModEq(p,(a · a + b · b) · (x · x),0 · (x · x))
    Exact native replay linehave hscaled : exists ftcn_left_ftsc_scaled_zero ftcn_right_ftsc_scaled_zero. ((a * a + b * b) * (x * x)) + (p) * ftcn_left_ftsc_scaled_zero = (0 * (x * x)) + (p) * ftcn_right_ftsc_scaled_zero
  39. 0039specialize mod_eq_mul_right p
  40. 0040specialize mod_eq_mul_right (a * a + b * b)
  41. 0041specialize mod_eq_mul_right 0
  42. 0042specialize mod_eq_mul_right (x * x)
  43. 0043apply mod_eq_mul_right
  44. 0044exact hnorm_mod
  45. 0045specialize two_square_scaled_norm_identity a
  46. 0046specialize two_square_scaled_norm_identity b
  47. 0047specialize two_square_scaled_norm_identity x
  48. 0048rewrite two_square_scaled_norm_identity at hscaled
  49. 0049specialize mul_zero_left (x * x)
  50. 0050rewrite mul_zero_left at hscaled
  51. 0051have hself : ModEq(p,a · x · (a · x),a · x · (a · x))
    Exact native replay linehave hself : exists ftcn_left_ftsc_self ftcn_right_ftsc_self. ((a * x) * (a * x)) + (p) * ftcn_left_ftsc_self = ((a * x) * (a * x)) + (p) * ftcn_right_ftsc_self
  52. 0052specialize mod_eq_refl p
  53. 0053specialize mod_eq_refl ((a * x) * (a * x))
  54. 0054exact mod_eq_refl
  55. 0055have hreplace : ModEq(p,a · x · (a · x) + b · x · (b · x),a · x · (a · x) + 1)
    Exact native replay linehave hreplace : exists ftcn_left_ftsc_replace ftcn_right_ftsc_replace. ((a * x) * (a * x) + (b * x) * (b * x)) + (p) * ftcn_left_ftsc_replace = ((a * x) * (a * x) + 1) + (p) * ftcn_right_ftsc_replace
  56. 0056specialize mod_eq_add p
  57. 0057specialize mod_eq_add ((a * x) * (a * x))
  58. 0058specialize mod_eq_add ((a * x) * (a * x))
  59. 0059specialize mod_eq_add ((b * x) * (b * x))
  60. 0060specialize mod_eq_add 1
  61. 0061apply mod_eq_add
  62. 0062exact hself
  63. 0063exact hinverse_square_raw
  64. 0064have hreverse : ModEq(p,a · x · (a · x) + 1,a · x · (a · x) + b · x · (b · x))
    Exact native replay linehave hreverse : exists ftcn_left_ftsc_reverse ftcn_right_ftsc_reverse. ((a * x) * (a * x) + 1) + (p) * ftcn_left_ftsc_reverse = ((a * x) * (a * x) + (b * x) * (b * x)) + (p) * ftcn_right_ftsc_reverse
  65. 0065specialize mod_eq_symm p
  66. 0066specialize mod_eq_symm ((a * x) * (a * x) + (b * x) * (b * x))
  67. 0067specialize mod_eq_symm ((a * x) * (a * x) + 1)
  68. 0068apply mod_eq_symm
  69. 0069exact hreplace
  70. 0070have hroot_mod : ModEq(p,a · x · (a · x) + 1,0)
    Exact native replay linehave hroot_mod : exists ftcn_left_ftsc_root_mod ftcn_right_ftsc_root_mod. ((a * x) * (a * x) + 1) + (p) * ftcn_left_ftsc_root_mod = (0) + (p) * ftcn_right_ftsc_root_mod
  71. 0071specialize mod_eq_trans p
  72. 0072specialize mod_eq_trans ((a * x) * (a * x) + 1)
  73. 0073specialize mod_eq_trans ((a * x) * (a * x) + (b * x) * (b * x))
  74. 0074specialize mod_eq_trans 0
  75. 0075apply mod_eq_trans
  76. 0076exact hreverse
  77. 0077exact hscaled
  78. 0078have hroot_multiple : Dvd(p,a · x · (a · x) + 1)
    Exact native replay linehave hroot_multiple : exists ftcn_factor_ftsc_root_multiple. ((a * x) * (a * x) + 1) = (p) * ftcn_factor_ftsc_root_multiple
  79. 0079specialize balanced_zero_congruence_implies_multiple p
  80. 0080specialize balanced_zero_congruence_implies_multiple ((a * x) * (a * x) + 1)
  81. 0081apply balanced_zero_congruence_implies_multiple
  82. 0082exact hroot_mod
  83. 0083specialize negative_one_norm_multiple_yields_predecessor_residue p
  84. 0084specialize negative_one_norm_multiple_yields_predecessor_residue n
  85. 0085specialize negative_one_norm_multiple_yields_predecessor_residue (a * x)
  86. 0086apply negative_one_norm_multiple_yields_predecessor_residue
  87. 0087exact hpredecessor
  88. 0088exact hroot_multiple