CD0011

finite_bit_intersection_from_product

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

An actual pointwise product code has exactly the membership of the finite-set intersection.

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.

Exact expanded first-order arithmetic statement

forall b c d e u v l. (forall fms_i_product fms_a_product fms_z_product fms_w_product. (exists fms_gap_product. fms_gap_product + S (fms_i_product) = (l)) -> (((exists fs_h_fms_product_a. fs_h_fms_product_a + S (fms_a_product) = S ((S (fms_i_product)) * c)) /\ exists fs_q_fms_product_a. b = fs_q_fms_product_a * S ((S (fms_i_product)) * c) + (fms_a_product))) -> (((exists fs_h_fms_product_b. fs_h_fms_product_b + S (fms_z_product) = S ((S (fms_i_product)) * e)) /\ exists fs_q_fms_product_b. d = fs_q_fms_product_b * S ((S (fms_i_product)) * e) + (fms_z_product))) -> (((exists fs_h_fms_product_w. fs_h_fms_product_w + S (fms_w_product) = S ((S (fms_i_product)) * v)) /\ exists fs_q_fms_product_w. u = fs_q_fms_product_w * S ((S (fms_i_product)) * v) + (fms_w_product))) -> fms_w_product=fms_a_product*fms_z_product) -> (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)))))))

Constructive proof overview

Generated structural guide

An actual pointwise product code has exactly the membership of the finite-set intersection.

The unchanged tactic script uses 2 declared prerequisites and contains 73 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_at_exists Stable theorem; checked-use authorized mul_eq_one_components Stable theorem; checked-use authorized

Direct dependents

CD0012 finite_bit_intersection_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

73 script commands · 20 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.

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 u
  6. L6
    intro v
  7. L7
    intro l
  8. L8
    intro hproduct
  9. L9
    intro i
  10. L10
    intro hi
02Separate the logical casesL11–11

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

  1. L11
    split
03Fix variables and assumptionsL12–12

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

  1. L12
    intro hone
04Establish haL13–17

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

  1. L13
    have ha : exists a. ((exists fs_h_fms_inter_a. fs_h_fms_inter_a + S (a) = S ((S (i)) * c)) /\ exists fs_q_fms_inter_a. b = fs_q_fms_inter_a * S ((S (i)) * c) + (a))
  2. L14
    specialize beta_at_exists b
  3. L15
    specialize beta_at_exists c
  4. L16
    specialize beta_at_exists i
  5. L17
    apply beta_at_exists
05Separate the logical casesL18–18

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

  1. L18
    cases ha
06Establish hbL19–23

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

  1. L19
    have hb : exists a. ((exists fs_h_fms_inter_b. fs_h_fms_inter_b + S (a) = S ((S (i)) * e)) /\ exists fs_q_fms_inter_b. d = fs_q_fms_inter_b * S ((S (i)) * e) + (a))
  2. L20
    specialize beta_at_exists d
  3. L21
    specialize beta_at_exists e
  4. L22
    specialize beta_at_exists i
  5. L23
    apply beta_at_exists
07Separate the logical casesL24–24

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

  1. L24
    cases hb
08Establish heL25–34

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

  1. L25
    have he : 1=x*x1
  2. L26
    specialize hproduct i
  3. L27
    specialize hproduct x
  4. L28
    specialize hproduct x1
  5. L29
    specialize hproduct 1
  6. L30
    apply hproduct
  7. L31
    exact hi
  8. L32
    exact ha_witness
  9. L33
    exact hb_witness
  10. L34
    exact hone
09Establish honesL35–40

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul eq one components.

  1. L35
    have hones : x=1 /\ x1=1
  2. L36
    specialize mul_eq_one_components x
  3. L37
    specialize mul_eq_one_components x1
  4. L38
    apply mul_eq_one_components
  5. L39
    symm
  6. L40
    exact he
10Separate the logical casesL41–42

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

  1. L41
    cases hones
  2. L42
    split
11Calculate and transport equalitiesL43–44

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

  1. L43
    rewrite hones_left at ha_witness
  2. L44
    rewrite hones_left at ha_witness
12Use earlier factsL45–45

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

  1. L45
    exact ha_witness
13Calculate and transport equalitiesL46–47

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

  1. L46
    rewrite hones_right at hb_witness
  2. L47
    rewrite hones_right at hb_witness
14Use earlier factsL48–48

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

  1. L48
    exact hb_witness
15Fix variables and assumptionsL49–49

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

  1. L49
    intro hboth
16Separate the logical casesL50–50

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

  1. L50
    cases hboth
17Establish hwL51–55

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

  1. L51
    have hw : exists a. ((exists fs_h_fms_inter_w. fs_h_fms_inter_w + S (a) = S ((S (i)) * v)) /\ exists fs_q_fms_inter_w. u = fs_q_fms_inter_w * S ((S (i)) * v) + (a))
  2. L52
    specialize beta_at_exists u
  3. L53
    specialize beta_at_exists v
  4. L54
    specialize beta_at_exists i
  5. L55
    apply beta_at_exists
18Separate the logical casesL56–56

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

  1. L56
    cases hw
19Establish heL57–66

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

  1. L57
    have he : x=1*1
  2. L58
    specialize hproduct i
  3. L59
    specialize hproduct 1
  4. L60
    specialize hproduct 1
  5. L61
    specialize hproduct x
  6. L62
    apply hproduct
  7. L63
    exact hi
  8. L64
    exact hboth_left
  9. L65
    exact hboth_right
  10. L66
    exact hw_witness
20Establish honeL67–73

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

  1. L67
    have hone : x=1
  2. L68
    trans 1*1
  3. L69
    exact he
  4. L70
    simp
  5. L71
    rewrite hone at hw_witness
  6. L72
    rewrite hone at hw_witness
  7. L73
    exact hw_witness

Library-wide reading audit

Original exact command ledger · 73 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro u
  6. 0006intro v
  7. 0007intro l
  8. 0008intro hproduct
  9. 0009intro i
  10. 0010intro hi
  11. 0011split
  12. 0012intro hone
  13. 0013have ha : exists a. ((exists fs_h_fms_inter_a. fs_h_fms_inter_a + S (a) = S ((S (i)) * c)) /\ exists fs_q_fms_inter_a. b = fs_q_fms_inter_a * S ((S (i)) * c) + (a))
  14. 0014specialize beta_at_exists b
  15. 0015specialize beta_at_exists c
  16. 0016specialize beta_at_exists i
  17. 0017apply beta_at_exists
  18. 0018cases ha
  19. 0019have hb : exists a. ((exists fs_h_fms_inter_b. fs_h_fms_inter_b + S (a) = S ((S (i)) * e)) /\ exists fs_q_fms_inter_b. d = fs_q_fms_inter_b * S ((S (i)) * e) + (a))
  20. 0020specialize beta_at_exists d
  21. 0021specialize beta_at_exists e
  22. 0022specialize beta_at_exists i
  23. 0023apply beta_at_exists
  24. 0024cases hb
  25. 0025have he : 1=x*x1
  26. 0026specialize hproduct i
  27. 0027specialize hproduct x
  28. 0028specialize hproduct x1
  29. 0029specialize hproduct 1
  30. 0030apply hproduct
  31. 0031exact hi
  32. 0032exact ha_witness
  33. 0033exact hb_witness
  34. 0034exact hone
  35. 0035have hones : x=1 /\ x1=1
  36. 0036specialize mul_eq_one_components x
  37. 0037specialize mul_eq_one_components x1
  38. 0038apply mul_eq_one_components
  39. 0039symm
  40. 0040exact he
  41. 0041cases hones
  42. 0042split
  43. 0043rewrite hones_left at ha_witness
  44. 0044rewrite hones_left at ha_witness
  45. 0045exact ha_witness
  46. 0046rewrite hones_right at hb_witness
  47. 0047rewrite hones_right at hb_witness
  48. 0048exact hb_witness
  49. 0049intro hboth
  50. 0050cases hboth
  51. 0051have hw : exists a. ((exists fs_h_fms_inter_w. fs_h_fms_inter_w + S (a) = S ((S (i)) * v)) /\ exists fs_q_fms_inter_w. u = fs_q_fms_inter_w * S ((S (i)) * v) + (a))
  52. 0052specialize beta_at_exists u
  53. 0053specialize beta_at_exists v
  54. 0054specialize beta_at_exists i
  55. 0055apply beta_at_exists
  56. 0056cases hw
  57. 0057have he : x=1*1
  58. 0058specialize hproduct i
  59. 0059specialize hproduct 1
  60. 0060specialize hproduct 1
  61. 0061specialize hproduct x
  62. 0062apply hproduct
  63. 0063exact hi
  64. 0064exact hboth_left
  65. 0065exact hboth_right
  66. 0066exact hw_witness
  67. 0067have hone : x=1
  68. 0068trans 1*1
  69. 0069exact he
  70. 0070simp
  71. 0071rewrite hone at hw_witness
  72. 0072rewrite hone at hw_witness
  73. 0073exact hw_witness