BL0003

binary_length_digit_split_functional

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Binary division by two has a unique quotient and unique digit.

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.

Exact expanded first-order arithmetic statement

forall n h b k c. ((((b = 0) \/ (b = 1)) /\ n = (h + h) + b)) -> ((((c = 0) \/ (c = 1)) /\ n = (k + k) + c)) -> (h = k /\ b = c)

Constructive proof overview

Generated structural guide

Binary division by two has a unique quotient and unique digit.

The unchanged tactic script uses 3 declared prerequisites and contains 42 exact native proof lines.

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

Proof neighborhood

Direct dependencies

BL0001 binary_length_digit_bounded two_mul_eq_add_self Alpha theorem; checked-use authorized division_remainder_unique Stable theorem; checked-use authorized

Direct dependents

BL0004 binary_length_digit_split_exists_unique

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

42 script commands · 7 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 (1)
binary length digit bounded
01Fix variables and assumptionsL1–7

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

  1. L1
    intro n
  2. L2
    intro h
  3. L3
    intro b
  4. L4
    intro k
  5. L5
    intro c
  6. L6
    intro hfirst
  7. L7
    intro hsecond
02Separate the logical casesL8–9

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

  1. L8
    cases hfirst
  2. L9
    cases hsecond
03Establish hboundL10–13

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary length digit bounded.

  1. L10
    have hbound : exists gap. gap + S b = 2
  2. L11
    specialize binary_length_digit_bounded b
  3. L12
    apply binary_length_digit_bounded
  4. L13
    exact hfirst_left
04Establish kboundL14–17

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary length digit bounded.

  1. L14
    have kbound : exists gap. gap + S c = 2
  2. L15
    specialize binary_length_digit_bounded c
  3. L16
    apply binary_length_digit_bounded
  4. L17
    exact hsecond_left
05Establish hequationL18–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply two mul eq add self.

  1. L18
    have hequation : n = 2 * h + b
  2. L19
    trans (h + h) + b
  3. L20
    exact hfirst_right
  4. L21
    congr
  5. L22
    symm
  6. L23
    apply two_mul_eq_add_self
  7. L24
    refl
06Establish kequationL25–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply two mul eq add self.

  1. L25
    have kequation : n = 2 * k + c
  2. L26
    trans (k + k) + c
  3. L27
    exact hsecond_right
  4. L28
    congr
  5. L29
    symm
  6. L30
    apply two_mul_eq_add_self
  7. L31
    refl
  8. L32
    specialize division_remainder_unique 2
  9. L33
    specialize division_remainder_unique n
  10. L34
    specialize division_remainder_unique h
07Use earlier factsL35–42

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

  1. L35
    specialize division_remainder_unique b
  2. L36
    specialize division_remainder_unique k
  3. L37
    specialize division_remainder_unique c
  4. L38
    apply division_remainder_unique
  5. L39
    exact hequation
  6. L40
    exact hbound
  7. L41
    exact kequation
  8. L42
    exact kbound

Library-wide reading audit

Original exact command ledger · 42 lines
  1. 0001intro n
  2. 0002intro h
  3. 0003intro b
  4. 0004intro k
  5. 0005intro c
  6. 0006intro hfirst
  7. 0007intro hsecond
  8. 0008cases hfirst
  9. 0009cases hsecond
  10. 0010have hbound : exists gap. gap + S b = 2
  11. 0011specialize binary_length_digit_bounded b
  12. 0012apply binary_length_digit_bounded
  13. 0013exact hfirst_left
  14. 0014have kbound : exists gap. gap + S c = 2
  15. 0015specialize binary_length_digit_bounded c
  16. 0016apply binary_length_digit_bounded
  17. 0017exact hsecond_left
  18. 0018have hequation : n = 2 * h + b
  19. 0019trans (h + h) + b
  20. 0020exact hfirst_right
  21. 0021congr
  22. 0022symm
  23. 0023apply two_mul_eq_add_self
  24. 0024refl
  25. 0025have kequation : n = 2 * k + c
  26. 0026trans (k + k) + c
  27. 0027exact hsecond_right
  28. 0028congr
  29. 0029symm
  30. 0030apply two_mul_eq_add_self
  31. 0031refl
  32. 0032specialize division_remainder_unique 2
  33. 0033specialize division_remainder_unique n
  34. 0034specialize division_remainder_unique h
  35. 0035specialize division_remainder_unique b
  36. 0036specialize division_remainder_unique k
  37. 0037specialize division_remainder_unique c
  38. 0038apply division_remainder_unique
  39. 0039exact hequation
  40. 0040exact hbound
  41. 0041exact kequation
  42. 0042exact kbound