CD000E

finite_bit_count_two_nonzero_member

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

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

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 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)

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 5 declared prerequisites and contains 56 exact native proof lines.

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

Proof neighborhood

Direct dependencies

le_trans Stable theorem; checked-use authorized ne_zero_of_one_le Stable theorem; checked-use authorized nonzero_is_succ Stable theorem; checked-use authorized bit_count_positive_last_one Alpha theorem; checked-use authorized le_of_succ_le_succ Stable theorem; checked-use authorized

Direct dependents

CD0041 prime_modular_normalized_boundary_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

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.

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
    have hone : exists fms_gap_le. fms_gap_le + (1) = (n)
  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 : exists i. (exists fms_gap_lt. fms_gap_lt + S (i) = (l)) /\ ((((exists fs_h_fms_two_member. fs_h_fms_two_member + S (1) = S ((S (i)) * c)) /\ exists fs_q_fms_two_member. b = fs_q_fms_two_member * S ((S (i)) * c) + (1))) /\ (exists fms_gap_le. fms_gap_le + (S x) = (S i)))
  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 exact 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 : exists fms_gap_le. fms_gap_le + (1) = (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 : exists i. (exists fms_gap_lt. fms_gap_lt + S (i) = (l)) /\ ((((exists fs_h_fms_two_member. fs_h_fms_two_member + S (1) = S ((S (i)) * c)) /\ exists fs_q_fms_two_member. b = fs_q_fms_two_member * S ((S (i)) * c) + (1))) /\ (exists fms_gap_le. fms_gap_le + (S 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