BT00JD

eisenstein_initial_segment_bit_count_functional

Alpha body-checked · checked-use disabled

The BitCount of a bounded exact initial segment is its threshold.

Exact expanded PA statement

forall q b c k n. (forall eis_index_initial_segment_exact_source. (exists eis_lt_gap_initial_segment_exact_source_bound. eis_lt_gap_initial_segment_exact_source_bound + S (eis_index_initial_segment_exact_source) = k) -> exists eis_bit_initial_segment_exact_source. ((((exists ff_h_eis_initial_segment_exact_source_decoded. ff_h_eis_initial_segment_exact_source_decoded + S (eis_bit_initial_segment_exact_source) = S ((S (eis_index_initial_segment_exact_source)) * c)) /\ exists ff_q_eis_initial_segment_exact_source_decoded. b = ff_q_eis_initial_segment_exact_source_decoded * S ((S (eis_index_initial_segment_exact_source)) * c) + (eis_bit_initial_segment_exact_source))) /\ (((eis_bit_initial_segment_exact_source = 1 /\ (exists eis_le_gap_initial_segment_exact_source_choice_inside. eis_le_gap_initial_segment_exact_source_choice_inside + (S eis_index_initial_segment_exact_source) = q)) \/ (eis_bit_initial_segment_exact_source = 0 /\ (exists eis_lt_gap_initial_segment_exact_source_choice_outside. eis_lt_gap_initial_segment_exact_source_choice_outside + S (q) = S eis_index_initial_segment_exact_source)))))) -> (exists eis_le_gap_initial_segment_exact_threshold. eis_le_gap_initial_segment_exact_threshold + (q) = k) -> (((exists ff_u_initial_segment_exact_count_sum ff_v_initial_segment_exact_count_sum. ((((exists ff_h_initial_segment_exact_count_sum_start. ff_h_initial_segment_exact_count_sum_start + S (0) = S ((S (0)) * ff_v_initial_segment_exact_count_sum)) /\ exists ff_q_initial_segment_exact_count_sum_start. ff_u_initial_segment_exact_count_sum = ff_q_initial_segment_exact_count_sum_start * S ((S (0)) * ff_v_initial_segment_exact_count_sum) + (0))) /\ ((((exists ff_h_initial_segment_exact_count_sum_terminal. ff_h_initial_segment_exact_count_sum_terminal + S (n) = S ((S (k)) * ff_v_initial_segment_exact_count_sum)) /\ exists ff_q_initial_segment_exact_count_sum_terminal. ff_u_initial_segment_exact_count_sum = ff_q_initial_segment_exact_count_sum_terminal * S ((S (k)) * ff_v_initial_segment_exact_count_sum) + (n))) /\ forall ff_i_initial_segment_exact_count_sum. (exists ff_lt_initial_segment_exact_count_sum_bound. ff_lt_initial_segment_exact_count_sum_bound + S ff_i_initial_segment_exact_count_sum = k) -> exists ff_a_initial_segment_exact_count_sum ff_r_initial_segment_exact_count_sum ff_s_initial_segment_exact_count_sum. ((((exists ff_h_initial_segment_exact_count_sum_summand. ff_h_initial_segment_exact_count_sum_summand + S (ff_a_initial_segment_exact_count_sum) = S ((S (ff_i_initial_segment_exact_count_sum)) * c)) /\ exists ff_q_initial_segment_exact_count_sum_summand. b = ff_q_initial_segment_exact_count_sum_summand * S ((S (ff_i_initial_segment_exact_count_sum)) * c) + (ff_a_initial_segment_exact_count_sum))) /\ ((((exists ff_h_initial_segment_exact_count_sum_partial. ff_h_initial_segment_exact_count_sum_partial + S (ff_r_initial_segment_exact_count_sum) = S ((S (ff_i_initial_segment_exact_count_sum)) * ff_v_initial_segment_exact_count_sum)) /\ exists ff_q_initial_segment_exact_count_sum_partial. ff_u_initial_segment_exact_count_sum = ff_q_initial_segment_exact_count_sum_partial * S ((S (ff_i_initial_segment_exact_count_sum)) * ff_v_initial_segment_exact_count_sum) + (ff_r_initial_segment_exact_count_sum))) /\ ((((exists ff_h_initial_segment_exact_count_sum_successor. ff_h_initial_segment_exact_count_sum_successor + S (ff_s_initial_segment_exact_count_sum) = S ((S (S ff_i_initial_segment_exact_count_sum)) * ff_v_initial_segment_exact_count_sum)) /\ exists ff_q_initial_segment_exact_count_sum_successor. ff_u_initial_segment_exact_count_sum = ff_q_initial_segment_exact_count_sum_successor * S ((S (S ff_i_initial_segment_exact_count_sum)) * ff_v_initial_segment_exact_count_sum) + (ff_s_initial_segment_exact_count_sum))) /\ ff_s_initial_segment_exact_count_sum = ff_r_initial_segment_exact_count_sum + ff_a_initial_segment_exact_count_sum)))))) /\ (forall ff_i_initial_segment_exact_count_bits. (exists ff_lt_initial_segment_exact_count_bits_bound. ff_lt_initial_segment_exact_count_bits_bound + S ff_i_initial_segment_exact_count_bits = k) -> exists ff_bit_initial_segment_exact_count_bits. ((((exists ff_h_initial_segment_exact_count_bits_decoded. ff_h_initial_segment_exact_count_bits_decoded + S (ff_bit_initial_segment_exact_count_bits) = S ((S (ff_i_initial_segment_exact_count_bits)) * c)) /\ exists ff_q_initial_segment_exact_count_bits_decoded. b = ff_q_initial_segment_exact_count_bits_decoded * S ((S (ff_i_initial_segment_exact_count_bits)) * c) + (ff_bit_initial_segment_exact_count_bits))) /\ (ff_bit_initial_segment_exact_count_bits = 0 \/ ff_bit_initial_segment_exact_count_bits = 1))))) -> n = q

Structural proof guide

The BitCount of a bounded exact initial segment is its threshold.

Direct prerequisites: le_zero, le_eq_or_lt, le_of_succ_le_succ, le_succ, le_refl, lt_not_le, bit_count_zero, bit_count_succ_decompose, eisenstein_initial_segment_decoded_choice, beta_all_one_bit_count_exact. The authored body proceeds by structural induction (1), case analysis (14), intermediate claims (12), equality transport (6).

Proof neighborhood

Direct dependencies

BT000Y le_zero BT001C le_eq_or_lt BT0017 le_of_succ_le_succ BT0018 le_succ BT000E le_refl BT001I lt_not_le BT008N bit_count_zero BT008O bit_count_succ_decompose BT00JB eisenstein_initial_segment_decoded_choice BT00JC beta_all_one_bit_count_exact

Direct dependents

BT00JE eisenstein_initial_segment_bit_count_exact

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 b
  3. 0003intro c
  4. 0004induction k
  5. 0005intro n
  6. 0006intro hprefix
  7. 0007intro hqk
  8. 0008intro hcount
  9. 0009have hq0 : q = 0
  10. 0010specialize le_zero q
  11. 0011apply le_zero
  12. 0012exact hqk
  13. 0013have hn0 : n = 0
  14. 0014specialize bit_count_zero b
  15. 0015specialize bit_count_zero c
  16. 0016specialize bit_count_zero 0
  17. 0017specialize bit_count_zero n
  18. 0018apply bit_count_zero
  19. 0019refl
  20. 0020exact hcount
  21. 0021trans 0
  22. 0022exact hn0
  23. 0023symm
  24. 0024exact hq0
  25. 0025intro n
  26. 0026intro hprefix
  27. 0027intro hqk
  28. 0028intro hcount
  29. 0029have hsplit : q = S k \/ exists gap. gap + S q = S k
  30. 0030specialize le_eq_or_lt q
  31. 0031specialize le_eq_or_lt (S k)
  32. 0032apply le_eq_or_lt
  33. 0033exact hqk
  34. 0034cases hsplit
  35. 0035have hallone : forall eis_one_index_initial_segment_functional_all_one. (exists eis_lt_gap_initial_segment_functional_all_one_bound. eis_lt_gap_initial_segment_functional_all_one_bound + S (eis_one_index_initial_segment_functional_all_one) = S k) -> (((exists ff_h_eis_initial_segment_functional_all_one_decoded. ff_h_eis_initial_segment_functional_all_one_decoded + S (1) = S ((S (eis_one_index_initial_segment_functional_all_one)) * c)) /\ exists ff_q_eis_initial_segment_functional_all_one_decoded. b = ff_q_eis_initial_segment_functional_all_one_decoded * S ((S (eis_one_index_initial_segment_functional_all_one)) * c) + (1)))
  36. 0036intro j
  37. 0037intro hj
  38. 0038have hstored : exists bit. ((((exists ff_h_initial_segment_functional_stored. ff_h_initial_segment_functional_stored + S (bit) = S ((S (j)) * c)) /\ exists ff_q_initial_segment_functional_stored. b = ff_q_initial_segment_functional_stored * S ((S (j)) * c) + (bit))) /\ (((bit = 1 /\ (exists eis_le_gap_initial_segment_functional_stored_choice_inside. eis_le_gap_initial_segment_functional_stored_choice_inside + (S j) = q)) \/ (bit = 0 /\ (exists eis_lt_gap_initial_segment_functional_stored_choice_outside. eis_lt_gap_initial_segment_functional_stored_choice_outside + S (q) = S j)))))
  39. 0039specialize hprefix j
  40. 0040apply hprefix
  41. 0041exact hj
  42. 0042cases hstored
  43. 0043cases hstored_witness
  44. 0044cases hstored_witness_right
  45. 0045cases hstored_witness_right_left
  46. 0046have hbit_one : x = 1
  47. 0047exact hstored_witness_right_left_left
  48. 0048rewrite hbit_one at hstored_witness_left
  49. 0049rewrite hbit_one at hstored_witness_left
  50. 0050exact hstored_witness_left
  51. 0051cases hstored_witness_right_right
  52. 0052exfalso
  53. 0053rewrite hsplit_left at hstored_witness_right_right_right
  54. 0054specialize lt_not_le (S k)
  55. 0055specialize lt_not_le (S j)
  56. 0056apply lt_not_le
  57. 0057exact hstored_witness_right_right_right
  58. 0058exact hj
  59. 0059have hn : n = S k
  60. 0060specialize beta_all_one_bit_count_exact b
  61. 0061specialize beta_all_one_bit_count_exact c
  62. 0062specialize beta_all_one_bit_count_exact (S k)
  63. 0063specialize beta_all_one_bit_count_exact n
  64. 0064apply beta_all_one_bit_count_exact
  65. 0065exact hallone
  66. 0066exact hcount
  67. 0067trans S k
  68. 0068exact hn
  69. 0069symm
  70. 0070exact hsplit_left
  71. 0071have hqk_previous : exists gap. gap + q = k
  72. 0072specialize le_of_succ_le_succ q
  73. 0073specialize le_of_succ_le_succ k
  74. 0074apply le_of_succ_le_succ
  75. 0075exact hsplit_right
  76. 0076have hprevious : forall eis_index_initial_segment_functional_previous. (exists eis_lt_gap_initial_segment_functional_previous_bound. eis_lt_gap_initial_segment_functional_previous_bound + S (eis_index_initial_segment_functional_previous) = k) -> exists eis_bit_initial_segment_functional_previous. ((((exists ff_h_eis_initial_segment_functional_previous_decoded. ff_h_eis_initial_segment_functional_previous_decoded + S (eis_bit_initial_segment_functional_previous) = S ((S (eis_index_initial_segment_functional_previous)) * c)) /\ exists ff_q_eis_initial_segment_functional_previous_decoded. b = ff_q_eis_initial_segment_functional_previous_decoded * S ((S (eis_index_initial_segment_functional_previous)) * c) + (eis_bit_initial_segment_functional_previous))) /\ (((eis_bit_initial_segment_functional_previous = 1 /\ (exists eis_le_gap_initial_segment_functional_previous_choice_inside. eis_le_gap_initial_segment_functional_previous_choice_inside + (S eis_index_initial_segment_functional_previous) = q)) \/ (eis_bit_initial_segment_functional_previous = 0 /\ (exists eis_lt_gap_initial_segment_functional_previous_choice_outside. eis_lt_gap_initial_segment_functional_previous_choice_outside + S (q) = S eis_index_initial_segment_functional_previous)))))
  77. 0077intro j
  78. 0078intro hj
  79. 0079specialize hprefix j
  80. 0080apply hprefix
  81. 0081specialize le_succ (S j)
  82. 0082specialize le_succ k
  83. 0083apply le_succ
  84. 0084exact hj
  85. 0085have hdecomp : exists a r. (((exists ff_h_initial_segment_functional_last. ff_h_initial_segment_functional_last + S (a) = S ((S (k)) * c)) /\ exists ff_q_initial_segment_functional_last. b = ff_q_initial_segment_functional_last * S ((S (k)) * c) + (a))) /\ ((((exists ff_u_initial_segment_functional_prefix_count_sum ff_v_initial_segment_functional_prefix_count_sum. ((((exists ff_h_initial_segment_functional_prefix_count_sum_start. ff_h_initial_segment_functional_prefix_count_sum_start + S (0) = S ((S (0)) * ff_v_initial_segment_functional_prefix_count_sum)) /\ exists ff_q_initial_segment_functional_prefix_count_sum_start. ff_u_initial_segment_functional_prefix_count_sum = ff_q_initial_segment_functional_prefix_count_sum_start * S ((S (0)) * ff_v_initial_segment_functional_prefix_count_sum) + (0))) /\ ((((exists ff_h_initial_segment_functional_prefix_count_sum_terminal. ff_h_initial_segment_functional_prefix_count_sum_terminal + S (r) = S ((S (k)) * ff_v_initial_segment_functional_prefix_count_sum)) /\ exists ff_q_initial_segment_functional_prefix_count_sum_terminal. ff_u_initial_segment_functional_prefix_count_sum = ff_q_initial_segment_functional_prefix_count_sum_terminal * S ((S (k)) * ff_v_initial_segment_functional_prefix_count_sum) + (r))) /\ forall ff_i_initial_segment_functional_prefix_count_sum. (exists ff_lt_initial_segment_functional_prefix_count_sum_bound. ff_lt_initial_segment_functional_prefix_count_sum_bound + S ff_i_initial_segment_functional_prefix_count_sum = k) -> exists ff_a_initial_segment_functional_prefix_count_sum ff_r_initial_segment_functional_prefix_count_sum ff_s_initial_segment_functional_prefix_count_sum. ((((exists ff_h_initial_segment_functional_prefix_count_sum_summand. ff_h_initial_segment_functional_prefix_count_sum_summand + S (ff_a_initial_segment_functional_prefix_count_sum) = S ((S (ff_i_initial_segment_functional_prefix_count_sum)) * c)) /\ exists ff_q_initial_segment_functional_prefix_count_sum_summand. b = ff_q_initial_segment_functional_prefix_count_sum_summand * S ((S (ff_i_initial_segment_functional_prefix_count_sum)) * c) + (ff_a_initial_segment_functional_prefix_count_sum))) /\ ((((exists ff_h_initial_segment_functional_prefix_count_sum_partial. ff_h_initial_segment_functional_prefix_count_sum_partial + S (ff_r_initial_segment_functional_prefix_count_sum) = S ((S (ff_i_initial_segment_functional_prefix_count_sum)) * ff_v_initial_segment_functional_prefix_count_sum)) /\ exists ff_q_initial_segment_functional_prefix_count_sum_partial. ff_u_initial_segment_functional_prefix_count_sum = ff_q_initial_segment_functional_prefix_count_sum_partial * S ((S (ff_i_initial_segment_functional_prefix_count_sum)) * ff_v_initial_segment_functional_prefix_count_sum) + (ff_r_initial_segment_functional_prefix_count_sum))) /\ ((((exists ff_h_initial_segment_functional_prefix_count_sum_successor. ff_h_initial_segment_functional_prefix_count_sum_successor + S (ff_s_initial_segment_functional_prefix_count_sum) = S ((S (S ff_i_initial_segment_functional_prefix_count_sum)) * ff_v_initial_segment_functional_prefix_count_sum)) /\ exists ff_q_initial_segment_functional_prefix_count_sum_successor. ff_u_initial_segment_functional_prefix_count_sum = ff_q_initial_segment_functional_prefix_count_sum_successor * S ((S (S ff_i_initial_segment_functional_prefix_count_sum)) * ff_v_initial_segment_functional_prefix_count_sum) + (ff_s_initial_segment_functional_prefix_count_sum))) /\ ff_s_initial_segment_functional_prefix_count_sum = ff_r_initial_segment_functional_prefix_count_sum + ff_a_initial_segment_functional_prefix_count_sum)))))) /\ (forall ff_i_initial_segment_functional_prefix_count_bits. (exists ff_lt_initial_segment_functional_prefix_count_bits_bound. ff_lt_initial_segment_functional_prefix_count_bits_bound + S ff_i_initial_segment_functional_prefix_count_bits = k) -> exists ff_bit_initial_segment_functional_prefix_count_bits. ((((exists ff_h_initial_segment_functional_prefix_count_bits_decoded. ff_h_initial_segment_functional_prefix_count_bits_decoded + S (ff_bit_initial_segment_functional_prefix_count_bits) = S ((S (ff_i_initial_segment_functional_prefix_count_bits)) * c)) /\ exists ff_q_initial_segment_functional_prefix_count_bits_decoded. b = ff_q_initial_segment_functional_prefix_count_bits_decoded * S ((S (ff_i_initial_segment_functional_prefix_count_bits)) * c) + (ff_bit_initial_segment_functional_prefix_count_bits))) /\ (ff_bit_initial_segment_functional_prefix_count_bits = 0 \/ ff_bit_initial_segment_functional_prefix_count_bits = 1))))) /\ ((a = 0 \/ a = 1) /\ n = r + a))
  86. 0086specialize bit_count_succ_decompose b
  87. 0087specialize bit_count_succ_decompose c
  88. 0088specialize bit_count_succ_decompose k
  89. 0089specialize bit_count_succ_decompose (S k)
  90. 0090specialize bit_count_succ_decompose n
  91. 0091apply bit_count_succ_decompose
  92. 0092refl
  93. 0093exact hcount
  94. 0094cases hdecomp
  95. 0095cases hdecomp_witness
  96. 0096cases hdecomp_witness_witness
  97. 0097cases hdecomp_witness_witness_right
  98. 0098cases hdecomp_witness_witness_right_right
  99. 0099have hlast_choice : ((x = 1 /\ (exists eis_le_gap_initial_segment_functional_last_choice_inside. eis_le_gap_initial_segment_functional_last_choice_inside + (S k) = q)) \/ (x = 0 /\ (exists eis_lt_gap_initial_segment_functional_last_choice_outside. eis_lt_gap_initial_segment_functional_last_choice_outside + S (q) = S k)))
  100. 0100specialize eisenstein_initial_segment_decoded_choice q
  101. 0101specialize eisenstein_initial_segment_decoded_choice b
  102. 0102specialize eisenstein_initial_segment_decoded_choice c
  103. 0103specialize eisenstein_initial_segment_decoded_choice (S k)
  104. 0104specialize eisenstein_initial_segment_decoded_choice k
  105. 0105specialize eisenstein_initial_segment_decoded_choice x
  106. 0106apply eisenstein_initial_segment_decoded_choice
  107. 0107exact hprefix
  108. 0108specialize le_refl (S k)
  109. 0109exact le_refl
  110. 0110exact hdecomp_witness_witness_left
  111. 0111cases hlast_choice
  112. 0112cases hlast_choice_left
  113. 0113exfalso
  114. 0114specialize lt_not_le q
  115. 0115specialize lt_not_le (S k)
  116. 0116apply lt_not_le
  117. 0117exact hsplit_right
  118. 0118exact hlast_choice_left_right
  119. 0119cases hlast_choice_right
  120. 0120have hrq : x1 = q
  121. 0121specialize IH x1
  122. 0122apply IH
  123. 0123exact hprevious
  124. 0124exact hqk_previous
  125. 0125exact hdecomp_witness_witness_right_left
  126. 0126rewrite hdecomp_witness_witness_right_right_right
  127. 0127rewrite hrq
  128. 0128rewrite hlast_choice_right_left
  129. 0129apply PA3