BP0007

central_binom_prime_divisor_multiplicity_one_exists

For every n>1, a prime in (n,2n) divides C(2n,n) exactly once.

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

Exact theorem in conservative defined notation

∀ n. Lt(1,n) → ∃ x. ∃ y. Prime(x) ∧ (Lt(n,x) ∧ (Lt(x,n + n) ∧ ((Lt(n + n,n) ∧ y = 0 ∨ Le(n,n + n) ∧ (∃ z. ∃ m. ∃ k. ∃ i. ∃ j. ∃ u. (∀ v. Lt(v,S (n + n)) → ∃ w. ∃ x0. Beta(z,m,v,w) ∧ (Beta(k,i,v,x0) ∧ (v = 0 ∧ (∀ x1. Lt(x1,S (n + n)) → ∃ x2. Beta(w,x0,x1,x2) ∧ (x1 = 0 ∧ x2 = 1 ∨ (∃ x3. x1 = S x3 ∧ x2 = 0))) ∨ (∃ x1. ∃ x2. ∃ x3. v = S x1 ∧ (Beta(z,m,x1,x2) ∧ (Beta(k,i,x1,x3) ∧ (∀ x4. Lt(x4,S (n + n)) → ∃ x5. Beta(w,x0,x4,x5) ∧ (x4 = 0 ∧ x5 = 1 ∨ (∃ x6. ∃ x7. ∃ x8. x4 = S x6 ∧ (Beta(x2,x3,x6,x7) ∧ (Beta(x2,x3,S x6,x8) ∧ x5 = x7 + x8))))))))))) ∧ (Beta(z,m,n + n,j) ∧ (Beta(k,i,n + n,u) ∧ Beta(j,u,n,y))))) ∧ PowerValuationOne(x,y))))

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

Definition DAG

Beta(b,c,i,x) · 11PowerValuationOne(p,n) · 1Le(a,b) · 1Lt(a,b) · 7Prime(p) · 1

Actual proof prerequisites

bertrand_strict · checked external prerequisitecentral_binom_exists · checked external prerequisitebertrand_window_central_valuation_one
Original expanded first-order statement 
forall n. (exists bcf_lt_gap_bpc_index. bcf_lt_gap_bpc_index + S (1) = n) -> exists p C. (((~(p = 1) /\ forall frm_prime_left_bpc_prime frm_prime_right_bpc_prime. p = frm_prime_left_bpc_prime * frm_prime_right_bpc_prime -> frm_prime_left_bpc_prime = 1 \/ frm_prime_right_bpc_prime = 1)) /\ ((exists bcf_lt_gap_bpc_lower. bcf_lt_gap_bpc_lower + S (n) = p) /\ ((exists bcf_lt_gap_bpc_upper. bcf_lt_gap_bpc_upper + S (p) = n + n) /\ ((((exists bcf_lt_gap_bpc_central_out_of_range. bcf_lt_gap_bpc_central_out_of_range + S (n + n) = n) /\ C = 0) \/ ((exists bcf_le_gap_bpc_central_in_range. bcf_le_gap_bpc_central_in_range + (n) = n + n) /\ (exists bcf_row_code_code_bpc_central bcf_row_code_scale_bpc_central bcf_row_scale_code_bpc_central bcf_row_scale_scale_bpc_central bcf_row_code_bpc_central bcf_row_scale_bpc_central. ((forall bcf_row_index_bpc_central_table. (exists bcf_lt_gap_bpc_central_table_row_bound. bcf_lt_gap_bpc_central_table_row_bound + S (bcf_row_index_bpc_central_table) = S (n + n)) -> exists bcf_row_code_bpc_central_table bcf_row_scale_bpc_central_table. ((((exists bcf_height_bpc_central_table_decoded_row_code. bcf_height_bpc_central_table_decoded_row_code + S (bcf_row_code_bpc_central_table) = S ((S (bcf_row_index_bpc_central_table)) * bcf_row_code_scale_bpc_central)) /\ exists bcf_quotient_bpc_central_table_decoded_row_code. bcf_row_code_code_bpc_central = bcf_quotient_bpc_central_table_decoded_row_code * S ((S (bcf_row_index_bpc_central_table)) * bcf_row_code_scale_bpc_central) + (bcf_row_code_bpc_central_table))) /\ ((((exists bcf_height_bpc_central_table_decoded_row_scale. bcf_height_bpc_central_table_decoded_row_scale + S (bcf_row_scale_bpc_central_table) = S ((S (bcf_row_index_bpc_central_table)) * bcf_row_scale_scale_bpc_central)) /\ exists bcf_quotient_bpc_central_table_decoded_row_scale. bcf_row_scale_code_bpc_central = bcf_quotient_bpc_central_table_decoded_row_scale * S ((S (bcf_row_index_bpc_central_table)) * bcf_row_scale_scale_bpc_central) + (bcf_row_scale_bpc_central_table))) /\ ((bcf_row_index_bpc_central_table = 0 /\ (forall bcf_index_bpc_central_table_zero_row. (exists bcf_lt_gap_bpc_central_table_zero_row_bound. bcf_lt_gap_bpc_central_table_zero_row_bound + S (bcf_index_bpc_central_table_zero_row) = S (n + n)) -> exists bcf_value_bpc_central_table_zero_row. ((((exists bcf_height_bpc_central_table_zero_row_entry. bcf_height_bpc_central_table_zero_row_entry + S (bcf_value_bpc_central_table_zero_row) = S ((S (bcf_index_bpc_central_table_zero_row)) * bcf_row_scale_bpc_central_table)) /\ exists bcf_quotient_bpc_central_table_zero_row_entry. bcf_row_code_bpc_central_table = bcf_quotient_bpc_central_table_zero_row_entry * S ((S (bcf_index_bpc_central_table_zero_row)) * bcf_row_scale_bpc_central_table) + (bcf_value_bpc_central_table_zero_row))) /\ ((bcf_index_bpc_central_table_zero_row = 0 /\ bcf_value_bpc_central_table_zero_row = 1) \/ exists bcf_predecessor_bpc_central_table_zero_row. bcf_index_bpc_central_table_zero_row = S bcf_predecessor_bpc_central_table_zero_row /\ bcf_value_bpc_central_table_zero_row = 0)))) \/ exists bcf_predecessor_bpc_central_table bcf_previous_code_bpc_central_table bcf_previous_scale_bpc_central_table. bcf_row_index_bpc_central_table = S bcf_predecessor_bpc_central_table /\ ((((exists bcf_height_bpc_central_table_decoded_previous_code. bcf_height_bpc_central_table_decoded_previous_code + S (bcf_previous_code_bpc_central_table) = S ((S (bcf_predecessor_bpc_central_table)) * bcf_row_code_scale_bpc_central)) /\ exists bcf_quotient_bpc_central_table_decoded_previous_code. bcf_row_code_code_bpc_central = bcf_quotient_bpc_central_table_decoded_previous_code * S ((S (bcf_predecessor_bpc_central_table)) * bcf_row_code_scale_bpc_central) + (bcf_previous_code_bpc_central_table))) /\ ((((exists bcf_height_bpc_central_table_decoded_previous_scale. bcf_height_bpc_central_table_decoded_previous_scale + S (bcf_previous_scale_bpc_central_table) = S ((S (bcf_predecessor_bpc_central_table)) * bcf_row_scale_scale_bpc_central)) /\ exists bcf_quotient_bpc_central_table_decoded_previous_scale. bcf_row_scale_code_bpc_central = bcf_quotient_bpc_central_table_decoded_previous_scale * S ((S (bcf_predecessor_bpc_central_table)) * bcf_row_scale_scale_bpc_central) + (bcf_previous_scale_bpc_central_table))) /\ (forall bcf_index_bpc_central_table_row_step. (exists bcf_lt_gap_bpc_central_table_row_step_bound. bcf_lt_gap_bpc_central_table_row_step_bound + S (bcf_index_bpc_central_table_row_step) = S (n + n)) -> exists bcf_value_bpc_central_table_row_step. ((((exists bcf_height_bpc_central_table_row_step_entry. bcf_height_bpc_central_table_row_step_entry + S (bcf_value_bpc_central_table_row_step) = S ((S (bcf_index_bpc_central_table_row_step)) * bcf_row_scale_bpc_central_table)) /\ exists bcf_quotient_bpc_central_table_row_step_entry. bcf_row_code_bpc_central_table = bcf_quotient_bpc_central_table_row_step_entry * S ((S (bcf_index_bpc_central_table_row_step)) * bcf_row_scale_bpc_central_table) + (bcf_value_bpc_central_table_row_step))) /\ ((bcf_index_bpc_central_table_row_step = 0 /\ bcf_value_bpc_central_table_row_step = 1) \/ exists bcf_predecessor_bpc_central_table_row_step bcf_left_bpc_central_table_row_step bcf_right_bpc_central_table_row_step. bcf_index_bpc_central_table_row_step = S bcf_predecessor_bpc_central_table_row_step /\ ((((exists bcf_height_bpc_central_table_row_step_previous_left. bcf_height_bpc_central_table_row_step_previous_left + S (bcf_left_bpc_central_table_row_step) = S ((S (bcf_predecessor_bpc_central_table_row_step)) * bcf_previous_scale_bpc_central_table)) /\ exists bcf_quotient_bpc_central_table_row_step_previous_left. bcf_previous_code_bpc_central_table = bcf_quotient_bpc_central_table_row_step_previous_left * S ((S (bcf_predecessor_bpc_central_table_row_step)) * bcf_previous_scale_bpc_central_table) + (bcf_left_bpc_central_table_row_step))) /\ ((((exists bcf_height_bpc_central_table_row_step_previous_right. bcf_height_bpc_central_table_row_step_previous_right + S (bcf_right_bpc_central_table_row_step) = S ((S (S (bcf_predecessor_bpc_central_table_row_step))) * bcf_previous_scale_bpc_central_table)) /\ exists bcf_quotient_bpc_central_table_row_step_previous_right. bcf_previous_code_bpc_central_table = bcf_quotient_bpc_central_table_row_step_previous_right * S ((S (S (bcf_predecessor_bpc_central_table_row_step))) * bcf_previous_scale_bpc_central_table) + (bcf_right_bpc_central_table_row_step))) /\ bcf_value_bpc_central_table_row_step = bcf_left_bpc_central_table_row_step + bcf_right_bpc_central_table_row_step))))))))))) /\ ((((exists bcf_height_bpc_central_decoded_row_code. bcf_height_bpc_central_decoded_row_code + S (bcf_row_code_bpc_central) = S ((S (n + n)) * bcf_row_code_scale_bpc_central)) /\ exists bcf_quotient_bpc_central_decoded_row_code. bcf_row_code_code_bpc_central = bcf_quotient_bpc_central_decoded_row_code * S ((S (n + n)) * bcf_row_code_scale_bpc_central) + (bcf_row_code_bpc_central))) /\ ((((exists bcf_height_bpc_central_decoded_row_scale. bcf_height_bpc_central_decoded_row_scale + S (bcf_row_scale_bpc_central) = S ((S (n + n)) * bcf_row_scale_scale_bpc_central)) /\ exists bcf_quotient_bpc_central_decoded_row_scale. bcf_row_scale_code_bpc_central = bcf_quotient_bpc_central_decoded_row_scale * S ((S (n + n)) * bcf_row_scale_scale_bpc_central) + (bcf_row_scale_bpc_central))) /\ (((exists bcf_height_bpc_central_decoded_value. bcf_height_bpc_central_decoded_value + S (C) = S ((S (n)) * bcf_row_scale_bpc_central)) /\ exists bcf_quotient_bpc_central_decoded_value. bcf_row_code_bpc_central = bcf_quotient_bpc_central_decoded_value * S ((S (n)) * bcf_row_scale_bpc_central) + (C))))))))) /\ (((exists bpv_gap_bpc_result_exponent_bound. bpv_gap_bpc_result_exponent_bound + 1 = C) /\ (exists bpv_result_bpc_result_selected. ((exists ff_b_bpc_result_selected_power ff_c_bpc_result_selected_power. ((forall ff_i_bpc_result_selected_power_repeat. (exists ff_lt_bpc_result_selected_power_repeat_bound. ff_lt_bpc_result_selected_power_repeat_bound + S ff_i_bpc_result_selected_power_repeat = 1) -> (((exists ff_h_bpc_result_selected_power_repeat_decoded. ff_h_bpc_result_selected_power_repeat_decoded + S (p) = S ((S (ff_i_bpc_result_selected_power_repeat)) * ff_c_bpc_result_selected_power)) /\ exists ff_q_bpc_result_selected_power_repeat_decoded. ff_b_bpc_result_selected_power = ff_q_bpc_result_selected_power_repeat_decoded * S ((S (ff_i_bpc_result_selected_power_repeat)) * ff_c_bpc_result_selected_power) + (p)))) /\ (exists ff_u_bpc_result_selected_power_product ff_v_bpc_result_selected_power_product. ((((exists ff_h_bpc_result_selected_power_product_start. ff_h_bpc_result_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpc_result_selected_power_product)) /\ exists ff_q_bpc_result_selected_power_product_start. ff_u_bpc_result_selected_power_product = ff_q_bpc_result_selected_power_product_start * S ((S (0)) * ff_v_bpc_result_selected_power_product) + (1))) /\ ((((exists ff_h_bpc_result_selected_power_product_terminal. ff_h_bpc_result_selected_power_product_terminal + S (bpv_result_bpc_result_selected) = S ((S (1)) * ff_v_bpc_result_selected_power_product)) /\ exists ff_q_bpc_result_selected_power_product_terminal. ff_u_bpc_result_selected_power_product = ff_q_bpc_result_selected_power_product_terminal * S ((S (1)) * ff_v_bpc_result_selected_power_product) + (bpv_result_bpc_result_selected))) /\ forall ff_i_bpc_result_selected_power_product. (exists ff_lt_bpc_result_selected_power_product_bound. ff_lt_bpc_result_selected_power_product_bound + S ff_i_bpc_result_selected_power_product = 1) -> exists ff_p_bpc_result_selected_power_product ff_r_bpc_result_selected_power_product ff_s_bpc_result_selected_power_product. ((((exists ff_h_bpc_result_selected_power_product_factor. ff_h_bpc_result_selected_power_product_factor + S (ff_p_bpc_result_selected_power_product) = S ((S (ff_i_bpc_result_selected_power_product)) * ff_c_bpc_result_selected_power)) /\ exists ff_q_bpc_result_selected_power_product_factor. ff_b_bpc_result_selected_power = ff_q_bpc_result_selected_power_product_factor * S ((S (ff_i_bpc_result_selected_power_product)) * ff_c_bpc_result_selected_power) + (ff_p_bpc_result_selected_power_product))) /\ ((((exists ff_h_bpc_result_selected_power_product_partial. ff_h_bpc_result_selected_power_product_partial + S (ff_r_bpc_result_selected_power_product) = S ((S (ff_i_bpc_result_selected_power_product)) * ff_v_bpc_result_selected_power_product)) /\ exists ff_q_bpc_result_selected_power_product_partial. ff_u_bpc_result_selected_power_product = ff_q_bpc_result_selected_power_product_partial * S ((S (ff_i_bpc_result_selected_power_product)) * ff_v_bpc_result_selected_power_product) + (ff_r_bpc_result_selected_power_product))) /\ ((((exists ff_h_bpc_result_selected_power_product_successor. ff_h_bpc_result_selected_power_product_successor + S (ff_s_bpc_result_selected_power_product) = S ((S (S ff_i_bpc_result_selected_power_product)) * ff_v_bpc_result_selected_power_product)) /\ exists ff_q_bpc_result_selected_power_product_successor. ff_u_bpc_result_selected_power_product = ff_q_bpc_result_selected_power_product_successor * S ((S (S ff_i_bpc_result_selected_power_product)) * ff_v_bpc_result_selected_power_product) + (ff_s_bpc_result_selected_power_product))) /\ ff_s_bpc_result_selected_power_product = ff_r_bpc_result_selected_power_product * ff_p_bpc_result_selected_power_product)))))))) /\ (exists bpv_factor_bpc_result_selected_divides. C = bpv_result_bpc_result_selected * bpv_factor_bpc_result_selected_divides)))) /\ forall bpv_candidate_bpc_result. (exists bpv_gap_bpc_result_candidate_bound. bpv_gap_bpc_result_candidate_bound + bpv_candidate_bpc_result = C) -> (exists bpv_result_bpc_result_candidate. ((exists ff_b_bpc_result_candidate_power ff_c_bpc_result_candidate_power. ((forall ff_i_bpc_result_candidate_power_repeat. (exists ff_lt_bpc_result_candidate_power_repeat_bound. ff_lt_bpc_result_candidate_power_repeat_bound + S ff_i_bpc_result_candidate_power_repeat = bpv_candidate_bpc_result) -> (((exists ff_h_bpc_result_candidate_power_repeat_decoded. ff_h_bpc_result_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_bpc_result_candidate_power_repeat)) * ff_c_bpc_result_candidate_power)) /\ exists ff_q_bpc_result_candidate_power_repeat_decoded. ff_b_bpc_result_candidate_power = ff_q_bpc_result_candidate_power_repeat_decoded * S ((S (ff_i_bpc_result_candidate_power_repeat)) * ff_c_bpc_result_candidate_power) + (p)))) /\ (exists ff_u_bpc_result_candidate_power_product ff_v_bpc_result_candidate_power_product. ((((exists ff_h_bpc_result_candidate_power_product_start. ff_h_bpc_result_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpc_result_candidate_power_product)) /\ exists ff_q_bpc_result_candidate_power_product_start. ff_u_bpc_result_candidate_power_product = ff_q_bpc_result_candidate_power_product_start * S ((S (0)) * ff_v_bpc_result_candidate_power_product) + (1))) /\ ((((exists ff_h_bpc_result_candidate_power_product_terminal. ff_h_bpc_result_candidate_power_product_terminal + S (bpv_result_bpc_result_candidate) = S ((S (bpv_candidate_bpc_result)) * ff_v_bpc_result_candidate_power_product)) /\ exists ff_q_bpc_result_candidate_power_product_terminal. ff_u_bpc_result_candidate_power_product = ff_q_bpc_result_candidate_power_product_terminal * S ((S (bpv_candidate_bpc_result)) * ff_v_bpc_result_candidate_power_product) + (bpv_result_bpc_result_candidate))) /\ forall ff_i_bpc_result_candidate_power_product. (exists ff_lt_bpc_result_candidate_power_product_bound. ff_lt_bpc_result_candidate_power_product_bound + S ff_i_bpc_result_candidate_power_product = bpv_candidate_bpc_result) -> exists ff_p_bpc_result_candidate_power_product ff_r_bpc_result_candidate_power_product ff_s_bpc_result_candidate_power_product. ((((exists ff_h_bpc_result_candidate_power_product_factor. ff_h_bpc_result_candidate_power_product_factor + S (ff_p_bpc_result_candidate_power_product) = S ((S (ff_i_bpc_result_candidate_power_product)) * ff_c_bpc_result_candidate_power)) /\ exists ff_q_bpc_result_candidate_power_product_factor. ff_b_bpc_result_candidate_power = ff_q_bpc_result_candidate_power_product_factor * S ((S (ff_i_bpc_result_candidate_power_product)) * ff_c_bpc_result_candidate_power) + (ff_p_bpc_result_candidate_power_product))) /\ ((((exists ff_h_bpc_result_candidate_power_product_partial. ff_h_bpc_result_candidate_power_product_partial + S (ff_r_bpc_result_candidate_power_product) = S ((S (ff_i_bpc_result_candidate_power_product)) * ff_v_bpc_result_candidate_power_product)) /\ exists ff_q_bpc_result_candidate_power_product_partial. ff_u_bpc_result_candidate_power_product = ff_q_bpc_result_candidate_power_product_partial * S ((S (ff_i_bpc_result_candidate_power_product)) * ff_v_bpc_result_candidate_power_product) + (ff_r_bpc_result_candidate_power_product))) /\ ((((exists ff_h_bpc_result_candidate_power_product_successor. ff_h_bpc_result_candidate_power_product_successor + S (ff_s_bpc_result_candidate_power_product) = S ((S (S ff_i_bpc_result_candidate_power_product)) * ff_v_bpc_result_candidate_power_product)) /\ exists ff_q_bpc_result_candidate_power_product_successor. ff_u_bpc_result_candidate_power_product = ff_q_bpc_result_candidate_power_product_successor * S ((S (S ff_i_bpc_result_candidate_power_product)) * ff_v_bpc_result_candidate_power_product) + (ff_s_bpc_result_candidate_power_product))) /\ ff_s_bpc_result_candidate_power_product = ff_r_bpc_result_candidate_power_product * ff_p_bpc_result_candidate_power_product)))))))) /\ (exists bpv_factor_bpc_result_candidate_divides. C = bpv_result_bpc_result_candidate * bpv_factor_bpc_result_candidate_divides))) -> (exists bpv_gap_bpc_result_maximal. bpv_gap_bpc_result_maximal + bpv_candidate_bpc_result = 1))))))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

32 script commands · 16 reading checkpoints · 2 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 (1)
bertrand window central valuation one

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–2

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

  1. L1
    intro n
  2. L2
    intro hindex
02Use earlier factsL3–3

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

  1. L3
    specialize bertrand_strict n
03Establish hprime_existsL4–6

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

  1. L4
    have hprime_exists : exists p. (((~(p = 1) /\ forall frm_prime_left_bpc_prime frm_prime_right_bpc_prime. p = frm_prime_left_bpc_prime * frm_prime_right_bpc_prime -> frm_prime_left_bpc_prime = 1 \/ frm_prime_right_bpc_prime = 1)) /\ ((exists bcf_lt_gap_bpc_lower. bcf_lt_gap_bpc_lower + S (n) = p) /\ (exists bcf_lt_gap_bpc_upper. bcf_lt_gap_bpc_upper + S (p) = n + n)))
  2. L5
    apply bertrand_strict
  3. L6
    exact hindex
04Separate the logical casesL7–9

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

  1. L7
    cases hprime_exists
  2. L8
    cases hprime_exists_witness
  3. L9
    cases hprime_exists_witness_right
05Use earlier factsL10–10

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

  1. L10
    specialize central_binom_exists n
06Establish hcentral_existsL11–12

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

  1. L11
    have hcentral_exists : ∃ C. Lt(n + n,n) ∧ C = 0 ∨ Le(n,n + n) ∧ (∃ x. ∃ y. ∃ z. ∃ m. ∃ k. ∃ i. (∀ j. Lt(j,S (n + n)) → ∃ u. ∃ v. Beta(x,y,j,u) ∧ (Beta(z,m,j,v) ∧ (j = 0 ∧ (∀ w. Lt(w,S (n + n)) → ∃ x0. Beta(u,v,w,x0) ∧ (w = 0 ∧ x0 = 1 ∨ (∃ x1. w = S x1 ∧ x0 = 0))) ∨ (∃ w. ∃ x0. ∃ x1. j = S w ∧ (Beta(x,y,w,x0) ∧ (Beta(z,m,w,x1) ∧ (∀ x2. Lt(x2,S (n + n)) → ∃ x3. Beta(u,v,x2,x3) ∧ (x2 = 0 ∧ x3 = 1 ∨ (∃ x4. ∃ x5. ∃ x6. x2 = S x4 ∧ (Beta(x0,x1,x4,x5) ∧ (Beta(x0,x1,S x4,x6) ∧ x3 = x5 + x6))))))))))) ∧ (Beta(x,y,n + n,k) ∧ (Beta(z,m,n + n,i) ∧ Beta(k,i,n,C))))Definitions: BetaLeLtOriginal native command in the exact edition
  2. L12
    exact central_binom_exists
07Separate the logical casesL13–13

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

  1. L13
    cases hcentral_exists
08Construct an explicit witnessL14–15

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

  1. L14
    exists x
  2. L15
    exists x1
09Separate the logical casesL16–16

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

  1. L16
    split
10Use earlier factsL17–17

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

  1. L17
    exact hprime_exists_witness_left
11Separate the logical casesL18–18

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

  1. L18
    split
12Use earlier factsL19–19

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

  1. L19
    exact hprime_exists_witness_right_left
13Separate the logical casesL20–20

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

  1. L20
    split
14Use earlier factsL21–21

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

  1. L21
    exact hprime_exists_witness_right_right
15Separate the logical casesL22–22

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

  1. L22
    split
16Use earlier factsL23–32

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

  1. L23
    exact hcentral_exists_witness
  2. L24
    specialize bertrand_window_central_valuation_one n
  3. L25
    specialize bertrand_window_central_valuation_one x
  4. L26
    specialize bertrand_window_central_valuation_one x1
  5. L27
    apply bertrand_window_central_valuation_one
  6. L28
    exact hindex
  7. L29
    exact hprime_exists_witness_left
  8. L30
    exact hprime_exists_witness_right_left
  9. L31
    exact hprime_exists_witness_right_right
  10. L32
    exact hcentral_exists_witness

Library-wide reading audit

Original defined command ledger · 32 lines
  1. 0001intro n
  2. 0002intro hindex
  3. 0003specialize bertrand_strict n
  4. 0004have hprime_exists : exists p. (((~(p = 1) /\ forall frm_prime_left_bpc_prime frm_prime_right_bpc_prime. p = frm_prime_left_bpc_prime * frm_prime_right_bpc_prime -> frm_prime_left_bpc_prime = 1 \/ frm_prime_right_bpc_prime = 1)) /\ ((exists bcf_lt_gap_bpc_lower. bcf_lt_gap_bpc_lower + S (n) = p) /\ (exists bcf_lt_gap_bpc_upper. bcf_lt_gap_bpc_upper + S (p) = n + n)))
  5. 0005apply bertrand_strict
  6. 0006exact hindex
  7. 0007cases hprime_exists
  8. 0008cases hprime_exists_witness
  9. 0009cases hprime_exists_witness_right
  10. 0010specialize central_binom_exists n
  11. 0011have hcentral_exists : exists C. (((exists bcf_lt_gap_bpc_central_out_of_range. bcf_lt_gap_bpc_central_out_of_range + S (n + n) = n) /\ C = 0) \/ ((exists bcf_le_gap_bpc_central_in_range. bcf_le_gap_bpc_central_in_range + (n) = n + n) /\ (exists bcf_row_code_code_bpc_central bcf_row_code_scale_bpc_central bcf_row_scale_code_bpc_central bcf_row_scale_scale_bpc_central bcf_row_code_bpc_central bcf_row_scale_bpc_central. ((forall bcf_row_index_bpc_central_table. (exists bcf_lt_gap_bpc_central_table_row_bound. bcf_lt_gap_bpc_central_table_row_bound + S (bcf_row_index_bpc_central_table) = S (n + n)) -> exists bcf_row_code_bpc_central_table bcf_row_scale_bpc_central_table. ((((exists bcf_height_bpc_central_table_decoded_row_code. bcf_height_bpc_central_table_decoded_row_code + S (bcf_row_code_bpc_central_table) = S ((S (bcf_row_index_bpc_central_table)) * bcf_row_code_scale_bpc_central)) /\ exists bcf_quotient_bpc_central_table_decoded_row_code. bcf_row_code_code_bpc_central = bcf_quotient_bpc_central_table_decoded_row_code * S ((S (bcf_row_index_bpc_central_table)) * bcf_row_code_scale_bpc_central) + (bcf_row_code_bpc_central_table))) /\ ((((exists bcf_height_bpc_central_table_decoded_row_scale. bcf_height_bpc_central_table_decoded_row_scale + S (bcf_row_scale_bpc_central_table) = S ((S (bcf_row_index_bpc_central_table)) * bcf_row_scale_scale_bpc_central)) /\ exists bcf_quotient_bpc_central_table_decoded_row_scale. bcf_row_scale_code_bpc_central = bcf_quotient_bpc_central_table_decoded_row_scale * S ((S (bcf_row_index_bpc_central_table)) * bcf_row_scale_scale_bpc_central) + (bcf_row_scale_bpc_central_table))) /\ ((bcf_row_index_bpc_central_table = 0 /\ (forall bcf_index_bpc_central_table_zero_row. (exists bcf_lt_gap_bpc_central_table_zero_row_bound. bcf_lt_gap_bpc_central_table_zero_row_bound + S (bcf_index_bpc_central_table_zero_row) = S (n + n)) -> exists bcf_value_bpc_central_table_zero_row. ((((exists bcf_height_bpc_central_table_zero_row_entry. bcf_height_bpc_central_table_zero_row_entry + S (bcf_value_bpc_central_table_zero_row) = S ((S (bcf_index_bpc_central_table_zero_row)) * bcf_row_scale_bpc_central_table)) /\ exists bcf_quotient_bpc_central_table_zero_row_entry. bcf_row_code_bpc_central_table = bcf_quotient_bpc_central_table_zero_row_entry * S ((S (bcf_index_bpc_central_table_zero_row)) * bcf_row_scale_bpc_central_table) + (bcf_value_bpc_central_table_zero_row))) /\ ((bcf_index_bpc_central_table_zero_row = 0 /\ bcf_value_bpc_central_table_zero_row = 1) \/ exists bcf_predecessor_bpc_central_table_zero_row. bcf_index_bpc_central_table_zero_row = S bcf_predecessor_bpc_central_table_zero_row /\ bcf_value_bpc_central_table_zero_row = 0)))) \/ exists bcf_predecessor_bpc_central_table bcf_previous_code_bpc_central_table bcf_previous_scale_bpc_central_table. bcf_row_index_bpc_central_table = S bcf_predecessor_bpc_central_table /\ ((((exists bcf_height_bpc_central_table_decoded_previous_code. bcf_height_bpc_central_table_decoded_previous_code + S (bcf_previous_code_bpc_central_table) = S ((S (bcf_predecessor_bpc_central_table)) * bcf_row_code_scale_bpc_central)) /\ exists bcf_quotient_bpc_central_table_decoded_previous_code. bcf_row_code_code_bpc_central = bcf_quotient_bpc_central_table_decoded_previous_code * S ((S (bcf_predecessor_bpc_central_table)) * bcf_row_code_scale_bpc_central) + (bcf_previous_code_bpc_central_table))) /\ ((((exists bcf_height_bpc_central_table_decoded_previous_scale. bcf_height_bpc_central_table_decoded_previous_scale + S (bcf_previous_scale_bpc_central_table) = S ((S (bcf_predecessor_bpc_central_table)) * bcf_row_scale_scale_bpc_central)) /\ exists bcf_quotient_bpc_central_table_decoded_previous_scale. bcf_row_scale_code_bpc_central = bcf_quotient_bpc_central_table_decoded_previous_scale * S ((S (bcf_predecessor_bpc_central_table)) * bcf_row_scale_scale_bpc_central) + (bcf_previous_scale_bpc_central_table))) /\ (forall bcf_index_bpc_central_table_row_step. (exists bcf_lt_gap_bpc_central_table_row_step_bound. bcf_lt_gap_bpc_central_table_row_step_bound + S (bcf_index_bpc_central_table_row_step) = S (n + n)) -> exists bcf_value_bpc_central_table_row_step. ((((exists bcf_height_bpc_central_table_row_step_entry. bcf_height_bpc_central_table_row_step_entry + S (bcf_value_bpc_central_table_row_step) = S ((S (bcf_index_bpc_central_table_row_step)) * bcf_row_scale_bpc_central_table)) /\ exists bcf_quotient_bpc_central_table_row_step_entry. bcf_row_code_bpc_central_table = bcf_quotient_bpc_central_table_row_step_entry * S ((S (bcf_index_bpc_central_table_row_step)) * bcf_row_scale_bpc_central_table) + (bcf_value_bpc_central_table_row_step))) /\ ((bcf_index_bpc_central_table_row_step = 0 /\ bcf_value_bpc_central_table_row_step = 1) \/ exists bcf_predecessor_bpc_central_table_row_step bcf_left_bpc_central_table_row_step bcf_right_bpc_central_table_row_step. bcf_index_bpc_central_table_row_step = S bcf_predecessor_bpc_central_table_row_step /\ ((((exists bcf_height_bpc_central_table_row_step_previous_left. bcf_height_bpc_central_table_row_step_previous_left + S (bcf_left_bpc_central_table_row_step) = S ((S (bcf_predecessor_bpc_central_table_row_step)) * bcf_previous_scale_bpc_central_table)) /\ exists bcf_quotient_bpc_central_table_row_step_previous_left. bcf_previous_code_bpc_central_table = bcf_quotient_bpc_central_table_row_step_previous_left * S ((S (bcf_predecessor_bpc_central_table_row_step)) * bcf_previous_scale_bpc_central_table) + (bcf_left_bpc_central_table_row_step))) /\ ((((exists bcf_height_bpc_central_table_row_step_previous_right. bcf_height_bpc_central_table_row_step_previous_right + S (bcf_right_bpc_central_table_row_step) = S ((S (S (bcf_predecessor_bpc_central_table_row_step))) * bcf_previous_scale_bpc_central_table)) /\ exists bcf_quotient_bpc_central_table_row_step_previous_right. bcf_previous_code_bpc_central_table = bcf_quotient_bpc_central_table_row_step_previous_right * S ((S (S (bcf_predecessor_bpc_central_table_row_step))) * bcf_previous_scale_bpc_central_table) + (bcf_right_bpc_central_table_row_step))) /\ bcf_value_bpc_central_table_row_step = bcf_left_bpc_central_table_row_step + bcf_right_bpc_central_table_row_step))))))))))) /\ ((((exists bcf_height_bpc_central_decoded_row_code. bcf_height_bpc_central_decoded_row_code + S (bcf_row_code_bpc_central) = S ((S (n + n)) * bcf_row_code_scale_bpc_central)) /\ exists bcf_quotient_bpc_central_decoded_row_code. bcf_row_code_code_bpc_central = bcf_quotient_bpc_central_decoded_row_code * S ((S (n + n)) * bcf_row_code_scale_bpc_central) + (bcf_row_code_bpc_central))) /\ ((((exists bcf_height_bpc_central_decoded_row_scale. bcf_height_bpc_central_decoded_row_scale + S (bcf_row_scale_bpc_central) = S ((S (n + n)) * bcf_row_scale_scale_bpc_central)) /\ exists bcf_quotient_bpc_central_decoded_row_scale. bcf_row_scale_code_bpc_central = bcf_quotient_bpc_central_decoded_row_scale * S ((S (n + n)) * bcf_row_scale_scale_bpc_central) + (bcf_row_scale_bpc_central))) /\ (((exists bcf_height_bpc_central_decoded_value. bcf_height_bpc_central_decoded_value + S (C) = S ((S (n)) * bcf_row_scale_bpc_central)) /\ exists bcf_quotient_bpc_central_decoded_value. bcf_row_code_bpc_central = bcf_quotient_bpc_central_decoded_value * S ((S (n)) * bcf_row_scale_bpc_central) + (C)))))))))
  12. 0012exact central_binom_exists
  13. 0013cases hcentral_exists
  14. 0014exists x
  15. 0015exists x1
  16. 0016split
  17. 0017exact hprime_exists_witness_left
  18. 0018split
  19. 0019exact hprime_exists_witness_right_left
  20. 0020split
  21. 0021exact hprime_exists_witness_right_right
  22. 0022split
  23. 0023exact hcentral_exists_witness
  24. 0024specialize bertrand_window_central_valuation_one n
  25. 0025specialize bertrand_window_central_valuation_one x
  26. 0026specialize bertrand_window_central_valuation_one x1
  27. 0027apply bertrand_window_central_valuation_one
  28. 0028exact hindex
  29. 0029exact hprime_exists_witness_left
  30. 0030exact hprime_exists_witness_right_left
  31. 0031exact hprime_exists_witness_right_right
  32. 0032exact hcentral_exists_witness