PA00F5

eisenstein_cell_indicator_choice_unique

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

The exact orientation predicate determines its zero-or-one indicator uniquely.

Exact expanded PA statement

forall p q i j a d. (((a = 0 /\ ((exists eri_gap_fubini_cell_choice_unique_first_left. eri_gap_fubini_cell_choice_unique_first_left + S (q * S i) = p * S j) /\ ~(exists eri_gap_fubini_cell_choice_unique_first_right. eri_gap_fubini_cell_choice_unique_first_right + S (p * S j) = q * S i))) \/ (a = 1 /\ ((exists eri_gap_fubini_cell_choice_unique_first_right. eri_gap_fubini_cell_choice_unique_first_right + S (p * S j) = q * S i) /\ ~(exists eri_gap_fubini_cell_choice_unique_first_left. eri_gap_fubini_cell_choice_unique_first_left + S (q * S i) = p * S j))))) -> (((d = 0 /\ ((exists eri_gap_fubini_cell_choice_unique_second_left. eri_gap_fubini_cell_choice_unique_second_left + S (q * S i) = p * S j) /\ ~(exists eri_gap_fubini_cell_choice_unique_second_right. eri_gap_fubini_cell_choice_unique_second_right + S (p * S j) = q * S i))) \/ (d = 1 /\ ((exists eri_gap_fubini_cell_choice_unique_second_right. eri_gap_fubini_cell_choice_unique_second_right + S (p * S j) = q * S i) /\ ~(exists eri_gap_fubini_cell_choice_unique_second_left. eri_gap_fubini_cell_choice_unique_second_left + S (q * S i) = p * S j))))) -> a = d

Structural proof guide

Generated structural guide

The exact orientation predicate determines its zero-or-one indicator uniquely.

This root lemma is proved directly from the PA rules and the hypotheses introduced by its statement.

The proof proceeds by case analysis (13).

Referenced ingredients

none

Proof neighborhood

Direct dependencies

none

Direct dependents

PA00F6 eisenstein_transposed_column_counts_extensional 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 j
  5. 0005intro a
  6. 0006intro d
  7. 0007intro ha
  8. 0008intro hd
  9. 0009cases ha
  10. 0010cases ha_left
  11. 0011cases ha_left_right
  12. 0012cases hd
  13. 0013cases hd_left
  14. 0014trans 0
  15. 0015exact ha_left_left
  16. 0016symm
  17. 0017exact hd_left_left
  18. 0018cases hd_right
  19. 0019cases hd_right_right
  20. 0020exfalso
  21. 0021apply hd_right_right_right
  22. 0022exact ha_left_right_left
  23. 0023cases ha_right
  24. 0024cases ha_right_right
  25. 0025cases hd
  26. 0026cases hd_left
  27. 0027cases hd_left_right
  28. 0028exfalso
  29. 0029apply ha_right_right_right
  30. 0030exact hd_left_right_left
  31. 0031cases hd_right
  32. 0032trans 1
  33. 0033exact ha_right_left
  34. 0034symm
  35. 0035exact hd_right_left