BD0012

binary_digit_operation_count_bound

The actual beta-counted initialization/square/optional-multiply cost of any binary prefix is at most 3*l+2.

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

∀ b. ∀ c. ∀ l. ∀ operations. BinaryExecutionOperationCount(b,c,l,operations) → Le(operations,3 · l + 2)

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

Definition DAG

BinaryExecutionOperationCount(b,c,ell,k) · 1Le(a,b) · 1

Actual proof prerequisites

bit_count_bounded · checked external prerequisiteadd_le_add_left · checked external prerequisitebinary_three_times_cost_normalization
Original expanded first-order statement 
forall b c l operations. (exists ff_ones_bd_operation_bound. ((((exists ff_u_bd_operation_bound_count_sum ff_v_bd_operation_bound_count_sum. ((((exists ff_h_bd_operation_bound_count_sum_start. ff_h_bd_operation_bound_count_sum_start + S (0) = S ((S (0)) * ff_v_bd_operation_bound_count_sum)) /\ exists ff_q_bd_operation_bound_count_sum_start. ff_u_bd_operation_bound_count_sum = ff_q_bd_operation_bound_count_sum_start * S ((S (0)) * ff_v_bd_operation_bound_count_sum) + (0))) /\ ((((exists ff_h_bd_operation_bound_count_sum_terminal. ff_h_bd_operation_bound_count_sum_terminal + S (ff_ones_bd_operation_bound) = S ((S (l)) * ff_v_bd_operation_bound_count_sum)) /\ exists ff_q_bd_operation_bound_count_sum_terminal. ff_u_bd_operation_bound_count_sum = ff_q_bd_operation_bound_count_sum_terminal * S ((S (l)) * ff_v_bd_operation_bound_count_sum) + (ff_ones_bd_operation_bound))) /\ forall ff_i_bd_operation_bound_count_sum. (exists ff_lt_bd_operation_bound_count_sum_bound. ff_lt_bd_operation_bound_count_sum_bound + S ff_i_bd_operation_bound_count_sum = l) -> exists ff_a_bd_operation_bound_count_sum ff_r_bd_operation_bound_count_sum ff_s_bd_operation_bound_count_sum. ((((exists ff_h_bd_operation_bound_count_sum_summand. ff_h_bd_operation_bound_count_sum_summand + S (ff_a_bd_operation_bound_count_sum) = S ((S (ff_i_bd_operation_bound_count_sum)) * c)) /\ exists ff_q_bd_operation_bound_count_sum_summand. b = ff_q_bd_operation_bound_count_sum_summand * S ((S (ff_i_bd_operation_bound_count_sum)) * c) + (ff_a_bd_operation_bound_count_sum))) /\ ((((exists ff_h_bd_operation_bound_count_sum_partial. ff_h_bd_operation_bound_count_sum_partial + S (ff_r_bd_operation_bound_count_sum) = S ((S (ff_i_bd_operation_bound_count_sum)) * ff_v_bd_operation_bound_count_sum)) /\ exists ff_q_bd_operation_bound_count_sum_partial. ff_u_bd_operation_bound_count_sum = ff_q_bd_operation_bound_count_sum_partial * S ((S (ff_i_bd_operation_bound_count_sum)) * ff_v_bd_operation_bound_count_sum) + (ff_r_bd_operation_bound_count_sum))) /\ ((((exists ff_h_bd_operation_bound_count_sum_successor. ff_h_bd_operation_bound_count_sum_successor + S (ff_s_bd_operation_bound_count_sum) = S ((S (S ff_i_bd_operation_bound_count_sum)) * ff_v_bd_operation_bound_count_sum)) /\ exists ff_q_bd_operation_bound_count_sum_successor. ff_u_bd_operation_bound_count_sum = ff_q_bd_operation_bound_count_sum_successor * S ((S (S ff_i_bd_operation_bound_count_sum)) * ff_v_bd_operation_bound_count_sum) + (ff_s_bd_operation_bound_count_sum))) /\ ff_s_bd_operation_bound_count_sum = ff_r_bd_operation_bound_count_sum + ff_a_bd_operation_bound_count_sum)))))) /\ (forall ff_i_bd_operation_bound_count_bits. (exists ff_lt_bd_operation_bound_count_bits_bound. ff_lt_bd_operation_bound_count_bits_bound + S ff_i_bd_operation_bound_count_bits = l) -> exists ff_bit_bd_operation_bound_count_bits. ((((exists ff_h_bd_operation_bound_count_bits_decoded. ff_h_bd_operation_bound_count_bits_decoded + S (ff_bit_bd_operation_bound_count_bits) = S ((S (ff_i_bd_operation_bound_count_bits)) * c)) /\ exists ff_q_bd_operation_bound_count_bits_decoded. b = ff_q_bd_operation_bound_count_bits_decoded * S ((S (ff_i_bd_operation_bound_count_bits)) * c) + (ff_bit_bd_operation_bound_count_bits))) /\ (ff_bit_bd_operation_bound_count_bits = 0 \/ ff_bit_bd_operation_bound_count_bits = 1))))) /\ operations = (2 + (l + l)) + ff_ones_bd_operation_bound)) -> exists gap. gap + operations = 3 * l + 2

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

26 script commands · 5 reading checkpoints · 3 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 three times cost normalization
01Fix variables and assumptionsL1–5

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro l
  4. L4
    intro operations
  5. L5
    intro hcost
02Separate the logical casesL6–7

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

  1. L6
    cases hcost
  2. L7
    cases hcost_witness
03Establish honesL8–14

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

  1. L8
    have hones : exists gap. gap + x = l
  2. L9
    specialize bit_count_bounded b
  3. L10
    specialize bit_count_bounded c
  4. L11
    specialize bit_count_bounded l
  5. L12
    specialize bit_count_bounded x
  6. L13
    apply bit_count_bounded
  7. L14
    exact hcost_witness_left
04Establish hscaledL15–20

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add le add left.

  1. L15
    have hscaled : exists gap. gap + ((2 + (l + l)) + x) = (2 + (l + l)) + l
  2. L16
    specialize add_le_add_left x
  3. L17
    specialize add_le_add_left l
  4. L18
    specialize add_le_add_left (2 + (l + l))
  5. L19
    apply add_le_add_left
  6. L20
    exact hones
05Establish hnormalL21–26

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

  1. L21
    have hnormal : (2 + (l + l)) + l = 3 * l + 2
  2. L22
    specialize binary_three_times_cost_normalization l
  3. L23
    exact binary_three_times_cost_normalization
  4. L24
    rewrite <- hcost_witness_right at hscaled
  5. L25
    rewrite hnormal at hscaled
  6. L26
    exact hscaled

Library-wide reading audit

Original defined command ledger · 26 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro operations
  5. 0005intro hcost
  6. 0006cases hcost
  7. 0007cases hcost_witness
  8. 0008have hones : exists gap. gap + x = l
  9. 0009specialize bit_count_bounded b
  10. 0010specialize bit_count_bounded c
  11. 0011specialize bit_count_bounded l
  12. 0012specialize bit_count_bounded x
  13. 0013apply bit_count_bounded
  14. 0014exact hcost_witness_left
  15. 0015have hscaled : exists gap. gap + ((2 + (l + l)) + x) = (2 + (l + l)) + l
  16. 0016specialize add_le_add_left x
  17. 0017specialize add_le_add_left l
  18. 0018specialize add_le_add_left (2 + (l + l))
  19. 0019apply add_le_add_left
  20. 0020exact hones
  21. 0021have hnormal : (2 + (l + l)) + l = 3 * l + 2
  22. 0022specialize binary_three_times_cost_normalization l
  23. 0023exact binary_three_times_cost_normalization
  24. 0024rewrite <- hcost_witness_right at hscaled
  25. 0025rewrite hnormal at hscaled
  26. 0026exact hscaled