CD000E

finite_bit_count_two_nonzero_member

A characteristic set with at least two elements has a genuine nonzero canonical member.

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. ∀ l. ∀ n. BitCount(b,c,l,n) → Lt(1,n) → ∃ x. ModularSetMember(b,c,l,x) ∧ ¬x = 0

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

Definition DAG

ModularSetMember(b,c,p,x) · 1Lt(a,b) · 4BetaAt(b,c,i,x) · 1BitCount(b,c,l,z) · 1

Actual proof prerequisites

le_trans · checked external prerequisitene_zero_of_one_le · checked external prerequisitenonzero_is_succ · checked external prerequisitebit_count_positive_last_one · checked external prerequisitele_of_succ_le_succ · checked external prerequisite
Original expanded first-order statement 
forall b c l n. (((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 fms_gap_le. fms_gap_le + (2) = (n)) -> exists i. (((exists fms_gap_member. fms_gap_member + S (i) = (l)) /\ (((exists fs_h_fms_member. fs_h_fms_member + S (1) = S ((S (i)) * c)) /\ exists fs_q_fms_member. b = fs_q_fms_member * S ((S (i)) * c) + (1))))) /\ ~(i=0)

Complete tactic proof in conservative notation

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

56 script commands · 17 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–6

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro l
  4. L4
    intro n
  5. L5
    intro hcount
  6. L6
    intro hn
02Establish honeL7–11

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

  1. L7
  2. L8
    specialize le_trans 1
  3. L9
    specialize le_trans 2
  4. L10
    specialize le_trans n
  5. L11
    apply le_trans
03Construct an explicit witnessL12–12

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

  1. L12
    exists 1
04Calculate and transport equalitiesL13–13

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

  1. L13
    simp
05Use earlier factsL14–14

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

  1. L14
    exact hn
06Establish hnonzeroL15–20

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply ne zero of one le.

  1. L15
    have hnonzero : ~(n=0)
  2. L16
    intro hz
  3. L17
    specialize ne_zero_of_one_le n
  4. L18
    apply ne_zero_of_one_le
  5. L19
    exact hone
  6. L20
    exact hz
07Establish hsuccL21–24

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

  1. L21
    have hsucc : exists q. n=S q
  2. L22
    specialize nonzero_is_succ n
  3. L23
    apply nonzero_is_succ
  4. L24
    exact hnonzero
08Separate the logical casesL25–25

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

  1. L25
    cases hsucc
09Calculate and transport equalitiesL26–28

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

  1. L26
    rewrite hsucc_witness at hcount
  2. L27
    rewrite hsucc_witness at hcount
  3. L28
    rewrite hsucc_witness at hn
10Establish hwL29–35

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

  1. L29
    have hw : ∃ i. Lt(i,l) ∧ (BetaAt(b,c,i,1) ∧ Lt(x,S i))Definitions: Lt(i,l)BetaAt(b,c,i,1)Lt(x,S i)Original native command in the exact edition
  2. L30
    specialize bit_count_positive_last_one b
  3. L31
    specialize bit_count_positive_last_one c
  4. L32
    specialize bit_count_positive_last_one l
  5. L33
    specialize bit_count_positive_last_one x
  6. L34
    apply bit_count_positive_last_one
  7. L35
    exact hcount
11Separate the logical casesL36–38

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

  1. L36
    cases hw
  2. L37
    cases hw_witness
  3. L38
    cases hw_witness_right
12Construct an explicit witnessL39–39

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

  1. L39
    exists x1
13Separate the logical casesL40–41

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

  1. L40
    split
  2. L41
    split
14Use earlier factsL42–43

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

  1. L42
    exact hw_witness_left
  2. L43
    exact hw_witness_right_left
15Fix variables and assumptionsL44–44

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

  1. L44
    intro hz
16Use earlier factsL45–54

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

  1. L45
    specialize ne_zero_of_one_le x1
  2. L46
    apply ne_zero_of_one_le
  3. L47
    specialize le_of_succ_le_succ 1
  4. L48
    specialize le_of_succ_le_succ x1
  5. L49
    apply le_of_succ_le_succ
  6. L50
    specialize le_trans 2
  7. L51
    specialize le_trans S x
  8. L52
    specialize le_trans S x1
  9. L53
    apply le_trans
  10. L54
    exact hn
17Use earlier factsL55–56

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

  1. L55
    exact hw_witness_right_right
  2. L56
    exact hz

Library-wide reading audit

Original defined command ledger · 56 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro n
  5. 0005intro hcount
  6. 0006intro hn
  7. 0007have hone : Lt(0,n)
  8. 0008specialize le_trans 1
  9. 0009specialize le_trans 2
  10. 0010specialize le_trans n
  11. 0011apply le_trans
  12. 0012exists 1
  13. 0013simp
  14. 0014exact hn
  15. 0015have hnonzero : ~(n=0)
  16. 0016intro hz
  17. 0017specialize ne_zero_of_one_le n
  18. 0018apply ne_zero_of_one_le
  19. 0019exact hone
  20. 0020exact hz
  21. 0021have hsucc : exists q. n=S q
  22. 0022specialize nonzero_is_succ n
  23. 0023apply nonzero_is_succ
  24. 0024exact hnonzero
  25. 0025cases hsucc
  26. 0026rewrite hsucc_witness at hcount
  27. 0027rewrite hsucc_witness at hcount
  28. 0028rewrite hsucc_witness at hn
  29. 0029have hw : ∃ i. Lt(i,l) ∧ (BetaAt(b,c,i,1) ∧ Lt(x,S i))
  30. 0030specialize bit_count_positive_last_one b
  31. 0031specialize bit_count_positive_last_one c
  32. 0032specialize bit_count_positive_last_one l
  33. 0033specialize bit_count_positive_last_one x
  34. 0034apply bit_count_positive_last_one
  35. 0035exact hcount
  36. 0036cases hw
  37. 0037cases hw_witness
  38. 0038cases hw_witness_right
  39. 0039exists x1
  40. 0040split
  41. 0041split
  42. 0042exact hw_witness_left
  43. 0043exact hw_witness_right_left
  44. 0044intro hz
  45. 0045specialize ne_zero_of_one_le x1
  46. 0046apply ne_zero_of_one_le
  47. 0047specialize le_of_succ_le_succ 1
  48. 0048specialize le_of_succ_le_succ x1
  49. 0049apply le_of_succ_le_succ
  50. 0050specialize le_trans 2
  51. 0051specialize le_trans S x
  52. 0052specialize le_trans S x1
  53. 0053apply le_trans
  54. 0054exact hn
  55. 0055exact hw_witness_right_right
  56. 0056exact hz