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 expanded first-order arithmetic statement
forall n k. (exists bcf_lt_gap_bpc_chain_initial. bcf_lt_gap_bpc_chain_initial + S (1) = n) -> exists b c. (((((exists bcf_height_bpc_old_start. bcf_height_bpc_old_start + S (n) = S ((S (0)) * c)) /\ exists bcf_quotient_bpc_old_start. b = bcf_quotient_bpc_old_start * S ((S (0)) * c) + (n))) /\ forall bcf_index_bpc_old_chain. (exists bcf_lt_gap_bpc_old_index. bcf_lt_gap_bpc_old_index + S (bcf_index_bpc_old_chain) = k) -> exists bcf_previous_bpc_old_chain bcf_following_bpc_old_chain. ((((exists bcf_height_bpc_old_previous. bcf_height_bpc_old_previous + S (bcf_previous_bpc_old_chain) = S ((S (bcf_index_bpc_old_chain)) * c)) /\ exists bcf_quotient_bpc_old_previous. b = bcf_quotient_bpc_old_previous * S ((S (bcf_index_bpc_old_chain)) * c) + (bcf_previous_bpc_old_chain))) /\ ((((exists bcf_height_bpc_old_following. bcf_height_bpc_old_following + S (bcf_following_bpc_old_chain) = S ((S (S bcf_index_bpc_old_chain)) * c)) /\ exists bcf_quotient_bpc_old_following. b = bcf_quotient_bpc_old_following * S ((S (S bcf_index_bpc_old_chain)) * c) + (bcf_following_bpc_old_chain))) /\ ((((~(bcf_following_bpc_old_chain = 1) /\ forall frm_prime_left_bpc_old_successor_prime frm_prime_right_bpc_old_successor_prime. bcf_following_bpc_old_chain = frm_prime_left_bpc_old_successor_prime * frm_prime_right_bpc_old_successor_prime -> frm_prime_left_bpc_old_successor_prime = 1 \/ frm_prime_right_bpc_old_successor_prime = 1)) /\ ((exists bcf_lt_gap_bpc_old_successor_lower. bcf_lt_gap_bpc_old_successor_lower + S (bcf_previous_bpc_old_chain) = bcf_following_bpc_old_chain) /\ (exists bcf_lt_gap_bpc_old_successor_upper. bcf_lt_gap_bpc_old_successor_upper + S (bcf_following_bpc_old_chain) = bcf_previous_bpc_old_chain + bcf_previous_bpc_old_chain))))))))Constructive proof overview
Generated structural guide
Every n>1 and finite k admit an exact beta-coded chain of k strict Bertrand primes.
The unchanged tactic script uses 1 declared prerequisite and contains 15 exact native proof lines.
Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
Direct dependents
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.
Read the argument
Proof checkpoints
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.
Named ingredients (1)
01Fix variables and assumptionsL1–3
02Use earlier factsL4–5
03Establish hwitnessL6–8
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bertrand chain prefix terminal exists.
04Separate the logical casesL9–12
05Construct an explicit witnessL13–14
06Use earlier factsL15–15
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L15
exact hwitness_witness_witness_witness_left
Original exact command ledger · 15 lines
- 0001
intro n - 0002
intro k - 0003
intro hguard - 0004
specialize bertrand_chain_prefix_terminal_exists n - 0005
specialize bertrand_chain_prefix_terminal_exists k - 0006
have hwitness : exists b c a. ((((((exists bcf_height_bpc_old_start. bcf_height_bpc_old_start + S (n) = S ((S (0)) * c)) /\ exists bcf_quotient_bpc_old_start. b = bcf_quotient_bpc_old_start * S ((S (0)) * c) + (n))) /\ forall bcf_index_bpc_old_chain. (exists bcf_lt_gap_bpc_old_index. bcf_lt_gap_bpc_old_index + S (bcf_index_bpc_old_chain) = k) -> exists bcf_previous_bpc_old_chain bcf_following_bpc_old_chain. ((((exists bcf_height_bpc_old_previous. bcf_height_bpc_old_previous + S (bcf_previous_bpc_old_chain) = S ((S (bcf_index_bpc_old_chain)) * c)) /\ exists bcf_quotient_bpc_old_previous. b = bcf_quotient_bpc_old_previous * S ((S (bcf_index_bpc_old_chain)) * c) + (bcf_previous_bpc_old_chain))) /\ ((((exists bcf_height_bpc_old_following. bcf_height_bpc_old_following + S (bcf_following_bpc_old_chain) = S ((S (S bcf_index_bpc_old_chain)) * c)) /\ exists bcf_quotient_bpc_old_following. b = bcf_quotient_bpc_old_following * S ((S (S bcf_index_bpc_old_chain)) * c) + (bcf_following_bpc_old_chain))) /\ ((((~(bcf_following_bpc_old_chain = 1) /\ forall frm_prime_left_bpc_old_successor_prime frm_prime_right_bpc_old_successor_prime. bcf_following_bpc_old_chain = frm_prime_left_bpc_old_successor_prime * frm_prime_right_bpc_old_successor_prime -> frm_prime_left_bpc_old_successor_prime = 1 \/ frm_prime_right_bpc_old_successor_prime = 1)) /\ ((exists bcf_lt_gap_bpc_old_successor_lower. bcf_lt_gap_bpc_old_successor_lower + S (bcf_previous_bpc_old_chain) = bcf_following_bpc_old_chain) /\ (exists bcf_lt_gap_bpc_old_successor_upper. bcf_lt_gap_bpc_old_successor_upper + S (bcf_following_bpc_old_chain) = bcf_previous_bpc_old_chain + bcf_previous_bpc_old_chain)))))))) /\ ((((exists bcf_height_bpc_old_terminal. bcf_height_bpc_old_terminal + S (a) = S ((S (k)) * c)) /\ exists bcf_quotient_bpc_old_terminal. b = bcf_quotient_bpc_old_terminal * S ((S (k)) * c) + (a))) /\ (exists bcf_lt_gap_bpc_chain_terminal. bcf_lt_gap_bpc_chain_terminal + S (1) = a))) - 0007
apply bertrand_chain_prefix_terminal_exists - 0008
exact hguard - 0009
cases hwitness - 0010
cases hwitness_witness - 0011
cases hwitness_witness_witness - 0012
cases hwitness_witness_witness_witness - 0013
exists x - 0014
exists x1 - 0015
exact hwitness_witness_witness_witness_left