PA00EA

eisenstein_row_indicator_decoded_choice

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

Every decoded row bit recovers its exact strict-orientation meaning.

Exact expanded PA statement

forall p q i rb rc l j bit. (forall eri_column_row_indicator_projection_prefix. (exists eri_gap_row_indicator_projection_prefix_bound. eri_gap_row_indicator_projection_prefix_bound + S (eri_column_row_indicator_projection_prefix) = l) -> exists eri_bit_row_indicator_projection_prefix. ((((exists ff_h_eri_row_indicator_projection_prefix_decoded. ff_h_eri_row_indicator_projection_prefix_decoded + S (eri_bit_row_indicator_projection_prefix) = S ((S (eri_column_row_indicator_projection_prefix)) * rc)) /\ exists ff_q_eri_row_indicator_projection_prefix_decoded. rb = ff_q_eri_row_indicator_projection_prefix_decoded * S ((S (eri_column_row_indicator_projection_prefix)) * rc) + (eri_bit_row_indicator_projection_prefix))) /\ (((eri_bit_row_indicator_projection_prefix = 0 /\ ((exists eri_gap_row_indicator_projection_prefix_choice_left. eri_gap_row_indicator_projection_prefix_choice_left + S (q * S i) = p * S eri_column_row_indicator_projection_prefix) /\ ~(exists eri_gap_row_indicator_projection_prefix_choice_right. eri_gap_row_indicator_projection_prefix_choice_right + S (p * S eri_column_row_indicator_projection_prefix) = q * S i))) \/ (eri_bit_row_indicator_projection_prefix = 1 /\ ((exists eri_gap_row_indicator_projection_prefix_choice_right. eri_gap_row_indicator_projection_prefix_choice_right + S (p * S eri_column_row_indicator_projection_prefix) = q * S i) /\ ~(exists eri_gap_row_indicator_projection_prefix_choice_left. eri_gap_row_indicator_projection_prefix_choice_left + S (q * S i) = p * S eri_column_row_indicator_projection_prefix))))))) -> (exists eri_gap_row_indicator_projection_bound. eri_gap_row_indicator_projection_bound + S (j) = l) -> (((exists ff_h_row_indicator_projection_entry. ff_h_row_indicator_projection_entry + S (bit) = S ((S (j)) * rc)) /\ exists ff_q_row_indicator_projection_entry. rb = ff_q_row_indicator_projection_entry * S ((S (j)) * rc) + (bit))) -> (((bit = 0 /\ ((exists eri_gap_row_indicator_projection_choice_left. eri_gap_row_indicator_projection_choice_left + S (q * S i) = p * S j) /\ ~(exists eri_gap_row_indicator_projection_choice_right. eri_gap_row_indicator_projection_choice_right + S (p * S j) = q * S i))) \/ (bit = 1 /\ ((exists eri_gap_row_indicator_projection_choice_right. eri_gap_row_indicator_projection_choice_right + S (p * S j) = q * S i) /\ ~(exists eri_gap_row_indicator_projection_choice_left. eri_gap_row_indicator_projection_choice_left + S (q * S i) = p * S j)))))

Structural proof guide

Generated structural guide

Every decoded row bit recovers its exact strict-orientation meaning.

Use the direct prerequisites beta_at_unique as previously established PA formulas.

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

Referenced ingredients

PA002F beta_at_unique

Proof neighborhood

Direct dependencies

PA002F beta_at_unique

Direct dependents

PA00EB eisenstein_transposed_column_prefix_all_bits PA00EC eisenstein_transposed_decoded_cell_bits_complementary PA00F4 eisenstein_transposed_column_decoded_choice PA00F9 eisenstein_successor_terminal_bit_matches_last_column

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 j
  8. 0008intro bit
  9. 0009intro hprefix
  10. 0010intro hj
  11. 0011intro hentry
  12. 0012have hstored : exists stored. ((((exists ff_h_row_indicator_projection_stored. ff_h_row_indicator_projection_stored + S (stored) = S ((S (j)) * rc)) /\ exists ff_q_row_indicator_projection_stored. rb = ff_q_row_indicator_projection_stored * S ((S (j)) * rc) + (stored))) /\ (((stored = 0 /\ ((exists eri_gap_row_indicator_projection_stored_choice_left. eri_gap_row_indicator_projection_stored_choice_left + S (q * S i) = p * S j) /\ ~(exists eri_gap_row_indicator_projection_stored_choice_right. eri_gap_row_indicator_projection_stored_choice_right + S (p * S j) = q * S i))) \/ (stored = 1 /\ ((exists eri_gap_row_indicator_projection_stored_choice_right. eri_gap_row_indicator_projection_stored_choice_right + S (p * S j) = q * S i) /\ ~(exists eri_gap_row_indicator_projection_stored_choice_left. eri_gap_row_indicator_projection_stored_choice_left + S (q * S i) = p * S j))))))
  13. 0013specialize hprefix j
  14. 0014apply hprefix
  15. 0015exact hj
  16. 0016cases hstored
  17. 0017cases hstored_witness
  18. 0018have heq : x = bit
  19. 0019specialize beta_at_unique rb
  20. 0020specialize beta_at_unique rc
  21. 0021specialize beta_at_unique j
  22. 0022specialize beta_at_unique x
  23. 0023specialize beta_at_unique bit
  24. 0024apply beta_at_unique
  25. 0025exact hstored_witness_left
  26. 0026exact hentry
  27. 0027rewrite heq at hstored_witness_right
  28. 0028rewrite heq at hstored_witness_right
  29. 0029exact hstored_witness_right