TS0007

predecessor_square_congruence_yields_divisible_norm

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

A square congruent to the predecessor of a successor yields an explicit divisor of its norm r²+1.

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 r. p = S n -> (exists u v. r * r + p * u = n + p * v) -> (exists fts_factor_root_norm. r * r + 1 = p * fts_factor_root_norm)

Constructive proof overview

Generated structural guide

A square congruent to the predecessor of a successor yields an explicit divisor of its norm r²+1.

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

mod_eq_to_remainder_decomposition Stable theorem; checked-use authorized add_assoc Stable theorem; checked-use authorized add_comm Stable theorem; checked-use authorized zero_add Stable theorem; checked-use authorized mul_comm Stable theorem; checked-use authorized

Direct dependents

TS0008 prime_mod_four_one_divisible_two_square_norm_exists TS0009 prime_mod_four_one_bounded_divisible_two_square_norm_exists

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

64 script commands · 35 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.

01Fix variables and assumptionsL1–5

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro r
  4. L4
    intro hpredecessor
  5. L5
    intro hroot
02Separate the logical casesL6–7

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

  1. L6
    cases hroot
  2. L7
    cases hroot_witness
03Establish hzeroL8–8

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

  1. L8
    have hzero : exists u v. (r * r + 1) + p * u = 0 + p * v
04Construct an explicit witnessL9–10

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

  1. L9
    exists x
  2. L10
    exists S x1
05Calculate and transport equalitiesL11–11

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

  1. L11
    trans r * r + (1 + p * x)
06Use earlier factsL12–12

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

  1. L12
    apply add_assoc
07Calculate and transport equalitiesL13–15

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

  1. L13
    trans r * r + (p * x + 1)
  2. L14
    congr
  3. L15
    refl
08Use earlier factsL16–16

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

  1. L16
    apply add_comm
09Calculate and transport equalitiesL17–18

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

  1. L17
    trans (r * r + p * x) + 1
  2. L18
    symm
10Use earlier factsL19–19

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

  1. L19
    apply add_assoc
11Calculate and transport equalitiesL20–21

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

  1. L20
    trans (n + p * x1) + 1
  2. L21
    congr
12Use earlier factsL22–22

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

  1. L22
    exact hroot_witness_witness
13Calculate and transport equalitiesL23–24

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

  1. L23
    refl
  2. L24
    trans n + (p * x1 + 1)
14Use earlier factsL25–25

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

  1. L25
    apply add_assoc
15Calculate and transport equalitiesL26–28

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

  1. L26
    trans n + (1 + p * x1)
  2. L27
    congr
  3. L28
    refl
16Use earlier factsL29–29

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

  1. L29
    apply add_comm
17Calculate and transport equalitiesL30–31

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

  1. L30
    trans (n + 1) + p * x1
  2. L31
    symm
18Use earlier factsL32–32

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

  1. L32
    apply add_assoc
19Calculate and transport equalitiesL33–37

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

  1. L33
    trans p + p * x1
  2. L34
    congr
  3. L35
    trans S n
  4. L36
    simp
  5. L37
    symm
20Use earlier factsL38–38

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

  1. L38
    exact hpredecessor
21Calculate and transport equalitiesL39–40

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

  1. L39
    refl
  2. L40
    trans p * x1 + p
22Use earlier factsL41–41

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

  1. L41
    apply add_comm
23Calculate 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 * S x1
  2. L43
    symm
24Use earlier factsL44–44

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

  1. L44
    apply PA6
25Calculate and transport equalitiesL45–45

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

  1. L45
    symm
26Use earlier factsL46–46

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

  1. L46
    apply zero_add
27Establish hdivisionL47–55

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

  1. L47
    have hdivision : exists q. r * r + 1 = q * p + 0
  2. L48
    specialize mod_eq_to_remainder_decomposition p
  3. L49
    specialize mod_eq_to_remainder_decomposition (r * r + 1)
  4. L50
    specialize mod_eq_to_remainder_decomposition 0
  5. L51
    apply mod_eq_to_remainder_decomposition
  6. L52
    intro hzero_modulus
  7. L53
    rewrite hpredecessor at hzero_modulus
  8. L54
    apply PA1
  9. L55
    exact hzero_modulus
28Construct an explicit witnessL56–56

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

  1. L56
    exists n
29Calculate and transport equalitiesL57–58

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

  1. L57
    rewrite hpredecessor
  2. L58
    simp
30Use earlier factsL59–59

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

  1. L59
    exact hzero
31Separate the logical casesL60–60

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

  1. L60
    cases hdivision
32Construct an explicit witnessL61–61

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

  1. L61
    exists x2
33Calculate and transport equalitiesL62–62

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

  1. L62
    trans x2 * p + 0
34Use earlier factsL63–63

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

  1. L63
    exact hdivision_witness
35Calculate and transport equalitiesL64–64

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

  1. L64
    simp [mul_comm]

Library-wide reading audit

Original exact command ledger · 64 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro r
  4. 0004intro hpredecessor
  5. 0005intro hroot
  6. 0006cases hroot
  7. 0007cases hroot_witness
  8. 0008have hzero : exists u v. (r * r + 1) + p * u = 0 + p * v
  9. 0009exists x
  10. 0010exists S x1
  11. 0011trans r * r + (1 + p * x)
  12. 0012apply add_assoc
  13. 0013trans r * r + (p * x + 1)
  14. 0014congr
  15. 0015refl
  16. 0016apply add_comm
  17. 0017trans (r * r + p * x) + 1
  18. 0018symm
  19. 0019apply add_assoc
  20. 0020trans (n + p * x1) + 1
  21. 0021congr
  22. 0022exact hroot_witness_witness
  23. 0023refl
  24. 0024trans n + (p * x1 + 1)
  25. 0025apply add_assoc
  26. 0026trans n + (1 + p * x1)
  27. 0027congr
  28. 0028refl
  29. 0029apply add_comm
  30. 0030trans (n + 1) + p * x1
  31. 0031symm
  32. 0032apply add_assoc
  33. 0033trans p + p * x1
  34. 0034congr
  35. 0035trans S n
  36. 0036simp
  37. 0037symm
  38. 0038exact hpredecessor
  39. 0039refl
  40. 0040trans p * x1 + p
  41. 0041apply add_comm
  42. 0042trans p * S x1
  43. 0043symm
  44. 0044apply PA6
  45. 0045symm
  46. 0046apply zero_add
  47. 0047have hdivision : exists q. r * r + 1 = q * p + 0
  48. 0048specialize mod_eq_to_remainder_decomposition p
  49. 0049specialize mod_eq_to_remainder_decomposition (r * r + 1)
  50. 0050specialize mod_eq_to_remainder_decomposition 0
  51. 0051apply mod_eq_to_remainder_decomposition
  52. 0052intro hzero_modulus
  53. 0053rewrite hpredecessor at hzero_modulus
  54. 0054apply PA1
  55. 0055exact hzero_modulus
  56. 0056exists n
  57. 0057rewrite hpredecessor
  58. 0058simp
  59. 0059exact hzero
  60. 0060cases hdivision
  61. 0061exists x2
  62. 0062trans x2 * p + 0
  63. 0063exact hdivision_witness
  64. 0064simp [mul_comm]