BL0015

binary_length_power_exact

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 5 declared prerequisites and contains 40 exact native proof lines.

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

Proof neighborhood

Direct dependencies

BL0008 binary_power_two_nonzero BL0005 binary_power_two_exists BL000A binary_power_two_strict_growth one_le_of_ne_zero Stable theorem; checked-use authorized le_refl Stable theorem; checked-use authorized

Direct dependents

none

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

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.

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