BP000B

bertrand_chain_prefix_extend

Appending a strict Bertrand successor recodes and preserves every prior chain edge.

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. ∀ b. ∀ c. ∀ a. ∀ p. BertrandChain(b,c,n,k) → Beta(b,c,k,a) → BertrandWindow(a,p) → ∃ x. ∃ y. BertrandChain(x,y,n,S k) ∧ Beta(x,y,S k,p)

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

Definition DAG

Beta(b,c,i,x) · 2BertrandWindow(n,p) · 1BertrandChain(b,c,n,k) · 2

Actual proof prerequisites

beta_prefix_extend · checked external prerequisitezero_le · checked external prerequisitesucc_le_succ · checked external prerequisitele_refl · checked external prerequisitefinite_lt_succ_eq_or_lt · checked external prerequisite
Original expanded first-order statement 
forall n k b c a p. (((((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))) -> ((((~(p = 1) /\ forall frm_prime_left_bpc_next_prime frm_prime_right_bpc_next_prime. p = frm_prime_left_bpc_next_prime * frm_prime_right_bpc_next_prime -> frm_prime_left_bpc_next_prime = 1 \/ frm_prime_right_bpc_next_prime = 1)) /\ ((exists bcf_lt_gap_bpc_next_lower. bcf_lt_gap_bpc_next_lower + S (a) = p) /\ (exists bcf_lt_gap_bpc_next_upper. bcf_lt_gap_bpc_next_upper + S (p) = a + a)))) -> exists z d. ((((((exists bcf_height_bpc_successor_start. bcf_height_bpc_successor_start + S (n) = S ((S (0)) * d)) /\ exists bcf_quotient_bpc_successor_start. z = bcf_quotient_bpc_successor_start * S ((S (0)) * d) + (n))) /\ forall bcf_index_bpc_successor_chain. (exists bcf_lt_gap_bpc_successor_index. bcf_lt_gap_bpc_successor_index + S (bcf_index_bpc_successor_chain) = S k) -> exists bcf_previous_bpc_successor_chain bcf_following_bpc_successor_chain. ((((exists bcf_height_bpc_successor_previous. bcf_height_bpc_successor_previous + S (bcf_previous_bpc_successor_chain) = S ((S (bcf_index_bpc_successor_chain)) * d)) /\ exists bcf_quotient_bpc_successor_previous. z = bcf_quotient_bpc_successor_previous * S ((S (bcf_index_bpc_successor_chain)) * d) + (bcf_previous_bpc_successor_chain))) /\ ((((exists bcf_height_bpc_successor_following. bcf_height_bpc_successor_following + S (bcf_following_bpc_successor_chain) = S ((S (S bcf_index_bpc_successor_chain)) * d)) /\ exists bcf_quotient_bpc_successor_following. z = bcf_quotient_bpc_successor_following * S ((S (S bcf_index_bpc_successor_chain)) * d) + (bcf_following_bpc_successor_chain))) /\ ((((~(bcf_following_bpc_successor_chain = 1) /\ forall frm_prime_left_bpc_successor_successor_prime frm_prime_right_bpc_successor_successor_prime. bcf_following_bpc_successor_chain = frm_prime_left_bpc_successor_successor_prime * frm_prime_right_bpc_successor_successor_prime -> frm_prime_left_bpc_successor_successor_prime = 1 \/ frm_prime_right_bpc_successor_successor_prime = 1)) /\ ((exists bcf_lt_gap_bpc_successor_successor_lower. bcf_lt_gap_bpc_successor_successor_lower + S (bcf_previous_bpc_successor_chain) = bcf_following_bpc_successor_chain) /\ (exists bcf_lt_gap_bpc_successor_successor_upper. bcf_lt_gap_bpc_successor_successor_upper + S (bcf_following_bpc_successor_chain) = bcf_previous_bpc_successor_chain + bcf_previous_bpc_successor_chain)))))))) /\ (((exists bcf_height_bpc_successor_terminal. bcf_height_bpc_successor_terminal + S (p) = S ((S (S k)) * d)) /\ exists bcf_quotient_bpc_successor_terminal. z = bcf_quotient_bpc_successor_terminal * S ((S (S k)) * d) + (p))))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

83 script commands · 24 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.

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

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

  1. L1
    intro n
  2. L2
    intro k
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro a
  6. L6
    intro p
  7. L7
    intro hchain
  8. L8
    intro hterminal
  9. L9
    intro hwindow
02Separate the logical casesL10–10

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

  1. L10
    cases hchain
03Establish hextensionL11–16

Establish this local claim before using it. It is not an additional assumption.

  1. L11
    have hextension : ∃ z. ∃ d. Beta(z,d,S k,p) ∧ (∀ x. ∀ y. Lt(x,S k) → Beta(b,c,x,y) → Beta(z,d,x,y))Definitions: BetaLtOriginal native command in the exact edition
  2. L12
    specialize beta_prefix_extend (S k)
  3. L13
    specialize beta_prefix_extend b
  4. L14
    specialize beta_prefix_extend c
  5. L15
    specialize beta_prefix_extend p
  6. L16
    exact beta_prefix_extend
04Separate the logical casesL17–19

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

  1. L17
    cases hextension
  2. L18
    cases hextension_witness
  3. L19
    cases hextension_witness_witness
05Construct an explicit witnessL20–21

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

  1. L20
    exists x
  2. L21
    exists x1
06Separate the logical casesL22–23

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

  1. L22
    split
  2. L23
    split
07Use earlier factsL24–32

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

  1. L24
    specialize hextension_witness_witness_right 0
  2. L25
    specialize hextension_witness_witness_right n
  3. L26
    apply hextension_witness_witness_right
  4. L27
    specialize succ_le_succ 0
  5. L28
    specialize succ_le_succ k
  6. L29
    apply succ_le_succ
  7. L30
    specialize zero_le k
  8. L31
    exact zero_le
  9. L32
    exact hchain_left
08Fix variables and assumptionsL33–34

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

  1. L33
    intro i
  2. L34
    intro hbound
09Establish hsplitL35–39

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L35
    have hsplit : i = k \/ exists gap. gap + S i = k
  2. L36
    specialize finite_lt_succ_eq_or_lt k
  3. L37
    specialize finite_lt_succ_eq_or_lt i
  4. L38
    apply finite_lt_succ_eq_or_lt
  5. L39
    exact hbound
10Separate the logical casesL40–40

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

  1. L40
    cases hsplit
11Construct an explicit witnessL41–42

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

  1. L41
    exists a
  2. L42
    exists p
12Separate the logical casesL43–43

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

  1. L43
    split
13Calculate and transport equalitiesL44–45

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

  1. L44
    rewrite hsplit_left
  2. L45
    rewrite hsplit_left
14Use earlier factsL46–51

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

  1. L46
    specialize hextension_witness_witness_right k
  2. L47
    specialize hextension_witness_witness_right a
  3. L48
    apply hextension_witness_witness_right
  4. L49
    specialize le_refl (S k)
  5. L50
    exact le_refl
  6. L51
    exact hterminal
15Separate the logical casesL52–52

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

  1. L52
    split
16Calculate and transport equalitiesL53–54

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

  1. L53
    rewrite hsplit_left
  2. L54
    rewrite hsplit_left
17Use earlier factsL55–56

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

  1. L55
    exact hextension_witness_witness_left
  2. L56
    exact hwindow
18Establish holdL57–60

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

  1. L57
    have hold : ∃ u. ∃ v. Beta(b,c,i,u) ∧ (Beta(b,c,S i,v) ∧ BertrandWindow(u,v))Definitions: BetaBertrandWindowOriginal native command in the exact edition
  2. L58
    specialize hchain_right i
  3. L59
    apply hchain_right
  4. L60
    exact hsplit_right
19Separate the logical casesL61–64

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

  1. L61
    cases hold
  2. L62
    cases hold_witness
  3. L63
    cases hold_witness_witness
  4. L64
    cases hold_witness_witness_right
20Construct an explicit witnessL65–66

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

  1. L65
    exists x2
  2. L66
    exists x3
21Separate the logical casesL67–67

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

  1. L67
    split
22Use earlier factsL68–72

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

  1. L68
    specialize hextension_witness_witness_right i
  2. L69
    specialize hextension_witness_witness_right x2
  3. L70
    apply hextension_witness_witness_right
  4. L71
    exact hbound
  5. L72
    exact hold_witness_witness_left
23Separate the logical casesL73–73

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

  1. L73
    split
24Use earlier factsL74–83

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

  1. L74
    specialize hextension_witness_witness_right (S i)
  2. L75
    specialize hextension_witness_witness_right x3
  3. L76
    apply hextension_witness_witness_right
  4. L77
    specialize succ_le_succ (S i)
  5. L78
    specialize succ_le_succ k
  6. L79
    apply succ_le_succ
  7. L80
    exact hsplit_right
  8. L81
    exact hold_witness_witness_right_left
  9. L82
    exact hold_witness_witness_right_right
  10. L83
    exact hextension_witness_witness_left

Library-wide reading audit

Original defined command ledger · 83 lines
  1. 0001intro n
  2. 0002intro k
  3. 0003intro b
  4. 0004intro c
  5. 0005intro a
  6. 0006intro p
  7. 0007intro hchain
  8. 0008intro hterminal
  9. 0009intro hwindow
  10. 0010cases hchain
  11. 0011have hextension : exists z d. ((((exists bcf_height_bpc_successor_terminal. bcf_height_bpc_successor_terminal + S (p) = S ((S (S k)) * d)) /\ exists bcf_quotient_bpc_successor_terminal. z = bcf_quotient_bpc_successor_terminal * S ((S (S k)) * d) + (p))) /\ forall i v. (exists bcf_lt_gap_bpc_transport_bound. bcf_lt_gap_bpc_transport_bound + S (i) = S k) -> (((exists bcf_height_bpc_transport_old. bcf_height_bpc_transport_old + S (v) = S ((S (i)) * c)) /\ exists bcf_quotient_bpc_transport_old. b = bcf_quotient_bpc_transport_old * S ((S (i)) * c) + (v))) -> (((exists bcf_height_bpc_transport_new. bcf_height_bpc_transport_new + S (v) = S ((S (i)) * d)) /\ exists bcf_quotient_bpc_transport_new. z = bcf_quotient_bpc_transport_new * S ((S (i)) * d) + (v))))
  12. 0012specialize beta_prefix_extend (S k)
  13. 0013specialize beta_prefix_extend b
  14. 0014specialize beta_prefix_extend c
  15. 0015specialize beta_prefix_extend p
  16. 0016exact beta_prefix_extend
  17. 0017cases hextension
  18. 0018cases hextension_witness
  19. 0019cases hextension_witness_witness
  20. 0020exists x
  21. 0021exists x1
  22. 0022split
  23. 0023split
  24. 0024specialize hextension_witness_witness_right 0
  25. 0025specialize hextension_witness_witness_right n
  26. 0026apply hextension_witness_witness_right
  27. 0027specialize succ_le_succ 0
  28. 0028specialize succ_le_succ k
  29. 0029apply succ_le_succ
  30. 0030specialize zero_le k
  31. 0031exact zero_le
  32. 0032exact hchain_left
  33. 0033intro i
  34. 0034intro hbound
  35. 0035have hsplit : i = k \/ exists gap. gap + S i = k
  36. 0036specialize finite_lt_succ_eq_or_lt k
  37. 0037specialize finite_lt_succ_eq_or_lt i
  38. 0038apply finite_lt_succ_eq_or_lt
  39. 0039exact hbound
  40. 0040cases hsplit
  41. 0041exists a
  42. 0042exists p
  43. 0043split
  44. 0044rewrite hsplit_left
  45. 0045rewrite hsplit_left
  46. 0046specialize hextension_witness_witness_right k
  47. 0047specialize hextension_witness_witness_right a
  48. 0048apply hextension_witness_witness_right
  49. 0049specialize le_refl (S k)
  50. 0050exact le_refl
  51. 0051exact hterminal
  52. 0052split
  53. 0053rewrite hsplit_left
  54. 0054rewrite hsplit_left
  55. 0055exact hextension_witness_witness_left
  56. 0056exact hwindow
  57. 0057have hold : exists u v. ((((exists bcf_height_bpc_step_old. bcf_height_bpc_step_old + S (u) = S ((S (i)) * c)) /\ exists bcf_quotient_bpc_step_old. b = bcf_quotient_bpc_step_old * S ((S (i)) * c) + (u))) /\ ((((exists bcf_height_bpc_step_next. bcf_height_bpc_step_next + S (v) = S ((S (S i)) * c)) /\ exists bcf_quotient_bpc_step_next. b = bcf_quotient_bpc_step_next * S ((S (S i)) * c) + (v))) /\ ((((~(v = 1) /\ forall frm_prime_left_bpc_old_step_prime frm_prime_right_bpc_old_step_prime. v = frm_prime_left_bpc_old_step_prime * frm_prime_right_bpc_old_step_prime -> frm_prime_left_bpc_old_step_prime = 1 \/ frm_prime_right_bpc_old_step_prime = 1)) /\ ((exists bcf_lt_gap_bpc_old_step_lower. bcf_lt_gap_bpc_old_step_lower + S (u) = v) /\ (exists bcf_lt_gap_bpc_old_step_upper. bcf_lt_gap_bpc_old_step_upper + S (v) = u + u))))))
  58. 0058specialize hchain_right i
  59. 0059apply hchain_right
  60. 0060exact hsplit_right
  61. 0061cases hold
  62. 0062cases hold_witness
  63. 0063cases hold_witness_witness
  64. 0064cases hold_witness_witness_right
  65. 0065exists x2
  66. 0066exists x3
  67. 0067split
  68. 0068specialize hextension_witness_witness_right i
  69. 0069specialize hextension_witness_witness_right x2
  70. 0070apply hextension_witness_witness_right
  71. 0071exact hbound
  72. 0072exact hold_witness_witness_left
  73. 0073split
  74. 0074specialize hextension_witness_witness_right (S i)
  75. 0075specialize hextension_witness_witness_right x3
  76. 0076apply hextension_witness_witness_right
  77. 0077specialize succ_le_succ (S i)
  78. 0078specialize succ_le_succ k
  79. 0079apply succ_le_succ
  80. 0080exact hsplit_right
  81. 0081exact hold_witness_witness_right_left
  82. 0082exact hold_witness_witness_right_right
  83. 0083exact hextension_witness_witness_left