BT00U4 · Bertrand theorem

four_pow_lt_mul_central_binom

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

For every index at least four, the fourth power is below the index-weighted central binomial.

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.

Statement with defined notation

∀ n. ∀ p. ∀ c. Lt(3,n) → Pow(4,n,p) → CentralBinom(n,c) → Lt(p,n · c)

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0020 Pow PD0042 CentralBinom

4 occurrences

In local proof propositions

PD0002 Lt PD0020 Pow PD0042 CentralBinom

13 occurrences

Exact expanded native-PA statement
forall n p c. (exists bcf_le_gap_bfplcb_bound. bcf_le_gap_bfplcb_bound + (4) = n) -> (exists pa_b_bfplcb_power pa_c_bfplcb_power. ((forall pa_i_bfplcb_power_repeat. (exists pa_lt_bfplcb_power_repeat_bound. pa_lt_bfplcb_power_repeat_bound + S pa_i_bfplcb_power_repeat = n) -> (((exists pa_h_bfplcb_power_repeat_decoded. pa_h_bfplcb_power_repeat_decoded + S (4) = S ((S (pa_i_bfplcb_power_repeat)) * pa_c_bfplcb_power)) /\ exists pa_q_bfplcb_power_repeat_decoded. pa_b_bfplcb_power = pa_q_bfplcb_power_repeat_decoded * S ((S (pa_i_bfplcb_power_repeat)) * pa_c_bfplcb_power) + (4)))) /\ (exists pa_u_bfplcb_power_product pa_v_bfplcb_power_product. ((((exists pa_h_bfplcb_power_product_start. pa_h_bfplcb_power_product_start + S (1) = S ((S (0)) * pa_v_bfplcb_power_product)) /\ exists pa_q_bfplcb_power_product_start. pa_u_bfplcb_power_product = pa_q_bfplcb_power_product_start * S ((S (0)) * pa_v_bfplcb_power_product) + (1))) /\ ((((exists pa_h_bfplcb_power_product_terminal. pa_h_bfplcb_power_product_terminal + S (p) = S ((S (n)) * pa_v_bfplcb_power_product)) /\ exists pa_q_bfplcb_power_product_terminal. pa_u_bfplcb_power_product = pa_q_bfplcb_power_product_terminal * S ((S (n)) * pa_v_bfplcb_power_product) + (p))) /\ forall pa_i_bfplcb_power_product. (exists pa_lt_bfplcb_power_product_bound. pa_lt_bfplcb_power_product_bound + S pa_i_bfplcb_power_product = n) -> exists pa_p_bfplcb_power_product pa_r_bfplcb_power_product pa_s_bfplcb_power_product. ((((exists pa_h_bfplcb_power_product_factor. pa_h_bfplcb_power_product_factor + S (pa_p_bfplcb_power_product) = S ((S (pa_i_bfplcb_power_product)) * pa_c_bfplcb_power)) /\ exists pa_q_bfplcb_power_product_factor. pa_b_bfplcb_power = pa_q_bfplcb_power_product_factor * S ((S (pa_i_bfplcb_power_product)) * pa_c_bfplcb_power) + (pa_p_bfplcb_power_product))) /\ ((((exists pa_h_bfplcb_power_product_partial. pa_h_bfplcb_power_product_partial + S (pa_r_bfplcb_power_product) = S ((S (pa_i_bfplcb_power_product)) * pa_v_bfplcb_power_product)) /\ exists pa_q_bfplcb_power_product_partial. pa_u_bfplcb_power_product = pa_q_bfplcb_power_product_partial * S ((S (pa_i_bfplcb_power_product)) * pa_v_bfplcb_power_product) + (pa_r_bfplcb_power_product))) /\ ((((exists pa_h_bfplcb_power_product_successor. pa_h_bfplcb_power_product_successor + S (pa_s_bfplcb_power_product) = S ((S (S pa_i_bfplcb_power_product)) * pa_v_bfplcb_power_product)) /\ exists pa_q_bfplcb_power_product_successor. pa_u_bfplcb_power_product = pa_q_bfplcb_power_product_successor * S ((S (S pa_i_bfplcb_power_product)) * pa_v_bfplcb_power_product) + (pa_s_bfplcb_power_product))) /\ pa_s_bfplcb_power_product = pa_r_bfplcb_power_product * pa_p_bfplcb_power_product)))))))) -> (((exists bcf_lt_gap_bfplcb_central_out_of_range. bcf_lt_gap_bfplcb_central_out_of_range + S (n + n) = n) /\ c = 0) \/ ((exists bcf_le_gap_bfplcb_central_in_range. bcf_le_gap_bfplcb_central_in_range + (n) = n + n) /\ (exists bcf_row_code_code_bfplcb_central bcf_row_code_scale_bfplcb_central bcf_row_scale_code_bfplcb_central bcf_row_scale_scale_bfplcb_central bcf_row_code_bfplcb_central bcf_row_scale_bfplcb_central. ((forall bcf_row_index_bfplcb_central_table. (exists bcf_lt_gap_bfplcb_central_table_row_bound. bcf_lt_gap_bfplcb_central_table_row_bound + S (bcf_row_index_bfplcb_central_table) = S (n + n)) -> exists bcf_row_code_bfplcb_central_table bcf_row_scale_bfplcb_central_table. ((((exists bcf_height_bfplcb_central_table_decoded_row_code. bcf_height_bfplcb_central_table_decoded_row_code + S (bcf_row_code_bfplcb_central_table) = S ((S (bcf_row_index_bfplcb_central_table)) * bcf_row_code_scale_bfplcb_central)) /\ exists bcf_quotient_bfplcb_central_table_decoded_row_code. bcf_row_code_code_bfplcb_central = bcf_quotient_bfplcb_central_table_decoded_row_code * S ((S (bcf_row_index_bfplcb_central_table)) * bcf_row_code_scale_bfplcb_central) + (bcf_row_code_bfplcb_central_table))) /\ ((((exists bcf_height_bfplcb_central_table_decoded_row_scale. bcf_height_bfplcb_central_table_decoded_row_scale + S (bcf_row_scale_bfplcb_central_table) = S ((S (bcf_row_index_bfplcb_central_table)) * bcf_row_scale_scale_bfplcb_central)) /\ exists bcf_quotient_bfplcb_central_table_decoded_row_scale. bcf_row_scale_code_bfplcb_central = bcf_quotient_bfplcb_central_table_decoded_row_scale * S ((S (bcf_row_index_bfplcb_central_table)) * bcf_row_scale_scale_bfplcb_central) + (bcf_row_scale_bfplcb_central_table))) /\ ((bcf_row_index_bfplcb_central_table = 0 /\ (forall bcf_index_bfplcb_central_table_zero_row. (exists bcf_lt_gap_bfplcb_central_table_zero_row_bound. bcf_lt_gap_bfplcb_central_table_zero_row_bound + S (bcf_index_bfplcb_central_table_zero_row) = S (n + n)) -> exists bcf_value_bfplcb_central_table_zero_row. ((((exists bcf_height_bfplcb_central_table_zero_row_entry. bcf_height_bfplcb_central_table_zero_row_entry + S (bcf_value_bfplcb_central_table_zero_row) = S ((S (bcf_index_bfplcb_central_table_zero_row)) * bcf_row_scale_bfplcb_central_table)) /\ exists bcf_quotient_bfplcb_central_table_zero_row_entry. bcf_row_code_bfplcb_central_table = bcf_quotient_bfplcb_central_table_zero_row_entry * S ((S (bcf_index_bfplcb_central_table_zero_row)) * bcf_row_scale_bfplcb_central_table) + (bcf_value_bfplcb_central_table_zero_row))) /\ ((bcf_index_bfplcb_central_table_zero_row = 0 /\ bcf_value_bfplcb_central_table_zero_row = 1) \/ exists bcf_predecessor_bfplcb_central_table_zero_row. bcf_index_bfplcb_central_table_zero_row = S bcf_predecessor_bfplcb_central_table_zero_row /\ bcf_value_bfplcb_central_table_zero_row = 0)))) \/ exists bcf_predecessor_bfplcb_central_table bcf_previous_code_bfplcb_central_table bcf_previous_scale_bfplcb_central_table. bcf_row_index_bfplcb_central_table = S bcf_predecessor_bfplcb_central_table /\ ((((exists bcf_height_bfplcb_central_table_decoded_previous_code. bcf_height_bfplcb_central_table_decoded_previous_code + S (bcf_previous_code_bfplcb_central_table) = S ((S (bcf_predecessor_bfplcb_central_table)) * bcf_row_code_scale_bfplcb_central)) /\ exists bcf_quotient_bfplcb_central_table_decoded_previous_code. bcf_row_code_code_bfplcb_central = bcf_quotient_bfplcb_central_table_decoded_previous_code * S ((S (bcf_predecessor_bfplcb_central_table)) * bcf_row_code_scale_bfplcb_central) + (bcf_previous_code_bfplcb_central_table))) /\ ((((exists bcf_height_bfplcb_central_table_decoded_previous_scale. bcf_height_bfplcb_central_table_decoded_previous_scale + S (bcf_previous_scale_bfplcb_central_table) = S ((S (bcf_predecessor_bfplcb_central_table)) * bcf_row_scale_scale_bfplcb_central)) /\ exists bcf_quotient_bfplcb_central_table_decoded_previous_scale. bcf_row_scale_code_bfplcb_central = bcf_quotient_bfplcb_central_table_decoded_previous_scale * S ((S (bcf_predecessor_bfplcb_central_table)) * bcf_row_scale_scale_bfplcb_central) + (bcf_previous_scale_bfplcb_central_table))) /\ (forall bcf_index_bfplcb_central_table_row_step. (exists bcf_lt_gap_bfplcb_central_table_row_step_bound. bcf_lt_gap_bfplcb_central_table_row_step_bound + S (bcf_index_bfplcb_central_table_row_step) = S (n + n)) -> exists bcf_value_bfplcb_central_table_row_step. ((((exists bcf_height_bfplcb_central_table_row_step_entry. bcf_height_bfplcb_central_table_row_step_entry + S (bcf_value_bfplcb_central_table_row_step) = S ((S (bcf_index_bfplcb_central_table_row_step)) * bcf_row_scale_bfplcb_central_table)) /\ exists bcf_quotient_bfplcb_central_table_row_step_entry. bcf_row_code_bfplcb_central_table = bcf_quotient_bfplcb_central_table_row_step_entry * S ((S (bcf_index_bfplcb_central_table_row_step)) * bcf_row_scale_bfplcb_central_table) + (bcf_value_bfplcb_central_table_row_step))) /\ ((bcf_index_bfplcb_central_table_row_step = 0 /\ bcf_value_bfplcb_central_table_row_step = 1) \/ exists bcf_predecessor_bfplcb_central_table_row_step bcf_left_bfplcb_central_table_row_step bcf_right_bfplcb_central_table_row_step. bcf_index_bfplcb_central_table_row_step = S bcf_predecessor_bfplcb_central_table_row_step /\ ((((exists bcf_height_bfplcb_central_table_row_step_previous_left. bcf_height_bfplcb_central_table_row_step_previous_left + S (bcf_left_bfplcb_central_table_row_step) = S ((S (bcf_predecessor_bfplcb_central_table_row_step)) * bcf_previous_scale_bfplcb_central_table)) /\ exists bcf_quotient_bfplcb_central_table_row_step_previous_left. bcf_previous_code_bfplcb_central_table = bcf_quotient_bfplcb_central_table_row_step_previous_left * S ((S (bcf_predecessor_bfplcb_central_table_row_step)) * bcf_previous_scale_bfplcb_central_table) + (bcf_left_bfplcb_central_table_row_step))) /\ ((((exists bcf_height_bfplcb_central_table_row_step_previous_right. bcf_height_bfplcb_central_table_row_step_previous_right + S (bcf_right_bfplcb_central_table_row_step) = S ((S (S (bcf_predecessor_bfplcb_central_table_row_step))) * bcf_previous_scale_bfplcb_central_table)) /\ exists bcf_quotient_bfplcb_central_table_row_step_previous_right. bcf_previous_code_bfplcb_central_table = bcf_quotient_bfplcb_central_table_row_step_previous_right * S ((S (S (bcf_predecessor_bfplcb_central_table_row_step))) * bcf_previous_scale_bfplcb_central_table) + (bcf_right_bfplcb_central_table_row_step))) /\ bcf_value_bfplcb_central_table_row_step = bcf_left_bfplcb_central_table_row_step + bcf_right_bfplcb_central_table_row_step))))))))))) /\ ((((exists bcf_height_bfplcb_central_decoded_row_code. bcf_height_bfplcb_central_decoded_row_code + S (bcf_row_code_bfplcb_central) = S ((S (n + n)) * bcf_row_code_scale_bfplcb_central)) /\ exists bcf_quotient_bfplcb_central_decoded_row_code. bcf_row_code_code_bfplcb_central = bcf_quotient_bfplcb_central_decoded_row_code * S ((S (n + n)) * bcf_row_code_scale_bfplcb_central) + (bcf_row_code_bfplcb_central))) /\ ((((exists bcf_height_bfplcb_central_decoded_row_scale. bcf_height_bfplcb_central_decoded_row_scale + S (bcf_row_scale_bfplcb_central) = S ((S (n + n)) * bcf_row_scale_scale_bfplcb_central)) /\ exists bcf_quotient_bfplcb_central_decoded_row_scale. bcf_row_scale_code_bfplcb_central = bcf_quotient_bfplcb_central_decoded_row_scale * S ((S (n + n)) * bcf_row_scale_scale_bfplcb_central) + (bcf_row_scale_bfplcb_central))) /\ (((exists bcf_height_bfplcb_central_decoded_value. bcf_height_bfplcb_central_decoded_value + S (c) = S ((S (n)) * bcf_row_scale_bfplcb_central)) /\ exists bcf_quotient_bfplcb_central_decoded_value. bcf_row_code_bfplcb_central = bcf_quotient_bfplcb_central_decoded_value * S ((S (n)) * bcf_row_scale_bfplcb_central) + (c))))))))) -> (exists bcf_lt_gap_bfplcb_result. bcf_lt_gap_bfplcb_result + S (p) = n * c)

Proof neighborhood

Direct theorem prerequisites

BT001I lt_not_le BT0083 pow_successor_decompose BT00TU central_binom_succ_recurrence BT00U0 four_power_central_recurrence_step BT00U3 four_pow_central_seed_package

Direct theorem dependents

BT0115 bertrand_eventually_closed_upper

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

105 script commands · 38 reading checkpoints · 11 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 (5)
lt not lepow successor decomposecentral binom succ recurrencefour power central recurrence stepfour pow central seed package
01Establish hzero_lt_fourL1–1

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

  1. L1
    have hzero_lt_four : Lt(0,4)Definitions: Lt(0,4)Original native command in the exact edition
02Construct an explicit witnessL2–2

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

  1. L2
    exists 3
03Calculate and transport equalitiesL3–3

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

  1. L3
    norm_num
04Establish hone_lt_fourL4–4

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

  1. L4
    have hone_lt_four : Lt(1,4)Definitions: Lt(1,4)Original native command in the exact edition
05Construct an explicit witnessL5–5

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

  1. L5
    exists 2
06Calculate and transport equalitiesL6–6

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

  1. L6
    norm_num
07Establish htwo_lt_fourL7–7

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

  1. L7
    have htwo_lt_four : Lt(2,4)Definitions: Lt(2,4)Original native command in the exact edition
08Construct an explicit witnessL8–8

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

  1. L8
    exists 1
09Calculate and transport equalitiesL9–9

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

  1. L9
    norm_num
10Establish hthree_lt_fourL10–10

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

  1. L10
    have hthree_lt_four : Lt(3,4)Definitions: Lt(3,4)Original native command in the exact edition
11Construct an explicit witnessL11–11

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

  1. L11
    exists 0
12Calculate and transport equalitiesL12–12

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

  1. L12
    norm_num
13Establish hpackageL13–15

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

  1. L13
    have hpackage : (∀ x. ∃ y. CentralBinom(x,y)) ∧ (∀ x. ∀ y. Pow(4,4,x) → CentralBinom(4,y) → Lt(x,4 · y))Definitions: CentralBinom(x,y)Pow(4,4,x)CentralBinom(4,y)Lt(x,4 · y)Original native command in the exact edition
  2. L14
    apply four_pow_central_seed_package
  3. L15
    exact central_binom_succ_recurrence
14Separate the logical casesL16–16

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

  1. L16
    cases hpackage
15Induction on nL17–22

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

  1. L17
    induction n
  2. L18
    intro p
  3. L19
    intro c
  4. L20
    intro hbound
  5. L21
    intro hpower
  6. L22
    intro hcentral
16Separate the logical casesL23–23

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

  1. L23
    exfalso
17Use earlier factsL24–28

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

  1. L24
    specialize lt_not_le 0
  2. L25
    specialize lt_not_le 4
  3. L26
    apply lt_not_le
  4. L27
    exact hzero_lt_four
  5. L28
    exact hbound
18Induction on nL29–34

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

  1. L29
    induction n
  2. L30
    intro p
  3. L31
    intro c
  4. L32
    intro hbound
  5. L33
    intro hpower
  6. L34
    intro hcentral
19Separate the logical casesL35–35

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

  1. L35
    exfalso
20Use earlier factsL36–40

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

  1. L36
    specialize lt_not_le 1
  2. L37
    specialize lt_not_le 4
  3. L38
    apply lt_not_le
  4. L39
    exact hone_lt_four
  5. L40
    exact hbound
21Induction on nL41–46

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

  1. L41
    induction n
  2. L42
    intro p
  3. L43
    intro c
  4. L44
    intro hbound
  5. L45
    intro hpower
  6. L46
    intro hcentral
22Separate the logical casesL47–47

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

  1. L47
    exfalso
23Use earlier factsL48–52

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

  1. L48
    specialize lt_not_le 2
  2. L49
    specialize lt_not_le 4
  3. L50
    apply lt_not_le
  4. L51
    exact htwo_lt_four
  5. L52
    exact hbound
24Induction on nL53–58

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

  1. L53
    induction n
  2. L54
    intro p
  3. L55
    intro c
  4. L56
    intro hbound
  5. L57
    intro hpower
  6. L58
    intro hcentral
25Separate the logical casesL59–59

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

  1. L59
    exfalso
26Use earlier factsL60–64

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

  1. L60
    specialize lt_not_le 3
  2. L61
    specialize lt_not_le 4
  3. L62
    apply lt_not_le
  4. L63
    exact hthree_lt_four
  5. L64
    exact hbound
27Induction on nL65–74

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

  1. L65
    induction n
  2. L66
    intro p
  3. L67
    intro c
  4. L68
    intro hbound
  5. L69
    intro hpower
  6. L70
    intro hcentral
  7. L71
    apply hpackage_right
  8. L72
    exact hpower
  9. L73
    exact hcentral
  10. L74
    intro p
28Fix variables and assumptionsL75–78

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

  1. L75
    intro c
  2. L76
    intro hbound
  3. L77
    intro hpower
  4. L78
    intro hcentral
29Establish hpower_stepL79–82

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

  1. L79
    have hpower_step : ∃ r. Pow(4,S S S S n,r) ∧ p = r · 4Definitions: Pow(4,S S S S n,r)Original native command in the exact edition
  2. L80
    apply pow_successor_decompose
  3. L81
    refl
  4. L82
    exact hpower
30Separate the logical casesL83–84

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

  1. L83
    cases hpower_step
  2. L84
    cases hpower_step_witness
31Establish hpredecessor_existsL85–86

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

  1. L85
    have hpredecessor_exists : ∃ a. CentralBinom(S S S S n,a)Definitions: CentralBinom(S S S S n,a)Original native command in the exact edition
  2. L86
    apply hpackage_left
32Separate the logical casesL87–87

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

  1. L87
    cases hpredecessor_exists
33Establish hpredecessor_boundL88–88

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

  1. L88
    have hpredecessor_bound : Lt(3,S S S S n)Definitions: Lt(3,S S S S n)Original native command in the exact edition
34Construct an explicit witnessL89–89

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

  1. L89
    exists n
35Calculate and transport equalitiesL90–90

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

  1. L90
    simp
36Establish hstrictL91–95

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

  1. L91
    have hstrict : Lt(x,S S S S n · x1)Definitions: Lt(x,S S S S n · x1)Original native command in the exact edition
  2. L92
    apply IH4
  3. L93
    exact hpredecessor_bound
  4. L94
    exact hpower_step_witness_left
  5. L95
    exact hpredecessor_exists_witness
37Establish hrecurrenceL96–99

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply central binom succ recurrence.

  1. L96
    have hrecurrence : S (S (S (S (S n)))) * c = (2 * S (S (S (S (S n))) + S (S (S (S n))))) * x1
  2. L97
    apply central_binom_succ_recurrence
  3. L98
    exact hpredecessor_exists_witness
  4. L99
    exact hcentral
38Establish hstepL100–105

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four power central recurrence step.

  1. L100
    have hstep : Lt(x · 4,S S S S S n · c)Definitions: Lt(x · 4,S S S S S n · c)Original native command in the exact edition
  2. L101
    apply four_power_central_recurrence_step
  3. L102
    exact hstrict
  4. L103
    exact hrecurrence
  5. L104
    rewrite hpower_step_witness_right
  6. L105
    exact hstep

Library-wide reading audit

Original defined command ledger · 105 lines
  1. 0001have hzero_lt_four : Lt(0,4)
    Exact native replay linehave hzero_lt_four : exists bcf_lt_gap_bfplcb_zero_lt_four. bcf_lt_gap_bfplcb_zero_lt_four + S (0) = 4
  2. 0002exists 3
  3. 0003norm_num
  4. 0004have hone_lt_four : Lt(1,4)
    Exact native replay linehave hone_lt_four : exists bcf_lt_gap_bfplcb_one_lt_four. bcf_lt_gap_bfplcb_one_lt_four + S (1) = 4
  5. 0005exists 2
  6. 0006norm_num
  7. 0007have htwo_lt_four : Lt(2,4)
    Exact native replay linehave htwo_lt_four : exists bcf_lt_gap_bfplcb_two_lt_four. bcf_lt_gap_bfplcb_two_lt_four + S (2) = 4
  8. 0008exists 1
  9. 0009norm_num
  10. 0010have hthree_lt_four : Lt(3,4)
    Exact native replay linehave hthree_lt_four : exists bcf_lt_gap_bfplcb_three_lt_four. bcf_lt_gap_bfplcb_three_lt_four + S (3) = 4
  11. 0011exists 0
  12. 0012norm_num
  13. 0013have hpackage : (∀ x. ∃ y. CentralBinom(x,y)) ∧ (∀ x. ∀ y. Pow(4,4,x) → CentralBinom(4,y) → Lt(x,4 · y))
    Exact native replay linehave hpackage : (forall n. exists z. (((exists bcf_lt_gap_bcb4we_exists_out_of_range. bcf_lt_gap_bcb4we_exists_out_of_range + S (n + n) = n) /\ z = 0) \/ ((exists bcf_le_gap_bcb4we_exists_in_range. bcf_le_gap_bcb4we_exists_in_range + (n) = n + n) /\ (exists bcf_row_code_code_bcb4we_exists bcf_row_code_scale_bcb4we_exists bcf_row_scale_code_bcb4we_exists bcf_row_scale_scale_bcb4we_exists bcf_row_code_bcb4we_exists bcf_row_scale_bcb4we_exists. ((forall bcf_row_index_bcb4we_exists_table. (exists bcf_lt_gap_bcb4we_exists_table_row_bound. bcf_lt_gap_bcb4we_exists_table_row_bound + S (bcf_row_index_bcb4we_exists_table) = S (n + n)) -> exists bcf_row_code_bcb4we_exists_table bcf_row_scale_bcb4we_exists_table. ((((exists bcf_height_bcb4we_exists_table_decoded_row_code. bcf_height_bcb4we_exists_table_decoded_row_code + S (bcf_row_code_bcb4we_exists_table) = S ((S (bcf_row_index_bcb4we_exists_table)) * bcf_row_code_scale_bcb4we_exists)) /\ exists bcf_quotient_bcb4we_exists_table_decoded_row_code. bcf_row_code_code_bcb4we_exists = bcf_quotient_bcb4we_exists_table_decoded_row_code * S ((S (bcf_row_index_bcb4we_exists_table)) * bcf_row_code_scale_bcb4we_exists) + (bcf_row_code_bcb4we_exists_table))) /\ ((((exists bcf_height_bcb4we_exists_table_decoded_row_scale. bcf_height_bcb4we_exists_table_decoded_row_scale + S (bcf_row_scale_bcb4we_exists_table) = S ((S (bcf_row_index_bcb4we_exists_table)) * bcf_row_scale_scale_bcb4we_exists)) /\ exists bcf_quotient_bcb4we_exists_table_decoded_row_scale. bcf_row_scale_code_bcb4we_exists = bcf_quotient_bcb4we_exists_table_decoded_row_scale * S ((S (bcf_row_index_bcb4we_exists_table)) * bcf_row_scale_scale_bcb4we_exists) + (bcf_row_scale_bcb4we_exists_table))) /\ ((bcf_row_index_bcb4we_exists_table = 0 /\ (forall bcf_index_bcb4we_exists_table_zero_row. (exists bcf_lt_gap_bcb4we_exists_table_zero_row_bound. bcf_lt_gap_bcb4we_exists_table_zero_row_bound + S (bcf_index_bcb4we_exists_table_zero_row) = S (n + n)) -> exists bcf_value_bcb4we_exists_table_zero_row. ((((exists bcf_height_bcb4we_exists_table_zero_row_entry. bcf_height_bcb4we_exists_table_zero_row_entry + S (bcf_value_bcb4we_exists_table_zero_row) = S ((S (bcf_index_bcb4we_exists_table_zero_row)) * bcf_row_scale_bcb4we_exists_table)) /\ exists bcf_quotient_bcb4we_exists_table_zero_row_entry. bcf_row_code_bcb4we_exists_table = bcf_quotient_bcb4we_exists_table_zero_row_entry * S ((S (bcf_index_bcb4we_exists_table_zero_row)) * bcf_row_scale_bcb4we_exists_table) + (bcf_value_bcb4we_exists_table_zero_row))) /\ ((bcf_index_bcb4we_exists_table_zero_row = 0 /\ bcf_value_bcb4we_exists_table_zero_row = 1) \/ exists bcf_predecessor_bcb4we_exists_table_zero_row. bcf_index_bcb4we_exists_table_zero_row = S bcf_predecessor_bcb4we_exists_table_zero_row /\ bcf_value_bcb4we_exists_table_zero_row = 0)))) \/ exists bcf_predecessor_bcb4we_exists_table bcf_previous_code_bcb4we_exists_table bcf_previous_scale_bcb4we_exists_table. bcf_row_index_bcb4we_exists_table = S bcf_predecessor_bcb4we_exists_table /\ ((((exists bcf_height_bcb4we_exists_table_decoded_previous_code. bcf_height_bcb4we_exists_table_decoded_previous_code + S (bcf_previous_code_bcb4we_exists_table) = S ((S (bcf_predecessor_bcb4we_exists_table)) * bcf_row_code_scale_bcb4we_exists)) /\ exists bcf_quotient_bcb4we_exists_table_decoded_previous_code. bcf_row_code_code_bcb4we_exists = bcf_quotient_bcb4we_exists_table_decoded_previous_code * S ((S (bcf_predecessor_bcb4we_exists_table)) * bcf_row_code_scale_bcb4we_exists) + (bcf_previous_code_bcb4we_exists_table))) /\ ((((exists bcf_height_bcb4we_exists_table_decoded_previous_scale. bcf_height_bcb4we_exists_table_decoded_previous_scale + S (bcf_previous_scale_bcb4we_exists_table) = S ((S (bcf_predecessor_bcb4we_exists_table)) * bcf_row_scale_scale_bcb4we_exists)) /\ exists bcf_quotient_bcb4we_exists_table_decoded_previous_scale. bcf_row_scale_code_bcb4we_exists = bcf_quotient_bcb4we_exists_table_decoded_previous_scale * S ((S (bcf_predecessor_bcb4we_exists_table)) * bcf_row_scale_scale_bcb4we_exists) + (bcf_previous_scale_bcb4we_exists_table))) /\ (forall bcf_index_bcb4we_exists_table_row_step. (exists bcf_lt_gap_bcb4we_exists_table_row_step_bound. bcf_lt_gap_bcb4we_exists_table_row_step_bound + S (bcf_index_bcb4we_exists_table_row_step) = S (n + n)) -> exists bcf_value_bcb4we_exists_table_row_step. ((((exists bcf_height_bcb4we_exists_table_row_step_entry. bcf_height_bcb4we_exists_table_row_step_entry + S (bcf_value_bcb4we_exists_table_row_step) = S ((S (bcf_index_bcb4we_exists_table_row_step)) * bcf_row_scale_bcb4we_exists_table)) /\ exists bcf_quotient_bcb4we_exists_table_row_step_entry. bcf_row_code_bcb4we_exists_table = bcf_quotient_bcb4we_exists_table_row_step_entry * S ((S (bcf_index_bcb4we_exists_table_row_step)) * bcf_row_scale_bcb4we_exists_table) + (bcf_value_bcb4we_exists_table_row_step))) /\ ((bcf_index_bcb4we_exists_table_row_step = 0 /\ bcf_value_bcb4we_exists_table_row_step = 1) \/ exists bcf_predecessor_bcb4we_exists_table_row_step bcf_left_bcb4we_exists_table_row_step bcf_right_bcb4we_exists_table_row_step. bcf_index_bcb4we_exists_table_row_step = S bcf_predecessor_bcb4we_exists_table_row_step /\ ((((exists bcf_height_bcb4we_exists_table_row_step_previous_left. bcf_height_bcb4we_exists_table_row_step_previous_left + S (bcf_left_bcb4we_exists_table_row_step) = S ((S (bcf_predecessor_bcb4we_exists_table_row_step)) * bcf_previous_scale_bcb4we_exists_table)) /\ exists bcf_quotient_bcb4we_exists_table_row_step_previous_left. bcf_previous_code_bcb4we_exists_table = bcf_quotient_bcb4we_exists_table_row_step_previous_left * S ((S (bcf_predecessor_bcb4we_exists_table_row_step)) * bcf_previous_scale_bcb4we_exists_table) + (bcf_left_bcb4we_exists_table_row_step))) /\ ((((exists bcf_height_bcb4we_exists_table_row_step_previous_right. bcf_height_bcb4we_exists_table_row_step_previous_right + S (bcf_right_bcb4we_exists_table_row_step) = S ((S (S (bcf_predecessor_bcb4we_exists_table_row_step))) * bcf_previous_scale_bcb4we_exists_table)) /\ exists bcf_quotient_bcb4we_exists_table_row_step_previous_right. bcf_previous_code_bcb4we_exists_table = bcf_quotient_bcb4we_exists_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcb4we_exists_table_row_step))) * bcf_previous_scale_bcb4we_exists_table) + (bcf_right_bcb4we_exists_table_row_step))) /\ bcf_value_bcb4we_exists_table_row_step = bcf_left_bcb4we_exists_table_row_step + bcf_right_bcb4we_exists_table_row_step))))))))))) /\ ((((exists bcf_height_bcb4we_exists_decoded_row_code. bcf_height_bcb4we_exists_decoded_row_code + S (bcf_row_code_bcb4we_exists) = S ((S (n + n)) * bcf_row_code_scale_bcb4we_exists)) /\ exists bcf_quotient_bcb4we_exists_decoded_row_code. bcf_row_code_code_bcb4we_exists = bcf_quotient_bcb4we_exists_decoded_row_code * S ((S (n + n)) * bcf_row_code_scale_bcb4we_exists) + (bcf_row_code_bcb4we_exists))) /\ ((((exists bcf_height_bcb4we_exists_decoded_row_scale. bcf_height_bcb4we_exists_decoded_row_scale + S (bcf_row_scale_bcb4we_exists) = S ((S (n + n)) * bcf_row_scale_scale_bcb4we_exists)) /\ exists bcf_quotient_bcb4we_exists_decoded_row_scale. bcf_row_scale_code_bcb4we_exists = bcf_quotient_bcb4we_exists_decoded_row_scale * S ((S (n + n)) * bcf_row_scale_scale_bcb4we_exists) + (bcf_row_scale_bcb4we_exists))) /\ (((exists bcf_height_bcb4we_exists_decoded_value. bcf_height_bcb4we_exists_decoded_value + S (z) = S ((S (n)) * bcf_row_scale_bcb4we_exists)) /\ exists bcf_quotient_bcb4we_exists_decoded_value. bcf_row_code_bcb4we_exists = bcf_quotient_bcb4we_exists_decoded_value * S ((S (n)) * bcf_row_scale_bcb4we_exists) + (z)))))))))) /\ (forall p c. (exists pa_b_bfplcb4_power pa_c_bfplcb4_power. ((forall pa_i_bfplcb4_power_repeat. (exists pa_lt_bfplcb4_power_repeat_bound. pa_lt_bfplcb4_power_repeat_bound + S pa_i_bfplcb4_power_repeat = 4) -> (((exists pa_h_bfplcb4_power_repeat_decoded. pa_h_bfplcb4_power_repeat_decoded + S (4) = S ((S (pa_i_bfplcb4_power_repeat)) * pa_c_bfplcb4_power)) /\ exists pa_q_bfplcb4_power_repeat_decoded. pa_b_bfplcb4_power = pa_q_bfplcb4_power_repeat_decoded * S ((S (pa_i_bfplcb4_power_repeat)) * pa_c_bfplcb4_power) + (4)))) /\ (exists pa_u_bfplcb4_power_product pa_v_bfplcb4_power_product. ((((exists pa_h_bfplcb4_power_product_start. pa_h_bfplcb4_power_product_start + S (1) = S ((S (0)) * pa_v_bfplcb4_power_product)) /\ exists pa_q_bfplcb4_power_product_start. pa_u_bfplcb4_power_product = pa_q_bfplcb4_power_product_start * S ((S (0)) * pa_v_bfplcb4_power_product) + (1))) /\ ((((exists pa_h_bfplcb4_power_product_terminal. pa_h_bfplcb4_power_product_terminal + S (p) = S ((S (4)) * pa_v_bfplcb4_power_product)) /\ exists pa_q_bfplcb4_power_product_terminal. pa_u_bfplcb4_power_product = pa_q_bfplcb4_power_product_terminal * S ((S (4)) * pa_v_bfplcb4_power_product) + (p))) /\ forall pa_i_bfplcb4_power_product. (exists pa_lt_bfplcb4_power_product_bound. pa_lt_bfplcb4_power_product_bound + S pa_i_bfplcb4_power_product = 4) -> exists pa_p_bfplcb4_power_product pa_r_bfplcb4_power_product pa_s_bfplcb4_power_product. ((((exists pa_h_bfplcb4_power_product_factor. pa_h_bfplcb4_power_product_factor + S (pa_p_bfplcb4_power_product) = S ((S (pa_i_bfplcb4_power_product)) * pa_c_bfplcb4_power)) /\ exists pa_q_bfplcb4_power_product_factor. pa_b_bfplcb4_power = pa_q_bfplcb4_power_product_factor * S ((S (pa_i_bfplcb4_power_product)) * pa_c_bfplcb4_power) + (pa_p_bfplcb4_power_product))) /\ ((((exists pa_h_bfplcb4_power_product_partial. pa_h_bfplcb4_power_product_partial + S (pa_r_bfplcb4_power_product) = S ((S (pa_i_bfplcb4_power_product)) * pa_v_bfplcb4_power_product)) /\ exists pa_q_bfplcb4_power_product_partial. pa_u_bfplcb4_power_product = pa_q_bfplcb4_power_product_partial * S ((S (pa_i_bfplcb4_power_product)) * pa_v_bfplcb4_power_product) + (pa_r_bfplcb4_power_product))) /\ ((((exists pa_h_bfplcb4_power_product_successor. pa_h_bfplcb4_power_product_successor + S (pa_s_bfplcb4_power_product) = S ((S (S pa_i_bfplcb4_power_product)) * pa_v_bfplcb4_power_product)) /\ exists pa_q_bfplcb4_power_product_successor. pa_u_bfplcb4_power_product = pa_q_bfplcb4_power_product_successor * S ((S (S pa_i_bfplcb4_power_product)) * pa_v_bfplcb4_power_product) + (pa_s_bfplcb4_power_product))) /\ pa_s_bfplcb4_power_product = pa_r_bfplcb4_power_product * pa_p_bfplcb4_power_product)))))))) -> (((exists bcf_lt_gap_bfplcb4_central_out_of_range. bcf_lt_gap_bfplcb4_central_out_of_range + S (4 + 4) = 4) /\ c = 0) \/ ((exists bcf_le_gap_bfplcb4_central_in_range. bcf_le_gap_bfplcb4_central_in_range + (4) = 4 + 4) /\ (exists bcf_row_code_code_bfplcb4_central bcf_row_code_scale_bfplcb4_central bcf_row_scale_code_bfplcb4_central bcf_row_scale_scale_bfplcb4_central bcf_row_code_bfplcb4_central bcf_row_scale_bfplcb4_central. ((forall bcf_row_index_bfplcb4_central_table. (exists bcf_lt_gap_bfplcb4_central_table_row_bound. bcf_lt_gap_bfplcb4_central_table_row_bound + S (bcf_row_index_bfplcb4_central_table) = S (4 + 4)) -> exists bcf_row_code_bfplcb4_central_table bcf_row_scale_bfplcb4_central_table. ((((exists bcf_height_bfplcb4_central_table_decoded_row_code. bcf_height_bfplcb4_central_table_decoded_row_code + S (bcf_row_code_bfplcb4_central_table) = S ((S (bcf_row_index_bfplcb4_central_table)) * bcf_row_code_scale_bfplcb4_central)) /\ exists bcf_quotient_bfplcb4_central_table_decoded_row_code. bcf_row_code_code_bfplcb4_central = bcf_quotient_bfplcb4_central_table_decoded_row_code * S ((S (bcf_row_index_bfplcb4_central_table)) * bcf_row_code_scale_bfplcb4_central) + (bcf_row_code_bfplcb4_central_table))) /\ ((((exists bcf_height_bfplcb4_central_table_decoded_row_scale. bcf_height_bfplcb4_central_table_decoded_row_scale + S (bcf_row_scale_bfplcb4_central_table) = S ((S (bcf_row_index_bfplcb4_central_table)) * bcf_row_scale_scale_bfplcb4_central)) /\ exists bcf_quotient_bfplcb4_central_table_decoded_row_scale. bcf_row_scale_code_bfplcb4_central = bcf_quotient_bfplcb4_central_table_decoded_row_scale * S ((S (bcf_row_index_bfplcb4_central_table)) * bcf_row_scale_scale_bfplcb4_central) + (bcf_row_scale_bfplcb4_central_table))) /\ ((bcf_row_index_bfplcb4_central_table = 0 /\ (forall bcf_index_bfplcb4_central_table_zero_row. (exists bcf_lt_gap_bfplcb4_central_table_zero_row_bound. bcf_lt_gap_bfplcb4_central_table_zero_row_bound + S (bcf_index_bfplcb4_central_table_zero_row) = S (4 + 4)) -> exists bcf_value_bfplcb4_central_table_zero_row. ((((exists bcf_height_bfplcb4_central_table_zero_row_entry. bcf_height_bfplcb4_central_table_zero_row_entry + S (bcf_value_bfplcb4_central_table_zero_row) = S ((S (bcf_index_bfplcb4_central_table_zero_row)) * bcf_row_scale_bfplcb4_central_table)) /\ exists bcf_quotient_bfplcb4_central_table_zero_row_entry. bcf_row_code_bfplcb4_central_table = bcf_quotient_bfplcb4_central_table_zero_row_entry * S ((S (bcf_index_bfplcb4_central_table_zero_row)) * bcf_row_scale_bfplcb4_central_table) + (bcf_value_bfplcb4_central_table_zero_row))) /\ ((bcf_index_bfplcb4_central_table_zero_row = 0 /\ bcf_value_bfplcb4_central_table_zero_row = 1) \/ exists bcf_predecessor_bfplcb4_central_table_zero_row. bcf_index_bfplcb4_central_table_zero_row = S bcf_predecessor_bfplcb4_central_table_zero_row /\ bcf_value_bfplcb4_central_table_zero_row = 0)))) \/ exists bcf_predecessor_bfplcb4_central_table bcf_previous_code_bfplcb4_central_table bcf_previous_scale_bfplcb4_central_table. bcf_row_index_bfplcb4_central_table = S bcf_predecessor_bfplcb4_central_table /\ ((((exists bcf_height_bfplcb4_central_table_decoded_previous_code. bcf_height_bfplcb4_central_table_decoded_previous_code + S (bcf_previous_code_bfplcb4_central_table) = S ((S (bcf_predecessor_bfplcb4_central_table)) * bcf_row_code_scale_bfplcb4_central)) /\ exists bcf_quotient_bfplcb4_central_table_decoded_previous_code. bcf_row_code_code_bfplcb4_central = bcf_quotient_bfplcb4_central_table_decoded_previous_code * S ((S (bcf_predecessor_bfplcb4_central_table)) * bcf_row_code_scale_bfplcb4_central) + (bcf_previous_code_bfplcb4_central_table))) /\ ((((exists bcf_height_bfplcb4_central_table_decoded_previous_scale. bcf_height_bfplcb4_central_table_decoded_previous_scale + S (bcf_previous_scale_bfplcb4_central_table) = S ((S (bcf_predecessor_bfplcb4_central_table)) * bcf_row_scale_scale_bfplcb4_central)) /\ exists bcf_quotient_bfplcb4_central_table_decoded_previous_scale. bcf_row_scale_code_bfplcb4_central = bcf_quotient_bfplcb4_central_table_decoded_previous_scale * S ((S (bcf_predecessor_bfplcb4_central_table)) * bcf_row_scale_scale_bfplcb4_central) + (bcf_previous_scale_bfplcb4_central_table))) /\ (forall bcf_index_bfplcb4_central_table_row_step. (exists bcf_lt_gap_bfplcb4_central_table_row_step_bound. bcf_lt_gap_bfplcb4_central_table_row_step_bound + S (bcf_index_bfplcb4_central_table_row_step) = S (4 + 4)) -> exists bcf_value_bfplcb4_central_table_row_step. ((((exists bcf_height_bfplcb4_central_table_row_step_entry. bcf_height_bfplcb4_central_table_row_step_entry + S (bcf_value_bfplcb4_central_table_row_step) = S ((S (bcf_index_bfplcb4_central_table_row_step)) * bcf_row_scale_bfplcb4_central_table)) /\ exists bcf_quotient_bfplcb4_central_table_row_step_entry. bcf_row_code_bfplcb4_central_table = bcf_quotient_bfplcb4_central_table_row_step_entry * S ((S (bcf_index_bfplcb4_central_table_row_step)) * bcf_row_scale_bfplcb4_central_table) + (bcf_value_bfplcb4_central_table_row_step))) /\ ((bcf_index_bfplcb4_central_table_row_step = 0 /\ bcf_value_bfplcb4_central_table_row_step = 1) \/ exists bcf_predecessor_bfplcb4_central_table_row_step bcf_left_bfplcb4_central_table_row_step bcf_right_bfplcb4_central_table_row_step. bcf_index_bfplcb4_central_table_row_step = S bcf_predecessor_bfplcb4_central_table_row_step /\ ((((exists bcf_height_bfplcb4_central_table_row_step_previous_left. bcf_height_bfplcb4_central_table_row_step_previous_left + S (bcf_left_bfplcb4_central_table_row_step) = S ((S (bcf_predecessor_bfplcb4_central_table_row_step)) * bcf_previous_scale_bfplcb4_central_table)) /\ exists bcf_quotient_bfplcb4_central_table_row_step_previous_left. bcf_previous_code_bfplcb4_central_table = bcf_quotient_bfplcb4_central_table_row_step_previous_left * S ((S (bcf_predecessor_bfplcb4_central_table_row_step)) * bcf_previous_scale_bfplcb4_central_table) + (bcf_left_bfplcb4_central_table_row_step))) /\ ((((exists bcf_height_bfplcb4_central_table_row_step_previous_right. bcf_height_bfplcb4_central_table_row_step_previous_right + S (bcf_right_bfplcb4_central_table_row_step) = S ((S (S (bcf_predecessor_bfplcb4_central_table_row_step))) * bcf_previous_scale_bfplcb4_central_table)) /\ exists bcf_quotient_bfplcb4_central_table_row_step_previous_right. bcf_previous_code_bfplcb4_central_table = bcf_quotient_bfplcb4_central_table_row_step_previous_right * S ((S (S (bcf_predecessor_bfplcb4_central_table_row_step))) * bcf_previous_scale_bfplcb4_central_table) + (bcf_right_bfplcb4_central_table_row_step))) /\ bcf_value_bfplcb4_central_table_row_step = bcf_left_bfplcb4_central_table_row_step + bcf_right_bfplcb4_central_table_row_step))))))))))) /\ ((((exists bcf_height_bfplcb4_central_decoded_row_code. bcf_height_bfplcb4_central_decoded_row_code + S (bcf_row_code_bfplcb4_central) = S ((S (4 + 4)) * bcf_row_code_scale_bfplcb4_central)) /\ exists bcf_quotient_bfplcb4_central_decoded_row_code. bcf_row_code_code_bfplcb4_central = bcf_quotient_bfplcb4_central_decoded_row_code * S ((S (4 + 4)) * bcf_row_code_scale_bfplcb4_central) + (bcf_row_code_bfplcb4_central))) /\ ((((exists bcf_height_bfplcb4_central_decoded_row_scale. bcf_height_bfplcb4_central_decoded_row_scale + S (bcf_row_scale_bfplcb4_central) = S ((S (4 + 4)) * bcf_row_scale_scale_bfplcb4_central)) /\ exists bcf_quotient_bfplcb4_central_decoded_row_scale. bcf_row_scale_code_bfplcb4_central = bcf_quotient_bfplcb4_central_decoded_row_scale * S ((S (4 + 4)) * bcf_row_scale_scale_bfplcb4_central) + (bcf_row_scale_bfplcb4_central))) /\ (((exists bcf_height_bfplcb4_central_decoded_value. bcf_height_bfplcb4_central_decoded_value + S (c) = S ((S (4)) * bcf_row_scale_bfplcb4_central)) /\ exists bcf_quotient_bfplcb4_central_decoded_value. bcf_row_code_bfplcb4_central = bcf_quotient_bfplcb4_central_decoded_value * S ((S (4)) * bcf_row_scale_bfplcb4_central) + (c))))))))) -> (exists bcf_lt_gap_bfplcb4_result. bcf_lt_gap_bfplcb4_result + S (p) = 4 * c))
  14. 0014apply four_pow_central_seed_package
  15. 0015exact central_binom_succ_recurrence
  16. 0016cases hpackage
  17. 0017induction n
  18. 0018intro p
  19. 0019intro c
  20. 0020intro hbound
  21. 0021intro hpower
  22. 0022intro hcentral
  23. 0023exfalso
  24. 0024specialize lt_not_le 0
  25. 0025specialize lt_not_le 4
  26. 0026apply lt_not_le
  27. 0027exact hzero_lt_four
  28. 0028exact hbound
  29. 0029induction n
  30. 0030intro p
  31. 0031intro c
  32. 0032intro hbound
  33. 0033intro hpower
  34. 0034intro hcentral
  35. 0035exfalso
  36. 0036specialize lt_not_le 1
  37. 0037specialize lt_not_le 4
  38. 0038apply lt_not_le
  39. 0039exact hone_lt_four
  40. 0040exact hbound
  41. 0041induction n
  42. 0042intro p
  43. 0043intro c
  44. 0044intro hbound
  45. 0045intro hpower
  46. 0046intro hcentral
  47. 0047exfalso
  48. 0048specialize lt_not_le 2
  49. 0049specialize lt_not_le 4
  50. 0050apply lt_not_le
  51. 0051exact htwo_lt_four
  52. 0052exact hbound
  53. 0053induction n
  54. 0054intro p
  55. 0055intro c
  56. 0056intro hbound
  57. 0057intro hpower
  58. 0058intro hcentral
  59. 0059exfalso
  60. 0060specialize lt_not_le 3
  61. 0061specialize lt_not_le 4
  62. 0062apply lt_not_le
  63. 0063exact hthree_lt_four
  64. 0064exact hbound
  65. 0065induction n
  66. 0066intro p
  67. 0067intro c
  68. 0068intro hbound
  69. 0069intro hpower
  70. 0070intro hcentral
  71. 0071apply hpackage_right
  72. 0072exact hpower
  73. 0073exact hcentral
  74. 0074intro p
  75. 0075intro c
  76. 0076intro hbound
  77. 0077intro hpower
  78. 0078intro hcentral
  79. 0079have hpower_step : ∃ r. Pow(4,S S S S n,r) ∧ p = r · 4
    Exact native replay linehave hpower_step : exists r. (exists pa_b_bfplcb_predecessor_power pa_c_bfplcb_predecessor_power. ((forall pa_i_bfplcb_predecessor_power_repeat. (exists pa_lt_bfplcb_predecessor_power_repeat_bound. pa_lt_bfplcb_predecessor_power_repeat_bound + S pa_i_bfplcb_predecessor_power_repeat = S (S (S (S n)))) -> (((exists pa_h_bfplcb_predecessor_power_repeat_decoded. pa_h_bfplcb_predecessor_power_repeat_decoded + S (4) = S ((S (pa_i_bfplcb_predecessor_power_repeat)) * pa_c_bfplcb_predecessor_power)) /\ exists pa_q_bfplcb_predecessor_power_repeat_decoded. pa_b_bfplcb_predecessor_power = pa_q_bfplcb_predecessor_power_repeat_decoded * S ((S (pa_i_bfplcb_predecessor_power_repeat)) * pa_c_bfplcb_predecessor_power) + (4)))) /\ (exists pa_u_bfplcb_predecessor_power_product pa_v_bfplcb_predecessor_power_product. ((((exists pa_h_bfplcb_predecessor_power_product_start. pa_h_bfplcb_predecessor_power_product_start + S (1) = S ((S (0)) * pa_v_bfplcb_predecessor_power_product)) /\ exists pa_q_bfplcb_predecessor_power_product_start. pa_u_bfplcb_predecessor_power_product = pa_q_bfplcb_predecessor_power_product_start * S ((S (0)) * pa_v_bfplcb_predecessor_power_product) + (1))) /\ ((((exists pa_h_bfplcb_predecessor_power_product_terminal. pa_h_bfplcb_predecessor_power_product_terminal + S (r) = S ((S (S (S (S (S n))))) * pa_v_bfplcb_predecessor_power_product)) /\ exists pa_q_bfplcb_predecessor_power_product_terminal. pa_u_bfplcb_predecessor_power_product = pa_q_bfplcb_predecessor_power_product_terminal * S ((S (S (S (S (S n))))) * pa_v_bfplcb_predecessor_power_product) + (r))) /\ forall pa_i_bfplcb_predecessor_power_product. (exists pa_lt_bfplcb_predecessor_power_product_bound. pa_lt_bfplcb_predecessor_power_product_bound + S pa_i_bfplcb_predecessor_power_product = S (S (S (S n)))) -> exists pa_p_bfplcb_predecessor_power_product pa_r_bfplcb_predecessor_power_product pa_s_bfplcb_predecessor_power_product. ((((exists pa_h_bfplcb_predecessor_power_product_factor. pa_h_bfplcb_predecessor_power_product_factor + S (pa_p_bfplcb_predecessor_power_product) = S ((S (pa_i_bfplcb_predecessor_power_product)) * pa_c_bfplcb_predecessor_power)) /\ exists pa_q_bfplcb_predecessor_power_product_factor. pa_b_bfplcb_predecessor_power = pa_q_bfplcb_predecessor_power_product_factor * S ((S (pa_i_bfplcb_predecessor_power_product)) * pa_c_bfplcb_predecessor_power) + (pa_p_bfplcb_predecessor_power_product))) /\ ((((exists pa_h_bfplcb_predecessor_power_product_partial. pa_h_bfplcb_predecessor_power_product_partial + S (pa_r_bfplcb_predecessor_power_product) = S ((S (pa_i_bfplcb_predecessor_power_product)) * pa_v_bfplcb_predecessor_power_product)) /\ exists pa_q_bfplcb_predecessor_power_product_partial. pa_u_bfplcb_predecessor_power_product = pa_q_bfplcb_predecessor_power_product_partial * S ((S (pa_i_bfplcb_predecessor_power_product)) * pa_v_bfplcb_predecessor_power_product) + (pa_r_bfplcb_predecessor_power_product))) /\ ((((exists pa_h_bfplcb_predecessor_power_product_successor. pa_h_bfplcb_predecessor_power_product_successor + S (pa_s_bfplcb_predecessor_power_product) = S ((S (S pa_i_bfplcb_predecessor_power_product)) * pa_v_bfplcb_predecessor_power_product)) /\ exists pa_q_bfplcb_predecessor_power_product_successor. pa_u_bfplcb_predecessor_power_product = pa_q_bfplcb_predecessor_power_product_successor * S ((S (S pa_i_bfplcb_predecessor_power_product)) * pa_v_bfplcb_predecessor_power_product) + (pa_s_bfplcb_predecessor_power_product))) /\ pa_s_bfplcb_predecessor_power_product = pa_r_bfplcb_predecessor_power_product * pa_p_bfplcb_predecessor_power_product)))))))) /\ p = r * 4
  80. 0080apply pow_successor_decompose
  81. 0081refl
  82. 0082exact hpower
  83. 0083cases hpower_step
  84. 0084cases hpower_step_witness
  85. 0085have hpredecessor_exists : ∃ a. CentralBinom(S S S S n,a)
    Exact native replay linehave hpredecessor_exists : exists a. (((exists bcf_lt_gap_bfplcb_predecessor_central_out_of_range. bcf_lt_gap_bfplcb_predecessor_central_out_of_range + S (S S S S n + S S S S n) = S S S S n) /\ a = 0) \/ ((exists bcf_le_gap_bfplcb_predecessor_central_in_range. bcf_le_gap_bfplcb_predecessor_central_in_range + (S S S S n) = S S S S n + S S S S n) /\ (exists bcf_row_code_code_bfplcb_predecessor_central bcf_row_code_scale_bfplcb_predecessor_central bcf_row_scale_code_bfplcb_predecessor_central bcf_row_scale_scale_bfplcb_predecessor_central bcf_row_code_bfplcb_predecessor_central bcf_row_scale_bfplcb_predecessor_central. ((forall bcf_row_index_bfplcb_predecessor_central_table. (exists bcf_lt_gap_bfplcb_predecessor_central_table_row_bound. bcf_lt_gap_bfplcb_predecessor_central_table_row_bound + S (bcf_row_index_bfplcb_predecessor_central_table) = S (S S S S n + S S S S n)) -> exists bcf_row_code_bfplcb_predecessor_central_table bcf_row_scale_bfplcb_predecessor_central_table. ((((exists bcf_height_bfplcb_predecessor_central_table_decoded_row_code. bcf_height_bfplcb_predecessor_central_table_decoded_row_code + S (bcf_row_code_bfplcb_predecessor_central_table) = S ((S (bcf_row_index_bfplcb_predecessor_central_table)) * bcf_row_code_scale_bfplcb_predecessor_central)) /\ exists bcf_quotient_bfplcb_predecessor_central_table_decoded_row_code. bcf_row_code_code_bfplcb_predecessor_central = bcf_quotient_bfplcb_predecessor_central_table_decoded_row_code * S ((S (bcf_row_index_bfplcb_predecessor_central_table)) * bcf_row_code_scale_bfplcb_predecessor_central) + (bcf_row_code_bfplcb_predecessor_central_table))) /\ ((((exists bcf_height_bfplcb_predecessor_central_table_decoded_row_scale. bcf_height_bfplcb_predecessor_central_table_decoded_row_scale + S (bcf_row_scale_bfplcb_predecessor_central_table) = S ((S (bcf_row_index_bfplcb_predecessor_central_table)) * bcf_row_scale_scale_bfplcb_predecessor_central)) /\ exists bcf_quotient_bfplcb_predecessor_central_table_decoded_row_scale. bcf_row_scale_code_bfplcb_predecessor_central = bcf_quotient_bfplcb_predecessor_central_table_decoded_row_scale * S ((S (bcf_row_index_bfplcb_predecessor_central_table)) * bcf_row_scale_scale_bfplcb_predecessor_central) + (bcf_row_scale_bfplcb_predecessor_central_table))) /\ ((bcf_row_index_bfplcb_predecessor_central_table = 0 /\ (forall bcf_index_bfplcb_predecessor_central_table_zero_row. (exists bcf_lt_gap_bfplcb_predecessor_central_table_zero_row_bound. bcf_lt_gap_bfplcb_predecessor_central_table_zero_row_bound + S (bcf_index_bfplcb_predecessor_central_table_zero_row) = S (S S S S n + S S S S n)) -> exists bcf_value_bfplcb_predecessor_central_table_zero_row. ((((exists bcf_height_bfplcb_predecessor_central_table_zero_row_entry. bcf_height_bfplcb_predecessor_central_table_zero_row_entry + S (bcf_value_bfplcb_predecessor_central_table_zero_row) = S ((S (bcf_index_bfplcb_predecessor_central_table_zero_row)) * bcf_row_scale_bfplcb_predecessor_central_table)) /\ exists bcf_quotient_bfplcb_predecessor_central_table_zero_row_entry. bcf_row_code_bfplcb_predecessor_central_table = bcf_quotient_bfplcb_predecessor_central_table_zero_row_entry * S ((S (bcf_index_bfplcb_predecessor_central_table_zero_row)) * bcf_row_scale_bfplcb_predecessor_central_table) + (bcf_value_bfplcb_predecessor_central_table_zero_row))) /\ ((bcf_index_bfplcb_predecessor_central_table_zero_row = 0 /\ bcf_value_bfplcb_predecessor_central_table_zero_row = 1) \/ exists bcf_predecessor_bfplcb_predecessor_central_table_zero_row. bcf_index_bfplcb_predecessor_central_table_zero_row = S bcf_predecessor_bfplcb_predecessor_central_table_zero_row /\ bcf_value_bfplcb_predecessor_central_table_zero_row = 0)))) \/ exists bcf_predecessor_bfplcb_predecessor_central_table bcf_previous_code_bfplcb_predecessor_central_table bcf_previous_scale_bfplcb_predecessor_central_table. bcf_row_index_bfplcb_predecessor_central_table = S bcf_predecessor_bfplcb_predecessor_central_table /\ ((((exists bcf_height_bfplcb_predecessor_central_table_decoded_previous_code. bcf_height_bfplcb_predecessor_central_table_decoded_previous_code + S (bcf_previous_code_bfplcb_predecessor_central_table) = S ((S (bcf_predecessor_bfplcb_predecessor_central_table)) * bcf_row_code_scale_bfplcb_predecessor_central)) /\ exists bcf_quotient_bfplcb_predecessor_central_table_decoded_previous_code. bcf_row_code_code_bfplcb_predecessor_central = bcf_quotient_bfplcb_predecessor_central_table_decoded_previous_code * S ((S (bcf_predecessor_bfplcb_predecessor_central_table)) * bcf_row_code_scale_bfplcb_predecessor_central) + (bcf_previous_code_bfplcb_predecessor_central_table))) /\ ((((exists bcf_height_bfplcb_predecessor_central_table_decoded_previous_scale. bcf_height_bfplcb_predecessor_central_table_decoded_previous_scale + S (bcf_previous_scale_bfplcb_predecessor_central_table) = S ((S (bcf_predecessor_bfplcb_predecessor_central_table)) * bcf_row_scale_scale_bfplcb_predecessor_central)) /\ exists bcf_quotient_bfplcb_predecessor_central_table_decoded_previous_scale. bcf_row_scale_code_bfplcb_predecessor_central = bcf_quotient_bfplcb_predecessor_central_table_decoded_previous_scale * S ((S (bcf_predecessor_bfplcb_predecessor_central_table)) * bcf_row_scale_scale_bfplcb_predecessor_central) + (bcf_previous_scale_bfplcb_predecessor_central_table))) /\ (forall bcf_index_bfplcb_predecessor_central_table_row_step. (exists bcf_lt_gap_bfplcb_predecessor_central_table_row_step_bound. bcf_lt_gap_bfplcb_predecessor_central_table_row_step_bound + S (bcf_index_bfplcb_predecessor_central_table_row_step) = S (S S S S n + S S S S n)) -> exists bcf_value_bfplcb_predecessor_central_table_row_step. ((((exists bcf_height_bfplcb_predecessor_central_table_row_step_entry. bcf_height_bfplcb_predecessor_central_table_row_step_entry + S (bcf_value_bfplcb_predecessor_central_table_row_step) = S ((S (bcf_index_bfplcb_predecessor_central_table_row_step)) * bcf_row_scale_bfplcb_predecessor_central_table)) /\ exists bcf_quotient_bfplcb_predecessor_central_table_row_step_entry. bcf_row_code_bfplcb_predecessor_central_table = bcf_quotient_bfplcb_predecessor_central_table_row_step_entry * S ((S (bcf_index_bfplcb_predecessor_central_table_row_step)) * bcf_row_scale_bfplcb_predecessor_central_table) + (bcf_value_bfplcb_predecessor_central_table_row_step))) /\ ((bcf_index_bfplcb_predecessor_central_table_row_step = 0 /\ bcf_value_bfplcb_predecessor_central_table_row_step = 1) \/ exists bcf_predecessor_bfplcb_predecessor_central_table_row_step bcf_left_bfplcb_predecessor_central_table_row_step bcf_right_bfplcb_predecessor_central_table_row_step. bcf_index_bfplcb_predecessor_central_table_row_step = S bcf_predecessor_bfplcb_predecessor_central_table_row_step /\ ((((exists bcf_height_bfplcb_predecessor_central_table_row_step_previous_left. bcf_height_bfplcb_predecessor_central_table_row_step_previous_left + S (bcf_left_bfplcb_predecessor_central_table_row_step) = S ((S (bcf_predecessor_bfplcb_predecessor_central_table_row_step)) * bcf_previous_scale_bfplcb_predecessor_central_table)) /\ exists bcf_quotient_bfplcb_predecessor_central_table_row_step_previous_left. bcf_previous_code_bfplcb_predecessor_central_table = bcf_quotient_bfplcb_predecessor_central_table_row_step_previous_left * S ((S (bcf_predecessor_bfplcb_predecessor_central_table_row_step)) * bcf_previous_scale_bfplcb_predecessor_central_table) + (bcf_left_bfplcb_predecessor_central_table_row_step))) /\ ((((exists bcf_height_bfplcb_predecessor_central_table_row_step_previous_right. bcf_height_bfplcb_predecessor_central_table_row_step_previous_right + S (bcf_right_bfplcb_predecessor_central_table_row_step) = S ((S (S (bcf_predecessor_bfplcb_predecessor_central_table_row_step))) * bcf_previous_scale_bfplcb_predecessor_central_table)) /\ exists bcf_quotient_bfplcb_predecessor_central_table_row_step_previous_right. bcf_previous_code_bfplcb_predecessor_central_table = bcf_quotient_bfplcb_predecessor_central_table_row_step_previous_right * S ((S (S (bcf_predecessor_bfplcb_predecessor_central_table_row_step))) * bcf_previous_scale_bfplcb_predecessor_central_table) + (bcf_right_bfplcb_predecessor_central_table_row_step))) /\ bcf_value_bfplcb_predecessor_central_table_row_step = bcf_left_bfplcb_predecessor_central_table_row_step + bcf_right_bfplcb_predecessor_central_table_row_step))))))))))) /\ ((((exists bcf_height_bfplcb_predecessor_central_decoded_row_code. bcf_height_bfplcb_predecessor_central_decoded_row_code + S (bcf_row_code_bfplcb_predecessor_central) = S ((S (S S S S n + S S S S n)) * bcf_row_code_scale_bfplcb_predecessor_central)) /\ exists bcf_quotient_bfplcb_predecessor_central_decoded_row_code. bcf_row_code_code_bfplcb_predecessor_central = bcf_quotient_bfplcb_predecessor_central_decoded_row_code * S ((S (S S S S n + S S S S n)) * bcf_row_code_scale_bfplcb_predecessor_central) + (bcf_row_code_bfplcb_predecessor_central))) /\ ((((exists bcf_height_bfplcb_predecessor_central_decoded_row_scale. bcf_height_bfplcb_predecessor_central_decoded_row_scale + S (bcf_row_scale_bfplcb_predecessor_central) = S ((S (S S S S n + S S S S n)) * bcf_row_scale_scale_bfplcb_predecessor_central)) /\ exists bcf_quotient_bfplcb_predecessor_central_decoded_row_scale. bcf_row_scale_code_bfplcb_predecessor_central = bcf_quotient_bfplcb_predecessor_central_decoded_row_scale * S ((S (S S S S n + S S S S n)) * bcf_row_scale_scale_bfplcb_predecessor_central) + (bcf_row_scale_bfplcb_predecessor_central))) /\ (((exists bcf_height_bfplcb_predecessor_central_decoded_value. bcf_height_bfplcb_predecessor_central_decoded_value + S (a) = S ((S (S S S S n)) * bcf_row_scale_bfplcb_predecessor_central)) /\ exists bcf_quotient_bfplcb_predecessor_central_decoded_value. bcf_row_code_bfplcb_predecessor_central = bcf_quotient_bfplcb_predecessor_central_decoded_value * S ((S (S S S S n)) * bcf_row_scale_bfplcb_predecessor_central) + (a)))))))))
  86. 0086apply hpackage_left
  87. 0087cases hpredecessor_exists
  88. 0088have hpredecessor_bound : Lt(3,S S S S n)
    Exact native replay linehave hpredecessor_bound : exists bcf_le_gap_bfplcb_predecessor_bound. bcf_le_gap_bfplcb_predecessor_bound + (4) = S (S (S (S n)))
  89. 0089exists n
  90. 0090simp
  91. 0091have hstrict : Lt(x,S S S S n · x1)
    Exact native replay linehave hstrict : exists bcf_lt_gap_bfplcb_predecessor_result. bcf_lt_gap_bfplcb_predecessor_result + S (x) = S (S (S (S n))) * x1
  92. 0092apply IH4
  93. 0093exact hpredecessor_bound
  94. 0094exact hpower_step_witness_left
  95. 0095exact hpredecessor_exists_witness
  96. 0096have hrecurrence : S (S (S (S (S n)))) * c = (2 * S (S (S (S (S n))) + S (S (S (S n))))) * x1
  97. 0097apply central_binom_succ_recurrence
  98. 0098exact hpredecessor_exists_witness
  99. 0099exact hcentral
  100. 0100have hstep : Lt(x · 4,S S S S S n · c)
    Exact native replay linehave hstep : exists bcf_lt_gap_bfplcb_successor_result. bcf_lt_gap_bfplcb_successor_result + S (x * 4) = S (S (S (S (S n)))) * c
  101. 0101apply four_power_central_recurrence_step
  102. 0102exact hstrict
  103. 0103exact hrecurrence
  104. 0104rewrite hpower_step_witness_right
  105. 0105exact hstep