SL000Q

quadratic_supplement_two_half_complete

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

Complete constructive second supplementary law for an explicitly decomposed odd prime, with no unproved count-shape hypothesis.

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 a. p = 2 * h + 1 -> ((~(p = 1) /\ forall frm_prime_left_qst_half_prime frm_prime_right_qst_half_prime. p = frm_prime_left_qst_half_prime * frm_prime_right_qst_half_prime -> frm_prime_left_qst_half_prime = 1 \/ frm_prime_right_qst_half_prime = 1)) -> a = 2 -> ((((((exists qst_root_two. exists qst_mod_left_two qst_mod_right_two. qst_root_two * qst_root_two + p * qst_mod_left_two = 2 + p * qst_mod_right_two) -> (((exists qst_mod_eight_modulus_one. p = 8 * qst_mod_eight_modulus_one + 1) \/ (exists qst_mod_eight_modulus_seven. p = 8 * qst_mod_eight_modulus_seven + 7)))) /\ ((((exists qst_mod_eight_modulus_one. p = 8 * qst_mod_eight_modulus_one + 1) \/ (exists qst_mod_eight_modulus_seven. p = 8 * qst_mod_eight_modulus_seven + 7))) -> (exists qst_root_two. exists qst_mod_left_two qst_mod_right_two. qst_root_two * qst_root_two + p * qst_mod_left_two = 2 + p * qst_mod_right_two)))) /\ ((((~(exists qst_root_two. exists qst_mod_left_two qst_mod_right_two. qst_root_two * qst_root_two + p * qst_mod_left_two = 2 + p * qst_mod_right_two)) -> (((exists qst_mod_eight_modulus_three. p = 8 * qst_mod_eight_modulus_three + 3) \/ (exists qst_mod_eight_modulus_five. p = 8 * qst_mod_eight_modulus_five + 5)))) /\ ((((exists qst_mod_eight_modulus_three. p = 8 * qst_mod_eight_modulus_three + 3) \/ (exists qst_mod_eight_modulus_five. p = 8 * qst_mod_eight_modulus_five + 5))) -> (~(exists qst_root_two. exists qst_mod_left_two qst_mod_right_two. qst_root_two * qst_root_two + p * qst_mod_left_two = 2 + p * qst_mod_right_two)))))))

Constructive proof overview

Generated structural guide

Complete constructive second supplementary law for an explicitly decomposed odd prime, with no unproved count-shape hypothesis.

The unchanged tactic script uses 5 declared prerequisites and contains 71 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

SL000P odd_prime_strictly_exceeds_two beta_range_exists Stable theorem; checked-use authorized SL0007 bounded_gauss_lemma_complete SL000N doubling_gauss_reflection_count_shape SL000O quadratic_supplement_two_conditional_on_gauss_count_shape

Direct dependents

SL000R quadratic_supplement_two_residue_iff_mod_eight_one_or_seven SL000S quadratic_supplement_two_nonresidue_iff_mod_eight_three_or_five

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

71 script commands · 15 reading checkpoints · 5 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 (4)
odd prime strictly exceeds twobounded gauss lemma completedoubling gauss reflection count shapequadratic supplement two conditional on gauss count shape

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–6

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

  1. L1
    intro p
  2. L2
    intro h
  3. L3
    intro a
  4. L4
    intro hpodd
  5. L5
    intro hprime
  6. L6
    intro hatwo
02Establish hpositiveL7–7

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

  1. L7
    have hpositive : exists gap. gap + S 0 = a
03Construct an explicit witnessL8–8

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

  1. L8
    exists 1
04Calculate and transport equalitiesL9–10

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

  1. L9
    rewrite hatwo
  2. L10
    norm_num
05Establish hboundL11–17

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply odd prime strictly exceeds two.

  1. L11
    have hbound : exists gap. gap + S a = p
  2. L12
    rewrite hatwo
  3. L13
    specialize odd_prime_strictly_exceeds_two p
  4. L14
    specialize odd_prime_strictly_exceeds_two h
  5. L15
    apply odd_prime_strictly_exceeds_two
  6. L16
    exact hpodd
  7. L17
    exact hprime
06Establish hrangeL18–21

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

  1. L18
    have hrange : exists b c. (forall gsp_range_index_qst_gauss_range. (exists gsp_lt_gap_qst_gauss_range_range_bound. gsp_lt_gap_qst_gauss_range_range_bound + S gsp_range_index_qst_gauss_range = h) -> (((exists gsp_beta_height_qst_gauss_range_range_entry. gsp_beta_height_qst_gauss_range_range_entry + S (1 + gsp_range_index_qst_gauss_range) = S ((S (gsp_range_index_qst_gauss_range)) * c)) /\ exists gsp_beta_quotient_qst_gauss_range_range_entry. b = gsp_beta_quotient_qst_gauss_range_range_entry * S ((S (gsp_range_index_qst_gauss_range)) * c) + (1 + gsp_range_index_qst_gauss_range))))
  2. L19
    specialize beta_range_exists 1
  3. L20
    specialize beta_range_exists h
  4. L21
    exact beta_range_exists
07Separate the logical casesL22–23

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

  1. L22
    cases hrange
  2. L23
    cases hrange_witness
08Establish hgaussL24–33

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bounded gauss lemma complete.

  1. L24
    have hgauss : ∃ e. (∃ y. ∃ z. ∃ n. ∃ m. (∀ k. Lt(k,h) → ∃ i. ∃ j. ∃ u. BetaAt(x,x1,k,i) ∧ (BetaAt(y,z,k,j) ∧ (BetaAt(n,m,k,u) ∧ (Lt(0,j) ∧ (Le(j,h) ∧ ((u = 0 ∨ u = 1) ∧ (u = 0 ∧ ModEq(p,a · i,j) ∨ u = 1 ∧ ModEq(p,a · i,2 · h · j)))))))) ∧ BitCount(n,m,h,e)) ∧ ((QRes(p,a) → Even(e)) ∧ (Even(e) → QRes(p,a)) ∧ ((¬QRes(p,a) → Odd(e)) ∧ (Odd(e) → ¬QRes(p,a))))Definitions: LeLtModEqEvenOddBetaAtBitCountQRes
  2. L25
    specialize bounded_gauss_lemma_complete p
  3. L26
    specialize bounded_gauss_lemma_complete h
  4. L27
    specialize bounded_gauss_lemma_complete a
  5. L28
    specialize bounded_gauss_lemma_complete x
  6. L29
    specialize bounded_gauss_lemma_complete x1
  7. L30
    apply bounded_gauss_lemma_complete
  8. L31
    exact hpodd
  9. L32
    exact hprime
  10. L33
    exact hpositive
09Use earlier factsL34–35

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

  1. L34
    exact hbound
  2. L35
    exact hrange_witness_witness
10Separate the logical casesL36–42

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

  1. L36
    cases hgauss
  2. L37
    cases hgauss_witness
  3. L38
    cases hgauss_witness_left
  4. L39
    cases hgauss_witness_left_witness
  5. L40
    cases hgauss_witness_left_witness_witness
  6. L41
    cases hgauss_witness_left_witness_witness_witness
  7. L42
    cases hgauss_witness_left_witness_witness_witness_witness
11Establish hshapeL43–52

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

  1. L43
    have hshape : (((h = 2 * x2) \/ (exists qst_count_half_qst_gauss_final_shape. h = 2 * qst_count_half_qst_gauss_final_shape + 1 /\ x2 = S qst_count_half_qst_gauss_final_shape)))
  2. L44
    specialize doubling_gauss_reflection_count_shape p
  3. L45
    specialize doubling_gauss_reflection_count_shape h
  4. L46
    specialize doubling_gauss_reflection_count_shape a
  5. L47
    specialize doubling_gauss_reflection_count_shape x
  6. L48
    specialize doubling_gauss_reflection_count_shape x1
  7. L49
    specialize doubling_gauss_reflection_count_shape x3
  8. L50
    specialize doubling_gauss_reflection_count_shape x4
  9. L51
    specialize doubling_gauss_reflection_count_shape x5
  10. L52
    specialize doubling_gauss_reflection_count_shape x6
12Use earlier factsL53–62

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

  1. L53
    specialize doubling_gauss_reflection_count_shape x2
  2. L54
    apply doubling_gauss_reflection_count_shape
  3. L55
    exact hpodd
  4. L56
    exact hatwo
  5. L57
    exact hrange_witness_witness
  6. L58
    exact hgauss_witness_left_witness_witness_witness_witness_left
  7. L59
    exact hgauss_witness_left_witness_witness_witness_witness_right
  8. L60
    specialize quadratic_supplement_two_conditional_on_gauss_count_shape p
  9. L61
    specialize quadratic_supplement_two_conditional_on_gauss_count_shape h
  10. L62
    specialize quadratic_supplement_two_conditional_on_gauss_count_shape x2
13Use earlier factsL63–66

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

  1. L63
    apply quadratic_supplement_two_conditional_on_gauss_count_shape
  2. L64
    exact hpodd
  3. L65
    exact hprime
  4. L66
    exact hshape
14Calculate and transport equalitiesL67–70

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

  1. L67
    rewrite hatwo at hgauss_witness_right
  2. L68
    rewrite hatwo at hgauss_witness_right
  3. L69
    rewrite hatwo at hgauss_witness_right
  4. L70
    rewrite hatwo at hgauss_witness_right
15Use earlier factsL71–71

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

  1. L71
    exact hgauss_witness_right

Library-wide reading audit

Original exact command ledger · 71 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro a
  4. 0004intro hpodd
  5. 0005intro hprime
  6. 0006intro hatwo
  7. 0007have hpositive : exists gap. gap + S 0 = a
  8. 0008exists 1
  9. 0009rewrite hatwo
  10. 0010norm_num
  11. 0011have hbound : exists gap. gap + S a = p
  12. 0012rewrite hatwo
  13. 0013specialize odd_prime_strictly_exceeds_two p
  14. 0014specialize odd_prime_strictly_exceeds_two h
  15. 0015apply odd_prime_strictly_exceeds_two
  16. 0016exact hpodd
  17. 0017exact hprime
  18. 0018have hrange : exists b c. (forall gsp_range_index_qst_gauss_range. (exists gsp_lt_gap_qst_gauss_range_range_bound. gsp_lt_gap_qst_gauss_range_range_bound + S gsp_range_index_qst_gauss_range = h) -> (((exists gsp_beta_height_qst_gauss_range_range_entry. gsp_beta_height_qst_gauss_range_range_entry + S (1 + gsp_range_index_qst_gauss_range) = S ((S (gsp_range_index_qst_gauss_range)) * c)) /\ exists gsp_beta_quotient_qst_gauss_range_range_entry. b = gsp_beta_quotient_qst_gauss_range_range_entry * S ((S (gsp_range_index_qst_gauss_range)) * c) + (1 + gsp_range_index_qst_gauss_range))))
  19. 0019specialize beta_range_exists 1
  20. 0020specialize beta_range_exists h
  21. 0021exact beta_range_exists
  22. 0022cases hrange
  23. 0023cases hrange_witness
  24. 0024have hgauss : exists e. ((exists mb mc sb sc. ((forall gsp_index_qst_gauss_signed. (exists gsp_lt_gap_qst_gauss_signed_index_bound. gsp_lt_gap_qst_gauss_signed_index_bound + S gsp_index_qst_gauss_signed = h) -> (exists gsp_value_qst_gauss_signed_entry gsp_magnitude_qst_gauss_signed_entry gsp_sign_qst_gauss_signed_entry. (((exists ff_h_gsp_qst_gauss_signed_entry_source. ff_h_gsp_qst_gauss_signed_entry_source + S (gsp_value_qst_gauss_signed_entry) = S ((S (gsp_index_qst_gauss_signed)) * x1)) /\ exists ff_q_gsp_qst_gauss_signed_entry_source. x = ff_q_gsp_qst_gauss_signed_entry_source * S ((S (gsp_index_qst_gauss_signed)) * x1) + (gsp_value_qst_gauss_signed_entry))) /\ ((((exists ff_h_gsp_qst_gauss_signed_entry_magnitude. ff_h_gsp_qst_gauss_signed_entry_magnitude + S (gsp_magnitude_qst_gauss_signed_entry) = S ((S (gsp_index_qst_gauss_signed)) * mc)) /\ exists ff_q_gsp_qst_gauss_signed_entry_magnitude. mb = ff_q_gsp_qst_gauss_signed_entry_magnitude * S ((S (gsp_index_qst_gauss_signed)) * mc) + (gsp_magnitude_qst_gauss_signed_entry))) /\ ((((exists ff_h_gsp_qst_gauss_signed_entry_sign. ff_h_gsp_qst_gauss_signed_entry_sign + S (gsp_sign_qst_gauss_signed_entry) = S ((S (gsp_index_qst_gauss_signed)) * sc)) /\ exists ff_q_gsp_qst_gauss_signed_entry_sign. sb = ff_q_gsp_qst_gauss_signed_entry_sign * S ((S (gsp_index_qst_gauss_signed)) * sc) + (gsp_sign_qst_gauss_signed_entry))) /\ ((exists gsp_lt_gap_qst_gauss_signed_entry_positive. gsp_lt_gap_qst_gauss_signed_entry_positive + S 0 = gsp_magnitude_qst_gauss_signed_entry) /\ ((exists gsp_le_gap_qst_gauss_signed_entry_bounded. gsp_le_gap_qst_gauss_signed_entry_bounded + gsp_magnitude_qst_gauss_signed_entry = h) /\ ((gsp_sign_qst_gauss_signed_entry = 0 \/ gsp_sign_qst_gauss_signed_entry = 1) /\ (((gsp_sign_qst_gauss_signed_entry = 0 /\ (exists gsp_mod_left_qst_gauss_signed_entry_lower gsp_mod_right_qst_gauss_signed_entry_lower. (a * gsp_value_qst_gauss_signed_entry) + p * gsp_mod_left_qst_gauss_signed_entry_lower = (gsp_magnitude_qst_gauss_signed_entry) + p * gsp_mod_right_qst_gauss_signed_entry_lower)) \/ (gsp_sign_qst_gauss_signed_entry = 1 /\ (exists gsp_mod_left_qst_gauss_signed_entry_reflected gsp_mod_right_qst_gauss_signed_entry_reflected. (a * gsp_value_qst_gauss_signed_entry) + p * gsp_mod_left_qst_gauss_signed_entry_reflected = ((2 * h) * gsp_magnitude_qst_gauss_signed_entry) + p * gsp_mod_right_qst_gauss_signed_entry_reflected))))))))))) /\ (((exists ff_u_qst_gauss_count_sum ff_v_qst_gauss_count_sum. ((((exists ff_h_qst_gauss_count_sum_start. ff_h_qst_gauss_count_sum_start + S (0) = S ((S (0)) * ff_v_qst_gauss_count_sum)) /\ exists ff_q_qst_gauss_count_sum_start. ff_u_qst_gauss_count_sum = ff_q_qst_gauss_count_sum_start * S ((S (0)) * ff_v_qst_gauss_count_sum) + (0))) /\ ((((exists ff_h_qst_gauss_count_sum_terminal. ff_h_qst_gauss_count_sum_terminal + S (e) = S ((S (h)) * ff_v_qst_gauss_count_sum)) /\ exists ff_q_qst_gauss_count_sum_terminal. ff_u_qst_gauss_count_sum = ff_q_qst_gauss_count_sum_terminal * S ((S (h)) * ff_v_qst_gauss_count_sum) + (e))) /\ forall ff_i_qst_gauss_count_sum. (exists ff_lt_qst_gauss_count_sum_bound. ff_lt_qst_gauss_count_sum_bound + S ff_i_qst_gauss_count_sum = h) -> exists ff_a_qst_gauss_count_sum ff_r_qst_gauss_count_sum ff_s_qst_gauss_count_sum. ((((exists ff_h_qst_gauss_count_sum_summand. ff_h_qst_gauss_count_sum_summand + S (ff_a_qst_gauss_count_sum) = S ((S (ff_i_qst_gauss_count_sum)) * sc)) /\ exists ff_q_qst_gauss_count_sum_summand. sb = ff_q_qst_gauss_count_sum_summand * S ((S (ff_i_qst_gauss_count_sum)) * sc) + (ff_a_qst_gauss_count_sum))) /\ ((((exists ff_h_qst_gauss_count_sum_partial. ff_h_qst_gauss_count_sum_partial + S (ff_r_qst_gauss_count_sum) = S ((S (ff_i_qst_gauss_count_sum)) * ff_v_qst_gauss_count_sum)) /\ exists ff_q_qst_gauss_count_sum_partial. ff_u_qst_gauss_count_sum = ff_q_qst_gauss_count_sum_partial * S ((S (ff_i_qst_gauss_count_sum)) * ff_v_qst_gauss_count_sum) + (ff_r_qst_gauss_count_sum))) /\ ((((exists ff_h_qst_gauss_count_sum_successor. ff_h_qst_gauss_count_sum_successor + S (ff_s_qst_gauss_count_sum) = S ((S (S ff_i_qst_gauss_count_sum)) * ff_v_qst_gauss_count_sum)) /\ exists ff_q_qst_gauss_count_sum_successor. ff_u_qst_gauss_count_sum = ff_q_qst_gauss_count_sum_successor * S ((S (S ff_i_qst_gauss_count_sum)) * ff_v_qst_gauss_count_sum) + (ff_s_qst_gauss_count_sum))) /\ ff_s_qst_gauss_count_sum = ff_r_qst_gauss_count_sum + ff_a_qst_gauss_count_sum)))))) /\ (forall ff_i_qst_gauss_count_bits. (exists ff_lt_qst_gauss_count_bits_bound. ff_lt_qst_gauss_count_bits_bound + S ff_i_qst_gauss_count_bits = h) -> exists ff_bit_qst_gauss_count_bits. ((((exists ff_h_qst_gauss_count_bits_decoded. ff_h_qst_gauss_count_bits_decoded + S (ff_bit_qst_gauss_count_bits) = S ((S (ff_i_qst_gauss_count_bits)) * sc)) /\ exists ff_q_qst_gauss_count_bits_decoded. sb = ff_q_qst_gauss_count_bits_decoded * S ((S (ff_i_qst_gauss_count_bits)) * sc) + (ff_bit_qst_gauss_count_bits))) /\ (ff_bit_qst_gauss_count_bits = 0 \/ ff_bit_qst_gauss_count_bits = 1))))))) /\ ((((((exists qr_x_qst_gauss_two. exists qr_u_qst_gauss_two qr_v_qst_gauss_two. qr_x_qst_gauss_two * qr_x_qst_gauss_two + p * qr_u_qst_gauss_two = a + p * qr_v_qst_gauss_two) -> (exists qst_even_count. e = 2 * qst_even_count)) /\ ((exists qst_even_count. e = 2 * qst_even_count) -> (exists qr_x_qst_gauss_two. exists qr_u_qst_gauss_two qr_v_qst_gauss_two. qr_x_qst_gauss_two * qr_x_qst_gauss_two + p * qr_u_qst_gauss_two = a + p * qr_v_qst_gauss_two)))) /\ ((((~(exists qr_x_qst_gauss_two. exists qr_u_qst_gauss_two qr_v_qst_gauss_two. qr_x_qst_gauss_two * qr_x_qst_gauss_two + p * qr_u_qst_gauss_two = a + p * qr_v_qst_gauss_two)) -> (exists qst_odd_count. e = 2 * qst_odd_count + 1)) /\ ((exists qst_odd_count. e = 2 * qst_odd_count + 1) -> (~(exists qr_x_qst_gauss_two. exists qr_u_qst_gauss_two qr_v_qst_gauss_two. qr_x_qst_gauss_two * qr_x_qst_gauss_two + p * qr_u_qst_gauss_two = a + p * qr_v_qst_gauss_two))))))))
  25. 0025specialize bounded_gauss_lemma_complete p
  26. 0026specialize bounded_gauss_lemma_complete h
  27. 0027specialize bounded_gauss_lemma_complete a
  28. 0028specialize bounded_gauss_lemma_complete x
  29. 0029specialize bounded_gauss_lemma_complete x1
  30. 0030apply bounded_gauss_lemma_complete
  31. 0031exact hpodd
  32. 0032exact hprime
  33. 0033exact hpositive
  34. 0034exact hbound
  35. 0035exact hrange_witness_witness
  36. 0036cases hgauss
  37. 0037cases hgauss_witness
  38. 0038cases hgauss_witness_left
  39. 0039cases hgauss_witness_left_witness
  40. 0040cases hgauss_witness_left_witness_witness
  41. 0041cases hgauss_witness_left_witness_witness_witness
  42. 0042cases hgauss_witness_left_witness_witness_witness_witness
  43. 0043have hshape : (((h = 2 * x2) \/ (exists qst_count_half_qst_gauss_final_shape. h = 2 * qst_count_half_qst_gauss_final_shape + 1 /\ x2 = S qst_count_half_qst_gauss_final_shape)))
  44. 0044specialize doubling_gauss_reflection_count_shape p
  45. 0045specialize doubling_gauss_reflection_count_shape h
  46. 0046specialize doubling_gauss_reflection_count_shape a
  47. 0047specialize doubling_gauss_reflection_count_shape x
  48. 0048specialize doubling_gauss_reflection_count_shape x1
  49. 0049specialize doubling_gauss_reflection_count_shape x3
  50. 0050specialize doubling_gauss_reflection_count_shape x4
  51. 0051specialize doubling_gauss_reflection_count_shape x5
  52. 0052specialize doubling_gauss_reflection_count_shape x6
  53. 0053specialize doubling_gauss_reflection_count_shape x2
  54. 0054apply doubling_gauss_reflection_count_shape
  55. 0055exact hpodd
  56. 0056exact hatwo
  57. 0057exact hrange_witness_witness
  58. 0058exact hgauss_witness_left_witness_witness_witness_witness_left
  59. 0059exact hgauss_witness_left_witness_witness_witness_witness_right
  60. 0060specialize quadratic_supplement_two_conditional_on_gauss_count_shape p
  61. 0061specialize quadratic_supplement_two_conditional_on_gauss_count_shape h
  62. 0062specialize quadratic_supplement_two_conditional_on_gauss_count_shape x2
  63. 0063apply quadratic_supplement_two_conditional_on_gauss_count_shape
  64. 0064exact hpodd
  65. 0065exact hprime
  66. 0066exact hshape
  67. 0067rewrite hatwo at hgauss_witness_right
  68. 0068rewrite hatwo at hgauss_witness_right
  69. 0069rewrite hatwo at hgauss_witness_right
  70. 0070rewrite hatwo at hgauss_witness_right
  71. 0071exact hgauss_witness_right