CD003B

finite_modular_dyson_lower_zero_member

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

When zero belongs to B and the shift belongs to A, zero genuinely belongs to the lower Dyson set.

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 u v p t. (forall cd_output_lower. (exists fms_gap_cd_lower_bound. fms_gap_cd_lower_bound + S (cd_output_lower) = (p)) -> ((((((exists fs_h_cd_lower_result. fs_h_cd_lower_result + S (1) = S ((S (cd_output_lower)) * v)) /\ exists fs_q_cd_lower_result. u = fs_q_cd_lower_result * S ((S (cd_output_lower)) * v) + (1))) -> ((((exists fs_h_cd_lower_old. fs_h_cd_lower_old + S (1) = S ((S (cd_output_lower)) * e)) /\ exists fs_q_cd_lower_old. d = fs_q_cd_lower_old * S ((S (cd_output_lower)) * e) + (1))) /\ (exists cd_source_lower. (((exists fms_gap_cd_lower_member. fms_gap_cd_lower_member + S (cd_source_lower) = (p)) /\ (((exists fs_h_fms_cd_lower_member. fs_h_fms_cd_lower_member + S (1) = S ((S (cd_source_lower)) * c)) /\ exists fs_q_fms_cd_lower_member. b = fs_q_fms_cd_lower_member * S ((S (cd_source_lower)) * c) + (1))))) /\ (exists fms_u_cd_lower_mod fms_v_cd_lower_mod. (cd_output_lower+t) + (p) * fms_u_cd_lower_mod = (cd_source_lower) + (p) * fms_v_cd_lower_mod)))) /\ (((((exists fs_h_cd_lower_old. fs_h_cd_lower_old + S (1) = S ((S (cd_output_lower)) * e)) /\ exists fs_q_cd_lower_old. d = fs_q_cd_lower_old * S ((S (cd_output_lower)) * e) + (1))) /\ (exists cd_source_lower. (((exists fms_gap_cd_lower_member. fms_gap_cd_lower_member + S (cd_source_lower) = (p)) /\ (((exists fs_h_fms_cd_lower_member. fs_h_fms_cd_lower_member + S (1) = S ((S (cd_source_lower)) * c)) /\ exists fs_q_fms_cd_lower_member. b = fs_q_fms_cd_lower_member * S ((S (cd_source_lower)) * c) + (1))))) /\ (exists fms_u_cd_lower_mod fms_v_cd_lower_mod. (cd_output_lower+t) + (p) * fms_u_cd_lower_mod = (cd_source_lower) + (p) * fms_v_cd_lower_mod))) -> (((exists fs_h_cd_lower_result. fs_h_cd_lower_result + S (1) = S ((S (cd_output_lower)) * v)) /\ exists fs_q_cd_lower_result. u = fs_q_cd_lower_result * S ((S (cd_output_lower)) * v) + (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))))) -> (((exists fms_gap_member. fms_gap_member + S (t) = (p)) /\ (((exists fs_h_fms_member. fs_h_fms_member + S (1) = S ((S (t)) * c)) /\ exists fs_q_fms_member. b = fs_q_fms_member * S ((S (t)) * c) + (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)) * v)) /\ exists fs_q_fms_member. u = fs_q_fms_member * S ((S (0)) * v) + (1)))))

Constructive proof overview

Generated structural guide

When zero belongs to B and the shift belongs to A, zero genuinely belongs to the lower Dyson set.

The unchanged tactic script uses 2 declared prerequisites and contains 32 exact native proof lines.

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

Proof neighborhood

Direct dependencies

zero_add Stable theorem; checked-use authorized mod_eq_refl Stable theorem; checked-use authorized

Direct dependents

CD003E finite_modular_dyson_strict_sizes CD0042 prime_cauchy_davenport_normalized_bounded_induction

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

32 script commands · 13 reading checkpoints · 2 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.

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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 u
  6. L6
    intro v
  7. L7
    intro p
  8. L8
    intro t
  9. L9
    intro hlower
  10. L10
    intro hzero
02Fix variables and assumptionsL11–11

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

  1. L11
    intro ht
03Separate the logical casesL12–13

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

  1. L12
    cases hzero
  2. L13
    split
04Use earlier factsL14–14

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

  1. L14
    exact hzero_left
05Establish heL15–18

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

  1. L15
    have he : (BetaAt(u,v,0,1) → BetaAt(d,e,0,1) ∧ (∃ x. ModularSetMember(b,c,p,x) ∧ ModEq(p,0 + t,x))) ∧ (BetaAt(d,e,0,1) ∧ (∃ x. ModularSetMember(b,c,p,x) ∧ ModEq(p,0 + t,x)) → BetaAt(u,v,0,1))Definitions: ModularSetMemberModEqBetaAt
  2. L16
    specialize hlower 0
  3. L17
    apply hlower
  4. L18
    exact hzero_left
06Separate the logical casesL19–19

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

  1. L19
    cases he
07Use earlier factsL20–20

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

  1. L20
    apply he_right
08Separate the logical casesL21–21

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

  1. L21
    split
09Use earlier factsL22–22

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

  1. L22
    exact hzero_right
10Construct an explicit witnessL23–23

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

  1. L23
    exists t
11Separate the logical casesL24–24

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

  1. L24
    split
12Use earlier factsL25–25

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

  1. L25
    exact ht
13Establish hzL26–32

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

  1. L26
    have hz : 0+t=t
  2. L27
    specialize zero_add t
  3. L28
    apply zero_add
  4. L29
    rewrite hz
  5. L30
    specialize mod_eq_refl p
  6. L31
    specialize mod_eq_refl t
  7. L32
    apply mod_eq_refl

Library-wide reading audit

Original exact command ledger · 32 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro u
  6. 0006intro v
  7. 0007intro p
  8. 0008intro t
  9. 0009intro hlower
  10. 0010intro hzero
  11. 0011intro ht
  12. 0012cases hzero
  13. 0013split
  14. 0014exact hzero_left
  15. 0015have he : (((((exists fs_h_cd_lower_zero_V. fs_h_cd_lower_zero_V + S (1) = S ((S (0)) * v)) /\ exists fs_q_cd_lower_zero_V. u = fs_q_cd_lower_zero_V * S ((S (0)) * v) + (1))) -> ((((exists fs_h_cd_lower_zero_B. fs_h_cd_lower_zero_B + S (1) = S ((S (0)) * e)) /\ exists fs_q_cd_lower_zero_B. d = fs_q_cd_lower_zero_B * S ((S (0)) * e) + (1))) /\ exists j. (((exists fms_gap_member. fms_gap_member + S (j) = (p)) /\ (((exists fs_h_fms_member. fs_h_fms_member + S (1) = S ((S (j)) * c)) /\ exists fs_q_fms_member. b = fs_q_fms_member * S ((S (j)) * c) + (1))))) /\ (exists fms_u_mod fms_v_mod. (0+t) + (p) * fms_u_mod = (j) + (p) * fms_v_mod))) /\ (((((exists fs_h_cd_lower_zero_B. fs_h_cd_lower_zero_B + S (1) = S ((S (0)) * e)) /\ exists fs_q_cd_lower_zero_B. d = fs_q_cd_lower_zero_B * S ((S (0)) * e) + (1))) /\ exists j. (((exists fms_gap_member. fms_gap_member + S (j) = (p)) /\ (((exists fs_h_fms_member. fs_h_fms_member + S (1) = S ((S (j)) * c)) /\ exists fs_q_fms_member. b = fs_q_fms_member * S ((S (j)) * c) + (1))))) /\ (exists fms_u_mod fms_v_mod. (0+t) + (p) * fms_u_mod = (j) + (p) * fms_v_mod)) -> (((exists fs_h_cd_lower_zero_V. fs_h_cd_lower_zero_V + S (1) = S ((S (0)) * v)) /\ exists fs_q_cd_lower_zero_V. u = fs_q_cd_lower_zero_V * S ((S (0)) * v) + (1)))))
  16. 0016specialize hlower 0
  17. 0017apply hlower
  18. 0018exact hzero_left
  19. 0019cases he
  20. 0020apply he_right
  21. 0021split
  22. 0022exact hzero_right
  23. 0023exists t
  24. 0024split
  25. 0025exact ht
  26. 0026have hz : 0+t=t
  27. 0027specialize zero_add t
  28. 0028apply zero_add
  29. 0029rewrite hz
  30. 0030specialize mod_eq_refl p
  31. 0031specialize mod_eq_refl t
  32. 0032apply mod_eq_refl