PA00D2

mod_two_cancel_middle

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

From x == q+x+s modulo two, cancel x and obtain 0 == q+s.

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 q s. (exists fspm_u_cancel_middle_input fspm_v_cancel_middle_input. (x) + 2 * fspm_u_cancel_middle_input = (q + x + s) + 2 * fspm_v_cancel_middle_input) -> (exists fspm_u_cancel_middle_result fspm_v_cancel_middle_result. (0) + 2 * fspm_u_cancel_middle_result = (q + s) + 2 * fspm_v_cancel_middle_result)

Structural proof guide

Generated structural guide

From x == q+x+s modulo two, cancel x and obtain 0 == q+s.

Use the direct prerequisites mod_eq_add_cancel_left, add_assoc, add_comm as previously established PA formulas.

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

Referenced ingredients

PA00D1 mod_eq_add_cancel_left PA0009 add_assoc PA000F add_comm

Proof neighborhood

Direct dependencies

PA00D1 mod_eq_add_cancel_left PA0009 add_assoc PA000F add_comm

Direct dependents

PA00D3 gauss_eisenstein_terminal_cancel_magnitude_mod_two

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

16 script commands · 3 reading checkpoints · 2 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 (1)
mod eq add cancel left
01Fix variables and assumptionsL1–4

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

  1. L1
    intro x
  2. L2
    intro q
  3. L3
    intro s
  4. L4
    intro hmod
02Establish hreorderL5–12

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

  1. L5
    have hreorder : q + x + s = x + (q + s)
  2. L6
    simp [add_assoc, add_comm]
  3. L7
    rewrite hreorder at hmod
  4. L8
    specialize mod_eq_add_cancel_left 2
  5. L9
    specialize mod_eq_add_cancel_left x
  6. L10
    specialize mod_eq_add_cancel_left 0
  7. L11
    specialize mod_eq_add_cancel_left (q + s)
  8. L12
    apply mod_eq_add_cancel_left
03Establish hxzeroL13–16

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

  1. L13
    have hxzero : x + 0 = x
  2. L14
    apply PA3
  3. L15
    rewrite hxzero
  4. L16
    exact hmod

Library-wide reading audit

Original exact command ledger · 16 lines
  1. 0001intro x
  2. 0002intro q
  3. 0003intro s
  4. 0004intro hmod
  5. 0005have hreorder : q + x + s = x + (q + s)
  6. 0006simp [add_assoc, add_comm]
  7. 0007rewrite hreorder at hmod
  8. 0008specialize mod_eq_add_cancel_left 2
  9. 0009specialize mod_eq_add_cancel_left x
  10. 0010specialize mod_eq_add_cancel_left 0
  11. 0011specialize mod_eq_add_cancel_left (q + s)
  12. 0012apply mod_eq_add_cancel_left
  13. 0013have hxzero : x + 0 = x
  14. 0014apply PA3
  15. 0015rewrite hxzero
  16. 0016exact hmod