CD0040

finite_modular_singleton_cover_bound

The normalized singleton case has the exact Cauchy--Davenport bound by genuine subset counting.

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. ∀ sb. ∀ sc. ∀ p. ∀ k. ∀ l. ∀ m. BitCount(b,c,p,k) → BitCount(sb,sc,p,m) → ModularSetSumCover(b,c,d,e,sb,sc,p) → ModularSetMember(d,e,p,0) → l = 1 → CauchyDavenportBound(p,k,l,m)

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

Definition DAG

ModularSetMember(b,c,p,x) · 1ModularSetSumCover(b,c,d,e,u,v,p) · 1CauchyDavenportBound(p,k,l,m) · 1BitCount(b,c,l,z) · 2

Actual proof prerequisites

finite_modular_zero_sum_left_subsetfinite_bit_count_subset_lesucc_le_succ · checked external prerequisite
Original expanded first-order statement 
forall b c d e sb sc p k l m. (((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 ((k)) = 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) + ((k)))) /\ 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)) * (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 = (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)) * (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 ((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) + ((m)))) /\ 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)) * (sc))) /\ exists ff_q_fms_count_summand. (sb) = ff_q_fms_count_summand * S ((S (ff_i_fms_count)) * (sc)) + (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)) * (sc))) /\ exists ff_q_fms_count_decoded. (sb) = ff_q_fms_count_decoded * S ((S (ff_i_fms_count)) * (sc)) + (ff_bit_fms_count))) /\ (ff_bit_fms_count = 0 \/ ff_bit_fms_count = 1))))) -> (forall fms_i_cover fms_j_cover fms_s_cover. (exists fms_gap_cover_i. fms_gap_cover_i + S (fms_i_cover) = (p)) -> (exists fms_gap_cover_j. fms_gap_cover_j + S (fms_j_cover) = (p)) -> (exists fms_gap_cover_s. fms_gap_cover_s + S (fms_s_cover) = (p)) -> (((exists fs_h_fms_cover_left. fs_h_fms_cover_left + S (1) = S ((S (fms_i_cover)) * c)) /\ exists fs_q_fms_cover_left. b = fs_q_fms_cover_left * S ((S (fms_i_cover)) * c) + (1))) -> (((exists fs_h_fms_cover_right. fs_h_fms_cover_right + S (1) = S ((S (fms_j_cover)) * e)) /\ exists fs_q_fms_cover_right. d = fs_q_fms_cover_right * S ((S (fms_j_cover)) * e) + (1))) -> (exists fms_u_cover fms_v_cover. (fms_i_cover + fms_j_cover) + (p) * fms_u_cover = (fms_s_cover) + (p) * fms_v_cover) -> (((exists fs_h_fms_cover_result. fs_h_fms_cover_result + S (1) = S ((S (fms_s_cover)) * sc)) /\ exists fs_q_fms_cover_result. sb = fs_q_fms_cover_result * S ((S (fms_s_cover)) * sc) + (1)))) -> (((exists fms_gap_member. fms_gap_member + S (0) = (p)) /\ (((exists fs_h_fms_member. fs_h_fms_member + S (1) = S ((S (0)) * e)) /\ exists fs_q_fms_member. d = fs_q_fms_member * S ((S (0)) * e) + (1))))) -> l=1 -> (((exists fms_gap_cd_bound_full. fms_gap_cd_bound_full + (p) = (m)) \/ (exists fms_gap_cd_bound_sum. fms_gap_cd_bound_sum + (k+l) = (S (m)))))

Complete tactic proof in conservative notation

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

43 script commands · 7 reading checkpoints · 1 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 bit count subset lefinite modular zero sum left subset
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 sb
  6. L6
    intro sc
  7. L7
    intro p
  8. L8
    intro k
  9. L9
    intro l
  10. L10
    intro m
02Fix variables and assumptionsL11–15

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

  1. L11
    intro hA
  2. L12
    intro hS
  3. L13
    intro hcover
  4. L14
    intro hzero
  5. L15
    intro hl
03Separate the logical casesL16–16

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

  1. L16
    right
04Calculate and transport equalitiesL17–17

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

  1. L17
    rewrite hl
05Establish heL18–27

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

  1. L18
    have he : k+1=S k
  2. L19
    simp
  3. L20
    rewrite he
  4. L21
    specialize succ_le_succ k
  5. L22
    specialize succ_le_succ m
  6. L23
    apply succ_le_succ
  7. L24
    specialize finite_bit_count_subset_le b
  8. L25
    specialize finite_bit_count_subset_le c
  9. L26
    specialize finite_bit_count_subset_le sb
  10. L27
    specialize finite_bit_count_subset_le sc
06Use earlier factsL28–37

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

  1. L28
    specialize finite_bit_count_subset_le p
  2. L29
    specialize finite_bit_count_subset_le k
  3. L30
    specialize finite_bit_count_subset_le m
  4. L31
    apply finite_bit_count_subset_le
  5. L32
    exact hA
  6. L33
    exact hS
  7. L34
    specialize finite_modular_zero_sum_left_subset b
  8. L35
    specialize finite_modular_zero_sum_left_subset c
  9. L36
    specialize finite_modular_zero_sum_left_subset d
  10. L37
    specialize finite_modular_zero_sum_left_subset e
07Use earlier factsL38–43

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

  1. L38
    specialize finite_modular_zero_sum_left_subset sb
  2. L39
    specialize finite_modular_zero_sum_left_subset sc
  3. L40
    specialize finite_modular_zero_sum_left_subset p
  4. L41
    apply finite_modular_zero_sum_left_subset
  5. L42
    exact hcover
  6. L43
    exact hzero

Library-wide reading audit

Original defined command ledger · 43 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro sb
  6. 0006intro sc
  7. 0007intro p
  8. 0008intro k
  9. 0009intro l
  10. 0010intro m
  11. 0011intro hA
  12. 0012intro hS
  13. 0013intro hcover
  14. 0014intro hzero
  15. 0015intro hl
  16. 0016right
  17. 0017rewrite hl
  18. 0018have he : k+1=S k
  19. 0019simp
  20. 0020rewrite he
  21. 0021specialize succ_le_succ k
  22. 0022specialize succ_le_succ m
  23. 0023apply succ_le_succ
  24. 0024specialize finite_bit_count_subset_le b
  25. 0025specialize finite_bit_count_subset_le c
  26. 0026specialize finite_bit_count_subset_le sb
  27. 0027specialize finite_bit_count_subset_le sc
  28. 0028specialize finite_bit_count_subset_le p
  29. 0029specialize finite_bit_count_subset_le k
  30. 0030specialize finite_bit_count_subset_le m
  31. 0031apply finite_bit_count_subset_le
  32. 0032exact hA
  33. 0033exact hS
  34. 0034specialize finite_modular_zero_sum_left_subset b
  35. 0035specialize finite_modular_zero_sum_left_subset c
  36. 0036specialize finite_modular_zero_sum_left_subset d
  37. 0037specialize finite_modular_zero_sum_left_subset e
  38. 0038specialize finite_modular_zero_sum_left_subset sb
  39. 0039specialize finite_modular_zero_sum_left_subset sc
  40. 0040specialize finite_modular_zero_sum_left_subset p
  41. 0041apply finite_modular_zero_sum_left_subset
  42. 0042exact hcover
  43. 0043exact hzero