PA00DF

distinct_odd_prime_half_row_count_exists

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

Every fixed half-rectangle row has an exact beta-coded indicator and BitCount witness.

Exact expanded PA statement

forall p q h k i. p = 2 * h + 1 -> q = 2 * k + 1 -> ((~(p = 1) /\ forall frp_prime_left_row_indicator_prime_p frp_prime_right_row_indicator_prime_p. p = frp_prime_left_row_indicator_prime_p * frp_prime_right_row_indicator_prime_p -> frp_prime_left_row_indicator_prime_p = 1 \/ frp_prime_right_row_indicator_prime_p = 1)) -> ((~(q = 1) /\ forall frp_prime_left_row_indicator_prime_q frp_prime_right_row_indicator_prime_q. q = frp_prime_left_row_indicator_prime_q * frp_prime_right_row_indicator_prime_q -> frp_prime_left_row_indicator_prime_q = 1 \/ frp_prime_right_row_indicator_prime_q = 1)) -> ~(p = q) -> (exists eri_gap_row_indicator_i_bound. eri_gap_row_indicator_i_bound + S (i) = h) -> (exists rb rc n. ((forall eri_column_row_indicator_counted_prefix. (exists eri_gap_row_indicator_counted_prefix_bound. eri_gap_row_indicator_counted_prefix_bound + S (eri_column_row_indicator_counted_prefix) = k) -> exists eri_bit_row_indicator_counted_prefix. ((((exists ff_h_eri_row_indicator_counted_prefix_decoded. ff_h_eri_row_indicator_counted_prefix_decoded + S (eri_bit_row_indicator_counted_prefix) = S ((S (eri_column_row_indicator_counted_prefix)) * rc)) /\ exists ff_q_eri_row_indicator_counted_prefix_decoded. rb = ff_q_eri_row_indicator_counted_prefix_decoded * S ((S (eri_column_row_indicator_counted_prefix)) * rc) + (eri_bit_row_indicator_counted_prefix))) /\ (((eri_bit_row_indicator_counted_prefix = 0 /\ ((exists eri_gap_row_indicator_counted_prefix_choice_left. eri_gap_row_indicator_counted_prefix_choice_left + S (q * S i) = p * S eri_column_row_indicator_counted_prefix) /\ ~(exists eri_gap_row_indicator_counted_prefix_choice_right. eri_gap_row_indicator_counted_prefix_choice_right + S (p * S eri_column_row_indicator_counted_prefix) = q * S i))) \/ (eri_bit_row_indicator_counted_prefix = 1 /\ ((exists eri_gap_row_indicator_counted_prefix_choice_right. eri_gap_row_indicator_counted_prefix_choice_right + S (p * S eri_column_row_indicator_counted_prefix) = q * S i) /\ ~(exists eri_gap_row_indicator_counted_prefix_choice_left. eri_gap_row_indicator_counted_prefix_choice_left + S (q * S i) = p * S eri_column_row_indicator_counted_prefix))))))) /\ (((exists ff_u_row_indicator_count_relation_sum ff_v_row_indicator_count_relation_sum. ((((exists ff_h_row_indicator_count_relation_sum_start. ff_h_row_indicator_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_row_indicator_count_relation_sum)) /\ exists ff_q_row_indicator_count_relation_sum_start. ff_u_row_indicator_count_relation_sum = ff_q_row_indicator_count_relation_sum_start * S ((S (0)) * ff_v_row_indicator_count_relation_sum) + (0))) /\ ((((exists ff_h_row_indicator_count_relation_sum_terminal. ff_h_row_indicator_count_relation_sum_terminal + S (n) = S ((S (k)) * ff_v_row_indicator_count_relation_sum)) /\ exists ff_q_row_indicator_count_relation_sum_terminal. ff_u_row_indicator_count_relation_sum = ff_q_row_indicator_count_relation_sum_terminal * S ((S (k)) * ff_v_row_indicator_count_relation_sum) + (n))) /\ forall ff_i_row_indicator_count_relation_sum. (exists ff_lt_row_indicator_count_relation_sum_bound. ff_lt_row_indicator_count_relation_sum_bound + S ff_i_row_indicator_count_relation_sum = k) -> exists ff_a_row_indicator_count_relation_sum ff_r_row_indicator_count_relation_sum ff_s_row_indicator_count_relation_sum. ((((exists ff_h_row_indicator_count_relation_sum_summand. ff_h_row_indicator_count_relation_sum_summand + S (ff_a_row_indicator_count_relation_sum) = S ((S (ff_i_row_indicator_count_relation_sum)) * rc)) /\ exists ff_q_row_indicator_count_relation_sum_summand. rb = ff_q_row_indicator_count_relation_sum_summand * S ((S (ff_i_row_indicator_count_relation_sum)) * rc) + (ff_a_row_indicator_count_relation_sum))) /\ ((((exists ff_h_row_indicator_count_relation_sum_partial. ff_h_row_indicator_count_relation_sum_partial + S (ff_r_row_indicator_count_relation_sum) = S ((S (ff_i_row_indicator_count_relation_sum)) * ff_v_row_indicator_count_relation_sum)) /\ exists ff_q_row_indicator_count_relation_sum_partial. ff_u_row_indicator_count_relation_sum = ff_q_row_indicator_count_relation_sum_partial * S ((S (ff_i_row_indicator_count_relation_sum)) * ff_v_row_indicator_count_relation_sum) + (ff_r_row_indicator_count_relation_sum))) /\ ((((exists ff_h_row_indicator_count_relation_sum_successor. ff_h_row_indicator_count_relation_sum_successor + S (ff_s_row_indicator_count_relation_sum) = S ((S (S ff_i_row_indicator_count_relation_sum)) * ff_v_row_indicator_count_relation_sum)) /\ exists ff_q_row_indicator_count_relation_sum_successor. ff_u_row_indicator_count_relation_sum = ff_q_row_indicator_count_relation_sum_successor * S ((S (S ff_i_row_indicator_count_relation_sum)) * ff_v_row_indicator_count_relation_sum) + (ff_s_row_indicator_count_relation_sum))) /\ ff_s_row_indicator_count_relation_sum = ff_r_row_indicator_count_relation_sum + ff_a_row_indicator_count_relation_sum)))))) /\ (forall ff_i_row_indicator_count_relation_bits. (exists ff_lt_row_indicator_count_relation_bits_bound. ff_lt_row_indicator_count_relation_bits_bound + S ff_i_row_indicator_count_relation_bits = k) -> exists ff_bit_row_indicator_count_relation_bits. ((((exists ff_h_row_indicator_count_relation_bits_decoded. ff_h_row_indicator_count_relation_bits_decoded + S (ff_bit_row_indicator_count_relation_bits) = S ((S (ff_i_row_indicator_count_relation_bits)) * rc)) /\ exists ff_q_row_indicator_count_relation_bits_decoded. rb = ff_q_row_indicator_count_relation_bits_decoded * S ((S (ff_i_row_indicator_count_relation_bits)) * rc) + (ff_bit_row_indicator_count_relation_bits))) /\ (ff_bit_row_indicator_count_relation_bits = 0 \/ ff_bit_row_indicator_count_relation_bits = 1)))))))

Structural proof guide

Generated structural guide

Every fixed half-rectangle row has an exact beta-coded indicator and BitCount witness.

Use the direct prerequisites distinct_odd_prime_half_row_indicator_choices, eisenstein_row_indicator_prefix_exists, eisenstein_row_indicator_prefix_all_bits, bit_count_exists as previously established PA formulas.

The proof proceeds by case analysis (3), intermediate claims (4).

Referenced ingredients

PA00DB distinct_odd_prime_half_row_indicator_choices PA00DD eisenstein_row_indicator_prefix_exists PA00DE eisenstein_row_indicator_prefix_all_bits PA003I bit_count_exists

Proof neighborhood

Direct dependencies

PA00DB distinct_odd_prime_half_row_indicator_choices PA00DD eisenstein_row_indicator_prefix_exists PA00DE eisenstein_row_indicator_prefix_all_bits PA003I bit_count_exists

Direct dependents

PA00DG distinct_odd_prime_half_row_count_choice

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 p
  2. 0002intro q
  3. 0003intro h
  4. 0004intro k
  5. 0005intro i
  6. 0006intro hpodd
  7. 0007intro hqodd
  8. 0008intro hp
  9. 0009intro hq
  10. 0010intro hpq
  11. 0011intro hi
  12. 0012have hchoices : forall eri_column_row_indicator_concrete_choices. (exists eri_gap_row_indicator_concrete_choices_bound. eri_gap_row_indicator_concrete_choices_bound + S (eri_column_row_indicator_concrete_choices) = k) -> exists eri_bit_row_indicator_concrete_choices. (((eri_bit_row_indicator_concrete_choices = 0 /\ ((exists eri_gap_row_indicator_concrete_choices_choice_left. eri_gap_row_indicator_concrete_choices_choice_left + S (q * S i) = p * S eri_column_row_indicator_concrete_choices) /\ ~(exists eri_gap_row_indicator_concrete_choices_choice_right. eri_gap_row_indicator_concrete_choices_choice_right + S (p * S eri_column_row_indicator_concrete_choices) = q * S i))) \/ (eri_bit_row_indicator_concrete_choices = 1 /\ ((exists eri_gap_row_indicator_concrete_choices_choice_right. eri_gap_row_indicator_concrete_choices_choice_right + S (p * S eri_column_row_indicator_concrete_choices) = q * S i) /\ ~(exists eri_gap_row_indicator_concrete_choices_choice_left. eri_gap_row_indicator_concrete_choices_choice_left + S (q * S i) = p * S eri_column_row_indicator_concrete_choices)))))
  13. 0013specialize distinct_odd_prime_half_row_indicator_choices p
  14. 0014specialize distinct_odd_prime_half_row_indicator_choices q
  15. 0015specialize distinct_odd_prime_half_row_indicator_choices h
  16. 0016specialize distinct_odd_prime_half_row_indicator_choices k
  17. 0017specialize distinct_odd_prime_half_row_indicator_choices i
  18. 0018apply distinct_odd_prime_half_row_indicator_choices
  19. 0019exact hpodd
  20. 0020exact hqodd
  21. 0021exact hp
  22. 0022exact hq
  23. 0023exact hpq
  24. 0024exact hi
  25. 0025have hprefix_exists : exists rb rc. (forall eri_column_row_indicator_concrete_prefix. (exists eri_gap_row_indicator_concrete_prefix_bound. eri_gap_row_indicator_concrete_prefix_bound + S (eri_column_row_indicator_concrete_prefix) = k) -> exists eri_bit_row_indicator_concrete_prefix. ((((exists ff_h_eri_row_indicator_concrete_prefix_decoded. ff_h_eri_row_indicator_concrete_prefix_decoded + S (eri_bit_row_indicator_concrete_prefix) = S ((S (eri_column_row_indicator_concrete_prefix)) * rc)) /\ exists ff_q_eri_row_indicator_concrete_prefix_decoded. rb = ff_q_eri_row_indicator_concrete_prefix_decoded * S ((S (eri_column_row_indicator_concrete_prefix)) * rc) + (eri_bit_row_indicator_concrete_prefix))) /\ (((eri_bit_row_indicator_concrete_prefix = 0 /\ ((exists eri_gap_row_indicator_concrete_prefix_choice_left. eri_gap_row_indicator_concrete_prefix_choice_left + S (q * S i) = p * S eri_column_row_indicator_concrete_prefix) /\ ~(exists eri_gap_row_indicator_concrete_prefix_choice_right. eri_gap_row_indicator_concrete_prefix_choice_right + S (p * S eri_column_row_indicator_concrete_prefix) = q * S i))) \/ (eri_bit_row_indicator_concrete_prefix = 1 /\ ((exists eri_gap_row_indicator_concrete_prefix_choice_right. eri_gap_row_indicator_concrete_prefix_choice_right + S (p * S eri_column_row_indicator_concrete_prefix) = q * S i) /\ ~(exists eri_gap_row_indicator_concrete_prefix_choice_left. eri_gap_row_indicator_concrete_prefix_choice_left + S (q * S i) = p * S eri_column_row_indicator_concrete_prefix)))))))
  26. 0026specialize eisenstein_row_indicator_prefix_exists p
  27. 0027specialize eisenstein_row_indicator_prefix_exists q
  28. 0028specialize eisenstein_row_indicator_prefix_exists i
  29. 0029specialize eisenstein_row_indicator_prefix_exists k
  30. 0030apply eisenstein_row_indicator_prefix_exists
  31. 0031exact hchoices
  32. 0032cases hprefix_exists
  33. 0033cases hprefix_exists_witness
  34. 0034have hbits : forall ff_i_row_indicator_counted_witness_bits. (exists ff_lt_row_indicator_counted_witness_bits_bound. ff_lt_row_indicator_counted_witness_bits_bound + S ff_i_row_indicator_counted_witness_bits = k) -> exists ff_bit_row_indicator_counted_witness_bits. ((((exists ff_h_row_indicator_counted_witness_bits_decoded. ff_h_row_indicator_counted_witness_bits_decoded + S (ff_bit_row_indicator_counted_witness_bits) = S ((S (ff_i_row_indicator_counted_witness_bits)) * x1)) /\ exists ff_q_row_indicator_counted_witness_bits_decoded. x = ff_q_row_indicator_counted_witness_bits_decoded * S ((S (ff_i_row_indicator_counted_witness_bits)) * x1) + (ff_bit_row_indicator_counted_witness_bits))) /\ (ff_bit_row_indicator_counted_witness_bits = 0 \/ ff_bit_row_indicator_counted_witness_bits = 1))
  35. 0035specialize eisenstein_row_indicator_prefix_all_bits p
  36. 0036specialize eisenstein_row_indicator_prefix_all_bits q
  37. 0037specialize eisenstein_row_indicator_prefix_all_bits i
  38. 0038specialize eisenstein_row_indicator_prefix_all_bits x
  39. 0039specialize eisenstein_row_indicator_prefix_all_bits x1
  40. 0040specialize eisenstein_row_indicator_prefix_all_bits k
  41. 0041apply eisenstein_row_indicator_prefix_all_bits
  42. 0042exact hprefix_exists_witness_witness
  43. 0043have hcount : exists n. (((exists ff_u_row_indicator_counted_witness_count_sum ff_v_row_indicator_counted_witness_count_sum. ((((exists ff_h_row_indicator_counted_witness_count_sum_start. ff_h_row_indicator_counted_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_row_indicator_counted_witness_count_sum)) /\ exists ff_q_row_indicator_counted_witness_count_sum_start. ff_u_row_indicator_counted_witness_count_sum = ff_q_row_indicator_counted_witness_count_sum_start * S ((S (0)) * ff_v_row_indicator_counted_witness_count_sum) + (0))) /\ ((((exists ff_h_row_indicator_counted_witness_count_sum_terminal. ff_h_row_indicator_counted_witness_count_sum_terminal + S (n) = S ((S (k)) * ff_v_row_indicator_counted_witness_count_sum)) /\ exists ff_q_row_indicator_counted_witness_count_sum_terminal. ff_u_row_indicator_counted_witness_count_sum = ff_q_row_indicator_counted_witness_count_sum_terminal * S ((S (k)) * ff_v_row_indicator_counted_witness_count_sum) + (n))) /\ forall ff_i_row_indicator_counted_witness_count_sum. (exists ff_lt_row_indicator_counted_witness_count_sum_bound. ff_lt_row_indicator_counted_witness_count_sum_bound + S ff_i_row_indicator_counted_witness_count_sum = k) -> exists ff_a_row_indicator_counted_witness_count_sum ff_r_row_indicator_counted_witness_count_sum ff_s_row_indicator_counted_witness_count_sum. ((((exists ff_h_row_indicator_counted_witness_count_sum_summand. ff_h_row_indicator_counted_witness_count_sum_summand + S (ff_a_row_indicator_counted_witness_count_sum) = S ((S (ff_i_row_indicator_counted_witness_count_sum)) * x1)) /\ exists ff_q_row_indicator_counted_witness_count_sum_summand. x = ff_q_row_indicator_counted_witness_count_sum_summand * S ((S (ff_i_row_indicator_counted_witness_count_sum)) * x1) + (ff_a_row_indicator_counted_witness_count_sum))) /\ ((((exists ff_h_row_indicator_counted_witness_count_sum_partial. ff_h_row_indicator_counted_witness_count_sum_partial + S (ff_r_row_indicator_counted_witness_count_sum) = S ((S (ff_i_row_indicator_counted_witness_count_sum)) * ff_v_row_indicator_counted_witness_count_sum)) /\ exists ff_q_row_indicator_counted_witness_count_sum_partial. ff_u_row_indicator_counted_witness_count_sum = ff_q_row_indicator_counted_witness_count_sum_partial * S ((S (ff_i_row_indicator_counted_witness_count_sum)) * ff_v_row_indicator_counted_witness_count_sum) + (ff_r_row_indicator_counted_witness_count_sum))) /\ ((((exists ff_h_row_indicator_counted_witness_count_sum_successor. ff_h_row_indicator_counted_witness_count_sum_successor + S (ff_s_row_indicator_counted_witness_count_sum) = S ((S (S ff_i_row_indicator_counted_witness_count_sum)) * ff_v_row_indicator_counted_witness_count_sum)) /\ exists ff_q_row_indicator_counted_witness_count_sum_successor. ff_u_row_indicator_counted_witness_count_sum = ff_q_row_indicator_counted_witness_count_sum_successor * S ((S (S ff_i_row_indicator_counted_witness_count_sum)) * ff_v_row_indicator_counted_witness_count_sum) + (ff_s_row_indicator_counted_witness_count_sum))) /\ ff_s_row_indicator_counted_witness_count_sum = ff_r_row_indicator_counted_witness_count_sum + ff_a_row_indicator_counted_witness_count_sum)))))) /\ (forall ff_i_row_indicator_counted_witness_count_bits. (exists ff_lt_row_indicator_counted_witness_count_bits_bound. ff_lt_row_indicator_counted_witness_count_bits_bound + S ff_i_row_indicator_counted_witness_count_bits = k) -> exists ff_bit_row_indicator_counted_witness_count_bits. ((((exists ff_h_row_indicator_counted_witness_count_bits_decoded. ff_h_row_indicator_counted_witness_count_bits_decoded + S (ff_bit_row_indicator_counted_witness_count_bits) = S ((S (ff_i_row_indicator_counted_witness_count_bits)) * x1)) /\ exists ff_q_row_indicator_counted_witness_count_bits_decoded. x = ff_q_row_indicator_counted_witness_count_bits_decoded * S ((S (ff_i_row_indicator_counted_witness_count_bits)) * x1) + (ff_bit_row_indicator_counted_witness_count_bits))) /\ (ff_bit_row_indicator_counted_witness_count_bits = 0 \/ ff_bit_row_indicator_counted_witness_count_bits = 1)))))
  44. 0044specialize bit_count_exists x
  45. 0045specialize bit_count_exists x1
  46. 0046specialize bit_count_exists k
  47. 0047apply bit_count_exists
  48. 0048exact hbits
  49. 0049cases hcount
  50. 0050exists x
  51. 0051exists x1
  52. 0052exists x2
  53. 0053split
  54. 0054exact hprefix_exists_witness_witness
  55. 0055exact hcount_witness