BD000F

binary_three_times_cost_normalization

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

The initialization-plus-three-per-digit arithmetic expression is exactly 3*l+2 in the unchanged Peano kernel.

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 l. (2 + (l + l)) + l = 3 * l + 2

Constructive proof overview

Generated structural guide

The initialization-plus-three-per-digit arithmetic expression is exactly 3*l+2 in the unchanged Peano kernel.

The unchanged tactic script uses 4 declared prerequisites and contains 21 exact native proof lines.

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

Proof neighborhood

Direct dependencies

mul_succ_left Stable theorem; checked-use authorized two_mul_eq_add_self Alpha theorem; checked-use authorized add_assoc Stable theorem; checked-use authorized add_comm Stable theorem; checked-use authorized

Direct dependents

BD0012 binary_digit_operation_count_bound

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

21 script commands · 6 reading checkpoints · 1 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.

01Fix variables and assumptionsL1–1

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

  1. L1
    intro l
02Establish hthreeL2–11

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

  1. L2
    have hthree : 3 * l = (l + l) + l
  2. L3
    trans 2 * l + l
  3. L4
    specialize mul_succ_left 2
  4. L5
    specialize mul_succ_left l
  5. L6
    exact mul_succ_left
  6. L7
    congr
  7. L8
    specialize two_mul_eq_add_self l
  8. L9
    exact two_mul_eq_add_self
  9. L10
    refl
  10. L11
    trans 2 + ((l + l) + l)
03Use earlier factsL12–15

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

  1. L12
    specialize add_assoc 2
  2. L13
    specialize add_assoc (l + l)
  3. L14
    specialize add_assoc l
  4. L15
    exact add_assoc
04Calculate and transport equalitiesL16–16

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

  1. L16
    trans ((l + l) + l) + 2
05Use earlier factsL17–19

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

  1. L17
    specialize add_comm 2
  2. L18
    specialize add_comm ((l + l) + l)
  3. L19
    exact add_comm
06Calculate and transport equalitiesL20–21

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

  1. L20
    rewrite hthree
  2. L21
    refl

Library-wide reading audit

Original exact command ledger · 21 lines
  1. 0001intro l
  2. 0002have hthree : 3 * l = (l + l) + l
  3. 0003trans 2 * l + l
  4. 0004specialize mul_succ_left 2
  5. 0005specialize mul_succ_left l
  6. 0006exact mul_succ_left
  7. 0007congr
  8. 0008specialize two_mul_eq_add_self l
  9. 0009exact two_mul_eq_add_self
  10. 0010refl
  11. 0011trans 2 + ((l + l) + l)
  12. 0012specialize add_assoc 2
  13. 0013specialize add_assoc (l + l)
  14. 0014specialize add_assoc l
  15. 0015exact add_assoc
  16. 0016trans ((l + l) + l) + 2
  17. 0017specialize add_comm 2
  18. 0018specialize add_comm ((l + l) + l)
  19. 0019exact add_comm
  20. 0020rewrite hthree
  21. 0021refl

Separate complete second-wave branches: Full T13 proof · Alpha v27.