DC0007

dirichlet_convolution_entry_exists

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

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

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 expanded first-order arithmetic 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))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 7 declared prerequisites and contains 72 exact native proof lines.

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

Proof neighborhood

Direct dependencies

eq_decidable Stable theorem; checked-use authorized DC0001 dirichlet_convolution_entry_zero multiple_decidable_nonzero Stable theorem; checked-use authorized signed_table_lookup_any Alpha theorem; checked-use authorized signed_mul_total Alpha theorem; checked-use authorized DC0002 dirichlet_convolution_entry_from_quotient DC0003 dirichlet_convolution_entry_from_nondivisor

Direct dependents

DC000A dirichlet_convolution_prefix_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

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.

Named ingredients (3)
dirichlet convolution entry zerodirichlet convolution entry from quotientdirichlet convolution entry from nondivisor

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

01Fix variables and assumptionsL1–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 : (exists pvs_factor_choice_yes. (n) = (d) * pvs_factor_choice_yes) \/ ~(exists pvs_factor_choice_no. (n) = (d) * pvs_factor_choice_no)
  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
  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
  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
  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 exact 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 : (exists pvs_factor_choice_yes. (n) = (d) * pvs_factor_choice_yes) \/ ~(exists pvs_factor_choice_no. (n) = (d) * pvs_factor_choice_no)
  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 : exists a. (exists dst_positive_code_choice_left dst_positive_scale_choice_left dst_negative_code_choice_left dst_negative_scale_choice_left dst_positive_choice_left dst_negative_choice_left. (((F) = (((((dst_positive_code_choice_left) + (dst_positive_scale_choice_left)) * S ((dst_positive_code_choice_left) + (dst_positive_scale_choice_left)) + ((dst_positive_scale_choice_left) + (dst_positive_scale_choice_left))) + (((dst_negative_code_choice_left) + (dst_negative_scale_choice_left)) * S ((dst_negative_code_choice_left) + (dst_negative_scale_choice_left)) + ((dst_negative_scale_choice_left) + (dst_negative_scale_choice_left)))) * S ((((dst_positive_code_choice_left) + (dst_positive_scale_choice_left)) * S ((dst_positive_code_choice_left) + (dst_positive_scale_choice_left)) + ((dst_positive_scale_choice_left) + (dst_positive_scale_choice_left))) + (((dst_negative_code_choice_left) + (dst_negative_scale_choice_left)) * S ((dst_negative_code_choice_left) + (dst_negative_scale_choice_left)) + ((dst_negative_scale_choice_left) + (dst_negative_scale_choice_left)))) + ((((dst_negative_code_choice_left) + (dst_negative_scale_choice_left)) * S ((dst_negative_code_choice_left) + (dst_negative_scale_choice_left)) + ((dst_negative_scale_choice_left) + (dst_negative_scale_choice_left))) + (((dst_negative_code_choice_left) + (dst_negative_scale_choice_left)) * S ((dst_negative_code_choice_left) + (dst_negative_scale_choice_left)) + ((dst_negative_scale_choice_left) + (dst_negative_scale_choice_left)))))) /\ (((((exists ff_h_pvs_choice_leftpositive. ff_h_pvs_choice_leftpositive + S (dst_positive_choice_left) = S ((S (d)) * dst_positive_scale_choice_left)) /\ exists ff_q_pvs_choice_leftpositive. dst_positive_code_choice_left = ff_q_pvs_choice_leftpositive * S ((S (d)) * dst_positive_scale_choice_left) + (dst_positive_choice_left))) /\ (((((exists ff_h_pvs_choice_leftnegative. ff_h_pvs_choice_leftnegative + S (dst_negative_choice_left) = S ((S (d)) * dst_negative_scale_choice_left)) /\ exists ff_q_pvs_choice_leftnegative. dst_negative_code_choice_left = ff_q_pvs_choice_leftnegative * S ((S (d)) * dst_negative_scale_choice_left) + (dst_negative_choice_left))) /\ (exists ge_balance_positive_choice_leftvalue ge_balance_negative_choice_leftvalue. (((((a) = 2 * (ge_balance_positive_choice_leftvalue) /\ (ge_balance_negative_choice_leftvalue) = 0) \/ exists ge_signed_half_choice_leftvaluedecode. (((a) = 2 * ge_signed_half_choice_leftvaluedecode + 1 /\ (ge_balance_positive_choice_leftvalue) = 0) /\ (ge_balance_negative_choice_leftvalue) = S ge_signed_half_choice_leftvaluedecode))) /\ ((dst_positive_choice_left) + ge_balance_negative_choice_leftvalue = (dst_negative_choice_left) + ge_balance_positive_choice_leftvalue)))))))))
  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 : exists b. (exists dst_positive_code_choice_right dst_positive_scale_choice_right dst_negative_code_choice_right dst_negative_scale_choice_right dst_positive_choice_right dst_negative_choice_right. (((G) = (((((dst_positive_code_choice_right) + (dst_positive_scale_choice_right)) * S ((dst_positive_code_choice_right) + (dst_positive_scale_choice_right)) + ((dst_positive_scale_choice_right) + (dst_positive_scale_choice_right))) + (((dst_negative_code_choice_right) + (dst_negative_scale_choice_right)) * S ((dst_negative_code_choice_right) + (dst_negative_scale_choice_right)) + ((dst_negative_scale_choice_right) + (dst_negative_scale_choice_right)))) * S ((((dst_positive_code_choice_right) + (dst_positive_scale_choice_right)) * S ((dst_positive_code_choice_right) + (dst_positive_scale_choice_right)) + ((dst_positive_scale_choice_right) + (dst_positive_scale_choice_right))) + (((dst_negative_code_choice_right) + (dst_negative_scale_choice_right)) * S ((dst_negative_code_choice_right) + (dst_negative_scale_choice_right)) + ((dst_negative_scale_choice_right) + (dst_negative_scale_choice_right)))) + ((((dst_negative_code_choice_right) + (dst_negative_scale_choice_right)) * S ((dst_negative_code_choice_right) + (dst_negative_scale_choice_right)) + ((dst_negative_scale_choice_right) + (dst_negative_scale_choice_right))) + (((dst_negative_code_choice_right) + (dst_negative_scale_choice_right)) * S ((dst_negative_code_choice_right) + (dst_negative_scale_choice_right)) + ((dst_negative_scale_choice_right) + (dst_negative_scale_choice_right)))))) /\ (((((exists ff_h_pvs_choice_rightpositive. ff_h_pvs_choice_rightpositive + S (dst_positive_choice_right) = S ((S (x)) * dst_positive_scale_choice_right)) /\ exists ff_q_pvs_choice_rightpositive. dst_positive_code_choice_right = ff_q_pvs_choice_rightpositive * S ((S (x)) * dst_positive_scale_choice_right) + (dst_positive_choice_right))) /\ (((((exists ff_h_pvs_choice_rightnegative. ff_h_pvs_choice_rightnegative + S (dst_negative_choice_right) = S ((S (x)) * dst_negative_scale_choice_right)) /\ exists ff_q_pvs_choice_rightnegative. dst_negative_code_choice_right = ff_q_pvs_choice_rightnegative * S ((S (x)) * dst_negative_scale_choice_right) + (dst_negative_choice_right))) /\ (exists ge_balance_positive_choice_rightvalue ge_balance_negative_choice_rightvalue. (((((b) = 2 * (ge_balance_positive_choice_rightvalue) /\ (ge_balance_negative_choice_rightvalue) = 0) \/ exists ge_signed_half_choice_rightvaluedecode. (((b) = 2 * ge_signed_half_choice_rightvaluedecode + 1 /\ (ge_balance_positive_choice_rightvalue) = 0) /\ (ge_balance_negative_choice_rightvalue) = S ge_signed_half_choice_rightvaluedecode))) /\ ((dst_positive_choice_right) + ge_balance_negative_choice_rightvalue = (dst_negative_choice_right) + ge_balance_positive_choice_rightvalue)))))))))
  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 : exists z. (exists sto_ap_choice_product sto_an_choice_product sto_bp_choice_product sto_bn_choice_product sto_cp_choice_product sto_cn_choice_product. (((((x1) = 2 * (sto_ap_choice_product) /\ (sto_an_choice_product) = 0) \/ exists ge_signed_half_choice_productleft. (((x1) = 2 * ge_signed_half_choice_productleft + 1 /\ (sto_ap_choice_product) = 0) /\ (sto_an_choice_product) = S ge_signed_half_choice_productleft))) /\ ((((((x2) = 2 * (sto_bp_choice_product) /\ (sto_bn_choice_product) = 0) \/ exists ge_signed_half_choice_productright. (((x2) = 2 * ge_signed_half_choice_productright + 1 /\ (sto_bp_choice_product) = 0) /\ (sto_bn_choice_product) = S ge_signed_half_choice_productright))) /\ ((((((z) = 2 * (sto_cp_choice_product) /\ (sto_cn_choice_product) = 0) \/ exists ge_signed_half_choice_productoutput. (((z) = 2 * ge_signed_half_choice_productoutput + 1 /\ (sto_cp_choice_product) = 0) /\ (sto_cn_choice_product) = S ge_signed_half_choice_productoutput))) /\ ((sto_ap_choice_product * sto_bp_choice_product + sto_an_choice_product * sto_bn_choice_product) + sto_cn_choice_product = (sto_ap_choice_product * sto_bn_choice_product + sto_an_choice_product * sto_bp_choice_product) + sto_cp_choice_product)))))))
  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