MV0002

alternating_signed_unit_functional

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

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Mobius(n,z) is positive-domain only, independently defined from squarefreeness and actual prime-factor parity. Signed codes 0, 2 and 1 represent zero, +1 and -1. This family proves values and prime-adjunction laws; the separate Möbius-inversion family supplies the complete G007 endpoint.

Exact theorem in conservative defined notation

∀ n. ∀ a. ∀ b. AlternatingSignedUnit(n,a) → AlternatingSignedUnit(n,b) → a = b

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

AlternatingSignedUnit(n,z) · 2

Actual proof prerequisites

even_not_odd · checked external prerequisiteodd_not_even · checked external prerequisite
Original expanded first-order 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

Complete tactic proof in conservative notation

All 32 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

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.

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–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 defined 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