CD002C

finite_partial_sumset_empty

The actual empty code is exactly the sumset restricted to the empty second-coordinate prefix.

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. ∀ p. ∀ fms_z_partial. Lt(fms_z_partial,p) → (BetaAt(0,0,fms_z_partial,1) → ∃ x. ∃ y. ModularSetMember(b,c,p,x) ∧ (ModularSetMember(d,e,p,y) ∧ (Lt(y,0) ∧ ModEq(p,x + y,fms_z_partial)))) ∧ ((∃ x. ∃ y. ModularSetMember(b,c,p,x) ∧ (ModularSetMember(d,e,p,y) ∧ (Lt(y,0) ∧ ModEq(p,x + y,fms_z_partial)))) → BetaAt(0,0,fms_z_partial,1))

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

Definition DAG

ModularSetMember(b,c,p,x) · 4Lt(a,b) · 3ModEq(m,a,b) · 2BetaAt(b,c,i,x) · 2

Actual proof prerequisites

finite_beta_zero_codefinite_bit_zero_nonmemberadd_eq_zero_right · checked external prerequisitesucc_ne_zero · checked external prerequisite
Original expanded first-order statement 
forall b c d e p. forall fms_z_partial. (exists fms_gap_partial_bound. fms_gap_partial_bound + S (fms_z_partial) = (p)) -> ((((((exists fs_h_fms_partial_result. fs_h_fms_partial_result + S (1) = S ((S (fms_z_partial)) * 0)) /\ exists fs_q_fms_partial_result. 0 = fs_q_fms_partial_result * S ((S (fms_z_partial)) * 0) + (1))) -> (exists fms_first_partial fms_second_partial. (((exists fms_gap_partial_left. fms_gap_partial_left + S (fms_first_partial) = (p)) /\ (((exists fs_h_fms_partial_left. fs_h_fms_partial_left + S (1) = S ((S (fms_first_partial)) * c)) /\ exists fs_q_fms_partial_left. b = fs_q_fms_partial_left * S ((S (fms_first_partial)) * c) + (1))))) /\ ((((exists fms_gap_partial_right. fms_gap_partial_right + S (fms_second_partial) = (p)) /\ (((exists fs_h_fms_partial_right. fs_h_fms_partial_right + S (1) = S ((S (fms_second_partial)) * e)) /\ exists fs_q_fms_partial_right. d = fs_q_fms_partial_right * S ((S (fms_second_partial)) * e) + (1))))) /\ ((exists fms_gap_partial_cutoff. fms_gap_partial_cutoff + S (fms_second_partial) = (0)) /\ (exists fms_u_partial_congruence fms_v_partial_congruence. (fms_first_partial+fms_second_partial) + (p) * fms_u_partial_congruence = (fms_z_partial) + (p) * fms_v_partial_congruence))))) /\ ((exists fms_first_partial fms_second_partial. (((exists fms_gap_partial_left. fms_gap_partial_left + S (fms_first_partial) = (p)) /\ (((exists fs_h_fms_partial_left. fs_h_fms_partial_left + S (1) = S ((S (fms_first_partial)) * c)) /\ exists fs_q_fms_partial_left. b = fs_q_fms_partial_left * S ((S (fms_first_partial)) * c) + (1))))) /\ ((((exists fms_gap_partial_right. fms_gap_partial_right + S (fms_second_partial) = (p)) /\ (((exists fs_h_fms_partial_right. fs_h_fms_partial_right + S (1) = S ((S (fms_second_partial)) * e)) /\ exists fs_q_fms_partial_right. d = fs_q_fms_partial_right * S ((S (fms_second_partial)) * e) + (1))))) /\ ((exists fms_gap_partial_cutoff. fms_gap_partial_cutoff + S (fms_second_partial) = (0)) /\ (exists fms_u_partial_congruence fms_v_partial_congruence. (fms_first_partial+fms_second_partial) + (p) * fms_u_partial_congruence = (fms_z_partial) + (p) * fms_v_partial_congruence)))) -> (((exists fs_h_fms_partial_result. fs_h_fms_partial_result + S (1) = S ((S (fms_z_partial)) * 0)) /\ exists fs_q_fms_partial_result. 0 = fs_q_fms_partial_result * S ((S (fms_z_partial)) * 0) + (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 · 8 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 zero nonmemberfinite beta zero code
01Fix variables and assumptionsL1–7

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 p
  6. L6
    intro z
  7. L7
    intro hz
02Separate the logical casesL8–8

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

  1. L8
    split
03Fix variables and assumptionsL9–9

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

  1. L9
    intro hmember
04Separate the logical casesL10–10

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

  1. L10
    exfalso
05Use earlier factsL11–17

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

  1. L11
    specialize finite_bit_zero_nonmember 0
  2. L12
    specialize finite_bit_zero_nonmember 0
  3. L13
    specialize finite_bit_zero_nonmember z
  4. L14
    apply finite_bit_zero_nonmember
  5. L15
    specialize finite_beta_zero_code z
  6. L16
    apply finite_beta_zero_code
  7. L17
    exact hmember
06Fix variables and assumptionsL18–18

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

  1. L18
    intro hw
07Separate the logical casesL19–25

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

  1. L19
    cases hw
  2. L20
    cases hw_witness
  3. L21
    cases hw_witness_witness
  4. L22
    cases hw_witness_witness_right
  5. L23
    cases hw_witness_witness_right_right
  6. L24
    cases hw_witness_witness_right_right_left
  7. L25
    exfalso
08Establish hzeroL26–33

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add eq zero right.

  1. L26
    have hzero : S x1=0
  2. L27
    specialize add_eq_zero_right x2
  3. L28
    specialize add_eq_zero_right S x1
  4. L29
    apply add_eq_zero_right
  5. L30
    exact hw_witness_witness_right_right_left_witness
  6. L31
    specialize succ_ne_zero x1
  7. L32
    apply succ_ne_zero
  8. L33
    exact hzero

Library-wide reading audit

Original defined command ledger · 33 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro p
  6. 0006intro z
  7. 0007intro hz
  8. 0008split
  9. 0009intro hmember
  10. 0010exfalso
  11. 0011specialize finite_bit_zero_nonmember 0
  12. 0012specialize finite_bit_zero_nonmember 0
  13. 0013specialize finite_bit_zero_nonmember z
  14. 0014apply finite_bit_zero_nonmember
  15. 0015specialize finite_beta_zero_code z
  16. 0016apply finite_beta_zero_code
  17. 0017exact hmember
  18. 0018intro hw
  19. 0019cases hw
  20. 0020cases hw_witness
  21. 0021cases hw_witness_witness
  22. 0022cases hw_witness_witness_right
  23. 0023cases hw_witness_witness_right_right
  24. 0024cases hw_witness_witness_right_right_left
  25. 0025exfalso
  26. 0026have hzero : S x1=0
  27. 0027specialize add_eq_zero_right x2
  28. 0028specialize add_eq_zero_right S x1
  29. 0029apply add_eq_zero_right
  30. 0030exact hw_witness_witness_right_right_left_witness
  31. 0031specialize succ_ne_zero x1
  32. 0032apply succ_ne_zero
  33. 0033exact hzero