BL000A

binary_power_two_strict_growth

Successive beta-coded powers of two grow strictly.

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. ∀ q. PowTwo(e,p) → PowTwo(S e,q) → Lt(p,q)

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

Definition DAG

PowTwo(e,p) · 2Lt(a,b) · 1

Actual proof prerequisites

binary_power_two_nonzerobinary_power_two_successor_doublefour_square_branch_positive_half_strict · checked external prerequisitetwo_mul_eq_add_self · checked external prerequisite
Original expanded first-order 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

Complete unchanged native tactic proof

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

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.

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