TS0024

prime_divisible_two_square_norm_unit_coordinate_yields_negative_one_root

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

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

Constructive proof overview

Generated structural guide

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

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

prime_mod_inverse Stable theorem; checked-use authorized TS0012 multiple_implies_balanced_zero_congruence mod_eq_mul Stable theorem; checked-use authorized one_mul Stable theorem; checked-use authorized mod_eq_mul_right Stable theorem; checked-use authorized TS0022 two_square_scaled_norm_identity mul_zero_left Stable theorem; checked-use authorized 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 TS0011 balanced_zero_congruence_implies_multiple TS0023 negative_one_norm_multiple_yields_predecessor_residue

Direct dependents

TS0026 three_mod_four_prime_norm_divisor_forces_second_coordinate

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

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.

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 : exists z u v. b * z + p * u = 1 + p * v
  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 : exists ftcn_left_ftsc_inverse ftcn_right_ftsc_inverse. (b * x) + (p) * ftcn_left_ftsc_inverse = (1) + (p) * ftcn_right_ftsc_inverse
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 : 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
  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 : 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
  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 : 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
  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 : 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
  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 : 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
  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 : 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
  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 : 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
  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 : exists ftcn_factor_ftsc_root_multiple. ((a * x) * (a * x) + 1) = (p) * ftcn_factor_ftsc_root_multiple
  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 exact 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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