CD0038

finite_modular_dyson_transform_exists

Construct both actual Dyson-transform sets and their exact cardinalities, preserving the sum of the two input sizes.

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. ∀ k. ∀ l. ∀ t. ¬p = 0 → BitCount(b,c,p,k) → BitCount(d,e,p,l) → Lt(t,p) → ∃ x. ∃ y. ∃ z. ∃ n. ∃ m. ∃ i. BitCount(x,y,p,m) ∧ (BitCount(z,n,p,i) ∧ (m + i = k + l ∧ ModularDysonTransform(b,c,d,e,x,y,z,n,p,t)))

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

Definition DAG

ModularSetUnion(b,c,d,e,u,v,p) · 1ModularSetIntersection(b,c,d,e,u,v,p) · 1ModularSetPullback(b,c,d,e,p,t) · 2ModularDysonTransform(b,c,d,e,ub,uc,vb,vc,p,t) · 1Lt(a,b) · 1BitCount(b,c,l,z) · 8

Actual proof prerequisites

finite_modular_additive_complementfinite_modular_set_pullback_existsfinite_bit_union_existsfinite_bit_intersection_existsfinite_bit_union_intersection_count_balancefinite_modular_dyson_upper_from_unionfinite_modular_dyson_lower_from_pullback
Original expanded first-order statement 
forall b c d e p k l t. ~(p=0) -> (((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 fms_gap_lt. fms_gap_lt + S (t) = (p)) -> exists ub uc vb vc K L. (((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)) * (uc))) /\ exists ff_q_fms_count_summand. (ub) = ff_q_fms_count_summand * S ((S (ff_i_fms_count)) * (uc)) + (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)) * (uc))) /\ exists ff_q_fms_count_decoded. (ub) = ff_q_fms_count_decoded * S ((S (ff_i_fms_count)) * (uc)) + (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)) * (vc))) /\ exists ff_q_fms_count_summand. (vb) = ff_q_fms_count_summand * S ((S (ff_i_fms_count)) * (vc)) + (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)) * (vc))) /\ exists ff_q_fms_count_decoded. (vb) = ff_q_fms_count_decoded * S ((S (ff_i_fms_count)) * (vc)) + (ff_bit_fms_count))) /\ (ff_bit_fms_count = 0 \/ ff_bit_fms_count = 1))))) /\ (K+L=k+l /\ (((forall cd_output_dyson_upper. (exists fms_gap_cd_dyson_upper_bound. fms_gap_cd_dyson_upper_bound + S (cd_output_dyson_upper) = (p)) -> ((((((exists fs_h_cd_dyson_upper_result. fs_h_cd_dyson_upper_result + S (1) = S ((S (cd_output_dyson_upper)) * uc)) /\ exists fs_q_cd_dyson_upper_result. ub = fs_q_cd_dyson_upper_result * S ((S (cd_output_dyson_upper)) * uc) + (1))) -> ((((exists fs_h_cd_dyson_upper_old. fs_h_cd_dyson_upper_old + S (1) = S ((S (cd_output_dyson_upper)) * c)) /\ exists fs_q_cd_dyson_upper_old. b = fs_q_cd_dyson_upper_old * S ((S (cd_output_dyson_upper)) * c) + (1))) \/ (exists cd_source_dyson_upper. (((exists fms_gap_cd_dyson_upper_member. fms_gap_cd_dyson_upper_member + S (cd_source_dyson_upper) = (p)) /\ (((exists fs_h_fms_cd_dyson_upper_member. fs_h_fms_cd_dyson_upper_member + S (1) = S ((S (cd_source_dyson_upper)) * e)) /\ exists fs_q_fms_cd_dyson_upper_member. d = fs_q_fms_cd_dyson_upper_member * S ((S (cd_source_dyson_upper)) * e) + (1))))) /\ (exists fms_u_cd_dyson_upper_mod fms_v_cd_dyson_upper_mod. (cd_source_dyson_upper+t) + (p) * fms_u_cd_dyson_upper_mod = (cd_output_dyson_upper) + (p) * fms_v_cd_dyson_upper_mod)))) /\ (((((exists fs_h_cd_dyson_upper_old. fs_h_cd_dyson_upper_old + S (1) = S ((S (cd_output_dyson_upper)) * c)) /\ exists fs_q_cd_dyson_upper_old. b = fs_q_cd_dyson_upper_old * S ((S (cd_output_dyson_upper)) * c) + (1))) \/ (exists cd_source_dyson_upper. (((exists fms_gap_cd_dyson_upper_member. fms_gap_cd_dyson_upper_member + S (cd_source_dyson_upper) = (p)) /\ (((exists fs_h_fms_cd_dyson_upper_member. fs_h_fms_cd_dyson_upper_member + S (1) = S ((S (cd_source_dyson_upper)) * e)) /\ exists fs_q_fms_cd_dyson_upper_member. d = fs_q_fms_cd_dyson_upper_member * S ((S (cd_source_dyson_upper)) * e) + (1))))) /\ (exists fms_u_cd_dyson_upper_mod fms_v_cd_dyson_upper_mod. (cd_source_dyson_upper+t) + (p) * fms_u_cd_dyson_upper_mod = (cd_output_dyson_upper) + (p) * fms_v_cd_dyson_upper_mod))) -> (((exists fs_h_cd_dyson_upper_result. fs_h_cd_dyson_upper_result + S (1) = S ((S (cd_output_dyson_upper)) * uc)) /\ exists fs_q_cd_dyson_upper_result. ub = fs_q_cd_dyson_upper_result * S ((S (cd_output_dyson_upper)) * uc) + (1))))))) /\ (forall cd_output_dyson_lower. (exists fms_gap_cd_dyson_lower_bound. fms_gap_cd_dyson_lower_bound + S (cd_output_dyson_lower) = (p)) -> ((((((exists fs_h_cd_dyson_lower_result. fs_h_cd_dyson_lower_result + S (1) = S ((S (cd_output_dyson_lower)) * vc)) /\ exists fs_q_cd_dyson_lower_result. vb = fs_q_cd_dyson_lower_result * S ((S (cd_output_dyson_lower)) * vc) + (1))) -> ((((exists fs_h_cd_dyson_lower_old. fs_h_cd_dyson_lower_old + S (1) = S ((S (cd_output_dyson_lower)) * e)) /\ exists fs_q_cd_dyson_lower_old. d = fs_q_cd_dyson_lower_old * S ((S (cd_output_dyson_lower)) * e) + (1))) /\ (exists cd_source_dyson_lower. (((exists fms_gap_cd_dyson_lower_member. fms_gap_cd_dyson_lower_member + S (cd_source_dyson_lower) = (p)) /\ (((exists fs_h_fms_cd_dyson_lower_member. fs_h_fms_cd_dyson_lower_member + S (1) = S ((S (cd_source_dyson_lower)) * c)) /\ exists fs_q_fms_cd_dyson_lower_member. b = fs_q_fms_cd_dyson_lower_member * S ((S (cd_source_dyson_lower)) * c) + (1))))) /\ (exists fms_u_cd_dyson_lower_mod fms_v_cd_dyson_lower_mod. (cd_output_dyson_lower+t) + (p) * fms_u_cd_dyson_lower_mod = (cd_source_dyson_lower) + (p) * fms_v_cd_dyson_lower_mod)))) /\ (((((exists fs_h_cd_dyson_lower_old. fs_h_cd_dyson_lower_old + S (1) = S ((S (cd_output_dyson_lower)) * e)) /\ exists fs_q_cd_dyson_lower_old. d = fs_q_cd_dyson_lower_old * S ((S (cd_output_dyson_lower)) * e) + (1))) /\ (exists cd_source_dyson_lower. (((exists fms_gap_cd_dyson_lower_member. fms_gap_cd_dyson_lower_member + S (cd_source_dyson_lower) = (p)) /\ (((exists fs_h_fms_cd_dyson_lower_member. fs_h_fms_cd_dyson_lower_member + S (1) = S ((S (cd_source_dyson_lower)) * c)) /\ exists fs_q_fms_cd_dyson_lower_member. b = fs_q_fms_cd_dyson_lower_member * S ((S (cd_source_dyson_lower)) * c) + (1))))) /\ (exists fms_u_cd_dyson_lower_mod fms_v_cd_dyson_lower_mod. (cd_output_dyson_lower+t) + (p) * fms_u_cd_dyson_lower_mod = (cd_source_dyson_lower) + (p) * fms_v_cd_dyson_lower_mod))) -> (((exists fs_h_cd_dyson_lower_result. fs_h_cd_dyson_lower_result + S (1) = S ((S (cd_output_dyson_lower)) * vc)) /\ exists fs_q_cd_dyson_lower_result. vb = fs_q_cd_dyson_lower_result * S ((S (cd_output_dyson_lower)) * vc) + (1)))))))))))

Complete tactic proof in conservative notation

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

139 script commands · 27 reading checkpoints · 5 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 modular additive complementfinite modular set pullback existsfinite bit union existsfinite bit intersection existsfinite bit union intersection count balancefinite modular dyson upper from unionfinite modular dyson lower from pullback
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 p
  6. L6
    intro k
  7. L7
    intro l
  8. L8
    intro t
  9. L9
    intro hp
  10. L10
    intro hA
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hB
  2. L12
    intro ht
03Establish hcompL13–17

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

  1. L13
    have hcomp : exists v. t+v=p
  2. L14
    specialize finite_modular_additive_complement p
  3. L15
    specialize finite_modular_additive_complement t
  4. L16
    apply finite_modular_additive_complement
  5. L17
    exact ht
04Separate the logical casesL18–18

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

  1. L18
    cases hcomp
05Establish hTL19–27

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

  1. L19
    have hT : ∃ tb. ∃ tc. BitCount(tb,tc,p,l) ∧ ModularSetPullback(d,e,tb,tc,p,x)Definitions: BitCount(tb,tc,p,l)ModularSetPullback(d,e,tb,tc,p,x)Original native command in the exact edition
  2. L20
    specialize finite_modular_set_pullback_exists d
  3. L21
    specialize finite_modular_set_pullback_exists e
  4. L22
    specialize finite_modular_set_pullback_exists p
  5. L23
    specialize finite_modular_set_pullback_exists l
  6. L24
    specialize finite_modular_set_pullback_exists x
  7. L25
    apply finite_modular_set_pullback_exists
  8. L26
    exact hp
  9. L27
    exact hB
06Separate the logical casesL28–30

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

  1. L28
    cases hT
  2. L29
    cases hT_witness
  3. L30
    cases hT_witness_witness
07Establish hUL31–40

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

  1. L31
    have hU : ∃ ub. ∃ uc. ∃ K. BitCount(ub,uc,p,K) ∧ ModularSetUnion(b,c,x1,x2,ub,uc,p)Definitions: BitCount(ub,uc,p,K)ModularSetUnion(b,c,x1,x2,ub,uc,p)Original native command in the exact edition
  2. L32
    specialize finite_bit_union_exists b
  3. L33
    specialize finite_bit_union_exists c
  4. L34
    specialize finite_bit_union_exists x1
  5. L35
    specialize finite_bit_union_exists x2
  6. L36
    specialize finite_bit_union_exists p
  7. L37
    specialize finite_bit_union_exists k
  8. L38
    specialize finite_bit_union_exists l
  9. L39
    apply finite_bit_union_exists
  10. L40
    exact hA
08Use earlier factsL41–41

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

  1. L41
    exact hT_witness_witness_left
09Separate the logical casesL42–45

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

  1. L42
    cases hU
  2. L43
    cases hU_witness
  3. L44
    cases hU_witness_witness
  4. L45
    cases hU_witness_witness_witness
10Establish hIL46–55

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

  1. L46
    have hI : ∃ ib. ∃ ic. ∃ L. BitCount(ib,ic,p,L) ∧ ModularSetIntersection(b,c,x1,x2,ib,ic,p)Definitions: BitCount(ib,ic,p,L)ModularSetIntersection(b,c,x1,x2,ib,ic,p)Original native command in the exact edition
  2. L47
    specialize finite_bit_intersection_exists b
  3. L48
    specialize finite_bit_intersection_exists c
  4. L49
    specialize finite_bit_intersection_exists x1
  5. L50
    specialize finite_bit_intersection_exists x2
  6. L51
    specialize finite_bit_intersection_exists p
  7. L52
    specialize finite_bit_intersection_exists k
  8. L53
    specialize finite_bit_intersection_exists l
  9. L54
    apply finite_bit_intersection_exists
  10. L55
    exact hA
11Use earlier factsL56–56

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

  1. L56
    exact hT_witness_witness_left
12Separate the logical casesL57–60

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

  1. L57
    cases hI
  2. L58
    cases hI_witness
  3. L59
    cases hI_witness_witness
  4. L60
    cases hI_witness_witness_witness
13Establish hVL61–69

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

  1. L61
    have hV : ∃ vb. ∃ vc. BitCount(vb,vc,p,x8) ∧ ModularSetPullback(x6,x7,vb,vc,p,t)Definitions: BitCount(vb,vc,p,x8)ModularSetPullback(x6,x7,vb,vc,p,t)Original native command in the exact edition
  2. L62
    specialize finite_modular_set_pullback_exists x6
  3. L63
    specialize finite_modular_set_pullback_exists x7
  4. L64
    specialize finite_modular_set_pullback_exists p
  5. L65
    specialize finite_modular_set_pullback_exists x8
  6. L66
    specialize finite_modular_set_pullback_exists t
  7. L67
    apply finite_modular_set_pullback_exists
  8. L68
    exact hp
  9. L69
    exact hI_witness_witness_witness_left
14Separate the logical casesL70–72

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

  1. L70
    cases hV
  2. L71
    cases hV_witness
  3. L72
    cases hV_witness_witness
15Construct an explicit witnessL73–78

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

  1. L73
    exists x3
  2. L74
    exists x4
  3. L75
    exists x9
  4. L76
    exists x10
  5. L77
    exists x5
  6. L78
    exists x8
16Separate the logical casesL79–79

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

  1. L79
    split
17Use earlier factsL80–80

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

  1. L80
    exact hU_witness_witness_witness_left
18Separate the logical casesL81–81

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

  1. L81
    split
19Use earlier factsL82–82

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

  1. L82
    exact hV_witness_witness_left
20Separate the logical casesL83–83

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

  1. L83
    split
21Use earlier factsL84–93

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

  1. L84
    specialize finite_bit_union_intersection_count_balance b
  2. L85
    specialize finite_bit_union_intersection_count_balance c
  3. L86
    specialize finite_bit_union_intersection_count_balance x1
  4. L87
    specialize finite_bit_union_intersection_count_balance x2
  5. L88
    specialize finite_bit_union_intersection_count_balance x3
  6. L89
    specialize finite_bit_union_intersection_count_balance x4
  7. L90
    specialize finite_bit_union_intersection_count_balance x6
  8. L91
    specialize finite_bit_union_intersection_count_balance x7
  9. L92
    specialize finite_bit_union_intersection_count_balance p
  10. L93
    specialize finite_bit_union_intersection_count_balance k
22Use earlier factsL94–103

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

  1. L94
    specialize finite_bit_union_intersection_count_balance l
  2. L95
    specialize finite_bit_union_intersection_count_balance x5
  3. L96
    specialize finite_bit_union_intersection_count_balance x8
  4. L97
    apply finite_bit_union_intersection_count_balance
  5. L98
    exact hA
  6. L99
    exact hT_witness_witness_left
  7. L100
    exact hU_witness_witness_witness_left
  8. L101
    exact hI_witness_witness_witness_left
  9. L102
    exact hU_witness_witness_witness_right
  10. L103
    exact hI_witness_witness_witness_right
23Separate the logical casesL104–104

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

  1. L104
    split
24Use earlier factsL105–114

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

  1. L105
    specialize finite_modular_dyson_upper_from_union b
  2. L106
    specialize finite_modular_dyson_upper_from_union c
  3. L107
    specialize finite_modular_dyson_upper_from_union d
  4. L108
    specialize finite_modular_dyson_upper_from_union e
  5. L109
    specialize finite_modular_dyson_upper_from_union x1
  6. L110
    specialize finite_modular_dyson_upper_from_union x2
  7. L111
    specialize finite_modular_dyson_upper_from_union x3
  8. L112
    specialize finite_modular_dyson_upper_from_union x4
  9. L113
    specialize finite_modular_dyson_upper_from_union p
  10. L114
    specialize finite_modular_dyson_upper_from_union t
25Use earlier factsL115–124

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

  1. L115
    specialize finite_modular_dyson_upper_from_union x
  2. L116
    apply finite_modular_dyson_upper_from_union
  3. L117
    exact hp
  4. L118
    exact hcomp_witness
  5. L119
    exact hT_witness_witness_right
  6. L120
    exact hU_witness_witness_witness_right
  7. L121
    specialize finite_modular_dyson_lower_from_pullback b
  8. L122
    specialize finite_modular_dyson_lower_from_pullback c
  9. L123
    specialize finite_modular_dyson_lower_from_pullback d
  10. L124
    specialize finite_modular_dyson_lower_from_pullback e
26Use earlier factsL125–134

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

  1. L125
    specialize finite_modular_dyson_lower_from_pullback x1
  2. L126
    specialize finite_modular_dyson_lower_from_pullback x2
  3. L127
    specialize finite_modular_dyson_lower_from_pullback x6
  4. L128
    specialize finite_modular_dyson_lower_from_pullback x7
  5. L129
    specialize finite_modular_dyson_lower_from_pullback x9
  6. L130
    specialize finite_modular_dyson_lower_from_pullback x10
  7. L131
    specialize finite_modular_dyson_lower_from_pullback p
  8. L132
    specialize finite_modular_dyson_lower_from_pullback t
  9. L133
    specialize finite_modular_dyson_lower_from_pullback x
  10. L134
    apply finite_modular_dyson_lower_from_pullback
27Use earlier factsL135–139

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

  1. L135
    exact hp
  2. L136
    exact hcomp_witness
  3. L137
    exact hT_witness_witness_right
  4. L138
    exact hI_witness_witness_witness_right
  5. L139
    exact hV_witness_witness_right

Library-wide reading audit

Original defined command ledger · 139 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro p
  6. 0006intro k
  7. 0007intro l
  8. 0008intro t
  9. 0009intro hp
  10. 0010intro hA
  11. 0011intro hB
  12. 0012intro ht
  13. 0013have hcomp : exists v. t+v=p
  14. 0014specialize finite_modular_additive_complement p
  15. 0015specialize finite_modular_additive_complement t
  16. 0016apply finite_modular_additive_complement
  17. 0017exact ht
  18. 0018cases hcomp
  19. 0019have hT : ∃ tb. ∃ tc. BitCount(tb,tc,p,l) ∧ ModularSetPullback(d,e,tb,tc,p,x)
  20. 0020specialize finite_modular_set_pullback_exists d
  21. 0021specialize finite_modular_set_pullback_exists e
  22. 0022specialize finite_modular_set_pullback_exists p
  23. 0023specialize finite_modular_set_pullback_exists l
  24. 0024specialize finite_modular_set_pullback_exists x
  25. 0025apply finite_modular_set_pullback_exists
  26. 0026exact hp
  27. 0027exact hB
  28. 0028cases hT
  29. 0029cases hT_witness
  30. 0030cases hT_witness_witness
  31. 0031have hU : ∃ ub. ∃ uc. ∃ K. BitCount(ub,uc,p,K) ∧ ModularSetUnion(b,c,x1,x2,ub,uc,p)
  32. 0032specialize finite_bit_union_exists b
  33. 0033specialize finite_bit_union_exists c
  34. 0034specialize finite_bit_union_exists x1
  35. 0035specialize finite_bit_union_exists x2
  36. 0036specialize finite_bit_union_exists p
  37. 0037specialize finite_bit_union_exists k
  38. 0038specialize finite_bit_union_exists l
  39. 0039apply finite_bit_union_exists
  40. 0040exact hA
  41. 0041exact hT_witness_witness_left
  42. 0042cases hU
  43. 0043cases hU_witness
  44. 0044cases hU_witness_witness
  45. 0045cases hU_witness_witness_witness
  46. 0046have hI : ∃ ib. ∃ ic. ∃ L. BitCount(ib,ic,p,L) ∧ ModularSetIntersection(b,c,x1,x2,ib,ic,p)
  47. 0047specialize finite_bit_intersection_exists b
  48. 0048specialize finite_bit_intersection_exists c
  49. 0049specialize finite_bit_intersection_exists x1
  50. 0050specialize finite_bit_intersection_exists x2
  51. 0051specialize finite_bit_intersection_exists p
  52. 0052specialize finite_bit_intersection_exists k
  53. 0053specialize finite_bit_intersection_exists l
  54. 0054apply finite_bit_intersection_exists
  55. 0055exact hA
  56. 0056exact hT_witness_witness_left
  57. 0057cases hI
  58. 0058cases hI_witness
  59. 0059cases hI_witness_witness
  60. 0060cases hI_witness_witness_witness
  61. 0061have hV : ∃ vb. ∃ vc. BitCount(vb,vc,p,x8) ∧ ModularSetPullback(x6,x7,vb,vc,p,t)
  62. 0062specialize finite_modular_set_pullback_exists x6
  63. 0063specialize finite_modular_set_pullback_exists x7
  64. 0064specialize finite_modular_set_pullback_exists p
  65. 0065specialize finite_modular_set_pullback_exists x8
  66. 0066specialize finite_modular_set_pullback_exists t
  67. 0067apply finite_modular_set_pullback_exists
  68. 0068exact hp
  69. 0069exact hI_witness_witness_witness_left
  70. 0070cases hV
  71. 0071cases hV_witness
  72. 0072cases hV_witness_witness
  73. 0073exists x3
  74. 0074exists x4
  75. 0075exists x9
  76. 0076exists x10
  77. 0077exists x5
  78. 0078exists x8
  79. 0079split
  80. 0080exact hU_witness_witness_witness_left
  81. 0081split
  82. 0082exact hV_witness_witness_left
  83. 0083split
  84. 0084specialize finite_bit_union_intersection_count_balance b
  85. 0085specialize finite_bit_union_intersection_count_balance c
  86. 0086specialize finite_bit_union_intersection_count_balance x1
  87. 0087specialize finite_bit_union_intersection_count_balance x2
  88. 0088specialize finite_bit_union_intersection_count_balance x3
  89. 0089specialize finite_bit_union_intersection_count_balance x4
  90. 0090specialize finite_bit_union_intersection_count_balance x6
  91. 0091specialize finite_bit_union_intersection_count_balance x7
  92. 0092specialize finite_bit_union_intersection_count_balance p
  93. 0093specialize finite_bit_union_intersection_count_balance k
  94. 0094specialize finite_bit_union_intersection_count_balance l
  95. 0095specialize finite_bit_union_intersection_count_balance x5
  96. 0096specialize finite_bit_union_intersection_count_balance x8
  97. 0097apply finite_bit_union_intersection_count_balance
  98. 0098exact hA
  99. 0099exact hT_witness_witness_left
  100. 0100exact hU_witness_witness_witness_left
  101. 0101exact hI_witness_witness_witness_left
  102. 0102exact hU_witness_witness_witness_right
  103. 0103exact hI_witness_witness_witness_right
  104. 0104split
  105. 0105specialize finite_modular_dyson_upper_from_union b
  106. 0106specialize finite_modular_dyson_upper_from_union c
  107. 0107specialize finite_modular_dyson_upper_from_union d
  108. 0108specialize finite_modular_dyson_upper_from_union e
  109. 0109specialize finite_modular_dyson_upper_from_union x1
  110. 0110specialize finite_modular_dyson_upper_from_union x2
  111. 0111specialize finite_modular_dyson_upper_from_union x3
  112. 0112specialize finite_modular_dyson_upper_from_union x4
  113. 0113specialize finite_modular_dyson_upper_from_union p
  114. 0114specialize finite_modular_dyson_upper_from_union t
  115. 0115specialize finite_modular_dyson_upper_from_union x
  116. 0116apply finite_modular_dyson_upper_from_union
  117. 0117exact hp
  118. 0118exact hcomp_witness
  119. 0119exact hT_witness_witness_right
  120. 0120exact hU_witness_witness_witness_right
  121. 0121specialize finite_modular_dyson_lower_from_pullback b
  122. 0122specialize finite_modular_dyson_lower_from_pullback c
  123. 0123specialize finite_modular_dyson_lower_from_pullback d
  124. 0124specialize finite_modular_dyson_lower_from_pullback e
  125. 0125specialize finite_modular_dyson_lower_from_pullback x1
  126. 0126specialize finite_modular_dyson_lower_from_pullback x2
  127. 0127specialize finite_modular_dyson_lower_from_pullback x6
  128. 0128specialize finite_modular_dyson_lower_from_pullback x7
  129. 0129specialize finite_modular_dyson_lower_from_pullback x9
  130. 0130specialize finite_modular_dyson_lower_from_pullback x10
  131. 0131specialize finite_modular_dyson_lower_from_pullback p
  132. 0132specialize finite_modular_dyson_lower_from_pullback t
  133. 0133specialize finite_modular_dyson_lower_from_pullback x
  134. 0134apply finite_modular_dyson_lower_from_pullback
  135. 0135exact hp
  136. 0136exact hcomp_witness
  137. 0137exact hT_witness_witness_right
  138. 0138exact hI_witness_witness_witness_right
  139. 0139exact hV_witness_witness_right