BT00XW · Bertrand theorem

double_quotient_carry_prefix_extend

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

A carry prefix extends by one freshly decoded carry bit.

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

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

10 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt

4 occurrences

Exact expanded native-PA statement
forall b c d e f g l. (forall b5cc_index_b5ccpe_before. (exists bcf_lt_gap_b5ccpe_before_bound. bcf_lt_gap_b5ccpe_before_bound + S (b5cc_index_b5ccpe_before) = l) -> exists b5cc_left_b5ccpe_before b5cc_right_b5ccpe_before b5cc_bit_b5ccpe_before. (((exists fs_h_b5cc_b5ccpe_before_left. fs_h_b5cc_b5ccpe_before_left + S (b5cc_left_b5ccpe_before) = S ((S (b5cc_index_b5ccpe_before)) * c)) /\ exists fs_q_b5cc_b5ccpe_before_left. b = fs_q_b5cc_b5ccpe_before_left * S ((S (b5cc_index_b5ccpe_before)) * c) + (b5cc_left_b5ccpe_before))) /\ ((((exists fs_h_b5cc_b5ccpe_before_right. fs_h_b5cc_b5ccpe_before_right + S (b5cc_right_b5ccpe_before) = S ((S (b5cc_index_b5ccpe_before)) * e)) /\ exists fs_q_b5cc_b5ccpe_before_right. d = fs_q_b5cc_b5ccpe_before_right * S ((S (b5cc_index_b5ccpe_before)) * e) + (b5cc_right_b5ccpe_before))) /\ ((((exists fs_h_b5cc_b5ccpe_before_bit. fs_h_b5cc_b5ccpe_before_bit + S (b5cc_bit_b5ccpe_before) = S ((S (b5cc_index_b5ccpe_before)) * g)) /\ exists fs_q_b5cc_b5ccpe_before_bit. f = fs_q_b5cc_b5ccpe_before_bit * S ((S (b5cc_index_b5ccpe_before)) * g) + (b5cc_bit_b5ccpe_before))) /\ (((b5cc_bit_b5ccpe_before = 0 /\ b5cc_right_b5ccpe_before = b5cc_left_b5ccpe_before + b5cc_left_b5ccpe_before) \/ (b5cc_bit_b5ccpe_before = 1 /\ b5cc_right_b5ccpe_before = S (b5cc_left_b5ccpe_before + b5cc_left_b5ccpe_before))))))) -> (exists q Q bit. (((exists fs_h_b5ccpe_last_left. fs_h_b5ccpe_last_left + S (q) = S ((S (l)) * c)) /\ exists fs_q_b5ccpe_last_left. b = fs_q_b5ccpe_last_left * S ((S (l)) * c) + (q))) /\ ((((exists fs_h_b5ccpe_last_right. fs_h_b5ccpe_last_right + S (Q) = S ((S (l)) * e)) /\ exists fs_q_b5ccpe_last_right. d = fs_q_b5ccpe_last_right * S ((S (l)) * e) + (Q))) /\ (((bit = 0 /\ Q = q + q) \/ (bit = 1 /\ Q = S (q + q)))))) -> exists z h. (forall b5cc_index_b5ccpe_after. (exists bcf_lt_gap_b5ccpe_after_bound. bcf_lt_gap_b5ccpe_after_bound + S (b5cc_index_b5ccpe_after) = S l) -> exists b5cc_left_b5ccpe_after b5cc_right_b5ccpe_after b5cc_bit_b5ccpe_after. (((exists fs_h_b5cc_b5ccpe_after_left. fs_h_b5cc_b5ccpe_after_left + S (b5cc_left_b5ccpe_after) = S ((S (b5cc_index_b5ccpe_after)) * c)) /\ exists fs_q_b5cc_b5ccpe_after_left. b = fs_q_b5cc_b5ccpe_after_left * S ((S (b5cc_index_b5ccpe_after)) * c) + (b5cc_left_b5ccpe_after))) /\ ((((exists fs_h_b5cc_b5ccpe_after_right. fs_h_b5cc_b5ccpe_after_right + S (b5cc_right_b5ccpe_after) = S ((S (b5cc_index_b5ccpe_after)) * e)) /\ exists fs_q_b5cc_b5ccpe_after_right. d = fs_q_b5cc_b5ccpe_after_right * S ((S (b5cc_index_b5ccpe_after)) * e) + (b5cc_right_b5ccpe_after))) /\ ((((exists fs_h_b5cc_b5ccpe_after_bit. fs_h_b5cc_b5ccpe_after_bit + S (b5cc_bit_b5ccpe_after) = S ((S (b5cc_index_b5ccpe_after)) * h)) /\ exists fs_q_b5cc_b5ccpe_after_bit. z = fs_q_b5cc_b5ccpe_after_bit * S ((S (b5cc_index_b5ccpe_after)) * h) + (b5cc_bit_b5ccpe_after))) /\ (((b5cc_bit_b5ccpe_after = 0 /\ b5cc_right_b5ccpe_after = b5cc_left_b5ccpe_after + b5cc_left_b5ccpe_after) \/ (b5cc_bit_b5ccpe_after = 1 /\ b5cc_right_b5ccpe_after = S (b5cc_left_b5ccpe_after + b5cc_left_b5ccpe_after)))))))

Proof neighborhood

Direct theorem prerequisites

BT005D beta_prefix_extend BT00AA finite_lt_succ_eq_or_lt

Direct theorem dependents

BT00XX double_quotient_carry_prefix_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

71 script commands · 26 reading checkpoints · 2 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 prefix extendfinite lt succ eq or lt
01Fix variables and assumptionsL1–9

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 f
  6. L6
    intro g
  7. L7
    intro l
  8. L8
    intro hprefix
  9. L9
    intro hlast
02Separate the logical casesL10–14

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

  1. L10
    cases hlast
  2. L11
    cases hlast_witness
  3. L12
    cases hlast_witness_witness
  4. L13
    cases hlast_witness_witness_witness
  5. L14
    cases hlast_witness_witness_witness_right
03Use earlier factsL15–18

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

  1. L15
    specialize beta_prefix_extend l
  2. L16
    specialize beta_prefix_extend f
  3. L17
    specialize beta_prefix_extend g
  4. L18
    specialize beta_prefix_extend x2
04Separate the logical casesL19–21

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

  1. L19
    cases beta_prefix_extend
  2. L20
    cases beta_prefix_extend_witness
  3. L21
    cases beta_prefix_extend_witness_witness
05Construct an explicit witnessL22–23

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

  1. L22
    exists x3
  2. L23
    exists x4
06Fix variables and assumptionsL24–25

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

  1. L24
    intro i
  2. L25
    intro hi
07Use earlier factsL26–27

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

  1. L26
    specialize finite_lt_succ_eq_or_lt l
  2. L27
    specialize finite_lt_succ_eq_or_lt i
08Establish hsplitL28–30

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. L28
    have hsplit : i = l ∨ Lt(i,l)Definitions: Lt(i,l)Original native command in the exact edition
  2. L29
    apply finite_lt_succ_eq_or_lt
  3. L30
    exact hi
09Separate the logical casesL31–31

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

  1. L31
    cases hsplit
10Calculate and transport equalitiesL32–37

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

  1. L32
    rewrite hsplit_left
  2. L33
    rewrite hsplit_left
  3. L34
    rewrite hsplit_left
  4. L35
    rewrite hsplit_left
  5. L36
    rewrite hsplit_left
  6. L37
    rewrite hsplit_left
11Construct an explicit witnessL38–40

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

  1. L38
    exists x
  2. L39
    exists x1
  3. L40
    exists x2
12Separate the logical casesL41–41

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

  1. L41
    split
13Use earlier factsL42–42

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

  1. L42
    exact hlast_witness_witness_witness_left
14Separate the logical casesL43–43

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

  1. L43
    split
15Use earlier factsL44–44

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

  1. L44
    exact hlast_witness_witness_witness_right_left
16Separate the logical casesL45–45

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

  1. L45
    split
17Use earlier factsL46–47

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

  1. L46
    exact beta_prefix_extend_witness_witness_left
  2. L47
    exact hlast_witness_witness_witness_right_right
18Establish holdL48–51

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

  1. L48
    have hold : ∃ q. ∃ Q. ∃ bit. BetaAt(b,c,i,q) ∧ (BetaAt(d,e,i,Q) ∧ (BetaAt(f,g,i,bit) ∧ (bit = 0 ∧ Q = q + q ∨ bit = 1 ∧ Q = S (q + q))))Definitions: BetaAt(b,c,i,q)BetaAt(d,e,i,Q)BetaAt(f,g,i,bit)Original native command in the exact edition
  2. L49
    specialize hprefix i
  3. L50
    apply hprefix
  4. L51
    exact hsplit_right
19Separate the logical casesL52–57

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

  1. L52
    cases hold
  2. L53
    cases hold_witness
  3. L54
    cases hold_witness_witness
  4. L55
    cases hold_witness_witness_witness
  5. L56
    cases hold_witness_witness_witness_right
  6. L57
    cases hold_witness_witness_witness_right_right
20Construct an explicit witnessL58–60

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

  1. L58
    exists x5
  2. L59
    exists x6
  3. L60
    exists x7
21Separate the logical casesL61–61

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

  1. L61
    split
22Use earlier factsL62–62

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

  1. L62
    exact hold_witness_witness_witness_left
23Separate the logical casesL63–63

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

  1. L63
    split
24Use earlier factsL64–64

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

  1. L64
    exact hold_witness_witness_witness_right_left
25Separate the logical casesL65–65

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

  1. L65
    split
26Use earlier factsL66–71

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

  1. L66
    specialize beta_prefix_extend_witness_witness_right i
  2. L67
    specialize beta_prefix_extend_witness_witness_right x7
  3. L68
    apply beta_prefix_extend_witness_witness_right
  4. L69
    exact hsplit_right
  5. L70
    exact hold_witness_witness_witness_right_right_left
  6. L71
    exact hold_witness_witness_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 71 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro f
  6. 0006intro g
  7. 0007intro l
  8. 0008intro hprefix
  9. 0009intro hlast
  10. 0010cases hlast
  11. 0011cases hlast_witness
  12. 0012cases hlast_witness_witness
  13. 0013cases hlast_witness_witness_witness
  14. 0014cases hlast_witness_witness_witness_right
  15. 0015specialize beta_prefix_extend l
  16. 0016specialize beta_prefix_extend f
  17. 0017specialize beta_prefix_extend g
  18. 0018specialize beta_prefix_extend x2
  19. 0019cases beta_prefix_extend
  20. 0020cases beta_prefix_extend_witness
  21. 0021cases beta_prefix_extend_witness_witness
  22. 0022exists x3
  23. 0023exists x4
  24. 0024intro i
  25. 0025intro hi
  26. 0026specialize finite_lt_succ_eq_or_lt l
  27. 0027specialize finite_lt_succ_eq_or_lt i
  28. 0028have hsplit : i = l ∨ Lt(i,l)
    Exact native replay linehave hsplit : i = l \/ exists k. k + S i = l
  29. 0029apply finite_lt_succ_eq_or_lt
  30. 0030exact hi
  31. 0031cases hsplit
  32. 0032rewrite hsplit_left
  33. 0033rewrite hsplit_left
  34. 0034rewrite hsplit_left
  35. 0035rewrite hsplit_left
  36. 0036rewrite hsplit_left
  37. 0037rewrite hsplit_left
  38. 0038exists x
  39. 0039exists x1
  40. 0040exists x2
  41. 0041split
  42. 0042exact hlast_witness_witness_witness_left
  43. 0043split
  44. 0044exact hlast_witness_witness_witness_right_left
  45. 0045split
  46. 0046exact beta_prefix_extend_witness_witness_left
  47. 0047exact hlast_witness_witness_witness_right_right
  48. 0048have hold : ∃ q. ∃ Q. ∃ bit. BetaAt(b,c,i,q) ∧ (BetaAt(d,e,i,Q) ∧ (BetaAt(f,g,i,bit) ∧ (bit = 0 ∧ Q = q + q ∨ bit = 1 ∧ Q = S (q + q))))
    Exact native replay linehave hold : exists q Q bit. (((exists fs_h_b5ccpe_old_left. fs_h_b5ccpe_old_left + S (q) = S ((S (i)) * c)) /\ exists fs_q_b5ccpe_old_left. b = fs_q_b5ccpe_old_left * S ((S (i)) * c) + (q))) /\ ((((exists fs_h_b5ccpe_old_right. fs_h_b5ccpe_old_right + S (Q) = S ((S (i)) * e)) /\ exists fs_q_b5ccpe_old_right. d = fs_q_b5ccpe_old_right * S ((S (i)) * e) + (Q))) /\ ((((exists fs_h_b5ccpe_old_bit. fs_h_b5ccpe_old_bit + S (bit) = S ((S (i)) * g)) /\ exists fs_q_b5ccpe_old_bit. f = fs_q_b5ccpe_old_bit * S ((S (i)) * g) + (bit))) /\ (((bit = 0 /\ Q = q + q) \/ (bit = 1 /\ Q = S (q + q))))))
  49. 0049specialize hprefix i
  50. 0050apply hprefix
  51. 0051exact hsplit_right
  52. 0052cases hold
  53. 0053cases hold_witness
  54. 0054cases hold_witness_witness
  55. 0055cases hold_witness_witness_witness
  56. 0056cases hold_witness_witness_witness_right
  57. 0057cases hold_witness_witness_witness_right_right
  58. 0058exists x5
  59. 0059exists x6
  60. 0060exists x7
  61. 0061split
  62. 0062exact hold_witness_witness_witness_left
  63. 0063split
  64. 0064exact hold_witness_witness_witness_right_left
  65. 0065split
  66. 0066specialize beta_prefix_extend_witness_witness_right i
  67. 0067specialize beta_prefix_extend_witness_witness_right x7
  68. 0068apply beta_prefix_extend_witness_witness_right
  69. 0069exact hsplit_right
  70. 0070exact hold_witness_witness_witness_right_right_left
  71. 0071exact hold_witness_witness_witness_right_right_right