FS003V · theorem body

four_square_parity_odd_blocks_crossed_selection

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

If both original coordinate-pair sums are odd, one of the two crossed pairings has matching parity in each pair.

historical independently replay-verified empty-context experiment; the experiment itself persisted no certificate and granted no release authority; current checked use follows separately sealed proof bundles; no Stable promotion.

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. ∀ c. ∀ d. Odd(a + b) → Odd(c + d) → (Even(a) ∧ Even(c) ∨ Odd(a) ∧ Odd(c)) ∧ (Even(b) ∧ Even(d) ∨ Odd(b) ∧ Odd(d)) ∨ (Even(a) ∧ Even(d) ∨ Odd(a) ∧ Odd(d)) ∧ (Even(b) ∧ Even(c) ∨ Odd(b) ∧ Odd(c))

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

PD0009 Even PD0010 Odd
Exact expanded first-order statement
forall a b c d. (exists fsps_odd_odd_first. (a + b) = 2 * fsps_odd_odd_first + 1) -> (exists fsps_odd_odd_second. (c + d) = 2 * fsps_odd_odd_second + 1) -> (((((((exists fsd_even_first_fsps_odd_blocks_ac. a = 2 * fsd_even_first_fsps_odd_blocks_ac) /\ (exists fsd_even_second_fsps_odd_blocks_ac. c = 2 * fsd_even_second_fsps_odd_blocks_ac)) \/ ((exists fsd_odd_first_fsps_odd_blocks_ac. a = 2 * fsd_odd_first_fsps_odd_blocks_ac + 1) /\ (exists fsd_odd_second_fsps_odd_blocks_ac. c = 2 * fsd_odd_second_fsps_odd_blocks_ac + 1)))) /\ ((((exists fsd_even_first_fsps_odd_blocks_bd. b = 2 * fsd_even_first_fsps_odd_blocks_bd) /\ (exists fsd_even_second_fsps_odd_blocks_bd. d = 2 * fsd_even_second_fsps_odd_blocks_bd)) \/ ((exists fsd_odd_first_fsps_odd_blocks_bd. b = 2 * fsd_odd_first_fsps_odd_blocks_bd + 1) /\ (exists fsd_odd_second_fsps_odd_blocks_bd. d = 2 * fsd_odd_second_fsps_odd_blocks_bd + 1))))) \/ (((((exists fsd_even_first_fsps_odd_blocks_ad. a = 2 * fsd_even_first_fsps_odd_blocks_ad) /\ (exists fsd_even_second_fsps_odd_blocks_ad. d = 2 * fsd_even_second_fsps_odd_blocks_ad)) \/ ((exists fsd_odd_first_fsps_odd_blocks_ad. a = 2 * fsd_odd_first_fsps_odd_blocks_ad + 1) /\ (exists fsd_odd_second_fsps_odd_blocks_ad. d = 2 * fsd_odd_second_fsps_odd_blocks_ad + 1)))) /\ ((((exists fsd_even_first_fsps_odd_blocks_bc. b = 2 * fsd_even_first_fsps_odd_blocks_bc) /\ (exists fsd_even_second_fsps_odd_blocks_bc. c = 2 * fsd_even_second_fsps_odd_blocks_bc)) \/ ((exists fsd_odd_first_fsps_odd_blocks_bc. b = 2 * fsd_odd_first_fsps_odd_blocks_bc + 1) /\ (exists fsd_odd_second_fsps_odd_blocks_bc. c = 2 * fsd_odd_second_fsps_odd_blocks_bc + 1)))))))

Proof neighborhood

Direct theorem prerequisites

odd_sum_parity_cases · Alpha closed

Direct theorem dependents

FS003W four_square_parity_even_coordinate_pair_selection

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

63 script commands · 19 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.

01Fix variables and assumptionsL1–6

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro d
  5. L5
    intro hfirst_odd
  6. L6
    intro hsecond_odd
02Establish hfirstL7–11

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

  1. L7
    have hfirst : Even(a) ∧ Odd(b) ∨ Odd(a) ∧ Even(b)Definitions: Even(a)Odd(b)Odd(a)Even(b)Original native command in the exact edition
  2. L8
    specialize odd_sum_parity_cases a
  3. L9
    specialize odd_sum_parity_cases b
  4. L10
    apply odd_sum_parity_cases
  5. L11
    exact hfirst_odd
03Establish hsecondL12–14

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

  1. L12
    have hsecond : Even(c) ∧ Odd(d) ∨ Odd(c) ∧ Even(d)Definitions: Even(c)Odd(d)Odd(c)Even(d)Original native command in the exact edition
  2. L13
    apply odd_sum_parity_cases
  3. L14
    exact hsecond_odd
04Separate the logical casesL15–22

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

  1. L15
    cases hfirst
  2. L16
    cases hfirst_left
  3. L17
    cases hsecond
  4. L18
    cases hsecond_left
  5. L19
    left
  6. L20
    split
  7. L21
    left
  8. L22
    split
05Use earlier factsL23–24

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

  1. L23
    exact hfirst_left_left
  2. L24
    exact hsecond_left_left
06Separate the logical casesL25–26

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

  1. L25
    right
  2. L26
    split
07Use earlier factsL27–28

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

  1. L27
    exact hfirst_left_right
  2. L28
    exact hsecond_left_right
08Separate the logical casesL29–33

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

  1. L29
    cases hsecond_right
  2. L30
    right
  3. L31
    split
  4. L32
    left
  5. L33
    split
09Use earlier factsL34–35

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

  1. L34
    exact hfirst_left_left
  2. L35
    exact hsecond_right_right
10Separate the logical casesL36–37

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

  1. L36
    right
  2. L37
    split
11Use earlier factsL38–39

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

  1. L38
    exact hfirst_left_right
  2. L39
    exact hsecond_right_left
12Separate the logical casesL40–46

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

  1. L40
    cases hfirst_right
  2. L41
    cases hsecond
  3. L42
    cases hsecond_left
  4. L43
    right
  5. L44
    split
  6. L45
    right
  7. L46
    split
13Use earlier factsL47–48

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

  1. L47
    exact hfirst_right_left
  2. L48
    exact hsecond_left_right
14Separate the logical casesL49–50

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

  1. L49
    left
  2. L50
    split
15Use earlier factsL51–52

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

  1. L51
    exact hfirst_right_right
  2. L52
    exact hsecond_left_left
16Separate the logical casesL53–57

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

  1. L53
    cases hsecond_right
  2. L54
    left
  3. L55
    split
  4. L56
    right
  5. L57
    split
17Use earlier factsL58–59

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

  1. L58
    exact hfirst_right_left
  2. L59
    exact hsecond_right_left
18Separate the logical casesL60–61

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

  1. L60
    left
  2. L61
    split
19Use earlier factsL62–63

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

  1. L62
    exact hfirst_right_right
  2. L63
    exact hsecond_right_right

Library-wide reading audit

Original defined command ledger · 63 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro hfirst_odd
  6. 0006intro hsecond_odd
  7. 0007have hfirst : Even(a) ∧ Odd(b) ∨ Odd(a) ∧ Even(b)
    Exact native replay linehave hfirst : (((exists fsps_even_first_a_even. (a) = 2 * fsps_even_first_a_even) /\ (exists fsps_odd_first_b_odd. (b) = 2 * fsps_odd_first_b_odd + 1)) \/ ((exists fsps_odd_first_a_odd. (a) = 2 * fsps_odd_first_a_odd + 1) /\ (exists fsps_even_first_b_even. (b) = 2 * fsps_even_first_b_even)))
  8. 0008specialize odd_sum_parity_cases a
  9. 0009specialize odd_sum_parity_cases b
  10. 0010apply odd_sum_parity_cases
  11. 0011exact hfirst_odd
  12. 0012have hsecond : Even(c) ∧ Odd(d) ∨ Odd(c) ∧ Even(d)
    Exact native replay linehave hsecond : (((exists fsps_even_second_c_even. (c) = 2 * fsps_even_second_c_even) /\ (exists fsps_odd_second_d_odd. (d) = 2 * fsps_odd_second_d_odd + 1)) \/ ((exists fsps_odd_second_c_odd. (c) = 2 * fsps_odd_second_c_odd + 1) /\ (exists fsps_even_second_d_even. (d) = 2 * fsps_even_second_d_even)))
  13. 0013apply odd_sum_parity_cases
  14. 0014exact hsecond_odd
  15. 0015cases hfirst
  16. 0016cases hfirst_left
  17. 0017cases hsecond
  18. 0018cases hsecond_left
  19. 0019left
  20. 0020split
  21. 0021left
  22. 0022split
  23. 0023exact hfirst_left_left
  24. 0024exact hsecond_left_left
  25. 0025right
  26. 0026split
  27. 0027exact hfirst_left_right
  28. 0028exact hsecond_left_right
  29. 0029cases hsecond_right
  30. 0030right
  31. 0031split
  32. 0032left
  33. 0033split
  34. 0034exact hfirst_left_left
  35. 0035exact hsecond_right_right
  36. 0036right
  37. 0037split
  38. 0038exact hfirst_left_right
  39. 0039exact hsecond_right_left
  40. 0040cases hfirst_right
  41. 0041cases hsecond
  42. 0042cases hsecond_left
  43. 0043right
  44. 0044split
  45. 0045right
  46. 0046split
  47. 0047exact hfirst_right_left
  48. 0048exact hsecond_left_right
  49. 0049left
  50. 0050split
  51. 0051exact hfirst_right_right
  52. 0052exact hsecond_left_left
  53. 0053cases hsecond_right
  54. 0054left
  55. 0055split
  56. 0056right
  57. 0057split
  58. 0058exact hfirst_right_left
  59. 0059exact hsecond_right_left
  60. 0060left
  61. 0061split
  62. 0062exact hfirst_right_right
  63. 0063exact hsecond_right_right