BL0003

binary_length_digit_split_functional

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

Alpha v34 checked-use · first admitted v22 · 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. Exact original first-admission records.

G101 and G102 were OPEN when these BitLen foundations were first admitted in Alpha v22. Both are now CLOSED in Alpha v23: complete canonical exponent digits and both exact logarithmic execution bounds are proved.

Exact theorem in conservative defined notation

∀ n. ∀ h. ∀ b. ∀ k. ∀ c. BinaryExponentSplit(n,h,b) → BinaryExponentSplit(n,k,c) → h = k ∧ b = c

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

Definition DAG

BinaryExponentSplit(e,h,b) · 2

Actual proof prerequisites

binary_length_digit_boundedtwo_mul_eq_add_self · checked external prerequisitedivision_remainder_unique · checked external prerequisite
Original expanded first-order 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)

Complete unchanged native tactic proof

All 42 lines are the exact independently kernel-checked original script.

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.

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