BP000C

bertrand_chain_prefix_terminal_exists

Induction constructs arbitrary strict prime chains and their guarded terminal values.

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

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

Definition DAG

Beta(b,c,i,x) · 1BertrandChain(b,c,n,k) · 1Lt(a,b) · 2

Actual proof prerequisites

bertrand_chain_singleton_existsbertrand_strict · checked external prerequisitebertrand_chain_prefix_extendbertrand_chain_successor_preserves_guard
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 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)))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

55 script commands · 21 reading checkpoints · 3 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 (3)
bertrand chain singleton existsbertrand chain prefix extendbertrand chain successor preserves guard

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

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

  1. L1
    intro n
02Induction on kL2–4

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L2
    induction k
  2. L3
    intro hguard
  3. L4
    specialize bertrand_chain_singleton_exists n
03Separate the logical casesL5–6

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

  1. L5
    cases bertrand_chain_singleton_exists
  2. L6
    cases bertrand_chain_singleton_exists_witness
04Construct an explicit witnessL7–9

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

  1. L7
    exists x
  2. L8
    exists x1
  3. L9
    exists n
05Separate the logical casesL10–10

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

  1. L10
    split
06Use earlier factsL11–11

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

  1. L11
    exact bertrand_chain_singleton_exists_witness_witness
07Separate the logical casesL12–13

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

  1. L12
    split
  2. L13
    cases bertrand_chain_singleton_exists_witness_witness
08Use earlier factsL14–15

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

  1. L14
    exact bertrand_chain_singleton_exists_witness_witness_left
  2. L15
    exact hguard
09Fix variables and assumptionsL16–16

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

  1. L16
    intro hguard
10Establish hpreviousL17–19

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

  1. L17
    have hprevious : ∃ 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. L18
    apply IH
  3. L19
    exact hguard
11Separate the logical casesL20–24

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

  1. L20
    cases hprevious
  2. L21
    cases hprevious_witness
  3. L22
    cases hprevious_witness_witness
  4. L23
    cases hprevious_witness_witness_witness
  5. L24
    cases hprevious_witness_witness_witness_right
12Establish hnextL25–28

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

  1. L25
    have hnext : exists p. ((((~(p = 1) /\ forall frm_prime_left_bpc_induction_next_prime frm_prime_right_bpc_induction_next_prime. p = frm_prime_left_bpc_induction_next_prime * frm_prime_right_bpc_induction_next_prime -> frm_prime_left_bpc_induction_next_prime = 1 \/ frm_prime_right_bpc_induction_next_prime = 1)) /\ ((exists bcf_lt_gap_bpc_induction_next_lower. bcf_lt_gap_bpc_induction_next_lower + S (x2) = p) /\ (exists bcf_lt_gap_bpc_induction_next_upper. bcf_lt_gap_bpc_induction_next_upper + S (p) = x2 + x2))))
  2. L26
    specialize bertrand_strict x2
  3. L27
    apply bertrand_strict
  4. L28
    exact hprevious_witness_witness_witness_right_right
13Separate the logical casesL29–29

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

  1. L29
    cases hnext
14Establish hextendedL30–39

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

  1. L30
    have hextended : ∃ z. ∃ d. BertrandChain(z,d,n,S k) ∧ Beta(z,d,S k,x3)Definitions: BetaBertrandChainOriginal native command in the exact edition
  2. L31
    specialize bertrand_chain_prefix_extend n
  3. L32
    specialize bertrand_chain_prefix_extend k
  4. L33
    specialize bertrand_chain_prefix_extend x
  5. L34
    specialize bertrand_chain_prefix_extend x1
  6. L35
    specialize bertrand_chain_prefix_extend x2
  7. L36
    specialize bertrand_chain_prefix_extend x3
  8. L37
    apply bertrand_chain_prefix_extend
  9. L38
    exact hprevious_witness_witness_witness_left
  10. L39
    exact hprevious_witness_witness_witness_right_left
15Use earlier factsL40–40

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

  1. L40
    exact hnext_witness
16Separate the logical casesL41–43

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

  1. L41
    cases hextended
  2. L42
    cases hextended_witness
  3. L43
    cases hextended_witness_witness
17Construct an explicit witnessL44–46

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

  1. L44
    exists x4
  2. L45
    exists x5
  3. L46
    exists x3
18Separate the logical casesL47–47

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

  1. L47
    split
19Use earlier factsL48–48

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

  1. L48
    exact hextended_witness_witness_left
20Separate the logical casesL49–49

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

  1. L49
    split
21Use earlier factsL50–55

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

  1. L50
    exact hextended_witness_witness_right
  2. L51
    specialize bertrand_chain_successor_preserves_guard x2
  3. L52
    specialize bertrand_chain_successor_preserves_guard x3
  4. L53
    apply bertrand_chain_successor_preserves_guard
  5. L54
    exact hprevious_witness_witness_witness_right_right
  6. L55
    exact hnext_witness

Library-wide reading audit

Original defined command ledger · 55 lines
  1. 0001intro n
  2. 0002induction k
  3. 0003intro hguard
  4. 0004specialize bertrand_chain_singleton_exists n
  5. 0005cases bertrand_chain_singleton_exists
  6. 0006cases bertrand_chain_singleton_exists_witness
  7. 0007exists x
  8. 0008exists x1
  9. 0009exists n
  10. 0010split
  11. 0011exact bertrand_chain_singleton_exists_witness_witness
  12. 0012split
  13. 0013cases bertrand_chain_singleton_exists_witness_witness
  14. 0014exact bertrand_chain_singleton_exists_witness_witness_left
  15. 0015exact hguard
  16. 0016intro hguard
  17. 0017have hprevious : 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)))
  18. 0018apply IH
  19. 0019exact hguard
  20. 0020cases hprevious
  21. 0021cases hprevious_witness
  22. 0022cases hprevious_witness_witness
  23. 0023cases hprevious_witness_witness_witness
  24. 0024cases hprevious_witness_witness_witness_right
  25. 0025have hnext : exists p. ((((~(p = 1) /\ forall frm_prime_left_bpc_induction_next_prime frm_prime_right_bpc_induction_next_prime. p = frm_prime_left_bpc_induction_next_prime * frm_prime_right_bpc_induction_next_prime -> frm_prime_left_bpc_induction_next_prime = 1 \/ frm_prime_right_bpc_induction_next_prime = 1)) /\ ((exists bcf_lt_gap_bpc_induction_next_lower. bcf_lt_gap_bpc_induction_next_lower + S (x2) = p) /\ (exists bcf_lt_gap_bpc_induction_next_upper. bcf_lt_gap_bpc_induction_next_upper + S (p) = x2 + x2))))
  26. 0026specialize bertrand_strict x2
  27. 0027apply bertrand_strict
  28. 0028exact hprevious_witness_witness_witness_right_right
  29. 0029cases hnext
  30. 0030have hextended : exists z d. ((((((exists bcf_height_bpc_induction_new_start. bcf_height_bpc_induction_new_start + S (n) = S ((S (0)) * d)) /\ exists bcf_quotient_bpc_induction_new_start. z = bcf_quotient_bpc_induction_new_start * S ((S (0)) * d) + (n))) /\ forall bcf_index_bpc_induction_new_chain. (exists bcf_lt_gap_bpc_induction_new_index. bcf_lt_gap_bpc_induction_new_index + S (bcf_index_bpc_induction_new_chain) = S k) -> exists bcf_previous_bpc_induction_new_chain bcf_following_bpc_induction_new_chain. ((((exists bcf_height_bpc_induction_new_previous. bcf_height_bpc_induction_new_previous + S (bcf_previous_bpc_induction_new_chain) = S ((S (bcf_index_bpc_induction_new_chain)) * d)) /\ exists bcf_quotient_bpc_induction_new_previous. z = bcf_quotient_bpc_induction_new_previous * S ((S (bcf_index_bpc_induction_new_chain)) * d) + (bcf_previous_bpc_induction_new_chain))) /\ ((((exists bcf_height_bpc_induction_new_following. bcf_height_bpc_induction_new_following + S (bcf_following_bpc_induction_new_chain) = S ((S (S bcf_index_bpc_induction_new_chain)) * d)) /\ exists bcf_quotient_bpc_induction_new_following. z = bcf_quotient_bpc_induction_new_following * S ((S (S bcf_index_bpc_induction_new_chain)) * d) + (bcf_following_bpc_induction_new_chain))) /\ ((((~(bcf_following_bpc_induction_new_chain = 1) /\ forall frm_prime_left_bpc_induction_new_successor_prime frm_prime_right_bpc_induction_new_successor_prime. bcf_following_bpc_induction_new_chain = frm_prime_left_bpc_induction_new_successor_prime * frm_prime_right_bpc_induction_new_successor_prime -> frm_prime_left_bpc_induction_new_successor_prime = 1 \/ frm_prime_right_bpc_induction_new_successor_prime = 1)) /\ ((exists bcf_lt_gap_bpc_induction_new_successor_lower. bcf_lt_gap_bpc_induction_new_successor_lower + S (bcf_previous_bpc_induction_new_chain) = bcf_following_bpc_induction_new_chain) /\ (exists bcf_lt_gap_bpc_induction_new_successor_upper. bcf_lt_gap_bpc_induction_new_successor_upper + S (bcf_following_bpc_induction_new_chain) = bcf_previous_bpc_induction_new_chain + bcf_previous_bpc_induction_new_chain)))))))) /\ (((exists bcf_height_bpc_induction_terminal. bcf_height_bpc_induction_terminal + S (x3) = S ((S (S k)) * d)) /\ exists bcf_quotient_bpc_induction_terminal. z = bcf_quotient_bpc_induction_terminal * S ((S (S k)) * d) + (x3))))
  31. 0031specialize bertrand_chain_prefix_extend n
  32. 0032specialize bertrand_chain_prefix_extend k
  33. 0033specialize bertrand_chain_prefix_extend x
  34. 0034specialize bertrand_chain_prefix_extend x1
  35. 0035specialize bertrand_chain_prefix_extend x2
  36. 0036specialize bertrand_chain_prefix_extend x3
  37. 0037apply bertrand_chain_prefix_extend
  38. 0038exact hprevious_witness_witness_witness_left
  39. 0039exact hprevious_witness_witness_witness_right_left
  40. 0040exact hnext_witness
  41. 0041cases hextended
  42. 0042cases hextended_witness
  43. 0043cases hextended_witness_witness
  44. 0044exists x4
  45. 0045exists x5
  46. 0046exists x3
  47. 0047split
  48. 0048exact hextended_witness_witness_left
  49. 0049split
  50. 0050exact hextended_witness_witness_right
  51. 0051specialize bertrand_chain_successor_preserves_guard x2
  52. 0052specialize bertrand_chain_successor_preserves_guard x3
  53. 0053apply bertrand_chain_successor_preserves_guard
  54. 0054exact hprevious_witness_witness_witness_right_right
  55. 0055exact hnext_witness