PA00CJ

matching_parity_mod_two

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

Naturals with the same constructive parity are congruent modulo two.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact expanded PA statement

forall x y. ((((exists sdp_even_matching_x. x = 2 * sdp_even_matching_x) /\ (exists sdp_even_matching_y. y = 2 * sdp_even_matching_y)) \/ ((exists sdp_odd_matching_x. x = 2 * sdp_odd_matching_x + 1) /\ (exists sdp_odd_matching_y. y = 2 * sdp_odd_matching_y + 1)))) -> (exists sdp_u_matching_result sdp_v_matching_result. (x) + 2 * sdp_u_matching_result = (y) + 2 * sdp_v_matching_result)

Structural proof guide

Generated structural guide

Naturals with the same constructive parity are congruent modulo two.

Use the direct prerequisites even_to_mod_two_zero, odd_to_mod_two_one, mod_eq_symm, mod_eq_trans as previously established PA formulas.

The proof proceeds by case analysis (3), intermediate claims (6).

Referenced ingredients

PA00CH even_to_mod_two_zero PA00CI odd_to_mod_two_one PA003L mod_eq_symm PA0024 mod_eq_trans

Proof neighborhood

Direct dependencies

PA00CH even_to_mod_two_zero PA00CI odd_to_mod_two_one PA003L mod_eq_symm PA0024 mod_eq_trans

Direct dependents

PA00CK odd_product_division_mod_two PA00D5 mod_two_zero_sum_to_congruent

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

Read the argument

Proof checkpoints

48 script commands · 11 reading checkpoints · 6 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (4)
even to mod two zeroodd to mod two onemod eq symmmod eq trans
01Fix variables and assumptionsL1–3

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro x
  2. L2
    intro y
  3. L3
    intro hmatching
02Separate the logical casesL4–5

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L4
    cases hmatching
  2. L5
    cases hmatching_left
03Establish hxzeroL6–9

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply even to mod two zero.

  1. L6
    have hxzero : exists sdp_u_proof_x_zero sdp_v_proof_x_zero. (x) + 2 * sdp_u_proof_x_zero = (0) + 2 * sdp_v_proof_x_zero
  2. L7
    specialize even_to_mod_two_zero x
  3. L8
    apply even_to_mod_two_zero
  4. L9
    exact hmatching_left_left
04Establish hyzeroL10–13

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply even to mod two zero.

  1. L10
    have hyzero : exists sdp_u_proof_y_zero sdp_v_proof_y_zero. (y) + 2 * sdp_u_proof_y_zero = (0) + 2 * sdp_v_proof_y_zero
  2. L11
    specialize even_to_mod_two_zero y
  3. L12
    apply even_to_mod_two_zero
  4. L13
    exact hmatching_left_right
05Establish hzeroyL14–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq symm.

  1. L14
    have hzeroy : exists sdp_u_proof_zero_y sdp_v_proof_zero_y. (0) + 2 * sdp_u_proof_zero_y = (y) + 2 * sdp_v_proof_zero_y
  2. L15
    specialize mod_eq_symm 2
  3. L16
    specialize mod_eq_symm y
  4. L17
    specialize mod_eq_symm 0
  5. L18
    apply mod_eq_symm
  6. L19
    exact hyzero
  7. L20
    specialize mod_eq_trans 2
  8. L21
    specialize mod_eq_trans x
  9. L22
    specialize mod_eq_trans 0
  10. L23
    specialize mod_eq_trans y
06Use earlier factsL24–26

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L24
    apply mod_eq_trans
  2. L25
    exact hxzero
  3. L26
    exact hzeroy
07Separate the logical casesL27–27

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L27
    cases hmatching_right
08Establish hxoneL28–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply odd to mod two one.

  1. L28
    have hxone : exists sdp_u_proof_x_one sdp_v_proof_x_one. (x) + 2 * sdp_u_proof_x_one = (1) + 2 * sdp_v_proof_x_one
  2. L29
    specialize odd_to_mod_two_one x
  3. L30
    apply odd_to_mod_two_one
  4. L31
    exact hmatching_right_left
09Establish hyoneL32–35

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply odd to mod two one.

  1. L32
    have hyone : exists sdp_u_proof_y_one sdp_v_proof_y_one. (y) + 2 * sdp_u_proof_y_one = (1) + 2 * sdp_v_proof_y_one
  2. L33
    specialize odd_to_mod_two_one y
  3. L34
    apply odd_to_mod_two_one
  4. L35
    exact hmatching_right_right
10Establish honeyL36–45

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq symm.

  1. L36
    have honey : exists sdp_u_proof_one_y sdp_v_proof_one_y. (1) + 2 * sdp_u_proof_one_y = (y) + 2 * sdp_v_proof_one_y
  2. L37
    specialize mod_eq_symm 2
  3. L38
    specialize mod_eq_symm y
  4. L39
    specialize mod_eq_symm 1
  5. L40
    apply mod_eq_symm
  6. L41
    exact hyone
  7. L42
    specialize mod_eq_trans 2
  8. L43
    specialize mod_eq_trans x
  9. L44
    specialize mod_eq_trans 1
  10. L45
    specialize mod_eq_trans y
11Use earlier factsL46–48

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L46
    apply mod_eq_trans
  2. L47
    exact hxone
  3. L48
    exact honey

Library-wide reading audit

Original exact command ledger · 48 lines
  1. 0001intro x
  2. 0002intro y
  3. 0003intro hmatching
  4. 0004cases hmatching
  5. 0005cases hmatching_left
  6. 0006have hxzero : exists sdp_u_proof_x_zero sdp_v_proof_x_zero. (x) + 2 * sdp_u_proof_x_zero = (0) + 2 * sdp_v_proof_x_zero
  7. 0007specialize even_to_mod_two_zero x
  8. 0008apply even_to_mod_two_zero
  9. 0009exact hmatching_left_left
  10. 0010have hyzero : exists sdp_u_proof_y_zero sdp_v_proof_y_zero. (y) + 2 * sdp_u_proof_y_zero = (0) + 2 * sdp_v_proof_y_zero
  11. 0011specialize even_to_mod_two_zero y
  12. 0012apply even_to_mod_two_zero
  13. 0013exact hmatching_left_right
  14. 0014have hzeroy : exists sdp_u_proof_zero_y sdp_v_proof_zero_y. (0) + 2 * sdp_u_proof_zero_y = (y) + 2 * sdp_v_proof_zero_y
  15. 0015specialize mod_eq_symm 2
  16. 0016specialize mod_eq_symm y
  17. 0017specialize mod_eq_symm 0
  18. 0018apply mod_eq_symm
  19. 0019exact hyzero
  20. 0020specialize mod_eq_trans 2
  21. 0021specialize mod_eq_trans x
  22. 0022specialize mod_eq_trans 0
  23. 0023specialize mod_eq_trans y
  24. 0024apply mod_eq_trans
  25. 0025exact hxzero
  26. 0026exact hzeroy
  27. 0027cases hmatching_right
  28. 0028have hxone : exists sdp_u_proof_x_one sdp_v_proof_x_one. (x) + 2 * sdp_u_proof_x_one = (1) + 2 * sdp_v_proof_x_one
  29. 0029specialize odd_to_mod_two_one x
  30. 0030apply odd_to_mod_two_one
  31. 0031exact hmatching_right_left
  32. 0032have hyone : exists sdp_u_proof_y_one sdp_v_proof_y_one. (y) + 2 * sdp_u_proof_y_one = (1) + 2 * sdp_v_proof_y_one
  33. 0033specialize odd_to_mod_two_one y
  34. 0034apply odd_to_mod_two_one
  35. 0035exact hmatching_right_right
  36. 0036have honey : exists sdp_u_proof_one_y sdp_v_proof_one_y. (1) + 2 * sdp_u_proof_one_y = (y) + 2 * sdp_v_proof_one_y
  37. 0037specialize mod_eq_symm 2
  38. 0038specialize mod_eq_symm y
  39. 0039specialize mod_eq_symm 1
  40. 0040apply mod_eq_symm
  41. 0041exact hyone
  42. 0042specialize mod_eq_trans 2
  43. 0043specialize mod_eq_trans x
  44. 0044specialize mod_eq_trans 1
  45. 0045specialize mod_eq_trans y
  46. 0046apply mod_eq_trans
  47. 0047exact hxone
  48. 0048exact honey