BT00JA

eisenstein_initial_segment_prefix_all_bits

Alpha body-checked · checked-use disabled

Every exact threshold prefix is an AllBits prefix.

Exact expanded PA statement

forall q b c k. (forall eis_index_initial_segment_bits_source. (exists eis_lt_gap_initial_segment_bits_source_bound. eis_lt_gap_initial_segment_bits_source_bound + S (eis_index_initial_segment_bits_source) = k) -> exists eis_bit_initial_segment_bits_source. ((((exists ff_h_eis_initial_segment_bits_source_decoded. ff_h_eis_initial_segment_bits_source_decoded + S (eis_bit_initial_segment_bits_source) = S ((S (eis_index_initial_segment_bits_source)) * c)) /\ exists ff_q_eis_initial_segment_bits_source_decoded. b = ff_q_eis_initial_segment_bits_source_decoded * S ((S (eis_index_initial_segment_bits_source)) * c) + (eis_bit_initial_segment_bits_source))) /\ (((eis_bit_initial_segment_bits_source = 1 /\ (exists eis_le_gap_initial_segment_bits_source_choice_inside. eis_le_gap_initial_segment_bits_source_choice_inside + (S eis_index_initial_segment_bits_source) = q)) \/ (eis_bit_initial_segment_bits_source = 0 /\ (exists eis_lt_gap_initial_segment_bits_source_choice_outside. eis_lt_gap_initial_segment_bits_source_choice_outside + S (q) = S eis_index_initial_segment_bits_source)))))) -> (forall ff_i_initial_segment_bits_result. (exists ff_lt_initial_segment_bits_result_bound. ff_lt_initial_segment_bits_result_bound + S ff_i_initial_segment_bits_result = k) -> exists ff_bit_initial_segment_bits_result. ((((exists ff_h_initial_segment_bits_result_decoded. ff_h_initial_segment_bits_result_decoded + S (ff_bit_initial_segment_bits_result) = S ((S (ff_i_initial_segment_bits_result)) * c)) /\ exists ff_q_initial_segment_bits_result_decoded. b = ff_q_initial_segment_bits_result_decoded * S ((S (ff_i_initial_segment_bits_result)) * c) + (ff_bit_initial_segment_bits_result))) /\ (ff_bit_initial_segment_bits_result = 0 \/ ff_bit_initial_segment_bits_result = 1)))

Structural proof guide

Every exact threshold prefix is an AllBits prefix.

Direct prerequisites: none. The authored body proceeds by case analysis (5), intermediate claims (1).

Proof neighborhood

Direct dependencies

none

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. 0004intro k
  5. 0005intro hprefix
  6. 0006intro j
  7. 0007intro hj
  8. 0008specialize hprefix j
  9. 0009have hstored : exists bit. ((((exists ff_h_initial_segment_bits_stored. ff_h_initial_segment_bits_stored + S (bit) = S ((S (j)) * c)) /\ exists ff_q_initial_segment_bits_stored. b = ff_q_initial_segment_bits_stored * S ((S (j)) * c) + (bit))) /\ (((bit = 1 /\ (exists eis_le_gap_initial_segment_bits_choice_inside. eis_le_gap_initial_segment_bits_choice_inside + (S j) = q)) \/ (bit = 0 /\ (exists eis_lt_gap_initial_segment_bits_choice_outside. eis_lt_gap_initial_segment_bits_choice_outside + S (q) = S j)))))
  10. 0010apply hprefix
  11. 0011exact hj
  12. 0012cases hstored
  13. 0013cases hstored_witness
  14. 0014exists x
  15. 0015split
  16. 0016exact hstored_witness_left
  17. 0017cases hstored_witness_right
  18. 0018cases hstored_witness_right_left
  19. 0019right
  20. 0020exact hstored_witness_right_left_left
  21. 0021cases hstored_witness_right_right
  22. 0022left
  23. 0023exact hstored_witness_right_right_left