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.
Exact expanded 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))))))))Structural proof guide
Every prime and natural input have a finite relational Legendre sum.
Direct prerequisites: prime_power_quotient_prefix_exists, beta_sum_exists. The authored body proceeds by case analysis (3), intermediate claims (2).
Proof neighborhood
Direct dependencies
Direct dependents
Formal native tactic body
Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.
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.
03Separate the logical casesL10–11
04Establish hsumL12–16
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 exact command ledger · 23 lines
- 0001
intro p - 0002
intro n - 0003
intro hp - 0004
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 : 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