DU0015

dirichlet_constant_one_entry_from_divisor_mask

Construct the actual bounded complementary lookup and its signed product from a genuine divisor-mask entry; omitted zero/nondivisor entries stay zero.

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.

Signed one is code 2. Positive-only table graphs preserve arbitrary zeroth values, including N=0. The unit and divisor-sum identities are proved, never embedded in definitions. The separate inverse family proves the general unit-at-one criterion; multiplicative-function closure remains open.

Exact theorem in conservative defined notation

∀ N. ∀ F. ∀ U. ∀ n. ∀ d. ∀ z. ConstantOneTable(N,U) → ¬n = 0 → Le(n,N) → DivisorMaskEntry(F,n,d,z) → DirichletEntry(F,U,n,d,z)

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

Definition DAG

ArithAt(F,i,z) · 1DivisorMaskEntry(F,n,d,z) · 1DirichletEntry(F,G,n,d,z) · 1ConstantOneTable(N,U) · 1Le(a,b) · 2

Actual proof prerequisites

factor_nonzero_right · checked external prerequisitele_trans · checked external prerequisitedivisor_le_nonzero · checked external prerequisitemul_comm · checked external prerequisitedirichlet_constant_one_table_valuedivisor_signed_table_lookup · checked external prerequisitedirichlet_convolution_entry_from_quotient · checked external prerequisitesigned_mul_one_right · checked external prerequisite
Original expanded first-order statement 
forall N F U n d z. (((exists dst_positive_code_ones_reverse_sourcetable dst_positive_scale_ones_reverse_sourcetable dst_negative_code_ones_reverse_sourcetable dst_negative_scale_ones_reverse_sourcetable. (((U) = (((((dst_positive_code_ones_reverse_sourcetable) + (dst_positive_scale_ones_reverse_sourcetable)) * S ((dst_positive_code_ones_reverse_sourcetable) + (dst_positive_scale_ones_reverse_sourcetable)) + ((dst_positive_scale_ones_reverse_sourcetable) + (dst_positive_scale_ones_reverse_sourcetable))) + (((dst_negative_code_ones_reverse_sourcetable) + (dst_negative_scale_ones_reverse_sourcetable)) * S ((dst_negative_code_ones_reverse_sourcetable) + (dst_negative_scale_ones_reverse_sourcetable)) + ((dst_negative_scale_ones_reverse_sourcetable) + (dst_negative_scale_ones_reverse_sourcetable)))) * S ((((dst_positive_code_ones_reverse_sourcetable) + (dst_positive_scale_ones_reverse_sourcetable)) * S ((dst_positive_code_ones_reverse_sourcetable) + (dst_positive_scale_ones_reverse_sourcetable)) + ((dst_positive_scale_ones_reverse_sourcetable) + (dst_positive_scale_ones_reverse_sourcetable))) + (((dst_negative_code_ones_reverse_sourcetable) + (dst_negative_scale_ones_reverse_sourcetable)) * S ((dst_negative_code_ones_reverse_sourcetable) + (dst_negative_scale_ones_reverse_sourcetable)) + ((dst_negative_scale_ones_reverse_sourcetable) + (dst_negative_scale_ones_reverse_sourcetable)))) + ((((dst_negative_code_ones_reverse_sourcetable) + (dst_negative_scale_ones_reverse_sourcetable)) * S ((dst_negative_code_ones_reverse_sourcetable) + (dst_negative_scale_ones_reverse_sourcetable)) + ((dst_negative_scale_ones_reverse_sourcetable) + (dst_negative_scale_ones_reverse_sourcetable))) + (((dst_negative_code_ones_reverse_sourcetable) + (dst_negative_scale_ones_reverse_sourcetable)) * S ((dst_negative_code_ones_reverse_sourcetable) + (dst_negative_scale_ones_reverse_sourcetable)) + ((dst_negative_scale_ones_reverse_sourcetable) + (dst_negative_scale_ones_reverse_sourcetable)))))) /\ (forall dst_index_ones_reverse_sourcetable. (exists pvs_le_gap_ones_reverse_sourcetabledomain. pvs_le_gap_ones_reverse_sourcetabledomain + (dst_index_ones_reverse_sourcetable) = (N)) -> exists dst_positive_ones_reverse_sourcetable dst_negative_ones_reverse_sourcetable dst_value_ones_reverse_sourcetable. ((((exists ff_h_pvs_ones_reverse_sourcetableentrypositive. ff_h_pvs_ones_reverse_sourcetableentrypositive + S (dst_positive_ones_reverse_sourcetable) = S ((S (dst_index_ones_reverse_sourcetable)) * dst_positive_scale_ones_reverse_sourcetable)) /\ exists ff_q_pvs_ones_reverse_sourcetableentrypositive. dst_positive_code_ones_reverse_sourcetable = ff_q_pvs_ones_reverse_sourcetableentrypositive * S ((S (dst_index_ones_reverse_sourcetable)) * dst_positive_scale_ones_reverse_sourcetable) + (dst_positive_ones_reverse_sourcetable))) /\ (((((exists ff_h_pvs_ones_reverse_sourcetableentrynegative. ff_h_pvs_ones_reverse_sourcetableentrynegative + S (dst_negative_ones_reverse_sourcetable) = S ((S (dst_index_ones_reverse_sourcetable)) * dst_negative_scale_ones_reverse_sourcetable)) /\ exists ff_q_pvs_ones_reverse_sourcetableentrynegative. dst_negative_code_ones_reverse_sourcetable = ff_q_pvs_ones_reverse_sourcetableentrynegative * S ((S (dst_index_ones_reverse_sourcetable)) * dst_negative_scale_ones_reverse_sourcetable) + (dst_negative_ones_reverse_sourcetable))) /\ (exists ge_balance_positive_ones_reverse_sourcetableentryvalue ge_balance_negative_ones_reverse_sourcetableentryvalue. (((((dst_value_ones_reverse_sourcetable) = 2 * (ge_balance_positive_ones_reverse_sourcetableentryvalue) /\ (ge_balance_negative_ones_reverse_sourcetableentryvalue) = 0) \/ exists ge_signed_half_ones_reverse_sourcetableentryvaluedecode. (((dst_value_ones_reverse_sourcetable) = 2 * ge_signed_half_ones_reverse_sourcetableentryvaluedecode + 1 /\ (ge_balance_positive_ones_reverse_sourcetableentryvalue) = 0) /\ (ge_balance_negative_ones_reverse_sourcetableentryvalue) = S ge_signed_half_ones_reverse_sourcetableentryvaluedecode))) /\ ((dst_positive_ones_reverse_sourcetable) + ge_balance_negative_ones_reverse_sourcetableentryvalue = (dst_negative_ones_reverse_sourcetable) + ge_balance_positive_ones_reverse_sourcetableentryvalue))))))))) /\ (forall du_index_ones_reverse_source du_value_ones_reverse_source. ~(du_index_ones_reverse_source=0) -> (exists pvs_le_gap_ones_reverse_sourcebound. pvs_le_gap_ones_reverse_sourcebound + (du_index_ones_reverse_source) = (N)) -> (exists dst_positive_code_ones_reverse_sourceentry dst_positive_scale_ones_reverse_sourceentry dst_negative_code_ones_reverse_sourceentry dst_negative_scale_ones_reverse_sourceentry dst_positive_ones_reverse_sourceentry dst_negative_ones_reverse_sourceentry. (((U) = (((((dst_positive_code_ones_reverse_sourceentry) + (dst_positive_scale_ones_reverse_sourceentry)) * S ((dst_positive_code_ones_reverse_sourceentry) + (dst_positive_scale_ones_reverse_sourceentry)) + ((dst_positive_scale_ones_reverse_sourceentry) + (dst_positive_scale_ones_reverse_sourceentry))) + (((dst_negative_code_ones_reverse_sourceentry) + (dst_negative_scale_ones_reverse_sourceentry)) * S ((dst_negative_code_ones_reverse_sourceentry) + (dst_negative_scale_ones_reverse_sourceentry)) + ((dst_negative_scale_ones_reverse_sourceentry) + (dst_negative_scale_ones_reverse_sourceentry)))) * S ((((dst_positive_code_ones_reverse_sourceentry) + (dst_positive_scale_ones_reverse_sourceentry)) * S ((dst_positive_code_ones_reverse_sourceentry) + (dst_positive_scale_ones_reverse_sourceentry)) + ((dst_positive_scale_ones_reverse_sourceentry) + (dst_positive_scale_ones_reverse_sourceentry))) + (((dst_negative_code_ones_reverse_sourceentry) + (dst_negative_scale_ones_reverse_sourceentry)) * S ((dst_negative_code_ones_reverse_sourceentry) + (dst_negative_scale_ones_reverse_sourceentry)) + ((dst_negative_scale_ones_reverse_sourceentry) + (dst_negative_scale_ones_reverse_sourceentry)))) + ((((dst_negative_code_ones_reverse_sourceentry) + (dst_negative_scale_ones_reverse_sourceentry)) * S ((dst_negative_code_ones_reverse_sourceentry) + (dst_negative_scale_ones_reverse_sourceentry)) + ((dst_negative_scale_ones_reverse_sourceentry) + (dst_negative_scale_ones_reverse_sourceentry))) + (((dst_negative_code_ones_reverse_sourceentry) + (dst_negative_scale_ones_reverse_sourceentry)) * S ((dst_negative_code_ones_reverse_sourceentry) + (dst_negative_scale_ones_reverse_sourceentry)) + ((dst_negative_scale_ones_reverse_sourceentry) + (dst_negative_scale_ones_reverse_sourceentry)))))) /\ (((((exists ff_h_pvs_ones_reverse_sourceentrypositive. ff_h_pvs_ones_reverse_sourceentrypositive + S (dst_positive_ones_reverse_sourceentry) = S ((S (du_index_ones_reverse_source)) * dst_positive_scale_ones_reverse_sourceentry)) /\ exists ff_q_pvs_ones_reverse_sourceentrypositive. dst_positive_code_ones_reverse_sourceentry = ff_q_pvs_ones_reverse_sourceentrypositive * S ((S (du_index_ones_reverse_source)) * dst_positive_scale_ones_reverse_sourceentry) + (dst_positive_ones_reverse_sourceentry))) /\ (((((exists ff_h_pvs_ones_reverse_sourceentrynegative. ff_h_pvs_ones_reverse_sourceentrynegative + S (dst_negative_ones_reverse_sourceentry) = S ((S (du_index_ones_reverse_source)) * dst_negative_scale_ones_reverse_sourceentry)) /\ exists ff_q_pvs_ones_reverse_sourceentrynegative. dst_negative_code_ones_reverse_sourceentry = ff_q_pvs_ones_reverse_sourceentrynegative * S ((S (du_index_ones_reverse_source)) * dst_negative_scale_ones_reverse_sourceentry) + (dst_negative_ones_reverse_sourceentry))) /\ (exists ge_balance_positive_ones_reverse_sourceentryvalue ge_balance_negative_ones_reverse_sourceentryvalue. (((((du_value_ones_reverse_source) = 2 * (ge_balance_positive_ones_reverse_sourceentryvalue) /\ (ge_balance_negative_ones_reverse_sourceentryvalue) = 0) \/ exists ge_signed_half_ones_reverse_sourceentryvaluedecode. (((du_value_ones_reverse_source) = 2 * ge_signed_half_ones_reverse_sourceentryvaluedecode + 1 /\ (ge_balance_positive_ones_reverse_sourceentryvalue) = 0) /\ (ge_balance_negative_ones_reverse_sourceentryvalue) = S ge_signed_half_ones_reverse_sourceentryvaluedecode))) /\ ((dst_positive_ones_reverse_sourceentry) + ge_balance_negative_ones_reverse_sourceentryvalue = (dst_negative_ones_reverse_sourceentry) + ge_balance_positive_ones_reverse_sourceentryvalue))))))))) -> du_value_ones_reverse_source=2))) -> ~(n=0) -> (exists pvs_le_gap_ones_reverse_bound. pvs_le_gap_ones_reverse_bound + (n) = (N)) -> ((((~((d)=0)) /\ (exists dm_quotient_ones_reverse_mask. (((n)=(d)*dm_quotient_ones_reverse_mask) /\ (exists dst_positive_code_ones_reverse_maskinput dst_positive_scale_ones_reverse_maskinput dst_negative_code_ones_reverse_maskinput dst_negative_scale_ones_reverse_maskinput dst_positive_ones_reverse_maskinput dst_negative_ones_reverse_maskinput. (((F) = (((((dst_positive_code_ones_reverse_maskinput) + (dst_positive_scale_ones_reverse_maskinput)) * S ((dst_positive_code_ones_reverse_maskinput) + (dst_positive_scale_ones_reverse_maskinput)) + ((dst_positive_scale_ones_reverse_maskinput) + (dst_positive_scale_ones_reverse_maskinput))) + (((dst_negative_code_ones_reverse_maskinput) + (dst_negative_scale_ones_reverse_maskinput)) * S ((dst_negative_code_ones_reverse_maskinput) + (dst_negative_scale_ones_reverse_maskinput)) + ((dst_negative_scale_ones_reverse_maskinput) + (dst_negative_scale_ones_reverse_maskinput)))) * S ((((dst_positive_code_ones_reverse_maskinput) + (dst_positive_scale_ones_reverse_maskinput)) * S ((dst_positive_code_ones_reverse_maskinput) + (dst_positive_scale_ones_reverse_maskinput)) + ((dst_positive_scale_ones_reverse_maskinput) + (dst_positive_scale_ones_reverse_maskinput))) + (((dst_negative_code_ones_reverse_maskinput) + (dst_negative_scale_ones_reverse_maskinput)) * S ((dst_negative_code_ones_reverse_maskinput) + (dst_negative_scale_ones_reverse_maskinput)) + ((dst_negative_scale_ones_reverse_maskinput) + (dst_negative_scale_ones_reverse_maskinput)))) + ((((dst_negative_code_ones_reverse_maskinput) + (dst_negative_scale_ones_reverse_maskinput)) * S ((dst_negative_code_ones_reverse_maskinput) + (dst_negative_scale_ones_reverse_maskinput)) + ((dst_negative_scale_ones_reverse_maskinput) + (dst_negative_scale_ones_reverse_maskinput))) + (((dst_negative_code_ones_reverse_maskinput) + (dst_negative_scale_ones_reverse_maskinput)) * S ((dst_negative_code_ones_reverse_maskinput) + (dst_negative_scale_ones_reverse_maskinput)) + ((dst_negative_scale_ones_reverse_maskinput) + (dst_negative_scale_ones_reverse_maskinput)))))) /\ (((((exists ff_h_pvs_ones_reverse_maskinputpositive. ff_h_pvs_ones_reverse_maskinputpositive + S (dst_positive_ones_reverse_maskinput) = S ((S (d)) * dst_positive_scale_ones_reverse_maskinput)) /\ exists ff_q_pvs_ones_reverse_maskinputpositive. dst_positive_code_ones_reverse_maskinput = ff_q_pvs_ones_reverse_maskinputpositive * S ((S (d)) * dst_positive_scale_ones_reverse_maskinput) + (dst_positive_ones_reverse_maskinput))) /\ (((((exists ff_h_pvs_ones_reverse_maskinputnegative. ff_h_pvs_ones_reverse_maskinputnegative + S (dst_negative_ones_reverse_maskinput) = S ((S (d)) * dst_negative_scale_ones_reverse_maskinput)) /\ exists ff_q_pvs_ones_reverse_maskinputnegative. dst_negative_code_ones_reverse_maskinput = ff_q_pvs_ones_reverse_maskinputnegative * S ((S (d)) * dst_negative_scale_ones_reverse_maskinput) + (dst_negative_ones_reverse_maskinput))) /\ (exists ge_balance_positive_ones_reverse_maskinputvalue ge_balance_negative_ones_reverse_maskinputvalue. (((((z) = 2 * (ge_balance_positive_ones_reverse_maskinputvalue) /\ (ge_balance_negative_ones_reverse_maskinputvalue) = 0) \/ exists ge_signed_half_ones_reverse_maskinputvaluedecode. (((z) = 2 * ge_signed_half_ones_reverse_maskinputvaluedecode + 1 /\ (ge_balance_positive_ones_reverse_maskinputvalue) = 0) /\ (ge_balance_negative_ones_reverse_maskinputvalue) = S ge_signed_half_ones_reverse_maskinputvaluedecode))) /\ ((dst_positive_ones_reverse_maskinput) + ge_balance_negative_ones_reverse_maskinputvalue = (dst_negative_ones_reverse_maskinput) + ge_balance_positive_ones_reverse_maskinputvalue))))))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_ones_reverse_masknondivisor. (n) = (d) * pvs_factor_ones_reverse_masknondivisor)) /\ ((z)=0)))) -> ((((~((d)=0)) /\ (exists dc_quotient_ones_reverse_convolution dc_left_ones_reverse_convolution dc_right_ones_reverse_convolution. (((n)=(d)*dc_quotient_ones_reverse_convolution) /\ (((exists dst_positive_code_ones_reverse_convolutionleft dst_positive_scale_ones_reverse_convolutionleft dst_negative_code_ones_reverse_convolutionleft dst_negative_scale_ones_reverse_convolutionleft dst_positive_ones_reverse_convolutionleft dst_negative_ones_reverse_convolutionleft. (((F) = (((((dst_positive_code_ones_reverse_convolutionleft) + (dst_positive_scale_ones_reverse_convolutionleft)) * S ((dst_positive_code_ones_reverse_convolutionleft) + (dst_positive_scale_ones_reverse_convolutionleft)) + ((dst_positive_scale_ones_reverse_convolutionleft) + (dst_positive_scale_ones_reverse_convolutionleft))) + (((dst_negative_code_ones_reverse_convolutionleft) + (dst_negative_scale_ones_reverse_convolutionleft)) * S ((dst_negative_code_ones_reverse_convolutionleft) + (dst_negative_scale_ones_reverse_convolutionleft)) + ((dst_negative_scale_ones_reverse_convolutionleft) + (dst_negative_scale_ones_reverse_convolutionleft)))) * S ((((dst_positive_code_ones_reverse_convolutionleft) + (dst_positive_scale_ones_reverse_convolutionleft)) * S ((dst_positive_code_ones_reverse_convolutionleft) + (dst_positive_scale_ones_reverse_convolutionleft)) + ((dst_positive_scale_ones_reverse_convolutionleft) + (dst_positive_scale_ones_reverse_convolutionleft))) + (((dst_negative_code_ones_reverse_convolutionleft) + (dst_negative_scale_ones_reverse_convolutionleft)) * S ((dst_negative_code_ones_reverse_convolutionleft) + (dst_negative_scale_ones_reverse_convolutionleft)) + ((dst_negative_scale_ones_reverse_convolutionleft) + (dst_negative_scale_ones_reverse_convolutionleft)))) + ((((dst_negative_code_ones_reverse_convolutionleft) + (dst_negative_scale_ones_reverse_convolutionleft)) * S ((dst_negative_code_ones_reverse_convolutionleft) + (dst_negative_scale_ones_reverse_convolutionleft)) + ((dst_negative_scale_ones_reverse_convolutionleft) + (dst_negative_scale_ones_reverse_convolutionleft))) + (((dst_negative_code_ones_reverse_convolutionleft) + (dst_negative_scale_ones_reverse_convolutionleft)) * S ((dst_negative_code_ones_reverse_convolutionleft) + (dst_negative_scale_ones_reverse_convolutionleft)) + ((dst_negative_scale_ones_reverse_convolutionleft) + (dst_negative_scale_ones_reverse_convolutionleft)))))) /\ (((((exists ff_h_pvs_ones_reverse_convolutionleftpositive. ff_h_pvs_ones_reverse_convolutionleftpositive + S (dst_positive_ones_reverse_convolutionleft) = S ((S (d)) * dst_positive_scale_ones_reverse_convolutionleft)) /\ exists ff_q_pvs_ones_reverse_convolutionleftpositive. dst_positive_code_ones_reverse_convolutionleft = ff_q_pvs_ones_reverse_convolutionleftpositive * S ((S (d)) * dst_positive_scale_ones_reverse_convolutionleft) + (dst_positive_ones_reverse_convolutionleft))) /\ (((((exists ff_h_pvs_ones_reverse_convolutionleftnegative. ff_h_pvs_ones_reverse_convolutionleftnegative + S (dst_negative_ones_reverse_convolutionleft) = S ((S (d)) * dst_negative_scale_ones_reverse_convolutionleft)) /\ exists ff_q_pvs_ones_reverse_convolutionleftnegative. dst_negative_code_ones_reverse_convolutionleft = ff_q_pvs_ones_reverse_convolutionleftnegative * S ((S (d)) * dst_negative_scale_ones_reverse_convolutionleft) + (dst_negative_ones_reverse_convolutionleft))) /\ (exists ge_balance_positive_ones_reverse_convolutionleftvalue ge_balance_negative_ones_reverse_convolutionleftvalue. (((((dc_left_ones_reverse_convolution) = 2 * (ge_balance_positive_ones_reverse_convolutionleftvalue) /\ (ge_balance_negative_ones_reverse_convolutionleftvalue) = 0) \/ exists ge_signed_half_ones_reverse_convolutionleftvaluedecode. (((dc_left_ones_reverse_convolution) = 2 * ge_signed_half_ones_reverse_convolutionleftvaluedecode + 1 /\ (ge_balance_positive_ones_reverse_convolutionleftvalue) = 0) /\ (ge_balance_negative_ones_reverse_convolutionleftvalue) = S ge_signed_half_ones_reverse_convolutionleftvaluedecode))) /\ ((dst_positive_ones_reverse_convolutionleft) + ge_balance_negative_ones_reverse_convolutionleftvalue = (dst_negative_ones_reverse_convolutionleft) + ge_balance_positive_ones_reverse_convolutionleftvalue))))))))) /\ (((exists dst_positive_code_ones_reverse_convolutionright dst_positive_scale_ones_reverse_convolutionright dst_negative_code_ones_reverse_convolutionright dst_negative_scale_ones_reverse_convolutionright dst_positive_ones_reverse_convolutionright dst_negative_ones_reverse_convolutionright. (((U) = (((((dst_positive_code_ones_reverse_convolutionright) + (dst_positive_scale_ones_reverse_convolutionright)) * S ((dst_positive_code_ones_reverse_convolutionright) + (dst_positive_scale_ones_reverse_convolutionright)) + ((dst_positive_scale_ones_reverse_convolutionright) + (dst_positive_scale_ones_reverse_convolutionright))) + (((dst_negative_code_ones_reverse_convolutionright) + (dst_negative_scale_ones_reverse_convolutionright)) * S ((dst_negative_code_ones_reverse_convolutionright) + (dst_negative_scale_ones_reverse_convolutionright)) + ((dst_negative_scale_ones_reverse_convolutionright) + (dst_negative_scale_ones_reverse_convolutionright)))) * S ((((dst_positive_code_ones_reverse_convolutionright) + (dst_positive_scale_ones_reverse_convolutionright)) * S ((dst_positive_code_ones_reverse_convolutionright) + (dst_positive_scale_ones_reverse_convolutionright)) + ((dst_positive_scale_ones_reverse_convolutionright) + (dst_positive_scale_ones_reverse_convolutionright))) + (((dst_negative_code_ones_reverse_convolutionright) + (dst_negative_scale_ones_reverse_convolutionright)) * S ((dst_negative_code_ones_reverse_convolutionright) + (dst_negative_scale_ones_reverse_convolutionright)) + ((dst_negative_scale_ones_reverse_convolutionright) + (dst_negative_scale_ones_reverse_convolutionright)))) + ((((dst_negative_code_ones_reverse_convolutionright) + (dst_negative_scale_ones_reverse_convolutionright)) * S ((dst_negative_code_ones_reverse_convolutionright) + (dst_negative_scale_ones_reverse_convolutionright)) + ((dst_negative_scale_ones_reverse_convolutionright) + (dst_negative_scale_ones_reverse_convolutionright))) + (((dst_negative_code_ones_reverse_convolutionright) + (dst_negative_scale_ones_reverse_convolutionright)) * S ((dst_negative_code_ones_reverse_convolutionright) + (dst_negative_scale_ones_reverse_convolutionright)) + ((dst_negative_scale_ones_reverse_convolutionright) + (dst_negative_scale_ones_reverse_convolutionright)))))) /\ (((((exists ff_h_pvs_ones_reverse_convolutionrightpositive. ff_h_pvs_ones_reverse_convolutionrightpositive + S (dst_positive_ones_reverse_convolutionright) = S ((S (dc_quotient_ones_reverse_convolution)) * dst_positive_scale_ones_reverse_convolutionright)) /\ exists ff_q_pvs_ones_reverse_convolutionrightpositive. dst_positive_code_ones_reverse_convolutionright = ff_q_pvs_ones_reverse_convolutionrightpositive * S ((S (dc_quotient_ones_reverse_convolution)) * dst_positive_scale_ones_reverse_convolutionright) + (dst_positive_ones_reverse_convolutionright))) /\ (((((exists ff_h_pvs_ones_reverse_convolutionrightnegative. ff_h_pvs_ones_reverse_convolutionrightnegative + S (dst_negative_ones_reverse_convolutionright) = S ((S (dc_quotient_ones_reverse_convolution)) * dst_negative_scale_ones_reverse_convolutionright)) /\ exists ff_q_pvs_ones_reverse_convolutionrightnegative. dst_negative_code_ones_reverse_convolutionright = ff_q_pvs_ones_reverse_convolutionrightnegative * S ((S (dc_quotient_ones_reverse_convolution)) * dst_negative_scale_ones_reverse_convolutionright) + (dst_negative_ones_reverse_convolutionright))) /\ (exists ge_balance_positive_ones_reverse_convolutionrightvalue ge_balance_negative_ones_reverse_convolutionrightvalue. (((((dc_right_ones_reverse_convolution) = 2 * (ge_balance_positive_ones_reverse_convolutionrightvalue) /\ (ge_balance_negative_ones_reverse_convolutionrightvalue) = 0) \/ exists ge_signed_half_ones_reverse_convolutionrightvaluedecode. (((dc_right_ones_reverse_convolution) = 2 * ge_signed_half_ones_reverse_convolutionrightvaluedecode + 1 /\ (ge_balance_positive_ones_reverse_convolutionrightvalue) = 0) /\ (ge_balance_negative_ones_reverse_convolutionrightvalue) = S ge_signed_half_ones_reverse_convolutionrightvaluedecode))) /\ ((dst_positive_ones_reverse_convolutionright) + ge_balance_negative_ones_reverse_convolutionrightvalue = (dst_negative_ones_reverse_convolutionright) + ge_balance_positive_ones_reverse_convolutionrightvalue))))))))) /\ (exists sto_ap_ones_reverse_convolutionproduct sto_an_ones_reverse_convolutionproduct sto_bp_ones_reverse_convolutionproduct sto_bn_ones_reverse_convolutionproduct sto_cp_ones_reverse_convolutionproduct sto_cn_ones_reverse_convolutionproduct. (((((dc_left_ones_reverse_convolution) = 2 * (sto_ap_ones_reverse_convolutionproduct) /\ (sto_an_ones_reverse_convolutionproduct) = 0) \/ exists ge_signed_half_ones_reverse_convolutionproductleft. (((dc_left_ones_reverse_convolution) = 2 * ge_signed_half_ones_reverse_convolutionproductleft + 1 /\ (sto_ap_ones_reverse_convolutionproduct) = 0) /\ (sto_an_ones_reverse_convolutionproduct) = S ge_signed_half_ones_reverse_convolutionproductleft))) /\ ((((((dc_right_ones_reverse_convolution) = 2 * (sto_bp_ones_reverse_convolutionproduct) /\ (sto_bn_ones_reverse_convolutionproduct) = 0) \/ exists ge_signed_half_ones_reverse_convolutionproductright. (((dc_right_ones_reverse_convolution) = 2 * ge_signed_half_ones_reverse_convolutionproductright + 1 /\ (sto_bp_ones_reverse_convolutionproduct) = 0) /\ (sto_bn_ones_reverse_convolutionproduct) = S ge_signed_half_ones_reverse_convolutionproductright))) /\ ((((((z) = 2 * (sto_cp_ones_reverse_convolutionproduct) /\ (sto_cn_ones_reverse_convolutionproduct) = 0) \/ exists ge_signed_half_ones_reverse_convolutionproductoutput. (((z) = 2 * ge_signed_half_ones_reverse_convolutionproductoutput + 1 /\ (sto_cp_ones_reverse_convolutionproduct) = 0) /\ (sto_cn_ones_reverse_convolutionproduct) = S ge_signed_half_ones_reverse_convolutionproductoutput))) /\ ((sto_ap_ones_reverse_convolutionproduct * sto_bp_ones_reverse_convolutionproduct + sto_an_ones_reverse_convolutionproduct * sto_bn_ones_reverse_convolutionproduct) + sto_cn_ones_reverse_convolutionproduct = (sto_ap_ones_reverse_convolutionproduct * sto_bn_ones_reverse_convolutionproduct + sto_an_ones_reverse_convolutionproduct * sto_bp_ones_reverse_convolutionproduct) + sto_cp_ones_reverse_convolutionproduct))))))))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_ones_reverse_convolutionnondivisor. (n) = (d) * pvs_factor_ones_reverse_convolutionnondivisor)) /\ ((z)=0))))

Complete tactic proof in conservative notation

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

76 script commands · 16 reading checkpoints · 4 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 (1)
dirichlet constant one table value
01Fix variables and assumptionsL1–10

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

  1. L1
    intro N
  2. L2
    intro F
  3. L3
    intro U
  4. L4
    intro n
  5. L5
    intro d
  6. L6
    intro z
  7. L7
    intro hu
  8. L8
    intro hn
  9. L9
    intro hb
  10. L10
    intro he
02Separate the logical casesL11–14

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

  1. L11
    cases he
  2. L12
    cases he_left
  3. L13
    cases he_left_right
  4. L14
    cases he_left_right_witness
03Establish hqpositiveL15–23

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

  1. L15
    have hqpositive : ~(x=0)
  2. L16
    intro hqzero
  3. L17
    specialize factor_nonzero_right (n)
  4. L18
    specialize factor_nonzero_right (d)
  5. L19
    specialize factor_nonzero_right (x)
  6. L20
    apply factor_nonzero_right
  7. L21
    exact hn
  8. L22
    exact he_left_right_witness_left
  9. L23
    exact hqzero
04Establish hqboundL24–32

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

  1. L24
    have hqbound : Le(x,N)Definitions: Le(x,N)Original native command in the exact edition
  2. L25
    specialize le_trans (x)
  3. L26
    specialize le_trans (n)
  4. L27
    specialize le_trans (N)
  5. L28
    apply le_trans
  6. L29
    specialize divisor_le_nonzero (x)
  7. L30
    specialize divisor_le_nonzero (n)
  8. L31
    apply divisor_le_nonzero
  9. L32
    exact hn
05Construct an explicit witnessL33–33

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

  1. L33
    exists d
06Calculate and transport equalitiesL34–34

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

  1. L34
    trans (d)*(x)
07Use earlier factsL35–37

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

  1. L35
    exact he_left_right_witness_left
  2. L36
    apply mul_comm
  3. L37
    exact hb
08Separate the logical casesL38–38

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

  1. L38
    cases hu
09Establish hvL39–45

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

  1. L39
    have hv : ∃ v. ArithAt(U,x,v)Definitions: ArithAt(U,x,v)Original native command in the exact edition
  2. L40
    specialize divisor_signed_table_lookup (N)
  3. L41
    specialize divisor_signed_table_lookup (U)
  4. L42
    specialize divisor_signed_table_lookup (x)
  5. L43
    apply divisor_signed_table_lookup
  6. L44
    exact hu_left
  7. L45
    exact hqbound
10Separate the logical casesL46–46

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

  1. L46
    cases hv
11Establish heqL47–56

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet constant one table value.

  1. L47
    have heq : x1=2
  2. L48
    specialize dirichlet_constant_one_table_value (N)
  3. L49
    specialize dirichlet_constant_one_table_value (U)
  4. L50
    specialize dirichlet_constant_one_table_value (x)
  5. L51
    specialize dirichlet_constant_one_table_value (x1)
  6. L52
    apply dirichlet_constant_one_table_value
  7. L53
    exact hu
  8. L54
    exact hqpositive
  9. L55
    exact hqbound
  10. L56
    exact hv_witness
12Calculate and transport equalitiesL57–58

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

  1. L57
    rewrite heq at hv_witness
  2. L58
    rewrite heq at hv_witness
13Use earlier factsL59–68

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

  1. L59
    specialize dirichlet_convolution_entry_from_quotient (F)
  2. L60
    specialize dirichlet_convolution_entry_from_quotient (U)
  3. L61
    specialize dirichlet_convolution_entry_from_quotient (n)
  4. L62
    specialize dirichlet_convolution_entry_from_quotient (d)
  5. L63
    specialize dirichlet_convolution_entry_from_quotient (x)
  6. L64
    specialize dirichlet_convolution_entry_from_quotient (z)
  7. L65
    specialize dirichlet_convolution_entry_from_quotient (2)
  8. L66
    specialize dirichlet_convolution_entry_from_quotient (z)
  9. L67
    apply dirichlet_convolution_entry_from_quotient
  10. L68
    exact he_left_left
14Use earlier factsL69–73

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

  1. L69
    exact he_left_right_witness_left
  2. L70
    exact he_left_right_witness_right
  3. L71
    exact hv_witness
  4. L72
    specialize signed_mul_one_right (z)
  5. L73
    apply signed_mul_one_right
15Separate the logical casesL74–75

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

  1. L74
    cases he_right
  2. L75
    right
16Use earlier factsL76–76

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

  1. L76
    exact he_right

Library-wide reading audit

Original defined command ledger · 76 lines
  1. 0001intro N
  2. 0002intro F
  3. 0003intro U
  4. 0004intro n
  5. 0005intro d
  6. 0006intro z
  7. 0007intro hu
  8. 0008intro hn
  9. 0009intro hb
  10. 0010intro he
  11. 0011cases he
  12. 0012cases he_left
  13. 0013cases he_left_right
  14. 0014cases he_left_right_witness
  15. 0015have hqpositive : ~(x=0)
  16. 0016intro hqzero
  17. 0017specialize factor_nonzero_right (n)
  18. 0018specialize factor_nonzero_right (d)
  19. 0019specialize factor_nonzero_right (x)
  20. 0020apply factor_nonzero_right
  21. 0021exact hn
  22. 0022exact he_left_right_witness_left
  23. 0023exact hqzero
  24. 0024have hqbound : Le(x,N)
  25. 0025specialize le_trans (x)
  26. 0026specialize le_trans (n)
  27. 0027specialize le_trans (N)
  28. 0028apply le_trans
  29. 0029specialize divisor_le_nonzero (x)
  30. 0030specialize divisor_le_nonzero (n)
  31. 0031apply divisor_le_nonzero
  32. 0032exact hn
  33. 0033exists d
  34. 0034trans (d)*(x)
  35. 0035exact he_left_right_witness_left
  36. 0036apply mul_comm
  37. 0037exact hb
  38. 0038cases hu
  39. 0039have hv : ∃ v. ArithAt(U,x,v)
  40. 0040specialize divisor_signed_table_lookup (N)
  41. 0041specialize divisor_signed_table_lookup (U)
  42. 0042specialize divisor_signed_table_lookup (x)
  43. 0043apply divisor_signed_table_lookup
  44. 0044exact hu_left
  45. 0045exact hqbound
  46. 0046cases hv
  47. 0047have heq : x1=2
  48. 0048specialize dirichlet_constant_one_table_value (N)
  49. 0049specialize dirichlet_constant_one_table_value (U)
  50. 0050specialize dirichlet_constant_one_table_value (x)
  51. 0051specialize dirichlet_constant_one_table_value (x1)
  52. 0052apply dirichlet_constant_one_table_value
  53. 0053exact hu
  54. 0054exact hqpositive
  55. 0055exact hqbound
  56. 0056exact hv_witness
  57. 0057rewrite heq at hv_witness
  58. 0058rewrite heq at hv_witness
  59. 0059specialize dirichlet_convolution_entry_from_quotient (F)
  60. 0060specialize dirichlet_convolution_entry_from_quotient (U)
  61. 0061specialize dirichlet_convolution_entry_from_quotient (n)
  62. 0062specialize dirichlet_convolution_entry_from_quotient (d)
  63. 0063specialize dirichlet_convolution_entry_from_quotient (x)
  64. 0064specialize dirichlet_convolution_entry_from_quotient (z)
  65. 0065specialize dirichlet_convolution_entry_from_quotient (2)
  66. 0066specialize dirichlet_convolution_entry_from_quotient (z)
  67. 0067apply dirichlet_convolution_entry_from_quotient
  68. 0068exact he_left_left
  69. 0069exact he_left_right_witness_left
  70. 0070exact he_left_right_witness_right
  71. 0071exact hv_witness
  72. 0072specialize signed_mul_one_right (z)
  73. 0073apply signed_mul_one_right
  74. 0074cases he_right
  75. 0075right
  76. 0076exact he_right