PA00DA

distinct_odd_prime_half_cell_indicator_choice

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

Every bounded lattice cell has a constructive exact indicator bit.

Exact expanded PA statement

forall p q h k i j. p = 2 * h + 1 -> q = 2 * k + 1 -> ((~(p = 1) /\ forall frp_prime_left_row_indicator_prime_p frp_prime_right_row_indicator_prime_p. p = frp_prime_left_row_indicator_prime_p * frp_prime_right_row_indicator_prime_p -> frp_prime_left_row_indicator_prime_p = 1 \/ frp_prime_right_row_indicator_prime_p = 1)) -> ((~(q = 1) /\ forall frp_prime_left_row_indicator_prime_q frp_prime_right_row_indicator_prime_q. q = frp_prime_left_row_indicator_prime_q * frp_prime_right_row_indicator_prime_q -> frp_prime_left_row_indicator_prime_q = 1 \/ frp_prime_right_row_indicator_prime_q = 1)) -> ~(p = q) -> (exists eri_gap_row_indicator_i_bound. eri_gap_row_indicator_i_bound + S (i) = h) -> (exists eri_gap_row_indicator_j_bound. eri_gap_row_indicator_j_bound + S (j) = k) -> exists bit. (((bit = 0 /\ ((exists eri_gap_row_indicator_point_result_left. eri_gap_row_indicator_point_result_left + S (q * S i) = p * S j) /\ ~(exists eri_gap_row_indicator_point_result_right. eri_gap_row_indicator_point_result_right + S (p * S j) = q * S i))) \/ (bit = 1 /\ ((exists eri_gap_row_indicator_point_result_right. eri_gap_row_indicator_point_result_right + S (p * S j) = q * S i) /\ ~(exists eri_gap_row_indicator_point_result_left. eri_gap_row_indicator_point_result_left + S (q * S i) = p * S j)))))

Structural proof guide

Generated structural guide

Every bounded lattice cell has a constructive exact indicator bit.

Use the direct prerequisites distinct_odd_prime_half_cell_oriented as previously established PA formulas.

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

Referenced ingredients

PA00D9 distinct_odd_prime_half_cell_oriented

Proof neighborhood

Direct dependencies

PA00D9 distinct_odd_prime_half_cell_oriented

Direct dependents

PA00DB distinct_odd_prime_half_row_indicator_choices

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 h
  4. 0004intro k
  5. 0005intro i
  6. 0006intro j
  7. 0007intro hpodd
  8. 0008intro hqodd
  9. 0009intro hp
  10. 0010intro hq
  11. 0011intro hpq
  12. 0012intro hi
  13. 0013intro hj
  14. 0014have horientation : (((exists elo_gap_row_indicator_point_orientation_left. elo_gap_row_indicator_point_orientation_left + S (q * S i) = p * S j) /\ ~(exists elo_gap_row_indicator_point_orientation_right. elo_gap_row_indicator_point_orientation_right + S (p * S j) = q * S i)) \/ ((exists elo_gap_row_indicator_point_orientation_right. elo_gap_row_indicator_point_orientation_right + S (p * S j) = q * S i) /\ ~(exists elo_gap_row_indicator_point_orientation_left. elo_gap_row_indicator_point_orientation_left + S (q * S i) = p * S j)))
  15. 0015specialize distinct_odd_prime_half_cell_oriented p
  16. 0016specialize distinct_odd_prime_half_cell_oriented q
  17. 0017specialize distinct_odd_prime_half_cell_oriented h
  18. 0018specialize distinct_odd_prime_half_cell_oriented k
  19. 0019specialize distinct_odd_prime_half_cell_oriented i
  20. 0020specialize distinct_odd_prime_half_cell_oriented j
  21. 0021apply distinct_odd_prime_half_cell_oriented
  22. 0022exact hpodd
  23. 0023exact hqodd
  24. 0024exact hp
  25. 0025exact hq
  26. 0026exact hpq
  27. 0027exact hi
  28. 0028exact hj
  29. 0029cases horientation
  30. 0030exists 0
  31. 0031left
  32. 0032split
  33. 0033refl
  34. 0034exact horientation_left
  35. 0035exists 1
  36. 0036right
  37. 0037split
  38. 0038refl
  39. 0039exact horientation_right