PA00DU

eisenstein_initial_segment_prefix_all_bits

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

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

Generated structural guide

Every exact threshold prefix is an AllBits prefix.

This root lemma is proved directly from the PA rules and the hypotheses introduced by its statement.

The proof proceeds by case analysis (5), intermediate claims (1).

Referenced ingredients

none

Proof neighborhood

Direct dependencies

none

Direct dependents

PA00DY eisenstein_initial_segment_bit_count_exact

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 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