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. ∀ b. ∀ c. p = 2 · h + 1 → Prime(p) → ¬Dvd(p,a) → Range(b,c,1,h) → ∃ x. ∃ y. ∃ z. ∃ n. ∀ m. Lt(m,h) → ∃ k. ∃ i. ∃ j. BetaAt(b,c,m,k) ∧ (BetaAt(x,y,m,i) ∧ (BetaAt(z,n,m,j) ∧ (Lt(0,i) ∧ (Le(i,h) ∧ ((j = 0 ∨ j = 1) ∧ (j = 0 ∧ ModEq(p,a · k,i) ∨ j = 1 ∧ ModEq(p,a · k,2 · h · i)))))))Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.
Definitions used by this theorem
In the theorem statement
11 occurrences
In local proof propositions
6 occurrences
Exact expanded native-PA statement
forall p h a b c. p = 2 * h + 1 -> ((~(p = 1) /\ forall gsp_prime_left_half_range_prime gsp_prime_right_half_range_prime. p = gsp_prime_left_half_range_prime * gsp_prime_right_half_range_prime -> gsp_prime_left_half_range_prime = 1 \/ gsp_prime_right_half_range_prime = 1)) -> (~(exists gsp_divisor_factor_half_range_multiplier. a = p * gsp_divisor_factor_half_range_multiplier)) -> (forall gsp_range_index_half_range_source. (exists gsp_lt_gap_half_range_source_range_bound. gsp_lt_gap_half_range_source_range_bound + S gsp_range_index_half_range_source = h) -> (((exists gsp_beta_height_half_range_source_range_entry. gsp_beta_height_half_range_source_range_entry + S (1 + gsp_range_index_half_range_source) = S ((S (gsp_range_index_half_range_source)) * c)) /\ exists gsp_beta_quotient_half_range_source_range_entry. b = gsp_beta_quotient_half_range_source_range_entry * S ((S (gsp_range_index_half_range_source)) * c) + (1 + gsp_range_index_half_range_source)))) -> (exists mb mc sb sc. (forall gsp_index_full_half_range_result. (exists gsp_lt_gap_full_half_range_result_index_bound. gsp_lt_gap_full_half_range_result_index_bound + S gsp_index_full_half_range_result = h) -> (exists gsp_value_full_half_range_result_entry gsp_magnitude_full_half_range_result_entry gsp_sign_full_half_range_result_entry. (((exists ff_h_gsp_full_half_range_result_entry_source. ff_h_gsp_full_half_range_result_entry_source + S (gsp_value_full_half_range_result_entry) = S ((S (gsp_index_full_half_range_result)) * c)) /\ exists ff_q_gsp_full_half_range_result_entry_source. b = ff_q_gsp_full_half_range_result_entry_source * S ((S (gsp_index_full_half_range_result)) * c) + (gsp_value_full_half_range_result_entry))) /\ ((((exists ff_h_gsp_full_half_range_result_entry_magnitude. ff_h_gsp_full_half_range_result_entry_magnitude + S (gsp_magnitude_full_half_range_result_entry) = S ((S (gsp_index_full_half_range_result)) * mc)) /\ exists ff_q_gsp_full_half_range_result_entry_magnitude. mb = ff_q_gsp_full_half_range_result_entry_magnitude * S ((S (gsp_index_full_half_range_result)) * mc) + (gsp_magnitude_full_half_range_result_entry))) /\ ((((exists ff_h_gsp_full_half_range_result_entry_sign. ff_h_gsp_full_half_range_result_entry_sign + S (gsp_sign_full_half_range_result_entry) = S ((S (gsp_index_full_half_range_result)) * sc)) /\ exists ff_q_gsp_full_half_range_result_entry_sign. sb = ff_q_gsp_full_half_range_result_entry_sign * S ((S (gsp_index_full_half_range_result)) * sc) + (gsp_sign_full_half_range_result_entry))) /\ ((exists gsp_lt_gap_full_half_range_result_entry_positive. gsp_lt_gap_full_half_range_result_entry_positive + S 0 = gsp_magnitude_full_half_range_result_entry) /\ ((exists gsp_le_gap_full_half_range_result_entry_bounded. gsp_le_gap_full_half_range_result_entry_bounded + gsp_magnitude_full_half_range_result_entry = h) /\ ((gsp_sign_full_half_range_result_entry = 0 \/ gsp_sign_full_half_range_result_entry = 1) /\ (((gsp_sign_full_half_range_result_entry = 0 /\ (exists gsp_mod_left_full_half_range_result_entry_lower gsp_mod_right_full_half_range_result_entry_lower. (a * gsp_value_full_half_range_result_entry) + p * gsp_mod_left_full_half_range_result_entry_lower = (gsp_magnitude_full_half_range_result_entry) + p * gsp_mod_right_full_half_range_result_entry_lower)) \/ (gsp_sign_full_half_range_result_entry = 1 /\ (exists gsp_mod_left_full_half_range_result_entry_reflected gsp_mod_right_full_half_range_result_entry_reflected. (a * gsp_value_full_half_range_result_entry) + p * gsp_mod_left_full_half_range_result_entry_reflected = ((2 * h) * gsp_magnitude_full_half_range_result_entry) + p * gsp_mod_right_full_half_range_result_entry_reflected))))))))))))Proof neighborhood
Direct theorem prerequisites
Direct theorem dependents
Definition-aware tactic body
Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed 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 (2)
01Fix variables and assumptionsL1–9
02Establish hchoicesL10–19
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gauss half range signed choices.
- L10
have hchoices : ∀ gsp_choice_index_half_range_choices. Lt(gsp_choice_index_half_range_choices,h) → ∃ x. ∃ y. ∃ z. BetaAt(b,c,gsp_choice_index_half_range_choices,x) ∧ (Lt(0,y) ∧ (Le(y,h) ∧ ((z = 0 ∨ z = 1) ∧ (z = 0 ∧ ModEq(p,a · x,y) ∨ z = 1 ∧ ModEq(p,a · x,2 · h · y)))))Definitions: Lt(gsp_choice_index_half_range_choices,h)BetaAt(b,c,gsp_choice_index_half_range_choices,x)Lt(0,y)Le(y,h)ModEq(p,a · x,y)ModEq(p,a · x,2 · h · y)Original native command in the exact edition - L11
specialize gauss_half_range_signed_choices p - L12
specialize gauss_half_range_signed_choices h - L13
specialize gauss_half_range_signed_choices a - L14
specialize gauss_half_range_signed_choices b - L15
specialize gauss_half_range_signed_choices c - L16
apply gauss_half_range_signed_choices - L17
exact hp - L18
exact hprime - L19
exact hnotdiv
03Use earlier factsL20–28
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L20
exact hrange - L21
specialize gauss_signed_half_prefix_exists p - L22
specialize gauss_signed_half_prefix_exists h - L23
specialize gauss_signed_half_prefix_exists a - L24
specialize gauss_signed_half_prefix_exists b - L25
specialize gauss_signed_half_prefix_exists c - L26
specialize gauss_signed_half_prefix_exists h - L27
apply gauss_signed_half_prefix_exists - L28
exact hchoices
Original defined command ledger · 28 lines
- 0001
intro p - 0002
intro h - 0003
intro a - 0004
intro b - 0005
intro c - 0006
intro hp - 0007
intro hprime - 0008
intro hnotdiv - 0009
intro hrange - 0010
have hchoices : ∀ gsp_choice_index_half_range_choices. Lt(gsp_choice_index_half_range_choices,h) → ∃ x. ∃ y. ∃ z. BetaAt(b,c,gsp_choice_index_half_range_choices,x) ∧ (Lt(0,y) ∧ (Le(y,h) ∧ ((z = 0 ∨ z = 1) ∧ (z = 0 ∧ ModEq(p,a · x,y) ∨ z = 1 ∧ ModEq(p,a · x,2 · h · y)))))Exact native replay line
have hchoices : forall gsp_choice_index_half_range_choices. (exists gsp_lt_gap_half_range_choices_choice_bound. gsp_lt_gap_half_range_choices_choice_bound + S gsp_choice_index_half_range_choices = h) -> (exists gsp_value_half_range_choices_choice gsp_magnitude_half_range_choices_choice gsp_sign_half_range_choices_choice. (((exists ff_h_gsp_half_range_choices_choice_source. ff_h_gsp_half_range_choices_choice_source + S (gsp_value_half_range_choices_choice) = S ((S (gsp_choice_index_half_range_choices)) * c)) /\ exists ff_q_gsp_half_range_choices_choice_source. b = ff_q_gsp_half_range_choices_choice_source * S ((S (gsp_choice_index_half_range_choices)) * c) + (gsp_value_half_range_choices_choice))) /\ ((exists gsp_lt_gap_half_range_choices_choice_positive. gsp_lt_gap_half_range_choices_choice_positive + S 0 = gsp_magnitude_half_range_choices_choice) /\ ((exists gsp_le_gap_half_range_choices_choice_bounded. gsp_le_gap_half_range_choices_choice_bounded + gsp_magnitude_half_range_choices_choice = h) /\ ((gsp_sign_half_range_choices_choice = 0 \/ gsp_sign_half_range_choices_choice = 1) /\ (((gsp_sign_half_range_choices_choice = 0 /\ (exists gsp_mod_left_half_range_choices_choice_lower gsp_mod_right_half_range_choices_choice_lower. (a * gsp_value_half_range_choices_choice) + p * gsp_mod_left_half_range_choices_choice_lower = (gsp_magnitude_half_range_choices_choice) + p * gsp_mod_right_half_range_choices_choice_lower)) \/ (gsp_sign_half_range_choices_choice = 1 /\ (exists gsp_mod_left_half_range_choices_choice_reflected gsp_mod_right_half_range_choices_choice_reflected. (a * gsp_value_half_range_choices_choice) + p * gsp_mod_left_half_range_choices_choice_reflected = ((2 * h) * gsp_magnitude_half_range_choices_choice) + p * gsp_mod_right_half_range_choices_choice_reflected)))))))) - 0011
specialize gauss_half_range_signed_choices p - 0012
specialize gauss_half_range_signed_choices h - 0013
specialize gauss_half_range_signed_choices a - 0014
specialize gauss_half_range_signed_choices b - 0015
specialize gauss_half_range_signed_choices c - 0016
apply gauss_half_range_signed_choices - 0017
exact hp - 0018
exact hprime - 0019
exact hnotdiv - 0020
exact hrange - 0021
specialize gauss_signed_half_prefix_exists p - 0022
specialize gauss_signed_half_prefix_exists h - 0023
specialize gauss_signed_half_prefix_exists a - 0024
specialize gauss_signed_half_prefix_exists b - 0025
specialize gauss_signed_half_prefix_exists c - 0026
specialize gauss_signed_half_prefix_exists h - 0027
apply gauss_signed_half_prefix_exists - 0028
exact hchoices