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. ∀ n. Prime(p) → ∃ x. LegendreSum(p,n,x)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
2 occurrences
In local proof propositions
2 occurrences
Exact expanded native-PA statement
forall p n. ((~(p = 1) /\ forall frm_prime_left_bls_prime frm_prime_right_bls_prime. p = frm_prime_left_bls_prime * frm_prime_right_bls_prime -> frm_prime_left_bls_prime = 1 \/ frm_prime_right_bls_prime = 1)) -> exists e. (exists bls_code_bls_total bls_scale_bls_total. ((forall bls_index_bls_total_prefix. (exists bls_gap_bls_total_prefix_bound. bls_gap_bls_total_prefix_bound + S (bls_index_bls_total_prefix) = (n)) -> exists bls_power_bls_total_prefix bls_quotient_bls_total_prefix bls_remainder_bls_total_prefix. ((exists bpvi_b_bls_bls_total_prefix_power bpvi_c_bls_bls_total_prefix_power. ((forall bpvi_i_bls_bls_total_prefix_power. (exists bpvi_repeat_gap_bls_bls_total_prefix_power. bpvi_repeat_gap_bls_bls_total_prefix_power + S bpvi_i_bls_bls_total_prefix_power = S bls_index_bls_total_prefix) -> (((exists bpvi_h_bls_bls_total_prefix_power_repeat. bpvi_h_bls_bls_total_prefix_power_repeat + S (p) = S ((S (bpvi_i_bls_bls_total_prefix_power)) * bpvi_c_bls_bls_total_prefix_power)) /\ exists bpvi_q_bls_bls_total_prefix_power_repeat. bpvi_b_bls_bls_total_prefix_power = bpvi_q_bls_bls_total_prefix_power_repeat * S ((S (bpvi_i_bls_bls_total_prefix_power)) * bpvi_c_bls_bls_total_prefix_power) + (p)))) /\ (exists bpvi_u_bls_bls_total_prefix_power bpvi_v_bls_bls_total_prefix_power. ((((exists bpvi_h_bls_bls_total_prefix_power_start. bpvi_h_bls_bls_total_prefix_power_start + S (1) = S ((S (0)) * bpvi_v_bls_bls_total_prefix_power)) /\ exists bpvi_q_bls_bls_total_prefix_power_start. bpvi_u_bls_bls_total_prefix_power = bpvi_q_bls_bls_total_prefix_power_start * S ((S (0)) * bpvi_v_bls_bls_total_prefix_power) + (1))) /\ ((((exists bpvi_h_bls_bls_total_prefix_power_terminal. bpvi_h_bls_bls_total_prefix_power_terminal + S (bls_power_bls_total_prefix) = S ((S (S bls_index_bls_total_prefix)) * bpvi_v_bls_bls_total_prefix_power)) /\ exists bpvi_q_bls_bls_total_prefix_power_terminal. bpvi_u_bls_bls_total_prefix_power = bpvi_q_bls_bls_total_prefix_power_terminal * S ((S (S bls_index_bls_total_prefix)) * bpvi_v_bls_bls_total_prefix_power) + (bls_power_bls_total_prefix))) /\ forall bpvi_j_bls_bls_total_prefix_power. (exists bpvi_product_gap_bls_bls_total_prefix_power. bpvi_product_gap_bls_bls_total_prefix_power + S bpvi_j_bls_bls_total_prefix_power = S bls_index_bls_total_prefix) -> exists bpvi_factor_bls_bls_total_prefix_power bpvi_partial_bls_bls_total_prefix_power bpvi_successor_bls_bls_total_prefix_power. ((((exists bpvi_h_bls_bls_total_prefix_power_factor. bpvi_h_bls_bls_total_prefix_power_factor + S (bpvi_factor_bls_bls_total_prefix_power) = S ((S (bpvi_j_bls_bls_total_prefix_power)) * bpvi_c_bls_bls_total_prefix_power)) /\ exists bpvi_q_bls_bls_total_prefix_power_factor. bpvi_b_bls_bls_total_prefix_power = bpvi_q_bls_bls_total_prefix_power_factor * S ((S (bpvi_j_bls_bls_total_prefix_power)) * bpvi_c_bls_bls_total_prefix_power) + (bpvi_factor_bls_bls_total_prefix_power))) /\ ((((exists bpvi_h_bls_bls_total_prefix_power_partial. bpvi_h_bls_bls_total_prefix_power_partial + S (bpvi_partial_bls_bls_total_prefix_power) = S ((S (bpvi_j_bls_bls_total_prefix_power)) * bpvi_v_bls_bls_total_prefix_power)) /\ exists bpvi_q_bls_bls_total_prefix_power_partial. bpvi_u_bls_bls_total_prefix_power = bpvi_q_bls_bls_total_prefix_power_partial * S ((S (bpvi_j_bls_bls_total_prefix_power)) * bpvi_v_bls_bls_total_prefix_power) + (bpvi_partial_bls_bls_total_prefix_power))) /\ ((((exists bpvi_h_bls_bls_total_prefix_power_successor. bpvi_h_bls_bls_total_prefix_power_successor + S (bpvi_successor_bls_bls_total_prefix_power) = S ((S (S bpvi_j_bls_bls_total_prefix_power)) * bpvi_v_bls_bls_total_prefix_power)) /\ exists bpvi_q_bls_bls_total_prefix_power_successor. bpvi_u_bls_bls_total_prefix_power = bpvi_q_bls_bls_total_prefix_power_successor * S ((S (S bpvi_j_bls_bls_total_prefix_power)) * bpvi_v_bls_bls_total_prefix_power) + (bpvi_successor_bls_bls_total_prefix_power))) /\ bpvi_successor_bls_bls_total_prefix_power = bpvi_partial_bls_bls_total_prefix_power * bpvi_factor_bls_bls_total_prefix_power)))))))) /\ ((((exists ff_h_bls_bls_total_prefix_quotient_entry. ff_h_bls_bls_total_prefix_quotient_entry + S (bls_quotient_bls_total_prefix) = S ((S (bls_index_bls_total_prefix)) * bls_scale_bls_total)) /\ exists ff_q_bls_bls_total_prefix_quotient_entry. bls_code_bls_total = ff_q_bls_bls_total_prefix_quotient_entry * S ((S (bls_index_bls_total_prefix)) * bls_scale_bls_total) + (bls_quotient_bls_total_prefix))) /\ ((n = bls_power_bls_total_prefix * bls_quotient_bls_total_prefix + bls_remainder_bls_total_prefix /\ exists bls_remainder_gap_bls_total_prefix_division. bls_remainder_gap_bls_total_prefix_division + S (bls_remainder_bls_total_prefix) = bls_power_bls_total_prefix))))) /\ (exists ff_u_bls_bls_total_sum ff_v_bls_bls_total_sum. ((((exists ff_h_bls_bls_total_sum_start. ff_h_bls_bls_total_sum_start + S (0) = S ((S (0)) * ff_v_bls_bls_total_sum)) /\ exists ff_q_bls_bls_total_sum_start. ff_u_bls_bls_total_sum = ff_q_bls_bls_total_sum_start * S ((S (0)) * ff_v_bls_bls_total_sum) + (0))) /\ ((((exists ff_h_bls_bls_total_sum_terminal. ff_h_bls_bls_total_sum_terminal + S (e) = S ((S (n)) * ff_v_bls_bls_total_sum)) /\ exists ff_q_bls_bls_total_sum_terminal. ff_u_bls_bls_total_sum = ff_q_bls_bls_total_sum_terminal * S ((S (n)) * ff_v_bls_bls_total_sum) + (e))) /\ forall ff_i_bls_bls_total_sum. (exists ff_lt_bls_bls_total_sum_bound. ff_lt_bls_bls_total_sum_bound + S ff_i_bls_bls_total_sum = n) -> exists ff_a_bls_bls_total_sum ff_r_bls_bls_total_sum ff_s_bls_bls_total_sum. ((((exists ff_h_bls_bls_total_sum_summand. ff_h_bls_bls_total_sum_summand + S (ff_a_bls_bls_total_sum) = S ((S (ff_i_bls_bls_total_sum)) * bls_scale_bls_total)) /\ exists ff_q_bls_bls_total_sum_summand. bls_code_bls_total = ff_q_bls_bls_total_sum_summand * S ((S (ff_i_bls_bls_total_sum)) * bls_scale_bls_total) + (ff_a_bls_bls_total_sum))) /\ ((((exists ff_h_bls_bls_total_sum_partial. ff_h_bls_bls_total_sum_partial + S (ff_r_bls_bls_total_sum) = S ((S (ff_i_bls_bls_total_sum)) * ff_v_bls_bls_total_sum)) /\ exists ff_q_bls_bls_total_sum_partial. ff_u_bls_bls_total_sum = ff_q_bls_bls_total_sum_partial * S ((S (ff_i_bls_bls_total_sum)) * ff_v_bls_bls_total_sum) + (ff_r_bls_bls_total_sum))) /\ ((((exists ff_h_bls_bls_total_sum_successor. ff_h_bls_bls_total_sum_successor + S (ff_s_bls_bls_total_sum) = S ((S (S ff_i_bls_bls_total_sum)) * ff_v_bls_bls_total_sum)) /\ exists ff_q_bls_bls_total_sum_successor. ff_u_bls_bls_total_sum = ff_q_bls_bls_total_sum_successor * S ((S (S ff_i_bls_bls_total_sum)) * ff_v_bls_bls_total_sum) + (ff_s_bls_bls_total_sum))) /\ ff_s_bls_bls_total_sum = ff_r_bls_bls_total_sum + ff_a_bls_bls_total_sum))))))))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 (2)
01Fix variables and assumptionsL1–3
02Establish hprefixL4–9
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime power quotient prefix exists.
- L4
have hprefix : ∃ b. ∃ c. PowerQuotPrefix(p,n,b,c,n)Definitions: PowerQuotPrefix(p,n,b,c,n)Original native command in the exact edition - L5
specialize prime_power_quotient_prefix_exists p - L6
specialize prime_power_quotient_prefix_exists n - L7
specialize prime_power_quotient_prefix_exists n - L8
apply prime_power_quotient_prefix_exists - L9
exact hp
03Separate the logical casesL10–11
04Establish hsumL12–16
Establish this local claim before using it. It is not an additional assumption.
- L12
have hsum : ∃ e. Sum(x,x1,n,e)Definitions: Sum(x,x1,n,e)Original native command in the exact edition - L13
specialize beta_sum_exists x - L14
specialize beta_sum_exists x1 - L15
specialize beta_sum_exists n - L16
exact beta_sum_exists
05Separate the logical casesL17–17
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L17
cases hsum
06Construct an explicit witnessL18–20
07Separate the logical casesL21–21
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L21
split
Original defined command ledger · 23 lines
- 0001
intro p - 0002
intro n - 0003
intro hp - 0004
have hprefix : ∃ b. ∃ c. PowerQuotPrefix(p,n,b,c,n)Exact native replay line
have hprefix : exists b c. (forall bls_index_bls_total_witness. (exists bls_gap_bls_total_witness_bound. bls_gap_bls_total_witness_bound + S (bls_index_bls_total_witness) = (n)) -> exists bls_power_bls_total_witness bls_quotient_bls_total_witness bls_remainder_bls_total_witness. ((exists bpvi_b_bls_bls_total_witness_power bpvi_c_bls_bls_total_witness_power. ((forall bpvi_i_bls_bls_total_witness_power. (exists bpvi_repeat_gap_bls_bls_total_witness_power. bpvi_repeat_gap_bls_bls_total_witness_power + S bpvi_i_bls_bls_total_witness_power = S bls_index_bls_total_witness) -> (((exists bpvi_h_bls_bls_total_witness_power_repeat. bpvi_h_bls_bls_total_witness_power_repeat + S (p) = S ((S (bpvi_i_bls_bls_total_witness_power)) * bpvi_c_bls_bls_total_witness_power)) /\ exists bpvi_q_bls_bls_total_witness_power_repeat. bpvi_b_bls_bls_total_witness_power = bpvi_q_bls_bls_total_witness_power_repeat * S ((S (bpvi_i_bls_bls_total_witness_power)) * bpvi_c_bls_bls_total_witness_power) + (p)))) /\ (exists bpvi_u_bls_bls_total_witness_power bpvi_v_bls_bls_total_witness_power. ((((exists bpvi_h_bls_bls_total_witness_power_start. bpvi_h_bls_bls_total_witness_power_start + S (1) = S ((S (0)) * bpvi_v_bls_bls_total_witness_power)) /\ exists bpvi_q_bls_bls_total_witness_power_start. bpvi_u_bls_bls_total_witness_power = bpvi_q_bls_bls_total_witness_power_start * S ((S (0)) * bpvi_v_bls_bls_total_witness_power) + (1))) /\ ((((exists bpvi_h_bls_bls_total_witness_power_terminal. bpvi_h_bls_bls_total_witness_power_terminal + S (bls_power_bls_total_witness) = S ((S (S bls_index_bls_total_witness)) * bpvi_v_bls_bls_total_witness_power)) /\ exists bpvi_q_bls_bls_total_witness_power_terminal. bpvi_u_bls_bls_total_witness_power = bpvi_q_bls_bls_total_witness_power_terminal * S ((S (S bls_index_bls_total_witness)) * bpvi_v_bls_bls_total_witness_power) + (bls_power_bls_total_witness))) /\ forall bpvi_j_bls_bls_total_witness_power. (exists bpvi_product_gap_bls_bls_total_witness_power. bpvi_product_gap_bls_bls_total_witness_power + S bpvi_j_bls_bls_total_witness_power = S bls_index_bls_total_witness) -> exists bpvi_factor_bls_bls_total_witness_power bpvi_partial_bls_bls_total_witness_power bpvi_successor_bls_bls_total_witness_power. ((((exists bpvi_h_bls_bls_total_witness_power_factor. bpvi_h_bls_bls_total_witness_power_factor + S (bpvi_factor_bls_bls_total_witness_power) = S ((S (bpvi_j_bls_bls_total_witness_power)) * bpvi_c_bls_bls_total_witness_power)) /\ exists bpvi_q_bls_bls_total_witness_power_factor. bpvi_b_bls_bls_total_witness_power = bpvi_q_bls_bls_total_witness_power_factor * S ((S (bpvi_j_bls_bls_total_witness_power)) * bpvi_c_bls_bls_total_witness_power) + (bpvi_factor_bls_bls_total_witness_power))) /\ ((((exists bpvi_h_bls_bls_total_witness_power_partial. bpvi_h_bls_bls_total_witness_power_partial + S (bpvi_partial_bls_bls_total_witness_power) = S ((S (bpvi_j_bls_bls_total_witness_power)) * bpvi_v_bls_bls_total_witness_power)) /\ exists bpvi_q_bls_bls_total_witness_power_partial. bpvi_u_bls_bls_total_witness_power = bpvi_q_bls_bls_total_witness_power_partial * S ((S (bpvi_j_bls_bls_total_witness_power)) * bpvi_v_bls_bls_total_witness_power) + (bpvi_partial_bls_bls_total_witness_power))) /\ ((((exists bpvi_h_bls_bls_total_witness_power_successor. bpvi_h_bls_bls_total_witness_power_successor + S (bpvi_successor_bls_bls_total_witness_power) = S ((S (S bpvi_j_bls_bls_total_witness_power)) * bpvi_v_bls_bls_total_witness_power)) /\ exists bpvi_q_bls_bls_total_witness_power_successor. bpvi_u_bls_bls_total_witness_power = bpvi_q_bls_bls_total_witness_power_successor * S ((S (S bpvi_j_bls_bls_total_witness_power)) * bpvi_v_bls_bls_total_witness_power) + (bpvi_successor_bls_bls_total_witness_power))) /\ bpvi_successor_bls_bls_total_witness_power = bpvi_partial_bls_bls_total_witness_power * bpvi_factor_bls_bls_total_witness_power)))))))) /\ ((((exists ff_h_bls_bls_total_witness_quotient_entry. ff_h_bls_bls_total_witness_quotient_entry + S (bls_quotient_bls_total_witness) = S ((S (bls_index_bls_total_witness)) * c)) /\ exists ff_q_bls_bls_total_witness_quotient_entry. b = ff_q_bls_bls_total_witness_quotient_entry * S ((S (bls_index_bls_total_witness)) * c) + (bls_quotient_bls_total_witness))) /\ ((n = bls_power_bls_total_witness * bls_quotient_bls_total_witness + bls_remainder_bls_total_witness /\ exists bls_remainder_gap_bls_total_witness_division. bls_remainder_gap_bls_total_witness_division + S (bls_remainder_bls_total_witness) = bls_power_bls_total_witness))))) - 0005
specialize prime_power_quotient_prefix_exists p - 0006
specialize prime_power_quotient_prefix_exists n - 0007
specialize prime_power_quotient_prefix_exists n - 0008
apply prime_power_quotient_prefix_exists - 0009
exact hp - 0010
cases hprefix - 0011
cases hprefix_witness - 0012
have hsum : ∃ e. Sum(x,x1,n,e)Exact native replay line
have hsum : exists e. (exists ff_u_bls_total_sum_witness ff_v_bls_total_sum_witness. ((((exists ff_h_bls_total_sum_witness_start. ff_h_bls_total_sum_witness_start + S (0) = S ((S (0)) * ff_v_bls_total_sum_witness)) /\ exists ff_q_bls_total_sum_witness_start. ff_u_bls_total_sum_witness = ff_q_bls_total_sum_witness_start * S ((S (0)) * ff_v_bls_total_sum_witness) + (0))) /\ ((((exists ff_h_bls_total_sum_witness_terminal. ff_h_bls_total_sum_witness_terminal + S (e) = S ((S (n)) * ff_v_bls_total_sum_witness)) /\ exists ff_q_bls_total_sum_witness_terminal. ff_u_bls_total_sum_witness = ff_q_bls_total_sum_witness_terminal * S ((S (n)) * ff_v_bls_total_sum_witness) + (e))) /\ forall ff_i_bls_total_sum_witness. (exists ff_lt_bls_total_sum_witness_bound. ff_lt_bls_total_sum_witness_bound + S ff_i_bls_total_sum_witness = n) -> exists ff_a_bls_total_sum_witness ff_r_bls_total_sum_witness ff_s_bls_total_sum_witness. ((((exists ff_h_bls_total_sum_witness_summand. ff_h_bls_total_sum_witness_summand + S (ff_a_bls_total_sum_witness) = S ((S (ff_i_bls_total_sum_witness)) * x1)) /\ exists ff_q_bls_total_sum_witness_summand. x = ff_q_bls_total_sum_witness_summand * S ((S (ff_i_bls_total_sum_witness)) * x1) + (ff_a_bls_total_sum_witness))) /\ ((((exists ff_h_bls_total_sum_witness_partial. ff_h_bls_total_sum_witness_partial + S (ff_r_bls_total_sum_witness) = S ((S (ff_i_bls_total_sum_witness)) * ff_v_bls_total_sum_witness)) /\ exists ff_q_bls_total_sum_witness_partial. ff_u_bls_total_sum_witness = ff_q_bls_total_sum_witness_partial * S ((S (ff_i_bls_total_sum_witness)) * ff_v_bls_total_sum_witness) + (ff_r_bls_total_sum_witness))) /\ ((((exists ff_h_bls_total_sum_witness_successor. ff_h_bls_total_sum_witness_successor + S (ff_s_bls_total_sum_witness) = S ((S (S ff_i_bls_total_sum_witness)) * ff_v_bls_total_sum_witness)) /\ exists ff_q_bls_total_sum_witness_successor. ff_u_bls_total_sum_witness = ff_q_bls_total_sum_witness_successor * S ((S (S ff_i_bls_total_sum_witness)) * ff_v_bls_total_sum_witness) + (ff_s_bls_total_sum_witness))) /\ ff_s_bls_total_sum_witness = ff_r_bls_total_sum_witness + ff_a_bls_total_sum_witness)))))) - 0013
specialize beta_sum_exists x - 0014
specialize beta_sum_exists x1 - 0015
specialize beta_sum_exists n - 0016
exact beta_sum_exists - 0017
cases hsum - 0018
exists x2 - 0019
exists x - 0020
exists x1 - 0021
split - 0022
exact hprefix_witness_witness - 0023
exact hsum_witness