DT0005

dirichlet_convolution_last_entry_iff

For n>0 the final divisor entry is exactly F(n)*G(1), using the actual quotient witness n=n*1 in both directions.

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.

The strict remainder is an actual inclusive prefix through k with an S k-entry fold; the future input at S k is excluded. A genuine table extension supplies the endpoint. The at-one identity inspects or constructs the real two-entry masked sum. No recurrence, inverse, or omitted summand value is assumed as a conclusion-bearing premise.

Exact theorem in conservative defined notation

∀ F. ∀ G. ∀ n. ∀ a. ∀ b. ∀ z. ¬n = 0 → ArithAt(F,n,a) → ArithAt(G,1,b) → (DirichletEntry(F,G,n,n,z) → SignedMul(a,b,z)) ∧ (SignedMul(a,b,z) → DirichletEntry(F,G,n,n,z))

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

Definition DAG

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

Actual proof prerequisites

dirichlet_convolution_entry_quotient_product · checked external prerequisitemul_one · checked external prerequisitedirichlet_convolution_entry_from_quotient · checked external prerequisite
Original expanded first-order statement 
forall F G n a b z. ~(n=0) -> (exists dst_positive_code_endpoint_first dst_positive_scale_endpoint_first dst_negative_code_endpoint_first dst_negative_scale_endpoint_first dst_positive_endpoint_first dst_negative_endpoint_first. (((F) = (((((dst_positive_code_endpoint_first) + (dst_positive_scale_endpoint_first)) * S ((dst_positive_code_endpoint_first) + (dst_positive_scale_endpoint_first)) + ((dst_positive_scale_endpoint_first) + (dst_positive_scale_endpoint_first))) + (((dst_negative_code_endpoint_first) + (dst_negative_scale_endpoint_first)) * S ((dst_negative_code_endpoint_first) + (dst_negative_scale_endpoint_first)) + ((dst_negative_scale_endpoint_first) + (dst_negative_scale_endpoint_first)))) * S ((((dst_positive_code_endpoint_first) + (dst_positive_scale_endpoint_first)) * S ((dst_positive_code_endpoint_first) + (dst_positive_scale_endpoint_first)) + ((dst_positive_scale_endpoint_first) + (dst_positive_scale_endpoint_first))) + (((dst_negative_code_endpoint_first) + (dst_negative_scale_endpoint_first)) * S ((dst_negative_code_endpoint_first) + (dst_negative_scale_endpoint_first)) + ((dst_negative_scale_endpoint_first) + (dst_negative_scale_endpoint_first)))) + ((((dst_negative_code_endpoint_first) + (dst_negative_scale_endpoint_first)) * S ((dst_negative_code_endpoint_first) + (dst_negative_scale_endpoint_first)) + ((dst_negative_scale_endpoint_first) + (dst_negative_scale_endpoint_first))) + (((dst_negative_code_endpoint_first) + (dst_negative_scale_endpoint_first)) * S ((dst_negative_code_endpoint_first) + (dst_negative_scale_endpoint_first)) + ((dst_negative_scale_endpoint_first) + (dst_negative_scale_endpoint_first)))))) /\ (((((exists ff_h_pvs_endpoint_firstpositive. ff_h_pvs_endpoint_firstpositive + S (dst_positive_endpoint_first) = S ((S (n)) * dst_positive_scale_endpoint_first)) /\ exists ff_q_pvs_endpoint_firstpositive. dst_positive_code_endpoint_first = ff_q_pvs_endpoint_firstpositive * S ((S (n)) * dst_positive_scale_endpoint_first) + (dst_positive_endpoint_first))) /\ (((((exists ff_h_pvs_endpoint_firstnegative. ff_h_pvs_endpoint_firstnegative + S (dst_negative_endpoint_first) = S ((S (n)) * dst_negative_scale_endpoint_first)) /\ exists ff_q_pvs_endpoint_firstnegative. dst_negative_code_endpoint_first = ff_q_pvs_endpoint_firstnegative * S ((S (n)) * dst_negative_scale_endpoint_first) + (dst_negative_endpoint_first))) /\ (exists ge_balance_positive_endpoint_firstvalue ge_balance_negative_endpoint_firstvalue. (((((a) = 2 * (ge_balance_positive_endpoint_firstvalue) /\ (ge_balance_negative_endpoint_firstvalue) = 0) \/ exists ge_signed_half_endpoint_firstvaluedecode. (((a) = 2 * ge_signed_half_endpoint_firstvaluedecode + 1 /\ (ge_balance_positive_endpoint_firstvalue) = 0) /\ (ge_balance_negative_endpoint_firstvalue) = S ge_signed_half_endpoint_firstvaluedecode))) /\ ((dst_positive_endpoint_first) + ge_balance_negative_endpoint_firstvalue = (dst_negative_endpoint_first) + ge_balance_positive_endpoint_firstvalue))))))))) -> (exists dst_positive_code_endpoint_second dst_positive_scale_endpoint_second dst_negative_code_endpoint_second dst_negative_scale_endpoint_second dst_positive_endpoint_second dst_negative_endpoint_second. (((G) = (((((dst_positive_code_endpoint_second) + (dst_positive_scale_endpoint_second)) * S ((dst_positive_code_endpoint_second) + (dst_positive_scale_endpoint_second)) + ((dst_positive_scale_endpoint_second) + (dst_positive_scale_endpoint_second))) + (((dst_negative_code_endpoint_second) + (dst_negative_scale_endpoint_second)) * S ((dst_negative_code_endpoint_second) + (dst_negative_scale_endpoint_second)) + ((dst_negative_scale_endpoint_second) + (dst_negative_scale_endpoint_second)))) * S ((((dst_positive_code_endpoint_second) + (dst_positive_scale_endpoint_second)) * S ((dst_positive_code_endpoint_second) + (dst_positive_scale_endpoint_second)) + ((dst_positive_scale_endpoint_second) + (dst_positive_scale_endpoint_second))) + (((dst_negative_code_endpoint_second) + (dst_negative_scale_endpoint_second)) * S ((dst_negative_code_endpoint_second) + (dst_negative_scale_endpoint_second)) + ((dst_negative_scale_endpoint_second) + (dst_negative_scale_endpoint_second)))) + ((((dst_negative_code_endpoint_second) + (dst_negative_scale_endpoint_second)) * S ((dst_negative_code_endpoint_second) + (dst_negative_scale_endpoint_second)) + ((dst_negative_scale_endpoint_second) + (dst_negative_scale_endpoint_second))) + (((dst_negative_code_endpoint_second) + (dst_negative_scale_endpoint_second)) * S ((dst_negative_code_endpoint_second) + (dst_negative_scale_endpoint_second)) + ((dst_negative_scale_endpoint_second) + (dst_negative_scale_endpoint_second)))))) /\ (((((exists ff_h_pvs_endpoint_secondpositive. ff_h_pvs_endpoint_secondpositive + S (dst_positive_endpoint_second) = S ((S (1)) * dst_positive_scale_endpoint_second)) /\ exists ff_q_pvs_endpoint_secondpositive. dst_positive_code_endpoint_second = ff_q_pvs_endpoint_secondpositive * S ((S (1)) * dst_positive_scale_endpoint_second) + (dst_positive_endpoint_second))) /\ (((((exists ff_h_pvs_endpoint_secondnegative. ff_h_pvs_endpoint_secondnegative + S (dst_negative_endpoint_second) = S ((S (1)) * dst_negative_scale_endpoint_second)) /\ exists ff_q_pvs_endpoint_secondnegative. dst_negative_code_endpoint_second = ff_q_pvs_endpoint_secondnegative * S ((S (1)) * dst_negative_scale_endpoint_second) + (dst_negative_endpoint_second))) /\ (exists ge_balance_positive_endpoint_secondvalue ge_balance_negative_endpoint_secondvalue. (((((b) = 2 * (ge_balance_positive_endpoint_secondvalue) /\ (ge_balance_negative_endpoint_secondvalue) = 0) \/ exists ge_signed_half_endpoint_secondvaluedecode. (((b) = 2 * ge_signed_half_endpoint_secondvaluedecode + 1 /\ (ge_balance_positive_endpoint_secondvalue) = 0) /\ (ge_balance_negative_endpoint_secondvalue) = S ge_signed_half_endpoint_secondvaluedecode))) /\ ((dst_positive_endpoint_second) + ge_balance_negative_endpoint_secondvalue = (dst_negative_endpoint_second) + ge_balance_positive_endpoint_secondvalue))))))))) -> ((((((~((n)=0)) /\ (exists dc_quotient_endpoint_summand dc_left_endpoint_summand dc_right_endpoint_summand. (((n)=(n)*dc_quotient_endpoint_summand) /\ (((exists dst_positive_code_endpoint_summandleft dst_positive_scale_endpoint_summandleft dst_negative_code_endpoint_summandleft dst_negative_scale_endpoint_summandleft dst_positive_endpoint_summandleft dst_negative_endpoint_summandleft. (((F) = (((((dst_positive_code_endpoint_summandleft) + (dst_positive_scale_endpoint_summandleft)) * S ((dst_positive_code_endpoint_summandleft) + (dst_positive_scale_endpoint_summandleft)) + ((dst_positive_scale_endpoint_summandleft) + (dst_positive_scale_endpoint_summandleft))) + (((dst_negative_code_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)) * S ((dst_negative_code_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)) + ((dst_negative_scale_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)))) * S ((((dst_positive_code_endpoint_summandleft) + (dst_positive_scale_endpoint_summandleft)) * S ((dst_positive_code_endpoint_summandleft) + (dst_positive_scale_endpoint_summandleft)) + ((dst_positive_scale_endpoint_summandleft) + (dst_positive_scale_endpoint_summandleft))) + (((dst_negative_code_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)) * S ((dst_negative_code_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)) + ((dst_negative_scale_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)))) + ((((dst_negative_code_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)) * S ((dst_negative_code_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)) + ((dst_negative_scale_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft))) + (((dst_negative_code_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)) * S ((dst_negative_code_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)) + ((dst_negative_scale_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)))))) /\ (((((exists ff_h_pvs_endpoint_summandleftpositive. ff_h_pvs_endpoint_summandleftpositive + S (dst_positive_endpoint_summandleft) = S ((S (n)) * dst_positive_scale_endpoint_summandleft)) /\ exists ff_q_pvs_endpoint_summandleftpositive. dst_positive_code_endpoint_summandleft = ff_q_pvs_endpoint_summandleftpositive * S ((S (n)) * dst_positive_scale_endpoint_summandleft) + (dst_positive_endpoint_summandleft))) /\ (((((exists ff_h_pvs_endpoint_summandleftnegative. ff_h_pvs_endpoint_summandleftnegative + S (dst_negative_endpoint_summandleft) = S ((S (n)) * dst_negative_scale_endpoint_summandleft)) /\ exists ff_q_pvs_endpoint_summandleftnegative. dst_negative_code_endpoint_summandleft = ff_q_pvs_endpoint_summandleftnegative * S ((S (n)) * dst_negative_scale_endpoint_summandleft) + (dst_negative_endpoint_summandleft))) /\ (exists ge_balance_positive_endpoint_summandleftvalue ge_balance_negative_endpoint_summandleftvalue. (((((dc_left_endpoint_summand) = 2 * (ge_balance_positive_endpoint_summandleftvalue) /\ (ge_balance_negative_endpoint_summandleftvalue) = 0) \/ exists ge_signed_half_endpoint_summandleftvaluedecode. (((dc_left_endpoint_summand) = 2 * ge_signed_half_endpoint_summandleftvaluedecode + 1 /\ (ge_balance_positive_endpoint_summandleftvalue) = 0) /\ (ge_balance_negative_endpoint_summandleftvalue) = S ge_signed_half_endpoint_summandleftvaluedecode))) /\ ((dst_positive_endpoint_summandleft) + ge_balance_negative_endpoint_summandleftvalue = (dst_negative_endpoint_summandleft) + ge_balance_positive_endpoint_summandleftvalue))))))))) /\ (((exists dst_positive_code_endpoint_summandright dst_positive_scale_endpoint_summandright dst_negative_code_endpoint_summandright dst_negative_scale_endpoint_summandright dst_positive_endpoint_summandright dst_negative_endpoint_summandright. (((G) = (((((dst_positive_code_endpoint_summandright) + (dst_positive_scale_endpoint_summandright)) * S ((dst_positive_code_endpoint_summandright) + (dst_positive_scale_endpoint_summandright)) + ((dst_positive_scale_endpoint_summandright) + (dst_positive_scale_endpoint_summandright))) + (((dst_negative_code_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)) * S ((dst_negative_code_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)) + ((dst_negative_scale_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)))) * S ((((dst_positive_code_endpoint_summandright) + (dst_positive_scale_endpoint_summandright)) * S ((dst_positive_code_endpoint_summandright) + (dst_positive_scale_endpoint_summandright)) + ((dst_positive_scale_endpoint_summandright) + (dst_positive_scale_endpoint_summandright))) + (((dst_negative_code_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)) * S ((dst_negative_code_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)) + ((dst_negative_scale_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)))) + ((((dst_negative_code_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)) * S ((dst_negative_code_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)) + ((dst_negative_scale_endpoint_summandright) + (dst_negative_scale_endpoint_summandright))) + (((dst_negative_code_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)) * S ((dst_negative_code_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)) + ((dst_negative_scale_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)))))) /\ (((((exists ff_h_pvs_endpoint_summandrightpositive. ff_h_pvs_endpoint_summandrightpositive + S (dst_positive_endpoint_summandright) = S ((S (dc_quotient_endpoint_summand)) * dst_positive_scale_endpoint_summandright)) /\ exists ff_q_pvs_endpoint_summandrightpositive. dst_positive_code_endpoint_summandright = ff_q_pvs_endpoint_summandrightpositive * S ((S (dc_quotient_endpoint_summand)) * dst_positive_scale_endpoint_summandright) + (dst_positive_endpoint_summandright))) /\ (((((exists ff_h_pvs_endpoint_summandrightnegative. ff_h_pvs_endpoint_summandrightnegative + S (dst_negative_endpoint_summandright) = S ((S (dc_quotient_endpoint_summand)) * dst_negative_scale_endpoint_summandright)) /\ exists ff_q_pvs_endpoint_summandrightnegative. dst_negative_code_endpoint_summandright = ff_q_pvs_endpoint_summandrightnegative * S ((S (dc_quotient_endpoint_summand)) * dst_negative_scale_endpoint_summandright) + (dst_negative_endpoint_summandright))) /\ (exists ge_balance_positive_endpoint_summandrightvalue ge_balance_negative_endpoint_summandrightvalue. (((((dc_right_endpoint_summand) = 2 * (ge_balance_positive_endpoint_summandrightvalue) /\ (ge_balance_negative_endpoint_summandrightvalue) = 0) \/ exists ge_signed_half_endpoint_summandrightvaluedecode. (((dc_right_endpoint_summand) = 2 * ge_signed_half_endpoint_summandrightvaluedecode + 1 /\ (ge_balance_positive_endpoint_summandrightvalue) = 0) /\ (ge_balance_negative_endpoint_summandrightvalue) = S ge_signed_half_endpoint_summandrightvaluedecode))) /\ ((dst_positive_endpoint_summandright) + ge_balance_negative_endpoint_summandrightvalue = (dst_negative_endpoint_summandright) + ge_balance_positive_endpoint_summandrightvalue))))))))) /\ (exists sto_ap_endpoint_summandproduct sto_an_endpoint_summandproduct sto_bp_endpoint_summandproduct sto_bn_endpoint_summandproduct sto_cp_endpoint_summandproduct sto_cn_endpoint_summandproduct. (((((dc_left_endpoint_summand) = 2 * (sto_ap_endpoint_summandproduct) /\ (sto_an_endpoint_summandproduct) = 0) \/ exists ge_signed_half_endpoint_summandproductleft. (((dc_left_endpoint_summand) = 2 * ge_signed_half_endpoint_summandproductleft + 1 /\ (sto_ap_endpoint_summandproduct) = 0) /\ (sto_an_endpoint_summandproduct) = S ge_signed_half_endpoint_summandproductleft))) /\ ((((((dc_right_endpoint_summand) = 2 * (sto_bp_endpoint_summandproduct) /\ (sto_bn_endpoint_summandproduct) = 0) \/ exists ge_signed_half_endpoint_summandproductright. (((dc_right_endpoint_summand) = 2 * ge_signed_half_endpoint_summandproductright + 1 /\ (sto_bp_endpoint_summandproduct) = 0) /\ (sto_bn_endpoint_summandproduct) = S ge_signed_half_endpoint_summandproductright))) /\ ((((((z) = 2 * (sto_cp_endpoint_summandproduct) /\ (sto_cn_endpoint_summandproduct) = 0) \/ exists ge_signed_half_endpoint_summandproductoutput. (((z) = 2 * ge_signed_half_endpoint_summandproductoutput + 1 /\ (sto_cp_endpoint_summandproduct) = 0) /\ (sto_cn_endpoint_summandproduct) = S ge_signed_half_endpoint_summandproductoutput))) /\ ((sto_ap_endpoint_summandproduct * sto_bp_endpoint_summandproduct + sto_an_endpoint_summandproduct * sto_bn_endpoint_summandproduct) + sto_cn_endpoint_summandproduct = (sto_ap_endpoint_summandproduct * sto_bn_endpoint_summandproduct + sto_an_endpoint_summandproduct * sto_bp_endpoint_summandproduct) + sto_cp_endpoint_summandproduct))))))))))))))) \/ ((((n)=0 \/ ~(exists pvs_factor_endpoint_summandnondivisor. (n) = (n) * pvs_factor_endpoint_summandnondivisor)) /\ ((z)=0)))) -> (exists sto_ap_endpoint_product sto_an_endpoint_product sto_bp_endpoint_product sto_bn_endpoint_product sto_cp_endpoint_product sto_cn_endpoint_product. (((((a) = 2 * (sto_ap_endpoint_product) /\ (sto_an_endpoint_product) = 0) \/ exists ge_signed_half_endpoint_productleft. (((a) = 2 * ge_signed_half_endpoint_productleft + 1 /\ (sto_ap_endpoint_product) = 0) /\ (sto_an_endpoint_product) = S ge_signed_half_endpoint_productleft))) /\ ((((((b) = 2 * (sto_bp_endpoint_product) /\ (sto_bn_endpoint_product) = 0) \/ exists ge_signed_half_endpoint_productright. (((b) = 2 * ge_signed_half_endpoint_productright + 1 /\ (sto_bp_endpoint_product) = 0) /\ (sto_bn_endpoint_product) = S ge_signed_half_endpoint_productright))) /\ ((((((z) = 2 * (sto_cp_endpoint_product) /\ (sto_cn_endpoint_product) = 0) \/ exists ge_signed_half_endpoint_productoutput. (((z) = 2 * ge_signed_half_endpoint_productoutput + 1 /\ (sto_cp_endpoint_product) = 0) /\ (sto_cn_endpoint_product) = S ge_signed_half_endpoint_productoutput))) /\ ((sto_ap_endpoint_product * sto_bp_endpoint_product + sto_an_endpoint_product * sto_bn_endpoint_product) + sto_cn_endpoint_product = (sto_ap_endpoint_product * sto_bn_endpoint_product + sto_an_endpoint_product * sto_bp_endpoint_product) + sto_cp_endpoint_product)))))))) /\ ((exists sto_ap_endpoint_product sto_an_endpoint_product sto_bp_endpoint_product sto_bn_endpoint_product sto_cp_endpoint_product sto_cn_endpoint_product. (((((a) = 2 * (sto_ap_endpoint_product) /\ (sto_an_endpoint_product) = 0) \/ exists ge_signed_half_endpoint_productleft. (((a) = 2 * ge_signed_half_endpoint_productleft + 1 /\ (sto_ap_endpoint_product) = 0) /\ (sto_an_endpoint_product) = S ge_signed_half_endpoint_productleft))) /\ ((((((b) = 2 * (sto_bp_endpoint_product) /\ (sto_bn_endpoint_product) = 0) \/ exists ge_signed_half_endpoint_productright. (((b) = 2 * ge_signed_half_endpoint_productright + 1 /\ (sto_bp_endpoint_product) = 0) /\ (sto_bn_endpoint_product) = S ge_signed_half_endpoint_productright))) /\ ((((((z) = 2 * (sto_cp_endpoint_product) /\ (sto_cn_endpoint_product) = 0) \/ exists ge_signed_half_endpoint_productoutput. (((z) = 2 * ge_signed_half_endpoint_productoutput + 1 /\ (sto_cp_endpoint_product) = 0) /\ (sto_cn_endpoint_product) = S ge_signed_half_endpoint_productoutput))) /\ ((sto_ap_endpoint_product * sto_bp_endpoint_product + sto_an_endpoint_product * sto_bn_endpoint_product) + sto_cn_endpoint_product = (sto_ap_endpoint_product * sto_bn_endpoint_product + sto_an_endpoint_product * sto_bp_endpoint_product) + sto_cp_endpoint_product))))))) -> ((((~((n)=0)) /\ (exists dc_quotient_endpoint_summand dc_left_endpoint_summand dc_right_endpoint_summand. (((n)=(n)*dc_quotient_endpoint_summand) /\ (((exists dst_positive_code_endpoint_summandleft dst_positive_scale_endpoint_summandleft dst_negative_code_endpoint_summandleft dst_negative_scale_endpoint_summandleft dst_positive_endpoint_summandleft dst_negative_endpoint_summandleft. (((F) = (((((dst_positive_code_endpoint_summandleft) + (dst_positive_scale_endpoint_summandleft)) * S ((dst_positive_code_endpoint_summandleft) + (dst_positive_scale_endpoint_summandleft)) + ((dst_positive_scale_endpoint_summandleft) + (dst_positive_scale_endpoint_summandleft))) + (((dst_negative_code_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)) * S ((dst_negative_code_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)) + ((dst_negative_scale_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)))) * S ((((dst_positive_code_endpoint_summandleft) + (dst_positive_scale_endpoint_summandleft)) * S ((dst_positive_code_endpoint_summandleft) + (dst_positive_scale_endpoint_summandleft)) + ((dst_positive_scale_endpoint_summandleft) + (dst_positive_scale_endpoint_summandleft))) + (((dst_negative_code_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)) * S ((dst_negative_code_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)) + ((dst_negative_scale_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)))) + ((((dst_negative_code_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)) * S ((dst_negative_code_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)) + ((dst_negative_scale_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft))) + (((dst_negative_code_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)) * S ((dst_negative_code_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)) + ((dst_negative_scale_endpoint_summandleft) + (dst_negative_scale_endpoint_summandleft)))))) /\ (((((exists ff_h_pvs_endpoint_summandleftpositive. ff_h_pvs_endpoint_summandleftpositive + S (dst_positive_endpoint_summandleft) = S ((S (n)) * dst_positive_scale_endpoint_summandleft)) /\ exists ff_q_pvs_endpoint_summandleftpositive. dst_positive_code_endpoint_summandleft = ff_q_pvs_endpoint_summandleftpositive * S ((S (n)) * dst_positive_scale_endpoint_summandleft) + (dst_positive_endpoint_summandleft))) /\ (((((exists ff_h_pvs_endpoint_summandleftnegative. ff_h_pvs_endpoint_summandleftnegative + S (dst_negative_endpoint_summandleft) = S ((S (n)) * dst_negative_scale_endpoint_summandleft)) /\ exists ff_q_pvs_endpoint_summandleftnegative. dst_negative_code_endpoint_summandleft = ff_q_pvs_endpoint_summandleftnegative * S ((S (n)) * dst_negative_scale_endpoint_summandleft) + (dst_negative_endpoint_summandleft))) /\ (exists ge_balance_positive_endpoint_summandleftvalue ge_balance_negative_endpoint_summandleftvalue. (((((dc_left_endpoint_summand) = 2 * (ge_balance_positive_endpoint_summandleftvalue) /\ (ge_balance_negative_endpoint_summandleftvalue) = 0) \/ exists ge_signed_half_endpoint_summandleftvaluedecode. (((dc_left_endpoint_summand) = 2 * ge_signed_half_endpoint_summandleftvaluedecode + 1 /\ (ge_balance_positive_endpoint_summandleftvalue) = 0) /\ (ge_balance_negative_endpoint_summandleftvalue) = S ge_signed_half_endpoint_summandleftvaluedecode))) /\ ((dst_positive_endpoint_summandleft) + ge_balance_negative_endpoint_summandleftvalue = (dst_negative_endpoint_summandleft) + ge_balance_positive_endpoint_summandleftvalue))))))))) /\ (((exists dst_positive_code_endpoint_summandright dst_positive_scale_endpoint_summandright dst_negative_code_endpoint_summandright dst_negative_scale_endpoint_summandright dst_positive_endpoint_summandright dst_negative_endpoint_summandright. (((G) = (((((dst_positive_code_endpoint_summandright) + (dst_positive_scale_endpoint_summandright)) * S ((dst_positive_code_endpoint_summandright) + (dst_positive_scale_endpoint_summandright)) + ((dst_positive_scale_endpoint_summandright) + (dst_positive_scale_endpoint_summandright))) + (((dst_negative_code_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)) * S ((dst_negative_code_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)) + ((dst_negative_scale_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)))) * S ((((dst_positive_code_endpoint_summandright) + (dst_positive_scale_endpoint_summandright)) * S ((dst_positive_code_endpoint_summandright) + (dst_positive_scale_endpoint_summandright)) + ((dst_positive_scale_endpoint_summandright) + (dst_positive_scale_endpoint_summandright))) + (((dst_negative_code_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)) * S ((dst_negative_code_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)) + ((dst_negative_scale_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)))) + ((((dst_negative_code_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)) * S ((dst_negative_code_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)) + ((dst_negative_scale_endpoint_summandright) + (dst_negative_scale_endpoint_summandright))) + (((dst_negative_code_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)) * S ((dst_negative_code_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)) + ((dst_negative_scale_endpoint_summandright) + (dst_negative_scale_endpoint_summandright)))))) /\ (((((exists ff_h_pvs_endpoint_summandrightpositive. ff_h_pvs_endpoint_summandrightpositive + S (dst_positive_endpoint_summandright) = S ((S (dc_quotient_endpoint_summand)) * dst_positive_scale_endpoint_summandright)) /\ exists ff_q_pvs_endpoint_summandrightpositive. dst_positive_code_endpoint_summandright = ff_q_pvs_endpoint_summandrightpositive * S ((S (dc_quotient_endpoint_summand)) * dst_positive_scale_endpoint_summandright) + (dst_positive_endpoint_summandright))) /\ (((((exists ff_h_pvs_endpoint_summandrightnegative. ff_h_pvs_endpoint_summandrightnegative + S (dst_negative_endpoint_summandright) = S ((S (dc_quotient_endpoint_summand)) * dst_negative_scale_endpoint_summandright)) /\ exists ff_q_pvs_endpoint_summandrightnegative. dst_negative_code_endpoint_summandright = ff_q_pvs_endpoint_summandrightnegative * S ((S (dc_quotient_endpoint_summand)) * dst_negative_scale_endpoint_summandright) + (dst_negative_endpoint_summandright))) /\ (exists ge_balance_positive_endpoint_summandrightvalue ge_balance_negative_endpoint_summandrightvalue. (((((dc_right_endpoint_summand) = 2 * (ge_balance_positive_endpoint_summandrightvalue) /\ (ge_balance_negative_endpoint_summandrightvalue) = 0) \/ exists ge_signed_half_endpoint_summandrightvaluedecode. (((dc_right_endpoint_summand) = 2 * ge_signed_half_endpoint_summandrightvaluedecode + 1 /\ (ge_balance_positive_endpoint_summandrightvalue) = 0) /\ (ge_balance_negative_endpoint_summandrightvalue) = S ge_signed_half_endpoint_summandrightvaluedecode))) /\ ((dst_positive_endpoint_summandright) + ge_balance_negative_endpoint_summandrightvalue = (dst_negative_endpoint_summandright) + ge_balance_positive_endpoint_summandrightvalue))))))))) /\ (exists sto_ap_endpoint_summandproduct sto_an_endpoint_summandproduct sto_bp_endpoint_summandproduct sto_bn_endpoint_summandproduct sto_cp_endpoint_summandproduct sto_cn_endpoint_summandproduct. (((((dc_left_endpoint_summand) = 2 * (sto_ap_endpoint_summandproduct) /\ (sto_an_endpoint_summandproduct) = 0) \/ exists ge_signed_half_endpoint_summandproductleft. (((dc_left_endpoint_summand) = 2 * ge_signed_half_endpoint_summandproductleft + 1 /\ (sto_ap_endpoint_summandproduct) = 0) /\ (sto_an_endpoint_summandproduct) = S ge_signed_half_endpoint_summandproductleft))) /\ ((((((dc_right_endpoint_summand) = 2 * (sto_bp_endpoint_summandproduct) /\ (sto_bn_endpoint_summandproduct) = 0) \/ exists ge_signed_half_endpoint_summandproductright. (((dc_right_endpoint_summand) = 2 * ge_signed_half_endpoint_summandproductright + 1 /\ (sto_bp_endpoint_summandproduct) = 0) /\ (sto_bn_endpoint_summandproduct) = S ge_signed_half_endpoint_summandproductright))) /\ ((((((z) = 2 * (sto_cp_endpoint_summandproduct) /\ (sto_cn_endpoint_summandproduct) = 0) \/ exists ge_signed_half_endpoint_summandproductoutput. (((z) = 2 * ge_signed_half_endpoint_summandproductoutput + 1 /\ (sto_cp_endpoint_summandproduct) = 0) /\ (sto_cn_endpoint_summandproduct) = S ge_signed_half_endpoint_summandproductoutput))) /\ ((sto_ap_endpoint_summandproduct * sto_bp_endpoint_summandproduct + sto_an_endpoint_summandproduct * sto_bn_endpoint_summandproduct) + sto_cn_endpoint_summandproduct = (sto_ap_endpoint_summandproduct * sto_bn_endpoint_summandproduct + sto_an_endpoint_summandproduct * sto_bp_endpoint_summandproduct) + sto_cp_endpoint_summandproduct))))))))))))))) \/ ((((n)=0 \/ ~(exists pvs_factor_endpoint_summandnondivisor. (n) = (n) * pvs_factor_endpoint_summandnondivisor)) /\ ((z)=0))))))

Complete tactic proof in conservative notation

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

42 script commands · 10 reading checkpoints · 0 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

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

01Fix variables and assumptionsL1–9

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 a
  5. L5
    intro b
  6. L6
    intro z
  7. L7
    intro hn
  8. L8
    intro ha
  9. L9
    intro hb
02Separate the logical casesL10–10

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

  1. L10
    split
03Fix variables and assumptionsL11–11

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

  1. L11
    intro he
04Use earlier factsL12–21

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

  1. L12
    specialize dirichlet_convolution_entry_quotient_product (F)
  2. L13
    specialize dirichlet_convolution_entry_quotient_product (G)
  3. L14
    specialize dirichlet_convolution_entry_quotient_product (n)
  4. L15
    specialize dirichlet_convolution_entry_quotient_product (n)
  5. L16
    specialize dirichlet_convolution_entry_quotient_product (1)
  6. L17
    specialize dirichlet_convolution_entry_quotient_product (a)
  7. L18
    specialize dirichlet_convolution_entry_quotient_product (b)
  8. L19
    specialize dirichlet_convolution_entry_quotient_product (z)
  9. L20
    apply dirichlet_convolution_entry_quotient_product
  10. L21
    exact hn
05Calculate and transport equalitiesL22–22

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

  1. L22
    symm
06Use earlier factsL23–26

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

  1. L23
    apply mul_one
  2. L24
    exact ha
  3. L25
    exact hb
  4. L26
    exact he
07Fix variables and assumptionsL27–27

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

  1. L27
    intro hp
08Use earlier factsL28–37

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

  1. L28
    specialize dirichlet_convolution_entry_from_quotient (F)
  2. L29
    specialize dirichlet_convolution_entry_from_quotient (G)
  3. L30
    specialize dirichlet_convolution_entry_from_quotient (n)
  4. L31
    specialize dirichlet_convolution_entry_from_quotient (n)
  5. L32
    specialize dirichlet_convolution_entry_from_quotient (1)
  6. L33
    specialize dirichlet_convolution_entry_from_quotient (a)
  7. L34
    specialize dirichlet_convolution_entry_from_quotient (b)
  8. L35
    specialize dirichlet_convolution_entry_from_quotient (z)
  9. L36
    apply dirichlet_convolution_entry_from_quotient
  10. L37
    exact hn
09Calculate and transport equalitiesL38–38

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

  1. L38
    symm
10Use earlier factsL39–42

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

  1. L39
    apply mul_one
  2. L40
    exact ha
  3. L41
    exact hb
  4. L42
    exact hp

Library-wide reading audit

Original defined command ledger · 42 lines
  1. 0001intro F
  2. 0002intro G
  3. 0003intro n
  4. 0004intro a
  5. 0005intro b
  6. 0006intro z
  7. 0007intro hn
  8. 0008intro ha
  9. 0009intro hb
  10. 0010split
  11. 0011intro he
  12. 0012specialize dirichlet_convolution_entry_quotient_product (F)
  13. 0013specialize dirichlet_convolution_entry_quotient_product (G)
  14. 0014specialize dirichlet_convolution_entry_quotient_product (n)
  15. 0015specialize dirichlet_convolution_entry_quotient_product (n)
  16. 0016specialize dirichlet_convolution_entry_quotient_product (1)
  17. 0017specialize dirichlet_convolution_entry_quotient_product (a)
  18. 0018specialize dirichlet_convolution_entry_quotient_product (b)
  19. 0019specialize dirichlet_convolution_entry_quotient_product (z)
  20. 0020apply dirichlet_convolution_entry_quotient_product
  21. 0021exact hn
  22. 0022symm
  23. 0023apply mul_one
  24. 0024exact ha
  25. 0025exact hb
  26. 0026exact he
  27. 0027intro hp
  28. 0028specialize dirichlet_convolution_entry_from_quotient (F)
  29. 0029specialize dirichlet_convolution_entry_from_quotient (G)
  30. 0030specialize dirichlet_convolution_entry_from_quotient (n)
  31. 0031specialize dirichlet_convolution_entry_from_quotient (n)
  32. 0032specialize dirichlet_convolution_entry_from_quotient (1)
  33. 0033specialize dirichlet_convolution_entry_from_quotient (a)
  34. 0034specialize dirichlet_convolution_entry_from_quotient (b)
  35. 0035specialize dirichlet_convolution_entry_from_quotient (z)
  36. 0036apply dirichlet_convolution_entry_from_quotient
  37. 0037exact hn
  38. 0038symm
  39. 0039apply mul_one
  40. 0040exact ha
  41. 0041exact hb
  42. 0042exact hp