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
∀ n. ∀ z. ∀ q. Primorial(n,z) → Pow(4,n,q) → Le(z,q)Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.
Definitions used by this theorem
In the theorem statement
3 occurrences
In local proof propositions
4 occurrences
Exact expanded native-PA statement
forall n z q. (exists bpr_code_bplfp_primorial bpr_scale_bplfp_primorial. ((forall bpr_index_bplfp_primorial_mask. (exists bpr_gap_bplfp_primorial_mask_bound. bpr_gap_bplfp_primorial_mask_bound + S (bpr_index_bplfp_primorial_mask) = n) -> exists bpr_value_bplfp_primorial_mask. ((((exists bpr_height_bplfp_primorial_mask_decoded. bpr_height_bplfp_primorial_mask_decoded + S (bpr_value_bplfp_primorial_mask) = S ((S (bpr_index_bplfp_primorial_mask)) * bpr_scale_bplfp_primorial)) /\ exists bpr_quotient_bplfp_primorial_mask_decoded. bpr_code_bplfp_primorial = bpr_quotient_bplfp_primorial_mask_decoded * S ((S (bpr_index_bplfp_primorial_mask)) * bpr_scale_bplfp_primorial) + (bpr_value_bplfp_primorial_mask))) /\ (((((~(S (bpr_index_bplfp_primorial_mask) = 1) /\ forall bpr_left_bplfp_primorial_mask_choice_prime bpr_right_bplfp_primorial_mask_choice_prime. S (bpr_index_bplfp_primorial_mask) = bpr_left_bplfp_primorial_mask_choice_prime * bpr_right_bplfp_primorial_mask_choice_prime -> bpr_left_bplfp_primorial_mask_choice_prime = 1 \/ bpr_right_bplfp_primorial_mask_choice_prime = 1)) /\ bpr_value_bplfp_primorial_mask = S (bpr_index_bplfp_primorial_mask)) \/ (~((~(S (bpr_index_bplfp_primorial_mask) = 1) /\ forall bpr_left_bplfp_primorial_mask_choice_prime bpr_right_bplfp_primorial_mask_choice_prime. S (bpr_index_bplfp_primorial_mask) = bpr_left_bplfp_primorial_mask_choice_prime * bpr_right_bplfp_primorial_mask_choice_prime -> bpr_left_bplfp_primorial_mask_choice_prime = 1 \/ bpr_right_bplfp_primorial_mask_choice_prime = 1)) /\ bpr_value_bplfp_primorial_mask = 1))))) /\ (exists ff_u_bplfp_primorial_product ff_v_bplfp_primorial_product. ((((exists ff_h_bplfp_primorial_product_start. ff_h_bplfp_primorial_product_start + S (1) = S ((S (0)) * ff_v_bplfp_primorial_product)) /\ exists ff_q_bplfp_primorial_product_start. ff_u_bplfp_primorial_product = ff_q_bplfp_primorial_product_start * S ((S (0)) * ff_v_bplfp_primorial_product) + (1))) /\ ((((exists ff_h_bplfp_primorial_product_terminal. ff_h_bplfp_primorial_product_terminal + S (z) = S ((S (n)) * ff_v_bplfp_primorial_product)) /\ exists ff_q_bplfp_primorial_product_terminal. ff_u_bplfp_primorial_product = ff_q_bplfp_primorial_product_terminal * S ((S (n)) * ff_v_bplfp_primorial_product) + (z))) /\ forall ff_i_bplfp_primorial_product. (exists ff_lt_bplfp_primorial_product_bound. ff_lt_bplfp_primorial_product_bound + S ff_i_bplfp_primorial_product = n) -> exists ff_p_bplfp_primorial_product ff_r_bplfp_primorial_product ff_s_bplfp_primorial_product. ((((exists ff_h_bplfp_primorial_product_factor. ff_h_bplfp_primorial_product_factor + S (ff_p_bplfp_primorial_product) = S ((S (ff_i_bplfp_primorial_product)) * bpr_scale_bplfp_primorial)) /\ exists ff_q_bplfp_primorial_product_factor. bpr_code_bplfp_primorial = ff_q_bplfp_primorial_product_factor * S ((S (ff_i_bplfp_primorial_product)) * bpr_scale_bplfp_primorial) + (ff_p_bplfp_primorial_product))) /\ ((((exists ff_h_bplfp_primorial_product_partial. ff_h_bplfp_primorial_product_partial + S (ff_r_bplfp_primorial_product) = S ((S (ff_i_bplfp_primorial_product)) * ff_v_bplfp_primorial_product)) /\ exists ff_q_bplfp_primorial_product_partial. ff_u_bplfp_primorial_product = ff_q_bplfp_primorial_product_partial * S ((S (ff_i_bplfp_primorial_product)) * ff_v_bplfp_primorial_product) + (ff_r_bplfp_primorial_product))) /\ ((((exists ff_h_bplfp_primorial_product_successor. ff_h_bplfp_primorial_product_successor + S (ff_s_bplfp_primorial_product) = S ((S (S ff_i_bplfp_primorial_product)) * ff_v_bplfp_primorial_product)) /\ exists ff_q_bplfp_primorial_product_successor. ff_u_bplfp_primorial_product = ff_q_bplfp_primorial_product_successor * S ((S (S ff_i_bplfp_primorial_product)) * ff_v_bplfp_primorial_product) + (ff_s_bplfp_primorial_product))) /\ ff_s_bplfp_primorial_product = ff_r_bplfp_primorial_product * ff_p_bplfp_primorial_product)))))))) -> (exists pa_b_bplfp_power pa_c_bplfp_power. ((forall pa_i_bplfp_power_repeat. (exists pa_lt_bplfp_power_repeat_bound. pa_lt_bplfp_power_repeat_bound + S pa_i_bplfp_power_repeat = n) -> (((exists pa_h_bplfp_power_repeat_decoded. pa_h_bplfp_power_repeat_decoded + S (4) = S ((S (pa_i_bplfp_power_repeat)) * pa_c_bplfp_power)) /\ exists pa_q_bplfp_power_repeat_decoded. pa_b_bplfp_power = pa_q_bplfp_power_repeat_decoded * S ((S (pa_i_bplfp_power_repeat)) * pa_c_bplfp_power) + (4)))) /\ (exists pa_u_bplfp_power_product pa_v_bplfp_power_product. ((((exists pa_h_bplfp_power_product_start. pa_h_bplfp_power_product_start + S (1) = S ((S (0)) * pa_v_bplfp_power_product)) /\ exists pa_q_bplfp_power_product_start. pa_u_bplfp_power_product = pa_q_bplfp_power_product_start * S ((S (0)) * pa_v_bplfp_power_product) + (1))) /\ ((((exists pa_h_bplfp_power_product_terminal. pa_h_bplfp_power_product_terminal + S (q) = S ((S (n)) * pa_v_bplfp_power_product)) /\ exists pa_q_bplfp_power_product_terminal. pa_u_bplfp_power_product = pa_q_bplfp_power_product_terminal * S ((S (n)) * pa_v_bplfp_power_product) + (q))) /\ forall pa_i_bplfp_power_product. (exists pa_lt_bplfp_power_product_bound. pa_lt_bplfp_power_product_bound + S pa_i_bplfp_power_product = n) -> exists pa_p_bplfp_power_product pa_r_bplfp_power_product pa_s_bplfp_power_product. ((((exists pa_h_bplfp_power_product_factor. pa_h_bplfp_power_product_factor + S (pa_p_bplfp_power_product) = S ((S (pa_i_bplfp_power_product)) * pa_c_bplfp_power)) /\ exists pa_q_bplfp_power_product_factor. pa_b_bplfp_power = pa_q_bplfp_power_product_factor * S ((S (pa_i_bplfp_power_product)) * pa_c_bplfp_power) + (pa_p_bplfp_power_product))) /\ ((((exists pa_h_bplfp_power_product_partial. pa_h_bplfp_power_product_partial + S (pa_r_bplfp_power_product) = S ((S (pa_i_bplfp_power_product)) * pa_v_bplfp_power_product)) /\ exists pa_q_bplfp_power_product_partial. pa_u_bplfp_power_product = pa_q_bplfp_power_product_partial * S ((S (pa_i_bplfp_power_product)) * pa_v_bplfp_power_product) + (pa_r_bplfp_power_product))) /\ ((((exists pa_h_bplfp_power_product_successor. pa_h_bplfp_power_product_successor + S (pa_s_bplfp_power_product) = S ((S (S pa_i_bplfp_power_product)) * pa_v_bplfp_power_product)) /\ exists pa_q_bplfp_power_product_successor. pa_u_bplfp_power_product = pa_q_bplfp_power_product_successor * S ((S (S pa_i_bplfp_power_product)) * pa_v_bplfp_power_product) + (pa_s_bplfp_power_product))) /\ pa_s_bplfp_power_product = pa_r_bplfp_power_product * pa_p_bplfp_power_product)))))))) -> (exists bcf_le_gap_bplfp_result. bcf_le_gap_bplfp_result + (z) = q)Proof neighborhood
Direct theorem prerequisites
Direct theorem dependents
Definition-aware tactic body
Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.
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 (3)
01Fix variables and assumptionsL1–5
02Establish hbounded_allL6–15
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply primorial le four pow bounded.
- L6
have hbounded_all : ∀ N. ∀ n. ∀ z. ∀ q. Le(n,N) → Primorial(n,z) → Pow(4,n,q) → Le(z,q)Definitions: Le(n,N)Primorial(n,z)Pow(4,n,q)Le(z,q)Original native command in the exact edition - L7
apply primorial_le_four_pow_bounded - L8
exact primorial_four_power_support_package - L9
specialize hbounded_all n - L10
specialize hbounded_all n - L11
specialize hbounded_all z - L12
specialize hbounded_all q - L13
apply hbounded_all - L14
specialize le_refl n - L15
exact le_refl
Original defined command ledger · 17 lines
- 0001
intro n - 0002
intro z - 0003
intro q - 0004
intro hprimorial - 0005
intro hpower - 0006
have hbounded_all : ∀ N. ∀ n. ∀ z. ∀ q. Le(n,N) → Primorial(n,z) → Pow(4,n,q) → Le(z,q)Exact native replay line
have hbounded_all : forall N n z q. (exists bcf_le_gap_bplfpb_index. bcf_le_gap_bplfpb_index + (n) = N) -> (exists bpr_code_bplfpb_primorial bpr_scale_bplfpb_primorial. ((forall bpr_index_bplfpb_primorial_mask. (exists bpr_gap_bplfpb_primorial_mask_bound. bpr_gap_bplfpb_primorial_mask_bound + S (bpr_index_bplfpb_primorial_mask) = n) -> exists bpr_value_bplfpb_primorial_mask. ((((exists bpr_height_bplfpb_primorial_mask_decoded. bpr_height_bplfpb_primorial_mask_decoded + S (bpr_value_bplfpb_primorial_mask) = S ((S (bpr_index_bplfpb_primorial_mask)) * bpr_scale_bplfpb_primorial)) /\ exists bpr_quotient_bplfpb_primorial_mask_decoded. bpr_code_bplfpb_primorial = bpr_quotient_bplfpb_primorial_mask_decoded * S ((S (bpr_index_bplfpb_primorial_mask)) * bpr_scale_bplfpb_primorial) + (bpr_value_bplfpb_primorial_mask))) /\ (((((~(S (bpr_index_bplfpb_primorial_mask) = 1) /\ forall bpr_left_bplfpb_primorial_mask_choice_prime bpr_right_bplfpb_primorial_mask_choice_prime. S (bpr_index_bplfpb_primorial_mask) = bpr_left_bplfpb_primorial_mask_choice_prime * bpr_right_bplfpb_primorial_mask_choice_prime -> bpr_left_bplfpb_primorial_mask_choice_prime = 1 \/ bpr_right_bplfpb_primorial_mask_choice_prime = 1)) /\ bpr_value_bplfpb_primorial_mask = S (bpr_index_bplfpb_primorial_mask)) \/ (~((~(S (bpr_index_bplfpb_primorial_mask) = 1) /\ forall bpr_left_bplfpb_primorial_mask_choice_prime bpr_right_bplfpb_primorial_mask_choice_prime. S (bpr_index_bplfpb_primorial_mask) = bpr_left_bplfpb_primorial_mask_choice_prime * bpr_right_bplfpb_primorial_mask_choice_prime -> bpr_left_bplfpb_primorial_mask_choice_prime = 1 \/ bpr_right_bplfpb_primorial_mask_choice_prime = 1)) /\ bpr_value_bplfpb_primorial_mask = 1))))) /\ (exists ff_u_bplfpb_primorial_product ff_v_bplfpb_primorial_product. ((((exists ff_h_bplfpb_primorial_product_start. ff_h_bplfpb_primorial_product_start + S (1) = S ((S (0)) * ff_v_bplfpb_primorial_product)) /\ exists ff_q_bplfpb_primorial_product_start. ff_u_bplfpb_primorial_product = ff_q_bplfpb_primorial_product_start * S ((S (0)) * ff_v_bplfpb_primorial_product) + (1))) /\ ((((exists ff_h_bplfpb_primorial_product_terminal. ff_h_bplfpb_primorial_product_terminal + S (z) = S ((S (n)) * ff_v_bplfpb_primorial_product)) /\ exists ff_q_bplfpb_primorial_product_terminal. ff_u_bplfpb_primorial_product = ff_q_bplfpb_primorial_product_terminal * S ((S (n)) * ff_v_bplfpb_primorial_product) + (z))) /\ forall ff_i_bplfpb_primorial_product. (exists ff_lt_bplfpb_primorial_product_bound. ff_lt_bplfpb_primorial_product_bound + S ff_i_bplfpb_primorial_product = n) -> exists ff_p_bplfpb_primorial_product ff_r_bplfpb_primorial_product ff_s_bplfpb_primorial_product. ((((exists ff_h_bplfpb_primorial_product_factor. ff_h_bplfpb_primorial_product_factor + S (ff_p_bplfpb_primorial_product) = S ((S (ff_i_bplfpb_primorial_product)) * bpr_scale_bplfpb_primorial)) /\ exists ff_q_bplfpb_primorial_product_factor. bpr_code_bplfpb_primorial = ff_q_bplfpb_primorial_product_factor * S ((S (ff_i_bplfpb_primorial_product)) * bpr_scale_bplfpb_primorial) + (ff_p_bplfpb_primorial_product))) /\ ((((exists ff_h_bplfpb_primorial_product_partial. ff_h_bplfpb_primorial_product_partial + S (ff_r_bplfpb_primorial_product) = S ((S (ff_i_bplfpb_primorial_product)) * ff_v_bplfpb_primorial_product)) /\ exists ff_q_bplfpb_primorial_product_partial. ff_u_bplfpb_primorial_product = ff_q_bplfpb_primorial_product_partial * S ((S (ff_i_bplfpb_primorial_product)) * ff_v_bplfpb_primorial_product) + (ff_r_bplfpb_primorial_product))) /\ ((((exists ff_h_bplfpb_primorial_product_successor. ff_h_bplfpb_primorial_product_successor + S (ff_s_bplfpb_primorial_product) = S ((S (S ff_i_bplfpb_primorial_product)) * ff_v_bplfpb_primorial_product)) /\ exists ff_q_bplfpb_primorial_product_successor. ff_u_bplfpb_primorial_product = ff_q_bplfpb_primorial_product_successor * S ((S (S ff_i_bplfpb_primorial_product)) * ff_v_bplfpb_primorial_product) + (ff_s_bplfpb_primorial_product))) /\ ff_s_bplfpb_primorial_product = ff_r_bplfpb_primorial_product * ff_p_bplfpb_primorial_product)))))))) -> (exists pa_b_bplfpb_power pa_c_bplfpb_power. ((forall pa_i_bplfpb_power_repeat. (exists pa_lt_bplfpb_power_repeat_bound. pa_lt_bplfpb_power_repeat_bound + S pa_i_bplfpb_power_repeat = n) -> (((exists pa_h_bplfpb_power_repeat_decoded. pa_h_bplfpb_power_repeat_decoded + S (4) = S ((S (pa_i_bplfpb_power_repeat)) * pa_c_bplfpb_power)) /\ exists pa_q_bplfpb_power_repeat_decoded. pa_b_bplfpb_power = pa_q_bplfpb_power_repeat_decoded * S ((S (pa_i_bplfpb_power_repeat)) * pa_c_bplfpb_power) + (4)))) /\ (exists pa_u_bplfpb_power_product pa_v_bplfpb_power_product. ((((exists pa_h_bplfpb_power_product_start. pa_h_bplfpb_power_product_start + S (1) = S ((S (0)) * pa_v_bplfpb_power_product)) /\ exists pa_q_bplfpb_power_product_start. pa_u_bplfpb_power_product = pa_q_bplfpb_power_product_start * S ((S (0)) * pa_v_bplfpb_power_product) + (1))) /\ ((((exists pa_h_bplfpb_power_product_terminal. pa_h_bplfpb_power_product_terminal + S (q) = S ((S (n)) * pa_v_bplfpb_power_product)) /\ exists pa_q_bplfpb_power_product_terminal. pa_u_bplfpb_power_product = pa_q_bplfpb_power_product_terminal * S ((S (n)) * pa_v_bplfpb_power_product) + (q))) /\ forall pa_i_bplfpb_power_product. (exists pa_lt_bplfpb_power_product_bound. pa_lt_bplfpb_power_product_bound + S pa_i_bplfpb_power_product = n) -> exists pa_p_bplfpb_power_product pa_r_bplfpb_power_product pa_s_bplfpb_power_product. ((((exists pa_h_bplfpb_power_product_factor. pa_h_bplfpb_power_product_factor + S (pa_p_bplfpb_power_product) = S ((S (pa_i_bplfpb_power_product)) * pa_c_bplfpb_power)) /\ exists pa_q_bplfpb_power_product_factor. pa_b_bplfpb_power = pa_q_bplfpb_power_product_factor * S ((S (pa_i_bplfpb_power_product)) * pa_c_bplfpb_power) + (pa_p_bplfpb_power_product))) /\ ((((exists pa_h_bplfpb_power_product_partial. pa_h_bplfpb_power_product_partial + S (pa_r_bplfpb_power_product) = S ((S (pa_i_bplfpb_power_product)) * pa_v_bplfpb_power_product)) /\ exists pa_q_bplfpb_power_product_partial. pa_u_bplfpb_power_product = pa_q_bplfpb_power_product_partial * S ((S (pa_i_bplfpb_power_product)) * pa_v_bplfpb_power_product) + (pa_r_bplfpb_power_product))) /\ ((((exists pa_h_bplfpb_power_product_successor. pa_h_bplfpb_power_product_successor + S (pa_s_bplfpb_power_product) = S ((S (S pa_i_bplfpb_power_product)) * pa_v_bplfpb_power_product)) /\ exists pa_q_bplfpb_power_product_successor. pa_u_bplfpb_power_product = pa_q_bplfpb_power_product_successor * S ((S (S pa_i_bplfpb_power_product)) * pa_v_bplfpb_power_product) + (pa_s_bplfpb_power_product))) /\ pa_s_bplfpb_power_product = pa_r_bplfpb_power_product * pa_p_bplfpb_power_product)))))))) -> (exists bcf_le_gap_bplfpb_result. bcf_le_gap_bplfpb_result + (z) = q) - 0007
apply primorial_le_four_pow_bounded - 0008
exact primorial_four_power_support_package - 0009
specialize hbounded_all n - 0010
specialize hbounded_all n - 0011
specialize hbounded_all z - 0012
specialize hbounded_all q - 0013
apply hbounded_all - 0014
specialize le_refl n - 0015
exact le_refl - 0016
exact hprimorial - 0017
exact hpower