CD0014

finite_bit_complement_member_iff

Membership in the constructed complement is exactly constructive nonmembership in its source.

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. ∀ i. (∀ x. ∀ y. ∀ z. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(d,e,x,z) → y = 0 ∧ z = 1 ∨ y = 1 ∧ z = 0) → Lt(i,l) → (BetaAt(d,e,i,1) → ¬BetaAt(b,c,i,1)) ∧ (¬BetaAt(b,c,i,1) → BetaAt(d,e,i,1))

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

Definition DAG

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

Actual proof prerequisites

beta_at_exists · checked external prerequisitesucc_ne_zero · checked external prerequisite
Original expanded first-order statement 
forall b c d e l i. (forall fms_i_complement fms_a_complement fms_v_complement. (exists fms_gap_complement. fms_gap_complement + S (fms_i_complement) = (l)) -> (((exists fs_h_fms_complement_a. fs_h_fms_complement_a + S (fms_a_complement) = S ((S (fms_i_complement)) * c)) /\ exists fs_q_fms_complement_a. b = fs_q_fms_complement_a * S ((S (fms_i_complement)) * c) + (fms_a_complement))) -> (((exists fs_h_fms_complement_b. fs_h_fms_complement_b + S (fms_v_complement) = S ((S (fms_i_complement)) * e)) /\ exists fs_q_fms_complement_b. d = fs_q_fms_complement_b * S ((S (fms_i_complement)) * e) + (fms_v_complement))) -> ((fms_a_complement=0 /\ fms_v_complement=1) \/ (fms_a_complement=1 /\ fms_v_complement=0))) -> (exists fms_gap_lt. fms_gap_lt + S (i) = (l)) -> ((((((exists fs_h_fms_comp_iff_t. fs_h_fms_comp_iff_t + S (1) = S ((S (i)) * e)) /\ exists fs_q_fms_comp_iff_t. d = fs_q_fms_comp_iff_t * S ((S (i)) * e) + (1))) -> (~(((exists fs_h_fms_comp_iff_s. fs_h_fms_comp_iff_s + S (1) = S ((S (i)) * c)) /\ exists fs_q_fms_comp_iff_s. b = fs_q_fms_comp_iff_s * S ((S (i)) * c) + (1))))) /\ ((~(((exists fs_h_fms_comp_iff_s. fs_h_fms_comp_iff_s + S (1) = S ((S (i)) * c)) /\ exists fs_q_fms_comp_iff_s. b = fs_q_fms_comp_iff_s * S ((S (i)) * c) + (1)))) -> (((exists fs_h_fms_comp_iff_t. fs_h_fms_comp_iff_t + S (1) = S ((S (i)) * e)) /\ exists fs_q_fms_comp_iff_t. d = fs_q_fms_comp_iff_t * S ((S (i)) * e) + (1))))))

Complete tactic proof in conservative notation

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

60 script commands · 21 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.

01Fix variables and assumptionsL1–8

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 i
  7. L7
    intro hcomp
  8. L8
    intro hi
02Separate the logical casesL9–9

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

  1. L9
    split
03Fix variables and assumptionsL10–11

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

  1. L10
    intro ht
  2. L11
    intro hs
04Establish hcL12–19

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

  1. L12
    have hc : (1=0 /\ 1=1) \/ (1=1 /\ 1=0)
  2. L13
    specialize hcomp i
  3. L14
    specialize hcomp 1
  4. L15
    specialize hcomp 1
  5. L16
    apply hcomp
  6. L17
    exact hi
  7. L18
    exact hs
  8. L19
    exact ht
05Separate the logical casesL20–21

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

  1. L20
    cases hc
  2. L21
    cases hc_left
06Use earlier factsL22–24

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

  1. L22
    specialize succ_ne_zero 0
  2. L23
    apply succ_ne_zero
  3. L24
    exact hc_left_left
07Separate the logical casesL25–25

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

  1. L25
    cases hc_right
08Use earlier factsL26–28

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

  1. L26
    specialize succ_ne_zero 0
  2. L27
    apply succ_ne_zero
  3. L28
    exact hc_right_right
09Fix variables and assumptionsL29–29

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

  1. L29
    intro hnot
10Establish haL30–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 ha : ∃ a. BetaAt(b,c,i,a)Definitions: BetaAt(b,c,i,a)Original native command in the exact edition
  2. L31
    specialize beta_at_exists b
  3. L32
    specialize beta_at_exists c
  4. L33
    specialize beta_at_exists i
  5. L34
    apply beta_at_exists
11Separate the logical casesL35–35

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

  1. L35
    cases ha
12Establish hvL36–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 hv : ∃ a. BetaAt(d,e,i,a)Definitions: BetaAt(d,e,i,a)Original native command in the exact edition
  2. L37
    specialize beta_at_exists d
  3. L38
    specialize beta_at_exists e
  4. L39
    specialize beta_at_exists i
  5. L40
    apply beta_at_exists
13Separate the logical casesL41–41

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

  1. L41
    cases hv
14Establish hcL42–49

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

  1. L42
    have hc : (x=0 /\ x1=1) \/ (x=1 /\ x1=0)
  2. L43
    specialize hcomp i
  3. L44
    specialize hcomp x
  4. L45
    specialize hcomp x1
  5. L46
    apply hcomp
  6. L47
    exact hi
  7. L48
    exact ha_witness
  8. L49
    exact hv_witness
15Separate the logical casesL50–51

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

  1. L50
    cases hc
  2. L51
    cases hc_left
16Calculate and transport equalitiesL52–53

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

  1. L52
    rewrite hc_left_right at hv_witness
  2. L53
    rewrite hc_left_right at hv_witness
17Use earlier factsL54–54

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

  1. L54
    exact hv_witness
18Separate the logical casesL55–56

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

  1. L55
    cases hc_right
  2. L56
    exfalso
19Use earlier factsL57–57

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

  1. L57
    apply hnot
20Calculate and transport equalitiesL58–59

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

  1. L58
    rewrite hc_right_left at ha_witness
  2. L59
    rewrite hc_right_left at ha_witness
21Use earlier factsL60–60

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

  1. L60
    exact ha_witness

Library-wide reading audit

Original defined command ledger · 60 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro l
  6. 0006intro i
  7. 0007intro hcomp
  8. 0008intro hi
  9. 0009split
  10. 0010intro ht
  11. 0011intro hs
  12. 0012have hc : (1=0 /\ 1=1) \/ (1=1 /\ 1=0)
  13. 0013specialize hcomp i
  14. 0014specialize hcomp 1
  15. 0015specialize hcomp 1
  16. 0016apply hcomp
  17. 0017exact hi
  18. 0018exact hs
  19. 0019exact ht
  20. 0020cases hc
  21. 0021cases hc_left
  22. 0022specialize succ_ne_zero 0
  23. 0023apply succ_ne_zero
  24. 0024exact hc_left_left
  25. 0025cases hc_right
  26. 0026specialize succ_ne_zero 0
  27. 0027apply succ_ne_zero
  28. 0028exact hc_right_right
  29. 0029intro hnot
  30. 0030have ha : ∃ a. BetaAt(b,c,i,a)
  31. 0031specialize beta_at_exists b
  32. 0032specialize beta_at_exists c
  33. 0033specialize beta_at_exists i
  34. 0034apply beta_at_exists
  35. 0035cases ha
  36. 0036have hv : ∃ a. BetaAt(d,e,i,a)
  37. 0037specialize beta_at_exists d
  38. 0038specialize beta_at_exists e
  39. 0039specialize beta_at_exists i
  40. 0040apply beta_at_exists
  41. 0041cases hv
  42. 0042have hc : (x=0 /\ x1=1) \/ (x=1 /\ x1=0)
  43. 0043specialize hcomp i
  44. 0044specialize hcomp x
  45. 0045specialize hcomp x1
  46. 0046apply hcomp
  47. 0047exact hi
  48. 0048exact ha_witness
  49. 0049exact hv_witness
  50. 0050cases hc
  51. 0051cases hc_left
  52. 0052rewrite hc_left_right at hv_witness
  53. 0053rewrite hc_left_right at hv_witness
  54. 0054exact hv_witness
  55. 0055cases hc_right
  56. 0056exfalso
  57. 0057apply hnot
  58. 0058rewrite hc_right_left at ha_witness
  59. 0059rewrite hc_right_left at ha_witness
  60. 0060exact ha_witness