BT00SF

eisenstein_initial_segment_prefix_exists

Alpha body-checked · checked-use disabled

Every threshold and finite length has an exact beta-coded indicator.

Exact expanded PA statement

forall q k. (exists b c. (forall eis_index_initial_segment_exists_result. (exists eis_lt_gap_initial_segment_exists_result_bound. eis_lt_gap_initial_segment_exists_result_bound + S (eis_index_initial_segment_exists_result) = k) -> exists eis_bit_initial_segment_exists_result. ((((exists ff_h_eis_initial_segment_exists_result_decoded. ff_h_eis_initial_segment_exists_result_decoded + S (eis_bit_initial_segment_exists_result) = S ((S (eis_index_initial_segment_exists_result)) * c)) /\ exists ff_q_eis_initial_segment_exists_result_decoded. b = ff_q_eis_initial_segment_exists_result_decoded * S ((S (eis_index_initial_segment_exists_result)) * c) + (eis_bit_initial_segment_exists_result))) /\ (((eis_bit_initial_segment_exists_result = 1 /\ (exists eis_le_gap_initial_segment_exists_result_choice_inside. eis_le_gap_initial_segment_exists_result_choice_inside + (S eis_index_initial_segment_exists_result) = q)) \/ (eis_bit_initial_segment_exists_result = 0 /\ (exists eis_lt_gap_initial_segment_exists_result_choice_outside. eis_lt_gap_initial_segment_exists_result_choice_outside + S (q) = S eis_index_initial_segment_exists_result)))))))

Structural proof guide

Every threshold and finite length has an exact beta-coded indicator.

Direct prerequisites: add_eq_zero_right, succ_ne_zero, eisenstein_initial_segment_indicator_choice, eisenstein_initial_segment_prefix_extend. The authored body proceeds by structural induction (1), case analysis (3), intermediate claims (4).

Proof neighborhood

Direct dependencies

BT000L add_eq_zero_right BT000C succ_ne_zero BT00SD eisenstein_initial_segment_indicator_choice BT00SE eisenstein_initial_segment_prefix_extend

Direct dependents

BT00SU initial_segment_prefix_sum_exists

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. 0002induction k
  3. 0003exists 0
  4. 0004exists 0
  5. 0005intro j
  6. 0006intro hj
  7. 0007exfalso
  8. 0008cases hj
  9. 0009have hsj : S j = 0
  10. 0010specialize add_eq_zero_right x
  11. 0011specialize add_eq_zero_right (S j)
  12. 0012apply add_eq_zero_right
  13. 0013exact hj_witness
  14. 0014specialize succ_ne_zero j
  15. 0015apply succ_ne_zero
  16. 0016exact hsj
  17. 0017have hprevious : exists b c. (forall eis_index_initial_segment_exists_previous. (exists eis_lt_gap_initial_segment_exists_previous_bound. eis_lt_gap_initial_segment_exists_previous_bound + S (eis_index_initial_segment_exists_previous) = k) -> exists eis_bit_initial_segment_exists_previous. ((((exists ff_h_eis_initial_segment_exists_previous_decoded. ff_h_eis_initial_segment_exists_previous_decoded + S (eis_bit_initial_segment_exists_previous) = S ((S (eis_index_initial_segment_exists_previous)) * c)) /\ exists ff_q_eis_initial_segment_exists_previous_decoded. b = ff_q_eis_initial_segment_exists_previous_decoded * S ((S (eis_index_initial_segment_exists_previous)) * c) + (eis_bit_initial_segment_exists_previous))) /\ (((eis_bit_initial_segment_exists_previous = 1 /\ (exists eis_le_gap_initial_segment_exists_previous_choice_inside. eis_le_gap_initial_segment_exists_previous_choice_inside + (S eis_index_initial_segment_exists_previous) = q)) \/ (eis_bit_initial_segment_exists_previous = 0 /\ (exists eis_lt_gap_initial_segment_exists_previous_choice_outside. eis_lt_gap_initial_segment_exists_previous_choice_outside + S (q) = S eis_index_initial_segment_exists_previous))))))
  18. 0018exact IH
  19. 0019cases hprevious
  20. 0020cases hprevious_witness
  21. 0021have hlast : exists bit. (((bit = 1 /\ (exists eis_le_gap_initial_segment_exists_last_inside. eis_le_gap_initial_segment_exists_last_inside + (S k) = q)) \/ (bit = 0 /\ (exists eis_lt_gap_initial_segment_exists_last_outside. eis_lt_gap_initial_segment_exists_last_outside + S (q) = S k))))
  22. 0022specialize eisenstein_initial_segment_indicator_choice q
  23. 0023specialize eisenstein_initial_segment_indicator_choice k
  24. 0024exact eisenstein_initial_segment_indicator_choice
  25. 0025have hnext : exists b c. (forall eis_index_initial_segment_exists_successor. (exists eis_lt_gap_initial_segment_exists_successor_bound. eis_lt_gap_initial_segment_exists_successor_bound + S (eis_index_initial_segment_exists_successor) = S k) -> exists eis_bit_initial_segment_exists_successor. ((((exists ff_h_eis_initial_segment_exists_successor_decoded. ff_h_eis_initial_segment_exists_successor_decoded + S (eis_bit_initial_segment_exists_successor) = S ((S (eis_index_initial_segment_exists_successor)) * c)) /\ exists ff_q_eis_initial_segment_exists_successor_decoded. b = ff_q_eis_initial_segment_exists_successor_decoded * S ((S (eis_index_initial_segment_exists_successor)) * c) + (eis_bit_initial_segment_exists_successor))) /\ (((eis_bit_initial_segment_exists_successor = 1 /\ (exists eis_le_gap_initial_segment_exists_successor_choice_inside. eis_le_gap_initial_segment_exists_successor_choice_inside + (S eis_index_initial_segment_exists_successor) = q)) \/ (eis_bit_initial_segment_exists_successor = 0 /\ (exists eis_lt_gap_initial_segment_exists_successor_choice_outside. eis_lt_gap_initial_segment_exists_successor_choice_outside + S (q) = S eis_index_initial_segment_exists_successor))))))
  26. 0026specialize eisenstein_initial_segment_prefix_extend q
  27. 0027specialize eisenstein_initial_segment_prefix_extend x
  28. 0028specialize eisenstein_initial_segment_prefix_extend x1
  29. 0029specialize eisenstein_initial_segment_prefix_extend k
  30. 0030apply eisenstein_initial_segment_prefix_extend
  31. 0031exact hprevious_witness_witness
  32. 0032exact hlast
  33. 0033exact hnext