PA00DE

eisenstein_row_indicator_prefix_all_bits

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

The beta-coded indicator projection contains only zero and one.

Exact expanded PA statement

forall p q i rb rc l. (forall eri_column_row_indicator_bits_prefix. (exists eri_gap_row_indicator_bits_prefix_bound. eri_gap_row_indicator_bits_prefix_bound + S (eri_column_row_indicator_bits_prefix) = l) -> exists eri_bit_row_indicator_bits_prefix. ((((exists ff_h_eri_row_indicator_bits_prefix_decoded. ff_h_eri_row_indicator_bits_prefix_decoded + S (eri_bit_row_indicator_bits_prefix) = S ((S (eri_column_row_indicator_bits_prefix)) * rc)) /\ exists ff_q_eri_row_indicator_bits_prefix_decoded. rb = ff_q_eri_row_indicator_bits_prefix_decoded * S ((S (eri_column_row_indicator_bits_prefix)) * rc) + (eri_bit_row_indicator_bits_prefix))) /\ (((eri_bit_row_indicator_bits_prefix = 0 /\ ((exists eri_gap_row_indicator_bits_prefix_choice_left. eri_gap_row_indicator_bits_prefix_choice_left + S (q * S i) = p * S eri_column_row_indicator_bits_prefix) /\ ~(exists eri_gap_row_indicator_bits_prefix_choice_right. eri_gap_row_indicator_bits_prefix_choice_right + S (p * S eri_column_row_indicator_bits_prefix) = q * S i))) \/ (eri_bit_row_indicator_bits_prefix = 1 /\ ((exists eri_gap_row_indicator_bits_prefix_choice_right. eri_gap_row_indicator_bits_prefix_choice_right + S (p * S eri_column_row_indicator_bits_prefix) = q * S i) /\ ~(exists eri_gap_row_indicator_bits_prefix_choice_left. eri_gap_row_indicator_bits_prefix_choice_left + S (q * S i) = p * S eri_column_row_indicator_bits_prefix))))))) -> (forall ff_i_row_indicator_all_bits. (exists ff_lt_row_indicator_all_bits_bound. ff_lt_row_indicator_all_bits_bound + S ff_i_row_indicator_all_bits = l) -> exists ff_bit_row_indicator_all_bits. ((((exists ff_h_row_indicator_all_bits_decoded. ff_h_row_indicator_all_bits_decoded + S (ff_bit_row_indicator_all_bits) = S ((S (ff_i_row_indicator_all_bits)) * rc)) /\ exists ff_q_row_indicator_all_bits_decoded. rb = ff_q_row_indicator_all_bits_decoded * S ((S (ff_i_row_indicator_all_bits)) * rc) + (ff_bit_row_indicator_all_bits))) /\ (ff_bit_row_indicator_all_bits = 0 \/ ff_bit_row_indicator_all_bits = 1)))

Structural proof guide

Generated structural guide

The beta-coded indicator projection contains only zero and one.

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 (2).

Referenced ingredients

none

Proof neighborhood

Direct dependencies

none

Direct dependents

PA00DF distinct_odd_prime_half_row_count_exists

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 rb
  5. 0005intro rc
  6. 0006intro l
  7. 0007intro hprefix
  8. 0008intro j
  9. 0009intro hj
  10. 0010have hentry : forall eri_column_row_indicator_bits_entry_source. (exists eri_gap_row_indicator_bits_entry_source_bound. eri_gap_row_indicator_bits_entry_source_bound + S (eri_column_row_indicator_bits_entry_source) = l) -> exists eri_bit_row_indicator_bits_entry_source. ((((exists ff_h_eri_row_indicator_bits_entry_source_decoded. ff_h_eri_row_indicator_bits_entry_source_decoded + S (eri_bit_row_indicator_bits_entry_source) = S ((S (eri_column_row_indicator_bits_entry_source)) * rc)) /\ exists ff_q_eri_row_indicator_bits_entry_source_decoded. rb = ff_q_eri_row_indicator_bits_entry_source_decoded * S ((S (eri_column_row_indicator_bits_entry_source)) * rc) + (eri_bit_row_indicator_bits_entry_source))) /\ (((eri_bit_row_indicator_bits_entry_source = 0 /\ ((exists eri_gap_row_indicator_bits_entry_source_choice_left. eri_gap_row_indicator_bits_entry_source_choice_left + S (q * S i) = p * S eri_column_row_indicator_bits_entry_source) /\ ~(exists eri_gap_row_indicator_bits_entry_source_choice_right. eri_gap_row_indicator_bits_entry_source_choice_right + S (p * S eri_column_row_indicator_bits_entry_source) = q * S i))) \/ (eri_bit_row_indicator_bits_entry_source = 1 /\ ((exists eri_gap_row_indicator_bits_entry_source_choice_right. eri_gap_row_indicator_bits_entry_source_choice_right + S (p * S eri_column_row_indicator_bits_entry_source) = q * S i) /\ ~(exists eri_gap_row_indicator_bits_entry_source_choice_left. eri_gap_row_indicator_bits_entry_source_choice_left + S (q * S i) = p * S eri_column_row_indicator_bits_entry_source))))))
  11. 0011exact hprefix
  12. 0012specialize hentry j
  13. 0013have hstored : exists bit. ((((exists ff_h_row_indicator_bits_stored. ff_h_row_indicator_bits_stored + S (bit) = S ((S (j)) * rc)) /\ exists ff_q_row_indicator_bits_stored. rb = ff_q_row_indicator_bits_stored * S ((S (j)) * rc) + (bit))) /\ (((bit = 0 /\ ((exists eri_gap_row_indicator_bits_choice_left. eri_gap_row_indicator_bits_choice_left + S (q * S i) = p * S j) /\ ~(exists eri_gap_row_indicator_bits_choice_right. eri_gap_row_indicator_bits_choice_right + S (p * S j) = q * S i))) \/ (bit = 1 /\ ((exists eri_gap_row_indicator_bits_choice_right. eri_gap_row_indicator_bits_choice_right + S (p * S j) = q * S i) /\ ~(exists eri_gap_row_indicator_bits_choice_left. eri_gap_row_indicator_bits_choice_left + S (q * S i) = p * S j))))))
  14. 0014apply hentry
  15. 0015exact hj
  16. 0016cases hstored
  17. 0017cases hstored_witness
  18. 0018exists x
  19. 0019split
  20. 0020exact hstored_witness_left
  21. 0021cases hstored_witness_right
  22. 0022cases hstored_witness_right_left
  23. 0023left
  24. 0024exact hstored_witness_right_left_left
  25. 0025cases hstored_witness_right_right
  26. 0026right
  27. 0027exact hstored_witness_right_right_left