CD003B

finite_modular_dyson_lower_zero_member

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

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

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

Definition DAG

ModularSetMember(b,c,p,x) · 7Lt(a,b) · 1ModEq(m,a,b) · 4BetaAt(b,c,i,x) · 8

Actual proof prerequisites

zero_add · checked external prerequisitemod_eq_refl · checked external prerequisite
Original expanded first-order 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)))))

Complete tactic proof in conservative notation

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

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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: BetaAt(u,v,0,1)BetaAt(d,e,0,1)ModularSetMember(b,c,p,x)ModEq(p,0 + t,x)Original native command in the exact edition
  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 defined 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 : (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))
  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