PA00CL

odd_reflected_remainder_mod_two

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

Reflecting two remainders across an odd modulus flips parity.

Exact expanded PA statement

forall p r m. (exists sdp_odd_prime_like_modulus. p = 2 * sdp_odd_prime_like_modulus + 1) -> r + m = p -> (exists sdp_u_reflected_remainder sdp_v_reflected_remainder. (r) + 2 * sdp_u_reflected_remainder = (m + 1) + 2 * sdp_v_reflected_remainder)

Structural proof guide

Generated structural guide

Reflecting two remainders across an odd modulus flips parity.

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

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

Referenced ingredients

PA0009 add_assoc PA000F add_comm PA000H mul_comm PA0001 zero_add PA000E add_succ_left

Proof neighborhood

Direct dependencies

PA0009 add_assoc PA000F add_comm PA000H mul_comm PA0001 zero_add PA000E add_succ_left

Direct dependents

PA00CM signed_remainder_sum_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 r
  3. 0003intro m
  4. 0004intro hp
  5. 0005intro hreflect
  6. 0006cases hp
  7. 0007have hdouble : 2 * m = m + m
  8. 0008trans m * 2
  9. 0009apply mul_comm
  10. 0010simp [zero_add]
  11. 0011exists m
  12. 0012exists x
  13. 0013trans r + (m + m)
  14. 0014congr
  15. 0015refl
  16. 0016exact hdouble
  17. 0017trans (r + m) + m
  18. 0018symm
  19. 0019apply add_assoc
  20. 0020trans p + m
  21. 0021rewrite hreflect
  22. 0022refl
  23. 0023trans (2 * x + 1) + m
  24. 0024rewrite hp_witness
  25. 0025refl
  26. 0026simp [add_assoc, add_comm]
  27. 0027apply add_succ_left