DC0007

dirichlet_convolution_entry_exists

Decide membership, extract the actual quotient, construct both signed lookups and multiply them; neither choice nor a quotient oracle is assumed.

Alpha v34 checked-use · first admitted v31 · 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.

Each retained summand has a witnessed n=d*q and actual signed multiplication. Zero and nondivisors contribute zero. Input and output values at zero are unrestricted; uniqueness is for positive represented values. The separate inverse family proves the unit-at-one criterion. Full G009 multiplicative-function closure is now admitted in the separate Alpha-v32 multiplicative-convolution family.

Exact theorem in conservative defined notation

∀ F. ∀ G. ∀ n. ∀ d. ArithTable(0,F) → ArithTable(0,G) → ∃ x. DirichletEntry(F,G,n,d,x)

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

Definition DAG

SignedMul(a,b,c) · 1ArithTable(N,F) · 2ArithAt(F,i,z) · 2DirichletEntry(F,G,n,d,z) · 1Dvd(d,n) · 2

Actual proof prerequisites

eq_decidable · checked external prerequisitedirichlet_convolution_entry_zeromultiple_decidable_nonzero · checked external prerequisitesigned_table_lookup_any · checked external prerequisitesigned_mul_total · checked external prerequisitedirichlet_convolution_entry_from_quotientdirichlet_convolution_entry_from_nondivisor
Original expanded first-order statement 
forall F G n d. (exists dst_positive_code_choice_left_table dst_positive_scale_choice_left_table dst_negative_code_choice_left_table dst_negative_scale_choice_left_table. (((F) = (((((dst_positive_code_choice_left_table) + (dst_positive_scale_choice_left_table)) * S ((dst_positive_code_choice_left_table) + (dst_positive_scale_choice_left_table)) + ((dst_positive_scale_choice_left_table) + (dst_positive_scale_choice_left_table))) + (((dst_negative_code_choice_left_table) + (dst_negative_scale_choice_left_table)) * S ((dst_negative_code_choice_left_table) + (dst_negative_scale_choice_left_table)) + ((dst_negative_scale_choice_left_table) + (dst_negative_scale_choice_left_table)))) * S ((((dst_positive_code_choice_left_table) + (dst_positive_scale_choice_left_table)) * S ((dst_positive_code_choice_left_table) + (dst_positive_scale_choice_left_table)) + ((dst_positive_scale_choice_left_table) + (dst_positive_scale_choice_left_table))) + (((dst_negative_code_choice_left_table) + (dst_negative_scale_choice_left_table)) * S ((dst_negative_code_choice_left_table) + (dst_negative_scale_choice_left_table)) + ((dst_negative_scale_choice_left_table) + (dst_negative_scale_choice_left_table)))) + ((((dst_negative_code_choice_left_table) + (dst_negative_scale_choice_left_table)) * S ((dst_negative_code_choice_left_table) + (dst_negative_scale_choice_left_table)) + ((dst_negative_scale_choice_left_table) + (dst_negative_scale_choice_left_table))) + (((dst_negative_code_choice_left_table) + (dst_negative_scale_choice_left_table)) * S ((dst_negative_code_choice_left_table) + (dst_negative_scale_choice_left_table)) + ((dst_negative_scale_choice_left_table) + (dst_negative_scale_choice_left_table)))))) /\ (forall dst_index_choice_left_table. (exists pvs_le_gap_choice_left_tabledomain. pvs_le_gap_choice_left_tabledomain + (dst_index_choice_left_table) = (0)) -> exists dst_positive_choice_left_table dst_negative_choice_left_table dst_value_choice_left_table. ((((exists ff_h_pvs_choice_left_tableentrypositive. ff_h_pvs_choice_left_tableentrypositive + S (dst_positive_choice_left_table) = S ((S (dst_index_choice_left_table)) * dst_positive_scale_choice_left_table)) /\ exists ff_q_pvs_choice_left_tableentrypositive. dst_positive_code_choice_left_table = ff_q_pvs_choice_left_tableentrypositive * S ((S (dst_index_choice_left_table)) * dst_positive_scale_choice_left_table) + (dst_positive_choice_left_table))) /\ (((((exists ff_h_pvs_choice_left_tableentrynegative. ff_h_pvs_choice_left_tableentrynegative + S (dst_negative_choice_left_table) = S ((S (dst_index_choice_left_table)) * dst_negative_scale_choice_left_table)) /\ exists ff_q_pvs_choice_left_tableentrynegative. dst_negative_code_choice_left_table = ff_q_pvs_choice_left_tableentrynegative * S ((S (dst_index_choice_left_table)) * dst_negative_scale_choice_left_table) + (dst_negative_choice_left_table))) /\ (exists ge_balance_positive_choice_left_tableentryvalue ge_balance_negative_choice_left_tableentryvalue. (((((dst_value_choice_left_table) = 2 * (ge_balance_positive_choice_left_tableentryvalue) /\ (ge_balance_negative_choice_left_tableentryvalue) = 0) \/ exists ge_signed_half_choice_left_tableentryvaluedecode. (((dst_value_choice_left_table) = 2 * ge_signed_half_choice_left_tableentryvaluedecode + 1 /\ (ge_balance_positive_choice_left_tableentryvalue) = 0) /\ (ge_balance_negative_choice_left_tableentryvalue) = S ge_signed_half_choice_left_tableentryvaluedecode))) /\ ((dst_positive_choice_left_table) + ge_balance_negative_choice_left_tableentryvalue = (dst_negative_choice_left_table) + ge_balance_positive_choice_left_tableentryvalue))))))))) -> (exists dst_positive_code_choice_right_table dst_positive_scale_choice_right_table dst_negative_code_choice_right_table dst_negative_scale_choice_right_table. (((G) = (((((dst_positive_code_choice_right_table) + (dst_positive_scale_choice_right_table)) * S ((dst_positive_code_choice_right_table) + (dst_positive_scale_choice_right_table)) + ((dst_positive_scale_choice_right_table) + (dst_positive_scale_choice_right_table))) + (((dst_negative_code_choice_right_table) + (dst_negative_scale_choice_right_table)) * S ((dst_negative_code_choice_right_table) + (dst_negative_scale_choice_right_table)) + ((dst_negative_scale_choice_right_table) + (dst_negative_scale_choice_right_table)))) * S ((((dst_positive_code_choice_right_table) + (dst_positive_scale_choice_right_table)) * S ((dst_positive_code_choice_right_table) + (dst_positive_scale_choice_right_table)) + ((dst_positive_scale_choice_right_table) + (dst_positive_scale_choice_right_table))) + (((dst_negative_code_choice_right_table) + (dst_negative_scale_choice_right_table)) * S ((dst_negative_code_choice_right_table) + (dst_negative_scale_choice_right_table)) + ((dst_negative_scale_choice_right_table) + (dst_negative_scale_choice_right_table)))) + ((((dst_negative_code_choice_right_table) + (dst_negative_scale_choice_right_table)) * S ((dst_negative_code_choice_right_table) + (dst_negative_scale_choice_right_table)) + ((dst_negative_scale_choice_right_table) + (dst_negative_scale_choice_right_table))) + (((dst_negative_code_choice_right_table) + (dst_negative_scale_choice_right_table)) * S ((dst_negative_code_choice_right_table) + (dst_negative_scale_choice_right_table)) + ((dst_negative_scale_choice_right_table) + (dst_negative_scale_choice_right_table)))))) /\ (forall dst_index_choice_right_table. (exists pvs_le_gap_choice_right_tabledomain. pvs_le_gap_choice_right_tabledomain + (dst_index_choice_right_table) = (0)) -> exists dst_positive_choice_right_table dst_negative_choice_right_table dst_value_choice_right_table. ((((exists ff_h_pvs_choice_right_tableentrypositive. ff_h_pvs_choice_right_tableentrypositive + S (dst_positive_choice_right_table) = S ((S (dst_index_choice_right_table)) * dst_positive_scale_choice_right_table)) /\ exists ff_q_pvs_choice_right_tableentrypositive. dst_positive_code_choice_right_table = ff_q_pvs_choice_right_tableentrypositive * S ((S (dst_index_choice_right_table)) * dst_positive_scale_choice_right_table) + (dst_positive_choice_right_table))) /\ (((((exists ff_h_pvs_choice_right_tableentrynegative. ff_h_pvs_choice_right_tableentrynegative + S (dst_negative_choice_right_table) = S ((S (dst_index_choice_right_table)) * dst_negative_scale_choice_right_table)) /\ exists ff_q_pvs_choice_right_tableentrynegative. dst_negative_code_choice_right_table = ff_q_pvs_choice_right_tableentrynegative * S ((S (dst_index_choice_right_table)) * dst_negative_scale_choice_right_table) + (dst_negative_choice_right_table))) /\ (exists ge_balance_positive_choice_right_tableentryvalue ge_balance_negative_choice_right_tableentryvalue. (((((dst_value_choice_right_table) = 2 * (ge_balance_positive_choice_right_tableentryvalue) /\ (ge_balance_negative_choice_right_tableentryvalue) = 0) \/ exists ge_signed_half_choice_right_tableentryvaluedecode. (((dst_value_choice_right_table) = 2 * ge_signed_half_choice_right_tableentryvaluedecode + 1 /\ (ge_balance_positive_choice_right_tableentryvalue) = 0) /\ (ge_balance_negative_choice_right_tableentryvalue) = S ge_signed_half_choice_right_tableentryvaluedecode))) /\ ((dst_positive_choice_right_table) + ge_balance_negative_choice_right_tableentryvalue = (dst_negative_choice_right_table) + ge_balance_positive_choice_right_tableentryvalue))))))))) -> exists z. ((((~((d)=0)) /\ (exists dc_quotient_choice_result dc_left_choice_result dc_right_choice_result. (((n)=(d)*dc_quotient_choice_result) /\ (((exists dst_positive_code_choice_resultleft dst_positive_scale_choice_resultleft dst_negative_code_choice_resultleft dst_negative_scale_choice_resultleft dst_positive_choice_resultleft dst_negative_choice_resultleft. (((F) = (((((dst_positive_code_choice_resultleft) + (dst_positive_scale_choice_resultleft)) * S ((dst_positive_code_choice_resultleft) + (dst_positive_scale_choice_resultleft)) + ((dst_positive_scale_choice_resultleft) + (dst_positive_scale_choice_resultleft))) + (((dst_negative_code_choice_resultleft) + (dst_negative_scale_choice_resultleft)) * S ((dst_negative_code_choice_resultleft) + (dst_negative_scale_choice_resultleft)) + ((dst_negative_scale_choice_resultleft) + (dst_negative_scale_choice_resultleft)))) * S ((((dst_positive_code_choice_resultleft) + (dst_positive_scale_choice_resultleft)) * S ((dst_positive_code_choice_resultleft) + (dst_positive_scale_choice_resultleft)) + ((dst_positive_scale_choice_resultleft) + (dst_positive_scale_choice_resultleft))) + (((dst_negative_code_choice_resultleft) + (dst_negative_scale_choice_resultleft)) * S ((dst_negative_code_choice_resultleft) + (dst_negative_scale_choice_resultleft)) + ((dst_negative_scale_choice_resultleft) + (dst_negative_scale_choice_resultleft)))) + ((((dst_negative_code_choice_resultleft) + (dst_negative_scale_choice_resultleft)) * S ((dst_negative_code_choice_resultleft) + (dst_negative_scale_choice_resultleft)) + ((dst_negative_scale_choice_resultleft) + (dst_negative_scale_choice_resultleft))) + (((dst_negative_code_choice_resultleft) + (dst_negative_scale_choice_resultleft)) * S ((dst_negative_code_choice_resultleft) + (dst_negative_scale_choice_resultleft)) + ((dst_negative_scale_choice_resultleft) + (dst_negative_scale_choice_resultleft)))))) /\ (((((exists ff_h_pvs_choice_resultleftpositive. ff_h_pvs_choice_resultleftpositive + S (dst_positive_choice_resultleft) = S ((S (d)) * dst_positive_scale_choice_resultleft)) /\ exists ff_q_pvs_choice_resultleftpositive. dst_positive_code_choice_resultleft = ff_q_pvs_choice_resultleftpositive * S ((S (d)) * dst_positive_scale_choice_resultleft) + (dst_positive_choice_resultleft))) /\ (((((exists ff_h_pvs_choice_resultleftnegative. ff_h_pvs_choice_resultleftnegative + S (dst_negative_choice_resultleft) = S ((S (d)) * dst_negative_scale_choice_resultleft)) /\ exists ff_q_pvs_choice_resultleftnegative. dst_negative_code_choice_resultleft = ff_q_pvs_choice_resultleftnegative * S ((S (d)) * dst_negative_scale_choice_resultleft) + (dst_negative_choice_resultleft))) /\ (exists ge_balance_positive_choice_resultleftvalue ge_balance_negative_choice_resultleftvalue. (((((dc_left_choice_result) = 2 * (ge_balance_positive_choice_resultleftvalue) /\ (ge_balance_negative_choice_resultleftvalue) = 0) \/ exists ge_signed_half_choice_resultleftvaluedecode. (((dc_left_choice_result) = 2 * ge_signed_half_choice_resultleftvaluedecode + 1 /\ (ge_balance_positive_choice_resultleftvalue) = 0) /\ (ge_balance_negative_choice_resultleftvalue) = S ge_signed_half_choice_resultleftvaluedecode))) /\ ((dst_positive_choice_resultleft) + ge_balance_negative_choice_resultleftvalue = (dst_negative_choice_resultleft) + ge_balance_positive_choice_resultleftvalue))))))))) /\ (((exists dst_positive_code_choice_resultright dst_positive_scale_choice_resultright dst_negative_code_choice_resultright dst_negative_scale_choice_resultright dst_positive_choice_resultright dst_negative_choice_resultright. (((G) = (((((dst_positive_code_choice_resultright) + (dst_positive_scale_choice_resultright)) * S ((dst_positive_code_choice_resultright) + (dst_positive_scale_choice_resultright)) + ((dst_positive_scale_choice_resultright) + (dst_positive_scale_choice_resultright))) + (((dst_negative_code_choice_resultright) + (dst_negative_scale_choice_resultright)) * S ((dst_negative_code_choice_resultright) + (dst_negative_scale_choice_resultright)) + ((dst_negative_scale_choice_resultright) + (dst_negative_scale_choice_resultright)))) * S ((((dst_positive_code_choice_resultright) + (dst_positive_scale_choice_resultright)) * S ((dst_positive_code_choice_resultright) + (dst_positive_scale_choice_resultright)) + ((dst_positive_scale_choice_resultright) + (dst_positive_scale_choice_resultright))) + (((dst_negative_code_choice_resultright) + (dst_negative_scale_choice_resultright)) * S ((dst_negative_code_choice_resultright) + (dst_negative_scale_choice_resultright)) + ((dst_negative_scale_choice_resultright) + (dst_negative_scale_choice_resultright)))) + ((((dst_negative_code_choice_resultright) + (dst_negative_scale_choice_resultright)) * S ((dst_negative_code_choice_resultright) + (dst_negative_scale_choice_resultright)) + ((dst_negative_scale_choice_resultright) + (dst_negative_scale_choice_resultright))) + (((dst_negative_code_choice_resultright) + (dst_negative_scale_choice_resultright)) * S ((dst_negative_code_choice_resultright) + (dst_negative_scale_choice_resultright)) + ((dst_negative_scale_choice_resultright) + (dst_negative_scale_choice_resultright)))))) /\ (((((exists ff_h_pvs_choice_resultrightpositive. ff_h_pvs_choice_resultrightpositive + S (dst_positive_choice_resultright) = S ((S (dc_quotient_choice_result)) * dst_positive_scale_choice_resultright)) /\ exists ff_q_pvs_choice_resultrightpositive. dst_positive_code_choice_resultright = ff_q_pvs_choice_resultrightpositive * S ((S (dc_quotient_choice_result)) * dst_positive_scale_choice_resultright) + (dst_positive_choice_resultright))) /\ (((((exists ff_h_pvs_choice_resultrightnegative. ff_h_pvs_choice_resultrightnegative + S (dst_negative_choice_resultright) = S ((S (dc_quotient_choice_result)) * dst_negative_scale_choice_resultright)) /\ exists ff_q_pvs_choice_resultrightnegative. dst_negative_code_choice_resultright = ff_q_pvs_choice_resultrightnegative * S ((S (dc_quotient_choice_result)) * dst_negative_scale_choice_resultright) + (dst_negative_choice_resultright))) /\ (exists ge_balance_positive_choice_resultrightvalue ge_balance_negative_choice_resultrightvalue. (((((dc_right_choice_result) = 2 * (ge_balance_positive_choice_resultrightvalue) /\ (ge_balance_negative_choice_resultrightvalue) = 0) \/ exists ge_signed_half_choice_resultrightvaluedecode. (((dc_right_choice_result) = 2 * ge_signed_half_choice_resultrightvaluedecode + 1 /\ (ge_balance_positive_choice_resultrightvalue) = 0) /\ (ge_balance_negative_choice_resultrightvalue) = S ge_signed_half_choice_resultrightvaluedecode))) /\ ((dst_positive_choice_resultright) + ge_balance_negative_choice_resultrightvalue = (dst_negative_choice_resultright) + ge_balance_positive_choice_resultrightvalue))))))))) /\ (exists sto_ap_choice_resultproduct sto_an_choice_resultproduct sto_bp_choice_resultproduct sto_bn_choice_resultproduct sto_cp_choice_resultproduct sto_cn_choice_resultproduct. (((((dc_left_choice_result) = 2 * (sto_ap_choice_resultproduct) /\ (sto_an_choice_resultproduct) = 0) \/ exists ge_signed_half_choice_resultproductleft. (((dc_left_choice_result) = 2 * ge_signed_half_choice_resultproductleft + 1 /\ (sto_ap_choice_resultproduct) = 0) /\ (sto_an_choice_resultproduct) = S ge_signed_half_choice_resultproductleft))) /\ ((((((dc_right_choice_result) = 2 * (sto_bp_choice_resultproduct) /\ (sto_bn_choice_resultproduct) = 0) \/ exists ge_signed_half_choice_resultproductright. (((dc_right_choice_result) = 2 * ge_signed_half_choice_resultproductright + 1 /\ (sto_bp_choice_resultproduct) = 0) /\ (sto_bn_choice_resultproduct) = S ge_signed_half_choice_resultproductright))) /\ ((((((z) = 2 * (sto_cp_choice_resultproduct) /\ (sto_cn_choice_resultproduct) = 0) \/ exists ge_signed_half_choice_resultproductoutput. (((z) = 2 * ge_signed_half_choice_resultproductoutput + 1 /\ (sto_cp_choice_resultproduct) = 0) /\ (sto_cn_choice_resultproduct) = S ge_signed_half_choice_resultproductoutput))) /\ ((sto_ap_choice_resultproduct * sto_bp_choice_resultproduct + sto_an_choice_resultproduct * sto_bn_choice_resultproduct) + sto_cn_choice_resultproduct = (sto_ap_choice_resultproduct * sto_bn_choice_resultproduct + sto_an_choice_resultproduct * sto_bp_choice_resultproduct) + sto_cp_choice_resultproduct))))))))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_choice_resultnondivisor. (n) = (d) * pvs_factor_choice_resultnondivisor)) /\ ((z)=0))))

Complete tactic proof in conservative notation

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

72 script commands · 19 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 (3)
dirichlet convolution entry zerodirichlet convolution entry from quotientdirichlet convolution entry from nondivisor
01Fix variables and assumptionsL1–6

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

  1. L1
    intro F
  2. L2
    intro G
  3. L3
    intro n
  4. L4
    intro d
  5. L5
    intro hF
  6. L6
    intro hG
02Establish hcL7–10

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

  1. L7
    have hc : d=0 \/ ~(d=0)
  2. L8
    specialize eq_decidable (d)
  3. L9
    specialize eq_decidable (0)
  4. L10
    apply eq_decidable
03Separate the logical casesL11–11

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

  1. L11
    cases hc
04Construct an explicit witnessL12–12

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

  1. L12
    exists 0
05Calculate and transport equalitiesL13–20

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

  1. L13
    rewrite hc_left
  2. L14
    rewrite hc_left
  3. L15
    rewrite hc_left
  4. L16
    rewrite hc_left
  5. L17
    rewrite hc_left
  6. L18
    rewrite hc_left
  7. L19
    rewrite hc_left
  8. L20
    rewrite hc_left
06Use earlier factsL21–24

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

  1. L21
    specialize dirichlet_convolution_entry_zero (F)
  2. L22
    specialize dirichlet_convolution_entry_zero (G)
  3. L23
    specialize dirichlet_convolution_entry_zero (n)
  4. L24
    apply dirichlet_convolution_entry_zero
07Establish hdivL25–29

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

  1. L25
    have hdiv : Dvd(d,n) ∨ ¬Dvd(d,n)Definitions: Dvd(d,n)Original native command in the exact edition
  2. L26
    specialize multiple_decidable_nonzero (d)
  3. L27
    specialize multiple_decidable_nonzero (n)
  4. L28
    apply multiple_decidable_nonzero
  5. L29
    exact hc_right
08Separate the logical casesL30–31

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

  1. L30
    cases hdiv
  2. L31
    cases hdiv_left
09Establish haL32–37

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed table lookup any.

  1. L32
    have ha : ∃ a. ArithAt(F,d,a)Definitions: ArithAt(F,d,a)Original native command in the exact edition
  2. L33
    specialize signed_table_lookup_any (0)
  3. L34
    specialize signed_table_lookup_any (F)
  4. L35
    specialize signed_table_lookup_any (d)
  5. L36
    apply signed_table_lookup_any
  6. L37
    exact hF
10Separate the logical casesL38–38

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

  1. L38
    cases ha
11Establish hbL39–44

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed table lookup any.

  1. L39
    have hb : ∃ b. ArithAt(G,x,b)Definitions: ArithAt(G,x,b)Original native command in the exact edition
  2. L40
    specialize signed_table_lookup_any (0)
  3. L41
    specialize signed_table_lookup_any (G)
  4. L42
    specialize signed_table_lookup_any (x)
  5. L43
    apply signed_table_lookup_any
  6. L44
    exact hG
12Separate the logical casesL45–45

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

  1. L45
    cases hb
13Establish hzL46–49

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

  1. L46
    have hz : ∃ z. SignedMul(x1,x2,z)Definitions: SignedMul(x1,x2,z)Original native command in the exact edition
  2. L47
    specialize signed_mul_total (x1)
  3. L48
    specialize signed_mul_total (x2)
  4. L49
    apply signed_mul_total
14Separate the logical casesL50–50

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

  1. L50
    cases hz
15Construct an explicit witnessL51–51

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

  1. L51
    exists x3
16Use earlier factsL52–61

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

  1. L52
    specialize dirichlet_convolution_entry_from_quotient (F)
  2. L53
    specialize dirichlet_convolution_entry_from_quotient (G)
  3. L54
    specialize dirichlet_convolution_entry_from_quotient (n)
  4. L55
    specialize dirichlet_convolution_entry_from_quotient (d)
  5. L56
    specialize dirichlet_convolution_entry_from_quotient (x)
  6. L57
    specialize dirichlet_convolution_entry_from_quotient (x1)
  7. L58
    specialize dirichlet_convolution_entry_from_quotient (x2)
  8. L59
    specialize dirichlet_convolution_entry_from_quotient (x3)
  9. L60
    apply dirichlet_convolution_entry_from_quotient
  10. L61
    exact hc_right
17Use earlier factsL62–65

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

  1. L62
    exact hdiv_left_witness
  2. L63
    exact ha_witness
  3. L64
    exact hb_witness
  4. L65
    exact hz_witness
18Construct an explicit witnessL66–66

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

  1. L66
    exists 0
19Use earlier factsL67–72

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

  1. L67
    specialize dirichlet_convolution_entry_from_nondivisor (F)
  2. L68
    specialize dirichlet_convolution_entry_from_nondivisor (G)
  3. L69
    specialize dirichlet_convolution_entry_from_nondivisor (n)
  4. L70
    specialize dirichlet_convolution_entry_from_nondivisor (d)
  5. L71
    apply dirichlet_convolution_entry_from_nondivisor
  6. L72
    exact hdiv_right

Library-wide reading audit

Original defined command ledger · 72 lines
  1. 0001intro F
  2. 0002intro G
  3. 0003intro n
  4. 0004intro d
  5. 0005intro hF
  6. 0006intro hG
  7. 0007have hc : d=0 \/ ~(d=0)
  8. 0008specialize eq_decidable (d)
  9. 0009specialize eq_decidable (0)
  10. 0010apply eq_decidable
  11. 0011cases hc
  12. 0012exists 0
  13. 0013rewrite hc_left
  14. 0014rewrite hc_left
  15. 0015rewrite hc_left
  16. 0016rewrite hc_left
  17. 0017rewrite hc_left
  18. 0018rewrite hc_left
  19. 0019rewrite hc_left
  20. 0020rewrite hc_left
  21. 0021specialize dirichlet_convolution_entry_zero (F)
  22. 0022specialize dirichlet_convolution_entry_zero (G)
  23. 0023specialize dirichlet_convolution_entry_zero (n)
  24. 0024apply dirichlet_convolution_entry_zero
  25. 0025have hdiv : Dvd(d,n) ∨ ¬Dvd(d,n)
  26. 0026specialize multiple_decidable_nonzero (d)
  27. 0027specialize multiple_decidable_nonzero (n)
  28. 0028apply multiple_decidable_nonzero
  29. 0029exact hc_right
  30. 0030cases hdiv
  31. 0031cases hdiv_left
  32. 0032have ha : ∃ a. ArithAt(F,d,a)
  33. 0033specialize signed_table_lookup_any (0)
  34. 0034specialize signed_table_lookup_any (F)
  35. 0035specialize signed_table_lookup_any (d)
  36. 0036apply signed_table_lookup_any
  37. 0037exact hF
  38. 0038cases ha
  39. 0039have hb : ∃ b. ArithAt(G,x,b)
  40. 0040specialize signed_table_lookup_any (0)
  41. 0041specialize signed_table_lookup_any (G)
  42. 0042specialize signed_table_lookup_any (x)
  43. 0043apply signed_table_lookup_any
  44. 0044exact hG
  45. 0045cases hb
  46. 0046have hz : ∃ z. SignedMul(x1,x2,z)
  47. 0047specialize signed_mul_total (x1)
  48. 0048specialize signed_mul_total (x2)
  49. 0049apply signed_mul_total
  50. 0050cases hz
  51. 0051exists x3
  52. 0052specialize dirichlet_convolution_entry_from_quotient (F)
  53. 0053specialize dirichlet_convolution_entry_from_quotient (G)
  54. 0054specialize dirichlet_convolution_entry_from_quotient (n)
  55. 0055specialize dirichlet_convolution_entry_from_quotient (d)
  56. 0056specialize dirichlet_convolution_entry_from_quotient (x)
  57. 0057specialize dirichlet_convolution_entry_from_quotient (x1)
  58. 0058specialize dirichlet_convolution_entry_from_quotient (x2)
  59. 0059specialize dirichlet_convolution_entry_from_quotient (x3)
  60. 0060apply dirichlet_convolution_entry_from_quotient
  61. 0061exact hc_right
  62. 0062exact hdiv_left_witness
  63. 0063exact ha_witness
  64. 0064exact hb_witness
  65. 0065exact hz_witness
  66. 0066exists 0
  67. 0067specialize dirichlet_convolution_entry_from_nondivisor (F)
  68. 0068specialize dirichlet_convolution_entry_from_nondivisor (G)
  69. 0069specialize dirichlet_convolution_entry_from_nondivisor (n)
  70. 0070specialize dirichlet_convolution_entry_from_nondivisor (d)
  71. 0071apply dirichlet_convolution_entry_from_nondivisor
  72. 0072exact hdiv_right