MV0013

alternating_signed_unit_successor_negates

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

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

Exact expanded first-order arithmetic 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)))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 5 declared prerequisites and contains 49 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

successor_odd_of_even Alpha theorem; checked-use authorized successor_even_of_odd Alpha theorem; checked-use authorized MV0002 alternating_signed_unit_functional MV0012 mobius_positive_unit_negates_to_negative_unit signed_negate_symmetric Alpha theorem; checked-use authorized

Direct dependents

MV0015 mobius_fresh_prime_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

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.

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 : (((exists mv_even_half_successor_oddeven. (S n) = 2 * mv_even_half_successor_oddeven) /\ ((1) = 2))) \/ (((exists mv_odd_half_successor_oddodd. (S n) = 2 * mv_odd_half_successor_oddodd + 1) /\ ((1) = 1)))
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 : (((exists mv_even_half_successor_eveneven. (S n) = 2 * mv_even_half_successor_eveneven) /\ ((2) = 2))) \/ (((exists mv_odd_half_successor_evenodd. (S n) = 2 * mv_odd_half_successor_evenodd + 1) /\ ((2) = 1)))
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 exact 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 : (((exists mv_even_half_successor_oddeven. (S n) = 2 * mv_even_half_successor_oddeven) /\ ((1) = 2))) \/ (((exists mv_odd_half_successor_oddodd. (S n) = 2 * mv_odd_half_successor_oddodd + 1) /\ ((1) = 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 : (((exists mv_even_half_successor_eveneven. (S n) = 2 * mv_even_half_successor_eveneven) /\ ((2) = 2))) \/ (((exists mv_odd_half_successor_evenodd. (S n) = 2 * mv_odd_half_successor_evenodd + 1) /\ ((2) = 1)))
  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