BP000D

iterated_bertrand_prime_chain_exists

Every n>1 and finite k admit an exact beta-coded chain of k strict Bertrand primes.

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. ∀ k. Lt(1,n) → ∃ x. ∃ y. BertrandChain(x,y,n,k)

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

Definition DAG

BertrandChain(b,c,n,k) · 1Lt(a,b) · 1

Actual proof prerequisites

bertrand_chain_prefix_terminal_exists
Original expanded first-order 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))))))))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

15 script commands · 6 reading checkpoints · 1 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 chain prefix terminal exists

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–3

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

  1. L1
    intro n
  2. L2
    intro k
  3. L3
    intro hguard
02Use earlier factsL4–5

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

  1. L4
    specialize bertrand_chain_prefix_terminal_exists n
  2. L5
    specialize bertrand_chain_prefix_terminal_exists k
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.

  1. L6
    have hwitness : ∃ b. ∃ c. ∃ a. BertrandChain(b,c,n,k) ∧ (Beta(b,c,k,a) ∧ Lt(1,a))Definitions: BetaBertrandChainLtOriginal native command in the exact edition
  2. L7
    apply bertrand_chain_prefix_terminal_exists
  3. L8
    exact hguard
04Separate the logical casesL9–12

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

  1. L9
    cases hwitness
  2. L10
    cases hwitness_witness
  3. L11
    cases hwitness_witness_witness
  4. L12
    cases hwitness_witness_witness_witness
05Construct an explicit witnessL13–14

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

  1. L13
    exists x
  2. L14
    exists x1
06Use earlier factsL15–15

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

  1. L15
    exact hwitness_witness_witness_witness_left

Library-wide reading audit

Original defined command ledger · 15 lines
  1. 0001intro n
  2. 0002intro k
  3. 0003intro hguard
  4. 0004specialize bertrand_chain_prefix_terminal_exists n
  5. 0005specialize bertrand_chain_prefix_terminal_exists k
  6. 0006have 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)))
  7. 0007apply bertrand_chain_prefix_terminal_exists
  8. 0008exact hguard
  9. 0009cases hwitness
  10. 0010cases hwitness_witness
  11. 0011cases hwitness_witness_witness
  12. 0012cases hwitness_witness_witness_witness
  13. 0013exists x
  14. 0014exists x1
  15. 0015exact hwitness_witness_witness_witness_left