CD001C

finite_beta_composition_exists

Construct an actual finite beta code for composition of two arbitrary decoded beta functions.

Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not Stable

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.

Sets are complete characteristic-bit codes with actual finite cardinality witnesses. The proof constructs translations and the sumset; no finite-choice oracle, supplied cardinality conclusion, or unproved polynomial-method premise is used.

Exact theorem in conservative defined notation

∀ r. ∀ s. ∀ b. ∀ c. ∀ l. ∃ z. ∃ d. ∀ x. ∀ y. ∀ n. Lt(x,l) → BetaAt(r,s,x,y) → BetaAt(b,c,y,n) → BetaAt(z,d,x,n)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

Lt(a,b) · 2BetaAt(b,c,i,x) · 5

Actual proof prerequisites

beta_prefix_extend · checked external prerequisitebeta_at_exists · checked external prerequisitebeta_at_unique · checked external prerequisitefinite_lt_succ_eq_or_lt · checked external prerequisiteadd_eq_zero_right · checked external prerequisitesucc_ne_zero · checked external prerequisite
Original expanded first-order statement 
forall r s b c l. exists z d. (forall fms_i_compose fms_j_compose fms_v_compose. (exists fms_gap_compose. fms_gap_compose + S (fms_i_compose) = (l)) -> (((exists fs_h_fms_compose_index. fs_h_fms_compose_index + S (fms_j_compose) = S ((S (fms_i_compose)) * s)) /\ exists fs_q_fms_compose_index. r = fs_q_fms_compose_index * S ((S (fms_i_compose)) * s) + (fms_j_compose))) -> (((exists fs_h_fms_compose_source. fs_h_fms_compose_source + S (fms_v_compose) = S ((S (fms_j_compose)) * c)) /\ exists fs_q_fms_compose_source. b = fs_q_fms_compose_source * S ((S (fms_j_compose)) * c) + (fms_v_compose))) -> (((exists fs_h_fms_compose_target. fs_h_fms_compose_target + S (fms_v_compose) = S ((S (fms_i_compose)) * d)) /\ exists fs_q_fms_compose_target. z = fs_q_fms_compose_target * S ((S (fms_i_compose)) * d) + (fms_v_compose))))

Complete tactic proof in conservative notation

All 96 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

96 script commands · 24 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.

01Fix variables and assumptionsL1–4

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

  1. L1
    intro r
  2. L2
    intro s
  3. L3
    intro b
  4. L4
    intro c
02Induction on lL5–5

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

  1. L5
    induction l
03Construct an explicit witnessL6–7

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

  1. L6
    exists 0
  2. L7
    exists 0
04Fix variables and assumptionsL8–13

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

  1. L8
    intro i
  2. L9
    intro j
  3. L10
    intro v
  4. L11
    intro hi
  5. L12
    intro hj
  6. L13
    intro hv
05Separate the logical casesL14–15

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

  1. L14
    exfalso
  2. L15
    cases hi
06Establish hzL16–23

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

  1. L16
    have hz : S i=0
  2. L17
    specialize add_eq_zero_right x
  3. L18
    specialize add_eq_zero_right S i
  4. L19
    apply add_eq_zero_right
  5. L20
    exact hi_witness
  6. L21
    specialize succ_ne_zero i
  7. L22
    apply succ_ne_zero
  8. L23
    exact hz
07Separate the logical casesL24–25

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

  1. L24
    cases IH
  2. L25
    cases IH_witness
08Establish hjL26–30

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

  1. L26
    have hj : ∃ j. BetaAt(r,s,l,j)Definitions: BetaAt(r,s,l,j)Original native command in the exact edition
  2. L27
    specialize beta_at_exists r
  3. L28
    specialize beta_at_exists s
  4. L29
    specialize beta_at_exists l
  5. L30
    apply beta_at_exists
09Separate the logical casesL31–31

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

  1. L31
    cases hj
10Establish hvL32–36

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

  1. L32
    have hv : ∃ v. BetaAt(b,c,x2,v)Definitions: BetaAt(b,c,x2,v)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 x2
  5. L36
    apply beta_at_exists
11Separate the logical casesL37–37

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

  1. L37
    cases hv
12Use earlier factsL38–41

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

  1. L38
    specialize beta_prefix_extend l
  2. L39
    specialize beta_prefix_extend x
  3. L40
    specialize beta_prefix_extend x1
  4. L41
    specialize beta_prefix_extend x3
13Separate the logical casesL42–44

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

  1. L42
    cases beta_prefix_extend
  2. L43
    cases beta_prefix_extend_witness
  3. L44
    cases beta_prefix_extend_witness_witness
14Construct an explicit witnessL45–46

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

  1. L45
    exists x4
  2. L46
    exists x5
15Fix variables and assumptionsL47–52

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

  1. L47
    intro i
  2. L48
    intro j
  3. L49
    intro v
  4. L50
    intro hi
  5. L51
    intro hji
  6. L52
    intro hvj
16Establish hcaseL53–57

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. L53
    have hcase : i = l ∨ Lt(i,l)Definitions: Lt(i,l)Original native command in the exact edition
  2. L54
    specialize finite_lt_succ_eq_or_lt l
  3. L55
    specialize finite_lt_succ_eq_or_lt i
  4. L56
    apply finite_lt_succ_eq_or_lt
  5. L57
    exact hi
17Separate the logical casesL58–58

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

  1. L58
    cases hcase
18Calculate and transport equalitiesL59–60

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

  1. L59
    rewrite hcase_left at hji
  2. L60
    rewrite hcase_left at hji
19Establish hjeqL61–70

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

  1. L61
    have hjeq : j=x2
  2. L62
    specialize beta_at_unique r
  3. L63
    specialize beta_at_unique s
  4. L64
    specialize beta_at_unique l
  5. L65
    specialize beta_at_unique j
  6. L66
    specialize beta_at_unique x2
  7. L67
    apply beta_at_unique
  8. L68
    exact hji
  9. L69
    exact hj_witness
  10. L70
    rewrite hjeq at hvj
20Calculate and transport equalitiesL71–71

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

  1. L71
    rewrite hjeq at hvj
21Establish hveqL72–81

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

  1. L72
    have hveq : v=x3
  2. L73
    specialize beta_at_unique b
  3. L74
    specialize beta_at_unique c
  4. L75
    specialize beta_at_unique x2
  5. L76
    specialize beta_at_unique v
  6. L77
    specialize beta_at_unique x3
  7. L78
    apply beta_at_unique
  8. L79
    exact hvj
  9. L80
    exact hv_witness
  10. L81
    rewrite hcase_left
22Calculate and transport equalitiesL82–84

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

  1. L82
    rewrite hcase_left
  2. L83
    rewrite hveq
  3. L84
    rewrite hveq
23Use earlier factsL85–94

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

  1. L85
    exact beta_prefix_extend_witness_witness_left
  2. L86
    specialize beta_prefix_extend_witness_witness_right i
  3. L87
    specialize beta_prefix_extend_witness_witness_right v
  4. L88
    apply beta_prefix_extend_witness_witness_right
  5. L89
    exact hcase_right
  6. L90
    specialize IH_witness_witness i
  7. L91
    specialize IH_witness_witness j
  8. L92
    specialize IH_witness_witness v
  9. L93
    apply IH_witness_witness
  10. L94
    exact hcase_right
24Use earlier factsL95–96

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

  1. L95
    exact hji
  2. L96
    exact hvj

Library-wide reading audit

Original defined command ledger · 96 lines
  1. 0001intro r
  2. 0002intro s
  3. 0003intro b
  4. 0004intro c
  5. 0005induction l
  6. 0006exists 0
  7. 0007exists 0
  8. 0008intro i
  9. 0009intro j
  10. 0010intro v
  11. 0011intro hi
  12. 0012intro hj
  13. 0013intro hv
  14. 0014exfalso
  15. 0015cases hi
  16. 0016have hz : S i=0
  17. 0017specialize add_eq_zero_right x
  18. 0018specialize add_eq_zero_right S i
  19. 0019apply add_eq_zero_right
  20. 0020exact hi_witness
  21. 0021specialize succ_ne_zero i
  22. 0022apply succ_ne_zero
  23. 0023exact hz
  24. 0024cases IH
  25. 0025cases IH_witness
  26. 0026have hj : ∃ j. BetaAt(r,s,l,j)
  27. 0027specialize beta_at_exists r
  28. 0028specialize beta_at_exists s
  29. 0029specialize beta_at_exists l
  30. 0030apply beta_at_exists
  31. 0031cases hj
  32. 0032have hv : ∃ v. BetaAt(b,c,x2,v)
  33. 0033specialize beta_at_exists b
  34. 0034specialize beta_at_exists c
  35. 0035specialize beta_at_exists x2
  36. 0036apply beta_at_exists
  37. 0037cases hv
  38. 0038specialize beta_prefix_extend l
  39. 0039specialize beta_prefix_extend x
  40. 0040specialize beta_prefix_extend x1
  41. 0041specialize beta_prefix_extend x3
  42. 0042cases beta_prefix_extend
  43. 0043cases beta_prefix_extend_witness
  44. 0044cases beta_prefix_extend_witness_witness
  45. 0045exists x4
  46. 0046exists x5
  47. 0047intro i
  48. 0048intro j
  49. 0049intro v
  50. 0050intro hi
  51. 0051intro hji
  52. 0052intro hvj
  53. 0053have hcase : i = l ∨ Lt(i,l)
  54. 0054specialize finite_lt_succ_eq_or_lt l
  55. 0055specialize finite_lt_succ_eq_or_lt i
  56. 0056apply finite_lt_succ_eq_or_lt
  57. 0057exact hi
  58. 0058cases hcase
  59. 0059rewrite hcase_left at hji
  60. 0060rewrite hcase_left at hji
  61. 0061have hjeq : j=x2
  62. 0062specialize beta_at_unique r
  63. 0063specialize beta_at_unique s
  64. 0064specialize beta_at_unique l
  65. 0065specialize beta_at_unique j
  66. 0066specialize beta_at_unique x2
  67. 0067apply beta_at_unique
  68. 0068exact hji
  69. 0069exact hj_witness
  70. 0070rewrite hjeq at hvj
  71. 0071rewrite hjeq at hvj
  72. 0072have hveq : v=x3
  73. 0073specialize beta_at_unique b
  74. 0074specialize beta_at_unique c
  75. 0075specialize beta_at_unique x2
  76. 0076specialize beta_at_unique v
  77. 0077specialize beta_at_unique x3
  78. 0078apply beta_at_unique
  79. 0079exact hvj
  80. 0080exact hv_witness
  81. 0081rewrite hcase_left
  82. 0082rewrite hcase_left
  83. 0083rewrite hveq
  84. 0084rewrite hveq
  85. 0085exact beta_prefix_extend_witness_witness_left
  86. 0086specialize beta_prefix_extend_witness_witness_right i
  87. 0087specialize beta_prefix_extend_witness_witness_right v
  88. 0088apply beta_prefix_extend_witness_witness_right
  89. 0089exact hcase_right
  90. 0090specialize IH_witness_witness i
  91. 0091specialize IH_witness_witness j
  92. 0092specialize IH_witness_witness v
  93. 0093apply IH_witness_witness
  94. 0094exact hcase_right
  95. 0095exact hji
  96. 0096exact hvj