BT00S2

prime_legendre_sum_exists

Alpha body-checked · checked-use disabled

Every prime and natural input have a finite relational Legendre sum.

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

BT00S0 prime_power_quotient_prefix_exists BT008A beta_sum_exists

Direct dependents

BT00T1 prime_factorial_valuation_eq_legendre_sum BT00Y4 central_binom_carry_bit_count

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro p
  2. 0002intro n
  3. 0003intro hp
  4. 0004have 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)))))
  5. 0005specialize prime_power_quotient_prefix_exists p
  6. 0006specialize prime_power_quotient_prefix_exists n
  7. 0007specialize prime_power_quotient_prefix_exists n
  8. 0008apply prime_power_quotient_prefix_exists
  9. 0009exact hp
  10. 0010cases hprefix
  11. 0011cases hprefix_witness
  12. 0012have 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))))))
  13. 0013specialize beta_sum_exists x
  14. 0014specialize beta_sum_exists x1
  15. 0015specialize beta_sum_exists n
  16. 0016exact beta_sum_exists
  17. 0017cases hsum
  18. 0018exists x2
  19. 0019exists x
  20. 0020exists x1
  21. 0021split
  22. 0022exact hprefix_witness_witness
  23. 0023exact hsum_witness