PA00C3

odd_half_positive_complement_exists

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

A positive magnitude at most the odd half has a complement below the modulus.

Exact expanded PA statement

forall p h m. p = 2 * h + 1 -> (exists gsp_lt_gap_gsd_m_positive. gsp_lt_gap_gsd_m_positive + S 0 = m) -> (exists gsp_le_gap_gsd_m_le_h. gsp_le_gap_gsd_m_le_h + m = h) -> (exists t. (exists gsp_lt_gap_gsd_t_below_p. gsp_lt_gap_gsd_t_below_p + S t = p) /\ t + m = p)

Structural proof guide

Generated structural guide

A positive magnitude at most the odd half has a complement below the modulus.

Use the direct prerequisites lt_irrefl_expanded, nonzero_is_succ, add_assoc, add_comm, mul_comm, zero_add, add_succ_left as previously established PA formulas.

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

Referenced ingredients

PA0010 lt_irrefl_expanded PA001V nonzero_is_succ PA0009 add_assoc PA000F add_comm PA000H mul_comm PA0001 zero_add PA000E add_succ_left

Proof neighborhood

Direct dependencies

PA0010 lt_irrefl_expanded PA001V nonzero_is_succ PA0009 add_assoc PA000F add_comm PA000H mul_comm PA0001 zero_add PA000E add_succ_left

Direct dependents

PA00C6 odd_signed_division_branch_exact

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 h
  3. 0003intro m
  4. 0004intro hp
  5. 0005intro hmpositive
  6. 0006intro hmle
  7. 0007cases hmle
  8. 0008have hsum : (h + x + 1) + m = p
  9. 0009trans h + (x + m) + 1
  10. 0010simp [add_assoc, add_comm]
  11. 0011congr
  12. 0012trans (m + x) + h
  13. 0013symm
  14. 0014apply add_assoc
  15. 0015trans (x + m) + h
  16. 0016congr
  17. 0017apply add_comm
  18. 0018refl
  19. 0019apply add_assoc
  20. 0020rewrite hmle_witness
  21. 0021rewrite hp
  22. 0022trans h + h + 1
  23. 0023refl
  24. 0024congr
  25. 0025trans h * 2
  26. 0026simp [zero_add]
  27. 0027specialize mul_comm h
  28. 0028specialize mul_comm 2
  29. 0029apply mul_comm
  30. 0030refl
  31. 0031have hm0 : ~(m = 0)
  32. 0032intro hmzero
  33. 0033specialize lt_irrefl_expanded 0
  34. 0034apply lt_irrefl_expanded
  35. 0035rewrite hmzero at hmpositive
  36. 0036exact hmpositive
  37. 0037have hmsucc : exists z. m = S z
  38. 0038specialize nonzero_is_succ m
  39. 0039apply nonzero_is_succ
  40. 0040exact hm0
  41. 0041cases hmsucc
  42. 0042exists h + x + 1
  43. 0043split
  44. 0044exists x1
  45. 0045trans S (x1 + (h + x + 1))
  46. 0046apply PA4
  47. 0047trans S ((h + x + 1) + x1)
  48. 0048congr
  49. 0049apply add_comm
  50. 0050trans (h + x + 1) + S x1
  51. 0051symm
  52. 0052apply PA4
  53. 0053trans (h + x + 1) + m
  54. 0054congr
  55. 0055refl
  56. 0056symm
  57. 0057exact hmsucc_witness
  58. 0058exact hsum
  59. 0059exact hsum