CD000C

finite_bit_count_proper_subset_lt

A witnessed missing member makes a proper subset strictly smaller in exact cardinality.

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. ∀ n. ∀ m. ∀ i. BitCount(b,c,l,n) → BitCount(d,e,l,m) → ModularSetSubset(b,c,d,e,l) → Lt(i,l) → BetaAt(b,c,i,0) → BetaAt(d,e,i,1) → Lt(n,m)

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

Definition DAG

ModularSetSubset(b,c,d,e,p) · 1Lt(a,b) · 2BetaAt(b,c,i,x) · 2BitCount(b,c,l,z) · 2

Actual proof prerequisites

finite_bit_subset_pointwise_lefinite_sum_pointwise_strict_atle_refl · checked external prerequisite
Original expanded first-order statement 
forall b c d e l n m i. (((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 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 ((m)) = 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) + ((m)))) /\ 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)) * (e))) /\ exists ff_q_fms_count_summand. (d) = ff_q_fms_count_summand * S ((S (ff_i_fms_count)) * (e)) + (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)) * (e))) /\ exists ff_q_fms_count_decoded. (d) = ff_q_fms_count_decoded * S ((S (ff_i_fms_count)) * (e)) + (ff_bit_fms_count))) /\ (ff_bit_fms_count = 0 \/ ff_bit_fms_count = 1))))) -> (forall fms_i_subset. (exists fms_gap_subset. fms_gap_subset + S (fms_i_subset) = (l)) -> (((exists fs_h_fms_subset_left. fs_h_fms_subset_left + S (1) = S ((S (fms_i_subset)) * c)) /\ exists fs_q_fms_subset_left. b = fs_q_fms_subset_left * S ((S (fms_i_subset)) * c) + (1))) -> (((exists fs_h_fms_subset_right. fs_h_fms_subset_right + S (1) = S ((S (fms_i_subset)) * e)) /\ exists fs_q_fms_subset_right. d = fs_q_fms_subset_right * S ((S (fms_i_subset)) * e) + (1)))) -> (exists fms_gap_lt. fms_gap_lt + S (i) = (l)) -> (((exists fs_h_fms_proper_zero. fs_h_fms_proper_zero + S (0) = S ((S (i)) * c)) /\ exists fs_q_fms_proper_zero. b = fs_q_fms_proper_zero * S ((S (i)) * c) + (0))) -> (((exists fs_h_fms_proper_one. fs_h_fms_proper_one + S (1) = S ((S (i)) * e)) /\ exists fs_q_fms_proper_one. d = fs_q_fms_proper_one * S ((S (i)) * e) + (1))) -> (exists fms_gap_lt. fms_gap_lt + S (n) = (m))

Complete tactic proof in conservative notation

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

42 script commands · 6 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 (2)
finite sum pointwise strict atfinite bit subset pointwise le
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 l
  6. L6
    intro n
  7. L7
    intro m
  8. L8
    intro i
  9. L9
    intro hn
  10. L10
    intro hm
02Fix variables and assumptionsL11–14

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

  1. L11
    intro hsub
  2. L12
    intro hi
  3. L13
    intro hzero
  4. L14
    intro hone
03Separate the logical casesL15–16

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

  1. L15
    cases hn
  2. L16
    cases hm
04Use earlier factsL17–26

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

  1. L17
    specialize finite_sum_pointwise_strict_at b
  2. L18
    specialize finite_sum_pointwise_strict_at c
  3. L19
    specialize finite_sum_pointwise_strict_at d
  4. L20
    specialize finite_sum_pointwise_strict_at e
  5. L21
    specialize finite_sum_pointwise_strict_at l
  6. L22
    specialize finite_sum_pointwise_strict_at n
  7. L23
    specialize finite_sum_pointwise_strict_at m
  8. L24
    specialize finite_sum_pointwise_strict_at i
  9. L25
    specialize finite_sum_pointwise_strict_at 0
  10. L26
    specialize finite_sum_pointwise_strict_at 1
05Use earlier factsL27–36

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

  1. L27
    apply finite_sum_pointwise_strict_at
  2. L28
    specialize finite_bit_subset_pointwise_le b
  3. L29
    specialize finite_bit_subset_pointwise_le c
  4. L30
    specialize finite_bit_subset_pointwise_le d
  5. L31
    specialize finite_bit_subset_pointwise_le e
  6. L32
    specialize finite_bit_subset_pointwise_le l
  7. L33
    apply finite_bit_subset_pointwise_le
  8. L34
    exact hn_right
  9. L35
    exact hsub
  10. L36
    exact hn_left
06Use earlier factsL37–42

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

  1. L37
    exact hm_left
  2. L38
    exact hi
  3. L39
    exact hzero
  4. L40
    exact hone
  5. L41
    specialize le_refl 1
  6. L42
    apply le_refl

Library-wide reading audit

Original defined command ledger · 42 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro l
  6. 0006intro n
  7. 0007intro m
  8. 0008intro i
  9. 0009intro hn
  10. 0010intro hm
  11. 0011intro hsub
  12. 0012intro hi
  13. 0013intro hzero
  14. 0014intro hone
  15. 0015cases hn
  16. 0016cases hm
  17. 0017specialize finite_sum_pointwise_strict_at b
  18. 0018specialize finite_sum_pointwise_strict_at c
  19. 0019specialize finite_sum_pointwise_strict_at d
  20. 0020specialize finite_sum_pointwise_strict_at e
  21. 0021specialize finite_sum_pointwise_strict_at l
  22. 0022specialize finite_sum_pointwise_strict_at n
  23. 0023specialize finite_sum_pointwise_strict_at m
  24. 0024specialize finite_sum_pointwise_strict_at i
  25. 0025specialize finite_sum_pointwise_strict_at 0
  26. 0026specialize finite_sum_pointwise_strict_at 1
  27. 0027apply finite_sum_pointwise_strict_at
  28. 0028specialize finite_bit_subset_pointwise_le b
  29. 0029specialize finite_bit_subset_pointwise_le c
  30. 0030specialize finite_bit_subset_pointwise_le d
  31. 0031specialize finite_bit_subset_pointwise_le e
  32. 0032specialize finite_bit_subset_pointwise_le l
  33. 0033apply finite_bit_subset_pointwise_le
  34. 0034exact hn_right
  35. 0035exact hsub
  36. 0036exact hn_left
  37. 0037exact hm_left
  38. 0038exact hi
  39. 0039exact hzero
  40. 0040exact hone
  41. 0041specialize le_refl 1
  42. 0042apply le_refl