BD000F

binary_three_times_cost_normalization

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

Alpha v34 checked-use · first admitted v23 · 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.

The exact G102 milestone is fully proved for every natural exponent and every modulus greater than one, including actual canonical digits, a beta-coded accumulator execution, modular-power correctness, and the formal bound k≤3·BitLen(e)+2. The independent T13 determinant/rank/integer-span substrate is now closed in the separate Alpha-v27 integer-linear-algebra branch. Full T13 proof · Alpha v27

Exact theorem in conservative defined notation

∀ l. 2 + (l + l) + l = 3 · l + 2

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

Definition DAG

none

Actual proof prerequisites

mul_succ_left · checked external prerequisitetwo_mul_eq_add_self · checked external prerequisiteadd_assoc · checked external prerequisiteadd_comm · checked external prerequisite
Original expanded first-order statement 
forall l. (2 + (l + l)) + l = 3 * l + 2

Complete unchanged native tactic proof

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

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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