PA00DT

eisenstein_row_indicator_prefix_to_initial_segment

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

A semantic row prefix is the exact initial segment cut out by its nonzero division quotient.

Exact expanded PA statement

forall p q i d r rb rc k. (forall eri_column_row_quotient_source. (exists eri_gap_row_quotient_source_bound. eri_gap_row_quotient_source_bound + S (eri_column_row_quotient_source) = k) -> exists eri_bit_row_quotient_source. ((((exists ff_h_eri_row_quotient_source_decoded. ff_h_eri_row_quotient_source_decoded + S (eri_bit_row_quotient_source) = S ((S (eri_column_row_quotient_source)) * rc)) /\ exists ff_q_eri_row_quotient_source_decoded. rb = ff_q_eri_row_quotient_source_decoded * S ((S (eri_column_row_quotient_source)) * rc) + (eri_bit_row_quotient_source))) /\ (((eri_bit_row_quotient_source = 0 /\ ((exists eri_gap_row_quotient_source_choice_left. eri_gap_row_quotient_source_choice_left + S (q * S i) = p * S eri_column_row_quotient_source) /\ ~(exists eri_gap_row_quotient_source_choice_right. eri_gap_row_quotient_source_choice_right + S (p * S eri_column_row_quotient_source) = q * S i))) \/ (eri_bit_row_quotient_source = 1 /\ ((exists eri_gap_row_quotient_source_choice_right. eri_gap_row_quotient_source_choice_right + S (p * S eri_column_row_quotient_source) = q * S i) /\ ~(exists eri_gap_row_quotient_source_choice_left. eri_gap_row_quotient_source_choice_left + S (q * S i) = p * S eri_column_row_quotient_source))))))) -> q * S i = p * d + r -> ~(r = 0) -> (exists edt_lt_gap_row_quotient_remainder_bound. edt_lt_gap_row_quotient_remainder_bound + S (r) = p) -> (forall eis_index_row_quotient_initial. (exists eis_lt_gap_row_quotient_initial_bound. eis_lt_gap_row_quotient_initial_bound + S (eis_index_row_quotient_initial) = k) -> exists eis_bit_row_quotient_initial. ((((exists ff_h_eis_row_quotient_initial_decoded. ff_h_eis_row_quotient_initial_decoded + S (eis_bit_row_quotient_initial) = S ((S (eis_index_row_quotient_initial)) * rc)) /\ exists ff_q_eis_row_quotient_initial_decoded. rb = ff_q_eis_row_quotient_initial_decoded * S ((S (eis_index_row_quotient_initial)) * rc) + (eis_bit_row_quotient_initial))) /\ (((eis_bit_row_quotient_initial = 1 /\ (exists eis_le_gap_row_quotient_initial_choice_inside. eis_le_gap_row_quotient_initial_choice_inside + (S eis_index_row_quotient_initial) = d)) \/ (eis_bit_row_quotient_initial = 0 /\ (exists eis_lt_gap_row_quotient_initial_choice_outside. eis_lt_gap_row_quotient_initial_choice_outside + S (d) = S eis_index_row_quotient_initial))))))

Structural proof guide

Generated structural guide

A semantic row prefix is the exact initial segment cut out by its nonzero division quotient.

Use the direct prerequisites nonzero_remainder_division_positive_multiple_threshold, le_or_lt as previously established PA formulas.

The proof proceeds by case analysis (9), intermediate claims (2).

Referenced ingredients

PA00DS nonzero_remainder_division_positive_multiple_threshold PA003B le_or_lt

Proof neighborhood

Direct dependencies

PA00DS nonzero_remainder_division_positive_multiple_threshold PA003B le_or_lt

Direct dependents

PA00E0 distinct_odd_prime_row_bit_count_equals_division_quotient

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 i
  4. 0004intro d
  5. 0005intro r
  6. 0006intro rb
  7. 0007intro rc
  8. 0008intro k
  9. 0009intro hrow
  10. 0010intro hdivision
  11. 0011intro hr0
  12. 0012intro hrp
  13. 0013intro j
  14. 0014intro hj
  15. 0015have hstored : exists bit. ((((exists ff_h_row_quotient_stored. ff_h_row_quotient_stored + S (bit) = S ((S (j)) * rc)) /\ exists ff_q_row_quotient_stored. rb = ff_q_row_quotient_stored * S ((S (j)) * rc) + (bit))) /\ (((bit = 0 /\ ((exists eri_gap_row_quotient_stored_choice_left. eri_gap_row_quotient_stored_choice_left + S (q * S i) = p * S j) /\ ~(exists eri_gap_row_quotient_stored_choice_right. eri_gap_row_quotient_stored_choice_right + S (p * S j) = q * S i))) \/ (bit = 1 /\ ((exists eri_gap_row_quotient_stored_choice_right. eri_gap_row_quotient_stored_choice_right + S (p * S j) = q * S i) /\ ~(exists eri_gap_row_quotient_stored_choice_left. eri_gap_row_quotient_stored_choice_left + S (q * S i) = p * S j))))))
  16. 0016specialize hrow j
  17. 0017apply hrow
  18. 0018exact hj
  19. 0019cases hstored
  20. 0020cases hstored_witness
  21. 0021exists x
  22. 0022split
  23. 0023exact hstored_witness_left
  24. 0024have hthreshold : (((exists edt_lt_gap_row_quotient_below. edt_lt_gap_row_quotient_below + S (p * S j) = q * S i) -> (exists edt_le_gap_row_quotient_bounded. edt_le_gap_row_quotient_bounded + (S j) = d)) /\ ((exists edt_le_gap_row_quotient_bounded. edt_le_gap_row_quotient_bounded + (S j) = d) -> (exists edt_lt_gap_row_quotient_below. edt_lt_gap_row_quotient_below + S (p * S j) = q * S i)))
  25. 0025specialize nonzero_remainder_division_positive_multiple_threshold p
  26. 0026specialize nonzero_remainder_division_positive_multiple_threshold (q * S i)
  27. 0027specialize nonzero_remainder_division_positive_multiple_threshold d
  28. 0028specialize nonzero_remainder_division_positive_multiple_threshold r
  29. 0029specialize nonzero_remainder_division_positive_multiple_threshold j
  30. 0030apply nonzero_remainder_division_positive_multiple_threshold
  31. 0031exact hdivision
  32. 0032exact hr0
  33. 0033exact hrp
  34. 0034cases hthreshold
  35. 0035cases hstored_witness_right
  36. 0036cases hstored_witness_right_left
  37. 0037cases hstored_witness_right_left_right
  38. 0038right
  39. 0039split
  40. 0040exact hstored_witness_right_left_left
  41. 0041specialize le_or_lt (S j)
  42. 0042specialize le_or_lt d
  43. 0043cases le_or_lt
  44. 0044exfalso
  45. 0045apply hstored_witness_right_left_right_right
  46. 0046apply hthreshold_right
  47. 0047exact le_or_lt_left
  48. 0048exact le_or_lt_right
  49. 0049cases hstored_witness_right_right
  50. 0050cases hstored_witness_right_right_right
  51. 0051left
  52. 0052split
  53. 0053exact hstored_witness_right_right_left
  54. 0054apply hthreshold_left
  55. 0055exact hstored_witness_right_right_right_left