PA006Y

odd_upper_remainder_reflection

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

A residue strictly above h and below 2*h+1 has a positive reflected magnitude at most h.

Exact expanded PA statement

forall p h r. p = 2 * h + 1 -> (exists gsh_lt_gap_reflection_remainder. gsh_lt_gap_reflection_remainder + S r = p) -> (exists gsh_lt_gap_reflection_upper. gsh_lt_gap_reflection_upper + S h = r) -> (exists m. (exists gsh_lt_gap_reflection_positive. gsh_lt_gap_reflection_positive + S 0 = m) /\ ((exists gsh_le_gap_reflection_bounded. gsh_le_gap_reflection_bounded + m = h) /\ r + m = p))

Structural proof guide

Generated structural guide

A residue strictly above h and below 2*h+1 has a positive reflected magnitude at most h.

Use the direct prerequisites add_assoc, add_comm, mul_succ_left, mul_zero_left, zero_add, add_right_cancel as previously established PA formulas.

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

Referenced ingredients

PA0009 add_assoc PA000F add_comm PA000G mul_succ_left PA000D mul_zero_left PA0001 zero_add PA0012 add_right_cancel

Proof neighborhood

Direct dependencies

PA0009 add_assoc PA000F add_comm PA000G mul_succ_left PA000D mul_zero_left PA0001 zero_add PA0012 add_right_cancel

Direct dependents

PA0070 gauss_pointwise_signed_half_representative

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 r
  4. 0004intro hp
  5. 0005intro hrp
  6. 0006intro hhr
  7. 0007cases hhr
  8. 0008cases hrp
  9. 0009have hrm : r + S x1 = p
  10. 0010trans S (r + x1)
  11. 0011apply PA4
  12. 0012trans S (x1 + r)
  13. 0013congr
  14. 0014apply add_comm
  15. 0015trans x1 + S r
  16. 0016symm
  17. 0017apply PA4
  18. 0018exact hrp_witness
  19. 0019have hsum : (x + S x1) + S h = h + S h
  20. 0020trans (x + S h) + S x1
  21. 0021trans x + (S x1 + S h)
  22. 0022apply add_assoc
  23. 0023trans x + (S h + S x1)
  24. 0024congr
  25. 0025refl
  26. 0026apply add_comm
  27. 0027symm
  28. 0028apply add_assoc
  29. 0029trans r + S x1
  30. 0030congr
  31. 0031exact hhr_witness
  32. 0032refl
  33. 0033trans p
  34. 0034exact hrm
  35. 0035rewrite hp
  36. 0036simp [mul_succ_left, mul_zero_left, zero_add, add_assoc]
  37. 0037have hmle : exists d. d + S x1 = h
  38. 0038exists x
  39. 0039specialize add_right_cancel (x + S x1)
  40. 0040specialize add_right_cancel h
  41. 0041specialize add_right_cancel (S h)
  42. 0042apply add_right_cancel
  43. 0043exact hsum
  44. 0044exists (S x1)
  45. 0045split
  46. 0046exists x1
  47. 0047simp
  48. 0048split
  49. 0049exact hmle
  50. 0050exact hrm