MV0002

alternating_signed_unit_functional

Public research checkpoint, not admitted to Alpha or Stable. Alpha v30 remains 3222 checked-use theorems; Stable remains 432. The on-demand Alpha Lean service does not yet expose these checkpoint theorems; their independently checked literal bundles and unchanged sources are available below.

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable

Constructive parity exclusivity makes the signed alternating-unit code unique.

Exact expanded first-order arithmetic statement

forall n a b. ((((exists mv_even_half_firsteven. (n) = 2 * mv_even_half_firsteven) /\ ((a) = 2))) \/ (((exists mv_odd_half_firstodd. (n) = 2 * mv_odd_half_firstodd + 1) /\ ((a) = 1)))) -> ((((exists mv_even_half_secondeven. (n) = 2 * mv_even_half_secondeven) /\ ((b) = 2))) \/ (((exists mv_odd_half_secondodd. (n) = 2 * mv_odd_half_secondodd + 1) /\ ((b) = 1)))) -> a = b

Constructive proof overview

Generated structural guide

Constructive parity exclusivity makes the signed alternating-unit code unique.

The unchanged tactic script uses 2 declared prerequisites and contains 32 exact native proof lines.

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable

Proof neighborhood

Direct dependencies

even_not_odd Alpha theorem; checked-use authorized odd_not_even Alpha theorem; checked-use authorized

Direct dependents

MV000B mobius_value_functional MV0013 alternating_signed_unit_successor_negates

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. The literal dependency-closed bundle is checked by original HA and the independently compiled Lean verifier. Public delivery grants no Alpha checked-use authority or Stable membership.

Read the argument

Proof checkpoints

32 script commands · 15 reading checkpoints · 0 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.

01Fix variables and assumptionsL1–5

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

  1. L1
    intro n
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro ha
  5. L5
    intro hb
02Separate the logical casesL6–9

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

  1. L6
    cases ha
  2. L7
    cases ha_left
  3. L8
    cases hb
  4. L9
    cases hb_left
03Calculate and transport equalitiesL10–10

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

  1. L10
    trans 2
04Use earlier factsL11–11

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

  1. L11
    exact ha_left_right
05Calculate and transport equalitiesL12–12

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

  1. L12
    symm
06Use earlier factsL13–13

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

  1. L13
    exact hb_left_right
07Separate the logical casesL14–15

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

  1. L14
    cases hb_right
  2. L15
    exfalso
08Use earlier factsL16–19

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

  1. L16
    specialize even_not_odd (n)
  2. L17
    apply even_not_odd
  3. L18
    exact ha_left_left
  4. L19
    exact hb_right_left
09Separate the logical casesL20–23

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

  1. L20
    cases ha_right
  2. L21
    cases hb
  3. L22
    cases hb_left
  4. L23
    exfalso
10Use earlier factsL24–27

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

  1. L24
    specialize odd_not_even (n)
  2. L25
    apply odd_not_even
  3. L26
    exact ha_right_left
  4. L27
    exact hb_left_left
11Separate the logical casesL28–28

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

  1. L28
    cases hb_right
12Calculate and transport equalitiesL29–29

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

  1. L29
    trans 1
13Use earlier factsL30–30

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

  1. L30
    exact ha_right_right
14Calculate and transport equalitiesL31–31

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

  1. L31
    symm
15Use earlier factsL32–32

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

  1. L32
    exact hb_right_right

Library-wide reading audit

Original exact command ledger · 32 lines
  1. 0001intro n
  2. 0002intro a
  3. 0003intro b
  4. 0004intro ha
  5. 0005intro hb
  6. 0006cases ha
  7. 0007cases ha_left
  8. 0008cases hb
  9. 0009cases hb_left
  10. 0010trans 2
  11. 0011exact ha_left_right
  12. 0012symm
  13. 0013exact hb_left_right
  14. 0014cases hb_right
  15. 0015exfalso
  16. 0016specialize even_not_odd (n)
  17. 0017apply even_not_odd
  18. 0018exact ha_left_left
  19. 0019exact hb_right_left
  20. 0020cases ha_right
  21. 0021cases hb
  22. 0022cases hb_left
  23. 0023exfalso
  24. 0024specialize odd_not_even (n)
  25. 0025apply odd_not_even
  26. 0026exact ha_right_left
  27. 0027exact hb_left_left
  28. 0028cases hb_right
  29. 0029trans 1
  30. 0030exact ha_right_right
  31. 0031symm
  32. 0032exact hb_right_right