BT00SU

initial_segment_prefix_sum_exists

Alpha body-checked · checked-use disabled

Every bounded threshold has a beta prefix whose exact sum is the threshold.

Exact expanded PA statement

forall q k. (exists blrr_le_gap_blrr_initial_bound. blrr_le_gap_blrr_initial_bound + (q) = (k)) -> (exists b c. ((forall eis_index_blrr_initial_prefix. (exists eis_lt_gap_blrr_initial_prefix_bound. eis_lt_gap_blrr_initial_prefix_bound + S (eis_index_blrr_initial_prefix) = k) -> exists eis_bit_blrr_initial_prefix. ((((exists ff_h_eis_blrr_initial_prefix_decoded. ff_h_eis_blrr_initial_prefix_decoded + S (eis_bit_blrr_initial_prefix) = S ((S (eis_index_blrr_initial_prefix)) * c)) /\ exists ff_q_eis_blrr_initial_prefix_decoded. b = ff_q_eis_blrr_initial_prefix_decoded * S ((S (eis_index_blrr_initial_prefix)) * c) + (eis_bit_blrr_initial_prefix))) /\ (((eis_bit_blrr_initial_prefix = 1 /\ (exists eis_le_gap_blrr_initial_prefix_choice_inside. eis_le_gap_blrr_initial_prefix_choice_inside + (S eis_index_blrr_initial_prefix) = q)) \/ (eis_bit_blrr_initial_prefix = 0 /\ (exists eis_lt_gap_blrr_initial_prefix_choice_outside. eis_lt_gap_blrr_initial_prefix_choice_outside + S (q) = S eis_index_blrr_initial_prefix)))))) /\ (exists ff_u_blrr_initial_sum ff_v_blrr_initial_sum. ((((exists ff_h_blrr_initial_sum_start. ff_h_blrr_initial_sum_start + S (0) = S ((S (0)) * ff_v_blrr_initial_sum)) /\ exists ff_q_blrr_initial_sum_start. ff_u_blrr_initial_sum = ff_q_blrr_initial_sum_start * S ((S (0)) * ff_v_blrr_initial_sum) + (0))) /\ ((((exists ff_h_blrr_initial_sum_terminal. ff_h_blrr_initial_sum_terminal + S (q) = S ((S (k)) * ff_v_blrr_initial_sum)) /\ exists ff_q_blrr_initial_sum_terminal. ff_u_blrr_initial_sum = ff_q_blrr_initial_sum_terminal * S ((S (k)) * ff_v_blrr_initial_sum) + (q))) /\ forall ff_i_blrr_initial_sum. (exists ff_lt_blrr_initial_sum_bound. ff_lt_blrr_initial_sum_bound + S ff_i_blrr_initial_sum = k) -> exists ff_a_blrr_initial_sum ff_r_blrr_initial_sum ff_s_blrr_initial_sum. ((((exists ff_h_blrr_initial_sum_summand. ff_h_blrr_initial_sum_summand + S (ff_a_blrr_initial_sum) = S ((S (ff_i_blrr_initial_sum)) * c)) /\ exists ff_q_blrr_initial_sum_summand. b = ff_q_blrr_initial_sum_summand * S ((S (ff_i_blrr_initial_sum)) * c) + (ff_a_blrr_initial_sum))) /\ ((((exists ff_h_blrr_initial_sum_partial. ff_h_blrr_initial_sum_partial + S (ff_r_blrr_initial_sum) = S ((S (ff_i_blrr_initial_sum)) * ff_v_blrr_initial_sum)) /\ exists ff_q_blrr_initial_sum_partial. ff_u_blrr_initial_sum = ff_q_blrr_initial_sum_partial * S ((S (ff_i_blrr_initial_sum)) * ff_v_blrr_initial_sum) + (ff_r_blrr_initial_sum))) /\ ((((exists ff_h_blrr_initial_sum_successor. ff_h_blrr_initial_sum_successor + S (ff_s_blrr_initial_sum) = S ((S (S ff_i_blrr_initial_sum)) * ff_v_blrr_initial_sum)) /\ exists ff_q_blrr_initial_sum_successor. ff_u_blrr_initial_sum = ff_q_blrr_initial_sum_successor * S ((S (S ff_i_blrr_initial_sum)) * ff_v_blrr_initial_sum) + (ff_s_blrr_initial_sum))) /\ ff_s_blrr_initial_sum = ff_r_blrr_initial_sum + ff_a_blrr_initial_sum))))))))

Structural proof guide

Every bounded threshold has a beta prefix whose exact sum is the threshold.

Direct prerequisites: eisenstein_initial_segment_prefix_exists, eisenstein_initial_segment_bit_count_exact. The authored body proceeds by case analysis (3), intermediate claims (2).

Proof neighborhood

Direct dependencies

BT00SF eisenstein_initial_segment_prefix_exists BT00JE eisenstein_initial_segment_bit_count_exact

Direct dependents

BT00SV prime_legendre_sum_succ

Formal native tactic body

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

  1. 0001intro q
  2. 0002intro k
  3. 0003intro hbound
  4. 0004have hprefix : exists b c. (forall eis_index_blrr_initial_prefix. (exists eis_lt_gap_blrr_initial_prefix_bound. eis_lt_gap_blrr_initial_prefix_bound + S (eis_index_blrr_initial_prefix) = k) -> exists eis_bit_blrr_initial_prefix. ((((exists ff_h_eis_blrr_initial_prefix_decoded. ff_h_eis_blrr_initial_prefix_decoded + S (eis_bit_blrr_initial_prefix) = S ((S (eis_index_blrr_initial_prefix)) * c)) /\ exists ff_q_eis_blrr_initial_prefix_decoded. b = ff_q_eis_blrr_initial_prefix_decoded * S ((S (eis_index_blrr_initial_prefix)) * c) + (eis_bit_blrr_initial_prefix))) /\ (((eis_bit_blrr_initial_prefix = 1 /\ (exists eis_le_gap_blrr_initial_prefix_choice_inside. eis_le_gap_blrr_initial_prefix_choice_inside + (S eis_index_blrr_initial_prefix) = q)) \/ (eis_bit_blrr_initial_prefix = 0 /\ (exists eis_lt_gap_blrr_initial_prefix_choice_outside. eis_lt_gap_blrr_initial_prefix_choice_outside + S (q) = S eis_index_blrr_initial_prefix))))))
  5. 0005specialize eisenstein_initial_segment_prefix_exists q
  6. 0006specialize eisenstein_initial_segment_prefix_exists k
  7. 0007exact eisenstein_initial_segment_prefix_exists
  8. 0008cases hprefix
  9. 0009cases hprefix_witness
  10. 0010have hcount : ((exists ff_u_blrr_initial_exact_count_sum ff_v_blrr_initial_exact_count_sum. ((((exists ff_h_blrr_initial_exact_count_sum_start. ff_h_blrr_initial_exact_count_sum_start + S (0) = S ((S (0)) * ff_v_blrr_initial_exact_count_sum)) /\ exists ff_q_blrr_initial_exact_count_sum_start. ff_u_blrr_initial_exact_count_sum = ff_q_blrr_initial_exact_count_sum_start * S ((S (0)) * ff_v_blrr_initial_exact_count_sum) + (0))) /\ ((((exists ff_h_blrr_initial_exact_count_sum_terminal. ff_h_blrr_initial_exact_count_sum_terminal + S (q) = S ((S (k)) * ff_v_blrr_initial_exact_count_sum)) /\ exists ff_q_blrr_initial_exact_count_sum_terminal. ff_u_blrr_initial_exact_count_sum = ff_q_blrr_initial_exact_count_sum_terminal * S ((S (k)) * ff_v_blrr_initial_exact_count_sum) + (q))) /\ forall ff_i_blrr_initial_exact_count_sum. (exists ff_lt_blrr_initial_exact_count_sum_bound. ff_lt_blrr_initial_exact_count_sum_bound + S ff_i_blrr_initial_exact_count_sum = k) -> exists ff_a_blrr_initial_exact_count_sum ff_r_blrr_initial_exact_count_sum ff_s_blrr_initial_exact_count_sum. ((((exists ff_h_blrr_initial_exact_count_sum_summand. ff_h_blrr_initial_exact_count_sum_summand + S (ff_a_blrr_initial_exact_count_sum) = S ((S (ff_i_blrr_initial_exact_count_sum)) * x1)) /\ exists ff_q_blrr_initial_exact_count_sum_summand. x = ff_q_blrr_initial_exact_count_sum_summand * S ((S (ff_i_blrr_initial_exact_count_sum)) * x1) + (ff_a_blrr_initial_exact_count_sum))) /\ ((((exists ff_h_blrr_initial_exact_count_sum_partial. ff_h_blrr_initial_exact_count_sum_partial + S (ff_r_blrr_initial_exact_count_sum) = S ((S (ff_i_blrr_initial_exact_count_sum)) * ff_v_blrr_initial_exact_count_sum)) /\ exists ff_q_blrr_initial_exact_count_sum_partial. ff_u_blrr_initial_exact_count_sum = ff_q_blrr_initial_exact_count_sum_partial * S ((S (ff_i_blrr_initial_exact_count_sum)) * ff_v_blrr_initial_exact_count_sum) + (ff_r_blrr_initial_exact_count_sum))) /\ ((((exists ff_h_blrr_initial_exact_count_sum_successor. ff_h_blrr_initial_exact_count_sum_successor + S (ff_s_blrr_initial_exact_count_sum) = S ((S (S ff_i_blrr_initial_exact_count_sum)) * ff_v_blrr_initial_exact_count_sum)) /\ exists ff_q_blrr_initial_exact_count_sum_successor. ff_u_blrr_initial_exact_count_sum = ff_q_blrr_initial_exact_count_sum_successor * S ((S (S ff_i_blrr_initial_exact_count_sum)) * ff_v_blrr_initial_exact_count_sum) + (ff_s_blrr_initial_exact_count_sum))) /\ ff_s_blrr_initial_exact_count_sum = ff_r_blrr_initial_exact_count_sum + ff_a_blrr_initial_exact_count_sum)))))) /\ (forall ff_i_blrr_initial_exact_count_bits. (exists ff_lt_blrr_initial_exact_count_bits_bound. ff_lt_blrr_initial_exact_count_bits_bound + S ff_i_blrr_initial_exact_count_bits = k) -> exists ff_bit_blrr_initial_exact_count_bits. ((((exists ff_h_blrr_initial_exact_count_bits_decoded. ff_h_blrr_initial_exact_count_bits_decoded + S (ff_bit_blrr_initial_exact_count_bits) = S ((S (ff_i_blrr_initial_exact_count_bits)) * x1)) /\ exists ff_q_blrr_initial_exact_count_bits_decoded. x = ff_q_blrr_initial_exact_count_bits_decoded * S ((S (ff_i_blrr_initial_exact_count_bits)) * x1) + (ff_bit_blrr_initial_exact_count_bits))) /\ (ff_bit_blrr_initial_exact_count_bits = 0 \/ ff_bit_blrr_initial_exact_count_bits = 1))))
  11. 0011specialize eisenstein_initial_segment_bit_count_exact q
  12. 0012specialize eisenstein_initial_segment_bit_count_exact x
  13. 0013specialize eisenstein_initial_segment_bit_count_exact x1
  14. 0014specialize eisenstein_initial_segment_bit_count_exact k
  15. 0015apply eisenstein_initial_segment_bit_count_exact
  16. 0016exact hprefix_witness_witness
  17. 0017exact hbound
  18. 0018cases hcount
  19. 0019exists x
  20. 0020exists x1
  21. 0021split
  22. 0022exact hprefix_witness_witness
  23. 0023exact hcount_left