PC0015

binary_power_two_dominates_successor

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 7 declared prerequisites and contains 41 exact native proof lines.

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

Proof neighborhood

Direct dependencies

pow_zero Stable theorem; checked-use authorized le_refl Stable theorem; checked-use authorized pow_successor_decompose Stable theorem; checked-use authorized mul_le_mul_right Stable theorem; checked-use authorized le_trans Stable theorem; checked-use authorized add_comm Stable theorem; checked-use authorized zero_add Stable theorem; checked-use authorized

Direct dependents

PC0019 central_binom_dominates_pow_two PC0026 binary_half_scale_bounds

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

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.

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.

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
  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
    have hpre : exists g. g + S n = x
  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 exact 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 : exists a. (exists pa_b_pc_power_dom_previous pa_c_pc_power_dom_previous. ((forall pa_i_pc_power_dom_previous_repeat. (exists pa_lt_pc_power_dom_previous_repeat_bound. pa_lt_pc_power_dom_previous_repeat_bound + S pa_i_pc_power_dom_previous_repeat = n) -> (((exists pa_h_pc_power_dom_previous_repeat_decoded. pa_h_pc_power_dom_previous_repeat_decoded + S (2) = S ((S (pa_i_pc_power_dom_previous_repeat)) * pa_c_pc_power_dom_previous)) /\ exists pa_q_pc_power_dom_previous_repeat_decoded. pa_b_pc_power_dom_previous = pa_q_pc_power_dom_previous_repeat_decoded * S ((S (pa_i_pc_power_dom_previous_repeat)) * pa_c_pc_power_dom_previous) + (2)))) /\ (exists pa_u_pc_power_dom_previous_product pa_v_pc_power_dom_previous_product. ((((exists pa_h_pc_power_dom_previous_product_start. pa_h_pc_power_dom_previous_product_start + S (1) = S ((S (0)) * pa_v_pc_power_dom_previous_product)) /\ exists pa_q_pc_power_dom_previous_product_start. pa_u_pc_power_dom_previous_product = pa_q_pc_power_dom_previous_product_start * S ((S (0)) * pa_v_pc_power_dom_previous_product) + (1))) /\ ((((exists pa_h_pc_power_dom_previous_product_terminal. pa_h_pc_power_dom_previous_product_terminal + S (a) = S ((S (n)) * pa_v_pc_power_dom_previous_product)) /\ exists pa_q_pc_power_dom_previous_product_terminal. pa_u_pc_power_dom_previous_product = pa_q_pc_power_dom_previous_product_terminal * S ((S (n)) * pa_v_pc_power_dom_previous_product) + (a))) /\ forall pa_i_pc_power_dom_previous_product. (exists pa_lt_pc_power_dom_previous_product_bound. pa_lt_pc_power_dom_previous_product_bound + S pa_i_pc_power_dom_previous_product = n) -> exists pa_p_pc_power_dom_previous_product pa_r_pc_power_dom_previous_product pa_s_pc_power_dom_previous_product. ((((exists pa_h_pc_power_dom_previous_product_factor. pa_h_pc_power_dom_previous_product_factor + S (pa_p_pc_power_dom_previous_product) = S ((S (pa_i_pc_power_dom_previous_product)) * pa_c_pc_power_dom_previous)) /\ exists pa_q_pc_power_dom_previous_product_factor. pa_b_pc_power_dom_previous = pa_q_pc_power_dom_previous_product_factor * S ((S (pa_i_pc_power_dom_previous_product)) * pa_c_pc_power_dom_previous) + (pa_p_pc_power_dom_previous_product))) /\ ((((exists pa_h_pc_power_dom_previous_product_partial. pa_h_pc_power_dom_previous_product_partial + S (pa_r_pc_power_dom_previous_product) = S ((S (pa_i_pc_power_dom_previous_product)) * pa_v_pc_power_dom_previous_product)) /\ exists pa_q_pc_power_dom_previous_product_partial. pa_u_pc_power_dom_previous_product = pa_q_pc_power_dom_previous_product_partial * S ((S (pa_i_pc_power_dom_previous_product)) * pa_v_pc_power_dom_previous_product) + (pa_r_pc_power_dom_previous_product))) /\ ((((exists pa_h_pc_power_dom_previous_product_successor. pa_h_pc_power_dom_previous_product_successor + S (pa_s_pc_power_dom_previous_product) = S ((S (S pa_i_pc_power_dom_previous_product)) * pa_v_pc_power_dom_previous_product)) /\ exists pa_q_pc_power_dom_previous_product_successor. pa_u_pc_power_dom_previous_product = pa_q_pc_power_dom_previous_product_successor * S ((S (S pa_i_pc_power_dom_previous_product)) * pa_v_pc_power_dom_previous_product) + (pa_s_pc_power_dom_previous_product))) /\ pa_s_pc_power_dom_previous_product = pa_r_pc_power_dom_previous_product * pa_p_pc_power_dom_previous_product)))))))) /\ 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 : exists g. g + S 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