CD0016

finite_bit_union_exists

Construct an actual beta characteristic union and a genuinely witnessed finite cardinality.

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

∀ b. ∀ c. ∀ d. ∀ e. ∀ l. ∀ n. ∀ m. BitCount(b,c,l,n) → BitCount(d,e,l,m) → ∃ x. ∃ y. ∃ z. BitCount(x,y,l,z) ∧ ModularSetUnion(b,c,d,e,x,y,l)

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

Definition DAG

ModularSetUnion(b,c,d,e,u,v,p) · 1ModularSetIntersection(b,c,d,e,u,v,p) · 1Lt(a,b) · 3BetaAt(b,c,i,x) · 6BitCount(b,c,l,z) · 7

Actual proof prerequisites

finite_bit_complement_existsfinite_bit_intersection_existsfinite_bit_union_of_complements
Original expanded first-order statement 
forall b c d e l n m. (((exists ff_u_fms_count ff_v_fms_count. ((((exists ff_h_fms_count_start. ff_h_fms_count_start + S (0) = S ((S (0)) * ff_v_fms_count)) /\ exists ff_q_fms_count_start. ff_u_fms_count = ff_q_fms_count_start * S ((S (0)) * ff_v_fms_count) + (0))) /\ ((((exists ff_h_fms_count_terminal. ff_h_fms_count_terminal + S ((n)) = S ((S ((l))) * ff_v_fms_count)) /\ exists ff_q_fms_count_terminal. ff_u_fms_count = ff_q_fms_count_terminal * S ((S ((l))) * ff_v_fms_count) + ((n)))) /\ forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (l)) -> exists ff_a_fms_count ff_r_fms_count ff_s_fms_count. ((((exists ff_h_fms_count_summand. ff_h_fms_count_summand + S (ff_a_fms_count) = S ((S (ff_i_fms_count)) * (c))) /\ exists ff_q_fms_count_summand. (b) = ff_q_fms_count_summand * S ((S (ff_i_fms_count)) * (c)) + (ff_a_fms_count))) /\ ((((exists ff_h_fms_count_partial. ff_h_fms_count_partial + S (ff_r_fms_count) = S ((S (ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_partial. ff_u_fms_count = ff_q_fms_count_partial * S ((S (ff_i_fms_count)) * ff_v_fms_count) + (ff_r_fms_count))) /\ ((((exists ff_h_fms_count_successor. ff_h_fms_count_successor + S (ff_s_fms_count) = S ((S (S ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_successor. ff_u_fms_count = ff_q_fms_count_successor * S ((S (S ff_i_fms_count)) * ff_v_fms_count) + (ff_s_fms_count))) /\ ff_s_fms_count = ff_r_fms_count + ff_a_fms_count)))))) /\ (forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (l)) -> exists ff_bit_fms_count. ((((exists ff_h_fms_count_decoded. ff_h_fms_count_decoded + S (ff_bit_fms_count) = S ((S (ff_i_fms_count)) * (c))) /\ exists ff_q_fms_count_decoded. (b) = ff_q_fms_count_decoded * S ((S (ff_i_fms_count)) * (c)) + (ff_bit_fms_count))) /\ (ff_bit_fms_count = 0 \/ ff_bit_fms_count = 1))))) -> (((exists ff_u_fms_count ff_v_fms_count. ((((exists ff_h_fms_count_start. ff_h_fms_count_start + S (0) = S ((S (0)) * ff_v_fms_count)) /\ exists ff_q_fms_count_start. ff_u_fms_count = ff_q_fms_count_start * S ((S (0)) * ff_v_fms_count) + (0))) /\ ((((exists ff_h_fms_count_terminal. ff_h_fms_count_terminal + S ((m)) = S ((S ((l))) * ff_v_fms_count)) /\ exists ff_q_fms_count_terminal. ff_u_fms_count = ff_q_fms_count_terminal * S ((S ((l))) * ff_v_fms_count) + ((m)))) /\ forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (l)) -> exists ff_a_fms_count ff_r_fms_count ff_s_fms_count. ((((exists ff_h_fms_count_summand. ff_h_fms_count_summand + S (ff_a_fms_count) = S ((S (ff_i_fms_count)) * (e))) /\ exists ff_q_fms_count_summand. (d) = ff_q_fms_count_summand * S ((S (ff_i_fms_count)) * (e)) + (ff_a_fms_count))) /\ ((((exists ff_h_fms_count_partial. ff_h_fms_count_partial + S (ff_r_fms_count) = S ((S (ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_partial. ff_u_fms_count = ff_q_fms_count_partial * S ((S (ff_i_fms_count)) * ff_v_fms_count) + (ff_r_fms_count))) /\ ((((exists ff_h_fms_count_successor. ff_h_fms_count_successor + S (ff_s_fms_count) = S ((S (S ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_successor. ff_u_fms_count = ff_q_fms_count_successor * S ((S (S ff_i_fms_count)) * ff_v_fms_count) + (ff_s_fms_count))) /\ ff_s_fms_count = ff_r_fms_count + ff_a_fms_count)))))) /\ (forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (l)) -> exists ff_bit_fms_count. ((((exists ff_h_fms_count_decoded. ff_h_fms_count_decoded + S (ff_bit_fms_count) = S ((S (ff_i_fms_count)) * (e))) /\ exists ff_q_fms_count_decoded. (d) = ff_q_fms_count_decoded * S ((S (ff_i_fms_count)) * (e)) + (ff_bit_fms_count))) /\ (ff_bit_fms_count = 0 \/ ff_bit_fms_count = 1))))) -> exists u v q. (((exists ff_u_fms_count ff_v_fms_count. ((((exists ff_h_fms_count_start. ff_h_fms_count_start + S (0) = S ((S (0)) * ff_v_fms_count)) /\ exists ff_q_fms_count_start. ff_u_fms_count = ff_q_fms_count_start * S ((S (0)) * ff_v_fms_count) + (0))) /\ ((((exists ff_h_fms_count_terminal. ff_h_fms_count_terminal + S ((q)) = S ((S ((l))) * ff_v_fms_count)) /\ exists ff_q_fms_count_terminal. ff_u_fms_count = ff_q_fms_count_terminal * S ((S ((l))) * ff_v_fms_count) + ((q)))) /\ forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (l)) -> exists ff_a_fms_count ff_r_fms_count ff_s_fms_count. ((((exists ff_h_fms_count_summand. ff_h_fms_count_summand + S (ff_a_fms_count) = S ((S (ff_i_fms_count)) * (v))) /\ exists ff_q_fms_count_summand. (u) = ff_q_fms_count_summand * S ((S (ff_i_fms_count)) * (v)) + (ff_a_fms_count))) /\ ((((exists ff_h_fms_count_partial. ff_h_fms_count_partial + S (ff_r_fms_count) = S ((S (ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_partial. ff_u_fms_count = ff_q_fms_count_partial * S ((S (ff_i_fms_count)) * ff_v_fms_count) + (ff_r_fms_count))) /\ ((((exists ff_h_fms_count_successor. ff_h_fms_count_successor + S (ff_s_fms_count) = S ((S (S ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_successor. ff_u_fms_count = ff_q_fms_count_successor * S ((S (S ff_i_fms_count)) * ff_v_fms_count) + (ff_s_fms_count))) /\ ff_s_fms_count = ff_r_fms_count + ff_a_fms_count)))))) /\ (forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (l)) -> exists ff_bit_fms_count. ((((exists ff_h_fms_count_decoded. ff_h_fms_count_decoded + S (ff_bit_fms_count) = S ((S (ff_i_fms_count)) * (v))) /\ exists ff_q_fms_count_decoded. (u) = ff_q_fms_count_decoded * S ((S (ff_i_fms_count)) * (v)) + (ff_bit_fms_count))) /\ (ff_bit_fms_count = 0 \/ ff_bit_fms_count = 1))))) /\ (forall fms_i_binary. (exists fms_gap_binary. fms_gap_binary + S (fms_i_binary) = (l)) -> ((((((exists fs_h_fms_binary_result. fs_h_fms_binary_result + S (1) = S ((S (fms_i_binary)) * v)) /\ exists fs_q_fms_binary_result. u = fs_q_fms_binary_result * S ((S (fms_i_binary)) * v) + (1))) -> (((((exists fs_h_fms_binary_left. fs_h_fms_binary_left + S (1) = S ((S (fms_i_binary)) * c)) /\ exists fs_q_fms_binary_left. b = fs_q_fms_binary_left * S ((S (fms_i_binary)) * c) + (1))) \/ (((exists fs_h_fms_binary_right. fs_h_fms_binary_right + S (1) = S ((S (fms_i_binary)) * e)) /\ exists fs_q_fms_binary_right. d = fs_q_fms_binary_right * S ((S (fms_i_binary)) * e) + (1)))))) /\ ((((((exists fs_h_fms_binary_left. fs_h_fms_binary_left + S (1) = S ((S (fms_i_binary)) * c)) /\ exists fs_q_fms_binary_left. b = fs_q_fms_binary_left * S ((S (fms_i_binary)) * c) + (1))) \/ (((exists fs_h_fms_binary_right. fs_h_fms_binary_right + S (1) = S ((S (fms_i_binary)) * e)) /\ exists fs_q_fms_binary_right. d = fs_q_fms_binary_right * S ((S (fms_i_binary)) * e) + (1))))) -> (((exists fs_h_fms_binary_result. fs_h_fms_binary_result + S (1) = S ((S (fms_i_binary)) * v)) /\ exists fs_q_fms_binary_result. u = fs_q_fms_binary_result * S ((S (fms_i_binary)) * v) + (1)))))))

Complete tactic proof in conservative notation

All 87 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

87 script commands · 16 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)
finite bit complement existsfinite bit intersection existsfinite bit union of complements
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 l
  6. L6
    intro n
  7. L7
    intro m
  8. L8
    intro hn
  9. L9
    intro hm
02Establish hAL10–16

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

  1. L10
    have hA : ∃ u. ∃ v. ∃ q. BitCount(u,v,l,q) ∧ ((∀ x. ∀ y. ∀ z. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(u,v,x,z) → y = 0 ∧ z = 1 ∨ y = 1 ∧ z = 0) ∧ n + q = l)Definitions: BitCount(u,v,l,q)Lt(x,l)BetaAt(b,c,x,y)BetaAt(u,v,x,z)Original native command in the exact edition
  2. L11
    specialize finite_bit_complement_exists b
  3. L12
    specialize finite_bit_complement_exists c
  4. L13
    specialize finite_bit_complement_exists l
  5. L14
    specialize finite_bit_complement_exists n
  6. L15
    apply finite_bit_complement_exists
  7. L16
    exact hn
03Separate the logical casesL17–21

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

  1. L17
    cases hA
  2. L18
    cases hA_witness
  3. L19
    cases hA_witness_witness
  4. L20
    cases hA_witness_witness_witness
  5. L21
    cases hA_witness_witness_witness_right
04Establish hBL22–28

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

  1. L22
    have hB : ∃ u. ∃ v. ∃ q. BitCount(u,v,l,q) ∧ ((∀ x. ∀ y. ∀ z. Lt(x,l) → BetaAt(d,e,x,y) → BetaAt(u,v,x,z) → y = 0 ∧ z = 1 ∨ y = 1 ∧ z = 0) ∧ m + q = l)Definitions: BitCount(u,v,l,q)Lt(x,l)BetaAt(d,e,x,y)BetaAt(u,v,x,z)Original native command in the exact edition
  2. L23
    specialize finite_bit_complement_exists d
  3. L24
    specialize finite_bit_complement_exists e
  4. L25
    specialize finite_bit_complement_exists l
  5. L26
    specialize finite_bit_complement_exists m
  6. L27
    apply finite_bit_complement_exists
  7. L28
    exact hm
05Separate the logical casesL29–33

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

  1. L29
    cases hB
  2. L30
    cases hB_witness
  3. L31
    cases hB_witness_witness
  4. L32
    cases hB_witness_witness_witness
  5. L33
    cases hB_witness_witness_witness_right
06Establish hIL34–43

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

  1. L34
    have hI : ∃ u. ∃ v. ∃ q. BitCount(u,v,l,q) ∧ ModularSetIntersection(x,x1,x3,x4,u,v,l)Definitions: BitCount(u,v,l,q)ModularSetIntersection(x,x1,x3,x4,u,v,l)Original native command in the exact edition
  2. L35
    specialize finite_bit_intersection_exists x
  3. L36
    specialize finite_bit_intersection_exists x1
  4. L37
    specialize finite_bit_intersection_exists x3
  5. L38
    specialize finite_bit_intersection_exists x4
  6. L39
    specialize finite_bit_intersection_exists l
  7. L40
    specialize finite_bit_intersection_exists x2
  8. L41
    specialize finite_bit_intersection_exists x5
  9. L42
    apply finite_bit_intersection_exists
  10. L43
    exact hA_witness_witness_witness_left
07Use earlier factsL44–44

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

  1. L44
    exact hB_witness_witness_witness_left
08Separate the logical casesL45–48

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

  1. L45
    cases hI
  2. L46
    cases hI_witness
  3. L47
    cases hI_witness_witness
  4. L48
    cases hI_witness_witness_witness
09Establish hUL49–55

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

  1. L49
    have hU : ∃ u. ∃ v. ∃ q. BitCount(u,v,l,q) ∧ ((∀ x. ∀ y. ∀ z. Lt(x,l) → BetaAt(x6,x7,x,y) → BetaAt(u,v,x,z) → y = 0 ∧ z = 1 ∨ y = 1 ∧ z = 0) ∧ x8 + q = l)Definitions: BitCount(u,v,l,q)Lt(x,l)BetaAt(x6,x7,x,y)BetaAt(u,v,x,z)Original native command in the exact edition
  2. L50
    specialize finite_bit_complement_exists x6
  3. L51
    specialize finite_bit_complement_exists x7
  4. L52
    specialize finite_bit_complement_exists l
  5. L53
    specialize finite_bit_complement_exists x8
  6. L54
    apply finite_bit_complement_exists
  7. L55
    exact hI_witness_witness_witness_left
10Separate the logical casesL56–60

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

  1. L56
    cases hU
  2. L57
    cases hU_witness
  3. L58
    cases hU_witness_witness
  4. L59
    cases hU_witness_witness_witness
  5. L60
    cases hU_witness_witness_witness_right
11Construct an explicit witnessL61–63

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

  1. L61
    exists x9
  2. L62
    exists x10
  3. L63
    exists x11
12Separate the logical casesL64–64

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

  1. L64
    split
13Use earlier factsL65–65

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

  1. L65
    exact hU_witness_witness_witness_left
14Separate the logical casesL66–67

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

  1. L66
    cases hn
  2. L67
    cases hm
15Use earlier factsL68–77

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

  1. L68
    specialize finite_bit_union_of_complements b
  2. L69
    specialize finite_bit_union_of_complements c
  3. L70
    specialize finite_bit_union_of_complements d
  4. L71
    specialize finite_bit_union_of_complements e
  5. L72
    specialize finite_bit_union_of_complements x
  6. L73
    specialize finite_bit_union_of_complements x1
  7. L74
    specialize finite_bit_union_of_complements x3
  8. L75
    specialize finite_bit_union_of_complements x4
  9. L76
    specialize finite_bit_union_of_complements x6
  10. L77
    specialize finite_bit_union_of_complements x7
16Use earlier factsL78–87

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

  1. L78
    specialize finite_bit_union_of_complements x9
  2. L79
    specialize finite_bit_union_of_complements x10
  3. L80
    specialize finite_bit_union_of_complements l
  4. L81
    apply finite_bit_union_of_complements
  5. L82
    exact hn_right
  6. L83
    exact hm_right
  7. L84
    exact hA_witness_witness_witness_right_left
  8. L85
    exact hB_witness_witness_witness_right_left
  9. L86
    exact hI_witness_witness_witness_right
  10. L87
    exact hU_witness_witness_witness_right_left

Library-wide reading audit

Original defined command ledger · 87 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro l
  6. 0006intro n
  7. 0007intro m
  8. 0008intro hn
  9. 0009intro hm
  10. 0010have hA : ∃ u. ∃ v. ∃ q. BitCount(u,v,l,q) ∧ ((∀ x. ∀ y. ∀ z. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(u,v,x,z) → y = 0 ∧ z = 1 ∨ y = 1 ∧ z = 0) ∧ n + q = l)
  11. 0011specialize finite_bit_complement_exists b
  12. 0012specialize finite_bit_complement_exists c
  13. 0013specialize finite_bit_complement_exists l
  14. 0014specialize finite_bit_complement_exists n
  15. 0015apply finite_bit_complement_exists
  16. 0016exact hn
  17. 0017cases hA
  18. 0018cases hA_witness
  19. 0019cases hA_witness_witness
  20. 0020cases hA_witness_witness_witness
  21. 0021cases hA_witness_witness_witness_right
  22. 0022have hB : ∃ u. ∃ v. ∃ q. BitCount(u,v,l,q) ∧ ((∀ x. ∀ y. ∀ z. Lt(x,l) → BetaAt(d,e,x,y) → BetaAt(u,v,x,z) → y = 0 ∧ z = 1 ∨ y = 1 ∧ z = 0) ∧ m + q = l)
  23. 0023specialize finite_bit_complement_exists d
  24. 0024specialize finite_bit_complement_exists e
  25. 0025specialize finite_bit_complement_exists l
  26. 0026specialize finite_bit_complement_exists m
  27. 0027apply finite_bit_complement_exists
  28. 0028exact hm
  29. 0029cases hB
  30. 0030cases hB_witness
  31. 0031cases hB_witness_witness
  32. 0032cases hB_witness_witness_witness
  33. 0033cases hB_witness_witness_witness_right
  34. 0034have hI : ∃ u. ∃ v. ∃ q. BitCount(u,v,l,q) ∧ ModularSetIntersection(x,x1,x3,x4,u,v,l)
  35. 0035specialize finite_bit_intersection_exists x
  36. 0036specialize finite_bit_intersection_exists x1
  37. 0037specialize finite_bit_intersection_exists x3
  38. 0038specialize finite_bit_intersection_exists x4
  39. 0039specialize finite_bit_intersection_exists l
  40. 0040specialize finite_bit_intersection_exists x2
  41. 0041specialize finite_bit_intersection_exists x5
  42. 0042apply finite_bit_intersection_exists
  43. 0043exact hA_witness_witness_witness_left
  44. 0044exact hB_witness_witness_witness_left
  45. 0045cases hI
  46. 0046cases hI_witness
  47. 0047cases hI_witness_witness
  48. 0048cases hI_witness_witness_witness
  49. 0049have hU : ∃ u. ∃ v. ∃ q. BitCount(u,v,l,q) ∧ ((∀ x. ∀ y. ∀ z. Lt(x,l) → BetaAt(x6,x7,x,y) → BetaAt(u,v,x,z) → y = 0 ∧ z = 1 ∨ y = 1 ∧ z = 0) ∧ x8 + q = l)
  50. 0050specialize finite_bit_complement_exists x6
  51. 0051specialize finite_bit_complement_exists x7
  52. 0052specialize finite_bit_complement_exists l
  53. 0053specialize finite_bit_complement_exists x8
  54. 0054apply finite_bit_complement_exists
  55. 0055exact hI_witness_witness_witness_left
  56. 0056cases hU
  57. 0057cases hU_witness
  58. 0058cases hU_witness_witness
  59. 0059cases hU_witness_witness_witness
  60. 0060cases hU_witness_witness_witness_right
  61. 0061exists x9
  62. 0062exists x10
  63. 0063exists x11
  64. 0064split
  65. 0065exact hU_witness_witness_witness_left
  66. 0066cases hn
  67. 0067cases hm
  68. 0068specialize finite_bit_union_of_complements b
  69. 0069specialize finite_bit_union_of_complements c
  70. 0070specialize finite_bit_union_of_complements d
  71. 0071specialize finite_bit_union_of_complements e
  72. 0072specialize finite_bit_union_of_complements x
  73. 0073specialize finite_bit_union_of_complements x1
  74. 0074specialize finite_bit_union_of_complements x3
  75. 0075specialize finite_bit_union_of_complements x4
  76. 0076specialize finite_bit_union_of_complements x6
  77. 0077specialize finite_bit_union_of_complements x7
  78. 0078specialize finite_bit_union_of_complements x9
  79. 0079specialize finite_bit_union_of_complements x10
  80. 0080specialize finite_bit_union_of_complements l
  81. 0081apply finite_bit_union_of_complements
  82. 0082exact hn_right
  83. 0083exact hm_right
  84. 0084exact hA_witness_witness_witness_right_left
  85. 0085exact hB_witness_witness_witness_right_left
  86. 0086exact hI_witness_witness_witness_right
  87. 0087exact hU_witness_witness_witness_right_left