CD002C

finite_partial_sumset_empty

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 4 declared prerequisites and contains 33 exact native proof lines.

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

Proof neighborhood

Direct dependencies

CD002A finite_beta_zero_code CD0023 finite_bit_zero_nonmember add_eq_zero_right Stable theorem; checked-use authorized succ_ne_zero Stable theorem; checked-use authorized

Direct dependents

CD002F finite_modular_sumset_prefix_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

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.

Named ingredients (2)
finite beta zero codefinite bit zero nonmember
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 exact 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