CD002B

finite_bit_empty_count

The literal zero code is an actual empty characteristic set with an exact zero sum trace at every ambient size.

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

∀ p. BitCount(0,0,p,0)

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

Definition DAG

BitCount(b,c,l,z) · 1

Actual proof prerequisites

finite_beta_zero_code
Original expanded first-order statement 
forall p. ((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 ((0)) = S ((S ((p))) * ff_v_fms_count)) /\ exists ff_q_fms_count_terminal. ff_u_fms_count = ff_q_fms_count_terminal * S ((S ((p))) * ff_v_fms_count) + ((0)))) /\ forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (p)) -> 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)) * (0))) /\ exists ff_q_fms_count_summand. (0) = ff_q_fms_count_summand * S ((S (ff_i_fms_count)) * (0)) + (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 = (p)) -> 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)) * (0))) /\ exists ff_q_fms_count_decoded. (0) = ff_q_fms_count_decoded * S ((S (ff_i_fms_count)) * (0)) + (ff_bit_fms_count))) /\ (ff_bit_fms_count = 0 \/ ff_bit_fms_count = 1))))

Complete tactic proof in conservative notation

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

33 script commands · 22 reading checkpoints · 0 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 (1)
finite beta zero code
01Fix variables and assumptionsL1–1

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

  1. L1
    intro p
02Separate the logical casesL2–2

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

  1. L2
    split
03Construct an explicit witnessL3–4

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

  1. L3
    exists 0
  2. L4
    exists 0
04Separate the logical casesL5–5

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

  1. L5
    split
05Use earlier factsL6–7

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

  1. L6
    specialize finite_beta_zero_code 0
  2. L7
    apply finite_beta_zero_code
06Separate the logical casesL8–8

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

  1. L8
    split
07Use earlier factsL9–10

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

  1. L9
    specialize finite_beta_zero_code p
  2. L10
    apply finite_beta_zero_code
08Fix variables and assumptionsL11–12

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

  1. L11
    intro i
  2. L12
    intro hi
09Construct an explicit witnessL13–15

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

  1. L13
    exists 0
  2. L14
    exists 0
  3. L15
    exists 0
10Separate the logical casesL16–16

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

  1. L16
    split
11Use earlier factsL17–18

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

  1. L17
    specialize finite_beta_zero_code i
  2. L18
    apply finite_beta_zero_code
12Separate the logical casesL19–19

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

  1. L19
    split
13Use earlier factsL20–21

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

  1. L20
    specialize finite_beta_zero_code i
  2. L21
    apply finite_beta_zero_code
14Separate the logical casesL22–22

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

  1. L22
    split
15Use earlier factsL23–24

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

  1. L23
    specialize finite_beta_zero_code S i
  2. L24
    apply finite_beta_zero_code
16Calculate and transport equalitiesL25–25

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

  1. L25
    simp
17Fix variables and assumptionsL26–27

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

  1. L26
    intro i
  2. L27
    intro hi
18Construct an explicit witnessL28–28

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

  1. L28
    exists 0
19Separate the logical casesL29–29

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

  1. L29
    split
20Use earlier factsL30–31

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

  1. L30
    specialize finite_beta_zero_code i
  2. L31
    apply finite_beta_zero_code
21Separate the logical casesL32–32

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

  1. L32
    left
22Calculate and transport equalitiesL33–33

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

  1. L33
    refl

Library-wide reading audit

Original defined command ledger · 33 lines
  1. 0001intro p
  2. 0002split
  3. 0003exists 0
  4. 0004exists 0
  5. 0005split
  6. 0006specialize finite_beta_zero_code 0
  7. 0007apply finite_beta_zero_code
  8. 0008split
  9. 0009specialize finite_beta_zero_code p
  10. 0010apply finite_beta_zero_code
  11. 0011intro i
  12. 0012intro hi
  13. 0013exists 0
  14. 0014exists 0
  15. 0015exists 0
  16. 0016split
  17. 0017specialize finite_beta_zero_code i
  18. 0018apply finite_beta_zero_code
  19. 0019split
  20. 0020specialize finite_beta_zero_code i
  21. 0021apply finite_beta_zero_code
  22. 0022split
  23. 0023specialize finite_beta_zero_code S i
  24. 0024apply finite_beta_zero_code
  25. 0025simp
  26. 0026intro i
  27. 0027intro hi
  28. 0028exists 0
  29. 0029split
  30. 0030specialize finite_beta_zero_code i
  31. 0031apply finite_beta_zero_code
  32. 0032left
  33. 0033refl