FS001Q · theorem body

four_square_descent_matching_parity_absolute_even

Alpha v34 checked-use · independently kernel and Lean verified; not Stable

Matching even or odd coordinate witnesses construct an explicitly even absolute difference without subtraction.

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.

Statement with defined notation

∀ a. ∀ b. Even(a) ∧ Even(b) ∨ Odd(a) ∧ Odd(b) → ∃ x. a = b + 2 · x ∨ b = a + 2 · x

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

PD0009 Even PD0010 Odd

In local proof propositions

none
Exact expanded first-order statement
forall a b. ((((exists fsd_even_first_absolute. a = 2 * fsd_even_first_absolute) /\ (exists fsd_even_second_absolute. b = 2 * fsd_even_second_absolute)) \/ ((exists fsd_odd_first_absolute. a = 2 * fsd_odd_first_absolute + 1) /\ (exists fsd_odd_second_absolute. b = 2 * fsd_odd_second_absolute + 1)))) -> exists v. ((a = b + 2 * v) \/ (b = a + 2 * v))

Proof neighborhood

Direct theorem prerequisites

FS000H four_square_absolute_difference_total mul_add · Stable closed FS002N four_square_euler_add_swap_last

Direct theorem dependents

FS001T four_square_descent_even_multiplier_matching_parity_halving

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

Read the argument

Proof checkpoints

48 script commands · 25 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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (2)
four square absolute difference totalfour square euler add swap last
01Fix variables and assumptionsL1–3

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro hmatching
02Separate the logical casesL4–7

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

  1. L4
    cases hmatching
  2. L5
    cases hmatching_left
  3. L6
    cases hmatching_left_left
  4. L7
    cases hmatching_left_right
03Establish hgapL8–9

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square absolute difference total.

  1. L8
    have hgap : exists v. x = x1 + v \/ x1 = x + v
  2. L9
    apply four_square_absolute_difference_total
04Separate the logical casesL10–10

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

  1. L10
    cases hgap
05Construct an explicit witnessL11–11

Supply the displayed value, then prove that it has the required property.

  1. L11
    exists x2
06Separate the logical casesL12–13

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

  1. L12
    cases hgap_witness
  2. L13
    left
07Calculate and transport equalitiesL14–16

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L14
    rewrite hmatching_left_left_witness
  2. L15
    rewrite hmatching_left_right_witness
  3. L16
    rewrite hgap_witness_left
08Use earlier factsL17–17

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

  1. L17
    apply mul_add
09Separate the logical casesL18–18

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

  1. L18
    right
10Calculate and transport equalitiesL19–21

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L19
    rewrite hmatching_left_right_witness
  2. L20
    rewrite hmatching_left_left_witness
  3. L21
    rewrite hgap_witness_right
11Use earlier factsL22–22

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

  1. L22
    apply mul_add
12Separate the logical casesL23–25

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

  1. L23
    cases hmatching_right
  2. L24
    cases hmatching_right_left
  3. L25
    cases hmatching_right_right
13Establish hgapL26–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square absolute difference total.

  1. L26
    have hgap : exists v. x = x1 + v \/ x1 = x + v
  2. L27
    apply four_square_absolute_difference_total
14Separate the logical casesL28–28

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

  1. L28
    cases hgap
15Construct an explicit witnessL29–29

Supply the displayed value, then prove that it has the required property.

  1. L29
    exists x2
16Separate the logical casesL30–31

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

  1. L30
    cases hgap_witness
  2. L31
    left
17Calculate and transport equalitiesL32–36

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L32
    rewrite hmatching_right_left_witness
  2. L33
    rewrite hmatching_right_right_witness
  3. L34
    rewrite hgap_witness_left
  4. L35
    trans (2 * x1 + 2 * x2) + 1
  5. L36
    congr
18Use earlier factsL37–37

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

  1. L37
    apply mul_add
19Calculate and transport equalitiesL38–38

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L38
    refl
20Use earlier factsL39–39

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

  1. L39
    apply four_square_euler_add_swap_last
21Separate the logical casesL40–40

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

  1. L40
    right
22Calculate and transport equalitiesL41–45

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L41
    rewrite hmatching_right_right_witness
  2. L42
    rewrite hmatching_right_left_witness
  3. L43
    rewrite hgap_witness_right
  4. L44
    trans (2 * x + 2 * x2) + 1
  5. L45
    congr
23Use earlier factsL46–46

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

  1. L46
    apply mul_add
24Calculate and transport equalitiesL47–47

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L47
    refl
25Use earlier factsL48–48

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

  1. L48
    apply four_square_euler_add_swap_last

Library-wide reading audit

Original defined command ledger · 48 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro hmatching
  4. 0004cases hmatching
  5. 0005cases hmatching_left
  6. 0006cases hmatching_left_left
  7. 0007cases hmatching_left_right
  8. 0008have hgap : exists v. x = x1 + v \/ x1 = x + v
  9. 0009apply four_square_absolute_difference_total
  10. 0010cases hgap
  11. 0011exists x2
  12. 0012cases hgap_witness
  13. 0013left
  14. 0014rewrite hmatching_left_left_witness
  15. 0015rewrite hmatching_left_right_witness
  16. 0016rewrite hgap_witness_left
  17. 0017apply mul_add
  18. 0018right
  19. 0019rewrite hmatching_left_right_witness
  20. 0020rewrite hmatching_left_left_witness
  21. 0021rewrite hgap_witness_right
  22. 0022apply mul_add
  23. 0023cases hmatching_right
  24. 0024cases hmatching_right_left
  25. 0025cases hmatching_right_right
  26. 0026have hgap : exists v. x = x1 + v \/ x1 = x + v
  27. 0027apply four_square_absolute_difference_total
  28. 0028cases hgap
  29. 0029exists x2
  30. 0030cases hgap_witness
  31. 0031left
  32. 0032rewrite hmatching_right_left_witness
  33. 0033rewrite hmatching_right_right_witness
  34. 0034rewrite hgap_witness_left
  35. 0035trans (2 * x1 + 2 * x2) + 1
  36. 0036congr
  37. 0037apply mul_add
  38. 0038refl
  39. 0039apply four_square_euler_add_swap_last
  40. 0040right
  41. 0041rewrite hmatching_right_right_witness
  42. 0042rewrite hmatching_right_left_witness
  43. 0043rewrite hgap_witness_right
  44. 0044trans (2 * x + 2 * x2) + 1
  45. 0045congr
  46. 0046apply mul_add
  47. 0047refl
  48. 0048apply four_square_euler_add_swap_last