PC0015

binary_power_two_dominates_successor

Actual powers of two dominate the successor of their exponent, by HA induction.

Alpha v34 checked-use · first admitted v27 · 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.

These are the exact finite integer inequalities with constant 8, for every N≥2. The proof uses constructive binomial and primorial infrastructure; it does not assume logarithms, asymptotic estimates, the prime number theorem, or a factorization oracle.

Exact theorem in conservative defined notation

∀ n. ∀ v. PowTwo(n,v) → Lt(n,v)

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

Definition DAG

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

Actual proof prerequisites

pow_zero · checked external prerequisitele_refl · checked external prerequisitepow_successor_decompose · checked external prerequisitemul_le_mul_right · checked external prerequisitele_trans · checked external prerequisiteadd_comm · checked external prerequisitezero_add · checked external prerequisite
Original expanded first-order statement 
forall n v. (exists pa_b_pc_power_dom_source pa_c_pc_power_dom_source. ((forall pa_i_pc_power_dom_source_repeat. (exists pa_lt_pc_power_dom_source_repeat_bound. pa_lt_pc_power_dom_source_repeat_bound + S pa_i_pc_power_dom_source_repeat = n) -> (((exists pa_h_pc_power_dom_source_repeat_decoded. pa_h_pc_power_dom_source_repeat_decoded + S (2) = S ((S (pa_i_pc_power_dom_source_repeat)) * pa_c_pc_power_dom_source)) /\ exists pa_q_pc_power_dom_source_repeat_decoded. pa_b_pc_power_dom_source = pa_q_pc_power_dom_source_repeat_decoded * S ((S (pa_i_pc_power_dom_source_repeat)) * pa_c_pc_power_dom_source) + (2)))) /\ (exists pa_u_pc_power_dom_source_product pa_v_pc_power_dom_source_product. ((((exists pa_h_pc_power_dom_source_product_start. pa_h_pc_power_dom_source_product_start + S (1) = S ((S (0)) * pa_v_pc_power_dom_source_product)) /\ exists pa_q_pc_power_dom_source_product_start. pa_u_pc_power_dom_source_product = pa_q_pc_power_dom_source_product_start * S ((S (0)) * pa_v_pc_power_dom_source_product) + (1))) /\ ((((exists pa_h_pc_power_dom_source_product_terminal. pa_h_pc_power_dom_source_product_terminal + S (v) = S ((S (n)) * pa_v_pc_power_dom_source_product)) /\ exists pa_q_pc_power_dom_source_product_terminal. pa_u_pc_power_dom_source_product = pa_q_pc_power_dom_source_product_terminal * S ((S (n)) * pa_v_pc_power_dom_source_product) + (v))) /\ forall pa_i_pc_power_dom_source_product. (exists pa_lt_pc_power_dom_source_product_bound. pa_lt_pc_power_dom_source_product_bound + S pa_i_pc_power_dom_source_product = n) -> exists pa_p_pc_power_dom_source_product pa_r_pc_power_dom_source_product pa_s_pc_power_dom_source_product. ((((exists pa_h_pc_power_dom_source_product_factor. pa_h_pc_power_dom_source_product_factor + S (pa_p_pc_power_dom_source_product) = S ((S (pa_i_pc_power_dom_source_product)) * pa_c_pc_power_dom_source)) /\ exists pa_q_pc_power_dom_source_product_factor. pa_b_pc_power_dom_source = pa_q_pc_power_dom_source_product_factor * S ((S (pa_i_pc_power_dom_source_product)) * pa_c_pc_power_dom_source) + (pa_p_pc_power_dom_source_product))) /\ ((((exists pa_h_pc_power_dom_source_product_partial. pa_h_pc_power_dom_source_product_partial + S (pa_r_pc_power_dom_source_product) = S ((S (pa_i_pc_power_dom_source_product)) * pa_v_pc_power_dom_source_product)) /\ exists pa_q_pc_power_dom_source_product_partial. pa_u_pc_power_dom_source_product = pa_q_pc_power_dom_source_product_partial * S ((S (pa_i_pc_power_dom_source_product)) * pa_v_pc_power_dom_source_product) + (pa_r_pc_power_dom_source_product))) /\ ((((exists pa_h_pc_power_dom_source_product_successor. pa_h_pc_power_dom_source_product_successor + S (pa_s_pc_power_dom_source_product) = S ((S (S pa_i_pc_power_dom_source_product)) * pa_v_pc_power_dom_source_product)) /\ exists pa_q_pc_power_dom_source_product_successor. pa_u_pc_power_dom_source_product = pa_q_pc_power_dom_source_product_successor * S ((S (S pa_i_pc_power_dom_source_product)) * pa_v_pc_power_dom_source_product) + (pa_s_pc_power_dom_source_product))) /\ pa_s_pc_power_dom_source_product = pa_r_pc_power_dom_source_product * pa_p_pc_power_dom_source_product)))))))) -> (exists pc_le_power_dom_result. pc_le_power_dom_result + (S n) = (v))

Complete tactic proof in conservative notation

All 41 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

41 script commands · 9 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.

01Induction on nL1–3

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L1
    induction n
  2. L2
    intro v
  3. L3
    intro h
02Establish heqL4–13

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

  1. L4
    have heq : v = 1
  2. L5
    specialize pow_zero 2
  3. L6
    specialize pow_zero 0
  4. L7
    specialize pow_zero v
  5. L8
    apply pow_zero
  6. L9
    refl
  7. L10
    exact h
  8. L11
    rewrite heq
  9. L12
    specialize le_refl 1
  10. L13
    apply le_refl
03Fix variables and assumptionsL14–15

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

  1. L14
    intro v
  2. L15
    intro h
04Establish hpL16–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow successor decompose.

  1. L16
    have hp : ∃ a. PowTwo(n,a) ∧ v = a · 2Definitions: PowTwo(n,a)Original native command in the exact edition
  2. L17
    specialize pow_successor_decompose 2
  3. L18
    specialize pow_successor_decompose n
  4. L19
    specialize pow_successor_decompose (S n)
  5. L20
    specialize pow_successor_decompose v
  6. L21
    apply pow_successor_decompose
  7. L22
    refl
  8. L23
    exact h
05Separate the logical casesL24–25

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

  1. L24
    cases hp
  2. L25
    cases hp_witness
06Establish hpreL26–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.

  1. L26
  2. L27
    specialize IH x
  3. L28
    apply IH
  4. L29
    exact hp_witness_left
  5. L30
    rewrite hp_witness_right
  6. L31
    specialize le_trans (S (S n))
  7. L32
    specialize le_trans ((S n) * 2)
  8. L33
    specialize le_trans (x * 2)
  9. L34
    apply le_trans
07Construct an explicit witnessL35–35

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

  1. L35
    exists n
08Calculate and transport equalitiesL36–36

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

  1. L36
    simp [add_comm, zero_add]
09Use earlier factsL37–41

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

  1. L37
    specialize mul_le_mul_right (S n)
  2. L38
    specialize mul_le_mul_right x
  3. L39
    specialize mul_le_mul_right 2
  4. L40
    apply mul_le_mul_right
  5. L41
    exact hpre

Library-wide reading audit

Original defined command ledger · 41 lines
  1. 0001induction n
  2. 0002intro v
  3. 0003intro h
  4. 0004have heq : v = 1
  5. 0005specialize pow_zero 2
  6. 0006specialize pow_zero 0
  7. 0007specialize pow_zero v
  8. 0008apply pow_zero
  9. 0009refl
  10. 0010exact h
  11. 0011rewrite heq
  12. 0012specialize le_refl 1
  13. 0013apply le_refl
  14. 0014intro v
  15. 0015intro h
  16. 0016have hp : ∃ a. PowTwo(n,a) ∧ v = a · 2
  17. 0017specialize pow_successor_decompose 2
  18. 0018specialize pow_successor_decompose n
  19. 0019specialize pow_successor_decompose (S n)
  20. 0020specialize pow_successor_decompose v
  21. 0021apply pow_successor_decompose
  22. 0022refl
  23. 0023exact h
  24. 0024cases hp
  25. 0025cases hp_witness
  26. 0026have hpre : Lt(n,x)
  27. 0027specialize IH x
  28. 0028apply IH
  29. 0029exact hp_witness_left
  30. 0030rewrite hp_witness_right
  31. 0031specialize le_trans (S (S n))
  32. 0032specialize le_trans ((S n) * 2)
  33. 0033specialize le_trans (x * 2)
  34. 0034apply le_trans
  35. 0035exists n
  36. 0036simp [add_comm, zero_add]
  37. 0037specialize mul_le_mul_right (S n)
  38. 0038specialize mul_le_mul_right x
  39. 0039specialize mul_le_mul_right 2
  40. 0040apply mul_le_mul_right
  41. 0041exact hpre