PA00DY

eisenstein_initial_segment_bit_count_exact

Alpha v16 checked-use theorem · independently closed; not Stable

A bounded exact initial-segment prefix has native BitCount q.

Exact expanded PA statement

forall q b c k. (forall eis_index_initial_segment_count_result_prefix. (exists eis_lt_gap_initial_segment_count_result_prefix_bound. eis_lt_gap_initial_segment_count_result_prefix_bound + S (eis_index_initial_segment_count_result_prefix) = k) -> exists eis_bit_initial_segment_count_result_prefix. ((((exists ff_h_eis_initial_segment_count_result_prefix_decoded. ff_h_eis_initial_segment_count_result_prefix_decoded + S (eis_bit_initial_segment_count_result_prefix) = S ((S (eis_index_initial_segment_count_result_prefix)) * c)) /\ exists ff_q_eis_initial_segment_count_result_prefix_decoded. b = ff_q_eis_initial_segment_count_result_prefix_decoded * S ((S (eis_index_initial_segment_count_result_prefix)) * c) + (eis_bit_initial_segment_count_result_prefix))) /\ (((eis_bit_initial_segment_count_result_prefix = 1 /\ (exists eis_le_gap_initial_segment_count_result_prefix_choice_inside. eis_le_gap_initial_segment_count_result_prefix_choice_inside + (S eis_index_initial_segment_count_result_prefix) = q)) \/ (eis_bit_initial_segment_count_result_prefix = 0 /\ (exists eis_lt_gap_initial_segment_count_result_prefix_choice_outside. eis_lt_gap_initial_segment_count_result_prefix_choice_outside + S (q) = S eis_index_initial_segment_count_result_prefix)))))) -> (exists eis_le_gap_initial_segment_count_result_bound. eis_le_gap_initial_segment_count_result_bound + (q) = k) -> (((exists ff_u_initial_segment_count_result_sum ff_v_initial_segment_count_result_sum. ((((exists ff_h_initial_segment_count_result_sum_start. ff_h_initial_segment_count_result_sum_start + S (0) = S ((S (0)) * ff_v_initial_segment_count_result_sum)) /\ exists ff_q_initial_segment_count_result_sum_start. ff_u_initial_segment_count_result_sum = ff_q_initial_segment_count_result_sum_start * S ((S (0)) * ff_v_initial_segment_count_result_sum) + (0))) /\ ((((exists ff_h_initial_segment_count_result_sum_terminal. ff_h_initial_segment_count_result_sum_terminal + S (q) = S ((S (k)) * ff_v_initial_segment_count_result_sum)) /\ exists ff_q_initial_segment_count_result_sum_terminal. ff_u_initial_segment_count_result_sum = ff_q_initial_segment_count_result_sum_terminal * S ((S (k)) * ff_v_initial_segment_count_result_sum) + (q))) /\ forall ff_i_initial_segment_count_result_sum. (exists ff_lt_initial_segment_count_result_sum_bound. ff_lt_initial_segment_count_result_sum_bound + S ff_i_initial_segment_count_result_sum = k) -> exists ff_a_initial_segment_count_result_sum ff_r_initial_segment_count_result_sum ff_s_initial_segment_count_result_sum. ((((exists ff_h_initial_segment_count_result_sum_summand. ff_h_initial_segment_count_result_sum_summand + S (ff_a_initial_segment_count_result_sum) = S ((S (ff_i_initial_segment_count_result_sum)) * c)) /\ exists ff_q_initial_segment_count_result_sum_summand. b = ff_q_initial_segment_count_result_sum_summand * S ((S (ff_i_initial_segment_count_result_sum)) * c) + (ff_a_initial_segment_count_result_sum))) /\ ((((exists ff_h_initial_segment_count_result_sum_partial. ff_h_initial_segment_count_result_sum_partial + S (ff_r_initial_segment_count_result_sum) = S ((S (ff_i_initial_segment_count_result_sum)) * ff_v_initial_segment_count_result_sum)) /\ exists ff_q_initial_segment_count_result_sum_partial. ff_u_initial_segment_count_result_sum = ff_q_initial_segment_count_result_sum_partial * S ((S (ff_i_initial_segment_count_result_sum)) * ff_v_initial_segment_count_result_sum) + (ff_r_initial_segment_count_result_sum))) /\ ((((exists ff_h_initial_segment_count_result_sum_successor. ff_h_initial_segment_count_result_sum_successor + S (ff_s_initial_segment_count_result_sum) = S ((S (S ff_i_initial_segment_count_result_sum)) * ff_v_initial_segment_count_result_sum)) /\ exists ff_q_initial_segment_count_result_sum_successor. ff_u_initial_segment_count_result_sum = ff_q_initial_segment_count_result_sum_successor * S ((S (S ff_i_initial_segment_count_result_sum)) * ff_v_initial_segment_count_result_sum) + (ff_s_initial_segment_count_result_sum))) /\ ff_s_initial_segment_count_result_sum = ff_r_initial_segment_count_result_sum + ff_a_initial_segment_count_result_sum)))))) /\ (forall ff_i_initial_segment_count_result_bits. (exists ff_lt_initial_segment_count_result_bits_bound. ff_lt_initial_segment_count_result_bits_bound + S ff_i_initial_segment_count_result_bits = k) -> exists ff_bit_initial_segment_count_result_bits. ((((exists ff_h_initial_segment_count_result_bits_decoded. ff_h_initial_segment_count_result_bits_decoded + S (ff_bit_initial_segment_count_result_bits) = S ((S (ff_i_initial_segment_count_result_bits)) * c)) /\ exists ff_q_initial_segment_count_result_bits_decoded. b = ff_q_initial_segment_count_result_bits_decoded * S ((S (ff_i_initial_segment_count_result_bits)) * c) + (ff_bit_initial_segment_count_result_bits))) /\ (ff_bit_initial_segment_count_result_bits = 0 \/ ff_bit_initial_segment_count_result_bits = 1)))))

Structural proof guide

Generated structural guide

A bounded exact initial-segment prefix has native BitCount q.

Use the direct prerequisites eisenstein_initial_segment_prefix_all_bits, bit_count_exists, eisenstein_initial_segment_bit_count_functional as previously established PA formulas.

The proof proceeds by case analysis (1), intermediate claims (3), equality transport (2).

Referenced ingredients

PA00DU eisenstein_initial_segment_prefix_all_bits PA003I bit_count_exists PA00DX eisenstein_initial_segment_bit_count_functional

Proof neighborhood

Direct dependencies

PA00DU eisenstein_initial_segment_prefix_all_bits PA003I bit_count_exists PA00DX eisenstein_initial_segment_bit_count_functional

Direct dependents

PA00E0 distinct_odd_prime_row_bit_count_equals_division_quotient

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  1. 0001intro q
  2. 0002intro b
  3. 0003intro c
  4. 0004intro k
  5. 0005intro hprefix
  6. 0006intro hqk
  7. 0007have hallbits : forall ff_i_initial_segment_exact_all_bits. (exists ff_lt_initial_segment_exact_all_bits_bound. ff_lt_initial_segment_exact_all_bits_bound + S ff_i_initial_segment_exact_all_bits = k) -> exists ff_bit_initial_segment_exact_all_bits. ((((exists ff_h_initial_segment_exact_all_bits_decoded. ff_h_initial_segment_exact_all_bits_decoded + S (ff_bit_initial_segment_exact_all_bits) = S ((S (ff_i_initial_segment_exact_all_bits)) * c)) /\ exists ff_q_initial_segment_exact_all_bits_decoded. b = ff_q_initial_segment_exact_all_bits_decoded * S ((S (ff_i_initial_segment_exact_all_bits)) * c) + (ff_bit_initial_segment_exact_all_bits))) /\ (ff_bit_initial_segment_exact_all_bits = 0 \/ ff_bit_initial_segment_exact_all_bits = 1))
  8. 0008specialize eisenstein_initial_segment_prefix_all_bits q
  9. 0009specialize eisenstein_initial_segment_prefix_all_bits b
  10. 0010specialize eisenstein_initial_segment_prefix_all_bits c
  11. 0011specialize eisenstein_initial_segment_prefix_all_bits k
  12. 0012apply eisenstein_initial_segment_prefix_all_bits
  13. 0013exact hprefix
  14. 0014have hcount : exists n. ((exists ff_u_initial_segment_exact_exists_sum ff_v_initial_segment_exact_exists_sum. ((((exists ff_h_initial_segment_exact_exists_sum_start. ff_h_initial_segment_exact_exists_sum_start + S (0) = S ((S (0)) * ff_v_initial_segment_exact_exists_sum)) /\ exists ff_q_initial_segment_exact_exists_sum_start. ff_u_initial_segment_exact_exists_sum = ff_q_initial_segment_exact_exists_sum_start * S ((S (0)) * ff_v_initial_segment_exact_exists_sum) + (0))) /\ ((((exists ff_h_initial_segment_exact_exists_sum_terminal. ff_h_initial_segment_exact_exists_sum_terminal + S (n) = S ((S (k)) * ff_v_initial_segment_exact_exists_sum)) /\ exists ff_q_initial_segment_exact_exists_sum_terminal. ff_u_initial_segment_exact_exists_sum = ff_q_initial_segment_exact_exists_sum_terminal * S ((S (k)) * ff_v_initial_segment_exact_exists_sum) + (n))) /\ forall ff_i_initial_segment_exact_exists_sum. (exists ff_lt_initial_segment_exact_exists_sum_bound. ff_lt_initial_segment_exact_exists_sum_bound + S ff_i_initial_segment_exact_exists_sum = k) -> exists ff_a_initial_segment_exact_exists_sum ff_r_initial_segment_exact_exists_sum ff_s_initial_segment_exact_exists_sum. ((((exists ff_h_initial_segment_exact_exists_sum_summand. ff_h_initial_segment_exact_exists_sum_summand + S (ff_a_initial_segment_exact_exists_sum) = S ((S (ff_i_initial_segment_exact_exists_sum)) * c)) /\ exists ff_q_initial_segment_exact_exists_sum_summand. b = ff_q_initial_segment_exact_exists_sum_summand * S ((S (ff_i_initial_segment_exact_exists_sum)) * c) + (ff_a_initial_segment_exact_exists_sum))) /\ ((((exists ff_h_initial_segment_exact_exists_sum_partial. ff_h_initial_segment_exact_exists_sum_partial + S (ff_r_initial_segment_exact_exists_sum) = S ((S (ff_i_initial_segment_exact_exists_sum)) * ff_v_initial_segment_exact_exists_sum)) /\ exists ff_q_initial_segment_exact_exists_sum_partial. ff_u_initial_segment_exact_exists_sum = ff_q_initial_segment_exact_exists_sum_partial * S ((S (ff_i_initial_segment_exact_exists_sum)) * ff_v_initial_segment_exact_exists_sum) + (ff_r_initial_segment_exact_exists_sum))) /\ ((((exists ff_h_initial_segment_exact_exists_sum_successor. ff_h_initial_segment_exact_exists_sum_successor + S (ff_s_initial_segment_exact_exists_sum) = S ((S (S ff_i_initial_segment_exact_exists_sum)) * ff_v_initial_segment_exact_exists_sum)) /\ exists ff_q_initial_segment_exact_exists_sum_successor. ff_u_initial_segment_exact_exists_sum = ff_q_initial_segment_exact_exists_sum_successor * S ((S (S ff_i_initial_segment_exact_exists_sum)) * ff_v_initial_segment_exact_exists_sum) + (ff_s_initial_segment_exact_exists_sum))) /\ ff_s_initial_segment_exact_exists_sum = ff_r_initial_segment_exact_exists_sum + ff_a_initial_segment_exact_exists_sum)))))) /\ (forall ff_i_initial_segment_exact_exists_bits. (exists ff_lt_initial_segment_exact_exists_bits_bound. ff_lt_initial_segment_exact_exists_bits_bound + S ff_i_initial_segment_exact_exists_bits = k) -> exists ff_bit_initial_segment_exact_exists_bits. ((((exists ff_h_initial_segment_exact_exists_bits_decoded. ff_h_initial_segment_exact_exists_bits_decoded + S (ff_bit_initial_segment_exact_exists_bits) = S ((S (ff_i_initial_segment_exact_exists_bits)) * c)) /\ exists ff_q_initial_segment_exact_exists_bits_decoded. b = ff_q_initial_segment_exact_exists_bits_decoded * S ((S (ff_i_initial_segment_exact_exists_bits)) * c) + (ff_bit_initial_segment_exact_exists_bits))) /\ (ff_bit_initial_segment_exact_exists_bits = 0 \/ ff_bit_initial_segment_exact_exists_bits = 1))))
  15. 0015specialize bit_count_exists b
  16. 0016specialize bit_count_exists c
  17. 0017specialize bit_count_exists k
  18. 0018apply bit_count_exists
  19. 0019exact hallbits
  20. 0020cases hcount
  21. 0021have hnq : x = q
  22. 0022specialize eisenstein_initial_segment_bit_count_functional q
  23. 0023specialize eisenstein_initial_segment_bit_count_functional b
  24. 0024specialize eisenstein_initial_segment_bit_count_functional c
  25. 0025specialize eisenstein_initial_segment_bit_count_functional k
  26. 0026specialize eisenstein_initial_segment_bit_count_functional x
  27. 0027apply eisenstein_initial_segment_bit_count_functional
  28. 0028exact hprefix
  29. 0029exact hqk
  30. 0030exact hcount_witness
  31. 0031rewrite hnq at hcount_witness
  32. 0032rewrite hnq at hcount_witness
  33. 0033exact hcount_witness