BP0006

bertrand_window_central_valuation_one

Every Bertrand-window prime has a witnessed literal valuation-one graph.

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. ∀ p. ∀ C. Lt(1,n) → Prime(p) → Lt(n,p) → Lt(p,n + n) → 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)))) → PowerValuationOne(p,C)

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

central_binom_positive · checked external prerequisiteprime_power_valuation_exists · checked external prerequisitebertrand_window_central_valuation_equals_one
Original expanded first-order statement 
forall n p C. (exists bcf_lt_gap_bpc_index. bcf_lt_gap_bpc_index + S (1) = n) -> ((~(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 46 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

46 script commands · 10 reading checkpoints · 4 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 equals 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–8

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

  1. L1
    intro n
  2. L2
    intro p
  3. L3
    intro C
  4. L4
    intro hindex
  5. L5
    intro hprime
  6. L6
    intro hlower
  7. L7
    intro hupper
  8. L8
    intro hcentral
02Establish hpositiveL9–13

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

  1. L9
    have hpositive : exists a. C = S a
  2. L10
    specialize central_binom_positive n
  3. L11
    specialize central_binom_positive C
  4. L12
    apply central_binom_positive
  5. L13
    exact hcentral
03Separate the logical casesL14–14

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

  1. L14
    cases hpositive
04Establish hnonzeroL15–21

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

  1. L15
    have hnonzero : ~(C = 0)
  2. L16
    intro hzero
  3. L17
    rewrite hpositive_witness at hzero
  4. L18
    apply PA1
  5. L19
    exact hzero
  6. L20
    specialize prime_power_valuation_exists p
  7. L21
    specialize prime_power_valuation_exists C
05Establish hvaluation_existsL22–25

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

  1. L22
    have hvaluation_exists : ∃ e. Prime(p) ∧ ¬C = 0 ∧ BoundedPowerValuation(p,C,C,e)Definitions: PrimeBoundedPowerValuationOriginal native command in the exact edition
  2. L23
    apply prime_power_valuation_exists
  3. L24
    exact hprime
  4. L25
    exact hnonzero
06Separate the logical casesL26–27

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

  1. L26
    cases hvaluation_exists
  2. L27
    cases hvaluation_exists_witness
07Establish hexactL28–37

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bertrand window central valuation equals one.

  1. L28
    have hexact : x1 = 1
  2. L29
    specialize bertrand_window_central_valuation_equals_one n
  3. L30
    specialize bertrand_window_central_valuation_equals_one p
  4. L31
    specialize bertrand_window_central_valuation_equals_one C
  5. L32
    specialize bertrand_window_central_valuation_equals_one x1
  6. L33
    apply bertrand_window_central_valuation_equals_one
  7. L34
    exact hindex
  8. L35
    exact hprime
  9. L36
    exact hlower
  10. L37
    exact hupper
08Use earlier factsL38–39

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

  1. L38
    exact hcentral
  2. L39
    exact hvaluation_exists_witness_right
09Calculate and transport equalitiesL40–45

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

  1. L40
    rewrite hexact at hvaluation_exists_witness_right
  2. L41
    rewrite hexact at hvaluation_exists_witness_right
  3. L42
    rewrite hexact at hvaluation_exists_witness_right
  4. L43
    rewrite hexact at hvaluation_exists_witness_right
  5. L44
    rewrite hexact at hvaluation_exists_witness_right
  6. L45
    rewrite hexact at hvaluation_exists_witness_right
10Use earlier factsL46–46

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

  1. L46
    exact hvaluation_exists_witness_right

Library-wide reading audit

Original defined command ledger · 46 lines
  1. 0001intro n
  2. 0002intro p
  3. 0003intro C
  4. 0004intro hindex
  5. 0005intro hprime
  6. 0006intro hlower
  7. 0007intro hupper
  8. 0008intro hcentral
  9. 0009have hpositive : exists a. C = S a
  10. 0010specialize central_binom_positive n
  11. 0011specialize central_binom_positive C
  12. 0012apply central_binom_positive
  13. 0013exact hcentral
  14. 0014cases hpositive
  15. 0015have hnonzero : ~(C = 0)
  16. 0016intro hzero
  17. 0017rewrite hpositive_witness at hzero
  18. 0018apply PA1
  19. 0019exact hzero
  20. 0020specialize prime_power_valuation_exists p
  21. 0021specialize prime_power_valuation_exists C
  22. 0022have hvaluation_exists : exists e. (((((~(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)) /\ ~(C = 0))) /\ (((exists bpv_gap_bpc_value_exponent_bound. bpv_gap_bpc_value_exponent_bound + e = C) /\ (exists bpv_result_bpc_value_selected. ((exists ff_b_bpc_value_selected_power ff_c_bpc_value_selected_power. ((forall ff_i_bpc_value_selected_power_repeat. (exists ff_lt_bpc_value_selected_power_repeat_bound. ff_lt_bpc_value_selected_power_repeat_bound + S ff_i_bpc_value_selected_power_repeat = e) -> (((exists ff_h_bpc_value_selected_power_repeat_decoded. ff_h_bpc_value_selected_power_repeat_decoded + S (p) = S ((S (ff_i_bpc_value_selected_power_repeat)) * ff_c_bpc_value_selected_power)) /\ exists ff_q_bpc_value_selected_power_repeat_decoded. ff_b_bpc_value_selected_power = ff_q_bpc_value_selected_power_repeat_decoded * S ((S (ff_i_bpc_value_selected_power_repeat)) * ff_c_bpc_value_selected_power) + (p)))) /\ (exists ff_u_bpc_value_selected_power_product ff_v_bpc_value_selected_power_product. ((((exists ff_h_bpc_value_selected_power_product_start. ff_h_bpc_value_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpc_value_selected_power_product)) /\ exists ff_q_bpc_value_selected_power_product_start. ff_u_bpc_value_selected_power_product = ff_q_bpc_value_selected_power_product_start * S ((S (0)) * ff_v_bpc_value_selected_power_product) + (1))) /\ ((((exists ff_h_bpc_value_selected_power_product_terminal. ff_h_bpc_value_selected_power_product_terminal + S (bpv_result_bpc_value_selected) = S ((S (e)) * ff_v_bpc_value_selected_power_product)) /\ exists ff_q_bpc_value_selected_power_product_terminal. ff_u_bpc_value_selected_power_product = ff_q_bpc_value_selected_power_product_terminal * S ((S (e)) * ff_v_bpc_value_selected_power_product) + (bpv_result_bpc_value_selected))) /\ forall ff_i_bpc_value_selected_power_product. (exists ff_lt_bpc_value_selected_power_product_bound. ff_lt_bpc_value_selected_power_product_bound + S ff_i_bpc_value_selected_power_product = e) -> exists ff_p_bpc_value_selected_power_product ff_r_bpc_value_selected_power_product ff_s_bpc_value_selected_power_product. ((((exists ff_h_bpc_value_selected_power_product_factor. ff_h_bpc_value_selected_power_product_factor + S (ff_p_bpc_value_selected_power_product) = S ((S (ff_i_bpc_value_selected_power_product)) * ff_c_bpc_value_selected_power)) /\ exists ff_q_bpc_value_selected_power_product_factor. ff_b_bpc_value_selected_power = ff_q_bpc_value_selected_power_product_factor * S ((S (ff_i_bpc_value_selected_power_product)) * ff_c_bpc_value_selected_power) + (ff_p_bpc_value_selected_power_product))) /\ ((((exists ff_h_bpc_value_selected_power_product_partial. ff_h_bpc_value_selected_power_product_partial + S (ff_r_bpc_value_selected_power_product) = S ((S (ff_i_bpc_value_selected_power_product)) * ff_v_bpc_value_selected_power_product)) /\ exists ff_q_bpc_value_selected_power_product_partial. ff_u_bpc_value_selected_power_product = ff_q_bpc_value_selected_power_product_partial * S ((S (ff_i_bpc_value_selected_power_product)) * ff_v_bpc_value_selected_power_product) + (ff_r_bpc_value_selected_power_product))) /\ ((((exists ff_h_bpc_value_selected_power_product_successor. ff_h_bpc_value_selected_power_product_successor + S (ff_s_bpc_value_selected_power_product) = S ((S (S ff_i_bpc_value_selected_power_product)) * ff_v_bpc_value_selected_power_product)) /\ exists ff_q_bpc_value_selected_power_product_successor. ff_u_bpc_value_selected_power_product = ff_q_bpc_value_selected_power_product_successor * S ((S (S ff_i_bpc_value_selected_power_product)) * ff_v_bpc_value_selected_power_product) + (ff_s_bpc_value_selected_power_product))) /\ ff_s_bpc_value_selected_power_product = ff_r_bpc_value_selected_power_product * ff_p_bpc_value_selected_power_product)))))))) /\ (exists bpv_factor_bpc_value_selected_divides. C = bpv_result_bpc_value_selected * bpv_factor_bpc_value_selected_divides)))) /\ forall bpv_candidate_bpc_value. (exists bpv_gap_bpc_value_candidate_bound. bpv_gap_bpc_value_candidate_bound + bpv_candidate_bpc_value = C) -> (exists bpv_result_bpc_value_candidate. ((exists ff_b_bpc_value_candidate_power ff_c_bpc_value_candidate_power. ((forall ff_i_bpc_value_candidate_power_repeat. (exists ff_lt_bpc_value_candidate_power_repeat_bound. ff_lt_bpc_value_candidate_power_repeat_bound + S ff_i_bpc_value_candidate_power_repeat = bpv_candidate_bpc_value) -> (((exists ff_h_bpc_value_candidate_power_repeat_decoded. ff_h_bpc_value_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_bpc_value_candidate_power_repeat)) * ff_c_bpc_value_candidate_power)) /\ exists ff_q_bpc_value_candidate_power_repeat_decoded. ff_b_bpc_value_candidate_power = ff_q_bpc_value_candidate_power_repeat_decoded * S ((S (ff_i_bpc_value_candidate_power_repeat)) * ff_c_bpc_value_candidate_power) + (p)))) /\ (exists ff_u_bpc_value_candidate_power_product ff_v_bpc_value_candidate_power_product. ((((exists ff_h_bpc_value_candidate_power_product_start. ff_h_bpc_value_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpc_value_candidate_power_product)) /\ exists ff_q_bpc_value_candidate_power_product_start. ff_u_bpc_value_candidate_power_product = ff_q_bpc_value_candidate_power_product_start * S ((S (0)) * ff_v_bpc_value_candidate_power_product) + (1))) /\ ((((exists ff_h_bpc_value_candidate_power_product_terminal. ff_h_bpc_value_candidate_power_product_terminal + S (bpv_result_bpc_value_candidate) = S ((S (bpv_candidate_bpc_value)) * ff_v_bpc_value_candidate_power_product)) /\ exists ff_q_bpc_value_candidate_power_product_terminal. ff_u_bpc_value_candidate_power_product = ff_q_bpc_value_candidate_power_product_terminal * S ((S (bpv_candidate_bpc_value)) * ff_v_bpc_value_candidate_power_product) + (bpv_result_bpc_value_candidate))) /\ forall ff_i_bpc_value_candidate_power_product. (exists ff_lt_bpc_value_candidate_power_product_bound. ff_lt_bpc_value_candidate_power_product_bound + S ff_i_bpc_value_candidate_power_product = bpv_candidate_bpc_value) -> exists ff_p_bpc_value_candidate_power_product ff_r_bpc_value_candidate_power_product ff_s_bpc_value_candidate_power_product. ((((exists ff_h_bpc_value_candidate_power_product_factor. ff_h_bpc_value_candidate_power_product_factor + S (ff_p_bpc_value_candidate_power_product) = S ((S (ff_i_bpc_value_candidate_power_product)) * ff_c_bpc_value_candidate_power)) /\ exists ff_q_bpc_value_candidate_power_product_factor. ff_b_bpc_value_candidate_power = ff_q_bpc_value_candidate_power_product_factor * S ((S (ff_i_bpc_value_candidate_power_product)) * ff_c_bpc_value_candidate_power) + (ff_p_bpc_value_candidate_power_product))) /\ ((((exists ff_h_bpc_value_candidate_power_product_partial. ff_h_bpc_value_candidate_power_product_partial + S (ff_r_bpc_value_candidate_power_product) = S ((S (ff_i_bpc_value_candidate_power_product)) * ff_v_bpc_value_candidate_power_product)) /\ exists ff_q_bpc_value_candidate_power_product_partial. ff_u_bpc_value_candidate_power_product = ff_q_bpc_value_candidate_power_product_partial * S ((S (ff_i_bpc_value_candidate_power_product)) * ff_v_bpc_value_candidate_power_product) + (ff_r_bpc_value_candidate_power_product))) /\ ((((exists ff_h_bpc_value_candidate_power_product_successor. ff_h_bpc_value_candidate_power_product_successor + S (ff_s_bpc_value_candidate_power_product) = S ((S (S ff_i_bpc_value_candidate_power_product)) * ff_v_bpc_value_candidate_power_product)) /\ exists ff_q_bpc_value_candidate_power_product_successor. ff_u_bpc_value_candidate_power_product = ff_q_bpc_value_candidate_power_product_successor * S ((S (S ff_i_bpc_value_candidate_power_product)) * ff_v_bpc_value_candidate_power_product) + (ff_s_bpc_value_candidate_power_product))) /\ ff_s_bpc_value_candidate_power_product = ff_r_bpc_value_candidate_power_product * ff_p_bpc_value_candidate_power_product)))))))) /\ (exists bpv_factor_bpc_value_candidate_divides. C = bpv_result_bpc_value_candidate * bpv_factor_bpc_value_candidate_divides))) -> (exists bpv_gap_bpc_value_maximal. bpv_gap_bpc_value_maximal + bpv_candidate_bpc_value = e)))
  23. 0023apply prime_power_valuation_exists
  24. 0024exact hprime
  25. 0025exact hnonzero
  26. 0026cases hvaluation_exists
  27. 0027cases hvaluation_exists_witness
  28. 0028have hexact : x1 = 1
  29. 0029specialize bertrand_window_central_valuation_equals_one n
  30. 0030specialize bertrand_window_central_valuation_equals_one p
  31. 0031specialize bertrand_window_central_valuation_equals_one C
  32. 0032specialize bertrand_window_central_valuation_equals_one x1
  33. 0033apply bertrand_window_central_valuation_equals_one
  34. 0034exact hindex
  35. 0035exact hprime
  36. 0036exact hlower
  37. 0037exact hupper
  38. 0038exact hcentral
  39. 0039exact hvaluation_exists_witness_right
  40. 0040rewrite hexact at hvaluation_exists_witness_right
  41. 0041rewrite hexact at hvaluation_exists_witness_right
  42. 0042rewrite hexact at hvaluation_exists_witness_right
  43. 0043rewrite hexact at hvaluation_exists_witness_right
  44. 0044rewrite hexact at hvaluation_exists_witness_right
  45. 0045rewrite hexact at hvaluation_exists_witness_right
  46. 0046exact hvaluation_exists_witness_right