PA00CO

odd_signed_division_congruence_mod_two

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

Exact signed division data gives the Gauss--Eisenstein modulo-two relation.

Exact expanded PA statement

forall p h a x n q r m s. p = 2 * h + 1 -> (exists sdp_odd_gep_scale. a = 2 * sdp_odd_gep_scale + 1) -> n = a * x -> n = p * q + r -> (exists gsp_lt_gap_gep_r_below. gsp_lt_gap_gep_r_below + S r = p) -> (exists gsp_lt_gap_gep_m_positive. gsp_lt_gap_gep_m_positive + S 0 = m) -> (exists gsp_le_gap_gep_m_bounded. gsp_le_gap_gep_m_bounded + m = h) -> (((s = 0 /\ (exists wpp_mod_left_gep_n_mod_m wpp_mod_right_gep_n_mod_m. (n) + p * wpp_mod_left_gep_n_mod_m = (m) + p * wpp_mod_right_gep_n_mod_m)) \/ (s = 1 /\ (exists wpp_mod_left_gep_n_mod_reflected wpp_mod_right_gep_n_mod_reflected. (n) + p * wpp_mod_left_gep_n_mod_reflected = ((2 * h) * m) + p * wpp_mod_right_gep_n_mod_reflected)))) -> (exists sdp_u_gep_generic_result sdp_v_gep_generic_result. (x) + 2 * sdp_u_gep_generic_result = (q + m + s) + 2 * sdp_v_gep_generic_result)

Structural proof guide

Generated structural guide

Exact signed division data gives the Gauss--Eisenstein modulo-two relation.

Use the direct prerequisites odd_signed_division_branch_exact, odd_scaled_division_signed_mod_two as previously established PA formulas.

The proof proceeds by intermediate claims (2).

Referenced ingredients

PA00C6 odd_signed_division_branch_exact PA00CN odd_scaled_division_signed_mod_two

Proof neighborhood

Direct dependencies

PA00C6 odd_signed_division_branch_exact PA00CN odd_scaled_division_signed_mod_two

Direct dependents

PA00CP gauss_eisenstein_prefix_pointwise_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 a
  4. 0004intro x
  5. 0005intro n
  6. 0006intro q
  7. 0007intro r
  8. 0008intro m
  9. 0009intro s
  10. 0010intro hp
  11. 0011intro ha
  12. 0012intro hnscale
  13. 0013intro hdivision
  14. 0014intro hrbelow
  15. 0015intro hmpositive
  16. 0016intro hmbounded
  17. 0017intro hsigned
  18. 0018have hexact : ((s = 0 /\ r = m) \/ (s = 1 /\ r + m = p))
  19. 0019specialize odd_signed_division_branch_exact p
  20. 0020specialize odd_signed_division_branch_exact h
  21. 0021specialize odd_signed_division_branch_exact n
  22. 0022specialize odd_signed_division_branch_exact q
  23. 0023specialize odd_signed_division_branch_exact r
  24. 0024specialize odd_signed_division_branch_exact m
  25. 0025specialize odd_signed_division_branch_exact s
  26. 0026apply odd_signed_division_branch_exact
  27. 0027exact hp
  28. 0028exact hdivision
  29. 0029exact hrbelow
  30. 0030exact hmpositive
  31. 0031exact hmbounded
  32. 0032exact hsigned
  33. 0033have hpodd : exists sdp_odd_gep_modulus. p = 2 * sdp_odd_gep_modulus + 1
  34. 0034exists h
  35. 0035exact hp
  36. 0036specialize odd_scaled_division_signed_mod_two p
  37. 0037specialize odd_scaled_division_signed_mod_two a
  38. 0038specialize odd_scaled_division_signed_mod_two x
  39. 0039specialize odd_scaled_division_signed_mod_two q
  40. 0040specialize odd_scaled_division_signed_mod_two r
  41. 0041specialize odd_scaled_division_signed_mod_two m
  42. 0042specialize odd_scaled_division_signed_mod_two s
  43. 0043apply odd_scaled_division_signed_mod_two
  44. 0044exact hpodd
  45. 0045exact ha
  46. 0046trans n
  47. 0047symm
  48. 0048exact hnscale
  49. 0049exact hdivision
  50. 0050exact hexact