TS001N · theorem body

prime_floor_affine_grid_collision_represents_prime

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

Decoding both entries of a genuine beta-coded affine collision yields a complete constructive prime two-square representation.

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. ∀ b. ∀ c. ∀ l. l = S s · S s → Prime(p) → FloorSqrt(p,s) → Dvd(p,r · r + 1) → (∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ n. ∃ m. x = S s · y + z ∧ (Lt(z,S s) ∧ (r · y + z = p · n + m ∧ (Lt(m,p) ∧ BetaAt(b,c,x,m))))) → (∃ x. ∃ y. ∃ z. Lt(x,l) ∧ (Lt(y,l) ∧ (¬x = y ∧ (BetaAt(b,c,x,z) ∧ BetaAt(b,c,y,z))))) → ∃ 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 PD0013 BetaAt PD0051 FloorSqrt

In local proof propositions

PD0002 Lt PD0008 ModEq PD0013 BetaAt
Exact expanded first-order statement
forall p s r b c l. l = S s * S s -> ((~(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) -> (forall ftrg_index_ftpr_grid. (exists ftrg_gap_ftpr_grid_index. ftrg_gap_ftpr_grid_index + S (ftrg_index_ftpr_grid) = (l)) -> exists ftrg_row_ftpr_grid ftrg_column_ftpr_grid ftrg_quotient_ftpr_grid ftrg_remainder_ftpr_grid. ((ftrg_index_ftpr_grid) = (S s) * ftrg_row_ftpr_grid + ftrg_column_ftpr_grid /\ ((exists ftrg_gap_ftpr_grid_column. ftrg_gap_ftpr_grid_column + S (ftrg_column_ftpr_grid) = (S s)) /\ ((r * ftrg_row_ftpr_grid + ftrg_column_ftpr_grid = (p) * ftrg_quotient_ftpr_grid + ftrg_remainder_ftpr_grid) /\ ((exists ftrg_gap_ftpr_grid_residue. ftrg_gap_ftpr_grid_residue + S (ftrg_remainder_ftpr_grid) = (p)) /\ (((exists ff_h_ftrg_ftpr_grid_entry. ff_h_ftrg_ftpr_grid_entry + S (ftrg_remainder_ftpr_grid) = S ((S (ftrg_index_ftpr_grid)) * c)) /\ exists ff_q_ftrg_ftpr_grid_entry. b = ff_q_ftrg_ftpr_grid_entry * S ((S (ftrg_index_ftpr_grid)) * c) + (ftrg_remainder_ftpr_grid)))))))) -> (exists ftsp_first_ftpr_collision ftsp_second_ftpr_collision ftsp_value_ftpr_collision. ((exists ftsp_gap_ftpr_collision_first. ftsp_gap_ftpr_collision_first + S (ftsp_first_ftpr_collision) = l) /\ ((exists ftsp_gap_ftpr_collision_second. ftsp_gap_ftpr_collision_second + S (ftsp_second_ftpr_collision) = l) /\ (~(ftsp_first_ftpr_collision = ftsp_second_ftpr_collision) /\ ((((exists ff_h_ftsp_ftpr_collision_left. ff_h_ftsp_ftpr_collision_left + S (ftsp_value_ftpr_collision) = S ((S (ftsp_first_ftpr_collision)) * c)) /\ exists ff_q_ftsp_ftpr_collision_left. b = ff_q_ftsp_ftpr_collision_left * S ((S (ftsp_first_ftpr_collision)) * c) + (ftsp_value_ftpr_collision))) /\ (((exists ff_h_ftsp_ftpr_collision_right. ff_h_ftsp_ftpr_collision_right + S (ftsp_value_ftpr_collision) = S ((S (ftsp_second_ftpr_collision)) * c)) /\ exists ff_q_ftsp_ftpr_collision_right. b = ff_q_ftsp_ftpr_collision_right * S ((S (ftsp_second_ftpr_collision)) * c) + (ftsp_value_ftpr_collision)))))))) -> exists x y. p = x * x + y * y

Proof neighborhood

Direct theorem prerequisites

TS001K shared_beta_collision_remainders_equal TS001L equal_remainder_affine_values_balanced_congruent TS001M prime_floor_decoded_affine_collision_represents_prime

Direct theorem dependents

TS001O prime_mod_four_one_is_sum_of_two_squares

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

93 script commands · 16 reading checkpoints · 4 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 (3)
shared beta collision remainders equalequal remainder affine values balanced congruentprime floor decoded affine collision 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 b
  5. L5
    intro c
  6. L6
    intro l
  7. L7
    intro hlength
  8. L8
    intro hprime
  9. L9
    intro hfloor
  10. L10
    intro hroot
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hgrid
  2. L12
    intro hcollision
03Separate the logical casesL13–19

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

  1. L13
    cases hcollision
  2. L14
    cases hcollision_witness
  3. L15
    cases hcollision_witness_witness
  4. L16
    cases hcollision_witness_witness_witness
  5. L17
    cases hcollision_witness_witness_witness_right
  6. L18
    cases hcollision_witness_witness_witness_right_right
  7. L19
    cases hcollision_witness_witness_witness_right_right_right
04Establish hfirstpointL20–23

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

  1. L20
    have hfirstpoint : ∃ i. ∃ j. ∃ q. ∃ t. x = S s · i + j ∧ (Lt(j,S s) ∧ (r · i + j = p · q + t ∧ (Lt(t,p) ∧ BetaAt(b,c,x,t))))Definitions: Lt(j,S s)Lt(t,p)BetaAt(b,c,x,t)Original native command in the exact edition
  2. L21
    specialize hgrid x
  3. L22
    apply hgrid
  4. L23
    exact hcollision_witness_witness_witness_left
05Separate the logical casesL24–31

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

  1. L24
    cases hfirstpoint
  2. L25
    cases hfirstpoint_witness
  3. L26
    cases hfirstpoint_witness_witness
  4. L27
    cases hfirstpoint_witness_witness_witness
  5. L28
    cases hfirstpoint_witness_witness_witness_witness
  6. L29
    cases hfirstpoint_witness_witness_witness_witness_right
  7. L30
    cases hfirstpoint_witness_witness_witness_witness_right_right
  8. L31
    cases hfirstpoint_witness_witness_witness_witness_right_right_right
06Establish hsecondpointL32–35

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

  1. L32
    have hsecondpoint : ∃ i. ∃ j. ∃ q. ∃ t. x1 = S s · i + j ∧ (Lt(j,S s) ∧ (r · i + j = p · q + t ∧ (Lt(t,p) ∧ BetaAt(b,c,x1,t))))Definitions: Lt(j,S s)Lt(t,p)BetaAt(b,c,x1,t)Original native command in the exact edition
  2. L33
    specialize hgrid x1
  3. L34
    apply hgrid
  4. L35
    exact hcollision_witness_witness_witness_right_left
07Separate the logical casesL36–43

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

  1. L36
    cases hsecondpoint
  2. L37
    cases hsecondpoint_witness
  3. L38
    cases hsecondpoint_witness_witness
  4. L39
    cases hsecondpoint_witness_witness_witness
  5. L40
    cases hsecondpoint_witness_witness_witness_witness
  6. L41
    cases hsecondpoint_witness_witness_witness_witness_right
  7. L42
    cases hsecondpoint_witness_witness_witness_witness_right_right
  8. L43
    cases hsecondpoint_witness_witness_witness_witness_right_right_right
08Establish hremainderL44–53

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply shared beta collision remainders equal.

  1. L44
    have hremainder : x6 = x10
  2. L45
    specialize shared_beta_collision_remainders_equal b
  3. L46
    specialize shared_beta_collision_remainders_equal c
  4. L47
    specialize shared_beta_collision_remainders_equal x
  5. L48
    specialize shared_beta_collision_remainders_equal x1
  6. L49
    specialize shared_beta_collision_remainders_equal x6
  7. L50
    specialize shared_beta_collision_remainders_equal x10
  8. L51
    specialize shared_beta_collision_remainders_equal x2
  9. L52
    apply shared_beta_collision_remainders_equal
  10. L53
    exact hfirstpoint_witness_witness_witness_witness_right_right_right_right
09Use earlier factsL54–56

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

  1. L54
    exact hcollision_witness_witness_witness_right_right_right_left
  2. L55
    exact hsecondpoint_witness_witness_witness_witness_right_right_right_right
  3. L56
    exact hcollision_witness_witness_witness_right_right_right_right
10Calculate and transport equalitiesL57–57

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

  1. L57
    rewrite hremainder at hfirstpoint_witness_witness_witness_witness_right_right_left
11Establish haffineL58–67

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

  1. L58
    have haffine : ModEq(p,r · x3 + x4,r · x7 + x8)Definitions: ModEq(p,r · x3 + x4,r · x7 + x8)Original native command in the exact edition
  2. L59
    specialize equal_remainder_affine_values_balanced_congruent p
  3. L60
    specialize equal_remainder_affine_values_balanced_congruent r
  4. L61
    specialize equal_remainder_affine_values_balanced_congruent x3
  5. L62
    specialize equal_remainder_affine_values_balanced_congruent x4
  6. L63
    specialize equal_remainder_affine_values_balanced_congruent x5
  7. L64
    specialize equal_remainder_affine_values_balanced_congruent x7
  8. L65
    specialize equal_remainder_affine_values_balanced_congruent x8
  9. L66
    specialize equal_remainder_affine_values_balanced_congruent x9
  10. L67
    specialize equal_remainder_affine_values_balanced_congruent x10
12Use earlier factsL68–70

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

  1. L68
    apply equal_remainder_affine_values_balanced_congruent
  2. L69
    exact hfirstpoint_witness_witness_witness_witness_right_right_left
  3. L70
    exact hsecondpoint_witness_witness_witness_witness_right_right_left
13Calculate and transport equalitiesL71–72

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

  1. L71
    rewrite hlength at hcollision_witness_witness_witness_left
  2. L72
    rewrite hlength at hcollision_witness_witness_witness_right_left
14Use earlier factsL73–82

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

  1. L73
    specialize prime_floor_decoded_affine_collision_represents_prime p
  2. L74
    specialize prime_floor_decoded_affine_collision_represents_prime s
  3. L75
    specialize prime_floor_decoded_affine_collision_represents_prime r
  4. L76
    specialize prime_floor_decoded_affine_collision_represents_prime x3
  5. L77
    specialize prime_floor_decoded_affine_collision_represents_prime x4
  6. L78
    specialize prime_floor_decoded_affine_collision_represents_prime x7
  7. L79
    specialize prime_floor_decoded_affine_collision_represents_prime x8
  8. L80
    specialize prime_floor_decoded_affine_collision_represents_prime x
  9. L81
    specialize prime_floor_decoded_affine_collision_represents_prime x1
  10. L82
    apply prime_floor_decoded_affine_collision_represents_prime
15Use earlier factsL83–92

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

  1. L83
    exact hprime
  2. L84
    exact hfloor
  3. L85
    exact hroot
  4. L86
    exact hfirstpoint_witness_witness_witness_witness_left
  5. L87
    exact hsecondpoint_witness_witness_witness_witness_left
  6. L88
    exact hcollision_witness_witness_witness_left
  7. L89
    exact hcollision_witness_witness_witness_right_left
  8. L90
    exact hfirstpoint_witness_witness_witness_witness_right_left
  9. L91
    exact hsecondpoint_witness_witness_witness_witness_right_left
  10. L92
    exact hcollision_witness_witness_witness_right_right_left
16Use earlier factsL93–93

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

  1. L93
    exact haffine

Library-wide reading audit

Original defined command ledger · 93 lines
  1. 0001intro p
  2. 0002intro s
  3. 0003intro r
  4. 0004intro b
  5. 0005intro c
  6. 0006intro l
  7. 0007intro hlength
  8. 0008intro hprime
  9. 0009intro hfloor
  10. 0010intro hroot
  11. 0011intro hgrid
  12. 0012intro hcollision
  13. 0013cases hcollision
  14. 0014cases hcollision_witness
  15. 0015cases hcollision_witness_witness
  16. 0016cases hcollision_witness_witness_witness
  17. 0017cases hcollision_witness_witness_witness_right
  18. 0018cases hcollision_witness_witness_witness_right_right
  19. 0019cases hcollision_witness_witness_witness_right_right_right
  20. 0020have hfirstpoint : ∃ i. ∃ j. ∃ q. ∃ t. x = S s · i + j ∧ (Lt(j,S s) ∧ (r · i + j = p · q + t ∧ (Lt(t,p) ∧ BetaAt(b,c,x,t))))
    Exact native replay linehave hfirstpoint : exists i j q t. ((x) = (S s) * i + j /\ ((exists ftcn_strict_point_first_column. ftcn_strict_point_first_column + S (j) = (S s)) /\ ((r * i + j = (p) * q + t) /\ ((exists ftcn_strict_point_first_residue. ftcn_strict_point_first_residue + S (t) = (p)) /\ (((exists ff_h_ftpr_point_first. ff_h_ftpr_point_first + S (t) = S ((S (x)) * c)) /\ exists ff_q_ftpr_point_first. b = ff_q_ftpr_point_first * S ((S (x)) * c) + (t)))))))
  21. 0021specialize hgrid x
  22. 0022apply hgrid
  23. 0023exact hcollision_witness_witness_witness_left
  24. 0024cases hfirstpoint
  25. 0025cases hfirstpoint_witness
  26. 0026cases hfirstpoint_witness_witness
  27. 0027cases hfirstpoint_witness_witness_witness
  28. 0028cases hfirstpoint_witness_witness_witness_witness
  29. 0029cases hfirstpoint_witness_witness_witness_witness_right
  30. 0030cases hfirstpoint_witness_witness_witness_witness_right_right
  31. 0031cases hfirstpoint_witness_witness_witness_witness_right_right_right
  32. 0032have hsecondpoint : ∃ i. ∃ j. ∃ q. ∃ t. x1 = S s · i + j ∧ (Lt(j,S s) ∧ (r · i + j = p · q + t ∧ (Lt(t,p) ∧ BetaAt(b,c,x1,t))))
    Exact native replay linehave hsecondpoint : exists i j q t. ((x1) = (S s) * i + j /\ ((exists ftcn_strict_point_second_column. ftcn_strict_point_second_column + S (j) = (S s)) /\ ((r * i + j = (p) * q + t) /\ ((exists ftcn_strict_point_second_residue. ftcn_strict_point_second_residue + S (t) = (p)) /\ (((exists ff_h_ftpr_point_second. ff_h_ftpr_point_second + S (t) = S ((S (x1)) * c)) /\ exists ff_q_ftpr_point_second. b = ff_q_ftpr_point_second * S ((S (x1)) * c) + (t)))))))
  33. 0033specialize hgrid x1
  34. 0034apply hgrid
  35. 0035exact hcollision_witness_witness_witness_right_left
  36. 0036cases hsecondpoint
  37. 0037cases hsecondpoint_witness
  38. 0038cases hsecondpoint_witness_witness
  39. 0039cases hsecondpoint_witness_witness_witness
  40. 0040cases hsecondpoint_witness_witness_witness_witness
  41. 0041cases hsecondpoint_witness_witness_witness_witness_right
  42. 0042cases hsecondpoint_witness_witness_witness_witness_right_right
  43. 0043cases hsecondpoint_witness_witness_witness_witness_right_right_right
  44. 0044have hremainder : x6 = x10
  45. 0045specialize shared_beta_collision_remainders_equal b
  46. 0046specialize shared_beta_collision_remainders_equal c
  47. 0047specialize shared_beta_collision_remainders_equal x
  48. 0048specialize shared_beta_collision_remainders_equal x1
  49. 0049specialize shared_beta_collision_remainders_equal x6
  50. 0050specialize shared_beta_collision_remainders_equal x10
  51. 0051specialize shared_beta_collision_remainders_equal x2
  52. 0052apply shared_beta_collision_remainders_equal
  53. 0053exact hfirstpoint_witness_witness_witness_witness_right_right_right_right
  54. 0054exact hcollision_witness_witness_witness_right_right_right_left
  55. 0055exact hsecondpoint_witness_witness_witness_witness_right_right_right_right
  56. 0056exact hcollision_witness_witness_witness_right_right_right_right
  57. 0057rewrite hremainder at hfirstpoint_witness_witness_witness_witness_right_right_left
  58. 0058have haffine : ModEq(p,r · x3 + x4,r · x7 + x8)
    Exact native replay linehave haffine : exists ftcn_left_grid_affine ftcn_right_grid_affine. (r * x3 + x4) + (p) * ftcn_left_grid_affine = (r * x7 + x8) + (p) * ftcn_right_grid_affine
  59. 0059specialize equal_remainder_affine_values_balanced_congruent p
  60. 0060specialize equal_remainder_affine_values_balanced_congruent r
  61. 0061specialize equal_remainder_affine_values_balanced_congruent x3
  62. 0062specialize equal_remainder_affine_values_balanced_congruent x4
  63. 0063specialize equal_remainder_affine_values_balanced_congruent x5
  64. 0064specialize equal_remainder_affine_values_balanced_congruent x7
  65. 0065specialize equal_remainder_affine_values_balanced_congruent x8
  66. 0066specialize equal_remainder_affine_values_balanced_congruent x9
  67. 0067specialize equal_remainder_affine_values_balanced_congruent x10
  68. 0068apply equal_remainder_affine_values_balanced_congruent
  69. 0069exact hfirstpoint_witness_witness_witness_witness_right_right_left
  70. 0070exact hsecondpoint_witness_witness_witness_witness_right_right_left
  71. 0071rewrite hlength at hcollision_witness_witness_witness_left
  72. 0072rewrite hlength at hcollision_witness_witness_witness_right_left
  73. 0073specialize prime_floor_decoded_affine_collision_represents_prime p
  74. 0074specialize prime_floor_decoded_affine_collision_represents_prime s
  75. 0075specialize prime_floor_decoded_affine_collision_represents_prime r
  76. 0076specialize prime_floor_decoded_affine_collision_represents_prime x3
  77. 0077specialize prime_floor_decoded_affine_collision_represents_prime x4
  78. 0078specialize prime_floor_decoded_affine_collision_represents_prime x7
  79. 0079specialize prime_floor_decoded_affine_collision_represents_prime x8
  80. 0080specialize prime_floor_decoded_affine_collision_represents_prime x
  81. 0081specialize prime_floor_decoded_affine_collision_represents_prime x1
  82. 0082apply prime_floor_decoded_affine_collision_represents_prime
  83. 0083exact hprime
  84. 0084exact hfloor
  85. 0085exact hroot
  86. 0086exact hfirstpoint_witness_witness_witness_witness_left
  87. 0087exact hsecondpoint_witness_witness_witness_witness_left
  88. 0088exact hcollision_witness_witness_witness_left
  89. 0089exact hcollision_witness_witness_witness_right_left
  90. 0090exact hfirstpoint_witness_witness_witness_witness_right_left
  91. 0091exact hsecondpoint_witness_witness_witness_witness_right_left
  92. 0092exact hcollision_witness_witness_witness_right_right_left
  93. 0093exact haffine