DU0014

dirichlet_constant_one_entry_to_divisor_mask

At every actual positive divisor the complementary one-table factor is signed one, so the convolution entry is precisely the existing divisor-mask entry.

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) → DirichletEntry(F,U,n,d,z) → DivisorMaskEntry(F,n,d,z)

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

Definition DAG

DivisorMaskEntry(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_valuesigned_mul_functional · 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_entry_sourcetable dst_positive_scale_ones_entry_sourcetable dst_negative_code_ones_entry_sourcetable dst_negative_scale_ones_entry_sourcetable. (((U) = (((((dst_positive_code_ones_entry_sourcetable) + (dst_positive_scale_ones_entry_sourcetable)) * S ((dst_positive_code_ones_entry_sourcetable) + (dst_positive_scale_ones_entry_sourcetable)) + ((dst_positive_scale_ones_entry_sourcetable) + (dst_positive_scale_ones_entry_sourcetable))) + (((dst_negative_code_ones_entry_sourcetable) + (dst_negative_scale_ones_entry_sourcetable)) * S ((dst_negative_code_ones_entry_sourcetable) + (dst_negative_scale_ones_entry_sourcetable)) + ((dst_negative_scale_ones_entry_sourcetable) + (dst_negative_scale_ones_entry_sourcetable)))) * S ((((dst_positive_code_ones_entry_sourcetable) + (dst_positive_scale_ones_entry_sourcetable)) * S ((dst_positive_code_ones_entry_sourcetable) + (dst_positive_scale_ones_entry_sourcetable)) + ((dst_positive_scale_ones_entry_sourcetable) + (dst_positive_scale_ones_entry_sourcetable))) + (((dst_negative_code_ones_entry_sourcetable) + (dst_negative_scale_ones_entry_sourcetable)) * S ((dst_negative_code_ones_entry_sourcetable) + (dst_negative_scale_ones_entry_sourcetable)) + ((dst_negative_scale_ones_entry_sourcetable) + (dst_negative_scale_ones_entry_sourcetable)))) + ((((dst_negative_code_ones_entry_sourcetable) + (dst_negative_scale_ones_entry_sourcetable)) * S ((dst_negative_code_ones_entry_sourcetable) + (dst_negative_scale_ones_entry_sourcetable)) + ((dst_negative_scale_ones_entry_sourcetable) + (dst_negative_scale_ones_entry_sourcetable))) + (((dst_negative_code_ones_entry_sourcetable) + (dst_negative_scale_ones_entry_sourcetable)) * S ((dst_negative_code_ones_entry_sourcetable) + (dst_negative_scale_ones_entry_sourcetable)) + ((dst_negative_scale_ones_entry_sourcetable) + (dst_negative_scale_ones_entry_sourcetable)))))) /\ (forall dst_index_ones_entry_sourcetable. (exists pvs_le_gap_ones_entry_sourcetabledomain. pvs_le_gap_ones_entry_sourcetabledomain + (dst_index_ones_entry_sourcetable) = (N)) -> exists dst_positive_ones_entry_sourcetable dst_negative_ones_entry_sourcetable dst_value_ones_entry_sourcetable. ((((exists ff_h_pvs_ones_entry_sourcetableentrypositive. ff_h_pvs_ones_entry_sourcetableentrypositive + S (dst_positive_ones_entry_sourcetable) = S ((S (dst_index_ones_entry_sourcetable)) * dst_positive_scale_ones_entry_sourcetable)) /\ exists ff_q_pvs_ones_entry_sourcetableentrypositive. dst_positive_code_ones_entry_sourcetable = ff_q_pvs_ones_entry_sourcetableentrypositive * S ((S (dst_index_ones_entry_sourcetable)) * dst_positive_scale_ones_entry_sourcetable) + (dst_positive_ones_entry_sourcetable))) /\ (((((exists ff_h_pvs_ones_entry_sourcetableentrynegative. ff_h_pvs_ones_entry_sourcetableentrynegative + S (dst_negative_ones_entry_sourcetable) = S ((S (dst_index_ones_entry_sourcetable)) * dst_negative_scale_ones_entry_sourcetable)) /\ exists ff_q_pvs_ones_entry_sourcetableentrynegative. dst_negative_code_ones_entry_sourcetable = ff_q_pvs_ones_entry_sourcetableentrynegative * S ((S (dst_index_ones_entry_sourcetable)) * dst_negative_scale_ones_entry_sourcetable) + (dst_negative_ones_entry_sourcetable))) /\ (exists ge_balance_positive_ones_entry_sourcetableentryvalue ge_balance_negative_ones_entry_sourcetableentryvalue. (((((dst_value_ones_entry_sourcetable) = 2 * (ge_balance_positive_ones_entry_sourcetableentryvalue) /\ (ge_balance_negative_ones_entry_sourcetableentryvalue) = 0) \/ exists ge_signed_half_ones_entry_sourcetableentryvaluedecode. (((dst_value_ones_entry_sourcetable) = 2 * ge_signed_half_ones_entry_sourcetableentryvaluedecode + 1 /\ (ge_balance_positive_ones_entry_sourcetableentryvalue) = 0) /\ (ge_balance_negative_ones_entry_sourcetableentryvalue) = S ge_signed_half_ones_entry_sourcetableentryvaluedecode))) /\ ((dst_positive_ones_entry_sourcetable) + ge_balance_negative_ones_entry_sourcetableentryvalue = (dst_negative_ones_entry_sourcetable) + ge_balance_positive_ones_entry_sourcetableentryvalue))))))))) /\ (forall du_index_ones_entry_source du_value_ones_entry_source. ~(du_index_ones_entry_source=0) -> (exists pvs_le_gap_ones_entry_sourcebound. pvs_le_gap_ones_entry_sourcebound + (du_index_ones_entry_source) = (N)) -> (exists dst_positive_code_ones_entry_sourceentry dst_positive_scale_ones_entry_sourceentry dst_negative_code_ones_entry_sourceentry dst_negative_scale_ones_entry_sourceentry dst_positive_ones_entry_sourceentry dst_negative_ones_entry_sourceentry. (((U) = (((((dst_positive_code_ones_entry_sourceentry) + (dst_positive_scale_ones_entry_sourceentry)) * S ((dst_positive_code_ones_entry_sourceentry) + (dst_positive_scale_ones_entry_sourceentry)) + ((dst_positive_scale_ones_entry_sourceentry) + (dst_positive_scale_ones_entry_sourceentry))) + (((dst_negative_code_ones_entry_sourceentry) + (dst_negative_scale_ones_entry_sourceentry)) * S ((dst_negative_code_ones_entry_sourceentry) + (dst_negative_scale_ones_entry_sourceentry)) + ((dst_negative_scale_ones_entry_sourceentry) + (dst_negative_scale_ones_entry_sourceentry)))) * S ((((dst_positive_code_ones_entry_sourceentry) + (dst_positive_scale_ones_entry_sourceentry)) * S ((dst_positive_code_ones_entry_sourceentry) + (dst_positive_scale_ones_entry_sourceentry)) + ((dst_positive_scale_ones_entry_sourceentry) + (dst_positive_scale_ones_entry_sourceentry))) + (((dst_negative_code_ones_entry_sourceentry) + (dst_negative_scale_ones_entry_sourceentry)) * S ((dst_negative_code_ones_entry_sourceentry) + (dst_negative_scale_ones_entry_sourceentry)) + ((dst_negative_scale_ones_entry_sourceentry) + (dst_negative_scale_ones_entry_sourceentry)))) + ((((dst_negative_code_ones_entry_sourceentry) + (dst_negative_scale_ones_entry_sourceentry)) * S ((dst_negative_code_ones_entry_sourceentry) + (dst_negative_scale_ones_entry_sourceentry)) + ((dst_negative_scale_ones_entry_sourceentry) + (dst_negative_scale_ones_entry_sourceentry))) + (((dst_negative_code_ones_entry_sourceentry) + (dst_negative_scale_ones_entry_sourceentry)) * S ((dst_negative_code_ones_entry_sourceentry) + (dst_negative_scale_ones_entry_sourceentry)) + ((dst_negative_scale_ones_entry_sourceentry) + (dst_negative_scale_ones_entry_sourceentry)))))) /\ (((((exists ff_h_pvs_ones_entry_sourceentrypositive. ff_h_pvs_ones_entry_sourceentrypositive + S (dst_positive_ones_entry_sourceentry) = S ((S (du_index_ones_entry_source)) * dst_positive_scale_ones_entry_sourceentry)) /\ exists ff_q_pvs_ones_entry_sourceentrypositive. dst_positive_code_ones_entry_sourceentry = ff_q_pvs_ones_entry_sourceentrypositive * S ((S (du_index_ones_entry_source)) * dst_positive_scale_ones_entry_sourceentry) + (dst_positive_ones_entry_sourceentry))) /\ (((((exists ff_h_pvs_ones_entry_sourceentrynegative. ff_h_pvs_ones_entry_sourceentrynegative + S (dst_negative_ones_entry_sourceentry) = S ((S (du_index_ones_entry_source)) * dst_negative_scale_ones_entry_sourceentry)) /\ exists ff_q_pvs_ones_entry_sourceentrynegative. dst_negative_code_ones_entry_sourceentry = ff_q_pvs_ones_entry_sourceentrynegative * S ((S (du_index_ones_entry_source)) * dst_negative_scale_ones_entry_sourceentry) + (dst_negative_ones_entry_sourceentry))) /\ (exists ge_balance_positive_ones_entry_sourceentryvalue ge_balance_negative_ones_entry_sourceentryvalue. (((((du_value_ones_entry_source) = 2 * (ge_balance_positive_ones_entry_sourceentryvalue) /\ (ge_balance_negative_ones_entry_sourceentryvalue) = 0) \/ exists ge_signed_half_ones_entry_sourceentryvaluedecode. (((du_value_ones_entry_source) = 2 * ge_signed_half_ones_entry_sourceentryvaluedecode + 1 /\ (ge_balance_positive_ones_entry_sourceentryvalue) = 0) /\ (ge_balance_negative_ones_entry_sourceentryvalue) = S ge_signed_half_ones_entry_sourceentryvaluedecode))) /\ ((dst_positive_ones_entry_sourceentry) + ge_balance_negative_ones_entry_sourceentryvalue = (dst_negative_ones_entry_sourceentry) + ge_balance_positive_ones_entry_sourceentryvalue))))))))) -> du_value_ones_entry_source=2))) -> ~(n=0) -> (exists pvs_le_gap_ones_entry_bound. pvs_le_gap_ones_entry_bound + (n) = (N)) -> ((((~((d)=0)) /\ (exists dc_quotient_ones_entry_convolution dc_left_ones_entry_convolution dc_right_ones_entry_convolution. (((n)=(d)*dc_quotient_ones_entry_convolution) /\ (((exists dst_positive_code_ones_entry_convolutionleft dst_positive_scale_ones_entry_convolutionleft dst_negative_code_ones_entry_convolutionleft dst_negative_scale_ones_entry_convolutionleft dst_positive_ones_entry_convolutionleft dst_negative_ones_entry_convolutionleft. (((F) = (((((dst_positive_code_ones_entry_convolutionleft) + (dst_positive_scale_ones_entry_convolutionleft)) * S ((dst_positive_code_ones_entry_convolutionleft) + (dst_positive_scale_ones_entry_convolutionleft)) + ((dst_positive_scale_ones_entry_convolutionleft) + (dst_positive_scale_ones_entry_convolutionleft))) + (((dst_negative_code_ones_entry_convolutionleft) + (dst_negative_scale_ones_entry_convolutionleft)) * S ((dst_negative_code_ones_entry_convolutionleft) + (dst_negative_scale_ones_entry_convolutionleft)) + ((dst_negative_scale_ones_entry_convolutionleft) + (dst_negative_scale_ones_entry_convolutionleft)))) * S ((((dst_positive_code_ones_entry_convolutionleft) + (dst_positive_scale_ones_entry_convolutionleft)) * S ((dst_positive_code_ones_entry_convolutionleft) + (dst_positive_scale_ones_entry_convolutionleft)) + ((dst_positive_scale_ones_entry_convolutionleft) + (dst_positive_scale_ones_entry_convolutionleft))) + (((dst_negative_code_ones_entry_convolutionleft) + (dst_negative_scale_ones_entry_convolutionleft)) * S ((dst_negative_code_ones_entry_convolutionleft) + (dst_negative_scale_ones_entry_convolutionleft)) + ((dst_negative_scale_ones_entry_convolutionleft) + (dst_negative_scale_ones_entry_convolutionleft)))) + ((((dst_negative_code_ones_entry_convolutionleft) + (dst_negative_scale_ones_entry_convolutionleft)) * S ((dst_negative_code_ones_entry_convolutionleft) + (dst_negative_scale_ones_entry_convolutionleft)) + ((dst_negative_scale_ones_entry_convolutionleft) + (dst_negative_scale_ones_entry_convolutionleft))) + (((dst_negative_code_ones_entry_convolutionleft) + (dst_negative_scale_ones_entry_convolutionleft)) * S ((dst_negative_code_ones_entry_convolutionleft) + (dst_negative_scale_ones_entry_convolutionleft)) + ((dst_negative_scale_ones_entry_convolutionleft) + (dst_negative_scale_ones_entry_convolutionleft)))))) /\ (((((exists ff_h_pvs_ones_entry_convolutionleftpositive. ff_h_pvs_ones_entry_convolutionleftpositive + S (dst_positive_ones_entry_convolutionleft) = S ((S (d)) * dst_positive_scale_ones_entry_convolutionleft)) /\ exists ff_q_pvs_ones_entry_convolutionleftpositive. dst_positive_code_ones_entry_convolutionleft = ff_q_pvs_ones_entry_convolutionleftpositive * S ((S (d)) * dst_positive_scale_ones_entry_convolutionleft) + (dst_positive_ones_entry_convolutionleft))) /\ (((((exists ff_h_pvs_ones_entry_convolutionleftnegative. ff_h_pvs_ones_entry_convolutionleftnegative + S (dst_negative_ones_entry_convolutionleft) = S ((S (d)) * dst_negative_scale_ones_entry_convolutionleft)) /\ exists ff_q_pvs_ones_entry_convolutionleftnegative. dst_negative_code_ones_entry_convolutionleft = ff_q_pvs_ones_entry_convolutionleftnegative * S ((S (d)) * dst_negative_scale_ones_entry_convolutionleft) + (dst_negative_ones_entry_convolutionleft))) /\ (exists ge_balance_positive_ones_entry_convolutionleftvalue ge_balance_negative_ones_entry_convolutionleftvalue. (((((dc_left_ones_entry_convolution) = 2 * (ge_balance_positive_ones_entry_convolutionleftvalue) /\ (ge_balance_negative_ones_entry_convolutionleftvalue) = 0) \/ exists ge_signed_half_ones_entry_convolutionleftvaluedecode. (((dc_left_ones_entry_convolution) = 2 * ge_signed_half_ones_entry_convolutionleftvaluedecode + 1 /\ (ge_balance_positive_ones_entry_convolutionleftvalue) = 0) /\ (ge_balance_negative_ones_entry_convolutionleftvalue) = S ge_signed_half_ones_entry_convolutionleftvaluedecode))) /\ ((dst_positive_ones_entry_convolutionleft) + ge_balance_negative_ones_entry_convolutionleftvalue = (dst_negative_ones_entry_convolutionleft) + ge_balance_positive_ones_entry_convolutionleftvalue))))))))) /\ (((exists dst_positive_code_ones_entry_convolutionright dst_positive_scale_ones_entry_convolutionright dst_negative_code_ones_entry_convolutionright dst_negative_scale_ones_entry_convolutionright dst_positive_ones_entry_convolutionright dst_negative_ones_entry_convolutionright. (((U) = (((((dst_positive_code_ones_entry_convolutionright) + (dst_positive_scale_ones_entry_convolutionright)) * S ((dst_positive_code_ones_entry_convolutionright) + (dst_positive_scale_ones_entry_convolutionright)) + ((dst_positive_scale_ones_entry_convolutionright) + (dst_positive_scale_ones_entry_convolutionright))) + (((dst_negative_code_ones_entry_convolutionright) + (dst_negative_scale_ones_entry_convolutionright)) * S ((dst_negative_code_ones_entry_convolutionright) + (dst_negative_scale_ones_entry_convolutionright)) + ((dst_negative_scale_ones_entry_convolutionright) + (dst_negative_scale_ones_entry_convolutionright)))) * S ((((dst_positive_code_ones_entry_convolutionright) + (dst_positive_scale_ones_entry_convolutionright)) * S ((dst_positive_code_ones_entry_convolutionright) + (dst_positive_scale_ones_entry_convolutionright)) + ((dst_positive_scale_ones_entry_convolutionright) + (dst_positive_scale_ones_entry_convolutionright))) + (((dst_negative_code_ones_entry_convolutionright) + (dst_negative_scale_ones_entry_convolutionright)) * S ((dst_negative_code_ones_entry_convolutionright) + (dst_negative_scale_ones_entry_convolutionright)) + ((dst_negative_scale_ones_entry_convolutionright) + (dst_negative_scale_ones_entry_convolutionright)))) + ((((dst_negative_code_ones_entry_convolutionright) + (dst_negative_scale_ones_entry_convolutionright)) * S ((dst_negative_code_ones_entry_convolutionright) + (dst_negative_scale_ones_entry_convolutionright)) + ((dst_negative_scale_ones_entry_convolutionright) + (dst_negative_scale_ones_entry_convolutionright))) + (((dst_negative_code_ones_entry_convolutionright) + (dst_negative_scale_ones_entry_convolutionright)) * S ((dst_negative_code_ones_entry_convolutionright) + (dst_negative_scale_ones_entry_convolutionright)) + ((dst_negative_scale_ones_entry_convolutionright) + (dst_negative_scale_ones_entry_convolutionright)))))) /\ (((((exists ff_h_pvs_ones_entry_convolutionrightpositive. ff_h_pvs_ones_entry_convolutionrightpositive + S (dst_positive_ones_entry_convolutionright) = S ((S (dc_quotient_ones_entry_convolution)) * dst_positive_scale_ones_entry_convolutionright)) /\ exists ff_q_pvs_ones_entry_convolutionrightpositive. dst_positive_code_ones_entry_convolutionright = ff_q_pvs_ones_entry_convolutionrightpositive * S ((S (dc_quotient_ones_entry_convolution)) * dst_positive_scale_ones_entry_convolutionright) + (dst_positive_ones_entry_convolutionright))) /\ (((((exists ff_h_pvs_ones_entry_convolutionrightnegative. ff_h_pvs_ones_entry_convolutionrightnegative + S (dst_negative_ones_entry_convolutionright) = S ((S (dc_quotient_ones_entry_convolution)) * dst_negative_scale_ones_entry_convolutionright)) /\ exists ff_q_pvs_ones_entry_convolutionrightnegative. dst_negative_code_ones_entry_convolutionright = ff_q_pvs_ones_entry_convolutionrightnegative * S ((S (dc_quotient_ones_entry_convolution)) * dst_negative_scale_ones_entry_convolutionright) + (dst_negative_ones_entry_convolutionright))) /\ (exists ge_balance_positive_ones_entry_convolutionrightvalue ge_balance_negative_ones_entry_convolutionrightvalue. (((((dc_right_ones_entry_convolution) = 2 * (ge_balance_positive_ones_entry_convolutionrightvalue) /\ (ge_balance_negative_ones_entry_convolutionrightvalue) = 0) \/ exists ge_signed_half_ones_entry_convolutionrightvaluedecode. (((dc_right_ones_entry_convolution) = 2 * ge_signed_half_ones_entry_convolutionrightvaluedecode + 1 /\ (ge_balance_positive_ones_entry_convolutionrightvalue) = 0) /\ (ge_balance_negative_ones_entry_convolutionrightvalue) = S ge_signed_half_ones_entry_convolutionrightvaluedecode))) /\ ((dst_positive_ones_entry_convolutionright) + ge_balance_negative_ones_entry_convolutionrightvalue = (dst_negative_ones_entry_convolutionright) + ge_balance_positive_ones_entry_convolutionrightvalue))))))))) /\ (exists sto_ap_ones_entry_convolutionproduct sto_an_ones_entry_convolutionproduct sto_bp_ones_entry_convolutionproduct sto_bn_ones_entry_convolutionproduct sto_cp_ones_entry_convolutionproduct sto_cn_ones_entry_convolutionproduct. (((((dc_left_ones_entry_convolution) = 2 * (sto_ap_ones_entry_convolutionproduct) /\ (sto_an_ones_entry_convolutionproduct) = 0) \/ exists ge_signed_half_ones_entry_convolutionproductleft. (((dc_left_ones_entry_convolution) = 2 * ge_signed_half_ones_entry_convolutionproductleft + 1 /\ (sto_ap_ones_entry_convolutionproduct) = 0) /\ (sto_an_ones_entry_convolutionproduct) = S ge_signed_half_ones_entry_convolutionproductleft))) /\ ((((((dc_right_ones_entry_convolution) = 2 * (sto_bp_ones_entry_convolutionproduct) /\ (sto_bn_ones_entry_convolutionproduct) = 0) \/ exists ge_signed_half_ones_entry_convolutionproductright. (((dc_right_ones_entry_convolution) = 2 * ge_signed_half_ones_entry_convolutionproductright + 1 /\ (sto_bp_ones_entry_convolutionproduct) = 0) /\ (sto_bn_ones_entry_convolutionproduct) = S ge_signed_half_ones_entry_convolutionproductright))) /\ ((((((z) = 2 * (sto_cp_ones_entry_convolutionproduct) /\ (sto_cn_ones_entry_convolutionproduct) = 0) \/ exists ge_signed_half_ones_entry_convolutionproductoutput. (((z) = 2 * ge_signed_half_ones_entry_convolutionproductoutput + 1 /\ (sto_cp_ones_entry_convolutionproduct) = 0) /\ (sto_cn_ones_entry_convolutionproduct) = S ge_signed_half_ones_entry_convolutionproductoutput))) /\ ((sto_ap_ones_entry_convolutionproduct * sto_bp_ones_entry_convolutionproduct + sto_an_ones_entry_convolutionproduct * sto_bn_ones_entry_convolutionproduct) + sto_cn_ones_entry_convolutionproduct = (sto_ap_ones_entry_convolutionproduct * sto_bn_ones_entry_convolutionproduct + sto_an_ones_entry_convolutionproduct * sto_bp_ones_entry_convolutionproduct) + sto_cp_ones_entry_convolutionproduct))))))))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_ones_entry_convolutionnondivisor. (n) = (d) * pvs_factor_ones_entry_convolutionnondivisor)) /\ ((z)=0)))) -> ((((~((d)=0)) /\ (exists dm_quotient_ones_entry_mask. (((n)=(d)*dm_quotient_ones_entry_mask) /\ (exists dst_positive_code_ones_entry_maskinput dst_positive_scale_ones_entry_maskinput dst_negative_code_ones_entry_maskinput dst_negative_scale_ones_entry_maskinput dst_positive_ones_entry_maskinput dst_negative_ones_entry_maskinput. (((F) = (((((dst_positive_code_ones_entry_maskinput) + (dst_positive_scale_ones_entry_maskinput)) * S ((dst_positive_code_ones_entry_maskinput) + (dst_positive_scale_ones_entry_maskinput)) + ((dst_positive_scale_ones_entry_maskinput) + (dst_positive_scale_ones_entry_maskinput))) + (((dst_negative_code_ones_entry_maskinput) + (dst_negative_scale_ones_entry_maskinput)) * S ((dst_negative_code_ones_entry_maskinput) + (dst_negative_scale_ones_entry_maskinput)) + ((dst_negative_scale_ones_entry_maskinput) + (dst_negative_scale_ones_entry_maskinput)))) * S ((((dst_positive_code_ones_entry_maskinput) + (dst_positive_scale_ones_entry_maskinput)) * S ((dst_positive_code_ones_entry_maskinput) + (dst_positive_scale_ones_entry_maskinput)) + ((dst_positive_scale_ones_entry_maskinput) + (dst_positive_scale_ones_entry_maskinput))) + (((dst_negative_code_ones_entry_maskinput) + (dst_negative_scale_ones_entry_maskinput)) * S ((dst_negative_code_ones_entry_maskinput) + (dst_negative_scale_ones_entry_maskinput)) + ((dst_negative_scale_ones_entry_maskinput) + (dst_negative_scale_ones_entry_maskinput)))) + ((((dst_negative_code_ones_entry_maskinput) + (dst_negative_scale_ones_entry_maskinput)) * S ((dst_negative_code_ones_entry_maskinput) + (dst_negative_scale_ones_entry_maskinput)) + ((dst_negative_scale_ones_entry_maskinput) + (dst_negative_scale_ones_entry_maskinput))) + (((dst_negative_code_ones_entry_maskinput) + (dst_negative_scale_ones_entry_maskinput)) * S ((dst_negative_code_ones_entry_maskinput) + (dst_negative_scale_ones_entry_maskinput)) + ((dst_negative_scale_ones_entry_maskinput) + (dst_negative_scale_ones_entry_maskinput)))))) /\ (((((exists ff_h_pvs_ones_entry_maskinputpositive. ff_h_pvs_ones_entry_maskinputpositive + S (dst_positive_ones_entry_maskinput) = S ((S (d)) * dst_positive_scale_ones_entry_maskinput)) /\ exists ff_q_pvs_ones_entry_maskinputpositive. dst_positive_code_ones_entry_maskinput = ff_q_pvs_ones_entry_maskinputpositive * S ((S (d)) * dst_positive_scale_ones_entry_maskinput) + (dst_positive_ones_entry_maskinput))) /\ (((((exists ff_h_pvs_ones_entry_maskinputnegative. ff_h_pvs_ones_entry_maskinputnegative + S (dst_negative_ones_entry_maskinput) = S ((S (d)) * dst_negative_scale_ones_entry_maskinput)) /\ exists ff_q_pvs_ones_entry_maskinputnegative. dst_negative_code_ones_entry_maskinput = ff_q_pvs_ones_entry_maskinputnegative * S ((S (d)) * dst_negative_scale_ones_entry_maskinput) + (dst_negative_ones_entry_maskinput))) /\ (exists ge_balance_positive_ones_entry_maskinputvalue ge_balance_negative_ones_entry_maskinputvalue. (((((z) = 2 * (ge_balance_positive_ones_entry_maskinputvalue) /\ (ge_balance_negative_ones_entry_maskinputvalue) = 0) \/ exists ge_signed_half_ones_entry_maskinputvaluedecode. (((z) = 2 * ge_signed_half_ones_entry_maskinputvaluedecode + 1 /\ (ge_balance_positive_ones_entry_maskinputvalue) = 0) /\ (ge_balance_negative_ones_entry_maskinputvalue) = S ge_signed_half_ones_entry_maskinputvaluedecode))) /\ ((dst_positive_ones_entry_maskinput) + ge_balance_negative_ones_entry_maskinputvalue = (dst_negative_ones_entry_maskinput) + ge_balance_positive_ones_entry_maskinputvalue))))))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_ones_entry_masknondivisor. (n) = (d) * pvs_factor_ones_entry_masknondivisor)) /\ ((z)=0))))

Complete tactic proof in conservative notation

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

74 script commands · 19 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–18

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
  5. L15
    cases he_left_right_witness_witness
  6. L16
    cases he_left_right_witness_witness_witness
  7. L17
    cases he_left_right_witness_witness_witness_right
  8. L18
    cases he_left_right_witness_witness_witness_right_right
03Establish hqpositiveL19–27

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

  1. L19
    have hqpositive : ~(x=0)
  2. L20
    intro hqzero
  3. L21
    specialize factor_nonzero_right (n)
  4. L22
    specialize factor_nonzero_right (d)
  5. L23
    specialize factor_nonzero_right (x)
  6. L24
    apply factor_nonzero_right
  7. L25
    exact hn
  8. L26
    exact he_left_right_witness_witness_witness_left
  9. L27
    exact hqzero
04Establish hqboundL28–36

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

  1. L28
    have hqbound : Le(x,N)Definitions: Le(x,N)Original native command in the exact edition
  2. L29
    specialize le_trans (x)
  3. L30
    specialize le_trans (n)
  4. L31
    specialize le_trans (N)
  5. L32
    apply le_trans
  6. L33
    specialize divisor_le_nonzero (x)
  7. L34
    specialize divisor_le_nonzero (n)
  8. L35
    apply divisor_le_nonzero
  9. L36
    exact hn
05Construct an explicit witnessL37–37

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

  1. L37
    exists d
06Calculate and transport equalitiesL38–38

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

  1. L38
    trans (d)*(x)
07Use earlier factsL39–41

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

  1. L39
    exact he_left_right_witness_witness_witness_left
  2. L40
    apply mul_comm
  3. L41
    exact hb
08Establish hvL42–51

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

  1. L42
    have hv : x2=2
  2. L43
    specialize dirichlet_constant_one_table_value (N)
  3. L44
    specialize dirichlet_constant_one_table_value (U)
  4. L45
    specialize dirichlet_constant_one_table_value (x)
  5. L46
    specialize dirichlet_constant_one_table_value (x2)
  6. L47
    apply dirichlet_constant_one_table_value
  7. L48
    exact hu
  8. L49
    exact hqpositive
  9. L50
    exact hqbound
  10. L51
    exact he_left_right_witness_witness_witness_right_right_left
09Calculate and transport equalitiesL52–53

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

  1. L52
    rewrite hv at he_left_right_witness_witness_witness_right_right_right
  2. L53
    rewrite hv at he_left_right_witness_witness_witness_right_right_right
10Establish heqL54–62

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

  1. L54
    have heq : z=x1
  2. L55
    specialize signed_mul_functional (x1)
  3. L56
    specialize signed_mul_functional (2)
  4. L57
    specialize signed_mul_functional (z)
  5. L58
    specialize signed_mul_functional (x1)
  6. L59
    apply signed_mul_functional
  7. L60
    exact he_left_right_witness_witness_witness_right_right_right
  8. L61
    specialize signed_mul_one_right (x1)
  9. L62
    apply signed_mul_one_right
11Separate the logical casesL63–64

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

  1. L63
    left
  2. L64
    split
12Use earlier factsL65–65

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

  1. L65
    exact he_left_left
13Construct an explicit witnessL66–66

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

  1. L66
    exists x
14Separate the logical casesL67–67

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

  1. L67
    split
15Use earlier factsL68–68

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

  1. L68
    exact he_left_right_witness_witness_witness_left
16Calculate and transport equalitiesL69–70

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

  1. L69
    rewrite heq
  2. L70
    rewrite heq
17Use earlier factsL71–71

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

  1. L71
    exact he_left_right_witness_witness_witness_right_left
18Separate the logical casesL72–73

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

  1. L72
    cases he_right
  2. L73
    right
19Use earlier factsL74–74

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

  1. L74
    exact he_right

Library-wide reading audit

Original defined command ledger · 74 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. 0015cases he_left_right_witness_witness
  16. 0016cases he_left_right_witness_witness_witness
  17. 0017cases he_left_right_witness_witness_witness_right
  18. 0018cases he_left_right_witness_witness_witness_right_right
  19. 0019have hqpositive : ~(x=0)
  20. 0020intro hqzero
  21. 0021specialize factor_nonzero_right (n)
  22. 0022specialize factor_nonzero_right (d)
  23. 0023specialize factor_nonzero_right (x)
  24. 0024apply factor_nonzero_right
  25. 0025exact hn
  26. 0026exact he_left_right_witness_witness_witness_left
  27. 0027exact hqzero
  28. 0028have hqbound : Le(x,N)
  29. 0029specialize le_trans (x)
  30. 0030specialize le_trans (n)
  31. 0031specialize le_trans (N)
  32. 0032apply le_trans
  33. 0033specialize divisor_le_nonzero (x)
  34. 0034specialize divisor_le_nonzero (n)
  35. 0035apply divisor_le_nonzero
  36. 0036exact hn
  37. 0037exists d
  38. 0038trans (d)*(x)
  39. 0039exact he_left_right_witness_witness_witness_left
  40. 0040apply mul_comm
  41. 0041exact hb
  42. 0042have hv : x2=2
  43. 0043specialize dirichlet_constant_one_table_value (N)
  44. 0044specialize dirichlet_constant_one_table_value (U)
  45. 0045specialize dirichlet_constant_one_table_value (x)
  46. 0046specialize dirichlet_constant_one_table_value (x2)
  47. 0047apply dirichlet_constant_one_table_value
  48. 0048exact hu
  49. 0049exact hqpositive
  50. 0050exact hqbound
  51. 0051exact he_left_right_witness_witness_witness_right_right_left
  52. 0052rewrite hv at he_left_right_witness_witness_witness_right_right_right
  53. 0053rewrite hv at he_left_right_witness_witness_witness_right_right_right
  54. 0054have heq : z=x1
  55. 0055specialize signed_mul_functional (x1)
  56. 0056specialize signed_mul_functional (2)
  57. 0057specialize signed_mul_functional (z)
  58. 0058specialize signed_mul_functional (x1)
  59. 0059apply signed_mul_functional
  60. 0060exact he_left_right_witness_witness_witness_right_right_right
  61. 0061specialize signed_mul_one_right (x1)
  62. 0062apply signed_mul_one_right
  63. 0063left
  64. 0064split
  65. 0065exact he_left_left
  66. 0066exists x
  67. 0067split
  68. 0068exact he_left_right_witness_witness_witness_left
  69. 0069rewrite heq
  70. 0070rewrite heq
  71. 0071exact he_left_right_witness_witness_witness_right_left
  72. 0072cases he_right
  73. 0073right
  74. 0074exact he_right