CD0012

finite_bit_intersection_exists

Construct an actual characteristic intersection code and its exact finite count.

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) ∧ ModularSetIntersection(b,c,d,e,x,y,l)

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

Definition DAG

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

Actual proof prerequisites

beta_pointwise_mul_prefix_exists · checked external prerequisitebeta_at_exists · checked external prerequisitefinite_bit_entry_casesfinite_bit_product_casesbit_count_exists · checked external prerequisitefinite_bit_intersection_from_product
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 98 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

98 script commands · 23 reading checkpoints · 7 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 product casesfinite bit entry casesfinite bit intersection from product
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 hcodeL10–16

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

  1. L10
    have hcode : ∃ u. ∃ v. ∀ fms_i_product. ∀ fms_a_product. ∀ fms_z_product. ∀ fms_w_product. Lt(fms_i_product,l) → BetaAt(b,c,fms_i_product,fms_a_product) → BetaAt(d,e,fms_i_product,fms_z_product) → BetaAt(u,v,fms_i_product,fms_w_product) → fms_w_product = fms_a_product · fms_z_productDefinitions: Lt(fms_i_product,l)BetaAt(b,c,fms_i_product,fms_a_product)BetaAt(d,e,fms_i_product,fms_z_product)BetaAt(u,v,fms_i_product,fms_w_product)Original native command in the exact edition
  2. L11
    specialize beta_pointwise_mul_prefix_exists b
  3. L12
    specialize beta_pointwise_mul_prefix_exists c
  4. L13
    specialize beta_pointwise_mul_prefix_exists d
  5. L14
    specialize beta_pointwise_mul_prefix_exists e
  6. L15
    specialize beta_pointwise_mul_prefix_exists l
  7. L16
    apply beta_pointwise_mul_prefix_exists
03Separate the logical casesL17–20

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

  1. L17
    cases hcode
  2. L18
    cases hcode_witness
  3. L19
    cases hn
  4. L20
    cases hm
04Establish hbitsL21–23

Establish this local claim before using it. It is not an additional assumption.

  1. L21
    have hbits : AllBits(x,x1,l)Definitions: AllBits(x,x1,l)Original native command in the exact edition
  2. L22
    intro i
  3. L23
    intro hi
05Establish haL24–28

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

  1. L24
    have ha : ∃ a. BetaAt(b,c,i,a)Definitions: BetaAt(b,c,i,a)Original native command in the exact edition
  2. L25
    specialize beta_at_exists b
  3. L26
    specialize beta_at_exists c
  4. L27
    specialize beta_at_exists i
  5. L28
    apply beta_at_exists
06Separate the logical casesL29–29

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

  1. L29
    cases ha
07Establish hbL30–34

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

  1. L30
    have hb : ∃ a. BetaAt(d,e,i,a)Definitions: BetaAt(d,e,i,a)Original native command in the exact edition
  2. L31
    specialize beta_at_exists d
  3. L32
    specialize beta_at_exists e
  4. L33
    specialize beta_at_exists i
  5. L34
    apply beta_at_exists
08Separate the logical casesL35–35

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

  1. L35
    cases hb
09Establish hwL36–40

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

  1. L36
    have hw : ∃ a. BetaAt(x,x1,i,a)Definitions: BetaAt(x,x1,i,a)Original native command in the exact edition
  2. L37
    specialize beta_at_exists x
  3. L38
    specialize beta_at_exists x1
  4. L39
    specialize beta_at_exists i
  5. L40
    apply beta_at_exists
10Separate the logical casesL41–41

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

  1. L41
    cases hw
11Establish heL42–51

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

  1. L42
    have he : x4=x2*x3
  2. L43
    specialize hcode_witness_witness i
  3. L44
    specialize hcode_witness_witness x2
  4. L45
    specialize hcode_witness_witness x3
  5. L46
    specialize hcode_witness_witness x4
  6. L47
    apply hcode_witness_witness
  7. L48
    exact hi
  8. L49
    exact ha_witness
  9. L50
    exact hb_witness
  10. L51
    exact hw_witness
12Construct an explicit witnessL52–52

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

  1. L52
    exists x4
13Separate the logical casesL53–53

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

  1. L53
    split
14Use earlier factsL54–54

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

  1. L54
    exact hw_witness
15Calculate and transport equalitiesL55–56

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

  1. L55
    rewrite he
  2. L56
    rewrite he
16Use earlier factsL57–66

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

  1. L57
    specialize finite_bit_product_cases x2
  2. L58
    specialize finite_bit_product_cases x3
  3. L59
    apply finite_bit_product_cases
  4. L60
    specialize finite_bit_entry_cases b
  5. L61
    specialize finite_bit_entry_cases c
  6. L62
    specialize finite_bit_entry_cases l
  7. L63
    specialize finite_bit_entry_cases i
  8. L64
    specialize finite_bit_entry_cases x2
  9. L65
    apply finite_bit_entry_cases
  10. L66
    exact hn_right
17Use earlier factsL67–76

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

  1. L67
    exact hi
  2. L68
    exact ha_witness
  3. L69
    specialize finite_bit_entry_cases d
  4. L70
    specialize finite_bit_entry_cases e
  5. L71
    specialize finite_bit_entry_cases l
  6. L72
    specialize finite_bit_entry_cases i
  7. L73
    specialize finite_bit_entry_cases x3
  8. L74
    apply finite_bit_entry_cases
  9. L75
    exact hm_right
  10. L76
    exact hi
18Use earlier factsL77–77

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

  1. L77
    exact hb_witness
19Establish hcountL78–83

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

  1. L78
    have hcount : ∃ q. BitCount(x,x1,l,q)Definitions: BitCount(x,x1,l,q)Original native command in the exact edition
  2. L79
    specialize bit_count_exists x
  3. L80
    specialize bit_count_exists x1
  4. L81
    specialize bit_count_exists l
  5. L82
    apply bit_count_exists
  6. L83
    exact hbits
20Separate the logical casesL84–84

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

  1. L84
    cases hcount
21Construct an explicit witnessL85–87

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

  1. L85
    exists x
  2. L86
    exists x1
  3. L87
    exists x2
22Separate the logical casesL88–88

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

  1. L88
    split
23Use earlier factsL89–98

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

  1. L89
    exact hcount_witness
  2. L90
    specialize finite_bit_intersection_from_product b
  3. L91
    specialize finite_bit_intersection_from_product c
  4. L92
    specialize finite_bit_intersection_from_product d
  5. L93
    specialize finite_bit_intersection_from_product e
  6. L94
    specialize finite_bit_intersection_from_product x
  7. L95
    specialize finite_bit_intersection_from_product x1
  8. L96
    specialize finite_bit_intersection_from_product l
  9. L97
    apply finite_bit_intersection_from_product
  10. L98
    exact hcode_witness_witness

Library-wide reading audit

Original defined command ledger · 98 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 hcode : ∃ u. ∃ v. ∀ fms_i_product. ∀ fms_a_product. ∀ fms_z_product. ∀ fms_w_product. Lt(fms_i_product,l) → BetaAt(b,c,fms_i_product,fms_a_product) → BetaAt(d,e,fms_i_product,fms_z_product) → BetaAt(u,v,fms_i_product,fms_w_product) → fms_w_product = fms_a_product · fms_z_product
  11. 0011specialize beta_pointwise_mul_prefix_exists b
  12. 0012specialize beta_pointwise_mul_prefix_exists c
  13. 0013specialize beta_pointwise_mul_prefix_exists d
  14. 0014specialize beta_pointwise_mul_prefix_exists e
  15. 0015specialize beta_pointwise_mul_prefix_exists l
  16. 0016apply beta_pointwise_mul_prefix_exists
  17. 0017cases hcode
  18. 0018cases hcode_witness
  19. 0019cases hn
  20. 0020cases hm
  21. 0021have hbits : AllBits(x,x1,l)
  22. 0022intro i
  23. 0023intro hi
  24. 0024have ha : ∃ a. BetaAt(b,c,i,a)
  25. 0025specialize beta_at_exists b
  26. 0026specialize beta_at_exists c
  27. 0027specialize beta_at_exists i
  28. 0028apply beta_at_exists
  29. 0029cases ha
  30. 0030have hb : ∃ a. BetaAt(d,e,i,a)
  31. 0031specialize beta_at_exists d
  32. 0032specialize beta_at_exists e
  33. 0033specialize beta_at_exists i
  34. 0034apply beta_at_exists
  35. 0035cases hb
  36. 0036have hw : ∃ a. BetaAt(x,x1,i,a)
  37. 0037specialize beta_at_exists x
  38. 0038specialize beta_at_exists x1
  39. 0039specialize beta_at_exists i
  40. 0040apply beta_at_exists
  41. 0041cases hw
  42. 0042have he : x4=x2*x3
  43. 0043specialize hcode_witness_witness i
  44. 0044specialize hcode_witness_witness x2
  45. 0045specialize hcode_witness_witness x3
  46. 0046specialize hcode_witness_witness x4
  47. 0047apply hcode_witness_witness
  48. 0048exact hi
  49. 0049exact ha_witness
  50. 0050exact hb_witness
  51. 0051exact hw_witness
  52. 0052exists x4
  53. 0053split
  54. 0054exact hw_witness
  55. 0055rewrite he
  56. 0056rewrite he
  57. 0057specialize finite_bit_product_cases x2
  58. 0058specialize finite_bit_product_cases x3
  59. 0059apply finite_bit_product_cases
  60. 0060specialize finite_bit_entry_cases b
  61. 0061specialize finite_bit_entry_cases c
  62. 0062specialize finite_bit_entry_cases l
  63. 0063specialize finite_bit_entry_cases i
  64. 0064specialize finite_bit_entry_cases x2
  65. 0065apply finite_bit_entry_cases
  66. 0066exact hn_right
  67. 0067exact hi
  68. 0068exact ha_witness
  69. 0069specialize finite_bit_entry_cases d
  70. 0070specialize finite_bit_entry_cases e
  71. 0071specialize finite_bit_entry_cases l
  72. 0072specialize finite_bit_entry_cases i
  73. 0073specialize finite_bit_entry_cases x3
  74. 0074apply finite_bit_entry_cases
  75. 0075exact hm_right
  76. 0076exact hi
  77. 0077exact hb_witness
  78. 0078have hcount : ∃ q. BitCount(x,x1,l,q)
  79. 0079specialize bit_count_exists x
  80. 0080specialize bit_count_exists x1
  81. 0081specialize bit_count_exists l
  82. 0082apply bit_count_exists
  83. 0083exact hbits
  84. 0084cases hcount
  85. 0085exists x
  86. 0086exists x1
  87. 0087exists x2
  88. 0088split
  89. 0089exact hcount_witness
  90. 0090specialize finite_bit_intersection_from_product b
  91. 0091specialize finite_bit_intersection_from_product c
  92. 0092specialize finite_bit_intersection_from_product d
  93. 0093specialize finite_bit_intersection_from_product e
  94. 0094specialize finite_bit_intersection_from_product x
  95. 0095specialize finite_bit_intersection_from_product x1
  96. 0096specialize finite_bit_intersection_from_product l
  97. 0097apply finite_bit_intersection_from_product
  98. 0098exact hcode_witness_witness