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. ∀ a. ∀ n. ∀ u. ∀ v. ∀ h. ∀ A. p = S n → Prime(p) → ¬QRes(p,a) → ScaledInversePrefix(p,a,n,u,v,n) → n = h + h → Pow(a,h,A) → ModEq(p,A,n)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
5 occurrences
In local proof propositions
12 occurrences
Exact expanded native-PA statement
forall p a n u v h A. p = S n -> ((~(p = 1) /\ forall esi_prime_left_enr_prime esi_prime_right_enr_prime. p = esi_prime_left_enr_prime * esi_prime_right_enr_prime -> esi_prime_left_enr_prime = 1 \/ esi_prime_right_enr_prime = 1)) -> ~(exists qr_x_enr_nonresidue. exists qr_u_enr_nonresidue qr_v_enr_nonresidue. qr_x_enr_nonresidue * qr_x_enr_nonresidue + p * qr_u_enr_nonresidue = a + p * qr_v_enr_nonresidue) -> (forall esip_index_enr_prefix. (exists esip_gap_enr_prefix_prefix_bound. esip_gap_enr_prefix_prefix_bound + S (esip_index_enr_prefix) = n) -> exists esip_mate_enr_prefix. ((((exists ff_h_esip_enr_prefix_entry. ff_h_esip_enr_prefix_entry + S (esip_mate_enr_prefix) = S ((S (esip_index_enr_prefix)) * v)) /\ exists ff_q_esip_enr_prefix_entry. u = ff_q_esip_enr_prefix_entry * S ((S (esip_index_enr_prefix)) * v) + (esip_mate_enr_prefix))) /\ ((exists esip_gap_enr_prefix_relation_index_bound. esip_gap_enr_prefix_relation_index_bound + S (esip_index_enr_prefix) = n) /\ ((((~((S esip_index_enr_prefix) = 0) /\ (exists esip_gap_enr_prefix_relation_scaled_left_bound. esip_gap_enr_prefix_relation_scaled_left_bound + S (S esip_index_enr_prefix) = p))) /\ (((~(esip_mate_enr_prefix = 0) /\ (exists esip_gap_enr_prefix_relation_scaled_right_bound. esip_gap_enr_prefix_relation_scaled_right_bound + S (esip_mate_enr_prefix) = p))) /\ (exists esi_mod_left_enr_prefix_relation_scaled_mod esi_mod_right_enr_prefix_relation_scaled_mod. ((S esip_index_enr_prefix) * esip_mate_enr_prefix) + p * esi_mod_left_enr_prefix_relation_scaled_mod = (a) + p * esi_mod_right_enr_prefix_relation_scaled_mod))))))) -> n = h + h -> (exists ff_b_enr_terminal_power ff_c_enr_terminal_power. ((forall ff_i_enr_terminal_power_repeat. (exists ff_lt_enr_terminal_power_repeat_bound. ff_lt_enr_terminal_power_repeat_bound + S ff_i_enr_terminal_power_repeat = h) -> (((exists ff_h_enr_terminal_power_repeat_decoded. ff_h_enr_terminal_power_repeat_decoded + S (a) = S ((S (ff_i_enr_terminal_power_repeat)) * ff_c_enr_terminal_power)) /\ exists ff_q_enr_terminal_power_repeat_decoded. ff_b_enr_terminal_power = ff_q_enr_terminal_power_repeat_decoded * S ((S (ff_i_enr_terminal_power_repeat)) * ff_c_enr_terminal_power) + (a)))) /\ (exists ff_u_enr_terminal_power_product ff_v_enr_terminal_power_product. ((((exists ff_h_enr_terminal_power_product_start. ff_h_enr_terminal_power_product_start + S (1) = S ((S (0)) * ff_v_enr_terminal_power_product)) /\ exists ff_q_enr_terminal_power_product_start. ff_u_enr_terminal_power_product = ff_q_enr_terminal_power_product_start * S ((S (0)) * ff_v_enr_terminal_power_product) + (1))) /\ ((((exists ff_h_enr_terminal_power_product_terminal. ff_h_enr_terminal_power_product_terminal + S (A) = S ((S (h)) * ff_v_enr_terminal_power_product)) /\ exists ff_q_enr_terminal_power_product_terminal. ff_u_enr_terminal_power_product = ff_q_enr_terminal_power_product_terminal * S ((S (h)) * ff_v_enr_terminal_power_product) + (A))) /\ forall ff_i_enr_terminal_power_product. (exists ff_lt_enr_terminal_power_product_bound. ff_lt_enr_terminal_power_product_bound + S ff_i_enr_terminal_power_product = h) -> exists ff_p_enr_terminal_power_product ff_r_enr_terminal_power_product ff_s_enr_terminal_power_product. ((((exists ff_h_enr_terminal_power_product_factor. ff_h_enr_terminal_power_product_factor + S (ff_p_enr_terminal_power_product) = S ((S (ff_i_enr_terminal_power_product)) * ff_c_enr_terminal_power)) /\ exists ff_q_enr_terminal_power_product_factor. ff_b_enr_terminal_power = ff_q_enr_terminal_power_product_factor * S ((S (ff_i_enr_terminal_power_product)) * ff_c_enr_terminal_power) + (ff_p_enr_terminal_power_product))) /\ ((((exists ff_h_enr_terminal_power_product_partial. ff_h_enr_terminal_power_product_partial + S (ff_r_enr_terminal_power_product) = S ((S (ff_i_enr_terminal_power_product)) * ff_v_enr_terminal_power_product)) /\ exists ff_q_enr_terminal_power_product_partial. ff_u_enr_terminal_power_product = ff_q_enr_terminal_power_product_partial * S ((S (ff_i_enr_terminal_power_product)) * ff_v_enr_terminal_power_product) + (ff_r_enr_terminal_power_product))) /\ ((((exists ff_h_enr_terminal_power_product_successor. ff_h_enr_terminal_power_product_successor + S (ff_s_enr_terminal_power_product) = S ((S (S ff_i_enr_terminal_power_product)) * ff_v_enr_terminal_power_product)) /\ exists ff_q_enr_terminal_power_product_successor. ff_u_enr_terminal_power_product = ff_q_enr_terminal_power_product_successor * S ((S (S ff_i_enr_terminal_power_product)) * ff_v_enr_terminal_power_product) + (ff_s_enr_terminal_power_product))) /\ ff_s_enr_terminal_power_product = ff_r_enr_terminal_power_product * ff_p_enr_terminal_power_product)))))))) -> (exists wpp_mod_left_enr_terminal_result wpp_mod_right_enr_terminal_result. (A) + p * wpp_mod_left_enr_terminal_result = (n) + p * wpp_mod_right_enr_terminal_result)Proof neighborhood
Direct theorem prerequisites
PA009W scaled_inverse_pair_order_terminal_package PA00BK scaled_pair_order_terminal_power_mod_predecessorDirect 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–10
02Fix variables and assumptionsL11–13
03Establish hterminalL14–23
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply scaled inverse pair order terminal package.
- L14
have hterminal : ∃ b. ∃ c. (∀ x. ∀ y. ∀ z. Lt(x,h + h) → BetaAt(b,c,x,y) → BetaAt(u,v,y,S z) → ContainsPrefix(b,c,h + h,z)) ∧ ((∀ x. Lt(x,h + h) → ∃ y. BetaAt(b,c,x,y) ∧ Lt(y,n)) ∧ InjectivePrefix(b,c,h + h)) ∧ (∀ x. Lt(x,h) → ∃ y. ∃ z. BetaAt(b,c,x + x,y) ∧ (BetaAt(b,c,S (x + x),z) ∧ BetaAt(u,v,y,S z)))Definitions: Lt(x,h + h)BetaAt(b,c,x,y)BetaAt(u,v,y,S z)ContainsPrefix(b,c,h + h,z)Lt(y,n)InjectivePrefix(b,c,h + h)Lt(x,h)BetaAt(b,c,x + x,y)BetaAt(b,c,S (x + x),z)Original native command in the exact edition - L15
specialize scaled_inverse_pair_order_terminal_package p - L16
specialize scaled_inverse_pair_order_terminal_package a - L17
specialize scaled_inverse_pair_order_terminal_package n - L18
specialize scaled_inverse_pair_order_terminal_package u - L19
specialize scaled_inverse_pair_order_terminal_package v - L20
specialize scaled_inverse_pair_order_terminal_package h - L21
apply scaled_inverse_pair_order_terminal_package - L22
exact hpn - L23
exact hp
04Use earlier factsL24–26
05Separate the logical casesL27–29
06Use earlier factsL30–39
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L30
specialize scaled_pair_order_terminal_power_mod_predecessor p - L31
specialize scaled_pair_order_terminal_power_mod_predecessor a - L32
specialize scaled_pair_order_terminal_power_mod_predecessor n - L33
specialize scaled_pair_order_terminal_power_mod_predecessor u - L34
specialize scaled_pair_order_terminal_power_mod_predecessor v - L35
specialize scaled_pair_order_terminal_power_mod_predecessor x - L36
specialize scaled_pair_order_terminal_power_mod_predecessor x1 - L37
specialize scaled_pair_order_terminal_power_mod_predecessor h - L38
specialize scaled_pair_order_terminal_power_mod_predecessor A - L39
apply scaled_pair_order_terminal_power_mod_predecessor
Original defined command ledger · 46 lines
- 0001
intro p - 0002
intro a - 0003
intro n - 0004
intro u - 0005
intro v - 0006
intro h - 0007
intro A - 0008
intro hpn - 0009
intro hp - 0010
intro hnonresidue - 0011
intro hprefix - 0012
intro heven - 0013
intro hpower - 0014
have hterminal : ∃ b. ∃ c. (∀ x. ∀ y. ∀ z. Lt(x,h + h) → BetaAt(b,c,x,y) → BetaAt(u,v,y,S z) → ContainsPrefix(b,c,h + h,z)) ∧ ((∀ x. Lt(x,h + h) → ∃ y. BetaAt(b,c,x,y) ∧ Lt(y,n)) ∧ InjectivePrefix(b,c,h + h)) ∧ (∀ x. Lt(x,h) → ∃ y. ∃ z. BetaAt(b,c,x + x,y) ∧ (BetaAt(b,c,S (x + x),z) ∧ BetaAt(u,v,y,S z)))Exact native replay line
have hterminal : exists b c. (((forall espo_position_enr_terminal_state_closed espo_source_enr_terminal_state_closed espo_mate_enr_terminal_state_closed. (exists wpo_gap_enr_terminal_state_closed_position_bound. wpo_gap_enr_terminal_state_closed_position_bound + S (espo_position_enr_terminal_state_closed) = h + h) -> (((exists wpo_beta_height_enr_terminal_state_closed_source_entry. wpo_beta_height_enr_terminal_state_closed_source_entry + S (espo_source_enr_terminal_state_closed) = S ((S (espo_position_enr_terminal_state_closed)) * c)) /\ exists wpo_beta_quotient_enr_terminal_state_closed_source_entry. b = wpo_beta_quotient_enr_terminal_state_closed_source_entry * S ((S (espo_position_enr_terminal_state_closed)) * c) + (espo_source_enr_terminal_state_closed))) -> (((exists wpo_beta_height_enr_terminal_state_closed_scaled_entry. wpo_beta_height_enr_terminal_state_closed_scaled_entry + S (S espo_mate_enr_terminal_state_closed) = S ((S (espo_source_enr_terminal_state_closed)) * v)) /\ exists wpo_beta_quotient_enr_terminal_state_closed_scaled_entry. u = wpo_beta_quotient_enr_terminal_state_closed_scaled_entry * S ((S (espo_source_enr_terminal_state_closed)) * v) + (S espo_mate_enr_terminal_state_closed))) -> exists espo_mate_position_enr_terminal_state_closed. ((exists wpo_gap_enr_terminal_state_closed_mate_bound. wpo_gap_enr_terminal_state_closed_mate_bound + S (espo_mate_position_enr_terminal_state_closed) = h + h) /\ (((exists wpo_beta_height_enr_terminal_state_closed_mate_entry. wpo_beta_height_enr_terminal_state_closed_mate_entry + S (espo_mate_enr_terminal_state_closed) = S ((S (espo_mate_position_enr_terminal_state_closed)) * c)) /\ exists wpo_beta_quotient_enr_terminal_state_closed_mate_entry. b = wpo_beta_quotient_enr_terminal_state_closed_mate_entry * S ((S (espo_mate_position_enr_terminal_state_closed)) * c) + (espo_mate_enr_terminal_state_closed))))) /\ (((forall fom_index_enr_terminal_state_bounded. (exists fom_gap_enr_terminal_state_bounded_index_bound. fom_gap_enr_terminal_state_bounded_index_bound + S (fom_index_enr_terminal_state_bounded) = h + h) -> exists fom_value_enr_terminal_state_bounded. ((((exists fom_beta_height_enr_terminal_state_bounded_entry. fom_beta_height_enr_terminal_state_bounded_entry + S (fom_value_enr_terminal_state_bounded) = S ((S (fom_index_enr_terminal_state_bounded)) * c)) /\ exists fom_beta_quotient_enr_terminal_state_bounded_entry. b = fom_beta_quotient_enr_terminal_state_bounded_entry * S ((S (fom_index_enr_terminal_state_bounded)) * c) + (fom_value_enr_terminal_state_bounded))) /\ (exists fom_gap_enr_terminal_state_bounded_value_bound. fom_gap_enr_terminal_state_bounded_value_bound + S (fom_value_enr_terminal_state_bounded) = n))) /\ (forall wpo_injective_left_enr_terminal_state_injective wpo_injective_right_enr_terminal_state_injective wpo_injective_value_enr_terminal_state_injective. (exists wpo_gap_enr_terminal_state_injective_left_bound. wpo_gap_enr_terminal_state_injective_left_bound + S (wpo_injective_left_enr_terminal_state_injective) = h + h) -> (exists wpo_gap_enr_terminal_state_injective_right_bound. wpo_gap_enr_terminal_state_injective_right_bound + S (wpo_injective_right_enr_terminal_state_injective) = h + h) -> (((exists wpo_beta_height_enr_terminal_state_injective_left_entry. wpo_beta_height_enr_terminal_state_injective_left_entry + S (wpo_injective_value_enr_terminal_state_injective) = S ((S (wpo_injective_left_enr_terminal_state_injective)) * c)) /\ exists wpo_beta_quotient_enr_terminal_state_injective_left_entry. b = wpo_beta_quotient_enr_terminal_state_injective_left_entry * S ((S (wpo_injective_left_enr_terminal_state_injective)) * c) + (wpo_injective_value_enr_terminal_state_injective))) -> (((exists wpo_beta_height_enr_terminal_state_injective_right_entry. wpo_beta_height_enr_terminal_state_injective_right_entry + S (wpo_injective_value_enr_terminal_state_injective) = S ((S (wpo_injective_right_enr_terminal_state_injective)) * c)) /\ exists wpo_beta_quotient_enr_terminal_state_injective_right_entry. b = wpo_beta_quotient_enr_terminal_state_injective_right_entry * S ((S (wpo_injective_right_enr_terminal_state_injective)) * c) + (wpo_injective_value_enr_terminal_state_injective))) -> wpo_injective_left_enr_terminal_state_injective = wpo_injective_right_enr_terminal_state_injective))))) /\ (forall espi_pair_enr_history. (exists wpo_gap_enr_history_pair_bound. wpo_gap_enr_history_pair_bound + S (espi_pair_enr_history) = h) -> exists espi_left_enr_history espi_right_enr_history. (((((exists wpo_beta_height_enr_history_left_entry. wpo_beta_height_enr_history_left_entry + S (espi_left_enr_history) = S ((S (espi_pair_enr_history + espi_pair_enr_history)) * c)) /\ exists wpo_beta_quotient_enr_history_left_entry. b = wpo_beta_quotient_enr_history_left_entry * S ((S (espi_pair_enr_history + espi_pair_enr_history)) * c) + (espi_left_enr_history))) /\ (((((exists wpo_beta_height_enr_history_right_entry. wpo_beta_height_enr_history_right_entry + S (espi_right_enr_history) = S ((S (S (espi_pair_enr_history + espi_pair_enr_history))) * c)) /\ exists wpo_beta_quotient_enr_history_right_entry. b = wpo_beta_quotient_enr_history_right_entry * S ((S (S (espi_pair_enr_history + espi_pair_enr_history))) * c) + (espi_right_enr_history))) /\ (((exists wpo_beta_height_enr_history_scaled_edge. wpo_beta_height_enr_history_scaled_edge + S (S espi_right_enr_history) = S ((S (espi_left_enr_history)) * v)) /\ exists wpo_beta_quotient_enr_history_scaled_edge. u = wpo_beta_quotient_enr_history_scaled_edge * S ((S (espi_left_enr_history)) * v) + (S espi_right_enr_history)))))))) - 0015
specialize scaled_inverse_pair_order_terminal_package p - 0016
specialize scaled_inverse_pair_order_terminal_package a - 0017
specialize scaled_inverse_pair_order_terminal_package n - 0018
specialize scaled_inverse_pair_order_terminal_package u - 0019
specialize scaled_inverse_pair_order_terminal_package v - 0020
specialize scaled_inverse_pair_order_terminal_package h - 0021
apply scaled_inverse_pair_order_terminal_package - 0022
exact hpn - 0023
exact hp - 0024
exact hnonresidue - 0025
exact hprefix - 0026
exact heven - 0027
cases hterminal - 0028
cases hterminal_witness - 0029
cases hterminal_witness_witness - 0030
specialize scaled_pair_order_terminal_power_mod_predecessor p - 0031
specialize scaled_pair_order_terminal_power_mod_predecessor a - 0032
specialize scaled_pair_order_terminal_power_mod_predecessor n - 0033
specialize scaled_pair_order_terminal_power_mod_predecessor u - 0034
specialize scaled_pair_order_terminal_power_mod_predecessor v - 0035
specialize scaled_pair_order_terminal_power_mod_predecessor x - 0036
specialize scaled_pair_order_terminal_power_mod_predecessor x1 - 0037
specialize scaled_pair_order_terminal_power_mod_predecessor h - 0038
specialize scaled_pair_order_terminal_power_mod_predecessor A - 0039
apply scaled_pair_order_terminal_power_mod_predecessor - 0040
exact hpn - 0041
exact hp - 0042
exact hprefix - 0043
exact heven - 0044
exact hterminal_witness_witness_left - 0045
exact hterminal_witness_witness_right - 0046
exact hpower