BT00T4 · Bertrand theorem

beta_pascal_row_step_extend

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

Append one Pascal successor-row value and preserve the prefix.

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

∀ pb. ∀ pc. ∀ b. ∀ c. ∀ w. (∀ x. Lt(x,w) → ∃ y. BetaAt(b,c,x,y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. ∃ n. ∃ m. x = S z ∧ (BetaAt(pb,pc,z,n) ∧ (BetaAt(pb,pc,S z,m) ∧ y = n + m))))) → ∃ x. ∃ y. ∀ z. Lt(z,S w) → ∃ n. BetaAt(x,y,z,n) ∧ (z = 0 ∧ n = 1 ∨ (∃ m. ∃ k. ∃ i. z = S m ∧ (BetaAt(pb,pc,m,k) ∧ (BetaAt(pb,pc,S m,i) ∧ n = k + i))))

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

8 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt

10 occurrences

Exact expanded native-PA statement
forall pb pc b c w. (forall bcf_index_bpsre_before. (exists bcf_lt_gap_bpsre_before_bound. bcf_lt_gap_bpsre_before_bound + S (bcf_index_bpsre_before) = w) -> exists bcf_value_bpsre_before. ((((exists bcf_height_bpsre_before_entry. bcf_height_bpsre_before_entry + S (bcf_value_bpsre_before) = S ((S (bcf_index_bpsre_before)) * c)) /\ exists bcf_quotient_bpsre_before_entry. b = bcf_quotient_bpsre_before_entry * S ((S (bcf_index_bpsre_before)) * c) + (bcf_value_bpsre_before))) /\ ((bcf_index_bpsre_before = 0 /\ bcf_value_bpsre_before = 1) \/ exists bcf_predecessor_bpsre_before bcf_left_bpsre_before bcf_right_bpsre_before. bcf_index_bpsre_before = S bcf_predecessor_bpsre_before /\ ((((exists bcf_height_bpsre_before_previous_left. bcf_height_bpsre_before_previous_left + S (bcf_left_bpsre_before) = S ((S (bcf_predecessor_bpsre_before)) * pc)) /\ exists bcf_quotient_bpsre_before_previous_left. pb = bcf_quotient_bpsre_before_previous_left * S ((S (bcf_predecessor_bpsre_before)) * pc) + (bcf_left_bpsre_before))) /\ ((((exists bcf_height_bpsre_before_previous_right. bcf_height_bpsre_before_previous_right + S (bcf_right_bpsre_before) = S ((S (S (bcf_predecessor_bpsre_before))) * pc)) /\ exists bcf_quotient_bpsre_before_previous_right. pb = bcf_quotient_bpsre_before_previous_right * S ((S (S (bcf_predecessor_bpsre_before))) * pc) + (bcf_right_bpsre_before))) /\ bcf_value_bpsre_before = bcf_left_bpsre_before + bcf_right_bpsre_before))))) -> exists d e. (forall bcf_index_bpsre_after. (exists bcf_lt_gap_bpsre_after_bound. bcf_lt_gap_bpsre_after_bound + S (bcf_index_bpsre_after) = S (w)) -> exists bcf_value_bpsre_after. ((((exists bcf_height_bpsre_after_entry. bcf_height_bpsre_after_entry + S (bcf_value_bpsre_after) = S ((S (bcf_index_bpsre_after)) * e)) /\ exists bcf_quotient_bpsre_after_entry. d = bcf_quotient_bpsre_after_entry * S ((S (bcf_index_bpsre_after)) * e) + (bcf_value_bpsre_after))) /\ ((bcf_index_bpsre_after = 0 /\ bcf_value_bpsre_after = 1) \/ exists bcf_predecessor_bpsre_after bcf_left_bpsre_after bcf_right_bpsre_after. bcf_index_bpsre_after = S bcf_predecessor_bpsre_after /\ ((((exists bcf_height_bpsre_after_previous_left. bcf_height_bpsre_after_previous_left + S (bcf_left_bpsre_after) = S ((S (bcf_predecessor_bpsre_after)) * pc)) /\ exists bcf_quotient_bpsre_after_previous_left. pb = bcf_quotient_bpsre_after_previous_left * S ((S (bcf_predecessor_bpsre_after)) * pc) + (bcf_left_bpsre_after))) /\ ((((exists bcf_height_bpsre_after_previous_right. bcf_height_bpsre_after_previous_right + S (bcf_right_bpsre_after) = S ((S (S (bcf_predecessor_bpsre_after))) * pc)) /\ exists bcf_quotient_bpsre_after_previous_right. pb = bcf_quotient_bpsre_after_previous_right * S ((S (S (bcf_predecessor_bpsre_after))) * pc) + (bcf_right_bpsre_after))) /\ bcf_value_bpsre_after = bcf_left_bpsre_after + bcf_right_bpsre_after)))))

Proof neighborhood

Direct theorem prerequisites

BT000Q zero_or_succ BT0041 beta_at_exists BT005D beta_prefix_extend BT00AA finite_lt_succ_eq_or_lt

Direct theorem dependents

BT00T5 beta_pascal_row_step_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

112 script commands · 54 reading checkpoints · 6 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 (4)
zero or succbeta at existsbeta prefix extendfinite lt succ eq or lt
01Fix variables and assumptionsL1–6

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

  1. L1
    intro pb
  2. L2
    intro pc
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro w
  6. L6
    intro hrow
02Use earlier factsL7–7

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

  1. L7
    specialize zero_or_succ w
03Separate the logical casesL8–8

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

  1. L8
    cases zero_or_succ
04Use earlier factsL9–12

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

  1. L9
    specialize beta_prefix_extend w
  2. L10
    specialize beta_prefix_extend b
  3. L11
    specialize beta_prefix_extend c
  4. L12
    specialize beta_prefix_extend 1
05Separate the logical casesL13–15

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

  1. L13
    cases beta_prefix_extend
  2. L14
    cases beta_prefix_extend_witness
  3. L15
    cases beta_prefix_extend_witness_witness
06Construct an explicit witnessL16–17

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

  1. L16
    exists x
  2. L17
    exists x1
07Fix variables and assumptionsL18–19

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

  1. L18
    intro i
  2. L19
    intro hi
08Establish hsplitL20–24

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. L20
    have hsplit : i = w ∨ Lt(i,w)Definitions: Lt(i,w)Original native command in the exact edition
  2. L21
    specialize finite_lt_succ_eq_or_lt w
  3. L22
    specialize finite_lt_succ_eq_or_lt i
  4. L23
    apply finite_lt_succ_eq_or_lt
  5. L24
    exact hi
09Separate the logical casesL25–25

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

  1. L25
    cases hsplit
10Construct an explicit witnessL26–26

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

  1. L26
    exists 1
11Separate the logical casesL27–27

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

  1. L27
    split
12Calculate and transport equalitiesL28–29

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

  1. L28
    rewrite hsplit_left
  2. L29
    rewrite hsplit_left
13Use earlier factsL30–30

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

  1. L30
    exact beta_prefix_extend_witness_witness_left
14Separate the logical casesL31–32

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

  1. L31
    left
  2. L32
    split
15Calculate and transport equalitiesL33–33

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

  1. L33
    trans w
16Use earlier factsL34–35

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

  1. L34
    exact hsplit_left
  2. L35
    exact zero_or_succ_left
17Calculate and transport equalitiesL36–36

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

  1. L36
    refl
18Use earlier factsL37–37

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

  1. L37
    specialize hrow i
19Establish holdL38–40

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

  1. L38
    have hold : ∃ value. BetaAt(b,c,i,value) ∧ (i = 0 ∧ value = 1 ∨ (∃ x. ∃ y. ∃ z. i = S x ∧ (BetaAt(pb,pc,x,y) ∧ (BetaAt(pb,pc,S x,z) ∧ value = y + z))))Definitions: BetaAt(b,c,i,value)BetaAt(pb,pc,x,y)BetaAt(pb,pc,S x,z)Original native command in the exact edition
  2. L39
    apply hrow
  3. L40
    exact hsplit_right
20Separate the logical casesL41–42

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

  1. L41
    cases hold
  2. L42
    cases hold_witness
21Construct an explicit witnessL43–43

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

  1. L43
    exists x2
22Separate the logical casesL44–44

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

  1. L44
    split
23Use earlier factsL45–50

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

  1. L45
    specialize beta_prefix_extend_witness_witness_right i
  2. L46
    specialize beta_prefix_extend_witness_witness_right x2
  3. L47
    apply beta_prefix_extend_witness_witness_right
  4. L48
    exact hsplit_right
  5. L49
    exact hold_witness_left
  6. L50
    exact hold_witness_right
24Separate the logical casesL51–51

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

  1. L51
    cases zero_or_succ_right
25Establish hleftL52–56

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

  1. L52
    have hleft : ∃ u. BetaAt(pb,pc,x,u)Definitions: BetaAt(pb,pc,x,u)Original native command in the exact edition
  2. L53
    specialize beta_at_exists pb
  3. L54
    specialize beta_at_exists pc
  4. L55
    specialize beta_at_exists x
  5. L56
    exact beta_at_exists
26Separate the logical casesL57–57

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

  1. L57
    cases hleft
27Establish hrightL58–62

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

  1. L58
    have hright : ∃ v. BetaAt(pb,pc,S x,v)Definitions: BetaAt(pb,pc,S x,v)Original native command in the exact edition
  2. L59
    specialize beta_at_exists pb
  3. L60
    specialize beta_at_exists pc
  4. L61
    specialize beta_at_exists (S x)
  5. L62
    exact beta_at_exists
28Separate the logical casesL63–63

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

  1. L63
    cases hright
29Use earlier factsL64–67

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

  1. L64
    specialize beta_prefix_extend w
  2. L65
    specialize beta_prefix_extend b
  3. L66
    specialize beta_prefix_extend c
  4. L67
    specialize beta_prefix_extend (x1 + x2)
30Separate the logical casesL68–70

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

  1. L68
    cases beta_prefix_extend
  2. L69
    cases beta_prefix_extend_witness
  3. L70
    cases beta_prefix_extend_witness_witness
31Construct an explicit witnessL71–72

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

  1. L71
    exists x3
  2. L72
    exists x4
32Fix variables and assumptionsL73–74

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

  1. L73
    intro i
  2. L74
    intro hi
33Establish hsplitL75–79

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. L75
    have hsplit : i = w ∨ Lt(i,w)Definitions: Lt(i,w)Original native command in the exact edition
  2. L76
    specialize finite_lt_succ_eq_or_lt w
  3. L77
    specialize finite_lt_succ_eq_or_lt i
  4. L78
    apply finite_lt_succ_eq_or_lt
  5. L79
    exact hi
34Separate the logical casesL80–80

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

  1. L80
    cases hsplit
35Construct an explicit witnessL81–81

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

  1. L81
    exists x1 + x2
36Separate the logical casesL82–82

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

  1. L82
    split
37Calculate and transport equalitiesL83–84

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

  1. L83
    rewrite hsplit_left
  2. L84
    rewrite hsplit_left
38Use earlier factsL85–85

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

  1. L85
    exact beta_prefix_extend_witness_witness_left
39Separate the logical casesL86–86

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

  1. L86
    right
40Construct an explicit witnessL87–89

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

  1. L87
    exists x
  2. L88
    exists x1
  3. L89
    exists x2
41Separate the logical casesL90–90

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

  1. L90
    split
42Calculate and transport equalitiesL91–91

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

  1. L91
    trans w
43Use earlier factsL92–93

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

  1. L92
    exact hsplit_left
  2. L93
    exact zero_or_succ_right_witness
44Separate the logical casesL94–94

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

  1. L94
    split
45Use earlier factsL95–95

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

  1. L95
    exact hleft_witness
46Separate the logical casesL96–96

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

  1. L96
    split
47Use earlier factsL97–97

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

  1. L97
    exact hright_witness
48Calculate and transport equalitiesL98–98

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

  1. L98
    refl
49Use earlier factsL99–99

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

  1. L99
    specialize hrow i
50Establish holdL100–102

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

  1. L100
    have hold : ∃ value. BetaAt(b,c,i,value) ∧ (i = 0 ∧ value = 1 ∨ (∃ x. ∃ y. ∃ z. i = S x ∧ (BetaAt(pb,pc,x,y) ∧ (BetaAt(pb,pc,S x,z) ∧ value = y + z))))Definitions: BetaAt(b,c,i,value)BetaAt(pb,pc,x,y)BetaAt(pb,pc,S x,z)Original native command in the exact edition
  2. L101
    apply hrow
  3. L102
    exact hsplit_right
51Separate the logical casesL103–104

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

  1. L103
    cases hold
  2. L104
    cases hold_witness
52Construct an explicit witnessL105–105

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

  1. L105
    exists x5
53Separate the logical casesL106–106

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

  1. L106
    split
54Use earlier factsL107–112

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

  1. L107
    specialize beta_prefix_extend_witness_witness_right i
  2. L108
    specialize beta_prefix_extend_witness_witness_right x5
  3. L109
    apply beta_prefix_extend_witness_witness_right
  4. L110
    exact hsplit_right
  5. L111
    exact hold_witness_left
  6. L112
    exact hold_witness_right

Library-wide reading audit

Original defined command ledger · 112 lines
  1. 0001intro pb
  2. 0002intro pc
  3. 0003intro b
  4. 0004intro c
  5. 0005intro w
  6. 0006intro hrow
  7. 0007specialize zero_or_succ w
  8. 0008cases zero_or_succ
  9. 0009specialize beta_prefix_extend w
  10. 0010specialize beta_prefix_extend b
  11. 0011specialize beta_prefix_extend c
  12. 0012specialize beta_prefix_extend 1
  13. 0013cases beta_prefix_extend
  14. 0014cases beta_prefix_extend_witness
  15. 0015cases beta_prefix_extend_witness_witness
  16. 0016exists x
  17. 0017exists x1
  18. 0018intro i
  19. 0019intro hi
  20. 0020have hsplit : i = w ∨ Lt(i,w)
    Exact native replay linehave hsplit : i = w \/ exists gap. gap + S i = w
  21. 0021specialize finite_lt_succ_eq_or_lt w
  22. 0022specialize finite_lt_succ_eq_or_lt i
  23. 0023apply finite_lt_succ_eq_or_lt
  24. 0024exact hi
  25. 0025cases hsplit
  26. 0026exists 1
  27. 0027split
  28. 0028rewrite hsplit_left
  29. 0029rewrite hsplit_left
  30. 0030exact beta_prefix_extend_witness_witness_left
  31. 0031left
  32. 0032split
  33. 0033trans w
  34. 0034exact hsplit_left
  35. 0035exact zero_or_succ_left
  36. 0036refl
  37. 0037specialize hrow i
  38. 0038have hold : ∃ value. BetaAt(b,c,i,value) ∧ (i = 0 ∧ value = 1 ∨ (∃ x. ∃ y. ∃ z. i = S x ∧ (BetaAt(pb,pc,x,y) ∧ (BetaAt(pb,pc,S x,z) ∧ value = y + z))))
    Exact native replay linehave hold : exists value. (((exists height. height + S value = S ((S i) * c)) /\ exists quotient. b = quotient * S ((S i) * c) + value) /\ ((i = 0 /\ value = 1) \/ exists p u v. i = S p /\ (((exists h. h + S u = S ((S p) * pc)) /\ exists q. pb = q * S ((S p) * pc) + u) /\ (((exists h. h + S v = S ((S (S p)) * pc)) /\ exists q. pb = q * S ((S (S p)) * pc) + v) /\ value = u + v))))
  39. 0039apply hrow
  40. 0040exact hsplit_right
  41. 0041cases hold
  42. 0042cases hold_witness
  43. 0043exists x2
  44. 0044split
  45. 0045specialize beta_prefix_extend_witness_witness_right i
  46. 0046specialize beta_prefix_extend_witness_witness_right x2
  47. 0047apply beta_prefix_extend_witness_witness_right
  48. 0048exact hsplit_right
  49. 0049exact hold_witness_left
  50. 0050exact hold_witness_right
  51. 0051cases zero_or_succ_right
  52. 0052have hleft : ∃ u. BetaAt(pb,pc,x,u)
    Exact native replay linehave hleft : exists u. ((exists h. h + S u = S ((S x) * pc)) /\ exists q. pb = q * S ((S x) * pc) + u)
  53. 0053specialize beta_at_exists pb
  54. 0054specialize beta_at_exists pc
  55. 0055specialize beta_at_exists x
  56. 0056exact beta_at_exists
  57. 0057cases hleft
  58. 0058have hright : ∃ v. BetaAt(pb,pc,S x,v)
    Exact native replay linehave hright : exists v. ((exists h. h + S v = S ((S (S x)) * pc)) /\ exists q. pb = q * S ((S (S x)) * pc) + v)
  59. 0059specialize beta_at_exists pb
  60. 0060specialize beta_at_exists pc
  61. 0061specialize beta_at_exists (S x)
  62. 0062exact beta_at_exists
  63. 0063cases hright
  64. 0064specialize beta_prefix_extend w
  65. 0065specialize beta_prefix_extend b
  66. 0066specialize beta_prefix_extend c
  67. 0067specialize beta_prefix_extend (x1 + x2)
  68. 0068cases beta_prefix_extend
  69. 0069cases beta_prefix_extend_witness
  70. 0070cases beta_prefix_extend_witness_witness
  71. 0071exists x3
  72. 0072exists x4
  73. 0073intro i
  74. 0074intro hi
  75. 0075have hsplit : i = w ∨ Lt(i,w)
    Exact native replay linehave hsplit : i = w \/ exists gap. gap + S i = w
  76. 0076specialize finite_lt_succ_eq_or_lt w
  77. 0077specialize finite_lt_succ_eq_or_lt i
  78. 0078apply finite_lt_succ_eq_or_lt
  79. 0079exact hi
  80. 0080cases hsplit
  81. 0081exists x1 + x2
  82. 0082split
  83. 0083rewrite hsplit_left
  84. 0084rewrite hsplit_left
  85. 0085exact beta_prefix_extend_witness_witness_left
  86. 0086right
  87. 0087exists x
  88. 0088exists x1
  89. 0089exists x2
  90. 0090split
  91. 0091trans w
  92. 0092exact hsplit_left
  93. 0093exact zero_or_succ_right_witness
  94. 0094split
  95. 0095exact hleft_witness
  96. 0096split
  97. 0097exact hright_witness
  98. 0098refl
  99. 0099specialize hrow i
  100. 0100have hold : ∃ value. BetaAt(b,c,i,value) ∧ (i = 0 ∧ value = 1 ∨ (∃ x. ∃ y. ∃ z. i = S x ∧ (BetaAt(pb,pc,x,y) ∧ (BetaAt(pb,pc,S x,z) ∧ value = y + z))))
    Exact native replay linehave hold : exists value. (((exists height. height + S value = S ((S i) * c)) /\ exists quotient. b = quotient * S ((S i) * c) + value) /\ ((i = 0 /\ value = 1) \/ exists p u v. i = S p /\ (((exists h. h + S u = S ((S p) * pc)) /\ exists q. pb = q * S ((S p) * pc) + u) /\ (((exists h. h + S v = S ((S (S p)) * pc)) /\ exists q. pb = q * S ((S (S p)) * pc) + v) /\ value = u + v))))
  101. 0101apply hrow
  102. 0102exact hsplit_right
  103. 0103cases hold
  104. 0104cases hold_witness
  105. 0105exists x5
  106. 0106split
  107. 0107specialize beta_prefix_extend_witness_witness_right i
  108. 0108specialize beta_prefix_extend_witness_witness_right x5
  109. 0109apply beta_prefix_extend_witness_witness_right
  110. 0110exact hsplit_right
  111. 0111exact hold_witness_left
  112. 0112exact hold_witness_right