PA00FR

odd_half_odd_iff_mod4_three

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

For a fixed odd decomposition, a modulo-four-three modulus is equivalent to an odd half.

Exact expanded PA statement

forall p h. p = 2 * h + 1 -> ((((exists poh_odd_half. h = 2 * poh_odd_half + 1) -> (exists poh_three_modulus. p = 4 * poh_three_modulus + 3)) /\ ((exists poh_three_modulus. p = 4 * poh_three_modulus + 3) -> (exists poh_odd_half. h = 2 * poh_odd_half + 1))))

Structural proof guide

Generated structural guide

For a fixed odd decomposition, a modulo-four-three modulus is equivalent to an odd half.

Use the direct prerequisites mul_add, four_mul_eq_double_double, odd_half_of_mod4_three_exact as previously established PA formulas.

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

Referenced ingredients

PA000A mul_add PA006R four_mul_eq_double_double PA00FQ odd_half_of_mod4_three_exact

Proof neighborhood

Direct dependencies

PA000A mul_add PA006R four_mul_eq_double_double PA00FQ odd_half_of_mod4_three_exact

Direct dependents

PA00FU qres_opposite_status_from_mod_four_three

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 hp
  4. 0004split
  5. 0005intro hodd
  6. 0006cases hodd
  7. 0007exists x
  8. 0008rewrite hp
  9. 0009rewrite hodd_witness
  10. 0010simp [mul_add]
  11. 0011congr
  12. 0012congr
  13. 0013congr
  14. 0014symm
  15. 0015apply four_mul_eq_double_double
  16. 0016intro hthree
  17. 0017cases hthree
  18. 0018exists x
  19. 0019specialize odd_half_of_mod4_three_exact p
  20. 0020specialize odd_half_of_mod4_three_exact h
  21. 0021specialize odd_half_of_mod4_three_exact x
  22. 0022apply odd_half_of_mod4_three_exact
  23. 0023exact hp
  24. 0024exact hthree_witness