BT00T2 · Bertrand theorem

beta_pascal_zero_row_extend

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

Append the next fixed zero-row value while preserving all earlier cells.

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. ∀ w. (∀ x. Lt(x,w) → ∃ y. BetaAt(b,c,x,y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. x = S z ∧ y = 0))) → ∃ x. ∃ y. ∀ z. Lt(z,S w) → ∃ n. BetaAt(x,y,z,n) ∧ (z = 0 ∧ n = 1 ∨ (∃ m. z = S m ∧ n = 0))

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

4 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt

4 occurrences

Exact expanded native-PA statement
forall b c w. (forall bcf_index_bpzre_before. (exists bcf_lt_gap_bpzre_before_bound. bcf_lt_gap_bpzre_before_bound + S (bcf_index_bpzre_before) = w) -> exists bcf_value_bpzre_before. ((((exists bcf_height_bpzre_before_entry. bcf_height_bpzre_before_entry + S (bcf_value_bpzre_before) = S ((S (bcf_index_bpzre_before)) * c)) /\ exists bcf_quotient_bpzre_before_entry. b = bcf_quotient_bpzre_before_entry * S ((S (bcf_index_bpzre_before)) * c) + (bcf_value_bpzre_before))) /\ ((bcf_index_bpzre_before = 0 /\ bcf_value_bpzre_before = 1) \/ exists bcf_predecessor_bpzre_before. bcf_index_bpzre_before = S bcf_predecessor_bpzre_before /\ bcf_value_bpzre_before = 0))) -> exists d e. (forall bcf_index_bpzre_after. (exists bcf_lt_gap_bpzre_after_bound. bcf_lt_gap_bpzre_after_bound + S (bcf_index_bpzre_after) = S (w)) -> exists bcf_value_bpzre_after. ((((exists bcf_height_bpzre_after_entry. bcf_height_bpzre_after_entry + S (bcf_value_bpzre_after) = S ((S (bcf_index_bpzre_after)) * e)) /\ exists bcf_quotient_bpzre_after_entry. d = bcf_quotient_bpzre_after_entry * S ((S (bcf_index_bpzre_after)) * e) + (bcf_value_bpzre_after))) /\ ((bcf_index_bpzre_after = 0 /\ bcf_value_bpzre_after = 1) \/ exists bcf_predecessor_bpzre_after. bcf_index_bpzre_after = S bcf_predecessor_bpzre_after /\ bcf_value_bpzre_after = 0)))

Proof neighborhood

Direct theorem prerequisites

BT000Q zero_or_succ BT005D beta_prefix_extend BT00AA finite_lt_succ_eq_or_lt

Direct theorem dependents

BT00T3 beta_pascal_zero_row_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

92 script commands · 46 reading checkpoints · 4 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)
zero or succbeta prefix extendfinite lt succ eq or lt
01Fix variables and assumptionsL1–4

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro w
  4. L4
    intro hrow
02Use earlier factsL5–5

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

  1. L5
    specialize zero_or_succ w
03Separate the logical casesL6–6

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

  1. L6
    cases zero_or_succ
04Use earlier factsL7–10

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

  1. L7
    specialize beta_prefix_extend w
  2. L8
    specialize beta_prefix_extend b
  3. L9
    specialize beta_prefix_extend c
  4. L10
    specialize beta_prefix_extend 1
05Separate the logical casesL11–13

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

  1. L11
    cases beta_prefix_extend
  2. L12
    cases beta_prefix_extend_witness
  3. L13
    cases beta_prefix_extend_witness_witness
06Construct an explicit witnessL14–15

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

  1. L14
    exists x
  2. L15
    exists x1
07Fix variables and assumptionsL16–17

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

  1. L16
    intro i
  2. L17
    intro hi
08Establish hsplitL18–22

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

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

  1. L23
    cases hsplit
10Construct an explicit witnessL24–24

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

  1. L24
    exists 1
11Separate the logical casesL25–25

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

  1. L25
    split
12Calculate and transport equalitiesL26–27

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

  1. L26
    rewrite hsplit_left
  2. L27
    rewrite hsplit_left
13Use earlier factsL28–28

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

  1. L28
    exact beta_prefix_extend_witness_witness_left
14Separate the logical casesL29–30

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

  1. L29
    left
  2. L30
    split
15Calculate and transport equalitiesL31–31

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

  1. L31
    trans w
16Use earlier factsL32–33

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

  1. L32
    exact hsplit_left
  2. L33
    exact zero_or_succ_left
17Calculate and transport equalitiesL34–34

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

  1. L34
    refl
18Use earlier factsL35–35

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

  1. L35
    specialize hrow i
19Establish holdL36–38

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

  1. L36
    have hold : ∃ value. BetaAt(b,c,i,value) ∧ (i = 0 ∧ value = 1 ∨ (∃ x. i = S x ∧ value = 0))Definitions: BetaAt(b,c,i,value)Original native command in the exact edition
  2. L37
    apply hrow
  3. L38
    exact hsplit_right
20Separate the logical casesL39–40

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

  1. L39
    cases hold
  2. L40
    cases hold_witness
21Construct an explicit witnessL41–41

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

  1. L41
    exists x2
22Separate the logical casesL42–42

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

  1. L42
    split
23Use earlier factsL43–48

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

  1. L43
    specialize beta_prefix_extend_witness_witness_right i
  2. L44
    specialize beta_prefix_extend_witness_witness_right x2
  3. L45
    apply beta_prefix_extend_witness_witness_right
  4. L46
    exact hsplit_right
  5. L47
    exact hold_witness_left
  6. L48
    exact hold_witness_right
24Separate the logical casesL49–49

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

  1. L49
    cases zero_or_succ_right
25Use earlier factsL50–53

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

  1. L50
    specialize beta_prefix_extend w
  2. L51
    specialize beta_prefix_extend b
  3. L52
    specialize beta_prefix_extend c
  4. L53
    specialize beta_prefix_extend 0
26Separate the logical casesL54–56

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

  1. L54
    cases beta_prefix_extend
  2. L55
    cases beta_prefix_extend_witness
  3. L56
    cases beta_prefix_extend_witness_witness
27Construct an explicit witnessL57–58

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

  1. L57
    exists x1
  2. L58
    exists x2
28Fix variables and assumptionsL59–60

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

  1. L59
    intro i
  2. L60
    intro hi
29Establish hsplitL61–65

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. L61
    have hsplit : i = w ∨ Lt(i,w)Definitions: Lt(i,w)Original native command in the exact edition
  2. L62
    specialize finite_lt_succ_eq_or_lt w
  3. L63
    specialize finite_lt_succ_eq_or_lt i
  4. L64
    apply finite_lt_succ_eq_or_lt
  5. L65
    exact hi
30Separate the logical casesL66–66

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

  1. L66
    cases hsplit
31Construct an explicit witnessL67–67

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

  1. L67
    exists 0
32Separate the logical casesL68–68

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

  1. L68
    split
33Calculate and transport equalitiesL69–70

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

  1. L69
    rewrite hsplit_left
  2. L70
    rewrite hsplit_left
34Use earlier factsL71–71

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

  1. L71
    exact beta_prefix_extend_witness_witness_left
35Separate the logical casesL72–72

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

  1. L72
    right
36Construct an explicit witnessL73–73

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

  1. L73
    exists x
37Separate the logical casesL74–74

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

  1. L74
    split
38Calculate and transport equalitiesL75–75

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

  1. L75
    trans w
39Use earlier factsL76–77

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

  1. L76
    exact hsplit_left
  2. L77
    exact zero_or_succ_right_witness
40Calculate and transport equalitiesL78–78

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

  1. L78
    refl
41Use earlier factsL79–79

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

  1. L79
    specialize hrow i
42Establish holdL80–82

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

  1. L80
    have hold : ∃ value. BetaAt(b,c,i,value) ∧ (i = 0 ∧ value = 1 ∨ (∃ x. i = S x ∧ value = 0))Definitions: BetaAt(b,c,i,value)Original native command in the exact edition
  2. L81
    apply hrow
  3. L82
    exact hsplit_right
43Separate the logical casesL83–84

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

  1. L83
    cases hold
  2. L84
    cases hold_witness
44Construct an explicit witnessL85–85

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

  1. L85
    exists x3
45Separate the logical casesL86–86

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

  1. L86
    split
46Use earlier factsL87–92

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

  1. L87
    specialize beta_prefix_extend_witness_witness_right i
  2. L88
    specialize beta_prefix_extend_witness_witness_right x3
  3. L89
    apply beta_prefix_extend_witness_witness_right
  4. L90
    exact hsplit_right
  5. L91
    exact hold_witness_left
  6. L92
    exact hold_witness_right

Library-wide reading audit

Original defined command ledger · 92 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro w
  4. 0004intro hrow
  5. 0005specialize zero_or_succ w
  6. 0006cases zero_or_succ
  7. 0007specialize beta_prefix_extend w
  8. 0008specialize beta_prefix_extend b
  9. 0009specialize beta_prefix_extend c
  10. 0010specialize beta_prefix_extend 1
  11. 0011cases beta_prefix_extend
  12. 0012cases beta_prefix_extend_witness
  13. 0013cases beta_prefix_extend_witness_witness
  14. 0014exists x
  15. 0015exists x1
  16. 0016intro i
  17. 0017intro hi
  18. 0018have hsplit : i = w ∨ Lt(i,w)
    Exact native replay linehave hsplit : i = w \/ exists gap. gap + S i = w
  19. 0019specialize finite_lt_succ_eq_or_lt w
  20. 0020specialize finite_lt_succ_eq_or_lt i
  21. 0021apply finite_lt_succ_eq_or_lt
  22. 0022exact hi
  23. 0023cases hsplit
  24. 0024exists 1
  25. 0025split
  26. 0026rewrite hsplit_left
  27. 0027rewrite hsplit_left
  28. 0028exact beta_prefix_extend_witness_witness_left
  29. 0029left
  30. 0030split
  31. 0031trans w
  32. 0032exact hsplit_left
  33. 0033exact zero_or_succ_left
  34. 0034refl
  35. 0035specialize hrow i
  36. 0036have hold : ∃ value. BetaAt(b,c,i,value) ∧ (i = 0 ∧ value = 1 ∨ (∃ x. i = S x ∧ value = 0))
    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 predecessor. i = S predecessor /\ value = 0))
  37. 0037apply hrow
  38. 0038exact hsplit_right
  39. 0039cases hold
  40. 0040cases hold_witness
  41. 0041exists x2
  42. 0042split
  43. 0043specialize beta_prefix_extend_witness_witness_right i
  44. 0044specialize beta_prefix_extend_witness_witness_right x2
  45. 0045apply beta_prefix_extend_witness_witness_right
  46. 0046exact hsplit_right
  47. 0047exact hold_witness_left
  48. 0048exact hold_witness_right
  49. 0049cases zero_or_succ_right
  50. 0050specialize beta_prefix_extend w
  51. 0051specialize beta_prefix_extend b
  52. 0052specialize beta_prefix_extend c
  53. 0053specialize beta_prefix_extend 0
  54. 0054cases beta_prefix_extend
  55. 0055cases beta_prefix_extend_witness
  56. 0056cases beta_prefix_extend_witness_witness
  57. 0057exists x1
  58. 0058exists x2
  59. 0059intro i
  60. 0060intro hi
  61. 0061have hsplit : i = w ∨ Lt(i,w)
    Exact native replay linehave hsplit : i = w \/ exists gap. gap + S i = w
  62. 0062specialize finite_lt_succ_eq_or_lt w
  63. 0063specialize finite_lt_succ_eq_or_lt i
  64. 0064apply finite_lt_succ_eq_or_lt
  65. 0065exact hi
  66. 0066cases hsplit
  67. 0067exists 0
  68. 0068split
  69. 0069rewrite hsplit_left
  70. 0070rewrite hsplit_left
  71. 0071exact beta_prefix_extend_witness_witness_left
  72. 0072right
  73. 0073exists x
  74. 0074split
  75. 0075trans w
  76. 0076exact hsplit_left
  77. 0077exact zero_or_succ_right_witness
  78. 0078refl
  79. 0079specialize hrow i
  80. 0080have hold : ∃ value. BetaAt(b,c,i,value) ∧ (i = 0 ∧ value = 1 ∨ (∃ x. i = S x ∧ value = 0))
    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 predecessor. i = S predecessor /\ value = 0))
  81. 0081apply hrow
  82. 0082exact hsplit_right
  83. 0083cases hold
  84. 0084cases hold_witness
  85. 0085exists x3
  86. 0086split
  87. 0087specialize beta_prefix_extend_witness_witness_right i
  88. 0088specialize beta_prefix_extend_witness_witness_right x3
  89. 0089apply beta_prefix_extend_witness_witness_right
  90. 0090exact hsplit_right
  91. 0091exact hold_witness_left
  92. 0092exact hold_witness_right