MV0013

alternating_signed_unit_successor_negates

The alternating unit at the successor exponent is the canonical signed negation, proved by the two constructive parity cases.

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(S n,b) → SignedNegate(a,b)

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

Definition DAG

SignedNegate(a,b) · 1AlternatingSignedUnit(n,z) · 4

Actual proof prerequisites

successor_odd_of_even · checked external prerequisitesuccessor_even_of_odd · checked external prerequisitealternating_signed_unit_functionalmobius_positive_unit_negates_to_negative_unitsigned_negate_symmetric · checked external prerequisite
Original expanded first-order statement 
forall n a b. ((((exists mv_even_half_successor_sourceeven. (n) = 2 * mv_even_half_successor_sourceeven) /\ ((a) = 2))) \/ (((exists mv_odd_half_successor_sourceodd. (n) = 2 * mv_odd_half_successor_sourceodd + 1) /\ ((a) = 1)))) -> ((((exists mv_even_half_successor_targeteven. (S n) = 2 * mv_even_half_successor_targeteven) /\ ((b) = 2))) \/ (((exists mv_odd_half_successor_targetodd. (S n) = 2 * mv_odd_half_successor_targetodd + 1) /\ ((b) = 1)))) -> (exists mps_positive_successor_negation mps_negative_successor_negation. (((((a) = 2 * (mps_positive_successor_negation) /\ (mps_negative_successor_negation) = 0) \/ exists ge_signed_half_successor_negationsource. (((a) = 2 * ge_signed_half_successor_negationsource + 1 /\ (mps_positive_successor_negation) = 0) /\ (mps_negative_successor_negation) = S ge_signed_half_successor_negationsource))) /\ ((((b) = 2 * (mps_negative_successor_negation) /\ (mps_positive_successor_negation) = 0) \/ exists ge_signed_half_successor_negationtarget. (((b) = 2 * ge_signed_half_successor_negationtarget + 1 /\ (mps_negative_successor_negation) = 0) /\ (mps_positive_successor_negation) = S ge_signed_half_successor_negationtarget)))))

Complete tactic proof in conservative notation

All 49 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

49 script commands · 17 reading checkpoints · 4 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)
alternating signed unit functionalmobius positive unit negates to negative unit
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–7

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

  1. L6
    cases ha
  2. L7
    cases ha_left
03Establish hsL8–8

Establish this local claim before using it. It is not an additional assumption.

  1. L8
    have hs : AlternatingSignedUnit(S n,1)Definitions: AlternatingSignedUnit(S n,1)Original native command in the exact edition
04Separate the logical casesL9–10

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

  1. L9
    right
  2. L10
    split
05Use earlier factsL11–13

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

  1. L11
    specialize successor_odd_of_even (n)
  2. L12
    apply successor_odd_of_even
  3. L13
    exact ha_left_left
06Calculate and transport equalitiesL14–14

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

  1. L14
    refl
07Establish heqL15–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply alternating signed unit functional.

  1. L15
    have heq : b = 1
  2. L16
    specialize alternating_signed_unit_functional (S n)
  3. L17
    specialize alternating_signed_unit_functional (b)
  4. L18
    specialize alternating_signed_unit_functional (1)
  5. L19
    apply alternating_signed_unit_functional
  6. L20
    exact hb
  7. L21
    exact hs
  8. L22
    rewrite ha_left_right
  9. L23
    rewrite ha_left_right
  10. L24
    rewrite heq
08Calculate and transport equalitiesL25–25

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

  1. L25
    rewrite heq
09Use earlier factsL26–26

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

  1. L26
    apply mobius_positive_unit_negates_to_negative_unit
10Separate the logical casesL27–27

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

  1. L27
    cases ha_right
11Establish hsL28–28

Establish this local claim before using it. It is not an additional assumption.

  1. L28
    have hs : AlternatingSignedUnit(S n,2)Definitions: AlternatingSignedUnit(S n,2)Original native command in the exact edition
12Separate the logical casesL29–30

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

  1. L29
    left
  2. L30
    split
13Use earlier factsL31–33

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

  1. L31
    specialize successor_even_of_odd (n)
  2. L32
    apply successor_even_of_odd
  3. L33
    exact ha_right_left
14Calculate and transport equalitiesL34–34

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

  1. L34
    refl
15Establish heqL35–44

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply alternating signed unit functional.

  1. L35
    have heq : b = 2
  2. L36
    specialize alternating_signed_unit_functional (S n)
  3. L37
    specialize alternating_signed_unit_functional (b)
  4. L38
    specialize alternating_signed_unit_functional (2)
  5. L39
    apply alternating_signed_unit_functional
  6. L40
    exact hb
  7. L41
    exact hs
  8. L42
    rewrite ha_right_right
  9. L43
    rewrite ha_right_right
  10. L44
    rewrite heq
16Calculate and transport equalitiesL45–45

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

  1. L45
    rewrite heq
17Use earlier factsL46–49

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

  1. L46
    specialize signed_negate_symmetric (2)
  2. L47
    specialize signed_negate_symmetric (1)
  3. L48
    apply signed_negate_symmetric
  4. L49
    apply mobius_positive_unit_negates_to_negative_unit

Library-wide reading audit

Original defined command ledger · 49 lines
  1. 0001intro n
  2. 0002intro a
  3. 0003intro b
  4. 0004intro ha
  5. 0005intro hb
  6. 0006cases ha
  7. 0007cases ha_left
  8. 0008have hs : AlternatingSignedUnit(S n,1)
  9. 0009right
  10. 0010split
  11. 0011specialize successor_odd_of_even (n)
  12. 0012apply successor_odd_of_even
  13. 0013exact ha_left_left
  14. 0014refl
  15. 0015have heq : b = 1
  16. 0016specialize alternating_signed_unit_functional (S n)
  17. 0017specialize alternating_signed_unit_functional (b)
  18. 0018specialize alternating_signed_unit_functional (1)
  19. 0019apply alternating_signed_unit_functional
  20. 0020exact hb
  21. 0021exact hs
  22. 0022rewrite ha_left_right
  23. 0023rewrite ha_left_right
  24. 0024rewrite heq
  25. 0025rewrite heq
  26. 0026apply mobius_positive_unit_negates_to_negative_unit
  27. 0027cases ha_right
  28. 0028have hs : AlternatingSignedUnit(S n,2)
  29. 0029left
  30. 0030split
  31. 0031specialize successor_even_of_odd (n)
  32. 0032apply successor_even_of_odd
  33. 0033exact ha_right_left
  34. 0034refl
  35. 0035have heq : b = 2
  36. 0036specialize alternating_signed_unit_functional (S n)
  37. 0037specialize alternating_signed_unit_functional (b)
  38. 0038specialize alternating_signed_unit_functional (2)
  39. 0039apply alternating_signed_unit_functional
  40. 0040exact hb
  41. 0041exact hs
  42. 0042rewrite ha_right_right
  43. 0043rewrite ha_right_right
  44. 0044rewrite heq
  45. 0045rewrite heq
  46. 0046specialize signed_negate_symmetric (2)
  47. 0047specialize signed_negate_symmetric (1)
  48. 0048apply signed_negate_symmetric
  49. 0049apply mobius_positive_unit_negates_to_negative_unit