TS0007 · theorem body

predecessor_square_congruence_yields_divisible_norm

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

Statement with defined notation

∀ p. ∀ n. ∀ r. p = S n → ModEq(p,r · r,n) → Dvd(p,r · r + 1)

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 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)

Proof neighborhood

Direct theorem prerequisites

mod_eq_to_remainder_decomposition · Stable closed add_assoc · Stable closed add_comm · Stable closed zero_add · Stable closed mul_comm · Stable closed

Direct theorem dependents

TS0008 prime_mod_four_one_divisible_two_square_norm_exists TS0009 prime_mod_four_one_bounded_divisible_two_square_norm_exists

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

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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