PA00C6

odd_signed_division_branch_exact

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

A Gauss signed congruence determines the exact canonical lower/reflected remainder branch.

Exact expanded PA statement

forall p h n q r m s. p = 2 * h + 1 -> n = p * q + r -> (exists gsp_lt_gap_gsd_r_below_p. gsp_lt_gap_gsd_r_below_p + S r = p) -> (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) -> (((s = 0 /\ (exists wpp_mod_left_gsd_n_mod_m wpp_mod_right_gsd_n_mod_m. (n) + p * wpp_mod_left_gsd_n_mod_m = (m) + p * wpp_mod_right_gsd_n_mod_m)) \/ (s = 1 /\ (exists wpp_mod_left_gsd_n_mod_reflected wpp_mod_right_gsd_n_mod_reflected. (n) + p * wpp_mod_left_gsd_n_mod_reflected = ((2 * h) * m) + p * wpp_mod_right_gsd_n_mod_reflected)))) -> (((s = 0 /\ r = m) \/ (s = 1 /\ r + m = p)))

Structural proof guide

Generated structural guide

A Gauss signed congruence determines the exact canonical lower/reflected remainder branch.

Use the direct prerequisites odd_half_strictly_below_modulus, lt_of_le_of_lt, odd_half_positive_complement_exists, predecessor_multiple_mod_complement, canonical_remainder_from_mod, mod_eq_trans as previously established PA formulas.

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

Referenced ingredients

PA00C2 odd_half_strictly_below_modulus PA0033 lt_of_le_of_lt PA00C3 odd_half_positive_complement_exists PA00C4 predecessor_multiple_mod_complement PA00C5 canonical_remainder_from_mod PA0024 mod_eq_trans

Proof neighborhood

Direct dependencies

PA00C2 odd_half_strictly_below_modulus PA0033 lt_of_le_of_lt PA00C3 odd_half_positive_complement_exists PA00C4 predecessor_multiple_mod_complement PA00C5 canonical_remainder_from_mod PA0024 mod_eq_trans

Direct dependents

PA00CO odd_signed_division_congruence_mod_two

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 n
  4. 0004intro q
  5. 0005intro r
  6. 0006intro m
  7. 0007intro s
  8. 0008intro hp
  9. 0009intro hdivision
  10. 0010intro hrbelow
  11. 0011intro hmpositive
  12. 0012intro hmle
  13. 0013intro hsigned
  14. 0014have hhalfbelow : exists d. d + S h = p
  15. 0015specialize odd_half_strictly_below_modulus p
  16. 0016specialize odd_half_strictly_below_modulus h
  17. 0017apply odd_half_strictly_below_modulus
  18. 0018exact hp
  19. 0019have hmbelow : exists gsp_lt_gap_gsd_m_below_p. gsp_lt_gap_gsd_m_below_p + S m = p
  20. 0020specialize lt_of_le_of_lt m
  21. 0021specialize lt_of_le_of_lt h
  22. 0022specialize lt_of_le_of_lt p
  23. 0023apply lt_of_le_of_lt
  24. 0024exact hmle
  25. 0025exact hhalfbelow
  26. 0026cases hsigned
  27. 0027cases hsigned_left
  28. 0028left
  29. 0029split
  30. 0030exact hsigned_left_left
  31. 0031specialize canonical_remainder_from_mod p
  32. 0032specialize canonical_remainder_from_mod n
  33. 0033specialize canonical_remainder_from_mod q
  34. 0034specialize canonical_remainder_from_mod r
  35. 0035specialize canonical_remainder_from_mod m
  36. 0036apply canonical_remainder_from_mod
  37. 0037exact hdivision
  38. 0038exact hrbelow
  39. 0039exact hmbelow
  40. 0040exact hsigned_left_right
  41. 0041cases hsigned_right
  42. 0042have hcomplement : exists t. (exists gsp_lt_gap_gsd_t_below_p. gsp_lt_gap_gsd_t_below_p + S t = p) /\ t + m = p
  43. 0043specialize odd_half_positive_complement_exists p
  44. 0044specialize odd_half_positive_complement_exists h
  45. 0045specialize odd_half_positive_complement_exists m
  46. 0046apply odd_half_positive_complement_exists
  47. 0047exact hp
  48. 0048exact hmpositive
  49. 0049exact hmle
  50. 0050cases hcomplement
  51. 0051cases hcomplement_witness
  52. 0052have hpsucc : p = S (2 * h)
  53. 0053trans 2 * h + 1
  54. 0054exact hp
  55. 0055simp
  56. 0056have hkmodt : exists wpp_mod_left_gsd_local_predecessor_mod wpp_mod_right_gsd_local_predecessor_mod. ((2 * h) * m) + p * wpp_mod_left_gsd_local_predecessor_mod = (x) + p * wpp_mod_right_gsd_local_predecessor_mod
  57. 0057specialize predecessor_multiple_mod_complement p
  58. 0058specialize predecessor_multiple_mod_complement (2 * h)
  59. 0059specialize predecessor_multiple_mod_complement m
  60. 0060specialize predecessor_multiple_mod_complement x
  61. 0061apply predecessor_multiple_mod_complement
  62. 0062exact hpsucc
  63. 0063exact hcomplement_witness_right
  64. 0064have hnlocalt : exists wpp_mod_left_gsd_local_n_mod_t wpp_mod_right_gsd_local_n_mod_t. (n) + p * wpp_mod_left_gsd_local_n_mod_t = (x) + p * wpp_mod_right_gsd_local_n_mod_t
  65. 0065specialize mod_eq_trans p
  66. 0066specialize mod_eq_trans n
  67. 0067specialize mod_eq_trans ((2 * h) * m)
  68. 0068specialize mod_eq_trans x
  69. 0069apply mod_eq_trans
  70. 0070exact hsigned_right_right
  71. 0071exact hkmodt
  72. 0072have hrt : r = x
  73. 0073specialize canonical_remainder_from_mod p
  74. 0074specialize canonical_remainder_from_mod n
  75. 0075specialize canonical_remainder_from_mod q
  76. 0076specialize canonical_remainder_from_mod r
  77. 0077specialize canonical_remainder_from_mod x
  78. 0078apply canonical_remainder_from_mod
  79. 0079exact hdivision
  80. 0080exact hrbelow
  81. 0081exact hcomplement_witness_left
  82. 0082exact hnlocalt
  83. 0083right
  84. 0084split
  85. 0085exact hsigned_right_left
  86. 0086trans x + m
  87. 0087congr
  88. 0088exact hrt
  89. 0089refl
  90. 0090exact hcomplement_witness_right