BL0015

binary_length_power_exact

The exact beta-coded power 2^e has canonical binary length e+1.

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

∀ e. ∀ p. PowTwo(e,p) → BitLen(p,S e)

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

Definition DAG

PowTwo(e,p) · 1BitLen(n,ell) · 1

Actual proof prerequisites

binary_power_two_nonzerobinary_power_two_existsbinary_power_two_strict_growthone_le_of_ne_zero · checked external prerequisitele_refl · checked external prerequisite
Original expanded first-order statement 
forall e p. (exists pa_b_bl_power pa_c_bl_power. ((forall pa_i_bl_power_repeat. (exists pa_lt_bl_power_repeat_bound. pa_lt_bl_power_repeat_bound + S pa_i_bl_power_repeat = e) -> (((exists pa_h_bl_power_repeat_decoded. pa_h_bl_power_repeat_decoded + S (2) = S ((S (pa_i_bl_power_repeat)) * pa_c_bl_power)) /\ exists pa_q_bl_power_repeat_decoded. pa_b_bl_power = pa_q_bl_power_repeat_decoded * S ((S (pa_i_bl_power_repeat)) * pa_c_bl_power) + (2)))) /\ (exists pa_u_bl_power_product pa_v_bl_power_product. ((((exists pa_h_bl_power_product_start. pa_h_bl_power_product_start + S (1) = S ((S (0)) * pa_v_bl_power_product)) /\ exists pa_q_bl_power_product_start. pa_u_bl_power_product = pa_q_bl_power_product_start * S ((S (0)) * pa_v_bl_power_product) + (1))) /\ ((((exists pa_h_bl_power_product_terminal. pa_h_bl_power_product_terminal + S (p) = S ((S (e)) * pa_v_bl_power_product)) /\ exists pa_q_bl_power_product_terminal. pa_u_bl_power_product = pa_q_bl_power_product_terminal * S ((S (e)) * pa_v_bl_power_product) + (p))) /\ forall pa_i_bl_power_product. (exists pa_lt_bl_power_product_bound. pa_lt_bl_power_product_bound + S pa_i_bl_power_product = e) -> exists pa_p_bl_power_product pa_r_bl_power_product pa_s_bl_power_product. ((((exists pa_h_bl_power_product_factor. pa_h_bl_power_product_factor + S (pa_p_bl_power_product) = S ((S (pa_i_bl_power_product)) * pa_c_bl_power)) /\ exists pa_q_bl_power_product_factor. pa_b_bl_power = pa_q_bl_power_product_factor * S ((S (pa_i_bl_power_product)) * pa_c_bl_power) + (pa_p_bl_power_product))) /\ ((((exists pa_h_bl_power_product_partial. pa_h_bl_power_product_partial + S (pa_r_bl_power_product) = S ((S (pa_i_bl_power_product)) * pa_v_bl_power_product)) /\ exists pa_q_bl_power_product_partial. pa_u_bl_power_product = pa_q_bl_power_product_partial * S ((S (pa_i_bl_power_product)) * pa_v_bl_power_product) + (pa_r_bl_power_product))) /\ ((((exists pa_h_bl_power_product_successor. pa_h_bl_power_product_successor + S (pa_s_bl_power_product) = S ((S (S pa_i_bl_power_product)) * pa_v_bl_power_product)) /\ exists pa_q_bl_power_product_successor. pa_u_bl_power_product = pa_q_bl_power_product_successor * S ((S (S pa_i_bl_power_product)) * pa_v_bl_power_product) + (pa_s_bl_power_product))) /\ pa_s_bl_power_product = pa_r_bl_power_product * pa_p_bl_power_product)))))))) -> ((((p) = 0 /\ (S e) = 1) \/ exists ff_exponent_bl_exact ff_lower_bl_exact ff_upper_bl_exact. (((S e) = S ff_exponent_bl_exact) /\ ((exists ff_positive_bl_exact. ff_positive_bl_exact + 1 = (p)) /\ ((exists pa_b_bl_exact_lower pa_c_bl_exact_lower. ((forall pa_i_bl_exact_lower_repeat. (exists pa_lt_bl_exact_lower_repeat_bound. pa_lt_bl_exact_lower_repeat_bound + S pa_i_bl_exact_lower_repeat = ff_exponent_bl_exact) -> (((exists pa_h_bl_exact_lower_repeat_decoded. pa_h_bl_exact_lower_repeat_decoded + S (2) = S ((S (pa_i_bl_exact_lower_repeat)) * pa_c_bl_exact_lower)) /\ exists pa_q_bl_exact_lower_repeat_decoded. pa_b_bl_exact_lower = pa_q_bl_exact_lower_repeat_decoded * S ((S (pa_i_bl_exact_lower_repeat)) * pa_c_bl_exact_lower) + (2)))) /\ (exists pa_u_bl_exact_lower_product pa_v_bl_exact_lower_product. ((((exists pa_h_bl_exact_lower_product_start. pa_h_bl_exact_lower_product_start + S (1) = S ((S (0)) * pa_v_bl_exact_lower_product)) /\ exists pa_q_bl_exact_lower_product_start. pa_u_bl_exact_lower_product = pa_q_bl_exact_lower_product_start * S ((S (0)) * pa_v_bl_exact_lower_product) + (1))) /\ ((((exists pa_h_bl_exact_lower_product_terminal. pa_h_bl_exact_lower_product_terminal + S (ff_lower_bl_exact) = S ((S (ff_exponent_bl_exact)) * pa_v_bl_exact_lower_product)) /\ exists pa_q_bl_exact_lower_product_terminal. pa_u_bl_exact_lower_product = pa_q_bl_exact_lower_product_terminal * S ((S (ff_exponent_bl_exact)) * pa_v_bl_exact_lower_product) + (ff_lower_bl_exact))) /\ forall pa_i_bl_exact_lower_product. (exists pa_lt_bl_exact_lower_product_bound. pa_lt_bl_exact_lower_product_bound + S pa_i_bl_exact_lower_product = ff_exponent_bl_exact) -> exists pa_p_bl_exact_lower_product pa_r_bl_exact_lower_product pa_s_bl_exact_lower_product. ((((exists pa_h_bl_exact_lower_product_factor. pa_h_bl_exact_lower_product_factor + S (pa_p_bl_exact_lower_product) = S ((S (pa_i_bl_exact_lower_product)) * pa_c_bl_exact_lower)) /\ exists pa_q_bl_exact_lower_product_factor. pa_b_bl_exact_lower = pa_q_bl_exact_lower_product_factor * S ((S (pa_i_bl_exact_lower_product)) * pa_c_bl_exact_lower) + (pa_p_bl_exact_lower_product))) /\ ((((exists pa_h_bl_exact_lower_product_partial. pa_h_bl_exact_lower_product_partial + S (pa_r_bl_exact_lower_product) = S ((S (pa_i_bl_exact_lower_product)) * pa_v_bl_exact_lower_product)) /\ exists pa_q_bl_exact_lower_product_partial. pa_u_bl_exact_lower_product = pa_q_bl_exact_lower_product_partial * S ((S (pa_i_bl_exact_lower_product)) * pa_v_bl_exact_lower_product) + (pa_r_bl_exact_lower_product))) /\ ((((exists pa_h_bl_exact_lower_product_successor. pa_h_bl_exact_lower_product_successor + S (pa_s_bl_exact_lower_product) = S ((S (S pa_i_bl_exact_lower_product)) * pa_v_bl_exact_lower_product)) /\ exists pa_q_bl_exact_lower_product_successor. pa_u_bl_exact_lower_product = pa_q_bl_exact_lower_product_successor * S ((S (S pa_i_bl_exact_lower_product)) * pa_v_bl_exact_lower_product) + (pa_s_bl_exact_lower_product))) /\ pa_s_bl_exact_lower_product = pa_r_bl_exact_lower_product * pa_p_bl_exact_lower_product)))))))) /\ ((exists pa_b_bl_exact_upper pa_c_bl_exact_upper. ((forall pa_i_bl_exact_upper_repeat. (exists pa_lt_bl_exact_upper_repeat_bound. pa_lt_bl_exact_upper_repeat_bound + S pa_i_bl_exact_upper_repeat = S e) -> (((exists pa_h_bl_exact_upper_repeat_decoded. pa_h_bl_exact_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_exact_upper_repeat)) * pa_c_bl_exact_upper)) /\ exists pa_q_bl_exact_upper_repeat_decoded. pa_b_bl_exact_upper = pa_q_bl_exact_upper_repeat_decoded * S ((S (pa_i_bl_exact_upper_repeat)) * pa_c_bl_exact_upper) + (2)))) /\ (exists pa_u_bl_exact_upper_product pa_v_bl_exact_upper_product. ((((exists pa_h_bl_exact_upper_product_start. pa_h_bl_exact_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_exact_upper_product)) /\ exists pa_q_bl_exact_upper_product_start. pa_u_bl_exact_upper_product = pa_q_bl_exact_upper_product_start * S ((S (0)) * pa_v_bl_exact_upper_product) + (1))) /\ ((((exists pa_h_bl_exact_upper_product_terminal. pa_h_bl_exact_upper_product_terminal + S (ff_upper_bl_exact) = S ((S (S e)) * pa_v_bl_exact_upper_product)) /\ exists pa_q_bl_exact_upper_product_terminal. pa_u_bl_exact_upper_product = pa_q_bl_exact_upper_product_terminal * S ((S (S e)) * pa_v_bl_exact_upper_product) + (ff_upper_bl_exact))) /\ forall pa_i_bl_exact_upper_product. (exists pa_lt_bl_exact_upper_product_bound. pa_lt_bl_exact_upper_product_bound + S pa_i_bl_exact_upper_product = S e) -> exists pa_p_bl_exact_upper_product pa_r_bl_exact_upper_product pa_s_bl_exact_upper_product. ((((exists pa_h_bl_exact_upper_product_factor. pa_h_bl_exact_upper_product_factor + S (pa_p_bl_exact_upper_product) = S ((S (pa_i_bl_exact_upper_product)) * pa_c_bl_exact_upper)) /\ exists pa_q_bl_exact_upper_product_factor. pa_b_bl_exact_upper = pa_q_bl_exact_upper_product_factor * S ((S (pa_i_bl_exact_upper_product)) * pa_c_bl_exact_upper) + (pa_p_bl_exact_upper_product))) /\ ((((exists pa_h_bl_exact_upper_product_partial. pa_h_bl_exact_upper_product_partial + S (pa_r_bl_exact_upper_product) = S ((S (pa_i_bl_exact_upper_product)) * pa_v_bl_exact_upper_product)) /\ exists pa_q_bl_exact_upper_product_partial. pa_u_bl_exact_upper_product = pa_q_bl_exact_upper_product_partial * S ((S (pa_i_bl_exact_upper_product)) * pa_v_bl_exact_upper_product) + (pa_r_bl_exact_upper_product))) /\ ((((exists pa_h_bl_exact_upper_product_successor. pa_h_bl_exact_upper_product_successor + S (pa_s_bl_exact_upper_product) = S ((S (S pa_i_bl_exact_upper_product)) * pa_v_bl_exact_upper_product)) /\ exists pa_q_bl_exact_upper_product_successor. pa_u_bl_exact_upper_product = pa_q_bl_exact_upper_product_successor * S ((S (S pa_i_bl_exact_upper_product)) * pa_v_bl_exact_upper_product) + (pa_s_bl_exact_upper_product))) /\ pa_s_bl_exact_upper_product = pa_r_bl_exact_upper_product * pa_p_bl_exact_upper_product)))))))) /\ ((exists ff_lower_gap_bl_exact. ff_lower_gap_bl_exact + (ff_lower_bl_exact) = (p)) /\ (exists ff_upper_gap_bl_exact. ff_upper_gap_bl_exact + S (p) = (ff_upper_bl_exact)))))))))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

40 script commands · 18 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 (3)
binary power two nonzerobinary power two existsbinary power two strict growth

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–3

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

  1. L1
    intro e
  2. L2
    intro p
  3. L3
    intro hp
02Establish hnonzeroL4–10

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary power two nonzero.

  1. L4
    have hnonzero : ~(p = 0)
  2. L5
    intro hzero
  3. L6
    specialize binary_power_two_nonzero e
  4. L7
    specialize binary_power_two_nonzero p
  5. L8
    apply binary_power_two_nonzero
  6. L9
    exact hp
  7. L10
    exact hzero
03Establish hpositiveL11–14

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply one le of ne zero.

  1. L11
    have hpositive : exists gap. gap + 1 = p
  2. L12
    specialize one_le_of_ne_zero p
  3. L13
    apply one_le_of_ne_zero
  4. L14
    exact hnonzero
04Establish hnextL15–17

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

  1. L15
    have hnext : ∃ q. PowTwo(S e,q)Definitions: PowTwoOriginal native command in the exact edition
  2. L16
    specialize binary_power_two_exists (S e)
  3. L17
    exact binary_power_two_exists
05Separate the logical casesL18–18

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

  1. L18
    cases hnext
06Establish hstrictL19–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary power two strict growth.

  1. L19
    have hstrict : exists gap. gap + S p = x
  2. L20
    specialize binary_power_two_strict_growth e
  3. L21
    specialize binary_power_two_strict_growth p
  4. L22
    specialize binary_power_two_strict_growth x
  5. L23
    apply binary_power_two_strict_growth
  6. L24
    exact hp
  7. L25
    exact hnext_witness
07Separate the logical casesL26–26

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

  1. L26
    right
08Construct an explicit witnessL27–29

Supply the displayed value, then prove that it has the required property.

  1. L27
    exists e
  2. L28
    exists p
  3. L29
    exists x
09Separate the logical casesL30–30

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

  1. L30
    split
10Calculate and transport equalitiesL31–31

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

  1. L31
    refl
11Separate the logical casesL32–32

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

  1. L32
    split
12Use earlier factsL33–33

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

  1. L33
    exact hpositive
13Separate the logical casesL34–34

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

  1. L34
    split
14Use earlier factsL35–35

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

  1. L35
    exact hp
15Separate the logical casesL36–36

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

  1. L36
    split
16Use earlier factsL37–37

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

  1. L37
    exact hnext_witness
17Separate the logical casesL38–38

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

  1. L38
    split
18Use earlier factsL39–40

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

  1. L39
    apply le_refl
  2. L40
    exact hstrict

Library-wide reading audit

Original defined command ledger · 40 lines
  1. 0001intro e
  2. 0002intro p
  3. 0003intro hp
  4. 0004have hnonzero : ~(p = 0)
  5. 0005intro hzero
  6. 0006specialize binary_power_two_nonzero e
  7. 0007specialize binary_power_two_nonzero p
  8. 0008apply binary_power_two_nonzero
  9. 0009exact hp
  10. 0010exact hzero
  11. 0011have hpositive : exists gap. gap + 1 = p
  12. 0012specialize one_le_of_ne_zero p
  13. 0013apply one_le_of_ne_zero
  14. 0014exact hnonzero
  15. 0015have hnext : exists q. (exists pa_b_bl_exact_next pa_c_bl_exact_next. ((forall pa_i_bl_exact_next_repeat. (exists pa_lt_bl_exact_next_repeat_bound. pa_lt_bl_exact_next_repeat_bound + S pa_i_bl_exact_next_repeat = S e) -> (((exists pa_h_bl_exact_next_repeat_decoded. pa_h_bl_exact_next_repeat_decoded + S (2) = S ((S (pa_i_bl_exact_next_repeat)) * pa_c_bl_exact_next)) /\ exists pa_q_bl_exact_next_repeat_decoded. pa_b_bl_exact_next = pa_q_bl_exact_next_repeat_decoded * S ((S (pa_i_bl_exact_next_repeat)) * pa_c_bl_exact_next) + (2)))) /\ (exists pa_u_bl_exact_next_product pa_v_bl_exact_next_product. ((((exists pa_h_bl_exact_next_product_start. pa_h_bl_exact_next_product_start + S (1) = S ((S (0)) * pa_v_bl_exact_next_product)) /\ exists pa_q_bl_exact_next_product_start. pa_u_bl_exact_next_product = pa_q_bl_exact_next_product_start * S ((S (0)) * pa_v_bl_exact_next_product) + (1))) /\ ((((exists pa_h_bl_exact_next_product_terminal. pa_h_bl_exact_next_product_terminal + S (q) = S ((S (S e)) * pa_v_bl_exact_next_product)) /\ exists pa_q_bl_exact_next_product_terminal. pa_u_bl_exact_next_product = pa_q_bl_exact_next_product_terminal * S ((S (S e)) * pa_v_bl_exact_next_product) + (q))) /\ forall pa_i_bl_exact_next_product. (exists pa_lt_bl_exact_next_product_bound. pa_lt_bl_exact_next_product_bound + S pa_i_bl_exact_next_product = S e) -> exists pa_p_bl_exact_next_product pa_r_bl_exact_next_product pa_s_bl_exact_next_product. ((((exists pa_h_bl_exact_next_product_factor. pa_h_bl_exact_next_product_factor + S (pa_p_bl_exact_next_product) = S ((S (pa_i_bl_exact_next_product)) * pa_c_bl_exact_next)) /\ exists pa_q_bl_exact_next_product_factor. pa_b_bl_exact_next = pa_q_bl_exact_next_product_factor * S ((S (pa_i_bl_exact_next_product)) * pa_c_bl_exact_next) + (pa_p_bl_exact_next_product))) /\ ((((exists pa_h_bl_exact_next_product_partial. pa_h_bl_exact_next_product_partial + S (pa_r_bl_exact_next_product) = S ((S (pa_i_bl_exact_next_product)) * pa_v_bl_exact_next_product)) /\ exists pa_q_bl_exact_next_product_partial. pa_u_bl_exact_next_product = pa_q_bl_exact_next_product_partial * S ((S (pa_i_bl_exact_next_product)) * pa_v_bl_exact_next_product) + (pa_r_bl_exact_next_product))) /\ ((((exists pa_h_bl_exact_next_product_successor. pa_h_bl_exact_next_product_successor + S (pa_s_bl_exact_next_product) = S ((S (S pa_i_bl_exact_next_product)) * pa_v_bl_exact_next_product)) /\ exists pa_q_bl_exact_next_product_successor. pa_u_bl_exact_next_product = pa_q_bl_exact_next_product_successor * S ((S (S pa_i_bl_exact_next_product)) * pa_v_bl_exact_next_product) + (pa_s_bl_exact_next_product))) /\ pa_s_bl_exact_next_product = pa_r_bl_exact_next_product * pa_p_bl_exact_next_product))))))))
  16. 0016specialize binary_power_two_exists (S e)
  17. 0017exact binary_power_two_exists
  18. 0018cases hnext
  19. 0019have hstrict : exists gap. gap + S p = x
  20. 0020specialize binary_power_two_strict_growth e
  21. 0021specialize binary_power_two_strict_growth p
  22. 0022specialize binary_power_two_strict_growth x
  23. 0023apply binary_power_two_strict_growth
  24. 0024exact hp
  25. 0025exact hnext_witness
  26. 0026right
  27. 0027exists e
  28. 0028exists p
  29. 0029exists x
  30. 0030split
  31. 0031refl
  32. 0032split
  33. 0033exact hpositive
  34. 0034split
  35. 0035exact hp
  36. 0036split
  37. 0037exact hnext_witness
  38. 0038split
  39. 0039apply le_refl
  40. 0040exact hstrict