PA0070

gauss_pointwise_signed_half_representative

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

A nonzero canonical product remainder has a positive half-range magnitude, with its sign recorded by a lower/reflected congruence disjunction.

Exact expanded PA statement

forall p h a x q r. p = 2 * h + 1 -> a * x = q * p + r -> (exists gsh_lt_gap_product_remainder. gsh_lt_gap_product_remainder + S r = p) -> ~(r = 0) -> (exists m. (exists gsh_lt_gap_product_positive. gsh_lt_gap_product_positive + S 0 = m) /\ ((exists gsh_le_gap_product_bounded. gsh_le_gap_product_bounded + m = h) /\ ((exists gsh_mod_left_product_lower gsh_mod_right_product_lower. (a * x) + p * gsh_mod_left_product_lower = (m) + p * gsh_mod_right_product_lower) \/ (exists gsh_mod_left_product_upper gsh_mod_right_product_upper. (a * x) + p * gsh_mod_left_product_upper = ((2 * h) * m) + p * gsh_mod_right_product_upper))))

Structural proof guide

Generated structural guide

A nonzero canonical product remainder has a positive half-range magnitude, with its sign recorded by a lower/reflected congruence disjunction.

Use the direct prerequisites add_assoc, add_comm, mul_succ_left, mul_one, le_or_lt, one_le_of_ne_zero, remainder_decomposition_to_mod_eq, odd_upper_remainder_reflection, mod_eq_trans as previously established PA formulas.

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

Referenced ingredients

PA0009 add_assoc PA000F add_comm PA000G mul_succ_left PA0002 mul_one PA003B le_or_lt PA002L one_le_of_ne_zero PA003C remainder_decomposition_to_mod_eq PA006Y odd_upper_remainder_reflection PA0024 mod_eq_trans

Proof neighborhood

Direct dependencies

PA0009 add_assoc PA000F add_comm PA000G mul_succ_left PA0002 mul_one PA003B le_or_lt PA002L one_le_of_ne_zero PA003C remainder_decomposition_to_mod_eq PA006Y odd_upper_remainder_reflection PA0024 mod_eq_trans

Direct dependents

PA0071 gauss_pointwise_signed_half_choice

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 a
  4. 0004intro x
  5. 0005intro q
  6. 0006intro r
  7. 0007intro hp
  8. 0008intro hdecomp
  9. 0009intro hrp
  10. 0010intro hr0
  11. 0011have hcanonical : exists gsh_mod_left_canonical_remainder gsh_mod_right_canonical_remainder. (a * x) + p * gsh_mod_left_canonical_remainder = (r) + p * gsh_mod_right_canonical_remainder
  12. 0012specialize remainder_decomposition_to_mod_eq p
  13. 0013specialize remainder_decomposition_to_mod_eq (a * x)
  14. 0014specialize remainder_decomposition_to_mod_eq q
  15. 0015specialize remainder_decomposition_to_mod_eq r
  16. 0016apply remainder_decomposition_to_mod_eq
  17. 0017exact hdecomp
  18. 0018have hsplit : (exists d. d + r = h) \/ (exists d. d + S h = r)
  19. 0019specialize le_or_lt r
  20. 0020specialize le_or_lt h
  21. 0021exact le_or_lt
  22. 0022cases hsplit
  23. 0023exists r
  24. 0024split
  25. 0025specialize one_le_of_ne_zero r
  26. 0026apply one_le_of_ne_zero
  27. 0027exact hr0
  28. 0028split
  29. 0029exact hsplit_left
  30. 0030left
  31. 0031exact hcanonical
  32. 0032have hreflection : 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)
  33. 0033specialize odd_upper_remainder_reflection p
  34. 0034specialize odd_upper_remainder_reflection h
  35. 0035specialize odd_upper_remainder_reflection r
  36. 0036apply odd_upper_remainder_reflection
  37. 0037exact hp
  38. 0038exact hrp
  39. 0039exact hsplit_right
  40. 0040cases hreflection
  41. 0041cases hreflection_witness
  42. 0042cases hreflection_witness_right
  43. 0043have hreflected_remainder : exists gsh_mod_left_reflected_remainder gsh_mod_right_reflected_remainder. (r) + p * gsh_mod_left_reflected_remainder = ((2 * h) * x1) + p * gsh_mod_right_reflected_remainder
  44. 0044exists x1
  45. 0045exists 1
  46. 0046trans (r + x1) + (2 * h) * x1
  47. 0047rewrite hp
  48. 0048trans r + (x1 + (2 * h) * x1)
  49. 0049simp
  50. 0050specialize mul_succ_left (2 * h)
  51. 0051specialize mul_succ_left x1
  52. 0052rewrite mul_succ_left
  53. 0053congr
  54. 0054refl
  55. 0055apply add_comm
  56. 0056symm
  57. 0057apply add_assoc
  58. 0058rewrite hreflection_witness_right_right
  59. 0059specialize mul_one p
  60. 0060rewrite mul_one
  61. 0061apply add_comm
  62. 0062have hreflected_product : exists gsh_mod_left_reflected_product gsh_mod_right_reflected_product. (a * x) + p * gsh_mod_left_reflected_product = ((2 * h) * x1) + p * gsh_mod_right_reflected_product
  63. 0063specialize mod_eq_trans p
  64. 0064specialize mod_eq_trans (a * x)
  65. 0065specialize mod_eq_trans r
  66. 0066specialize mod_eq_trans ((2 * h) * x1)
  67. 0067apply mod_eq_trans
  68. 0068exact hcanonical
  69. 0069exact hreflected_remainder
  70. 0070exists x1
  71. 0071split
  72. 0072exact hreflection_witness_left
  73. 0073split
  74. 0074exact hreflection_witness_right_left
  75. 0075right
  76. 0076exact hreflected_product