PA00DC

eisenstein_row_indicator_prefix_extend

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

Append one exact orientation bit while preserving the previous row prefix.

Exact expanded PA statement

forall p q i rb rc l. (forall eri_column_row_indicator_extend_before. (exists eri_gap_row_indicator_extend_before_bound. eri_gap_row_indicator_extend_before_bound + S (eri_column_row_indicator_extend_before) = l) -> exists eri_bit_row_indicator_extend_before. ((((exists ff_h_eri_row_indicator_extend_before_decoded. ff_h_eri_row_indicator_extend_before_decoded + S (eri_bit_row_indicator_extend_before) = S ((S (eri_column_row_indicator_extend_before)) * rc)) /\ exists ff_q_eri_row_indicator_extend_before_decoded. rb = ff_q_eri_row_indicator_extend_before_decoded * S ((S (eri_column_row_indicator_extend_before)) * rc) + (eri_bit_row_indicator_extend_before))) /\ (((eri_bit_row_indicator_extend_before = 0 /\ ((exists eri_gap_row_indicator_extend_before_choice_left. eri_gap_row_indicator_extend_before_choice_left + S (q * S i) = p * S eri_column_row_indicator_extend_before) /\ ~(exists eri_gap_row_indicator_extend_before_choice_right. eri_gap_row_indicator_extend_before_choice_right + S (p * S eri_column_row_indicator_extend_before) = q * S i))) \/ (eri_bit_row_indicator_extend_before = 1 /\ ((exists eri_gap_row_indicator_extend_before_choice_right. eri_gap_row_indicator_extend_before_choice_right + S (p * S eri_column_row_indicator_extend_before) = q * S i) /\ ~(exists eri_gap_row_indicator_extend_before_choice_left. eri_gap_row_indicator_extend_before_choice_left + S (q * S i) = p * S eri_column_row_indicator_extend_before))))))) -> (exists bit. (((bit = 0 /\ ((exists eri_gap_row_indicator_extend_last_left. eri_gap_row_indicator_extend_last_left + S (q * S i) = p * S l) /\ ~(exists eri_gap_row_indicator_extend_last_right. eri_gap_row_indicator_extend_last_right + S (p * S l) = q * S i))) \/ (bit = 1 /\ ((exists eri_gap_row_indicator_extend_last_right. eri_gap_row_indicator_extend_last_right + S (p * S l) = q * S i) /\ ~(exists eri_gap_row_indicator_extend_last_left. eri_gap_row_indicator_extend_last_left + S (q * S i) = p * S l)))))) -> exists z d. (forall eri_column_row_indicator_extend_after. (exists eri_gap_row_indicator_extend_after_bound. eri_gap_row_indicator_extend_after_bound + S (eri_column_row_indicator_extend_after) = S l) -> exists eri_bit_row_indicator_extend_after. ((((exists ff_h_eri_row_indicator_extend_after_decoded. ff_h_eri_row_indicator_extend_after_decoded + S (eri_bit_row_indicator_extend_after) = S ((S (eri_column_row_indicator_extend_after)) * d)) /\ exists ff_q_eri_row_indicator_extend_after_decoded. z = ff_q_eri_row_indicator_extend_after_decoded * S ((S (eri_column_row_indicator_extend_after)) * d) + (eri_bit_row_indicator_extend_after))) /\ (((eri_bit_row_indicator_extend_after = 0 /\ ((exists eri_gap_row_indicator_extend_after_choice_left. eri_gap_row_indicator_extend_after_choice_left + S (q * S i) = p * S eri_column_row_indicator_extend_after) /\ ~(exists eri_gap_row_indicator_extend_after_choice_right. eri_gap_row_indicator_extend_after_choice_right + S (p * S eri_column_row_indicator_extend_after) = q * S i))) \/ (eri_bit_row_indicator_extend_after = 1 /\ ((exists eri_gap_row_indicator_extend_after_choice_right. eri_gap_row_indicator_extend_after_choice_right + S (p * S eri_column_row_indicator_extend_after) = q * S i) /\ ~(exists eri_gap_row_indicator_extend_after_choice_left. eri_gap_row_indicator_extend_after_choice_left + S (q * S i) = p * S eri_column_row_indicator_extend_after)))))))

Structural proof guide

Generated structural guide

Append one exact orientation bit while preserving the previous row prefix.

Use the direct prerequisites beta_prefix_extend, finite_lt_succ_eq_or_lt as previously established PA formulas.

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

Referenced ingredients

PA002X beta_prefix_extend PA003D finite_lt_succ_eq_or_lt

Proof neighborhood

Direct dependencies

PA002X beta_prefix_extend PA003D finite_lt_succ_eq_or_lt

Direct dependents

PA00DD eisenstein_row_indicator_prefix_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 hchoice
  9. 0009cases hchoice
  10. 0010specialize beta_prefix_extend l
  11. 0011specialize beta_prefix_extend rb
  12. 0012specialize beta_prefix_extend rc
  13. 0013specialize beta_prefix_extend x
  14. 0014cases beta_prefix_extend
  15. 0015cases beta_prefix_extend_witness
  16. 0016cases beta_prefix_extend_witness_witness
  17. 0017exists x1
  18. 0018exists x2
  19. 0019intro j
  20. 0020intro hj
  21. 0021have hsplit : j = l \/ exists gap. gap + S j = l
  22. 0022specialize finite_lt_succ_eq_or_lt l
  23. 0023specialize finite_lt_succ_eq_or_lt j
  24. 0024apply finite_lt_succ_eq_or_lt
  25. 0025exact hj
  26. 0026cases hsplit
  27. 0027exists x
  28. 0028split
  29. 0029rewrite hsplit_left
  30. 0030rewrite hsplit_left
  31. 0031exact beta_prefix_extend_witness_witness_left
  32. 0032rewrite hsplit_left
  33. 0033rewrite hsplit_left
  34. 0034rewrite hsplit_left
  35. 0035rewrite hsplit_left
  36. 0036exact hchoice_witness
  37. 0037have hold : exists oldbit. ((((exists ff_h_row_indicator_extend_old_entry. ff_h_row_indicator_extend_old_entry + S (oldbit) = S ((S (j)) * rc)) /\ exists ff_q_row_indicator_extend_old_entry. rb = ff_q_row_indicator_extend_old_entry * S ((S (j)) * rc) + (oldbit))) /\ (((oldbit = 0 /\ ((exists eri_gap_row_indicator_extend_old_choice_left. eri_gap_row_indicator_extend_old_choice_left + S (q * S i) = p * S j) /\ ~(exists eri_gap_row_indicator_extend_old_choice_right. eri_gap_row_indicator_extend_old_choice_right + S (p * S j) = q * S i))) \/ (oldbit = 1 /\ ((exists eri_gap_row_indicator_extend_old_choice_right. eri_gap_row_indicator_extend_old_choice_right + S (p * S j) = q * S i) /\ ~(exists eri_gap_row_indicator_extend_old_choice_left. eri_gap_row_indicator_extend_old_choice_left + S (q * S i) = p * S j))))))
  38. 0038specialize hprefix j
  39. 0039apply hprefix
  40. 0040exact hsplit_right
  41. 0041cases hold
  42. 0042cases hold_witness
  43. 0043exists x3
  44. 0044split
  45. 0045specialize beta_prefix_extend_witness_witness_right j
  46. 0046specialize beta_prefix_extend_witness_witness_right x3
  47. 0047apply beta_prefix_extend_witness_witness_right
  48. 0048exact hsplit_right
  49. 0049exact hold_witness_left
  50. 0050exact hold_witness_right