BD0012

binary_digit_operation_count_bound

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

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

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

Constructive proof overview

Generated structural guide

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

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

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

Proof neighborhood

Direct dependencies

bit_count_bounded Stable theorem; checked-use authorized add_le_add_left Stable theorem; checked-use authorized BD000F binary_three_times_cost_normalization

Direct dependents

BD0017 binary_modular_execution_bitlength_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

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.

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

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