BL000C

binary_power_two_exponent_strict

Strictly ordered exponents have strictly ordered powers of two.

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

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

Definition DAG

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

Actual proof prerequisites

binary_power_two_existsbinary_power_two_strict_growthbinary_power_two_exponent_monotonelt_of_lt_of_le · checked external prerequisite
Original expanded first-order statement 
forall e f p q. (exists gap. gap + S e = f) -> (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_later_power pa_c_bl_later_power. ((forall pa_i_bl_later_power_repeat. (exists pa_lt_bl_later_power_repeat_bound. pa_lt_bl_later_power_repeat_bound + S pa_i_bl_later_power_repeat = f) -> (((exists pa_h_bl_later_power_repeat_decoded. pa_h_bl_later_power_repeat_decoded + S (2) = S ((S (pa_i_bl_later_power_repeat)) * pa_c_bl_later_power)) /\ exists pa_q_bl_later_power_repeat_decoded. pa_b_bl_later_power = pa_q_bl_later_power_repeat_decoded * S ((S (pa_i_bl_later_power_repeat)) * pa_c_bl_later_power) + (2)))) /\ (exists pa_u_bl_later_power_product pa_v_bl_later_power_product. ((((exists pa_h_bl_later_power_product_start. pa_h_bl_later_power_product_start + S (1) = S ((S (0)) * pa_v_bl_later_power_product)) /\ exists pa_q_bl_later_power_product_start. pa_u_bl_later_power_product = pa_q_bl_later_power_product_start * S ((S (0)) * pa_v_bl_later_power_product) + (1))) /\ ((((exists pa_h_bl_later_power_product_terminal. pa_h_bl_later_power_product_terminal + S (q) = S ((S (f)) * pa_v_bl_later_power_product)) /\ exists pa_q_bl_later_power_product_terminal. pa_u_bl_later_power_product = pa_q_bl_later_power_product_terminal * S ((S (f)) * pa_v_bl_later_power_product) + (q))) /\ forall pa_i_bl_later_power_product. (exists pa_lt_bl_later_power_product_bound. pa_lt_bl_later_power_product_bound + S pa_i_bl_later_power_product = f) -> exists pa_p_bl_later_power_product pa_r_bl_later_power_product pa_s_bl_later_power_product. ((((exists pa_h_bl_later_power_product_factor. pa_h_bl_later_power_product_factor + S (pa_p_bl_later_power_product) = S ((S (pa_i_bl_later_power_product)) * pa_c_bl_later_power)) /\ exists pa_q_bl_later_power_product_factor. pa_b_bl_later_power = pa_q_bl_later_power_product_factor * S ((S (pa_i_bl_later_power_product)) * pa_c_bl_later_power) + (pa_p_bl_later_power_product))) /\ ((((exists pa_h_bl_later_power_product_partial. pa_h_bl_later_power_product_partial + S (pa_r_bl_later_power_product) = S ((S (pa_i_bl_later_power_product)) * pa_v_bl_later_power_product)) /\ exists pa_q_bl_later_power_product_partial. pa_u_bl_later_power_product = pa_q_bl_later_power_product_partial * S ((S (pa_i_bl_later_power_product)) * pa_v_bl_later_power_product) + (pa_r_bl_later_power_product))) /\ ((((exists pa_h_bl_later_power_product_successor. pa_h_bl_later_power_product_successor + S (pa_s_bl_later_power_product) = S ((S (S pa_i_bl_later_power_product)) * pa_v_bl_later_power_product)) /\ exists pa_q_bl_later_power_product_successor. pa_u_bl_later_power_product = pa_q_bl_later_power_product_successor * S ((S (S pa_i_bl_later_power_product)) * pa_v_bl_later_power_product) + (pa_s_bl_later_power_product))) /\ pa_s_bl_later_power_product = pa_r_bl_later_power_product * pa_p_bl_later_power_product)))))))) -> exists gap. gap + S p = q

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

33 script commands · 6 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 (3)
binary power two existsbinary power two strict growthbinary power two exponent monotone

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

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

  1. L1
    intro e
  2. L2
    intro f
  3. L3
    intro p
  4. L4
    intro q
  5. L5
    intro horder
  6. L6
    intro hp
  7. L7
    intro hq
02Establish hnextL8–10

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

  1. L8
    have hnext : ∃ z. PowTwo(S e,z)Definitions: PowTwoOriginal native command in the exact edition
  2. L9
    specialize binary_power_two_exists (S e)
  3. L10
    exact binary_power_two_exists
03Separate the logical casesL11–11

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

  1. L11
    cases hnext
04Establish hfirstL12–18

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

  1. L12
    have hfirst : exists gap. gap + S p = x
  2. L13
    specialize binary_power_two_strict_growth e
  3. L14
    specialize binary_power_two_strict_growth p
  4. L15
    specialize binary_power_two_strict_growth x
  5. L16
    apply binary_power_two_strict_growth
  6. L17
    exact hp
  7. L18
    exact hnext_witness
05Establish hsecondL19–28

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

  1. L19
    have hsecond : exists gap. gap + x = q
  2. L20
    specialize binary_power_two_exponent_monotone (S e)
  3. L21
    specialize binary_power_two_exponent_monotone f
  4. L22
    specialize binary_power_two_exponent_monotone x
  5. L23
    specialize binary_power_two_exponent_monotone q
  6. L24
    apply binary_power_two_exponent_monotone
  7. L25
    exact horder
  8. L26
    exact hnext_witness
  9. L27
    exact hq
  10. L28
    specialize lt_of_lt_of_le p
06Use earlier factsL29–33

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

  1. L29
    specialize lt_of_lt_of_le x
  2. L30
    specialize lt_of_lt_of_le q
  3. L31
    apply lt_of_lt_of_le
  4. L32
    exact hfirst
  5. L33
    exact hsecond

Library-wide reading audit

Original defined command ledger · 33 lines
  1. 0001intro e
  2. 0002intro f
  3. 0003intro p
  4. 0004intro q
  5. 0005intro horder
  6. 0006intro hp
  7. 0007intro hq
  8. 0008have hnext : exists z. (exists pa_b_bl_strict_next pa_c_bl_strict_next. ((forall pa_i_bl_strict_next_repeat. (exists pa_lt_bl_strict_next_repeat_bound. pa_lt_bl_strict_next_repeat_bound + S pa_i_bl_strict_next_repeat = S e) -> (((exists pa_h_bl_strict_next_repeat_decoded. pa_h_bl_strict_next_repeat_decoded + S (2) = S ((S (pa_i_bl_strict_next_repeat)) * pa_c_bl_strict_next)) /\ exists pa_q_bl_strict_next_repeat_decoded. pa_b_bl_strict_next = pa_q_bl_strict_next_repeat_decoded * S ((S (pa_i_bl_strict_next_repeat)) * pa_c_bl_strict_next) + (2)))) /\ (exists pa_u_bl_strict_next_product pa_v_bl_strict_next_product. ((((exists pa_h_bl_strict_next_product_start. pa_h_bl_strict_next_product_start + S (1) = S ((S (0)) * pa_v_bl_strict_next_product)) /\ exists pa_q_bl_strict_next_product_start. pa_u_bl_strict_next_product = pa_q_bl_strict_next_product_start * S ((S (0)) * pa_v_bl_strict_next_product) + (1))) /\ ((((exists pa_h_bl_strict_next_product_terminal. pa_h_bl_strict_next_product_terminal + S (z) = S ((S (S e)) * pa_v_bl_strict_next_product)) /\ exists pa_q_bl_strict_next_product_terminal. pa_u_bl_strict_next_product = pa_q_bl_strict_next_product_terminal * S ((S (S e)) * pa_v_bl_strict_next_product) + (z))) /\ forall pa_i_bl_strict_next_product. (exists pa_lt_bl_strict_next_product_bound. pa_lt_bl_strict_next_product_bound + S pa_i_bl_strict_next_product = S e) -> exists pa_p_bl_strict_next_product pa_r_bl_strict_next_product pa_s_bl_strict_next_product. ((((exists pa_h_bl_strict_next_product_factor. pa_h_bl_strict_next_product_factor + S (pa_p_bl_strict_next_product) = S ((S (pa_i_bl_strict_next_product)) * pa_c_bl_strict_next)) /\ exists pa_q_bl_strict_next_product_factor. pa_b_bl_strict_next = pa_q_bl_strict_next_product_factor * S ((S (pa_i_bl_strict_next_product)) * pa_c_bl_strict_next) + (pa_p_bl_strict_next_product))) /\ ((((exists pa_h_bl_strict_next_product_partial. pa_h_bl_strict_next_product_partial + S (pa_r_bl_strict_next_product) = S ((S (pa_i_bl_strict_next_product)) * pa_v_bl_strict_next_product)) /\ exists pa_q_bl_strict_next_product_partial. pa_u_bl_strict_next_product = pa_q_bl_strict_next_product_partial * S ((S (pa_i_bl_strict_next_product)) * pa_v_bl_strict_next_product) + (pa_r_bl_strict_next_product))) /\ ((((exists pa_h_bl_strict_next_product_successor. pa_h_bl_strict_next_product_successor + S (pa_s_bl_strict_next_product) = S ((S (S pa_i_bl_strict_next_product)) * pa_v_bl_strict_next_product)) /\ exists pa_q_bl_strict_next_product_successor. pa_u_bl_strict_next_product = pa_q_bl_strict_next_product_successor * S ((S (S pa_i_bl_strict_next_product)) * pa_v_bl_strict_next_product) + (pa_s_bl_strict_next_product))) /\ pa_s_bl_strict_next_product = pa_r_bl_strict_next_product * pa_p_bl_strict_next_product))))))))
  9. 0009specialize binary_power_two_exists (S e)
  10. 0010exact binary_power_two_exists
  11. 0011cases hnext
  12. 0012have hfirst : exists gap. gap + S p = x
  13. 0013specialize binary_power_two_strict_growth e
  14. 0014specialize binary_power_two_strict_growth p
  15. 0015specialize binary_power_two_strict_growth x
  16. 0016apply binary_power_two_strict_growth
  17. 0017exact hp
  18. 0018exact hnext_witness
  19. 0019have hsecond : exists gap. gap + x = q
  20. 0020specialize binary_power_two_exponent_monotone (S e)
  21. 0021specialize binary_power_two_exponent_monotone f
  22. 0022specialize binary_power_two_exponent_monotone x
  23. 0023specialize binary_power_two_exponent_monotone q
  24. 0024apply binary_power_two_exponent_monotone
  25. 0025exact horder
  26. 0026exact hnext_witness
  27. 0027exact hq
  28. 0028specialize lt_of_lt_of_le p
  29. 0029specialize lt_of_lt_of_le x
  30. 0030specialize lt_of_lt_of_le q
  31. 0031apply lt_of_lt_of_le
  32. 0032exact hfirst
  33. 0033exact hsecond