BL000A

binary_power_two_strict_growth

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

Successive beta-coded powers of two grow strictly.

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 q. (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)))))))) -> (exists pa_b_bl_next_power pa_c_bl_next_power. ((forall pa_i_bl_next_power_repeat. (exists pa_lt_bl_next_power_repeat_bound. pa_lt_bl_next_power_repeat_bound + S pa_i_bl_next_power_repeat = S e) -> (((exists pa_h_bl_next_power_repeat_decoded. pa_h_bl_next_power_repeat_decoded + S (2) = S ((S (pa_i_bl_next_power_repeat)) * pa_c_bl_next_power)) /\ exists pa_q_bl_next_power_repeat_decoded. pa_b_bl_next_power = pa_q_bl_next_power_repeat_decoded * S ((S (pa_i_bl_next_power_repeat)) * pa_c_bl_next_power) + (2)))) /\ (exists pa_u_bl_next_power_product pa_v_bl_next_power_product. ((((exists pa_h_bl_next_power_product_start. pa_h_bl_next_power_product_start + S (1) = S ((S (0)) * pa_v_bl_next_power_product)) /\ exists pa_q_bl_next_power_product_start. pa_u_bl_next_power_product = pa_q_bl_next_power_product_start * S ((S (0)) * pa_v_bl_next_power_product) + (1))) /\ ((((exists pa_h_bl_next_power_product_terminal. pa_h_bl_next_power_product_terminal + S (q) = S ((S (S e)) * pa_v_bl_next_power_product)) /\ exists pa_q_bl_next_power_product_terminal. pa_u_bl_next_power_product = pa_q_bl_next_power_product_terminal * S ((S (S e)) * pa_v_bl_next_power_product) + (q))) /\ forall pa_i_bl_next_power_product. (exists pa_lt_bl_next_power_product_bound. pa_lt_bl_next_power_product_bound + S pa_i_bl_next_power_product = S e) -> exists pa_p_bl_next_power_product pa_r_bl_next_power_product pa_s_bl_next_power_product. ((((exists pa_h_bl_next_power_product_factor. pa_h_bl_next_power_product_factor + S (pa_p_bl_next_power_product) = S ((S (pa_i_bl_next_power_product)) * pa_c_bl_next_power)) /\ exists pa_q_bl_next_power_product_factor. pa_b_bl_next_power = pa_q_bl_next_power_product_factor * S ((S (pa_i_bl_next_power_product)) * pa_c_bl_next_power) + (pa_p_bl_next_power_product))) /\ ((((exists pa_h_bl_next_power_product_partial. pa_h_bl_next_power_product_partial + S (pa_r_bl_next_power_product) = S ((S (pa_i_bl_next_power_product)) * pa_v_bl_next_power_product)) /\ exists pa_q_bl_next_power_product_partial. pa_u_bl_next_power_product = pa_q_bl_next_power_product_partial * S ((S (pa_i_bl_next_power_product)) * pa_v_bl_next_power_product) + (pa_r_bl_next_power_product))) /\ ((((exists pa_h_bl_next_power_product_successor. pa_h_bl_next_power_product_successor + S (pa_s_bl_next_power_product) = S ((S (S pa_i_bl_next_power_product)) * pa_v_bl_next_power_product)) /\ exists pa_q_bl_next_power_product_successor. pa_u_bl_next_power_product = pa_q_bl_next_power_product_successor * S ((S (S pa_i_bl_next_power_product)) * pa_v_bl_next_power_product) + (pa_s_bl_next_power_product))) /\ pa_s_bl_next_power_product = pa_r_bl_next_power_product * pa_p_bl_next_power_product)))))))) -> exists gap. gap + S p = q

Constructive proof overview

Generated structural guide

Successive beta-coded powers of two grow strictly.

The unchanged tactic script uses 4 declared prerequisites and contains 31 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 BL0009 binary_power_two_successor_double four_square_branch_positive_half_strict Alpha theorem; checked-use authorized two_mul_eq_add_self Alpha theorem; checked-use authorized

Direct dependents

BL000C binary_power_two_exponent_strict BL0010 binary_length_successor_step BL0015 binary_length_power_exact

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

31 script commands · 12 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 (2)
binary power two nonzerobinary power two successor double
01Fix variables and assumptionsL1–5

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

  1. L1
    intro e
  2. L2
    intro p
  3. L3
    intro q
  4. L4
    intro hp
  5. L5
    intro hq
02Establish hnonzeroL6–12

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

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

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

  1. L13
    have hdouble : q = p + p
  2. L14
    specialize binary_power_two_successor_double e
  3. L15
    specialize binary_power_two_successor_double p
  4. L16
    specialize binary_power_two_successor_double q
  5. L17
    apply binary_power_two_successor_double
  6. L18
    exact hp
  7. L19
    exact hq
04Establish hstrictL20–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square branch positive half strict.

  1. L20
    have hstrict : exists gap. gap + S p = 2 * p
  2. L21
    specialize four_square_branch_positive_half_strict p
  3. L22
    apply four_square_branch_positive_half_strict
  4. L23
    exact hnonzero
05Separate the logical casesL24–24

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

  1. L24
    cases hstrict
06Construct an explicit witnessL25–25

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

  1. L25
    exists x
07Calculate and transport equalitiesL26–26

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

  1. L26
    trans 2 * p
08Use earlier factsL27–27

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

  1. L27
    exact hstrict_witness
09Calculate and transport equalitiesL28–28

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

  1. L28
    trans p + p
10Use earlier factsL29–29

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

  1. L29
    apply two_mul_eq_add_self
11Calculate and transport equalitiesL30–30

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

  1. L30
    symm
12Use earlier factsL31–31

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

  1. L31
    exact hdouble

Library-wide reading audit

Original exact command ledger · 31 lines
  1. 0001intro e
  2. 0002intro p
  3. 0003intro q
  4. 0004intro hp
  5. 0005intro hq
  6. 0006have hnonzero : ~(p = 0)
  7. 0007intro hzero
  8. 0008specialize binary_power_two_nonzero e
  9. 0009specialize binary_power_two_nonzero p
  10. 0010apply binary_power_two_nonzero
  11. 0011exact hp
  12. 0012exact hzero
  13. 0013have hdouble : q = p + p
  14. 0014specialize binary_power_two_successor_double e
  15. 0015specialize binary_power_two_successor_double p
  16. 0016specialize binary_power_two_successor_double q
  17. 0017apply binary_power_two_successor_double
  18. 0018exact hp
  19. 0019exact hq
  20. 0020have hstrict : exists gap. gap + S p = 2 * p
  21. 0021specialize four_square_branch_positive_half_strict p
  22. 0022apply four_square_branch_positive_half_strict
  23. 0023exact hnonzero
  24. 0024cases hstrict
  25. 0025exists x
  26. 0026trans 2 * p
  27. 0027exact hstrict_witness
  28. 0028trans p + p
  29. 0029apply two_mul_eq_add_self
  30. 0030symm
  31. 0031exact hdouble