FS000K

four_square_odd_prime_half_coordinate_seed

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

The actual odd-prime residue intersection supplies both square coordinates in the witnessed interval 0≤a,b≤h.

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.

Exact expanded first-order arithmetic statement

forall p h. p = 2 * h + 1 -> ((~(p = 1) /\ forall frm_prime_left_fsbs_prime frm_prime_right_fsbs_prime. p = frm_prime_left_fsbs_prime * frm_prime_right_fsbs_prime -> frm_prime_left_fsbs_prime = 1 \/ frm_prime_right_fsbs_prime = 1)) -> exists a b k. ((a * a + b * b + 1 = p * k) /\ ((exists fsbs_le_gap_first_half. fsbs_le_gap_first_half + (a) = (h)) /\ (exists fsbs_le_gap_second_half. fsbs_le_gap_second_half + (b) = (h))))

Constructive proof overview

Generated structural guide

The actual odd-prime residue intersection supplies both square coordinates in the witnessed interval 0≤a,b≤h.

The unchanged tactic script uses 12 declared prerequisites and contains 143 exact native proof lines.

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Proof neighborhood

Direct dependencies

prime_nonzero Stable theorem; checked-use authorized FS004B four_square_square_residue_prefix_exists FS004C four_square_square_residue_prefix_bounded FS004E four_square_half_square_residue_prefix_injective FS004F four_square_bounded_complement_prefix_exists FS004H four_square_complement_prefix_bounded FS004I four_square_complement_prefix_preserves_injectivity FS0044 four_square_two_half_ranges_overflow_odd FS0017 four_square_cross_intersection beta_at_unique Stable theorem; checked-use authorized FS004J four_square_complementary_remainders_form_multiple le_of_succ_le_succ Stable theorem; checked-use authorized

Direct dependents

FS000N four_square_odd_prime_bounded_modular_seed

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

143 script commands · 26 reading checkpoints · 12 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.

Named ingredients (9)
four square square residue prefix existsfour square square residue prefix boundedfour square half square residue prefix injectivefour square bounded complement prefix existsfour square complement prefix boundedfour square complement prefix preserves injectivityfour square two half ranges overflow oddfour square cross intersectionfour square complementary remainders form multiple

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–4

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

  1. L1
    intro p
  2. L2
    intro h
  3. L3
    intro hodd
  4. L4
    intro hprime
02Establish hsquaresL5–13

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square square residue prefix exists.

  1. L5
    have hsquares : ∃ b. ∃ c. ∀ x. Lt(x,S h) → ∃ y. ∃ z. x · x = p · y + z ∧ (Lt(z,p) ∧ BetaAt(b,c,x,z))Definitions: LtBetaAt
  2. L6
    specialize four_square_square_residue_prefix_exists p
  3. L7
    specialize four_square_square_residue_prefix_exists (S h)
  4. L8
    apply four_square_square_residue_prefix_exists
  5. L9
    intro hpzero
  6. L10
    specialize prime_nonzero p
  7. L11
    apply prime_nonzero
  8. L12
    exact hprime
  9. L13
    exact hpzero
03Separate the logical casesL14–15

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

  1. L14
    cases hsquares
  2. L15
    cases hsquares_witness
04Establish hboundedL16–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square square residue prefix bounded.

  1. L16
    have hbounded : ∀ fscp_index_seed_square_bounded. Lt(fscp_index_seed_square_bounded,S h) → ∃ y. BetaAt(x,x1,fscp_index_seed_square_bounded,y) ∧ Lt(y,p)Definitions: LtBetaAt
  2. L17
    specialize four_square_square_residue_prefix_bounded p
  3. L18
    specialize four_square_square_residue_prefix_bounded x
  4. L19
    specialize four_square_square_residue_prefix_bounded x1
  5. L20
    specialize four_square_square_residue_prefix_bounded (S h)
  6. L21
    apply four_square_square_residue_prefix_bounded
  7. L22
    exact hsquares_witness_witness
05Establish hinjectiveL23–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square half square residue prefix injective.

  1. L23
    have hinjective : InjectivePrefix(x,x1,S h)Definitions: InjectivePrefix
  2. L24
    specialize four_square_half_square_residue_prefix_injective p
  3. L25
    specialize four_square_half_square_residue_prefix_injective h
  4. L26
    specialize four_square_half_square_residue_prefix_injective x
  5. L27
    specialize four_square_half_square_residue_prefix_injective x1
  6. L28
    apply four_square_half_square_residue_prefix_injective
  7. L29
    exact hodd
  8. L30
    exact hprime
  9. L31
    exact hsquares_witness_witness
06Establish hcomplementL32–38

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square bounded complement prefix exists.

  1. L32
    have hcomplement : ∃ z. ∃ d. ∀ y. ∀ n. ∀ m. Lt(y,S h) → BetaAt(x,x1,y,n) → BetaAt(z,d,y,m) → m + S n = pDefinitions: LtBetaAt
  2. L33
    specialize four_square_bounded_complement_prefix_exists p
  3. L34
    specialize four_square_bounded_complement_prefix_exists x
  4. L35
    specialize four_square_bounded_complement_prefix_exists x1
  5. L36
    specialize four_square_bounded_complement_prefix_exists (S h)
  6. L37
    apply four_square_bounded_complement_prefix_exists
  7. L38
    exact hbounded
07Separate the logical casesL39–40

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

  1. L39
    cases hcomplement
  2. L40
    cases hcomplement_witness
08Establish hcomplement_boundedL41–50

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square complement prefix bounded.

  1. L41
    have hcomplement_bounded : ∀ fscp_index_seed_complement_bounded. Lt(fscp_index_seed_complement_bounded,S h) → ∃ x. BetaAt(x2,x3,fscp_index_seed_complement_bounded,x) ∧ Lt(x,p)Definitions: LtBetaAt
  2. L42
    specialize four_square_complement_prefix_bounded p
  3. L43
    specialize four_square_complement_prefix_bounded x
  4. L44
    specialize four_square_complement_prefix_bounded x1
  5. L45
    specialize four_square_complement_prefix_bounded x2
  6. L46
    specialize four_square_complement_prefix_bounded x3
  7. L47
    specialize four_square_complement_prefix_bounded (S h)
  8. L48
    apply four_square_complement_prefix_bounded
  9. L49
    exact hbounded
  10. L50
    exact hcomplement_witness_witness
09Establish hcomplement_injectiveL51–60

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square complement prefix preserves injectivity.

  1. L51
    have hcomplement_injective : InjectivePrefix(x2,x3,S h)Definitions: InjectivePrefix
  2. L52
    specialize four_square_complement_prefix_preserves_injectivity p
  3. L53
    specialize four_square_complement_prefix_preserves_injectivity x
  4. L54
    specialize four_square_complement_prefix_preserves_injectivity x1
  5. L55
    specialize four_square_complement_prefix_preserves_injectivity x2
  6. L56
    specialize four_square_complement_prefix_preserves_injectivity x3
  7. L57
    specialize four_square_complement_prefix_preserves_injectivity (S h)
  8. L58
    apply four_square_complement_prefix_preserves_injectivity
  9. L59
    exact hinjective
  10. L60
    exact hcomplement_witness_witness
10Establish hcrossL61–70

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square cross intersection.

  1. L61
    have hcross : ∃ fscp_left_seed_cross. ∃ fscp_right_seed_cross. ∃ fscp_value_seed_cross. Lt(fscp_left_seed_cross,S h) ∧ (Lt(fscp_right_seed_cross,S h) ∧ (BetaAt(x,x1,fscp_left_seed_cross,fscp_value_seed_cross) ∧ BetaAt(x2,x3,fscp_right_seed_cross,fscp_value_seed_cross)))Definitions: LtBetaAt
  2. L62
    specialize four_square_cross_intersection x
  3. L63
    specialize four_square_cross_intersection x1
  4. L64
    specialize four_square_cross_intersection x2
  5. L65
    specialize four_square_cross_intersection x3
  6. L66
    specialize four_square_cross_intersection (S h)
  7. L67
    specialize four_square_cross_intersection p
  8. L68
    apply four_square_cross_intersection
  9. L69
    exact hbounded
  10. L70
    exact hcomplement_bounded
11Use earlier factsL71–76

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

  1. L71
    exact hinjective
  2. L72
    exact hcomplement_injective
  3. L73
    specialize four_square_two_half_ranges_overflow_odd p
  4. L74
    specialize four_square_two_half_ranges_overflow_odd h
  5. L75
    apply four_square_two_half_ranges_overflow_odd
  6. L76
    exact hodd
12Separate the logical casesL77–82

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

  1. L77
    cases hcross
  2. L78
    cases hcross_witness
  3. L79
    cases hcross_witness_witness
  4. L80
    cases hcross_witness_witness_witness
  5. L81
    cases hcross_witness_witness_witness_right
  6. L82
    cases hcross_witness_witness_witness_right_right
13Establish hfirstL83–86

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

  1. L83
    have hfirst : exists q r. (x4 * x4 = p * q + r /\ ((exists fsri_gap_seed_first_bound. fsri_gap_seed_first_bound + S (r) = (p)) /\ (((exists fsri_height_seed_first_entry. fsri_height_seed_first_entry + S (r) = S ((S (x4)) * (x1))) /\ exists fsri_quotient_seed_first_entry. (x) = fsri_quotient_seed_first_entry * S ((S (x4)) * (x1)) + (r)))))
  2. L84
    specialize hsquares_witness_witness x4
  3. L85
    apply hsquares_witness_witness
  4. L86
    exact hcross_witness_witness_witness_left
14Separate the logical casesL87–90

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

  1. L87
    cases hfirst
  2. L88
    cases hfirst_witness
  3. L89
    cases hfirst_witness_witness
  4. L90
    cases hfirst_witness_witness_right
15Establish hsecondL91–94

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

  1. L91
    have hsecond : exists q r. (x5 * x5 = p * q + r /\ ((exists fsri_gap_seed_second_bound. fsri_gap_seed_second_bound + S (r) = (p)) /\ (((exists fsri_height_seed_second_entry. fsri_height_seed_second_entry + S (r) = S ((S (x5)) * (x1))) /\ exists fsri_quotient_seed_second_entry. (x) = fsri_quotient_seed_second_entry * S ((S (x5)) * (x1)) + (r)))))
  2. L92
    specialize hsquares_witness_witness x5
  3. L93
    apply hsquares_witness_witness
  4. L94
    exact hcross_witness_witness_witness_right_left
16Separate the logical casesL95–98

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

  1. L95
    cases hsecond
  2. L96
    cases hsecond_witness
  3. L97
    cases hsecond_witness_witness
  4. L98
    cases hsecond_witness_witness_right
17Establish hfirst_valueL99–108

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

  1. L99
    have hfirst_value : x8 = x6
  2. L100
    specialize beta_at_unique x
  3. L101
    specialize beta_at_unique x1
  4. L102
    specialize beta_at_unique x4
  5. L103
    specialize beta_at_unique x8
  6. L104
    specialize beta_at_unique x6
  7. L105
    apply beta_at_unique
  8. L106
    exact hfirst_witness_witness_right_right
  9. L107
    exact hcross_witness_witness_witness_right_right_left
  10. L108
    rewrite hfirst_value at hfirst_witness_witness_left
18Establish hgapL109–116

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

  1. L109
    have hgap : x6 + S x10 = p
  2. L110
    specialize hcomplement_witness_witness x5
  3. L111
    specialize hcomplement_witness_witness x10
  4. L112
    specialize hcomplement_witness_witness x6
  5. L113
    apply hcomplement_witness_witness
  6. L114
    exact hcross_witness_witness_witness_right_left
  7. L115
    exact hsecond_witness_witness_right_right
  8. L116
    exact hcross_witness_witness_witness_right_right_right
19Establish hmultipleL117–126

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square complementary remainders form multiple.

  1. L117
    have hmultiple : exists fsri_factor_seed_multiple. (x4 * x4 + x5 * x5 + 1) = (p) * fsri_factor_seed_multiple
  2. L118
    specialize four_square_complementary_remainders_form_multiple p
  3. L119
    specialize four_square_complementary_remainders_form_multiple (x4 * x4)
  4. L120
    specialize four_square_complementary_remainders_form_multiple (x5 * x5)
  5. L121
    specialize four_square_complementary_remainders_form_multiple x7
  6. L122
    specialize four_square_complementary_remainders_form_multiple x6
  7. L123
    specialize four_square_complementary_remainders_form_multiple x9
  8. L124
    specialize four_square_complementary_remainders_form_multiple x10
  9. L125
    apply four_square_complementary_remainders_form_multiple
  10. L126
    exact hfirst_witness_witness_left
20Use earlier factsL127–128

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

  1. L127
    exact hsecond_witness_witness_left
  2. L128
    exact hgap
21Separate the logical casesL129–129

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

  1. L129
    cases hmultiple
22Construct an explicit witnessL130–132

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

  1. L130
    exists x4
  2. L131
    exists x5
  3. L132
    exists x11
23Separate the logical casesL133–133

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

  1. L133
    split
24Use earlier factsL134–134

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

  1. L134
    exact hmultiple_witness
25Separate the logical casesL135–135

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

  1. L135
    split
26Use earlier factsL136–143

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

  1. L136
    specialize le_of_succ_le_succ x4
  2. L137
    specialize le_of_succ_le_succ h
  3. L138
    apply le_of_succ_le_succ
  4. L139
    exact hcross_witness_witness_witness_left
  5. L140
    specialize le_of_succ_le_succ x5
  6. L141
    specialize le_of_succ_le_succ h
  7. L142
    apply le_of_succ_le_succ
  8. L143
    exact hcross_witness_witness_witness_right_left

Library-wide reading audit

Original exact command ledger · 143 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro hodd
  4. 0004intro hprime
  5. 0005have hsquares : exists b c. (forall fsri_index_seed_squares. (exists fsri_gap_seed_squares_index. fsri_gap_seed_squares_index + S (fsri_index_seed_squares) = (S h)) -> exists fsri_quotient_seed_squares fsri_residue_seed_squares. (fsri_index_seed_squares * fsri_index_seed_squares = (p) * fsri_quotient_seed_squares + fsri_residue_seed_squares /\ ((exists fsri_gap_seed_squares_residue. fsri_gap_seed_squares_residue + S (fsri_residue_seed_squares) = (p)) /\ (((exists fsri_height_seed_squares_entry. fsri_height_seed_squares_entry + S (fsri_residue_seed_squares) = S ((S (fsri_index_seed_squares)) * (c))) /\ exists fsri_quotient_seed_squares_entry. (b) = fsri_quotient_seed_squares_entry * S ((S (fsri_index_seed_squares)) * (c)) + (fsri_residue_seed_squares))))))
  6. 0006specialize four_square_square_residue_prefix_exists p
  7. 0007specialize four_square_square_residue_prefix_exists (S h)
  8. 0008apply four_square_square_residue_prefix_exists
  9. 0009intro hpzero
  10. 0010specialize prime_nonzero p
  11. 0011apply prime_nonzero
  12. 0012exact hprime
  13. 0013exact hpzero
  14. 0014cases hsquares
  15. 0015cases hsquares_witness
  16. 0016have hbounded : forall fscp_index_seed_square_bounded. (exists fscp_gap_seed_square_bounded_index. fscp_gap_seed_square_bounded_index + S (fscp_index_seed_square_bounded) = (S h)) -> exists fscp_value_seed_square_bounded. ((((exists ff_h_fscp_seed_square_bounded_entry. ff_h_fscp_seed_square_bounded_entry + S (fscp_value_seed_square_bounded) = S ((S (fscp_index_seed_square_bounded)) * x1)) /\ exists ff_q_fscp_seed_square_bounded_entry. x = ff_q_fscp_seed_square_bounded_entry * S ((S (fscp_index_seed_square_bounded)) * x1) + (fscp_value_seed_square_bounded))) /\ (exists fscp_gap_seed_square_bounded_value. fscp_gap_seed_square_bounded_value + S (fscp_value_seed_square_bounded) = (p)))
  17. 0017specialize four_square_square_residue_prefix_bounded p
  18. 0018specialize four_square_square_residue_prefix_bounded x
  19. 0019specialize four_square_square_residue_prefix_bounded x1
  20. 0020specialize four_square_square_residue_prefix_bounded (S h)
  21. 0021apply four_square_square_residue_prefix_bounded
  22. 0022exact hsquares_witness_witness
  23. 0023have hinjective : forall fp_i_fsri_seed_square_injective fp_j_fsri_seed_square_injective fp_value_fsri_seed_square_injective. (exists fp_gap_fsri_seed_square_injective_i. fp_gap_fsri_seed_square_injective_i + S fp_i_fsri_seed_square_injective = S h) -> (exists fp_gap_fsri_seed_square_injective_j. fp_gap_fsri_seed_square_injective_j + S fp_j_fsri_seed_square_injective = S h) -> (((exists ff_h_fsri_seed_square_injective_left. ff_h_fsri_seed_square_injective_left + S (fp_value_fsri_seed_square_injective) = S ((S (fp_i_fsri_seed_square_injective)) * x1)) /\ exists ff_q_fsri_seed_square_injective_left. x = ff_q_fsri_seed_square_injective_left * S ((S (fp_i_fsri_seed_square_injective)) * x1) + (fp_value_fsri_seed_square_injective))) -> (((exists ff_h_fsri_seed_square_injective_right. ff_h_fsri_seed_square_injective_right + S (fp_value_fsri_seed_square_injective) = S ((S (fp_j_fsri_seed_square_injective)) * x1)) /\ exists ff_q_fsri_seed_square_injective_right. x = ff_q_fsri_seed_square_injective_right * S ((S (fp_j_fsri_seed_square_injective)) * x1) + (fp_value_fsri_seed_square_injective))) -> fp_i_fsri_seed_square_injective = fp_j_fsri_seed_square_injective
  24. 0024specialize four_square_half_square_residue_prefix_injective p
  25. 0025specialize four_square_half_square_residue_prefix_injective h
  26. 0026specialize four_square_half_square_residue_prefix_injective x
  27. 0027specialize four_square_half_square_residue_prefix_injective x1
  28. 0028apply four_square_half_square_residue_prefix_injective
  29. 0029exact hodd
  30. 0030exact hprime
  31. 0031exact hsquares_witness_witness
  32. 0032have hcomplement : exists z d. (forall fsri_complement_index_seed_complement fsri_complement_source_seed_complement fsri_complement_target_seed_complement. (exists fsri_gap_seed_complement_index. fsri_gap_seed_complement_index + S (fsri_complement_index_seed_complement) = (S h)) -> (((exists fsri_height_seed_complement_source. fsri_height_seed_complement_source + S (fsri_complement_source_seed_complement) = S ((S (fsri_complement_index_seed_complement)) * (x1))) /\ exists fsri_quotient_seed_complement_source. (x) = fsri_quotient_seed_complement_source * S ((S (fsri_complement_index_seed_complement)) * (x1)) + (fsri_complement_source_seed_complement))) -> (((exists fsri_height_seed_complement_target. fsri_height_seed_complement_target + S (fsri_complement_target_seed_complement) = S ((S (fsri_complement_index_seed_complement)) * (d))) /\ exists fsri_quotient_seed_complement_target. (z) = fsri_quotient_seed_complement_target * S ((S (fsri_complement_index_seed_complement)) * (d)) + (fsri_complement_target_seed_complement))) -> fsri_complement_target_seed_complement + S fsri_complement_source_seed_complement = (p))
  33. 0033specialize four_square_bounded_complement_prefix_exists p
  34. 0034specialize four_square_bounded_complement_prefix_exists x
  35. 0035specialize four_square_bounded_complement_prefix_exists x1
  36. 0036specialize four_square_bounded_complement_prefix_exists (S h)
  37. 0037apply four_square_bounded_complement_prefix_exists
  38. 0038exact hbounded
  39. 0039cases hcomplement
  40. 0040cases hcomplement_witness
  41. 0041have hcomplement_bounded : forall fscp_index_seed_complement_bounded. (exists fscp_gap_seed_complement_bounded_index. fscp_gap_seed_complement_bounded_index + S (fscp_index_seed_complement_bounded) = (S h)) -> exists fscp_value_seed_complement_bounded. ((((exists ff_h_fscp_seed_complement_bounded_entry. ff_h_fscp_seed_complement_bounded_entry + S (fscp_value_seed_complement_bounded) = S ((S (fscp_index_seed_complement_bounded)) * x3)) /\ exists ff_q_fscp_seed_complement_bounded_entry. x2 = ff_q_fscp_seed_complement_bounded_entry * S ((S (fscp_index_seed_complement_bounded)) * x3) + (fscp_value_seed_complement_bounded))) /\ (exists fscp_gap_seed_complement_bounded_value. fscp_gap_seed_complement_bounded_value + S (fscp_value_seed_complement_bounded) = (p)))
  42. 0042specialize four_square_complement_prefix_bounded p
  43. 0043specialize four_square_complement_prefix_bounded x
  44. 0044specialize four_square_complement_prefix_bounded x1
  45. 0045specialize four_square_complement_prefix_bounded x2
  46. 0046specialize four_square_complement_prefix_bounded x3
  47. 0047specialize four_square_complement_prefix_bounded (S h)
  48. 0048apply four_square_complement_prefix_bounded
  49. 0049exact hbounded
  50. 0050exact hcomplement_witness_witness
  51. 0051have hcomplement_injective : forall fp_i_fsri_seed_complement_injective fp_j_fsri_seed_complement_injective fp_value_fsri_seed_complement_injective. (exists fp_gap_fsri_seed_complement_injective_i. fp_gap_fsri_seed_complement_injective_i + S fp_i_fsri_seed_complement_injective = S h) -> (exists fp_gap_fsri_seed_complement_injective_j. fp_gap_fsri_seed_complement_injective_j + S fp_j_fsri_seed_complement_injective = S h) -> (((exists ff_h_fsri_seed_complement_injective_left. ff_h_fsri_seed_complement_injective_left + S (fp_value_fsri_seed_complement_injective) = S ((S (fp_i_fsri_seed_complement_injective)) * x3)) /\ exists ff_q_fsri_seed_complement_injective_left. x2 = ff_q_fsri_seed_complement_injective_left * S ((S (fp_i_fsri_seed_complement_injective)) * x3) + (fp_value_fsri_seed_complement_injective))) -> (((exists ff_h_fsri_seed_complement_injective_right. ff_h_fsri_seed_complement_injective_right + S (fp_value_fsri_seed_complement_injective) = S ((S (fp_j_fsri_seed_complement_injective)) * x3)) /\ exists ff_q_fsri_seed_complement_injective_right. x2 = ff_q_fsri_seed_complement_injective_right * S ((S (fp_j_fsri_seed_complement_injective)) * x3) + (fp_value_fsri_seed_complement_injective))) -> fp_i_fsri_seed_complement_injective = fp_j_fsri_seed_complement_injective
  52. 0052specialize four_square_complement_prefix_preserves_injectivity p
  53. 0053specialize four_square_complement_prefix_preserves_injectivity x
  54. 0054specialize four_square_complement_prefix_preserves_injectivity x1
  55. 0055specialize four_square_complement_prefix_preserves_injectivity x2
  56. 0056specialize four_square_complement_prefix_preserves_injectivity x3
  57. 0057specialize four_square_complement_prefix_preserves_injectivity (S h)
  58. 0058apply four_square_complement_prefix_preserves_injectivity
  59. 0059exact hinjective
  60. 0060exact hcomplement_witness_witness
  61. 0061have hcross : exists fscp_left_seed_cross fscp_right_seed_cross fscp_value_seed_cross. ((exists fscp_gap_seed_cross_left_bound. fscp_gap_seed_cross_left_bound + S (fscp_left_seed_cross) = (S h)) /\ ((exists fscp_gap_seed_cross_right_bound. fscp_gap_seed_cross_right_bound + S (fscp_right_seed_cross) = (S h)) /\ ((((exists ff_h_fscp_seed_cross_left. ff_h_fscp_seed_cross_left + S (fscp_value_seed_cross) = S ((S (fscp_left_seed_cross)) * x1)) /\ exists ff_q_fscp_seed_cross_left. x = ff_q_fscp_seed_cross_left * S ((S (fscp_left_seed_cross)) * x1) + (fscp_value_seed_cross))) /\ (((exists ff_h_fscp_seed_cross_right. ff_h_fscp_seed_cross_right + S (fscp_value_seed_cross) = S ((S (fscp_right_seed_cross)) * x3)) /\ exists ff_q_fscp_seed_cross_right. x2 = ff_q_fscp_seed_cross_right * S ((S (fscp_right_seed_cross)) * x3) + (fscp_value_seed_cross))))))
  62. 0062specialize four_square_cross_intersection x
  63. 0063specialize four_square_cross_intersection x1
  64. 0064specialize four_square_cross_intersection x2
  65. 0065specialize four_square_cross_intersection x3
  66. 0066specialize four_square_cross_intersection (S h)
  67. 0067specialize four_square_cross_intersection p
  68. 0068apply four_square_cross_intersection
  69. 0069exact hbounded
  70. 0070exact hcomplement_bounded
  71. 0071exact hinjective
  72. 0072exact hcomplement_injective
  73. 0073specialize four_square_two_half_ranges_overflow_odd p
  74. 0074specialize four_square_two_half_ranges_overflow_odd h
  75. 0075apply four_square_two_half_ranges_overflow_odd
  76. 0076exact hodd
  77. 0077cases hcross
  78. 0078cases hcross_witness
  79. 0079cases hcross_witness_witness
  80. 0080cases hcross_witness_witness_witness
  81. 0081cases hcross_witness_witness_witness_right
  82. 0082cases hcross_witness_witness_witness_right_right
  83. 0083have hfirst : exists q r. (x4 * x4 = p * q + r /\ ((exists fsri_gap_seed_first_bound. fsri_gap_seed_first_bound + S (r) = (p)) /\ (((exists fsri_height_seed_first_entry. fsri_height_seed_first_entry + S (r) = S ((S (x4)) * (x1))) /\ exists fsri_quotient_seed_first_entry. (x) = fsri_quotient_seed_first_entry * S ((S (x4)) * (x1)) + (r)))))
  84. 0084specialize hsquares_witness_witness x4
  85. 0085apply hsquares_witness_witness
  86. 0086exact hcross_witness_witness_witness_left
  87. 0087cases hfirst
  88. 0088cases hfirst_witness
  89. 0089cases hfirst_witness_witness
  90. 0090cases hfirst_witness_witness_right
  91. 0091have hsecond : exists q r. (x5 * x5 = p * q + r /\ ((exists fsri_gap_seed_second_bound. fsri_gap_seed_second_bound + S (r) = (p)) /\ (((exists fsri_height_seed_second_entry. fsri_height_seed_second_entry + S (r) = S ((S (x5)) * (x1))) /\ exists fsri_quotient_seed_second_entry. (x) = fsri_quotient_seed_second_entry * S ((S (x5)) * (x1)) + (r)))))
  92. 0092specialize hsquares_witness_witness x5
  93. 0093apply hsquares_witness_witness
  94. 0094exact hcross_witness_witness_witness_right_left
  95. 0095cases hsecond
  96. 0096cases hsecond_witness
  97. 0097cases hsecond_witness_witness
  98. 0098cases hsecond_witness_witness_right
  99. 0099have hfirst_value : x8 = x6
  100. 0100specialize beta_at_unique x
  101. 0101specialize beta_at_unique x1
  102. 0102specialize beta_at_unique x4
  103. 0103specialize beta_at_unique x8
  104. 0104specialize beta_at_unique x6
  105. 0105apply beta_at_unique
  106. 0106exact hfirst_witness_witness_right_right
  107. 0107exact hcross_witness_witness_witness_right_right_left
  108. 0108rewrite hfirst_value at hfirst_witness_witness_left
  109. 0109have hgap : x6 + S x10 = p
  110. 0110specialize hcomplement_witness_witness x5
  111. 0111specialize hcomplement_witness_witness x10
  112. 0112specialize hcomplement_witness_witness x6
  113. 0113apply hcomplement_witness_witness
  114. 0114exact hcross_witness_witness_witness_right_left
  115. 0115exact hsecond_witness_witness_right_right
  116. 0116exact hcross_witness_witness_witness_right_right_right
  117. 0117have hmultiple : exists fsri_factor_seed_multiple. (x4 * x4 + x5 * x5 + 1) = (p) * fsri_factor_seed_multiple
  118. 0118specialize four_square_complementary_remainders_form_multiple p
  119. 0119specialize four_square_complementary_remainders_form_multiple (x4 * x4)
  120. 0120specialize four_square_complementary_remainders_form_multiple (x5 * x5)
  121. 0121specialize four_square_complementary_remainders_form_multiple x7
  122. 0122specialize four_square_complementary_remainders_form_multiple x6
  123. 0123specialize four_square_complementary_remainders_form_multiple x9
  124. 0124specialize four_square_complementary_remainders_form_multiple x10
  125. 0125apply four_square_complementary_remainders_form_multiple
  126. 0126exact hfirst_witness_witness_left
  127. 0127exact hsecond_witness_witness_left
  128. 0128exact hgap
  129. 0129cases hmultiple
  130. 0130exists x4
  131. 0131exists x5
  132. 0132exists x11
  133. 0133split
  134. 0134exact hmultiple_witness
  135. 0135split
  136. 0136specialize le_of_succ_le_succ x4
  137. 0137specialize le_of_succ_le_succ h
  138. 0138apply le_of_succ_le_succ
  139. 0139exact hcross_witness_witness_witness_left
  140. 0140specialize le_of_succ_le_succ x5
  141. 0141specialize le_of_succ_le_succ h
  142. 0142apply le_of_succ_le_succ
  143. 0143exact hcross_witness_witness_witness_right_left