PA00D5

mod_two_zero_sum_to_congruent

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

If q+e is zero modulo two, q and e have the same parity and are congruent.

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 q e. (exists fspm_u_zero_sum_input fspm_v_zero_sum_input. (0) + 2 * fspm_u_zero_sum_input = (q + e) + 2 * fspm_v_zero_sum_input) -> (exists fspm_u_zero_sum_result fspm_v_zero_sum_result. (q) + 2 * fspm_u_zero_sum_result = (e) + 2 * fspm_v_zero_sum_result)

Structural proof guide

Generated structural guide

If q+e is zero modulo two, q and e have the same parity and are congruent.

Use the direct prerequisites mod_eq_symm, mod_two_zero_to_even, even_sum_parity_cases, matching_parity_mod_two as previously established PA formulas.

The proof proceeds by intermediate claims (3).

Referenced ingredients

PA003L mod_eq_symm PA00D4 mod_two_zero_to_even PA00CA even_sum_parity_cases PA00CJ matching_parity_mod_two

Proof neighborhood

Direct dependencies

PA003L mod_eq_symm PA00D4 mod_two_zero_to_even PA00CA even_sum_parity_cases PA00CJ matching_parity_mod_two

Direct dependents

PA00D6 gauss_eisenstein_sign_count_mod_quotient_sum

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

22 script commands · 4 reading checkpoints · 3 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)
mod eq symmmod two zero to eveneven sum parity casesmatching parity mod two
01Fix variables and assumptionsL1–3

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

  1. L1
    intro q
  2. L2
    intro e
  3. L3
    intro hzero
02Establish hsum_zeroL4–9

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

  1. L4
    have hsum_zero : exists fspm_u_sum_zero fspm_v_sum_zero. (q + e) + 2 * fspm_u_sum_zero = (0) + 2 * fspm_v_sum_zero
  2. L5
    specialize mod_eq_symm 2
  3. L6
    specialize mod_eq_symm 0
  4. L7
    specialize mod_eq_symm (q + e)
  5. L8
    apply mod_eq_symm
  6. L9
    exact hzero
03Establish hevenL10–13

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

  1. L10
    have heven : exists fspm_even_sum. q + e = 2 * fspm_even_sum
  2. L11
    specialize mod_two_zero_to_even (q + e)
  3. L12
    apply mod_two_zero_to_even
  4. L13
    exact hsum_zero
04Establish hsameL14–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply even sum parity cases.

  1. L14
    have hsame : (((exists fspm_even_q. q = 2 * fspm_even_q) /\ (exists fspm_even_e. e = 2 * fspm_even_e)) \/ ((exists fspm_odd_q. q = 2 * fspm_odd_q + 1) /\ (exists fspm_odd_e. e = 2 * fspm_odd_e + 1)))
  2. L15
    specialize even_sum_parity_cases q
  3. L16
    specialize even_sum_parity_cases e
  4. L17
    apply even_sum_parity_cases
  5. L18
    exact heven
  6. L19
    specialize matching_parity_mod_two q
  7. L20
    specialize matching_parity_mod_two e
  8. L21
    apply matching_parity_mod_two
  9. L22
    exact hsame

Library-wide reading audit

Original exact command ledger · 22 lines
  1. 0001intro q
  2. 0002intro e
  3. 0003intro hzero
  4. 0004have hsum_zero : exists fspm_u_sum_zero fspm_v_sum_zero. (q + e) + 2 * fspm_u_sum_zero = (0) + 2 * fspm_v_sum_zero
  5. 0005specialize mod_eq_symm 2
  6. 0006specialize mod_eq_symm 0
  7. 0007specialize mod_eq_symm (q + e)
  8. 0008apply mod_eq_symm
  9. 0009exact hzero
  10. 0010have heven : exists fspm_even_sum. q + e = 2 * fspm_even_sum
  11. 0011specialize mod_two_zero_to_even (q + e)
  12. 0012apply mod_two_zero_to_even
  13. 0013exact hsum_zero
  14. 0014have hsame : (((exists fspm_even_q. q = 2 * fspm_even_q) /\ (exists fspm_even_e. e = 2 * fspm_even_e)) \/ ((exists fspm_odd_q. q = 2 * fspm_odd_q + 1) /\ (exists fspm_odd_e. e = 2 * fspm_odd_e + 1)))
  15. 0015specialize even_sum_parity_cases q
  16. 0016specialize even_sum_parity_cases e
  17. 0017apply even_sum_parity_cases
  18. 0018exact heven
  19. 0019specialize matching_parity_mod_two q
  20. 0020specialize matching_parity_mod_two e
  21. 0021apply matching_parity_mod_two
  22. 0022exact hsame