PC0019

central_binom_dominates_pow_two

For n at least four, the central binomial coefficient dominates the actual 2^n value.

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. ∀ C. ∀ v. Lt(3,n) → CentralBinom(n,C) → PowTwo(n,v) → Le(v,C)

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

Definition DAG

PowTwo(e,p) · 1Le(a,b) · 4Lt(a,b) · 2Pow(a,e,z) · 1CentralBinom(n,z) · 1

Actual proof prerequisites

pow_exists · checked external prerequisitepow_four_is_square_of_pow_twofour_pow_lt_mul_central_binom · checked external prerequisitebinary_power_two_dominates_successorlt_to_le · checked external prerequisitemul_le_mul_right · checked external prerequisitele_trans · checked external prerequisitemul_le_cancel_left_nonzero · checked external prerequisitepow_nonzero_of_one_le · checked external prerequisite
Original expanded first-order statement 
forall n C v. (exists pc_le_central_lower_bound. pc_le_central_lower_bound + (4) = (n)) -> (((exists bcf_lt_gap_pc_central_lower_value_out_of_range. bcf_lt_gap_pc_central_lower_value_out_of_range + S (n + n) = n) /\ C = 0) \/ ((exists bcf_le_gap_pc_central_lower_value_in_range. bcf_le_gap_pc_central_lower_value_in_range + (n) = n + n) /\ (exists bcf_row_code_code_pc_central_lower_value bcf_row_code_scale_pc_central_lower_value bcf_row_scale_code_pc_central_lower_value bcf_row_scale_scale_pc_central_lower_value bcf_row_code_pc_central_lower_value bcf_row_scale_pc_central_lower_value. ((forall bcf_row_index_pc_central_lower_value_table. (exists bcf_lt_gap_pc_central_lower_value_table_row_bound. bcf_lt_gap_pc_central_lower_value_table_row_bound + S (bcf_row_index_pc_central_lower_value_table) = S (n + n)) -> exists bcf_row_code_pc_central_lower_value_table bcf_row_scale_pc_central_lower_value_table. ((((exists bcf_height_pc_central_lower_value_table_decoded_row_code. bcf_height_pc_central_lower_value_table_decoded_row_code + S (bcf_row_code_pc_central_lower_value_table) = S ((S (bcf_row_index_pc_central_lower_value_table)) * bcf_row_code_scale_pc_central_lower_value)) /\ exists bcf_quotient_pc_central_lower_value_table_decoded_row_code. bcf_row_code_code_pc_central_lower_value = bcf_quotient_pc_central_lower_value_table_decoded_row_code * S ((S (bcf_row_index_pc_central_lower_value_table)) * bcf_row_code_scale_pc_central_lower_value) + (bcf_row_code_pc_central_lower_value_table))) /\ ((((exists bcf_height_pc_central_lower_value_table_decoded_row_scale. bcf_height_pc_central_lower_value_table_decoded_row_scale + S (bcf_row_scale_pc_central_lower_value_table) = S ((S (bcf_row_index_pc_central_lower_value_table)) * bcf_row_scale_scale_pc_central_lower_value)) /\ exists bcf_quotient_pc_central_lower_value_table_decoded_row_scale. bcf_row_scale_code_pc_central_lower_value = bcf_quotient_pc_central_lower_value_table_decoded_row_scale * S ((S (bcf_row_index_pc_central_lower_value_table)) * bcf_row_scale_scale_pc_central_lower_value) + (bcf_row_scale_pc_central_lower_value_table))) /\ ((bcf_row_index_pc_central_lower_value_table = 0 /\ (forall bcf_index_pc_central_lower_value_table_zero_row. (exists bcf_lt_gap_pc_central_lower_value_table_zero_row_bound. bcf_lt_gap_pc_central_lower_value_table_zero_row_bound + S (bcf_index_pc_central_lower_value_table_zero_row) = S (n + n)) -> exists bcf_value_pc_central_lower_value_table_zero_row. ((((exists bcf_height_pc_central_lower_value_table_zero_row_entry. bcf_height_pc_central_lower_value_table_zero_row_entry + S (bcf_value_pc_central_lower_value_table_zero_row) = S ((S (bcf_index_pc_central_lower_value_table_zero_row)) * bcf_row_scale_pc_central_lower_value_table)) /\ exists bcf_quotient_pc_central_lower_value_table_zero_row_entry. bcf_row_code_pc_central_lower_value_table = bcf_quotient_pc_central_lower_value_table_zero_row_entry * S ((S (bcf_index_pc_central_lower_value_table_zero_row)) * bcf_row_scale_pc_central_lower_value_table) + (bcf_value_pc_central_lower_value_table_zero_row))) /\ ((bcf_index_pc_central_lower_value_table_zero_row = 0 /\ bcf_value_pc_central_lower_value_table_zero_row = 1) \/ exists bcf_predecessor_pc_central_lower_value_table_zero_row. bcf_index_pc_central_lower_value_table_zero_row = S bcf_predecessor_pc_central_lower_value_table_zero_row /\ bcf_value_pc_central_lower_value_table_zero_row = 0)))) \/ exists bcf_predecessor_pc_central_lower_value_table bcf_previous_code_pc_central_lower_value_table bcf_previous_scale_pc_central_lower_value_table. bcf_row_index_pc_central_lower_value_table = S bcf_predecessor_pc_central_lower_value_table /\ ((((exists bcf_height_pc_central_lower_value_table_decoded_previous_code. bcf_height_pc_central_lower_value_table_decoded_previous_code + S (bcf_previous_code_pc_central_lower_value_table) = S ((S (bcf_predecessor_pc_central_lower_value_table)) * bcf_row_code_scale_pc_central_lower_value)) /\ exists bcf_quotient_pc_central_lower_value_table_decoded_previous_code. bcf_row_code_code_pc_central_lower_value = bcf_quotient_pc_central_lower_value_table_decoded_previous_code * S ((S (bcf_predecessor_pc_central_lower_value_table)) * bcf_row_code_scale_pc_central_lower_value) + (bcf_previous_code_pc_central_lower_value_table))) /\ ((((exists bcf_height_pc_central_lower_value_table_decoded_previous_scale. bcf_height_pc_central_lower_value_table_decoded_previous_scale + S (bcf_previous_scale_pc_central_lower_value_table) = S ((S (bcf_predecessor_pc_central_lower_value_table)) * bcf_row_scale_scale_pc_central_lower_value)) /\ exists bcf_quotient_pc_central_lower_value_table_decoded_previous_scale. bcf_row_scale_code_pc_central_lower_value = bcf_quotient_pc_central_lower_value_table_decoded_previous_scale * S ((S (bcf_predecessor_pc_central_lower_value_table)) * bcf_row_scale_scale_pc_central_lower_value) + (bcf_previous_scale_pc_central_lower_value_table))) /\ (forall bcf_index_pc_central_lower_value_table_row_step. (exists bcf_lt_gap_pc_central_lower_value_table_row_step_bound. bcf_lt_gap_pc_central_lower_value_table_row_step_bound + S (bcf_index_pc_central_lower_value_table_row_step) = S (n + n)) -> exists bcf_value_pc_central_lower_value_table_row_step. ((((exists bcf_height_pc_central_lower_value_table_row_step_entry. bcf_height_pc_central_lower_value_table_row_step_entry + S (bcf_value_pc_central_lower_value_table_row_step) = S ((S (bcf_index_pc_central_lower_value_table_row_step)) * bcf_row_scale_pc_central_lower_value_table)) /\ exists bcf_quotient_pc_central_lower_value_table_row_step_entry. bcf_row_code_pc_central_lower_value_table = bcf_quotient_pc_central_lower_value_table_row_step_entry * S ((S (bcf_index_pc_central_lower_value_table_row_step)) * bcf_row_scale_pc_central_lower_value_table) + (bcf_value_pc_central_lower_value_table_row_step))) /\ ((bcf_index_pc_central_lower_value_table_row_step = 0 /\ bcf_value_pc_central_lower_value_table_row_step = 1) \/ exists bcf_predecessor_pc_central_lower_value_table_row_step bcf_left_pc_central_lower_value_table_row_step bcf_right_pc_central_lower_value_table_row_step. bcf_index_pc_central_lower_value_table_row_step = S bcf_predecessor_pc_central_lower_value_table_row_step /\ ((((exists bcf_height_pc_central_lower_value_table_row_step_previous_left. bcf_height_pc_central_lower_value_table_row_step_previous_left + S (bcf_left_pc_central_lower_value_table_row_step) = S ((S (bcf_predecessor_pc_central_lower_value_table_row_step)) * bcf_previous_scale_pc_central_lower_value_table)) /\ exists bcf_quotient_pc_central_lower_value_table_row_step_previous_left. bcf_previous_code_pc_central_lower_value_table = bcf_quotient_pc_central_lower_value_table_row_step_previous_left * S ((S (bcf_predecessor_pc_central_lower_value_table_row_step)) * bcf_previous_scale_pc_central_lower_value_table) + (bcf_left_pc_central_lower_value_table_row_step))) /\ ((((exists bcf_height_pc_central_lower_value_table_row_step_previous_right. bcf_height_pc_central_lower_value_table_row_step_previous_right + S (bcf_right_pc_central_lower_value_table_row_step) = S ((S (S (bcf_predecessor_pc_central_lower_value_table_row_step))) * bcf_previous_scale_pc_central_lower_value_table)) /\ exists bcf_quotient_pc_central_lower_value_table_row_step_previous_right. bcf_previous_code_pc_central_lower_value_table = bcf_quotient_pc_central_lower_value_table_row_step_previous_right * S ((S (S (bcf_predecessor_pc_central_lower_value_table_row_step))) * bcf_previous_scale_pc_central_lower_value_table) + (bcf_right_pc_central_lower_value_table_row_step))) /\ bcf_value_pc_central_lower_value_table_row_step = bcf_left_pc_central_lower_value_table_row_step + bcf_right_pc_central_lower_value_table_row_step))))))))))) /\ ((((exists bcf_height_pc_central_lower_value_decoded_row_code. bcf_height_pc_central_lower_value_decoded_row_code + S (bcf_row_code_pc_central_lower_value) = S ((S (n + n)) * bcf_row_code_scale_pc_central_lower_value)) /\ exists bcf_quotient_pc_central_lower_value_decoded_row_code. bcf_row_code_code_pc_central_lower_value = bcf_quotient_pc_central_lower_value_decoded_row_code * S ((S (n + n)) * bcf_row_code_scale_pc_central_lower_value) + (bcf_row_code_pc_central_lower_value))) /\ ((((exists bcf_height_pc_central_lower_value_decoded_row_scale. bcf_height_pc_central_lower_value_decoded_row_scale + S (bcf_row_scale_pc_central_lower_value) = S ((S (n + n)) * bcf_row_scale_scale_pc_central_lower_value)) /\ exists bcf_quotient_pc_central_lower_value_decoded_row_scale. bcf_row_scale_code_pc_central_lower_value = bcf_quotient_pc_central_lower_value_decoded_row_scale * S ((S (n + n)) * bcf_row_scale_scale_pc_central_lower_value) + (bcf_row_scale_pc_central_lower_value))) /\ (((exists bcf_height_pc_central_lower_value_decoded_value. bcf_height_pc_central_lower_value_decoded_value + S (C) = S ((S (n)) * bcf_row_scale_pc_central_lower_value)) /\ exists bcf_quotient_pc_central_lower_value_decoded_value. bcf_row_code_pc_central_lower_value = bcf_quotient_pc_central_lower_value_decoded_value * S ((S (n)) * bcf_row_scale_pc_central_lower_value) + (C))))))))) -> (exists pa_b_pc_central_lower_power pa_c_pc_central_lower_power. ((forall pa_i_pc_central_lower_power_repeat. (exists pa_lt_pc_central_lower_power_repeat_bound. pa_lt_pc_central_lower_power_repeat_bound + S pa_i_pc_central_lower_power_repeat = n) -> (((exists pa_h_pc_central_lower_power_repeat_decoded. pa_h_pc_central_lower_power_repeat_decoded + S (2) = S ((S (pa_i_pc_central_lower_power_repeat)) * pa_c_pc_central_lower_power)) /\ exists pa_q_pc_central_lower_power_repeat_decoded. pa_b_pc_central_lower_power = pa_q_pc_central_lower_power_repeat_decoded * S ((S (pa_i_pc_central_lower_power_repeat)) * pa_c_pc_central_lower_power) + (2)))) /\ (exists pa_u_pc_central_lower_power_product pa_v_pc_central_lower_power_product. ((((exists pa_h_pc_central_lower_power_product_start. pa_h_pc_central_lower_power_product_start + S (1) = S ((S (0)) * pa_v_pc_central_lower_power_product)) /\ exists pa_q_pc_central_lower_power_product_start. pa_u_pc_central_lower_power_product = pa_q_pc_central_lower_power_product_start * S ((S (0)) * pa_v_pc_central_lower_power_product) + (1))) /\ ((((exists pa_h_pc_central_lower_power_product_terminal. pa_h_pc_central_lower_power_product_terminal + S (v) = S ((S (n)) * pa_v_pc_central_lower_power_product)) /\ exists pa_q_pc_central_lower_power_product_terminal. pa_u_pc_central_lower_power_product = pa_q_pc_central_lower_power_product_terminal * S ((S (n)) * pa_v_pc_central_lower_power_product) + (v))) /\ forall pa_i_pc_central_lower_power_product. (exists pa_lt_pc_central_lower_power_product_bound. pa_lt_pc_central_lower_power_product_bound + S pa_i_pc_central_lower_power_product = n) -> exists pa_p_pc_central_lower_power_product pa_r_pc_central_lower_power_product pa_s_pc_central_lower_power_product. ((((exists pa_h_pc_central_lower_power_product_factor. pa_h_pc_central_lower_power_product_factor + S (pa_p_pc_central_lower_power_product) = S ((S (pa_i_pc_central_lower_power_product)) * pa_c_pc_central_lower_power)) /\ exists pa_q_pc_central_lower_power_product_factor. pa_b_pc_central_lower_power = pa_q_pc_central_lower_power_product_factor * S ((S (pa_i_pc_central_lower_power_product)) * pa_c_pc_central_lower_power) + (pa_p_pc_central_lower_power_product))) /\ ((((exists pa_h_pc_central_lower_power_product_partial. pa_h_pc_central_lower_power_product_partial + S (pa_r_pc_central_lower_power_product) = S ((S (pa_i_pc_central_lower_power_product)) * pa_v_pc_central_lower_power_product)) /\ exists pa_q_pc_central_lower_power_product_partial. pa_u_pc_central_lower_power_product = pa_q_pc_central_lower_power_product_partial * S ((S (pa_i_pc_central_lower_power_product)) * pa_v_pc_central_lower_power_product) + (pa_r_pc_central_lower_power_product))) /\ ((((exists pa_h_pc_central_lower_power_product_successor. pa_h_pc_central_lower_power_product_successor + S (pa_s_pc_central_lower_power_product) = S ((S (S pa_i_pc_central_lower_power_product)) * pa_v_pc_central_lower_power_product)) /\ exists pa_q_pc_central_lower_power_product_successor. pa_u_pc_central_lower_power_product = pa_q_pc_central_lower_power_product_successor * S ((S (S pa_i_pc_central_lower_power_product)) * pa_v_pc_central_lower_power_product) + (pa_s_pc_central_lower_power_product))) /\ pa_s_pc_central_lower_power_product = pa_r_pc_central_lower_power_product * pa_p_pc_central_lower_power_product)))))))) -> (exists pc_le_central_lower_result. pc_le_central_lower_result + (v) = (C))

Complete tactic proof in conservative notation

All 65 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

65 script commands · 15 reading checkpoints · 6 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)
pow four is square of pow twobinary power two dominates successor
01Fix variables and assumptionsL1–6

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

  1. L1
    intro n
  2. L2
    intro C
  3. L3
    intro v
  4. L4
    intro hn
  5. L5
    intro hC
  6. L6
    intro hv
02Establish hwL7–10

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

  1. L7
    have hw : ∃ w. Pow(4,n,w)Definitions: Pow(4,n,w)Original native command in the exact edition
  2. L8
    specialize pow_exists 4
  3. L9
    specialize pow_exists n
  4. L10
    apply pow_exists
03Separate the logical casesL11–11

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

  1. L11
    cases hw
04Establish hsquareL12–18

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

  1. L12
    have hsquare : x = v * v
  2. L13
    specialize pow_four_is_square_of_pow_two n
  3. L14
    specialize pow_four_is_square_of_pow_two v
  4. L15
    specialize pow_four_is_square_of_pow_two x
  5. L16
    apply pow_four_is_square_of_pow_two
  6. L17
    exact hv
  7. L18
    exact hw_witness
05Establish hlowerL19–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four pow lt mul central binom.

  1. L19
    have hlower : Lt(x,n · C)Definitions: Lt(x,n · C)Original native command in the exact edition
  2. L20
    specialize four_pow_lt_mul_central_binom n
  3. L21
    specialize four_pow_lt_mul_central_binom x
  4. L22
    specialize four_pow_lt_mul_central_binom C
  5. L23
    apply four_pow_lt_mul_central_binom
  6. L24
    exact hn
  7. L25
    exact hw_witness
  8. L26
    exact hC
06Establish hnsmallL27–34

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

  1. L27
    have hnsmall : Le(n,v)Definitions: Le(n,v)Original native command in the exact edition
  2. L28
    specialize lt_to_le n
  3. L29
    specialize lt_to_le v
  4. L30
    apply lt_to_le
  5. L31
    specialize binary_power_two_dominates_successor n
  6. L32
    specialize binary_power_two_dominates_successor v
  7. L33
    apply binary_power_two_dominates_successor
  8. L34
    exact hv
07Establish hscaleL35–40

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

  1. L35
    have hscale : Le(n · C,v · C)Definitions: Le(n · C,v · C)Original native command in the exact edition
  2. L36
    specialize mul_le_mul_right n
  3. L37
    specialize mul_le_mul_right v
  4. L38
    specialize mul_le_mul_right C
  5. L39
    apply mul_le_mul_right
  6. L40
    exact hnsmall
08Establish hfullL41–50

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

  1. L41
    have hfull : Le(x,v · C)Definitions: Le(x,v · C)Original native command in the exact edition
  2. L42
    specialize le_trans x
  3. L43
    specialize le_trans (n * C)
  4. L44
    specialize le_trans (v * C)
  5. L45
    apply le_trans
  6. L46
    specialize lt_to_le x
  7. L47
    specialize lt_to_le (n * C)
  8. L48
    apply lt_to_le
  9. L49
    exact hlower
  10. L50
    exact hscale
09Calculate and transport equalitiesL51–51

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

  1. L51
    rewrite hsquare at hfull
10Use earlier factsL52–55

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

  1. L52
    specialize mul_le_cancel_left_nonzero v
  2. L53
    specialize mul_le_cancel_left_nonzero v
  3. L54
    specialize mul_le_cancel_left_nonzero C
  4. L55
    apply mul_le_cancel_left_nonzero
11Fix variables and assumptionsL56–56

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

  1. L56
    intro hz
12Use earlier factsL57–60

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

  1. L57
    specialize pow_nonzero_of_one_le 2
  2. L58
    specialize pow_nonzero_of_one_le n
  3. L59
    specialize pow_nonzero_of_one_le v
  4. L60
    apply pow_nonzero_of_one_le
13Construct an explicit witnessL61–61

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

  1. L61
    exists 1
14Calculate and transport equalitiesL62–62

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

  1. L62
    norm_num
15Use earlier factsL63–65

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

  1. L63
    exact hv
  2. L64
    exact hz
  3. L65
    exact hfull

Library-wide reading audit

Original defined command ledger · 65 lines
  1. 0001intro n
  2. 0002intro C
  3. 0003intro v
  4. 0004intro hn
  5. 0005intro hC
  6. 0006intro hv
  7. 0007have hw : ∃ w. Pow(4,n,w)
  8. 0008specialize pow_exists 4
  9. 0009specialize pow_exists n
  10. 0010apply pow_exists
  11. 0011cases hw
  12. 0012have hsquare : x = v * v
  13. 0013specialize pow_four_is_square_of_pow_two n
  14. 0014specialize pow_four_is_square_of_pow_two v
  15. 0015specialize pow_four_is_square_of_pow_two x
  16. 0016apply pow_four_is_square_of_pow_two
  17. 0017exact hv
  18. 0018exact hw_witness
  19. 0019have hlower : Lt(x,n · C)
  20. 0020specialize four_pow_lt_mul_central_binom n
  21. 0021specialize four_pow_lt_mul_central_binom x
  22. 0022specialize four_pow_lt_mul_central_binom C
  23. 0023apply four_pow_lt_mul_central_binom
  24. 0024exact hn
  25. 0025exact hw_witness
  26. 0026exact hC
  27. 0027have hnsmall : Le(n,v)
  28. 0028specialize lt_to_le n
  29. 0029specialize lt_to_le v
  30. 0030apply lt_to_le
  31. 0031specialize binary_power_two_dominates_successor n
  32. 0032specialize binary_power_two_dominates_successor v
  33. 0033apply binary_power_two_dominates_successor
  34. 0034exact hv
  35. 0035have hscale : Le(n · C,v · C)
  36. 0036specialize mul_le_mul_right n
  37. 0037specialize mul_le_mul_right v
  38. 0038specialize mul_le_mul_right C
  39. 0039apply mul_le_mul_right
  40. 0040exact hnsmall
  41. 0041have hfull : Le(x,v · C)
  42. 0042specialize le_trans x
  43. 0043specialize le_trans (n * C)
  44. 0044specialize le_trans (v * C)
  45. 0045apply le_trans
  46. 0046specialize lt_to_le x
  47. 0047specialize lt_to_le (n * C)
  48. 0048apply lt_to_le
  49. 0049exact hlower
  50. 0050exact hscale
  51. 0051rewrite hsquare at hfull
  52. 0052specialize mul_le_cancel_left_nonzero v
  53. 0053specialize mul_le_cancel_left_nonzero v
  54. 0054specialize mul_le_cancel_left_nonzero C
  55. 0055apply mul_le_cancel_left_nonzero
  56. 0056intro hz
  57. 0057specialize pow_nonzero_of_one_le 2
  58. 0058specialize pow_nonzero_of_one_le n
  59. 0059specialize pow_nonzero_of_one_le v
  60. 0060apply pow_nonzero_of_one_le
  61. 0061exists 1
  62. 0062norm_num
  63. 0063exact hv
  64. 0064exact hz
  65. 0065exact hfull