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. ∀ a. p = 2 · h + 1 → Prime(p) → a = 2 → (QRes(p,2) → (∃ x. p = 8 · x + 1) ∨ (∃ x. p = 8 · x + 7)) ∧ ((∃ x. p = 8 · x + 1) ∨ (∃ x. p = 8 · x + 7) → QRes(p,2)) ∧ ((¬QRes(p,2) → (∃ x. p = 8 · x + 3) ∨ (∃ x. p = 8 · x + 5)) ∧ ((∃ x. p = 8 · x + 3) ∨ (∃ x. p = 8 · x + 5) → ¬QRes(p,2)))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
In local proof propositions
Exact expanded first-order 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)))))))Proof neighborhood
Direct theorem prerequisites
SL000P odd_prime_strictly_exceeds_two beta_range_exists · Stable closed SL0007 bounded_gauss_lemma_complete SL000N doubling_gauss_reflection_count_shape SL000O quadratic_supplement_two_conditional_on_gauss_count_shapeDirect theorem dependents
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
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)
01Fix variables and assumptionsL1–6
02Establish hpositiveL7–7
Establish this local claim before using it. It is not an additional assumption.
03Construct an explicit witnessL8–8
Supply the displayed value, then prove that it has the required property.
- L8
exists 1
04Calculate and transport equalitiesL9–10
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.
06Establish hrangeL18–21
Establish this local claim before using it. It is not an additional assumption.
- L18
have hrange : ∃ b. ∃ c. Range(b,c,1,h)Definitions: Range(b,c,1,h)Original native command in the exact edition - L19
specialize beta_range_exists 1 - L20
specialize beta_range_exists h - L21
exact beta_range_exists
07Separate the logical casesL22–23
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.
- 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: Lt(k,h)BetaAt(x,x1,k,i)BetaAt(y,z,k,j)BetaAt(n,m,k,u)Lt(0,j)Le(j,h)ModEq(p,a · i,j)ModEq(p,a · i,2 · h · j)BitCount(n,m,h,e)QRes(p,a)Even(e)Odd(e)Original native command in the exact edition - L25
specialize bounded_gauss_lemma_complete p - L26
specialize bounded_gauss_lemma_complete h - L27
specialize bounded_gauss_lemma_complete a - L28
specialize bounded_gauss_lemma_complete x - L29
specialize bounded_gauss_lemma_complete x1 - L30
apply bounded_gauss_lemma_complete - L31
exact hpodd - L32
exact hprime - L33
exact hpositive
09Use earlier factsL34–35
10Separate the logical casesL36–42
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
11Establish hshapeL43–52
Establish this local claim before using it. It is not an additional assumption.
- 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))) - L44
specialize doubling_gauss_reflection_count_shape p - L45
specialize doubling_gauss_reflection_count_shape h - L46
specialize doubling_gauss_reflection_count_shape a - L47
specialize doubling_gauss_reflection_count_shape x - L48
specialize doubling_gauss_reflection_count_shape x1 - L49
specialize doubling_gauss_reflection_count_shape x3 - L50
specialize doubling_gauss_reflection_count_shape x4 - L51
specialize doubling_gauss_reflection_count_shape x5 - L52
specialize doubling_gauss_reflection_count_shape x6
12Use earlier factsL53–62
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L53
specialize doubling_gauss_reflection_count_shape x2 - L54
apply doubling_gauss_reflection_count_shape - L55
exact hpodd - L56
exact hatwo - L57
exact hrange_witness_witness - L58
exact hgauss_witness_left_witness_witness_witness_witness_left - L59
exact hgauss_witness_left_witness_witness_witness_witness_right - L60
specialize quadratic_supplement_two_conditional_on_gauss_count_shape p - L61
specialize quadratic_supplement_two_conditional_on_gauss_count_shape h - L62
specialize quadratic_supplement_two_conditional_on_gauss_count_shape x2
13Use earlier factsL63–66
14Calculate and transport equalitiesL67–70
15Use earlier factsL71–71
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L71
exact hgauss_witness_right
Original defined command ledger · 71 lines
- 0001
intro p - 0002
intro h - 0003
intro a - 0004
intro hpodd - 0005
intro hprime - 0006
intro hatwo - 0007
have hpositive : Lt(0,a)Exact native replay line
have hpositive : exists gap. gap + S 0 = a - 0008
exists 1 - 0009
rewrite hatwo - 0010
norm_num - 0011
have hbound : Lt(a,p)Exact native replay line
have hbound : exists gap. gap + S a = p - 0012
rewrite hatwo - 0013
specialize odd_prime_strictly_exceeds_two p - 0014
specialize odd_prime_strictly_exceeds_two h - 0015
apply odd_prime_strictly_exceeds_two - 0016
exact hpodd - 0017
exact hprime - 0018
have hrange : ∃ b. ∃ c. Range(b,c,1,h)Exact native replay line
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)))) - 0019
specialize beta_range_exists 1 - 0020
specialize beta_range_exists h - 0021
exact beta_range_exists - 0022
cases hrange - 0023
cases hrange_witness - 0024
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))))Exact native replay line
have 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)))))))) - 0025
specialize bounded_gauss_lemma_complete p - 0026
specialize bounded_gauss_lemma_complete h - 0027
specialize bounded_gauss_lemma_complete a - 0028
specialize bounded_gauss_lemma_complete x - 0029
specialize bounded_gauss_lemma_complete x1 - 0030
apply bounded_gauss_lemma_complete - 0031
exact hpodd - 0032
exact hprime - 0033
exact hpositive - 0034
exact hbound - 0035
exact hrange_witness_witness - 0036
cases hgauss - 0037
cases hgauss_witness - 0038
cases hgauss_witness_left - 0039
cases hgauss_witness_left_witness - 0040
cases hgauss_witness_left_witness_witness - 0041
cases hgauss_witness_left_witness_witness_witness - 0042
cases hgauss_witness_left_witness_witness_witness_witness - 0043
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))) - 0044
specialize doubling_gauss_reflection_count_shape p - 0045
specialize doubling_gauss_reflection_count_shape h - 0046
specialize doubling_gauss_reflection_count_shape a - 0047
specialize doubling_gauss_reflection_count_shape x - 0048
specialize doubling_gauss_reflection_count_shape x1 - 0049
specialize doubling_gauss_reflection_count_shape x3 - 0050
specialize doubling_gauss_reflection_count_shape x4 - 0051
specialize doubling_gauss_reflection_count_shape x5 - 0052
specialize doubling_gauss_reflection_count_shape x6 - 0053
specialize doubling_gauss_reflection_count_shape x2 - 0054
apply doubling_gauss_reflection_count_shape - 0055
exact hpodd - 0056
exact hatwo - 0057
exact hrange_witness_witness - 0058
exact hgauss_witness_left_witness_witness_witness_witness_left - 0059
exact hgauss_witness_left_witness_witness_witness_witness_right - 0060
specialize quadratic_supplement_two_conditional_on_gauss_count_shape p - 0061
specialize quadratic_supplement_two_conditional_on_gauss_count_shape h - 0062
specialize quadratic_supplement_two_conditional_on_gauss_count_shape x2 - 0063
apply quadratic_supplement_two_conditional_on_gauss_count_shape - 0064
exact hpodd - 0065
exact hprime - 0066
exact hshape - 0067
rewrite hatwo at hgauss_witness_right - 0068
rewrite hatwo at hgauss_witness_right - 0069
rewrite hatwo at hgauss_witness_right - 0070
rewrite hatwo at hgauss_witness_right - 0071
exact hgauss_witness_right