CD0042

prime_cauchy_davenport_normalized_bounded_induction

Ordinary bounded induction on the actual second-set cardinality proves the full normalized Cauchy--Davenport bound using genuine strict Dyson descent.

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

∀ N. ∀ p. ∀ b. ∀ c. ∀ d. ∀ e. ∀ sb. ∀ sc. ∀ k. ∀ l. ∀ m. Prime(p) → BitCount(b,c,p,k) → BitCount(d,e,p,l) → BitCount(sb,sc,p,m) → ¬k = 0 → ModularSetMember(d,e,p,0) → ModularSetSumCover(b,c,d,e,sb,sc,p) → Lt(l,N) → CauchyDavenportBound(p,k,l,m)

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

Definition DAG

ModularSetMember(b,c,p,x) · 4ModularSetSumCover(b,c,d,e,u,v,p) · 2ModularTranslationBoundary(b,c,p,d,a,r) · 1ModularDysonTransform(b,c,d,e,ub,uc,vb,vc,p,t) · 1CauchyDavenportBound(p,k,l,m) · 2Le(a,b) · 1Lt(a,b) · 4Prime(p) · 1BitCount(b,c,l,z) · 5

Actual proof prerequisites

add_eq_zero_right · checked external prerequisitesucc_ne_zero · checked external prerequisitefinite_lt_succ_eq_or_lt · checked external prerequisiteeq_decidable · checked external prerequisitele_refl · checked external prerequisitele_or_lt · checked external prerequisitele_antisymm · checked external prerequisiteone_le_of_ne_zero · checked external prerequisitefinite_bit_member_count_nonzerofinite_modular_singleton_cover_boundprime_modular_normalized_boundary_existsprime_nonzero · checked external prerequisitefinite_modular_dyson_transform_existsfinite_modular_dyson_strict_sizesfinite_modular_dyson_lower_zero_memberfinite_modular_dyson_sum_cover
Original expanded first-order statement 
forall N. forall p b c d e sb sc k l m. ((~(p = 1) /\ forall frp_prime_left_cd_induction_prime frp_prime_right_cd_induction_prime. p = frp_prime_left_cd_induction_prime * frp_prime_right_cd_induction_prime -> frp_prime_left_cd_induction_prime = 1 \/ frp_prime_right_cd_induction_prime = 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 ((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 ((l)) = 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) + ((l)))) /\ 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)) * (e))) /\ exists ff_q_fms_count_summand. (d) = ff_q_fms_count_summand * S ((S (ff_i_fms_count)) * (e)) + (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)) * (e))) /\ exists ff_q_fms_count_decoded. (d) = ff_q_fms_count_decoded * S ((S (ff_i_fms_count)) * (e)) + (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))))) -> ~(k=0) -> (((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))))) -> (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_cd_induction_bound. fms_gap_cd_induction_bound + S (l) = (N)) -> (((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 258 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

258 script commands · 50 reading checkpoints · 12 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 (7)
finite bit member count nonzerofinite modular singleton cover boundprime modular normalized boundary existsfinite modular dyson transform existsfinite modular dyson strict sizesfinite modular dyson lower zero memberfinite modular dyson sum cover
01Induction on NL1–10

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L1
    induction N
  2. L2
    intro p
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro d
  6. L6
    intro e
  7. L7
    intro sb
  8. L8
    intro sc
  9. L9
    intro k
  10. L10
    intro l
02Fix variables and assumptionsL11–19

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

  1. L11
    intro m
  2. L12
    intro hprime
  3. L13
    intro hA
  4. L14
    intro hB
  5. L15
    intro hS
  6. L16
    intro hk
  7. L17
    intro hzero
  8. L18
    intro hcover
  9. L19
    intro hbound
03Separate the logical casesL20–21

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

  1. L20
    exfalso
  2. L21
    cases hbound
04Establish hzL22–31

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

  1. L22
    have hz : S l=0
  2. L23
    specialize add_eq_zero_right x
  3. L24
    specialize add_eq_zero_right S l
  4. L25
    apply add_eq_zero_right
  5. L26
    exact hbound_witness
  6. L27
    specialize succ_ne_zero l
  7. L28
    apply succ_ne_zero
  8. L29
    exact hz
  9. L30
    intro p
  10. L31
    intro b
05Fix variables and assumptionsL32–41

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

  1. L32
    intro c
  2. L33
    intro d
  3. L34
    intro e
  4. L35
    intro sb
  5. L36
    intro sc
  6. L37
    intro k
  7. L38
    intro l
  8. L39
    intro m
  9. L40
    intro hprime
  10. L41
    intro hA
06Fix variables and assumptionsL42–47

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

  1. L42
    intro hB
  2. L43
    intro hS
  3. L44
    intro hk
  4. L45
    intro hzero
  5. L46
    intro hcover
  6. L47
    intro hbound
07Establish hcaseL48–52

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

  1. L48
    have hcase : l = N ∨ Lt(l,N)Definitions: Lt(l,N)Original native command in the exact edition
  2. L49
    specialize finite_lt_succ_eq_or_lt N
  3. L50
    specialize finite_lt_succ_eq_or_lt l
  4. L51
    apply finite_lt_succ_eq_or_lt
  5. L52
    exact hbound
08Separate the logical casesL53–53

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

  1. L53
    cases hcase
09Use earlier factsL54–55

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

  1. L54
    specialize eq_decidable m
  2. L55
    specialize eq_decidable p
10Separate the logical casesL56–57

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

  1. L56
    cases eq_decidable
  2. L57
    left
11Calculate and transport equalitiesL58–58

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

  1. L58
    rewrite eq_decidable_left
12Use earlier factsL59–60

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

  1. L59
    specialize le_refl p
  2. L60
    apply le_refl
13Establish hsmallL61–64

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

  1. L61
    have hsmall : Le(l,1) ∨ Lt(1,l)Definitions: Le(l,1)Lt(1,l)Original native command in the exact edition
  2. L62
    specialize le_or_lt l
  3. L63
    specialize le_or_lt 1
  4. L64
    apply le_or_lt
14Separate the logical casesL65–65

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

  1. L65
    cases hsmall
15Establish hloneL66–75

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

  1. L66
    have hlone : l=1
  2. L67
    specialize le_antisymm l
  3. L68
    specialize le_antisymm 1
  4. L69
    apply le_antisymm
  5. L70
    exact hsmall_left
  6. L71
    specialize one_le_of_ne_zero l
  7. L72
    apply one_le_of_ne_zero
  8. L73
    intro hz
  9. L74
    specialize finite_bit_member_count_nonzero d
  10. L75
    specialize finite_bit_member_count_nonzero e
16Use earlier factsL76–85

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

  1. L76
    specialize finite_bit_member_count_nonzero p
  2. L77
    specialize finite_bit_member_count_nonzero l
  3. L78
    specialize finite_bit_member_count_nonzero 0
  4. L79
    apply finite_bit_member_count_nonzero
  5. L80
    exact hB
  6. L81
    exact hzero
  7. L82
    exact hz
  8. L83
    specialize finite_modular_singleton_cover_bound b
  9. L84
    specialize finite_modular_singleton_cover_bound c
  10. L85
    specialize finite_modular_singleton_cover_bound d
17Use earlier factsL86–95

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

  1. L86
    specialize finite_modular_singleton_cover_bound e
  2. L87
    specialize finite_modular_singleton_cover_bound sb
  3. L88
    specialize finite_modular_singleton_cover_bound sc
  4. L89
    specialize finite_modular_singleton_cover_bound p
  5. L90
    specialize finite_modular_singleton_cover_bound k
  6. L91
    specialize finite_modular_singleton_cover_bound l
  7. L92
    specialize finite_modular_singleton_cover_bound m
  8. L93
    apply finite_modular_singleton_cover_bound
  9. L94
    exact hA
  10. L95
    exact hS
18Use earlier factsL96–98

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

  1. L96
    exact hcover
  2. L97
    exact hzero
  3. L98
    exact hlone
19Establish hboundaryL99–108

Establish this local claim before using it. It is not an additional assumption.

  1. L99
    have hboundary : ∃ h. ∃ t. ∃ r. ModularSetMember(d,e,p,h) ∧ ModularTranslationBoundary(b,c,p,h,t,r)Definitions: ModularSetMember(d,e,p,h)ModularTranslationBoundary(b,c,p,h,t,r)Original native command in the exact edition
  2. L100
    specialize prime_modular_normalized_boundary_exists b
  3. L101
    specialize prime_modular_normalized_boundary_exists c
  4. L102
    specialize prime_modular_normalized_boundary_exists d
  5. L103
    specialize prime_modular_normalized_boundary_exists e
  6. L104
    specialize prime_modular_normalized_boundary_exists sb
  7. L105
    specialize prime_modular_normalized_boundary_exists sc
  8. L106
    specialize prime_modular_normalized_boundary_exists p
  9. L107
    specialize prime_modular_normalized_boundary_exists k
  10. L108
    specialize prime_modular_normalized_boundary_exists l
20Use earlier factsL109–118

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

  1. L109
    specialize prime_modular_normalized_boundary_exists m
  2. L110
    apply prime_modular_normalized_boundary_exists
  3. L111
    exact hprime
  4. L112
    exact hA
  5. L113
    exact hB
  6. L114
    exact hS
  7. L115
    exact hk
  8. L116
    exact hsmall_right
  9. L117
    exact hzero
  10. L118
    exact hcover
21Use earlier factsL119–119

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

  1. L119
    exact eq_decidable_right
22Separate the logical casesL120–123

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

  1. L120
    cases hboundary
  2. L121
    cases hboundary_witness
  3. L122
    cases hboundary_witness_witness
  4. L123
    cases hboundary_witness_witness_witness
23Establish hsourceL124–124

Establish this local claim before using it. It is not an additional assumption.

  1. L124
    have hsource : ModularSetMember(b,c,p,x1)Definitions: ModularSetMember(b,c,p,x1)Original native command in the exact edition
24Separate the logical casesL125–125

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

  1. L125
    cases hboundary_witness_witness_witness_right
25Use earlier factsL126–126

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

  1. L126
    exact hboundary_witness_witness_witness_right_left
26Establish hpzeroL127–132

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

  1. L127
    have hpzero : ~(p=0)
  2. L128
    intro he
  3. L129
    specialize prime_nonzero p
  4. L130
    apply prime_nonzero
  5. L131
    exact hprime
  6. L132
    exact he
27Establish htransformL133–142

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite modular dyson transform exists.

  1. L133
    have htransform : ∃ ub. ∃ uc. ∃ vb. ∃ vc. ∃ K. ∃ L. BitCount(ub,uc,p,K) ∧ (BitCount(vb,vc,p,L) ∧ (K + L = k + l ∧ ModularDysonTransform(b,c,d,e,ub,uc,vb,vc,p,x1)))Definitions: BitCount(ub,uc,p,K)BitCount(vb,vc,p,L)ModularDysonTransform(b,c,d,e,ub,uc,vb,vc,p,x1)Original native command in the exact edition
  2. L134
    specialize finite_modular_dyson_transform_exists b
  3. L135
    specialize finite_modular_dyson_transform_exists c
  4. L136
    specialize finite_modular_dyson_transform_exists d
  5. L137
    specialize finite_modular_dyson_transform_exists e
  6. L138
    specialize finite_modular_dyson_transform_exists p
  7. L139
    specialize finite_modular_dyson_transform_exists k
  8. L140
    specialize finite_modular_dyson_transform_exists l
  9. L141
    specialize finite_modular_dyson_transform_exists x1
  10. L142
    apply finite_modular_dyson_transform_exists
28Use earlier factsL143–145

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

  1. L143
    exact hpzero
  2. L144
    exact hA
  3. L145
    exact hB
29Separate the logical casesL146–146

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

  1. L146
    cases hsource
30Use earlier factsL147–147

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

  1. L147
    exact hsource_left
31Separate the logical casesL148–156

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

  1. L148
    cases htransform
  2. L149
    cases htransform_witness
  3. L150
    cases htransform_witness_witness
  4. L151
    cases htransform_witness_witness_witness
  5. L152
    cases htransform_witness_witness_witness_witness
  6. L153
    cases htransform_witness_witness_witness_witness_witness
  7. L154
    cases htransform_witness_witness_witness_witness_witness_witness
  8. L155
    cases htransform_witness_witness_witness_witness_witness_witness_right
  9. L156
    cases htransform_witness_witness_witness_witness_witness_witness_right_right
32Establish hstrictL157–166

Establish this local claim before using it. It is not an additional assumption.

  1. L157
    have hstrict : ¬x7 = 0 ∧ (¬x8 = 0 ∧ Lt(x8,l))Definitions: Lt(x8,l)Original native command in the exact edition
  2. L158
    specialize finite_modular_dyson_strict_sizes b
  3. L159
    specialize finite_modular_dyson_strict_sizes c
  4. L160
    specialize finite_modular_dyson_strict_sizes d
  5. L161
    specialize finite_modular_dyson_strict_sizes e
  6. L162
    specialize finite_modular_dyson_strict_sizes x3
  7. L163
    specialize finite_modular_dyson_strict_sizes x4
  8. L164
    specialize finite_modular_dyson_strict_sizes x5
  9. L165
    specialize finite_modular_dyson_strict_sizes x6
  10. L166
    specialize finite_modular_dyson_strict_sizes p
33Use earlier factsL167–176

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

  1. L167
    specialize finite_modular_dyson_strict_sizes x1
  2. L168
    specialize finite_modular_dyson_strict_sizes x
  3. L169
    specialize finite_modular_dyson_strict_sizes x2
  4. L170
    specialize finite_modular_dyson_strict_sizes x7
  5. L171
    specialize finite_modular_dyson_strict_sizes x8
  6. L172
    specialize finite_modular_dyson_strict_sizes l
  7. L173
    apply finite_modular_dyson_strict_sizes
  8. L174
    exact htransform_witness_witness_witness_witness_witness_witness_left
  9. L175
    exact htransform_witness_witness_witness_witness_witness_witness_right_left
  10. L176
    exact hB
34Use earlier factsL177–180

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

  1. L177
    exact htransform_witness_witness_witness_witness_witness_witness_right_right_right
  2. L178
    exact hzero
  3. L179
    exact hboundary_witness_witness_witness_left
  4. L180
    exact hboundary_witness_witness_witness_right
35Separate the logical casesL181–182

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

  1. L181
    cases hstrict
  2. L182
    cases hstrict_right
36Establish hzeroVL183–192

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite modular dyson lower zero member.

  1. L183
    have hzeroV : ModularSetMember(x5,x6,p,0)Definitions: ModularSetMember(x5,x6,p,0)Original native command in the exact edition
  2. L184
    specialize finite_modular_dyson_lower_zero_member b
  3. L185
    specialize finite_modular_dyson_lower_zero_member c
  4. L186
    specialize finite_modular_dyson_lower_zero_member d
  5. L187
    specialize finite_modular_dyson_lower_zero_member e
  6. L188
    specialize finite_modular_dyson_lower_zero_member x5
  7. L189
    specialize finite_modular_dyson_lower_zero_member x6
  8. L190
    specialize finite_modular_dyson_lower_zero_member p
  9. L191
    specialize finite_modular_dyson_lower_zero_member x1
  10. L192
    apply finite_modular_dyson_lower_zero_member
37Separate the logical casesL193–193

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

  1. L193
    cases htransform_witness_witness_witness_witness_witness_witness_right_right_right
38Use earlier factsL194–196

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

  1. L194
    exact htransform_witness_witness_witness_witness_witness_witness_right_right_right_right
  2. L195
    exact hzero
  3. L196
    exact hsource
39Establish hnewcoverL197–206

Establish this local claim before using it. It is not an additional assumption.

  1. L197
    have hnewcover : ModularSetSumCover(x3,x4,x5,x6,sb,sc,p)Definitions: ModularSetSumCover(x3,x4,x5,x6,sb,sc,p)Original native command in the exact edition
  2. L198
    specialize finite_modular_dyson_sum_cover b
  3. L199
    specialize finite_modular_dyson_sum_cover c
  4. L200
    specialize finite_modular_dyson_sum_cover d
  5. L201
    specialize finite_modular_dyson_sum_cover e
  6. L202
    specialize finite_modular_dyson_sum_cover x3
  7. L203
    specialize finite_modular_dyson_sum_cover x4
  8. L204
    specialize finite_modular_dyson_sum_cover x5
  9. L205
    specialize finite_modular_dyson_sum_cover x6
  10. L206
    specialize finite_modular_dyson_sum_cover sb
40Use earlier factsL207–212

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

  1. L207
    specialize finite_modular_dyson_sum_cover sc
  2. L208
    specialize finite_modular_dyson_sum_cover p
  3. L209
    specialize finite_modular_dyson_sum_cover x1
  4. L210
    apply finite_modular_dyson_sum_cover
  5. L211
    exact htransform_witness_witness_witness_witness_witness_witness_right_right_right
  6. L212
    exact hcover
41Establish hresultL213–222

Establish this local claim before using it. It is not an additional assumption.

  1. L213
    have hresult : CauchyDavenportBound(p,x7,x8,m)Definitions: CauchyDavenportBound(p,x7,x8,m)Original native command in the exact edition
  2. L214
    specialize IH p
  3. L215
    specialize IH x3
  4. L216
    specialize IH x4
  5. L217
    specialize IH x5
  6. L218
    specialize IH x6
  7. L219
    specialize IH sb
  8. L220
    specialize IH sc
  9. L221
    specialize IH x7
  10. L222
    specialize IH x8
42Use earlier factsL223–231

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

  1. L223
    specialize IH m
  2. L224
    apply IH
  3. L225
    exact hprime
  4. L226
    exact htransform_witness_witness_witness_witness_witness_witness_left
  5. L227
    exact htransform_witness_witness_witness_witness_witness_witness_right_left
  6. L228
    exact hS
  7. L229
    exact hstrict_left
  8. L230
    exact hzeroV
  9. L231
    exact hnewcover
43Calculate and transport equalitiesL232–232

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

  1. L232
    rewrite hcase_left at hstrict_right_right
44Use earlier factsL233–233

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

  1. L233
    exact hstrict_right_right
45Separate the logical casesL234–235

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

  1. L234
    cases hresult
  2. L235
    left
46Use earlier factsL236–236

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

  1. L236
    exact hresult_left
47Separate the logical casesL237–237

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

  1. L237
    right
48Calculate and transport equalitiesL238–238

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

  1. L238
    rewrite htransform_witness_witness_witness_witness_witness_witness_right_right_left at hresult_right
49Use earlier factsL239–248

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

  1. L239
    exact hresult_right
  2. L240
    specialize IH p
  3. L241
    specialize IH b
  4. L242
    specialize IH c
  5. L243
    specialize IH d
  6. L244
    specialize IH e
  7. L245
    specialize IH sb
  8. L246
    specialize IH sc
  9. L247
    specialize IH k
  10. L248
    specialize IH l
50Use earlier factsL249–258

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

  1. L249
    specialize IH m
  2. L250
    apply IH
  3. L251
    exact hprime
  4. L252
    exact hA
  5. L253
    exact hB
  6. L254
    exact hS
  7. L255
    exact hk
  8. L256
    exact hzero
  9. L257
    exact hcover
  10. L258
    exact hcase_right

Library-wide reading audit

Original defined command ledger · 258 lines
  1. 0001induction N
  2. 0002intro p
  3. 0003intro b
  4. 0004intro c
  5. 0005intro d
  6. 0006intro e
  7. 0007intro sb
  8. 0008intro sc
  9. 0009intro k
  10. 0010intro l
  11. 0011intro m
  12. 0012intro hprime
  13. 0013intro hA
  14. 0014intro hB
  15. 0015intro hS
  16. 0016intro hk
  17. 0017intro hzero
  18. 0018intro hcover
  19. 0019intro hbound
  20. 0020exfalso
  21. 0021cases hbound
  22. 0022have hz : S l=0
  23. 0023specialize add_eq_zero_right x
  24. 0024specialize add_eq_zero_right S l
  25. 0025apply add_eq_zero_right
  26. 0026exact hbound_witness
  27. 0027specialize succ_ne_zero l
  28. 0028apply succ_ne_zero
  29. 0029exact hz
  30. 0030intro p
  31. 0031intro b
  32. 0032intro c
  33. 0033intro d
  34. 0034intro e
  35. 0035intro sb
  36. 0036intro sc
  37. 0037intro k
  38. 0038intro l
  39. 0039intro m
  40. 0040intro hprime
  41. 0041intro hA
  42. 0042intro hB
  43. 0043intro hS
  44. 0044intro hk
  45. 0045intro hzero
  46. 0046intro hcover
  47. 0047intro hbound
  48. 0048have hcase : l = N ∨ Lt(l,N)
  49. 0049specialize finite_lt_succ_eq_or_lt N
  50. 0050specialize finite_lt_succ_eq_or_lt l
  51. 0051apply finite_lt_succ_eq_or_lt
  52. 0052exact hbound
  53. 0053cases hcase
  54. 0054specialize eq_decidable m
  55. 0055specialize eq_decidable p
  56. 0056cases eq_decidable
  57. 0057left
  58. 0058rewrite eq_decidable_left
  59. 0059specialize le_refl p
  60. 0060apply le_refl
  61. 0061have hsmall : Le(l,1) ∨ Lt(1,l)
  62. 0062specialize le_or_lt l
  63. 0063specialize le_or_lt 1
  64. 0064apply le_or_lt
  65. 0065cases hsmall
  66. 0066have hlone : l=1
  67. 0067specialize le_antisymm l
  68. 0068specialize le_antisymm 1
  69. 0069apply le_antisymm
  70. 0070exact hsmall_left
  71. 0071specialize one_le_of_ne_zero l
  72. 0072apply one_le_of_ne_zero
  73. 0073intro hz
  74. 0074specialize finite_bit_member_count_nonzero d
  75. 0075specialize finite_bit_member_count_nonzero e
  76. 0076specialize finite_bit_member_count_nonzero p
  77. 0077specialize finite_bit_member_count_nonzero l
  78. 0078specialize finite_bit_member_count_nonzero 0
  79. 0079apply finite_bit_member_count_nonzero
  80. 0080exact hB
  81. 0081exact hzero
  82. 0082exact hz
  83. 0083specialize finite_modular_singleton_cover_bound b
  84. 0084specialize finite_modular_singleton_cover_bound c
  85. 0085specialize finite_modular_singleton_cover_bound d
  86. 0086specialize finite_modular_singleton_cover_bound e
  87. 0087specialize finite_modular_singleton_cover_bound sb
  88. 0088specialize finite_modular_singleton_cover_bound sc
  89. 0089specialize finite_modular_singleton_cover_bound p
  90. 0090specialize finite_modular_singleton_cover_bound k
  91. 0091specialize finite_modular_singleton_cover_bound l
  92. 0092specialize finite_modular_singleton_cover_bound m
  93. 0093apply finite_modular_singleton_cover_bound
  94. 0094exact hA
  95. 0095exact hS
  96. 0096exact hcover
  97. 0097exact hzero
  98. 0098exact hlone
  99. 0099have hboundary : ∃ h. ∃ t. ∃ r. ModularSetMember(d,e,p,h) ∧ ModularTranslationBoundary(b,c,p,h,t,r)
  100. 0100specialize prime_modular_normalized_boundary_exists b
  101. 0101specialize prime_modular_normalized_boundary_exists c
  102. 0102specialize prime_modular_normalized_boundary_exists d
  103. 0103specialize prime_modular_normalized_boundary_exists e
  104. 0104specialize prime_modular_normalized_boundary_exists sb
  105. 0105specialize prime_modular_normalized_boundary_exists sc
  106. 0106specialize prime_modular_normalized_boundary_exists p
  107. 0107specialize prime_modular_normalized_boundary_exists k
  108. 0108specialize prime_modular_normalized_boundary_exists l
  109. 0109specialize prime_modular_normalized_boundary_exists m
  110. 0110apply prime_modular_normalized_boundary_exists
  111. 0111exact hprime
  112. 0112exact hA
  113. 0113exact hB
  114. 0114exact hS
  115. 0115exact hk
  116. 0116exact hsmall_right
  117. 0117exact hzero
  118. 0118exact hcover
  119. 0119exact eq_decidable_right
  120. 0120cases hboundary
  121. 0121cases hboundary_witness
  122. 0122cases hboundary_witness_witness
  123. 0123cases hboundary_witness_witness_witness
  124. 0124have hsource : ModularSetMember(b,c,p,x1)
  125. 0125cases hboundary_witness_witness_witness_right
  126. 0126exact hboundary_witness_witness_witness_right_left
  127. 0127have hpzero : ~(p=0)
  128. 0128intro he
  129. 0129specialize prime_nonzero p
  130. 0130apply prime_nonzero
  131. 0131exact hprime
  132. 0132exact he
  133. 0133have htransform : ∃ ub. ∃ uc. ∃ vb. ∃ vc. ∃ K. ∃ L. BitCount(ub,uc,p,K) ∧ (BitCount(vb,vc,p,L) ∧ (K + L = k + l ∧ ModularDysonTransform(b,c,d,e,ub,uc,vb,vc,p,x1)))
  134. 0134specialize finite_modular_dyson_transform_exists b
  135. 0135specialize finite_modular_dyson_transform_exists c
  136. 0136specialize finite_modular_dyson_transform_exists d
  137. 0137specialize finite_modular_dyson_transform_exists e
  138. 0138specialize finite_modular_dyson_transform_exists p
  139. 0139specialize finite_modular_dyson_transform_exists k
  140. 0140specialize finite_modular_dyson_transform_exists l
  141. 0141specialize finite_modular_dyson_transform_exists x1
  142. 0142apply finite_modular_dyson_transform_exists
  143. 0143exact hpzero
  144. 0144exact hA
  145. 0145exact hB
  146. 0146cases hsource
  147. 0147exact hsource_left
  148. 0148cases htransform
  149. 0149cases htransform_witness
  150. 0150cases htransform_witness_witness
  151. 0151cases htransform_witness_witness_witness
  152. 0152cases htransform_witness_witness_witness_witness
  153. 0153cases htransform_witness_witness_witness_witness_witness
  154. 0154cases htransform_witness_witness_witness_witness_witness_witness
  155. 0155cases htransform_witness_witness_witness_witness_witness_witness_right
  156. 0156cases htransform_witness_witness_witness_witness_witness_witness_right_right
  157. 0157have hstrict : ¬x7 = 0 ∧ (¬x8 = 0 ∧ Lt(x8,l))
  158. 0158specialize finite_modular_dyson_strict_sizes b
  159. 0159specialize finite_modular_dyson_strict_sizes c
  160. 0160specialize finite_modular_dyson_strict_sizes d
  161. 0161specialize finite_modular_dyson_strict_sizes e
  162. 0162specialize finite_modular_dyson_strict_sizes x3
  163. 0163specialize finite_modular_dyson_strict_sizes x4
  164. 0164specialize finite_modular_dyson_strict_sizes x5
  165. 0165specialize finite_modular_dyson_strict_sizes x6
  166. 0166specialize finite_modular_dyson_strict_sizes p
  167. 0167specialize finite_modular_dyson_strict_sizes x1
  168. 0168specialize finite_modular_dyson_strict_sizes x
  169. 0169specialize finite_modular_dyson_strict_sizes x2
  170. 0170specialize finite_modular_dyson_strict_sizes x7
  171. 0171specialize finite_modular_dyson_strict_sizes x8
  172. 0172specialize finite_modular_dyson_strict_sizes l
  173. 0173apply finite_modular_dyson_strict_sizes
  174. 0174exact htransform_witness_witness_witness_witness_witness_witness_left
  175. 0175exact htransform_witness_witness_witness_witness_witness_witness_right_left
  176. 0176exact hB
  177. 0177exact htransform_witness_witness_witness_witness_witness_witness_right_right_right
  178. 0178exact hzero
  179. 0179exact hboundary_witness_witness_witness_left
  180. 0180exact hboundary_witness_witness_witness_right
  181. 0181cases hstrict
  182. 0182cases hstrict_right
  183. 0183have hzeroV : ModularSetMember(x5,x6,p,0)
  184. 0184specialize finite_modular_dyson_lower_zero_member b
  185. 0185specialize finite_modular_dyson_lower_zero_member c
  186. 0186specialize finite_modular_dyson_lower_zero_member d
  187. 0187specialize finite_modular_dyson_lower_zero_member e
  188. 0188specialize finite_modular_dyson_lower_zero_member x5
  189. 0189specialize finite_modular_dyson_lower_zero_member x6
  190. 0190specialize finite_modular_dyson_lower_zero_member p
  191. 0191specialize finite_modular_dyson_lower_zero_member x1
  192. 0192apply finite_modular_dyson_lower_zero_member
  193. 0193cases htransform_witness_witness_witness_witness_witness_witness_right_right_right
  194. 0194exact htransform_witness_witness_witness_witness_witness_witness_right_right_right_right
  195. 0195exact hzero
  196. 0196exact hsource
  197. 0197have hnewcover : ModularSetSumCover(x3,x4,x5,x6,sb,sc,p)
  198. 0198specialize finite_modular_dyson_sum_cover b
  199. 0199specialize finite_modular_dyson_sum_cover c
  200. 0200specialize finite_modular_dyson_sum_cover d
  201. 0201specialize finite_modular_dyson_sum_cover e
  202. 0202specialize finite_modular_dyson_sum_cover x3
  203. 0203specialize finite_modular_dyson_sum_cover x4
  204. 0204specialize finite_modular_dyson_sum_cover x5
  205. 0205specialize finite_modular_dyson_sum_cover x6
  206. 0206specialize finite_modular_dyson_sum_cover sb
  207. 0207specialize finite_modular_dyson_sum_cover sc
  208. 0208specialize finite_modular_dyson_sum_cover p
  209. 0209specialize finite_modular_dyson_sum_cover x1
  210. 0210apply finite_modular_dyson_sum_cover
  211. 0211exact htransform_witness_witness_witness_witness_witness_witness_right_right_right
  212. 0212exact hcover
  213. 0213have hresult : CauchyDavenportBound(p,x7,x8,m)
  214. 0214specialize IH p
  215. 0215specialize IH x3
  216. 0216specialize IH x4
  217. 0217specialize IH x5
  218. 0218specialize IH x6
  219. 0219specialize IH sb
  220. 0220specialize IH sc
  221. 0221specialize IH x7
  222. 0222specialize IH x8
  223. 0223specialize IH m
  224. 0224apply IH
  225. 0225exact hprime
  226. 0226exact htransform_witness_witness_witness_witness_witness_witness_left
  227. 0227exact htransform_witness_witness_witness_witness_witness_witness_right_left
  228. 0228exact hS
  229. 0229exact hstrict_left
  230. 0230exact hzeroV
  231. 0231exact hnewcover
  232. 0232rewrite hcase_left at hstrict_right_right
  233. 0233exact hstrict_right_right
  234. 0234cases hresult
  235. 0235left
  236. 0236exact hresult_left
  237. 0237right
  238. 0238rewrite htransform_witness_witness_witness_witness_witness_witness_right_right_left at hresult_right
  239. 0239exact hresult_right
  240. 0240specialize IH p
  241. 0241specialize IH b
  242. 0242specialize IH c
  243. 0243specialize IH d
  244. 0244specialize IH e
  245. 0245specialize IH sb
  246. 0246specialize IH sc
  247. 0247specialize IH k
  248. 0248specialize IH l
  249. 0249specialize IH m
  250. 0250apply IH
  251. 0251exact hprime
  252. 0252exact hA
  253. 0253exact hB
  254. 0254exact hS
  255. 0255exact hk
  256. 0256exact hzero
  257. 0257exact hcover
  258. 0258exact hcase_right