TS001M · theorem body

prime_floor_decoded_affine_collision_represents_prime

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

A genuinely decoded, distinct affine collision at the floor-square grid produces an exact representation of the prime as two natural squares.

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. ∀ s. ∀ r. ∀ i. ∀ j. ∀ i2. ∀ j2. ∀ k. ∀ k2. Prime(p) → FloorSqrt(p,s) → Dvd(p,r · r + 1) → k = S s · i + j → k2 = S s · i2 + j2 → Lt(k,S s · S s) → Lt(k2,S s · S s) → Lt(j,S s) → Lt(j2,S s) → ¬k = k2 → ModEq(p,r · i + j,r · i2 + j2) → ∃ x. ∃ y. 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

PD0002 Lt PD0003 Dvd PD0004 Prime PD0008 ModEq PD0051 FloorSqrt

In local proof propositions

PD0001 Le PD0002 Lt PD0003 Dvd
Exact expanded first-order statement
forall p s r i j i2 j2 k k2. ((~(p = 1) /\ forall frm_prime_left_ftpr_prime frm_prime_right_ftpr_prime. p = frm_prime_left_ftpr_prime * frm_prime_right_ftpr_prime -> frm_prime_left_ftpr_prime = 1 \/ frm_prime_right_ftpr_prime = 1)) -> (((exists bcs_sqrt_lower_gap_ftpr_floor. bcs_sqrt_lower_gap_ftpr_floor + (s) * (s) = (p)) /\ exists bcs_sqrt_upper_gap_ftpr_floor. bcs_sqrt_upper_gap_ftpr_floor + S (p) = S (s) * S (s))) -> (exists ftcn_factor_prime_root. (r * r + 1) = (p) * ftcn_factor_prime_root) -> k = S s * i + j -> k2 = S s * i2 + j2 -> (exists ftcn_strict_prime_index_first. ftcn_strict_prime_index_first + S (k) = (S s * S s)) -> (exists ftcn_strict_prime_index_second. ftcn_strict_prime_index_second + S (k2) = (S s * S s)) -> (exists ftcn_strict_prime_column_first. ftcn_strict_prime_column_first + S (j) = (S s)) -> (exists ftcn_strict_prime_column_second. ftcn_strict_prime_column_second + S (j2) = (S s)) -> ~(k = k2) -> (exists ftcn_left_prime_affine ftcn_right_prime_affine. (r * i + j) + (p) * ftcn_left_prime_affine = (r * i2 + j2) + (p) * ftcn_right_prime_affine) -> exists x y. p = x * x + y * y

Proof neighborhood

Direct theorem prerequisites

TS001D affine_collision_absolute_difference_norm_multiple TS001F flat_square_index_row_below_width TS001J strict_successor_coordinate_bound_is_weak_bound TS001B bounded_natural_absolute_difference TS001I distinct_flat_indices_have_positive_difference_norm TS000K prime_floor_bounded_divisible_norm_represents_prime

Direct theorem dependents

TS001N prime_floor_affine_grid_collision_represents_prime

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

117 script commands · 17 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 (6)
affine collision absolute difference norm multipleflat square index row below widthstrict successor coordinate bound is weak boundbounded natural absolute differencedistinct flat indices have positive difference normprime floor bounded divisible norm represents prime
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro s
  3. L3
    intro r
  4. L4
    intro i
  5. L5
    intro j
  6. L6
    intro i2
  7. L7
    intro j2
  8. L8
    intro k
  9. L9
    intro k2
  10. L10
    intro hprime
02Fix variables and assumptionsL11–20

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

  1. L11
    intro hfloor
  2. L12
    intro hroot
  3. L13
    intro hindex
  4. L14
    intro hindex2
  5. L15
    intro hbound
  6. L16
    intro hbound2
  7. L17
    intro hcolumn
  8. L18
    intro hcolumn2
  9. L19
    intro hdistinct
  10. L20
    intro haffine
03Establish hnormL21–30

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply affine collision absolute difference norm multiple.

  1. L21
    have hnorm : ∃ x. ∃ y. (i = i2 + x ∨ i2 = i + x) ∧ ((j = j2 + y ∨ j2 = j + y) ∧ Dvd(p,x · x + y · y))Definitions: Dvd(p,x · x + y · y)Original native command in the exact edition
  2. L22
    specialize affine_collision_absolute_difference_norm_multiple p
  3. L23
    specialize affine_collision_absolute_difference_norm_multiple r
  4. L24
    specialize affine_collision_absolute_difference_norm_multiple i
  5. L25
    specialize affine_collision_absolute_difference_norm_multiple j
  6. L26
    specialize affine_collision_absolute_difference_norm_multiple i2
  7. L27
    specialize affine_collision_absolute_difference_norm_multiple j2
  8. L28
    apply affine_collision_absolute_difference_norm_multiple
  9. L29
    exact hroot
  10. L30
    exact haffine
04Separate the logical casesL31–34

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

  1. L31
    cases hnorm
  2. L32
    cases hnorm_witness
  3. L33
    cases hnorm_witness_witness
  4. L34
    cases hnorm_witness_witness_right
05Establish hrowL35–42

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply flat square index row below width.

  1. L35
  2. L36
    specialize flat_square_index_row_below_width (S s)
  3. L37
    specialize flat_square_index_row_below_width i
  4. L38
    specialize flat_square_index_row_below_width j
  5. L39
    specialize flat_square_index_row_below_width k
  6. L40
    apply flat_square_index_row_below_width
  7. L41
    exact hindex
  8. L42
    exact hbound
06Establish hrow2L43–50

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply flat square index row below width.

  1. L43
    have hrow2 : Lt(i2,S s)Definitions: Lt(i2,S s)Original native command in the exact edition
  2. L44
    specialize flat_square_index_row_below_width (S s)
  3. L45
    specialize flat_square_index_row_below_width i2
  4. L46
    specialize flat_square_index_row_below_width j2
  5. L47
    specialize flat_square_index_row_below_width k2
  6. L48
    apply flat_square_index_row_below_width
  7. L49
    exact hindex2
  8. L50
    exact hbound2
07Establish hiL51–55

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply strict successor coordinate bound is weak bound.

  1. L51
  2. L52
    specialize strict_successor_coordinate_bound_is_weak_bound i
  3. L53
    specialize strict_successor_coordinate_bound_is_weak_bound s
  4. L54
    apply strict_successor_coordinate_bound_is_weak_bound
  5. L55
    exact hrow
08Establish hi2L56–60

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply strict successor coordinate bound is weak bound.

  1. L56
  2. L57
    specialize strict_successor_coordinate_bound_is_weak_bound i2
  3. L58
    specialize strict_successor_coordinate_bound_is_weak_bound s
  4. L59
    apply strict_successor_coordinate_bound_is_weak_bound
  5. L60
    exact hrow2
09Establish hjL61–65

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply strict successor coordinate bound is weak bound.

  1. L61
  2. L62
    specialize strict_successor_coordinate_bound_is_weak_bound j
  3. L63
    specialize strict_successor_coordinate_bound_is_weak_bound s
  4. L64
    apply strict_successor_coordinate_bound_is_weak_bound
  5. L65
    exact hcolumn
10Establish hj2L66–70

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply strict successor coordinate bound is weak bound.

  1. L66
  2. L67
    specialize strict_successor_coordinate_bound_is_weak_bound j2
  3. L68
    specialize strict_successor_coordinate_bound_is_weak_bound s
  4. L69
    apply strict_successor_coordinate_bound_is_weak_bound
  5. L70
    exact hcolumn2
11Establish hxL71–79

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bounded natural absolute difference.

  1. L71
  2. L72
    specialize bounded_natural_absolute_difference s
  3. L73
    specialize bounded_natural_absolute_difference i
  4. L74
    specialize bounded_natural_absolute_difference i2
  5. L75
    specialize bounded_natural_absolute_difference x
  6. L76
    apply bounded_natural_absolute_difference
  7. L77
    exact hi
  8. L78
    exact hi2
  9. L79
    exact hnorm_witness_witness_left
12Establish hyL80–88

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bounded natural absolute difference.

  1. L80
  2. L81
    specialize bounded_natural_absolute_difference s
  3. L82
    specialize bounded_natural_absolute_difference j
  4. L83
    specialize bounded_natural_absolute_difference j2
  5. L84
    specialize bounded_natural_absolute_difference x1
  6. L85
    apply bounded_natural_absolute_difference
  7. L86
    exact hj
  8. L87
    exact hj2
  9. L88
    exact hnorm_witness_witness_right_left
13Establish hpositiveL89–98

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

  1. L89
    have hpositive : Lt(0,x · x + x1 · x1)Definitions: Lt(0,x · x + x1 · x1)Original native command in the exact edition
  2. L90
    specialize distinct_flat_indices_have_positive_difference_norm (S s)
  3. L91
    specialize distinct_flat_indices_have_positive_difference_norm k
  4. L92
    specialize distinct_flat_indices_have_positive_difference_norm k2
  5. L93
    specialize distinct_flat_indices_have_positive_difference_norm i
  6. L94
    specialize distinct_flat_indices_have_positive_difference_norm j
  7. L95
    specialize distinct_flat_indices_have_positive_difference_norm i2
  8. L96
    specialize distinct_flat_indices_have_positive_difference_norm j2
  9. L97
    specialize distinct_flat_indices_have_positive_difference_norm x
  10. L98
    specialize distinct_flat_indices_have_positive_difference_norm x1
14Use earlier factsL99–104

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

  1. L99
    apply distinct_flat_indices_have_positive_difference_norm
  2. L100
    exact hindex
  3. L101
    exact hindex2
  4. L102
    exact hdistinct
  5. L103
    exact hnorm_witness_witness_left
  6. L104
    exact hnorm_witness_witness_right_left
15Construct an explicit witnessL105–106

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

  1. L105
    exists x
  2. L106
    exists x1
16Use earlier factsL107–116

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

  1. L107
    specialize prime_floor_bounded_divisible_norm_represents_prime p
  2. L108
    specialize prime_floor_bounded_divisible_norm_represents_prime s
  3. L109
    specialize prime_floor_bounded_divisible_norm_represents_prime x
  4. L110
    specialize prime_floor_bounded_divisible_norm_represents_prime x1
  5. L111
    apply prime_floor_bounded_divisible_norm_represents_prime
  6. L112
    exact hprime
  7. L113
    exact hfloor
  8. L114
    exact hx
  9. L115
    exact hy
  10. L116
    exact hpositive
17Use earlier factsL117–117

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

  1. L117
    exact hnorm_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 117 lines
  1. 0001intro p
  2. 0002intro s
  3. 0003intro r
  4. 0004intro i
  5. 0005intro j
  6. 0006intro i2
  7. 0007intro j2
  8. 0008intro k
  9. 0009intro k2
  10. 0010intro hprime
  11. 0011intro hfloor
  12. 0012intro hroot
  13. 0013intro hindex
  14. 0014intro hindex2
  15. 0015intro hbound
  16. 0016intro hbound2
  17. 0017intro hcolumn
  18. 0018intro hcolumn2
  19. 0019intro hdistinct
  20. 0020intro haffine
  21. 0021have hnorm : ∃ x. ∃ y. (i = i2 + x ∨ i2 = i + x) ∧ ((j = j2 + y ∨ j2 = j + y) ∧ Dvd(p,x · x + y · y))
    Exact native replay linehave hnorm : exists x y. ((((i) = (i2) + (x) \/ (i2) = (i) + (x))) /\ ((((j) = (j2) + (y) \/ (j2) = (j) + (y))) /\ (exists ftcn_factor_prime_norm. (x * x + y * y) = (p) * ftcn_factor_prime_norm)))
  22. 0022specialize affine_collision_absolute_difference_norm_multiple p
  23. 0023specialize affine_collision_absolute_difference_norm_multiple r
  24. 0024specialize affine_collision_absolute_difference_norm_multiple i
  25. 0025specialize affine_collision_absolute_difference_norm_multiple j
  26. 0026specialize affine_collision_absolute_difference_norm_multiple i2
  27. 0027specialize affine_collision_absolute_difference_norm_multiple j2
  28. 0028apply affine_collision_absolute_difference_norm_multiple
  29. 0029exact hroot
  30. 0030exact haffine
  31. 0031cases hnorm
  32. 0032cases hnorm_witness
  33. 0033cases hnorm_witness_witness
  34. 0034cases hnorm_witness_witness_right
  35. 0035have hrow : Lt(i,S s)
    Exact native replay linehave hrow : exists ftcn_strict_decoded_row. ftcn_strict_decoded_row + S (i) = (S s)
  36. 0036specialize flat_square_index_row_below_width (S s)
  37. 0037specialize flat_square_index_row_below_width i
  38. 0038specialize flat_square_index_row_below_width j
  39. 0039specialize flat_square_index_row_below_width k
  40. 0040apply flat_square_index_row_below_width
  41. 0041exact hindex
  42. 0042exact hbound
  43. 0043have hrow2 : Lt(i2,S s)
    Exact native replay linehave hrow2 : exists ftcn_strict_decoded_row2. ftcn_strict_decoded_row2 + S (i2) = (S s)
  44. 0044specialize flat_square_index_row_below_width (S s)
  45. 0045specialize flat_square_index_row_below_width i2
  46. 0046specialize flat_square_index_row_below_width j2
  47. 0047specialize flat_square_index_row_below_width k2
  48. 0048apply flat_square_index_row_below_width
  49. 0049exact hindex2
  50. 0050exact hbound2
  51. 0051have hi : Le(i,s)
    Exact native replay linehave hi : exists ftcn_bound_decoded_i. ftcn_bound_decoded_i + (i) = (s)
  52. 0052specialize strict_successor_coordinate_bound_is_weak_bound i
  53. 0053specialize strict_successor_coordinate_bound_is_weak_bound s
  54. 0054apply strict_successor_coordinate_bound_is_weak_bound
  55. 0055exact hrow
  56. 0056have hi2 : Le(i2,s)
    Exact native replay linehave hi2 : exists ftcn_bound_decoded_i2. ftcn_bound_decoded_i2 + (i2) = (s)
  57. 0057specialize strict_successor_coordinate_bound_is_weak_bound i2
  58. 0058specialize strict_successor_coordinate_bound_is_weak_bound s
  59. 0059apply strict_successor_coordinate_bound_is_weak_bound
  60. 0060exact hrow2
  61. 0061have hj : Le(j,s)
    Exact native replay linehave hj : exists ftcn_bound_decoded_j. ftcn_bound_decoded_j + (j) = (s)
  62. 0062specialize strict_successor_coordinate_bound_is_weak_bound j
  63. 0063specialize strict_successor_coordinate_bound_is_weak_bound s
  64. 0064apply strict_successor_coordinate_bound_is_weak_bound
  65. 0065exact hcolumn
  66. 0066have hj2 : Le(j2,s)
    Exact native replay linehave hj2 : exists ftcn_bound_decoded_j2. ftcn_bound_decoded_j2 + (j2) = (s)
  67. 0067specialize strict_successor_coordinate_bound_is_weak_bound j2
  68. 0068specialize strict_successor_coordinate_bound_is_weak_bound s
  69. 0069apply strict_successor_coordinate_bound_is_weak_bound
  70. 0070exact hcolumn2
  71. 0071have hx : Le(x,s)
    Exact native replay linehave hx : exists ftcn_bound_decoded_x. ftcn_bound_decoded_x + (x) = (s)
  72. 0072specialize bounded_natural_absolute_difference s
  73. 0073specialize bounded_natural_absolute_difference i
  74. 0074specialize bounded_natural_absolute_difference i2
  75. 0075specialize bounded_natural_absolute_difference x
  76. 0076apply bounded_natural_absolute_difference
  77. 0077exact hi
  78. 0078exact hi2
  79. 0079exact hnorm_witness_witness_left
  80. 0080have hy : Le(x1,s)
    Exact native replay linehave hy : exists ftcn_bound_decoded_y. ftcn_bound_decoded_y + (x1) = (s)
  81. 0081specialize bounded_natural_absolute_difference s
  82. 0082specialize bounded_natural_absolute_difference j
  83. 0083specialize bounded_natural_absolute_difference j2
  84. 0084specialize bounded_natural_absolute_difference x1
  85. 0085apply bounded_natural_absolute_difference
  86. 0086exact hj
  87. 0087exact hj2
  88. 0088exact hnorm_witness_witness_right_left
  89. 0089have hpositive : Lt(0,x · x + x1 · x1)
    Exact native replay linehave hpositive : exists ftcn_strict_decoded_positive. ftcn_strict_decoded_positive + S (0) = (x * x + x1 * x1)
  90. 0090specialize distinct_flat_indices_have_positive_difference_norm (S s)
  91. 0091specialize distinct_flat_indices_have_positive_difference_norm k
  92. 0092specialize distinct_flat_indices_have_positive_difference_norm k2
  93. 0093specialize distinct_flat_indices_have_positive_difference_norm i
  94. 0094specialize distinct_flat_indices_have_positive_difference_norm j
  95. 0095specialize distinct_flat_indices_have_positive_difference_norm i2
  96. 0096specialize distinct_flat_indices_have_positive_difference_norm j2
  97. 0097specialize distinct_flat_indices_have_positive_difference_norm x
  98. 0098specialize distinct_flat_indices_have_positive_difference_norm x1
  99. 0099apply distinct_flat_indices_have_positive_difference_norm
  100. 0100exact hindex
  101. 0101exact hindex2
  102. 0102exact hdistinct
  103. 0103exact hnorm_witness_witness_left
  104. 0104exact hnorm_witness_witness_right_left
  105. 0105exists x
  106. 0106exists x1
  107. 0107specialize prime_floor_bounded_divisible_norm_represents_prime p
  108. 0108specialize prime_floor_bounded_divisible_norm_represents_prime s
  109. 0109specialize prime_floor_bounded_divisible_norm_represents_prime x
  110. 0110specialize prime_floor_bounded_divisible_norm_represents_prime x1
  111. 0111apply prime_floor_bounded_divisible_norm_represents_prime
  112. 0112exact hprime
  113. 0113exact hfloor
  114. 0114exact hx
  115. 0115exact hy
  116. 0116exact hpositive
  117. 0117exact hnorm_witness_witness_right_right