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. 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) ))) → Dvd(p,C) Every linked abbreviation expands hygienically to the identical original native formula.
Actual proof prerequisites lt_to_le · checked external prerequisite choose_prime_divides_between · checked external prerequisite
Original expanded first-order statement
forall n 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 bcf_quotient_bpc_bpc_central_factor. C = p * bcf_quotient_bpc_bpc_central_factor)Complete unchanged native tactic proof
All 22 lines are the exact independently kernel-checked original script.
Read the argument
Proof checkpoints 22 script commands · 4 reading checkpoints · 0 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.
Expand checkpoints Collapse checkpoints Show original steps Find a step
01 Fix variables and assumptions L1–7 Work with arbitrary variables or the premises of the current implication.
L1 intro n
L2 intro p
L3 intro C
L4 intro hprime
L5 intro hlower
L6 intro hupper
L7 intro hcentral
02 Use earlier facts L8–13 Instantiate or apply named facts and discharge the corresponding proof obligations.
L8 specialize choose_prime_divides_between (n + n)
L9 specialize choose_prime_divides_between n
L10 specialize choose_prime_divides_between n
L11 specialize choose_prime_divides_between p
L12 specialize choose_prime_divides_between C
L13 apply choose_prime_divides_between
03 Calculate and transport equalities L14–14 Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
L14 refl
04 Use earlier facts L15–22 Instantiate or apply named facts and discharge the corresponding proof obligations.
L15 exact hprime
L16 exact hlower
L17 exact hlower
L18 specialize lt_to_le p
L19 specialize lt_to_le (n + n)
L20 apply lt_to_le
L21 exact hupper
L22 exact hcentral
Library-wide reading audit
Original defined command ledger · 22 lines 0001 intro n0002 intro p0003 intro C0004 intro hprime0005 intro hlower0006 intro hupper0007 intro hcentral0008 specialize choose_prime_divides_between (n + n)0009 specialize choose_prime_divides_between n0010 specialize choose_prime_divides_between n0011 specialize choose_prime_divides_between p0012 specialize choose_prime_divides_between C0013 apply choose_prime_divides_between0014 refl0015 exact hprime0016 exact hlower0017 exact hlower0018 specialize lt_to_le p0019 specialize lt_to_le (n + n)0020 apply lt_to_le0021 exact hupper0022 exact hcentral