BT005E · Bertrand theorem

beta_prefix_product_trace_exists

Stable checked-use theorem · independently kernel verified

Every decoded beta factor prefix admits a beta-coded exact prefix-product trace.

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.

Statement with defined notation

∀ b. ∀ c. ∀ l. ∃ u. ∃ v. BetaAt(u,v,0,1) ∧ (∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ n. BetaAt(b,c,x,y) ∧ (BetaAt(u,v,x,z) ∧ (BetaAt(u,v,S x,n) ∧ n = z · y)))

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0013 BetaAt

5 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0013 BetaAt

18 occurrences

Exact expanded native-PA statement
forall b c l. exists u v. (((exists h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ forall i. (exists h. h + S i = l) -> exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * v)) /\ exists q. u = q * S ((S i) * v) + r) /\ (((exists h. h + S s = S ((S (S i)) * v)) /\ exists q. u = q * S ((S (S i)) * v) + s) /\ s = r * p))))

Proof neighborhood

Direct theorem prerequisites

BT0040 beta_at_self_of_bound BT000L add_eq_zero_right BT000C succ_ne_zero BT0041 beta_at_exists BT005D beta_prefix_extend BT000W zero_le BT0016 succ_le_succ BT000E le_refl BT0017 le_of_succ_le_succ BT001C le_eq_or_lt BT0009 one_mul

Direct theorem dependents

BT005F beta_product_exists

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

133 script commands · 47 reading checkpoints · 10 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 (11)
beta at self of boundadd eq zero rightsucc ne zerobeta at existsbeta prefix extendzero lesucc le succle reflle of succ le succle eq or ltone mul
01Fix variables and assumptionsL1–2

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

  1. L1
    intro b
  2. L2
    intro c
02Induction on lL3–3

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

  1. L3
    induction l
03Construct an explicit witnessL4–5

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

  1. L4
    exists 1
  2. L5
    exists 1
04Separate the logical casesL6–6

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

  1. L6
    split
05Use earlier factsL7–11

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

  1. L7
    specialize beta_at_self_of_bound 1
  2. L8
    specialize beta_at_self_of_bound 0
  3. L9
    specialize beta_at_self_of_bound 1
  4. L10
    apply beta_at_self_of_bound
  5. L11
    specialize one_mul 1
06Calculate and transport equalitiesL12–12

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

  1. L12
    rewrite one_mul
07Use earlier factsL13–14

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

  1. L13
    specialize le_refl 2
  2. L14
    exact le_refl
08Fix variables and assumptionsL15–16

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

  1. L15
    intro i
  2. L16
    intro hi
09Separate the logical casesL17–18

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

  1. L17
    exfalso
  2. L18
    cases hi
10Establish hsi0L19–26

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

  1. L19
    have hsi0 : S i = 0
  2. L20
    specialize add_eq_zero_right x
  3. L21
    specialize add_eq_zero_right (S i)
  4. L22
    apply add_eq_zero_right
  5. L23
    exact hi_witness
  6. L24
    specialize succ_ne_zero i
  7. L25
    apply succ_ne_zero
  8. L26
    exact hsi0
11Establish htraceL27–28

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

  1. L27
    have htrace : ∃ u. ∃ v. BetaAt(u,v,0,1) ∧ (∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ n. BetaAt(b,c,x,y) ∧ (BetaAt(u,v,x,z) ∧ (BetaAt(u,v,S x,n) ∧ n = z · y)))Definitions: BetaAt(u,v,0,1)Lt(x,l)BetaAt(b,c,x,y)BetaAt(u,v,x,z)BetaAt(u,v,S x,n)Original native command in the exact edition
  2. L28
    apply IH
12Separate the logical casesL29–31

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

  1. L29
    cases htrace
  2. L30
    cases htrace_witness
  3. L31
    cases htrace_witness_witness
13Establish hfactorL32–36

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

  1. L32
    have hfactor : ∃ p. BetaAt(b,c,l,p)Definitions: BetaAt(b,c,l,p)Original native command in the exact edition
  2. L33
    specialize beta_at_exists b
  3. L34
    specialize beta_at_exists c
  4. L35
    specialize beta_at_exists l
  5. L36
    exact beta_at_exists
14Separate the logical casesL37–37

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

  1. L37
    cases hfactor
15Establish hlastL38–42

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

  1. L38
    have hlast : ∃ r. BetaAt(x,x1,l,r)Definitions: BetaAt(x,x1,l,r)Original native command in the exact edition
  2. L39
    specialize beta_at_exists x
  3. L40
    specialize beta_at_exists x1
  4. L41
    specialize beta_at_exists l
  5. L42
    exact beta_at_exists
16Separate the logical casesL43–43

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

  1. L43
    cases hlast
17Establish hextL44–49

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

  1. L44
    have hext : ∃ z. ∃ v. BetaAt(z,v,S l,x3 · x2) ∧ (∀ y. ∀ n. Lt(y,S l) → BetaAt(x,x1,y,n) → BetaAt(z,v,y,n))Definitions: BetaAt(z,v,S l,x3 · x2)Lt(y,S l)BetaAt(x,x1,y,n)BetaAt(z,v,y,n)Original native command in the exact edition
  2. L45
    specialize beta_prefix_extend (S l)
  3. L46
    specialize beta_prefix_extend x
  4. L47
    specialize beta_prefix_extend x1
  5. L48
    specialize beta_prefix_extend (x3 * x2)
  6. L49
    exact beta_prefix_extend
18Separate the logical casesL50–52

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

  1. L50
    cases hext
  2. L51
    cases hext_witness
  3. L52
    cases hext_witness_witness
19Construct an explicit witnessL53–54

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

  1. L53
    exists x4
  2. L54
    exists x5
20Separate the logical casesL55–55

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

  1. L55
    split
21Use earlier factsL56–58

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

  1. L56
    specialize hext_witness_witness_right 0
  2. L57
    specialize hext_witness_witness_right 1
  3. L58
    apply hext_witness_witness_right
22Establish h0L59–59

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

  1. L59
23Establish hzeroL60–69

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

  1. L60
  2. L61
    specialize zero_le l
  3. L62
    exact zero_le
  4. L63
    specialize succ_le_succ 0
  5. L64
    specialize succ_le_succ l
  6. L65
    apply succ_le_succ
  7. L66
    exact hzero
  8. L67
    exact h0
  9. L68
    exact htrace_witness_witness_left
  10. L69
    intro i
24Fix variables and assumptionsL70–70

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

  1. L70
    intro hi
25Establish hilL71–75

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

  1. L71
  2. L72
    specialize le_of_succ_le_succ i
  3. L73
    specialize le_of_succ_le_succ l
  4. L74
    apply le_of_succ_le_succ
  5. L75
    exact hi
26Establish hsplitL76–80

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

  1. L76
    have hsplit : i = l ∨ Lt(i,l)Definitions: Lt(i,l)Original native command in the exact edition
  2. L77
    specialize le_eq_or_lt i
  3. L78
    specialize le_eq_or_lt l
  4. L79
    apply le_eq_or_lt
  5. L80
    exact hil
27Separate the logical casesL81–81

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

  1. L81
    cases hsplit
28Construct an explicit witnessL82–84

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

  1. L82
    exists x2
  2. L83
    exists x3
  3. L84
    exists x3 * x2
29Separate the logical casesL85–85

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

  1. L85
    split
30Calculate and transport equalitiesL86–87

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

  1. L86
    rewrite hsplit_left
  2. L87
    rewrite hsplit_left
31Use earlier factsL88–88

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

  1. L88
    exact hfactor_witness
32Separate the logical casesL89–89

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

  1. L89
    split
33Calculate and transport equalitiesL90–91

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

  1. L90
    rewrite hsplit_left
  2. L91
    rewrite hsplit_left
34Use earlier factsL92–97

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

  1. L92
    specialize hext_witness_witness_right l
  2. L93
    specialize hext_witness_witness_right x3
  3. L94
    apply hext_witness_witness_right
  4. L95
    specialize le_refl (S l)
  5. L96
    exact le_refl
  6. L97
    exact hlast_witness
35Separate the logical casesL98–98

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

  1. L98
    split
36Calculate and transport equalitiesL99–100

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

  1. L99
    rewrite hsplit_left
  2. L100
    rewrite hsplit_left
37Use earlier factsL101–101

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

  1. L101
    exact hext_witness_witness_left
38Calculate and transport equalitiesL102–102

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

  1. L102
    refl
39Establish holdL103–106

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

  1. L103
    have hold : ∃ p. ∃ r. ∃ s. BetaAt(b,c,i,p) ∧ (BetaAt(x,x1,i,r) ∧ (BetaAt(x,x1,S i,s) ∧ s = r · p))Definitions: BetaAt(b,c,i,p)BetaAt(x,x1,i,r)BetaAt(x,x1,S i,s)Original native command in the exact edition
  2. L104
    specialize htrace_witness_witness_right i
  3. L105
    apply htrace_witness_witness_right
  4. L106
    exact hsplit_right
40Separate the logical casesL107–112

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

  1. L107
    cases hold
  2. L108
    cases hold_witness
  3. L109
    cases hold_witness_witness
  4. L110
    cases hold_witness_witness_witness
  5. L111
    cases hold_witness_witness_witness_right
  6. L112
    cases hold_witness_witness_witness_right_right
41Construct an explicit witnessL113–115

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

  1. L113
    exists x6
  2. L114
    exists x7
  3. L115
    exists x8
42Separate the logical casesL116–116

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

  1. L116
    split
43Use earlier factsL117–117

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

  1. L117
    exact hold_witness_witness_witness_left
44Separate the logical casesL118–118

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

  1. L118
    split
45Use earlier factsL119–123

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

  1. L119
    specialize hext_witness_witness_right i
  2. L120
    specialize hext_witness_witness_right x7
  3. L121
    apply hext_witness_witness_right
  4. L122
    exact hi
  5. L123
    exact hold_witness_witness_witness_right_left
46Separate the logical casesL124–124

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

  1. L124
    split
47Use earlier factsL125–133

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

  1. L125
    specialize hext_witness_witness_right (S i)
  2. L126
    specialize hext_witness_witness_right x8
  3. L127
    apply hext_witness_witness_right
  4. L128
    specialize succ_le_succ (S i)
  5. L129
    specialize succ_le_succ l
  6. L130
    apply succ_le_succ
  7. L131
    exact hsplit_right
  8. L132
    exact hold_witness_witness_witness_right_right_left
  9. L133
    exact hold_witness_witness_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 133 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003induction l
  4. 0004exists 1
  5. 0005exists 1
  6. 0006split
  7. 0007specialize beta_at_self_of_bound 1
  8. 0008specialize beta_at_self_of_bound 0
  9. 0009specialize beta_at_self_of_bound 1
  10. 0010apply beta_at_self_of_bound
  11. 0011specialize one_mul 1
  12. 0012rewrite one_mul
  13. 0013specialize le_refl 2
  14. 0014exact le_refl
  15. 0015intro i
  16. 0016intro hi
  17. 0017exfalso
  18. 0018cases hi
  19. 0019have hsi0 : S i = 0
  20. 0020specialize add_eq_zero_right x
  21. 0021specialize add_eq_zero_right (S i)
  22. 0022apply add_eq_zero_right
  23. 0023exact hi_witness
  24. 0024specialize succ_ne_zero i
  25. 0025apply succ_ne_zero
  26. 0026exact hsi0
  27. 0027have htrace : ∃ u. ∃ v. BetaAt(u,v,0,1) ∧ (∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ n. BetaAt(b,c,x,y) ∧ (BetaAt(u,v,x,z) ∧ (BetaAt(u,v,S x,n) ∧ n = z · y)))
    Exact native replay linehave htrace : exists u v. (((exists h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ forall i. (exists h. h + S i = l) -> exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * v)) /\ exists q. u = q * S ((S i) * v) + r) /\ (((exists h. h + S s = S ((S (S i)) * v)) /\ exists q. u = q * S ((S (S i)) * v) + s) /\ s = r * p))))
  28. 0028apply IH
  29. 0029cases htrace
  30. 0030cases htrace_witness
  31. 0031cases htrace_witness_witness
  32. 0032have hfactor : ∃ p. BetaAt(b,c,l,p)
    Exact native replay linehave hfactor : exists p. ((exists h. h + S p = S ((S l) * c)) /\ exists q. b = q * S ((S l) * c) + p)
  33. 0033specialize beta_at_exists b
  34. 0034specialize beta_at_exists c
  35. 0035specialize beta_at_exists l
  36. 0036exact beta_at_exists
  37. 0037cases hfactor
  38. 0038have hlast : ∃ r. BetaAt(x,x1,l,r)
    Exact native replay linehave hlast : exists r. ((exists h. h + S r = S ((S l) * x1)) /\ exists q. x = q * S ((S l) * x1) + r)
  39. 0039specialize beta_at_exists x
  40. 0040specialize beta_at_exists x1
  41. 0041specialize beta_at_exists l
  42. 0042exact beta_at_exists
  43. 0043cases hlast
  44. 0044have hext : ∃ z. ∃ v. BetaAt(z,v,S l,x3 · x2) ∧ (∀ y. ∀ n. Lt(y,S l) → BetaAt(x,x1,y,n) → BetaAt(z,v,y,n))
    Exact native replay linehave hext : exists z v. (((exists h. h + S (x3 * x2) = S ((S (S l)) * v)) /\ exists q. z = q * S ((S (S l)) * v) + (x3 * x2)) /\ forall i a. (exists h. h + S i = S l) -> ((exists h. h + S a = S ((S i) * x1)) /\ exists q. x = q * S ((S i) * x1) + a) -> ((exists h. h + S a = S ((S i) * v)) /\ exists q. z = q * S ((S i) * v) + a))
  45. 0045specialize beta_prefix_extend (S l)
  46. 0046specialize beta_prefix_extend x
  47. 0047specialize beta_prefix_extend x1
  48. 0048specialize beta_prefix_extend (x3 * x2)
  49. 0049exact beta_prefix_extend
  50. 0050cases hext
  51. 0051cases hext_witness
  52. 0052cases hext_witness_witness
  53. 0053exists x4
  54. 0054exists x5
  55. 0055split
  56. 0056specialize hext_witness_witness_right 0
  57. 0057specialize hext_witness_witness_right 1
  58. 0058apply hext_witness_witness_right
  59. 0059have h0 : Lt(0,S l)
    Exact native replay linehave h0 : exists h. h + S 0 = S l
  60. 0060have hzero : Le(0,l)
    Exact native replay linehave hzero : exists h. h + 0 = l
  61. 0061specialize zero_le l
  62. 0062exact zero_le
  63. 0063specialize succ_le_succ 0
  64. 0064specialize succ_le_succ l
  65. 0065apply succ_le_succ
  66. 0066exact hzero
  67. 0067exact h0
  68. 0068exact htrace_witness_witness_left
  69. 0069intro i
  70. 0070intro hi
  71. 0071have hil : Le(i,l)
    Exact native replay linehave hil : exists h. h + i = l
  72. 0072specialize le_of_succ_le_succ i
  73. 0073specialize le_of_succ_le_succ l
  74. 0074apply le_of_succ_le_succ
  75. 0075exact hi
  76. 0076have hsplit : i = l ∨ Lt(i,l)
    Exact native replay linehave hsplit : i = l \/ exists h. h + S i = l
  77. 0077specialize le_eq_or_lt i
  78. 0078specialize le_eq_or_lt l
  79. 0079apply le_eq_or_lt
  80. 0080exact hil
  81. 0081cases hsplit
  82. 0082exists x2
  83. 0083exists x3
  84. 0084exists x3 * x2
  85. 0085split
  86. 0086rewrite hsplit_left
  87. 0087rewrite hsplit_left
  88. 0088exact hfactor_witness
  89. 0089split
  90. 0090rewrite hsplit_left
  91. 0091rewrite hsplit_left
  92. 0092specialize hext_witness_witness_right l
  93. 0093specialize hext_witness_witness_right x3
  94. 0094apply hext_witness_witness_right
  95. 0095specialize le_refl (S l)
  96. 0096exact le_refl
  97. 0097exact hlast_witness
  98. 0098split
  99. 0099rewrite hsplit_left
  100. 0100rewrite hsplit_left
  101. 0101exact hext_witness_witness_left
  102. 0102refl
  103. 0103have hold : ∃ p. ∃ r. ∃ s. BetaAt(b,c,i,p) ∧ (BetaAt(x,x1,i,r) ∧ (BetaAt(x,x1,S i,s) ∧ s = r · p))
    Exact native replay linehave hold : exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * x1)) /\ exists q. x = q * S ((S i) * x1) + r) /\ (((exists h. h + S s = S ((S (S i)) * x1)) /\ exists q. x = q * S ((S (S i)) * x1) + s) /\ s = r * p)))
  104. 0104specialize htrace_witness_witness_right i
  105. 0105apply htrace_witness_witness_right
  106. 0106exact hsplit_right
  107. 0107cases hold
  108. 0108cases hold_witness
  109. 0109cases hold_witness_witness
  110. 0110cases hold_witness_witness_witness
  111. 0111cases hold_witness_witness_witness_right
  112. 0112cases hold_witness_witness_witness_right_right
  113. 0113exists x6
  114. 0114exists x7
  115. 0115exists x8
  116. 0116split
  117. 0117exact hold_witness_witness_witness_left
  118. 0118split
  119. 0119specialize hext_witness_witness_right i
  120. 0120specialize hext_witness_witness_right x7
  121. 0121apply hext_witness_witness_right
  122. 0122exact hi
  123. 0123exact hold_witness_witness_witness_right_left
  124. 0124split
  125. 0125specialize hext_witness_witness_right (S i)
  126. 0126specialize hext_witness_witness_right x8
  127. 0127apply hext_witness_witness_right
  128. 0128specialize succ_le_succ (S i)
  129. 0129specialize succ_le_succ l
  130. 0130apply succ_le_succ
  131. 0131exact hsplit_right
  132. 0132exact hold_witness_witness_witness_right_right_left
  133. 0133exact hold_witness_witness_witness_right_right_right