TS000Z · theorem body

prime_floor_affine_residue_grid_collision

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

The actual affine prime-residue grid on all square-root points has explicit distinct flat indices with the same residue.

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

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 PD0004 Prime PD0013 BetaAt PD0051 FloorSqrt

In local proof propositions

PD0002 Lt PD0013 BetaAt
Exact expanded first-order statement
forall p s r l. l = S s * S s -> ((~(p = 1) /\ forall frm_prime_left_ftrg_prime frm_prime_right_ftrg_prime. p = frm_prime_left_ftrg_prime * frm_prime_right_ftrg_prime -> frm_prime_left_ftrg_prime = 1 \/ frm_prime_right_ftrg_prime = 1)) -> (((exists bcs_sqrt_lower_gap_ftrg_floor. bcs_sqrt_lower_gap_ftrg_floor + (s) * (s) = (p)) /\ exists bcs_sqrt_upper_gap_ftrg_floor. bcs_sqrt_upper_gap_ftrg_floor + S (p) = S (s) * S (s))) -> exists b c. ((forall ftrg_index_collision_grid. (exists ftrg_gap_collision_grid_index. ftrg_gap_collision_grid_index + S (ftrg_index_collision_grid) = (l)) -> exists ftrg_row_collision_grid ftrg_column_collision_grid ftrg_quotient_collision_grid ftrg_remainder_collision_grid. ((ftrg_index_collision_grid) = (S s) * ftrg_row_collision_grid + ftrg_column_collision_grid /\ ((exists ftrg_gap_collision_grid_column. ftrg_gap_collision_grid_column + S (ftrg_column_collision_grid) = (S s)) /\ ((r * ftrg_row_collision_grid + ftrg_column_collision_grid = (p) * ftrg_quotient_collision_grid + ftrg_remainder_collision_grid) /\ ((exists ftrg_gap_collision_grid_residue. ftrg_gap_collision_grid_residue + S (ftrg_remainder_collision_grid) = (p)) /\ (((exists ff_h_ftrg_collision_grid_entry. ff_h_ftrg_collision_grid_entry + S (ftrg_remainder_collision_grid) = S ((S (ftrg_index_collision_grid)) * c)) /\ exists ff_q_ftrg_collision_grid_entry. b = ff_q_ftrg_collision_grid_entry * S ((S (ftrg_index_collision_grid)) * c) + (ftrg_remainder_collision_grid)))))))) /\ (exists ftsp_first_ftrg_actual ftsp_second_ftrg_actual ftsp_value_ftrg_actual. ((exists ftsp_gap_ftrg_actual_first. ftsp_gap_ftrg_actual_first + S (ftsp_first_ftrg_actual) = l) /\ ((exists ftsp_gap_ftrg_actual_second. ftsp_gap_ftrg_actual_second + S (ftsp_second_ftrg_actual) = l) /\ (~(ftsp_first_ftrg_actual = ftsp_second_ftrg_actual) /\ ((((exists ff_h_ftsp_ftrg_actual_left. ff_h_ftsp_ftrg_actual_left + S (ftsp_value_ftrg_actual) = S ((S (ftsp_first_ftrg_actual)) * c)) /\ exists ff_q_ftsp_ftrg_actual_left. b = ff_q_ftsp_ftrg_actual_left * S ((S (ftsp_first_ftrg_actual)) * c) + (ftsp_value_ftrg_actual))) /\ (((exists ff_h_ftsp_ftrg_actual_right. ff_h_ftsp_ftrg_actual_right + S (ftsp_value_ftrg_actual) = S ((S (ftsp_second_ftrg_actual)) * c)) /\ exists ff_q_ftsp_ftrg_actual_right. b = ff_q_ftsp_ftrg_actual_right * S ((S (ftsp_second_ftrg_actual)) * c) + (ftsp_value_ftrg_actual)))))))))

Proof neighborhood

Direct theorem prerequisites

TS000Y prime_floor_affine_residue_grid_exists TS000X beta_affine_residue_grid_bounded TS000T floor_square_oversized_bounded_grid_collision

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

37 script commands · 7 reading checkpoints · 1 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)
prime floor affine residue grid existsbeta affine residue grid boundedfloor square oversized bounded grid collision
01Fix variables and assumptionsL1–7

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 l
  5. L5
    intro hlength
  6. L6
    intro hprime
  7. L7
    intro hfloor
02Establish hgridL8–15

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime floor affine residue grid exists.

  1. L8
    have hgrid : ∃ b. ∃ c. ∀ 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))))Definitions: Lt(x,l)Lt(z,S s)Lt(m,p)BetaAt(b,c,x,m)Original native command in the exact edition
  2. L9
    specialize prime_floor_affine_residue_grid_exists p
  3. L10
    specialize prime_floor_affine_residue_grid_exists s
  4. L11
    specialize prime_floor_affine_residue_grid_exists r
  5. L12
    specialize prime_floor_affine_residue_grid_exists l
  6. L13
    apply prime_floor_affine_residue_grid_exists
  7. L14
    exact hlength
  8. L15
    exact hprime
03Separate the logical casesL16–17

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

  1. L16
    cases hgrid
  2. L17
    cases hgrid_witness
04Construct an explicit witnessL18–19

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

  1. L18
    exists x
  2. L19
    exists x1
05Separate the logical casesL20–20

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

  1. L20
    split
06Use earlier factsL21–30

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

  1. L21
    exact hgrid_witness_witness
  2. L22
    specialize floor_square_oversized_bounded_grid_collision x
  3. L23
    specialize floor_square_oversized_bounded_grid_collision x1
  4. L24
    specialize floor_square_oversized_bounded_grid_collision l
  5. L25
    specialize floor_square_oversized_bounded_grid_collision p
  6. L26
    specialize floor_square_oversized_bounded_grid_collision s
  7. L27
    apply floor_square_oversized_bounded_grid_collision
  8. L28
    exact hlength
  9. L29
    exact hfloor
  10. L30
    specialize beta_affine_residue_grid_bounded p
07Use earlier factsL31–37

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

  1. L31
    specialize beta_affine_residue_grid_bounded (S s)
  2. L32
    specialize beta_affine_residue_grid_bounded r
  3. L33
    specialize beta_affine_residue_grid_bounded x
  4. L34
    specialize beta_affine_residue_grid_bounded x1
  5. L35
    specialize beta_affine_residue_grid_bounded l
  6. L36
    apply beta_affine_residue_grid_bounded
  7. L37
    exact hgrid_witness_witness

Library-wide reading audit

Original defined command ledger · 37 lines
  1. 0001intro p
  2. 0002intro s
  3. 0003intro r
  4. 0004intro l
  5. 0005intro hlength
  6. 0006intro hprime
  7. 0007intro hfloor
  8. 0008have hgrid : ∃ b. ∃ c. ∀ 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))))
    Exact native replay linehave hgrid : exists b c. (forall ftrg_index_square_grid. (exists ftrg_gap_square_grid_index. ftrg_gap_square_grid_index + S (ftrg_index_square_grid) = (l)) -> exists ftrg_row_square_grid ftrg_column_square_grid ftrg_quotient_square_grid ftrg_remainder_square_grid. ((ftrg_index_square_grid) = (S s) * ftrg_row_square_grid + ftrg_column_square_grid /\ ((exists ftrg_gap_square_grid_column. ftrg_gap_square_grid_column + S (ftrg_column_square_grid) = (S s)) /\ ((r * ftrg_row_square_grid + ftrg_column_square_grid = (p) * ftrg_quotient_square_grid + ftrg_remainder_square_grid) /\ ((exists ftrg_gap_square_grid_residue. ftrg_gap_square_grid_residue + S (ftrg_remainder_square_grid) = (p)) /\ (((exists ff_h_ftrg_square_grid_entry. ff_h_ftrg_square_grid_entry + S (ftrg_remainder_square_grid) = S ((S (ftrg_index_square_grid)) * c)) /\ exists ff_q_ftrg_square_grid_entry. b = ff_q_ftrg_square_grid_entry * S ((S (ftrg_index_square_grid)) * c) + (ftrg_remainder_square_grid))))))))
  9. 0009specialize prime_floor_affine_residue_grid_exists p
  10. 0010specialize prime_floor_affine_residue_grid_exists s
  11. 0011specialize prime_floor_affine_residue_grid_exists r
  12. 0012specialize prime_floor_affine_residue_grid_exists l
  13. 0013apply prime_floor_affine_residue_grid_exists
  14. 0014exact hlength
  15. 0015exact hprime
  16. 0016cases hgrid
  17. 0017cases hgrid_witness
  18. 0018exists x
  19. 0019exists x1
  20. 0020split
  21. 0021exact hgrid_witness_witness
  22. 0022specialize floor_square_oversized_bounded_grid_collision x
  23. 0023specialize floor_square_oversized_bounded_grid_collision x1
  24. 0024specialize floor_square_oversized_bounded_grid_collision l
  25. 0025specialize floor_square_oversized_bounded_grid_collision p
  26. 0026specialize floor_square_oversized_bounded_grid_collision s
  27. 0027apply floor_square_oversized_bounded_grid_collision
  28. 0028exact hlength
  29. 0029exact hfloor
  30. 0030specialize beta_affine_residue_grid_bounded p
  31. 0031specialize beta_affine_residue_grid_bounded (S s)
  32. 0032specialize beta_affine_residue_grid_bounded r
  33. 0033specialize beta_affine_residue_grid_bounded x
  34. 0034specialize beta_affine_residue_grid_bounded x1
  35. 0035specialize beta_affine_residue_grid_bounded l
  36. 0036apply beta_affine_residue_grid_bounded
  37. 0037exact hgrid_witness_witness