FS004E · theorem body

four_square_half_square_residue_prefix_injective

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

The beta-coded square residues of the complete inclusive odd-prime half range form an actually injective bounded prefix.

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. ∀ h. ∀ b. ∀ c. p = 2 · h + 1 → Prime(p) → (∀ x. Lt(x,S h) → ∃ y. ∃ z. x · x = p · y + z ∧ (Lt(z,p) ∧ BetaAt(b,c,x,z))) → InjectivePrefix(b,c,S h)

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 PD0025 InjectivePrefix

In local proof propositions

PD0002 Lt PD0008 ModEq PD0013 BetaAt
Exact expanded first-order statement
forall p h b c. p = 2 * h + 1 -> ((~(p = 1) /\ forall frm_prime_left_fsri_prime frm_prime_right_fsri_prime. p = frm_prime_left_fsri_prime * frm_prime_right_fsri_prime -> frm_prime_left_fsri_prime = 1 \/ frm_prime_right_fsri_prime = 1)) -> (forall fsri_index_prefix_injective_source. (exists fsri_gap_prefix_injective_source_index. fsri_gap_prefix_injective_source_index + S (fsri_index_prefix_injective_source) = (S h)) -> exists fsri_quotient_prefix_injective_source fsri_residue_prefix_injective_source. (fsri_index_prefix_injective_source * fsri_index_prefix_injective_source = (p) * fsri_quotient_prefix_injective_source + fsri_residue_prefix_injective_source /\ ((exists fsri_gap_prefix_injective_source_residue. fsri_gap_prefix_injective_source_residue + S (fsri_residue_prefix_injective_source) = (p)) /\ (((exists fsri_height_prefix_injective_source_entry. fsri_height_prefix_injective_source_entry + S (fsri_residue_prefix_injective_source) = S ((S (fsri_index_prefix_injective_source)) * (c))) /\ exists fsri_quotient_prefix_injective_source_entry. (b) = fsri_quotient_prefix_injective_source_entry * S ((S (fsri_index_prefix_injective_source)) * (c)) + (fsri_residue_prefix_injective_source)))))) -> (forall fp_i_fsri_prefix_injective_result fp_j_fsri_prefix_injective_result fp_value_fsri_prefix_injective_result. (exists fp_gap_fsri_prefix_injective_result_i. fp_gap_fsri_prefix_injective_result_i + S fp_i_fsri_prefix_injective_result = S h) -> (exists fp_gap_fsri_prefix_injective_result_j. fp_gap_fsri_prefix_injective_result_j + S fp_j_fsri_prefix_injective_result = S h) -> (((exists ff_h_fsri_prefix_injective_result_left. ff_h_fsri_prefix_injective_result_left + S (fp_value_fsri_prefix_injective_result) = S ((S (fp_i_fsri_prefix_injective_result)) * c)) /\ exists ff_q_fsri_prefix_injective_result_left. b = ff_q_fsri_prefix_injective_result_left * S ((S (fp_i_fsri_prefix_injective_result)) * c) + (fp_value_fsri_prefix_injective_result))) -> (((exists ff_h_fsri_prefix_injective_result_right. ff_h_fsri_prefix_injective_result_right + S (fp_value_fsri_prefix_injective_result) = S ((S (fp_j_fsri_prefix_injective_result)) * c)) /\ exists ff_q_fsri_prefix_injective_result_right. b = ff_q_fsri_prefix_injective_result_right * S ((S (fp_j_fsri_prefix_injective_result)) * c) + (fp_value_fsri_prefix_injective_result))) -> fp_i_fsri_prefix_injective_result = fp_j_fsri_prefix_injective_result)

Proof neighborhood

Direct theorem prerequisites

beta_at_unique · Stable closed le_of_succ_le_succ · Stable closed FS004D four_square_equal_square_remainders_are_congruent FS004A four_square_prime_half_square_residues_injective

Direct theorem dependents

FS000K four_square_odd_prime_half_coordinate_seed FS004K four_square_odd_prime_modular_seed

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

80 script commands · 12 reading checkpoints · 6 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 (2)
four square equal square remainders are congruentfour square prime half square residues injective
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro h
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro hodd
  6. L6
    intro hprime
  7. L7
    intro hprefix
  8. L8
    intro i
  9. L9
    intro j
  10. L10
    intro v
02Fix variables and assumptionsL11–14

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

  1. L11
    intro hi
  2. L12
    intro hj
  3. L13
    intro hleft
  4. L14
    intro hright
03Establish hfirstL15–18

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

  1. L15
    have hfirst : ∃ q. ∃ r. i · i = p · q + r ∧ (Lt(r,p) ∧ BetaAt(b,c,i,r))Definitions: Lt(r,p)BetaAt(b,c,i,r)Original native command in the exact edition
  2. L16
    specialize hprefix i
  3. L17
    apply hprefix
  4. L18
    exact hi
04Separate the logical casesL19–22

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

  1. L19
    cases hfirst
  2. L20
    cases hfirst_witness
  3. L21
    cases hfirst_witness_witness
  4. L22
    cases hfirst_witness_witness_right
05Establish hsecondL23–26

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

  1. L23
    have hsecond : ∃ q. ∃ r. j · j = p · q + r ∧ (Lt(r,p) ∧ BetaAt(b,c,j,r))Definitions: Lt(r,p)BetaAt(b,c,j,r)Original native command in the exact edition
  2. L24
    specialize hprefix j
  3. L25
    apply hprefix
  4. L26
    exact hj
06Separate the logical casesL27–30

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

  1. L27
    cases hsecond
  2. L28
    cases hsecond_witness
  3. L29
    cases hsecond_witness_witness
  4. L30
    cases hsecond_witness_witness_right
07Establish hfirst_valueL31–39

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

  1. L31
    have hfirst_value : x1 = v
  2. L32
    specialize beta_at_unique b
  3. L33
    specialize beta_at_unique c
  4. L34
    specialize beta_at_unique i
  5. L35
    specialize beta_at_unique x1
  6. L36
    specialize beta_at_unique v
  7. L37
    apply beta_at_unique
  8. L38
    exact hfirst_witness_witness_right_right
  9. L39
    exact hleft
08Establish hsecond_valueL40–48

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

  1. L40
    have hsecond_value : x3 = v
  2. L41
    specialize beta_at_unique b
  3. L42
    specialize beta_at_unique c
  4. L43
    specialize beta_at_unique j
  5. L44
    specialize beta_at_unique x3
  6. L45
    specialize beta_at_unique v
  7. L46
    apply beta_at_unique
  8. L47
    exact hsecond_witness_witness_right_right
  9. L48
    exact hright
09Establish hsameL49–54

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

  1. L49
    have hsame : x3 = x1
  2. L50
    trans v
  3. L51
    exact hsecond_value
  4. L52
    symm
  5. L53
    exact hfirst_value
  6. L54
    rewrite hsame at hsecond_witness_witness_left
10Establish hmodL55–64

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square equal square remainders are congruent.

  1. L55
    have hmod : ModEq(p,i · i,j · j)Definitions: ModEq(p,i · i,j · j)Original native command in the exact edition
  2. L56
    specialize four_square_equal_square_remainders_are_congruent p
  3. L57
    specialize four_square_equal_square_remainders_are_congruent i
  4. L58
    specialize four_square_equal_square_remainders_are_congruent j
  5. L59
    specialize four_square_equal_square_remainders_are_congruent x
  6. L60
    specialize four_square_equal_square_remainders_are_congruent x2
  7. L61
    specialize four_square_equal_square_remainders_are_congruent x1
  8. L62
    apply four_square_equal_square_remainders_are_congruent
  9. L63
    exact hfirst_witness_witness_left
  10. L64
    exact hsecond_witness_witness_left
11Use earlier factsL65–74

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

  1. L65
    specialize four_square_prime_half_square_residues_injective p
  2. L66
    specialize four_square_prime_half_square_residues_injective h
  3. L67
    specialize four_square_prime_half_square_residues_injective i
  4. L68
    specialize four_square_prime_half_square_residues_injective j
  5. L69
    apply four_square_prime_half_square_residues_injective
  6. L70
    exact hodd
  7. L71
    exact hprime
  8. L72
    specialize le_of_succ_le_succ i
  9. L73
    specialize le_of_succ_le_succ h
  10. L74
    apply le_of_succ_le_succ
12Use earlier factsL75–80

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

  1. L75
    exact hi
  2. L76
    specialize le_of_succ_le_succ j
  3. L77
    specialize le_of_succ_le_succ h
  4. L78
    apply le_of_succ_le_succ
  5. L79
    exact hj
  6. L80
    exact hmod

Library-wide reading audit

Original defined command ledger · 80 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro b
  4. 0004intro c
  5. 0005intro hodd
  6. 0006intro hprime
  7. 0007intro hprefix
  8. 0008intro i
  9. 0009intro j
  10. 0010intro v
  11. 0011intro hi
  12. 0012intro hj
  13. 0013intro hleft
  14. 0014intro hright
  15. 0015have hfirst : ∃ q. ∃ r. i · i = p · q + r ∧ (Lt(r,p) ∧ BetaAt(b,c,i,r))
    Exact native replay linehave hfirst : exists q r. (i * i = p * q + r /\ ((exists fsri_gap_prefix_first_bound. fsri_gap_prefix_first_bound + S (r) = (p)) /\ (((exists fsri_height_prefix_first_entry. fsri_height_prefix_first_entry + S (r) = S ((S (i)) * (c))) /\ exists fsri_quotient_prefix_first_entry. (b) = fsri_quotient_prefix_first_entry * S ((S (i)) * (c)) + (r)))))
  16. 0016specialize hprefix i
  17. 0017apply hprefix
  18. 0018exact hi
  19. 0019cases hfirst
  20. 0020cases hfirst_witness
  21. 0021cases hfirst_witness_witness
  22. 0022cases hfirst_witness_witness_right
  23. 0023have hsecond : ∃ q. ∃ r. j · j = p · q + r ∧ (Lt(r,p) ∧ BetaAt(b,c,j,r))
    Exact native replay linehave hsecond : exists q r. (j * j = p * q + r /\ ((exists fsri_gap_prefix_second_bound. fsri_gap_prefix_second_bound + S (r) = (p)) /\ (((exists fsri_height_prefix_second_entry. fsri_height_prefix_second_entry + S (r) = S ((S (j)) * (c))) /\ exists fsri_quotient_prefix_second_entry. (b) = fsri_quotient_prefix_second_entry * S ((S (j)) * (c)) + (r)))))
  24. 0024specialize hprefix j
  25. 0025apply hprefix
  26. 0026exact hj
  27. 0027cases hsecond
  28. 0028cases hsecond_witness
  29. 0029cases hsecond_witness_witness
  30. 0030cases hsecond_witness_witness_right
  31. 0031have hfirst_value : x1 = v
  32. 0032specialize beta_at_unique b
  33. 0033specialize beta_at_unique c
  34. 0034specialize beta_at_unique i
  35. 0035specialize beta_at_unique x1
  36. 0036specialize beta_at_unique v
  37. 0037apply beta_at_unique
  38. 0038exact hfirst_witness_witness_right_right
  39. 0039exact hleft
  40. 0040have hsecond_value : x3 = v
  41. 0041specialize beta_at_unique b
  42. 0042specialize beta_at_unique c
  43. 0043specialize beta_at_unique j
  44. 0044specialize beta_at_unique x3
  45. 0045specialize beta_at_unique v
  46. 0046apply beta_at_unique
  47. 0047exact hsecond_witness_witness_right_right
  48. 0048exact hright
  49. 0049have hsame : x3 = x1
  50. 0050trans v
  51. 0051exact hsecond_value
  52. 0052symm
  53. 0053exact hfirst_value
  54. 0054rewrite hsame at hsecond_witness_witness_left
  55. 0055have hmod : ModEq(p,i · i,j · j)
    Exact native replay linehave hmod : exists fsri_left_prefix_equal_mod fsri_right_prefix_equal_mod. (i * i) + (p) * fsri_left_prefix_equal_mod = (j * j) + (p) * fsri_right_prefix_equal_mod
  56. 0056specialize four_square_equal_square_remainders_are_congruent p
  57. 0057specialize four_square_equal_square_remainders_are_congruent i
  58. 0058specialize four_square_equal_square_remainders_are_congruent j
  59. 0059specialize four_square_equal_square_remainders_are_congruent x
  60. 0060specialize four_square_equal_square_remainders_are_congruent x2
  61. 0061specialize four_square_equal_square_remainders_are_congruent x1
  62. 0062apply four_square_equal_square_remainders_are_congruent
  63. 0063exact hfirst_witness_witness_left
  64. 0064exact hsecond_witness_witness_left
  65. 0065specialize four_square_prime_half_square_residues_injective p
  66. 0066specialize four_square_prime_half_square_residues_injective h
  67. 0067specialize four_square_prime_half_square_residues_injective i
  68. 0068specialize four_square_prime_half_square_residues_injective j
  69. 0069apply four_square_prime_half_square_residues_injective
  70. 0070exact hodd
  71. 0071exact hprime
  72. 0072specialize le_of_succ_le_succ i
  73. 0073specialize le_of_succ_le_succ h
  74. 0074apply le_of_succ_le_succ
  75. 0075exact hi
  76. 0076specialize le_of_succ_le_succ j
  77. 0077specialize le_of_succ_le_succ h
  78. 0078apply le_of_succ_le_succ
  79. 0079exact hj
  80. 0080exact hmod