BT00T9 · Bertrand theorem

beta_pascal_zero_row_pointwise_functional

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

Zero-row values agree pointwise across beta encodings and widths.

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

8 occurrences

In local proof propositions

PD0013 BetaAt

2 occurrences

Exact expanded native-PA statement
forall b c d e w v i x y. (forall bcf_index_bzrpf_left. (exists bcf_lt_gap_bzrpf_left_bound. bcf_lt_gap_bzrpf_left_bound + S (bcf_index_bzrpf_left) = w) -> exists bcf_value_bzrpf_left. ((((exists bcf_height_bzrpf_left_entry. bcf_height_bzrpf_left_entry + S (bcf_value_bzrpf_left) = S ((S (bcf_index_bzrpf_left)) * c)) /\ exists bcf_quotient_bzrpf_left_entry. b = bcf_quotient_bzrpf_left_entry * S ((S (bcf_index_bzrpf_left)) * c) + (bcf_value_bzrpf_left))) /\ ((bcf_index_bzrpf_left = 0 /\ bcf_value_bzrpf_left = 1) \/ exists bcf_predecessor_bzrpf_left. bcf_index_bzrpf_left = S bcf_predecessor_bzrpf_left /\ bcf_value_bzrpf_left = 0))) -> (forall bcf_index_bzrpf_right. (exists bcf_lt_gap_bzrpf_right_bound. bcf_lt_gap_bzrpf_right_bound + S (bcf_index_bzrpf_right) = v) -> exists bcf_value_bzrpf_right. ((((exists bcf_height_bzrpf_right_entry. bcf_height_bzrpf_right_entry + S (bcf_value_bzrpf_right) = S ((S (bcf_index_bzrpf_right)) * e)) /\ exists bcf_quotient_bzrpf_right_entry. d = bcf_quotient_bzrpf_right_entry * S ((S (bcf_index_bzrpf_right)) * e) + (bcf_value_bzrpf_right))) /\ ((bcf_index_bzrpf_right = 0 /\ bcf_value_bzrpf_right = 1) \/ exists bcf_predecessor_bzrpf_right. bcf_index_bzrpf_right = S bcf_predecessor_bzrpf_right /\ bcf_value_bzrpf_right = 0))) -> (exists bcf_lt_gap_bzrpf_left_bound. bcf_lt_gap_bzrpf_left_bound + S (i) = w) -> (exists bcf_lt_gap_bzrpf_right_bound. bcf_lt_gap_bzrpf_right_bound + S (i) = v) -> (((exists bcf_height_bzrpf_left_at. bcf_height_bzrpf_left_at + S (x) = S ((S (i)) * c)) /\ exists bcf_quotient_bzrpf_left_at. b = bcf_quotient_bzrpf_left_at * S ((S (i)) * c) + (x))) -> (((exists bcf_height_bzrpf_right_at. bcf_height_bzrpf_right_at + S (y) = S ((S (i)) * e)) /\ exists bcf_quotient_bzrpf_right_at. d = bcf_quotient_bzrpf_right_at * S ((S (i)) * e) + (y))) -> x = y

Proof neighborhood

Direct theorem prerequisites

BT0042 beta_at_unique BT000C succ_ne_zero

Direct theorem dependents

BT00TB beta_pascal_table_row_pointwise_functional

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

93 script commands · 30 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 (2)
beta at uniquesucc ne zero
01Fix variables and assumptionsL1–10

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro d
  4. L4
    intro e
  5. L5
    intro w
  6. L6
    intro v
  7. L7
    intro i
  8. L8
    intro x
  9. L9
    intro y
  10. L10
    intro hleft
02Fix variables and assumptionsL11–15

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

  1. L11
    intro hright
  2. L12
    intro hiw
  3. L13
    intro hiv
  4. L14
    intro hxi
  5. L15
    intro hyi
03Establish hleft_valueL16–19

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

  1. L16
    have hleft_value : ∃ bcf_cell_value_bzrpf_left_cell. BetaAt(b,c,i,bcf_cell_value_bzrpf_left_cell) ∧ (i = 0 ∧ bcf_cell_value_bzrpf_left_cell = 1 ∨ (∃ x. i = S x ∧ bcf_cell_value_bzrpf_left_cell = 0))Definitions: BetaAt(b,c,i,bcf_cell_value_bzrpf_left_cell)Original native command in the exact edition
  2. L17
    specialize hleft i
  3. L18
    apply hleft
  4. L19
    exact hiw
04Separate the logical casesL20–21

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

  1. L20
    cases hleft_value
  2. L21
    cases hleft_value_witness
05Establish hright_valueL22–25

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

  1. L22
    have hright_value : ∃ bcf_cell_value_bzrpf_right_cell. BetaAt(d,e,i,bcf_cell_value_bzrpf_right_cell) ∧ (i = 0 ∧ bcf_cell_value_bzrpf_right_cell = 1 ∨ (∃ x. i = S x ∧ bcf_cell_value_bzrpf_right_cell = 0))Definitions: BetaAt(d,e,i,bcf_cell_value_bzrpf_right_cell)Original native command in the exact edition
  2. L23
    specialize hright i
  3. L24
    apply hright
  4. L25
    exact hiv
06Separate the logical casesL26–27

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

  1. L26
    cases hright_value
  2. L27
    cases hright_value_witness
07Establish hx_valueL28–36

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

  1. L28
    have hx_value : x = x1
  2. L29
    specialize beta_at_unique b
  3. L30
    specialize beta_at_unique c
  4. L31
    specialize beta_at_unique i
  5. L32
    specialize beta_at_unique x
  6. L33
    specialize beta_at_unique x1
  7. L34
    apply beta_at_unique
  8. L35
    exact hxi
  9. L36
    exact hleft_value_witness_left
08Establish hy_valueL37–45

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

  1. L37
    have hy_value : y = x2
  2. L38
    specialize beta_at_unique d
  3. L39
    specialize beta_at_unique e
  4. L40
    specialize beta_at_unique i
  5. L41
    specialize beta_at_unique y
  6. L42
    specialize beta_at_unique x2
  7. L43
    apply beta_at_unique
  8. L44
    exact hyi
  9. L45
    exact hright_value_witness_left
09Separate the logical casesL46–49

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

  1. L46
    cases hleft_value_witness_right
  2. L47
    cases hleft_value_witness_right_left
  3. L48
    cases hright_value_witness_right
  4. L49
    cases hright_value_witness_right_left
10Calculate and transport equalitiesL50–50

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

  1. L50
    trans x1
11Use earlier factsL51–51

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

  1. L51
    exact hx_value
12Calculate and transport equalitiesL52–52

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

  1. L52
    trans 1
13Use earlier factsL53–53

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

  1. L53
    exact hleft_value_witness_right_left_right
14Calculate and transport equalitiesL54–55

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

  1. L54
    trans x2
  2. L55
    symm
15Use earlier factsL56–56

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

  1. L56
    exact hright_value_witness_right_left_right
16Calculate and transport equalitiesL57–57

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

  1. L57
    symm
17Use earlier factsL58–58

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

  1. L58
    exact hy_value
18Separate the logical casesL59–61

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

  1. L59
    cases hright_value_witness_right_right
  2. L60
    cases hright_value_witness_right_right_witness
  3. L61
    exfalso
19Establish hbadL62–69

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

  1. L62
    have hbad : S x3 = 0
  2. L63
    trans i
  3. L64
    symm
  4. L65
    exact hright_value_witness_right_right_witness_left
  5. L66
    exact hleft_value_witness_right_left_left
  6. L67
    specialize succ_ne_zero x3
  7. L68
    apply succ_ne_zero
  8. L69
    exact hbad
20Separate the logical casesL70–74

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

  1. L70
    cases hleft_value_witness_right_right
  2. L71
    cases hleft_value_witness_right_right_witness
  3. L72
    cases hright_value_witness_right
  4. L73
    cases hright_value_witness_right_left
  5. L74
    exfalso
21Establish hbadL75–82

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

  1. L75
    have hbad : S x3 = 0
  2. L76
    trans i
  3. L77
    symm
  4. L78
    exact hleft_value_witness_right_right_witness_left
  5. L79
    exact hright_value_witness_right_left_left
  6. L80
    specialize succ_ne_zero x3
  7. L81
    apply succ_ne_zero
  8. L82
    exact hbad
22Separate the logical casesL83–84

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

  1. L83
    cases hright_value_witness_right_right
  2. L84
    cases hright_value_witness_right_right_witness
23Calculate and transport equalitiesL85–85

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

  1. L85
    trans x1
24Use earlier factsL86–86

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

  1. L86
    exact hx_value
25Calculate and transport equalitiesL87–87

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

  1. L87
    trans 0
26Use earlier factsL88–88

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

  1. L88
    exact hleft_value_witness_right_right_witness_right
27Calculate and transport equalitiesL89–90

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

  1. L89
    trans x2
  2. L90
    symm
28Use earlier factsL91–91

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

  1. L91
    exact hright_value_witness_right_right_witness_right
29Calculate and transport equalitiesL92–92

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

  1. L92
    symm
30Use earlier factsL93–93

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

  1. L93
    exact hy_value

Library-wide reading audit

Original defined command ledger · 93 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro w
  6. 0006intro v
  7. 0007intro i
  8. 0008intro x
  9. 0009intro y
  10. 0010intro hleft
  11. 0011intro hright
  12. 0012intro hiw
  13. 0013intro hiv
  14. 0014intro hxi
  15. 0015intro hyi
  16. 0016have hleft_value : ∃ bcf_cell_value_bzrpf_left_cell. BetaAt(b,c,i,bcf_cell_value_bzrpf_left_cell) ∧ (i = 0 ∧ bcf_cell_value_bzrpf_left_cell = 1 ∨ (∃ x. i = S x ∧ bcf_cell_value_bzrpf_left_cell = 0))
    Exact native replay linehave hleft_value : exists bcf_cell_value_bzrpf_left_cell. ((((exists bcf_height_bzrpf_left_cell_entry. bcf_height_bzrpf_left_cell_entry + S (bcf_cell_value_bzrpf_left_cell) = S ((S (i)) * c)) /\ exists bcf_quotient_bzrpf_left_cell_entry. b = bcf_quotient_bzrpf_left_cell_entry * S ((S (i)) * c) + (bcf_cell_value_bzrpf_left_cell))) /\ ((i = 0 /\ bcf_cell_value_bzrpf_left_cell = 1) \/ exists bcf_cell_predecessor_bzrpf_left_cell. i = S bcf_cell_predecessor_bzrpf_left_cell /\ bcf_cell_value_bzrpf_left_cell = 0))
  17. 0017specialize hleft i
  18. 0018apply hleft
  19. 0019exact hiw
  20. 0020cases hleft_value
  21. 0021cases hleft_value_witness
  22. 0022have hright_value : ∃ bcf_cell_value_bzrpf_right_cell. BetaAt(d,e,i,bcf_cell_value_bzrpf_right_cell) ∧ (i = 0 ∧ bcf_cell_value_bzrpf_right_cell = 1 ∨ (∃ x. i = S x ∧ bcf_cell_value_bzrpf_right_cell = 0))
    Exact native replay linehave hright_value : exists bcf_cell_value_bzrpf_right_cell. ((((exists bcf_height_bzrpf_right_cell_entry. bcf_height_bzrpf_right_cell_entry + S (bcf_cell_value_bzrpf_right_cell) = S ((S (i)) * e)) /\ exists bcf_quotient_bzrpf_right_cell_entry. d = bcf_quotient_bzrpf_right_cell_entry * S ((S (i)) * e) + (bcf_cell_value_bzrpf_right_cell))) /\ ((i = 0 /\ bcf_cell_value_bzrpf_right_cell = 1) \/ exists bcf_cell_predecessor_bzrpf_right_cell. i = S bcf_cell_predecessor_bzrpf_right_cell /\ bcf_cell_value_bzrpf_right_cell = 0))
  23. 0023specialize hright i
  24. 0024apply hright
  25. 0025exact hiv
  26. 0026cases hright_value
  27. 0027cases hright_value_witness
  28. 0028have hx_value : x = x1
  29. 0029specialize beta_at_unique b
  30. 0030specialize beta_at_unique c
  31. 0031specialize beta_at_unique i
  32. 0032specialize beta_at_unique x
  33. 0033specialize beta_at_unique x1
  34. 0034apply beta_at_unique
  35. 0035exact hxi
  36. 0036exact hleft_value_witness_left
  37. 0037have hy_value : y = x2
  38. 0038specialize beta_at_unique d
  39. 0039specialize beta_at_unique e
  40. 0040specialize beta_at_unique i
  41. 0041specialize beta_at_unique y
  42. 0042specialize beta_at_unique x2
  43. 0043apply beta_at_unique
  44. 0044exact hyi
  45. 0045exact hright_value_witness_left
  46. 0046cases hleft_value_witness_right
  47. 0047cases hleft_value_witness_right_left
  48. 0048cases hright_value_witness_right
  49. 0049cases hright_value_witness_right_left
  50. 0050trans x1
  51. 0051exact hx_value
  52. 0052trans 1
  53. 0053exact hleft_value_witness_right_left_right
  54. 0054trans x2
  55. 0055symm
  56. 0056exact hright_value_witness_right_left_right
  57. 0057symm
  58. 0058exact hy_value
  59. 0059cases hright_value_witness_right_right
  60. 0060cases hright_value_witness_right_right_witness
  61. 0061exfalso
  62. 0062have hbad : S x3 = 0
  63. 0063trans i
  64. 0064symm
  65. 0065exact hright_value_witness_right_right_witness_left
  66. 0066exact hleft_value_witness_right_left_left
  67. 0067specialize succ_ne_zero x3
  68. 0068apply succ_ne_zero
  69. 0069exact hbad
  70. 0070cases hleft_value_witness_right_right
  71. 0071cases hleft_value_witness_right_right_witness
  72. 0072cases hright_value_witness_right
  73. 0073cases hright_value_witness_right_left
  74. 0074exfalso
  75. 0075have hbad : S x3 = 0
  76. 0076trans i
  77. 0077symm
  78. 0078exact hleft_value_witness_right_right_witness_left
  79. 0079exact hright_value_witness_right_left_left
  80. 0080specialize succ_ne_zero x3
  81. 0081apply succ_ne_zero
  82. 0082exact hbad
  83. 0083cases hright_value_witness_right_right
  84. 0084cases hright_value_witness_right_right_witness
  85. 0085trans x1
  86. 0086exact hx_value
  87. 0087trans 0
  88. 0088exact hleft_value_witness_right_right_witness_right
  89. 0089trans x2
  90. 0090symm
  91. 0091exact hright_value_witness_right_right_witness_right
  92. 0092symm
  93. 0093exact hy_value