DF0006

dirichlet_grid_entry_exists

Constructively decide the factor guards, extract the actual middle factor, and construct three signed lookups and both products.

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.

Every grid, slice, row sum and intermediate table is constructed. Retained cells have witnessed n=(a*e)*c and value F(a)*(H(e)*G(c)). The flat endpoint is unused. Table associativity includes N=0 and compares only positive values, not encodings. Full G009 remains broader.

Exact theorem in conservative defined notation

∀ F. ∀ G. ∀ H. ∀ n. ∀ a. ∀ e. ArithTable(0,F) → ArithTable(0,G) → ArithTable(0,H) → ∃ x. DirichletGridEntry(F,G,H,n,a,e,x)

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

Definition DAG

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

Actual proof prerequisites

eq_decidable · checked external prerequisitedirichlet_grid_entry_omittedmultiple_decidable_nonzero · checked external prerequisitemul_ne_zero · checked external prerequisitesigned_table_lookup_any · checked external prerequisitesigned_mul_total · checked external prerequisitedirichlet_grid_entry_from_factorization
Original expanded first-order statement 
forall F G H n a e. (exists dst_positive_code_choice_F dst_positive_scale_choice_F dst_negative_code_choice_F dst_negative_scale_choice_F. (((F) = (((((dst_positive_code_choice_F) + (dst_positive_scale_choice_F)) * S ((dst_positive_code_choice_F) + (dst_positive_scale_choice_F)) + ((dst_positive_scale_choice_F) + (dst_positive_scale_choice_F))) + (((dst_negative_code_choice_F) + (dst_negative_scale_choice_F)) * S ((dst_negative_code_choice_F) + (dst_negative_scale_choice_F)) + ((dst_negative_scale_choice_F) + (dst_negative_scale_choice_F)))) * S ((((dst_positive_code_choice_F) + (dst_positive_scale_choice_F)) * S ((dst_positive_code_choice_F) + (dst_positive_scale_choice_F)) + ((dst_positive_scale_choice_F) + (dst_positive_scale_choice_F))) + (((dst_negative_code_choice_F) + (dst_negative_scale_choice_F)) * S ((dst_negative_code_choice_F) + (dst_negative_scale_choice_F)) + ((dst_negative_scale_choice_F) + (dst_negative_scale_choice_F)))) + ((((dst_negative_code_choice_F) + (dst_negative_scale_choice_F)) * S ((dst_negative_code_choice_F) + (dst_negative_scale_choice_F)) + ((dst_negative_scale_choice_F) + (dst_negative_scale_choice_F))) + (((dst_negative_code_choice_F) + (dst_negative_scale_choice_F)) * S ((dst_negative_code_choice_F) + (dst_negative_scale_choice_F)) + ((dst_negative_scale_choice_F) + (dst_negative_scale_choice_F)))))) /\ (forall dst_index_choice_F. (exists pvs_le_gap_choice_Fdomain. pvs_le_gap_choice_Fdomain + (dst_index_choice_F) = (0)) -> exists dst_positive_choice_F dst_negative_choice_F dst_value_choice_F. ((((exists ff_h_pvs_choice_Fentrypositive. ff_h_pvs_choice_Fentrypositive + S (dst_positive_choice_F) = S ((S (dst_index_choice_F)) * dst_positive_scale_choice_F)) /\ exists ff_q_pvs_choice_Fentrypositive. dst_positive_code_choice_F = ff_q_pvs_choice_Fentrypositive * S ((S (dst_index_choice_F)) * dst_positive_scale_choice_F) + (dst_positive_choice_F))) /\ (((((exists ff_h_pvs_choice_Fentrynegative. ff_h_pvs_choice_Fentrynegative + S (dst_negative_choice_F) = S ((S (dst_index_choice_F)) * dst_negative_scale_choice_F)) /\ exists ff_q_pvs_choice_Fentrynegative. dst_negative_code_choice_F = ff_q_pvs_choice_Fentrynegative * S ((S (dst_index_choice_F)) * dst_negative_scale_choice_F) + (dst_negative_choice_F))) /\ (exists ge_balance_positive_choice_Fentryvalue ge_balance_negative_choice_Fentryvalue. (((((dst_value_choice_F) = 2 * (ge_balance_positive_choice_Fentryvalue) /\ (ge_balance_negative_choice_Fentryvalue) = 0) \/ exists ge_signed_half_choice_Fentryvaluedecode. (((dst_value_choice_F) = 2 * ge_signed_half_choice_Fentryvaluedecode + 1 /\ (ge_balance_positive_choice_Fentryvalue) = 0) /\ (ge_balance_negative_choice_Fentryvalue) = S ge_signed_half_choice_Fentryvaluedecode))) /\ ((dst_positive_choice_F) + ge_balance_negative_choice_Fentryvalue = (dst_negative_choice_F) + ge_balance_positive_choice_Fentryvalue))))))))) -> (exists dst_positive_code_choice_G dst_positive_scale_choice_G dst_negative_code_choice_G dst_negative_scale_choice_G. (((G) = (((((dst_positive_code_choice_G) + (dst_positive_scale_choice_G)) * S ((dst_positive_code_choice_G) + (dst_positive_scale_choice_G)) + ((dst_positive_scale_choice_G) + (dst_positive_scale_choice_G))) + (((dst_negative_code_choice_G) + (dst_negative_scale_choice_G)) * S ((dst_negative_code_choice_G) + (dst_negative_scale_choice_G)) + ((dst_negative_scale_choice_G) + (dst_negative_scale_choice_G)))) * S ((((dst_positive_code_choice_G) + (dst_positive_scale_choice_G)) * S ((dst_positive_code_choice_G) + (dst_positive_scale_choice_G)) + ((dst_positive_scale_choice_G) + (dst_positive_scale_choice_G))) + (((dst_negative_code_choice_G) + (dst_negative_scale_choice_G)) * S ((dst_negative_code_choice_G) + (dst_negative_scale_choice_G)) + ((dst_negative_scale_choice_G) + (dst_negative_scale_choice_G)))) + ((((dst_negative_code_choice_G) + (dst_negative_scale_choice_G)) * S ((dst_negative_code_choice_G) + (dst_negative_scale_choice_G)) + ((dst_negative_scale_choice_G) + (dst_negative_scale_choice_G))) + (((dst_negative_code_choice_G) + (dst_negative_scale_choice_G)) * S ((dst_negative_code_choice_G) + (dst_negative_scale_choice_G)) + ((dst_negative_scale_choice_G) + (dst_negative_scale_choice_G)))))) /\ (forall dst_index_choice_G. (exists pvs_le_gap_choice_Gdomain. pvs_le_gap_choice_Gdomain + (dst_index_choice_G) = (0)) -> exists dst_positive_choice_G dst_negative_choice_G dst_value_choice_G. ((((exists ff_h_pvs_choice_Gentrypositive. ff_h_pvs_choice_Gentrypositive + S (dst_positive_choice_G) = S ((S (dst_index_choice_G)) * dst_positive_scale_choice_G)) /\ exists ff_q_pvs_choice_Gentrypositive. dst_positive_code_choice_G = ff_q_pvs_choice_Gentrypositive * S ((S (dst_index_choice_G)) * dst_positive_scale_choice_G) + (dst_positive_choice_G))) /\ (((((exists ff_h_pvs_choice_Gentrynegative. ff_h_pvs_choice_Gentrynegative + S (dst_negative_choice_G) = S ((S (dst_index_choice_G)) * dst_negative_scale_choice_G)) /\ exists ff_q_pvs_choice_Gentrynegative. dst_negative_code_choice_G = ff_q_pvs_choice_Gentrynegative * S ((S (dst_index_choice_G)) * dst_negative_scale_choice_G) + (dst_negative_choice_G))) /\ (exists ge_balance_positive_choice_Gentryvalue ge_balance_negative_choice_Gentryvalue. (((((dst_value_choice_G) = 2 * (ge_balance_positive_choice_Gentryvalue) /\ (ge_balance_negative_choice_Gentryvalue) = 0) \/ exists ge_signed_half_choice_Gentryvaluedecode. (((dst_value_choice_G) = 2 * ge_signed_half_choice_Gentryvaluedecode + 1 /\ (ge_balance_positive_choice_Gentryvalue) = 0) /\ (ge_balance_negative_choice_Gentryvalue) = S ge_signed_half_choice_Gentryvaluedecode))) /\ ((dst_positive_choice_G) + ge_balance_negative_choice_Gentryvalue = (dst_negative_choice_G) + ge_balance_positive_choice_Gentryvalue))))))))) -> (exists dst_positive_code_choice_H dst_positive_scale_choice_H dst_negative_code_choice_H dst_negative_scale_choice_H. (((H) = (((((dst_positive_code_choice_H) + (dst_positive_scale_choice_H)) * S ((dst_positive_code_choice_H) + (dst_positive_scale_choice_H)) + ((dst_positive_scale_choice_H) + (dst_positive_scale_choice_H))) + (((dst_negative_code_choice_H) + (dst_negative_scale_choice_H)) * S ((dst_negative_code_choice_H) + (dst_negative_scale_choice_H)) + ((dst_negative_scale_choice_H) + (dst_negative_scale_choice_H)))) * S ((((dst_positive_code_choice_H) + (dst_positive_scale_choice_H)) * S ((dst_positive_code_choice_H) + (dst_positive_scale_choice_H)) + ((dst_positive_scale_choice_H) + (dst_positive_scale_choice_H))) + (((dst_negative_code_choice_H) + (dst_negative_scale_choice_H)) * S ((dst_negative_code_choice_H) + (dst_negative_scale_choice_H)) + ((dst_negative_scale_choice_H) + (dst_negative_scale_choice_H)))) + ((((dst_negative_code_choice_H) + (dst_negative_scale_choice_H)) * S ((dst_negative_code_choice_H) + (dst_negative_scale_choice_H)) + ((dst_negative_scale_choice_H) + (dst_negative_scale_choice_H))) + (((dst_negative_code_choice_H) + (dst_negative_scale_choice_H)) * S ((dst_negative_code_choice_H) + (dst_negative_scale_choice_H)) + ((dst_negative_scale_choice_H) + (dst_negative_scale_choice_H)))))) /\ (forall dst_index_choice_H. (exists pvs_le_gap_choice_Hdomain. pvs_le_gap_choice_Hdomain + (dst_index_choice_H) = (0)) -> exists dst_positive_choice_H dst_negative_choice_H dst_value_choice_H. ((((exists ff_h_pvs_choice_Hentrypositive. ff_h_pvs_choice_Hentrypositive + S (dst_positive_choice_H) = S ((S (dst_index_choice_H)) * dst_positive_scale_choice_H)) /\ exists ff_q_pvs_choice_Hentrypositive. dst_positive_code_choice_H = ff_q_pvs_choice_Hentrypositive * S ((S (dst_index_choice_H)) * dst_positive_scale_choice_H) + (dst_positive_choice_H))) /\ (((((exists ff_h_pvs_choice_Hentrynegative. ff_h_pvs_choice_Hentrynegative + S (dst_negative_choice_H) = S ((S (dst_index_choice_H)) * dst_negative_scale_choice_H)) /\ exists ff_q_pvs_choice_Hentrynegative. dst_negative_code_choice_H = ff_q_pvs_choice_Hentrynegative * S ((S (dst_index_choice_H)) * dst_negative_scale_choice_H) + (dst_negative_choice_H))) /\ (exists ge_balance_positive_choice_Hentryvalue ge_balance_negative_choice_Hentryvalue. (((((dst_value_choice_H) = 2 * (ge_balance_positive_choice_Hentryvalue) /\ (ge_balance_negative_choice_Hentryvalue) = 0) \/ exists ge_signed_half_choice_Hentryvaluedecode. (((dst_value_choice_H) = 2 * ge_signed_half_choice_Hentryvaluedecode + 1 /\ (ge_balance_positive_choice_Hentryvalue) = 0) /\ (ge_balance_negative_choice_Hentryvalue) = S ge_signed_half_choice_Hentryvaluedecode))) /\ ((dst_positive_choice_H) + ge_balance_negative_choice_Hentryvalue = (dst_negative_choice_H) + ge_balance_positive_choice_Hentryvalue))))))))) -> exists z. ((((~((a)=0)) /\ (((~((e)=0)) /\ (exists dfg_middle_choice_result dfg_first_choice_result dfg_last_choice_result dfg_value_choice_result. (((n)=((a)*(e))*dfg_middle_choice_result) /\ (((exists dst_positive_code_choice_resultfirst dst_positive_scale_choice_resultfirst dst_negative_code_choice_resultfirst dst_negative_scale_choice_resultfirst dst_positive_choice_resultfirst dst_negative_choice_resultfirst. (((F) = (((((dst_positive_code_choice_resultfirst) + (dst_positive_scale_choice_resultfirst)) * S ((dst_positive_code_choice_resultfirst) + (dst_positive_scale_choice_resultfirst)) + ((dst_positive_scale_choice_resultfirst) + (dst_positive_scale_choice_resultfirst))) + (((dst_negative_code_choice_resultfirst) + (dst_negative_scale_choice_resultfirst)) * S ((dst_negative_code_choice_resultfirst) + (dst_negative_scale_choice_resultfirst)) + ((dst_negative_scale_choice_resultfirst) + (dst_negative_scale_choice_resultfirst)))) * S ((((dst_positive_code_choice_resultfirst) + (dst_positive_scale_choice_resultfirst)) * S ((dst_positive_code_choice_resultfirst) + (dst_positive_scale_choice_resultfirst)) + ((dst_positive_scale_choice_resultfirst) + (dst_positive_scale_choice_resultfirst))) + (((dst_negative_code_choice_resultfirst) + (dst_negative_scale_choice_resultfirst)) * S ((dst_negative_code_choice_resultfirst) + (dst_negative_scale_choice_resultfirst)) + ((dst_negative_scale_choice_resultfirst) + (dst_negative_scale_choice_resultfirst)))) + ((((dst_negative_code_choice_resultfirst) + (dst_negative_scale_choice_resultfirst)) * S ((dst_negative_code_choice_resultfirst) + (dst_negative_scale_choice_resultfirst)) + ((dst_negative_scale_choice_resultfirst) + (dst_negative_scale_choice_resultfirst))) + (((dst_negative_code_choice_resultfirst) + (dst_negative_scale_choice_resultfirst)) * S ((dst_negative_code_choice_resultfirst) + (dst_negative_scale_choice_resultfirst)) + ((dst_negative_scale_choice_resultfirst) + (dst_negative_scale_choice_resultfirst)))))) /\ (((((exists ff_h_pvs_choice_resultfirstpositive. ff_h_pvs_choice_resultfirstpositive + S (dst_positive_choice_resultfirst) = S ((S (a)) * dst_positive_scale_choice_resultfirst)) /\ exists ff_q_pvs_choice_resultfirstpositive. dst_positive_code_choice_resultfirst = ff_q_pvs_choice_resultfirstpositive * S ((S (a)) * dst_positive_scale_choice_resultfirst) + (dst_positive_choice_resultfirst))) /\ (((((exists ff_h_pvs_choice_resultfirstnegative. ff_h_pvs_choice_resultfirstnegative + S (dst_negative_choice_resultfirst) = S ((S (a)) * dst_negative_scale_choice_resultfirst)) /\ exists ff_q_pvs_choice_resultfirstnegative. dst_negative_code_choice_resultfirst = ff_q_pvs_choice_resultfirstnegative * S ((S (a)) * dst_negative_scale_choice_resultfirst) + (dst_negative_choice_resultfirst))) /\ (exists ge_balance_positive_choice_resultfirstvalue ge_balance_negative_choice_resultfirstvalue. (((((dfg_first_choice_result) = 2 * (ge_balance_positive_choice_resultfirstvalue) /\ (ge_balance_negative_choice_resultfirstvalue) = 0) \/ exists ge_signed_half_choice_resultfirstvaluedecode. (((dfg_first_choice_result) = 2 * ge_signed_half_choice_resultfirstvaluedecode + 1 /\ (ge_balance_positive_choice_resultfirstvalue) = 0) /\ (ge_balance_negative_choice_resultfirstvalue) = S ge_signed_half_choice_resultfirstvaluedecode))) /\ ((dst_positive_choice_resultfirst) + ge_balance_negative_choice_resultfirstvalue = (dst_negative_choice_resultfirst) + ge_balance_positive_choice_resultfirstvalue))))))))) /\ (((exists dst_positive_code_choice_resultlast dst_positive_scale_choice_resultlast dst_negative_code_choice_resultlast dst_negative_scale_choice_resultlast dst_positive_choice_resultlast dst_negative_choice_resultlast. (((H) = (((((dst_positive_code_choice_resultlast) + (dst_positive_scale_choice_resultlast)) * S ((dst_positive_code_choice_resultlast) + (dst_positive_scale_choice_resultlast)) + ((dst_positive_scale_choice_resultlast) + (dst_positive_scale_choice_resultlast))) + (((dst_negative_code_choice_resultlast) + (dst_negative_scale_choice_resultlast)) * S ((dst_negative_code_choice_resultlast) + (dst_negative_scale_choice_resultlast)) + ((dst_negative_scale_choice_resultlast) + (dst_negative_scale_choice_resultlast)))) * S ((((dst_positive_code_choice_resultlast) + (dst_positive_scale_choice_resultlast)) * S ((dst_positive_code_choice_resultlast) + (dst_positive_scale_choice_resultlast)) + ((dst_positive_scale_choice_resultlast) + (dst_positive_scale_choice_resultlast))) + (((dst_negative_code_choice_resultlast) + (dst_negative_scale_choice_resultlast)) * S ((dst_negative_code_choice_resultlast) + (dst_negative_scale_choice_resultlast)) + ((dst_negative_scale_choice_resultlast) + (dst_negative_scale_choice_resultlast)))) + ((((dst_negative_code_choice_resultlast) + (dst_negative_scale_choice_resultlast)) * S ((dst_negative_code_choice_resultlast) + (dst_negative_scale_choice_resultlast)) + ((dst_negative_scale_choice_resultlast) + (dst_negative_scale_choice_resultlast))) + (((dst_negative_code_choice_resultlast) + (dst_negative_scale_choice_resultlast)) * S ((dst_negative_code_choice_resultlast) + (dst_negative_scale_choice_resultlast)) + ((dst_negative_scale_choice_resultlast) + (dst_negative_scale_choice_resultlast)))))) /\ (((((exists ff_h_pvs_choice_resultlastpositive. ff_h_pvs_choice_resultlastpositive + S (dst_positive_choice_resultlast) = S ((S (e)) * dst_positive_scale_choice_resultlast)) /\ exists ff_q_pvs_choice_resultlastpositive. dst_positive_code_choice_resultlast = ff_q_pvs_choice_resultlastpositive * S ((S (e)) * dst_positive_scale_choice_resultlast) + (dst_positive_choice_resultlast))) /\ (((((exists ff_h_pvs_choice_resultlastnegative. ff_h_pvs_choice_resultlastnegative + S (dst_negative_choice_resultlast) = S ((S (e)) * dst_negative_scale_choice_resultlast)) /\ exists ff_q_pvs_choice_resultlastnegative. dst_negative_code_choice_resultlast = ff_q_pvs_choice_resultlastnegative * S ((S (e)) * dst_negative_scale_choice_resultlast) + (dst_negative_choice_resultlast))) /\ (exists ge_balance_positive_choice_resultlastvalue ge_balance_negative_choice_resultlastvalue. (((((dfg_last_choice_result) = 2 * (ge_balance_positive_choice_resultlastvalue) /\ (ge_balance_negative_choice_resultlastvalue) = 0) \/ exists ge_signed_half_choice_resultlastvaluedecode. (((dfg_last_choice_result) = 2 * ge_signed_half_choice_resultlastvaluedecode + 1 /\ (ge_balance_positive_choice_resultlastvalue) = 0) /\ (ge_balance_negative_choice_resultlastvalue) = S ge_signed_half_choice_resultlastvaluedecode))) /\ ((dst_positive_choice_resultlast) + ge_balance_negative_choice_resultlastvalue = (dst_negative_choice_resultlast) + ge_balance_positive_choice_resultlastvalue))))))))) /\ (((exists dst_positive_code_choice_resultmiddle dst_positive_scale_choice_resultmiddle dst_negative_code_choice_resultmiddle dst_negative_scale_choice_resultmiddle dst_positive_choice_resultmiddle dst_negative_choice_resultmiddle. (((G) = (((((dst_positive_code_choice_resultmiddle) + (dst_positive_scale_choice_resultmiddle)) * S ((dst_positive_code_choice_resultmiddle) + (dst_positive_scale_choice_resultmiddle)) + ((dst_positive_scale_choice_resultmiddle) + (dst_positive_scale_choice_resultmiddle))) + (((dst_negative_code_choice_resultmiddle) + (dst_negative_scale_choice_resultmiddle)) * S ((dst_negative_code_choice_resultmiddle) + (dst_negative_scale_choice_resultmiddle)) + ((dst_negative_scale_choice_resultmiddle) + (dst_negative_scale_choice_resultmiddle)))) * S ((((dst_positive_code_choice_resultmiddle) + (dst_positive_scale_choice_resultmiddle)) * S ((dst_positive_code_choice_resultmiddle) + (dst_positive_scale_choice_resultmiddle)) + ((dst_positive_scale_choice_resultmiddle) + (dst_positive_scale_choice_resultmiddle))) + (((dst_negative_code_choice_resultmiddle) + (dst_negative_scale_choice_resultmiddle)) * S ((dst_negative_code_choice_resultmiddle) + (dst_negative_scale_choice_resultmiddle)) + ((dst_negative_scale_choice_resultmiddle) + (dst_negative_scale_choice_resultmiddle)))) + ((((dst_negative_code_choice_resultmiddle) + (dst_negative_scale_choice_resultmiddle)) * S ((dst_negative_code_choice_resultmiddle) + (dst_negative_scale_choice_resultmiddle)) + ((dst_negative_scale_choice_resultmiddle) + (dst_negative_scale_choice_resultmiddle))) + (((dst_negative_code_choice_resultmiddle) + (dst_negative_scale_choice_resultmiddle)) * S ((dst_negative_code_choice_resultmiddle) + (dst_negative_scale_choice_resultmiddle)) + ((dst_negative_scale_choice_resultmiddle) + (dst_negative_scale_choice_resultmiddle)))))) /\ (((((exists ff_h_pvs_choice_resultmiddlepositive. ff_h_pvs_choice_resultmiddlepositive + S (dst_positive_choice_resultmiddle) = S ((S (dfg_middle_choice_result)) * dst_positive_scale_choice_resultmiddle)) /\ exists ff_q_pvs_choice_resultmiddlepositive. dst_positive_code_choice_resultmiddle = ff_q_pvs_choice_resultmiddlepositive * S ((S (dfg_middle_choice_result)) * dst_positive_scale_choice_resultmiddle) + (dst_positive_choice_resultmiddle))) /\ (((((exists ff_h_pvs_choice_resultmiddlenegative. ff_h_pvs_choice_resultmiddlenegative + S (dst_negative_choice_resultmiddle) = S ((S (dfg_middle_choice_result)) * dst_negative_scale_choice_resultmiddle)) /\ exists ff_q_pvs_choice_resultmiddlenegative. dst_negative_code_choice_resultmiddle = ff_q_pvs_choice_resultmiddlenegative * S ((S (dfg_middle_choice_result)) * dst_negative_scale_choice_resultmiddle) + (dst_negative_choice_resultmiddle))) /\ (exists ge_balance_positive_choice_resultmiddlevalue ge_balance_negative_choice_resultmiddlevalue. (((((dfg_value_choice_result) = 2 * (ge_balance_positive_choice_resultmiddlevalue) /\ (ge_balance_negative_choice_resultmiddlevalue) = 0) \/ exists ge_signed_half_choice_resultmiddlevaluedecode. (((dfg_value_choice_result) = 2 * ge_signed_half_choice_resultmiddlevaluedecode + 1 /\ (ge_balance_positive_choice_resultmiddlevalue) = 0) /\ (ge_balance_negative_choice_resultmiddlevalue) = S ge_signed_half_choice_resultmiddlevaluedecode))) /\ ((dst_positive_choice_resultmiddle) + ge_balance_negative_choice_resultmiddlevalue = (dst_negative_choice_resultmiddle) + ge_balance_positive_choice_resultmiddlevalue))))))))) /\ (exists dfg_inner_choice_resultproduct. ((exists sto_ap_choice_resultproductinner sto_an_choice_resultproductinner sto_bp_choice_resultproductinner sto_bn_choice_resultproductinner sto_cp_choice_resultproductinner sto_cn_choice_resultproductinner. (((((dfg_last_choice_result) = 2 * (sto_ap_choice_resultproductinner) /\ (sto_an_choice_resultproductinner) = 0) \/ exists ge_signed_half_choice_resultproductinnerleft. (((dfg_last_choice_result) = 2 * ge_signed_half_choice_resultproductinnerleft + 1 /\ (sto_ap_choice_resultproductinner) = 0) /\ (sto_an_choice_resultproductinner) = S ge_signed_half_choice_resultproductinnerleft))) /\ ((((((dfg_value_choice_result) = 2 * (sto_bp_choice_resultproductinner) /\ (sto_bn_choice_resultproductinner) = 0) \/ exists ge_signed_half_choice_resultproductinnerright. (((dfg_value_choice_result) = 2 * ge_signed_half_choice_resultproductinnerright + 1 /\ (sto_bp_choice_resultproductinner) = 0) /\ (sto_bn_choice_resultproductinner) = S ge_signed_half_choice_resultproductinnerright))) /\ ((((((dfg_inner_choice_resultproduct) = 2 * (sto_cp_choice_resultproductinner) /\ (sto_cn_choice_resultproductinner) = 0) \/ exists ge_signed_half_choice_resultproductinneroutput. (((dfg_inner_choice_resultproduct) = 2 * ge_signed_half_choice_resultproductinneroutput + 1 /\ (sto_cp_choice_resultproductinner) = 0) /\ (sto_cn_choice_resultproductinner) = S ge_signed_half_choice_resultproductinneroutput))) /\ ((sto_ap_choice_resultproductinner * sto_bp_choice_resultproductinner + sto_an_choice_resultproductinner * sto_bn_choice_resultproductinner) + sto_cn_choice_resultproductinner = (sto_ap_choice_resultproductinner * sto_bn_choice_resultproductinner + sto_an_choice_resultproductinner * sto_bp_choice_resultproductinner) + sto_cp_choice_resultproductinner))))))) /\ (exists sto_ap_choice_resultproductouter sto_an_choice_resultproductouter sto_bp_choice_resultproductouter sto_bn_choice_resultproductouter sto_cp_choice_resultproductouter sto_cn_choice_resultproductouter. (((((dfg_first_choice_result) = 2 * (sto_ap_choice_resultproductouter) /\ (sto_an_choice_resultproductouter) = 0) \/ exists ge_signed_half_choice_resultproductouterleft. (((dfg_first_choice_result) = 2 * ge_signed_half_choice_resultproductouterleft + 1 /\ (sto_ap_choice_resultproductouter) = 0) /\ (sto_an_choice_resultproductouter) = S ge_signed_half_choice_resultproductouterleft))) /\ ((((((dfg_inner_choice_resultproduct) = 2 * (sto_bp_choice_resultproductouter) /\ (sto_bn_choice_resultproductouter) = 0) \/ exists ge_signed_half_choice_resultproductouterright. (((dfg_inner_choice_resultproduct) = 2 * ge_signed_half_choice_resultproductouterright + 1 /\ (sto_bp_choice_resultproductouter) = 0) /\ (sto_bn_choice_resultproductouter) = S ge_signed_half_choice_resultproductouterright))) /\ ((((((z) = 2 * (sto_cp_choice_resultproductouter) /\ (sto_cn_choice_resultproductouter) = 0) \/ exists ge_signed_half_choice_resultproductouteroutput. (((z) = 2 * ge_signed_half_choice_resultproductouteroutput + 1 /\ (sto_cp_choice_resultproductouter) = 0) /\ (sto_cn_choice_resultproductouter) = S ge_signed_half_choice_resultproductouteroutput))) /\ ((sto_ap_choice_resultproductouter * sto_bp_choice_resultproductouter + sto_an_choice_resultproductouter * sto_bn_choice_resultproductouter) + sto_cn_choice_resultproductouter = (sto_ap_choice_resultproductouter * sto_bn_choice_resultproductouter + sto_an_choice_resultproductouter * sto_bp_choice_resultproductouter) + sto_cp_choice_resultproductouter))))))))))))))))))))) \/ ((((a)=0 \/ ((e)=0 \/ ~(exists pvs_factor_choice_resultomittednondivisor. (n) = ((a)*(e)) * pvs_factor_choice_resultomittednondivisor))) /\ ((z)=0))))

Complete tactic proof in conservative notation

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

117 script commands · 34 reading checkpoints · 8 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 (2)
dirichlet grid entry omitteddirichlet grid entry from factorization
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 H
  4. L4
    intro n
  5. L5
    intro a
  6. L6
    intro e
  7. L7
    intro hF
  8. L8
    intro hG
  9. L9
    intro hH
02Establish haL10–13

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

  1. L10
    have ha : a=0 \/ ~(a=0)
  2. L11
    specialize eq_decidable (a)
  3. L12
    specialize eq_decidable (0)
  4. L13
    apply eq_decidable
03Separate the logical casesL14–14

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

  1. L14
    cases ha
04Construct an explicit witnessL15–15

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

  1. L15
    exists 0
05Use earlier factsL16–22

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

  1. L16
    specialize dirichlet_grid_entry_omitted (F)
  2. L17
    specialize dirichlet_grid_entry_omitted (G)
  3. L18
    specialize dirichlet_grid_entry_omitted (H)
  4. L19
    specialize dirichlet_grid_entry_omitted (n)
  5. L20
    specialize dirichlet_grid_entry_omitted (a)
  6. L21
    specialize dirichlet_grid_entry_omitted (e)
  7. L22
    apply dirichlet_grid_entry_omitted
06Separate the logical casesL23–23

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

  1. L23
    left
07Use earlier factsL24–24

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

  1. L24
    exact ha_left
08Establish heL25–28

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

  1. L25
    have he : e=0 \/ ~(e=0)
  2. L26
    specialize eq_decidable (e)
  3. L27
    specialize eq_decidable (0)
  4. L28
    apply eq_decidable
09Separate the logical casesL29–29

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

  1. L29
    cases he
10Construct an explicit witnessL30–30

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

  1. L30
    exists 0
11Use earlier factsL31–37

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

  1. L31
    specialize dirichlet_grid_entry_omitted (F)
  2. L32
    specialize dirichlet_grid_entry_omitted (G)
  3. L33
    specialize dirichlet_grid_entry_omitted (H)
  4. L34
    specialize dirichlet_grid_entry_omitted (n)
  5. L35
    specialize dirichlet_grid_entry_omitted (a)
  6. L36
    specialize dirichlet_grid_entry_omitted (e)
  7. L37
    apply dirichlet_grid_entry_omitted
12Separate the logical casesL38–39

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

  1. L38
    right
  2. L39
    left
13Use earlier factsL40–40

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

  1. L40
    exact he_left
14Establish hdL41–50

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

  1. L41
    have hd : Dvd(a · e,n) ∨ ¬Dvd(a · e,n)Definitions: Dvd(a · e,n)Original native command in the exact edition
  2. L42
    specialize multiple_decidable_nonzero (a*e)
  3. L43
    specialize multiple_decidable_nonzero (n)
  4. L44
    apply multiple_decidable_nonzero
  5. L45
    intro hmulzero
  6. L46
    specialize mul_ne_zero (a)
  7. L47
    specialize mul_ne_zero (e)
  8. L48
    apply mul_ne_zero
  9. L49
    exact ha_right
  10. L50
    exact he_right
15Use earlier factsL51–51

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

  1. L51
    exact hmulzero
16Separate the logical casesL52–53

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

  1. L52
    cases hd
  2. L53
    cases hd_left
17Establish huL54–59

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

  1. L54
    have hu : ∃ z. ArithAt(F,a,z)Definitions: ArithAt(F,a,z)Original native command in the exact edition
  2. L55
    specialize signed_table_lookup_any (0)
  3. L56
    specialize signed_table_lookup_any (F)
  4. L57
    specialize signed_table_lookup_any (a)
  5. L58
    apply signed_table_lookup_any
  6. L59
    exact hF
18Separate the logical casesL60–60

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

  1. L60
    cases hu
19Establish hvL61–66

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

  1. L61
    have hv : ∃ z. ArithAt(H,e,z)Definitions: ArithAt(H,e,z)Original native command in the exact edition
  2. L62
    specialize signed_table_lookup_any (0)
  3. L63
    specialize signed_table_lookup_any (H)
  4. L64
    specialize signed_table_lookup_any (e)
  5. L65
    apply signed_table_lookup_any
  6. L66
    exact hH
20Separate the logical casesL67–67

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

  1. L67
    cases hv
21Establish hwL68–73

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

  1. L68
    have hw : ∃ z. ArithAt(G,x,z)Definitions: ArithAt(G,x,z)Original native command in the exact edition
  2. L69
    specialize signed_table_lookup_any (0)
  3. L70
    specialize signed_table_lookup_any (G)
  4. L71
    specialize signed_table_lookup_any (x)
  5. L72
    apply signed_table_lookup_any
  6. L73
    exact hG
22Separate the logical casesL74–74

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

  1. L74
    cases hw
23Establish hiL75–78

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

  1. L75
    have hi : ∃ r. SignedMul(x2,x3,r)Definitions: SignedMul(x2,x3,r)Original native command in the exact edition
  2. L76
    specialize signed_mul_total (x2)
  3. L77
    specialize signed_mul_total (x3)
  4. L78
    apply signed_mul_total
24Separate the logical casesL79–79

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

  1. L79
    cases hi
25Establish hoL80–83

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

  1. L80
    have ho : ∃ z. SignedMul(x1,x4,z)Definitions: SignedMul(x1,x4,z)Original native command in the exact edition
  2. L81
    specialize signed_mul_total (x1)
  3. L82
    specialize signed_mul_total (x4)
  4. L83
    apply signed_mul_total
26Separate the logical casesL84–84

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

  1. L84
    cases ho
27Construct an explicit witnessL85–85

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

  1. L85
    exists x5
28Use earlier factsL86–95

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

  1. L86
    specialize dirichlet_grid_entry_from_factorization (F)
  2. L87
    specialize dirichlet_grid_entry_from_factorization (G)
  3. L88
    specialize dirichlet_grid_entry_from_factorization (H)
  4. L89
    specialize dirichlet_grid_entry_from_factorization (n)
  5. L90
    specialize dirichlet_grid_entry_from_factorization (a)
  6. L91
    specialize dirichlet_grid_entry_from_factorization (e)
  7. L92
    specialize dirichlet_grid_entry_from_factorization (x)
  8. L93
    specialize dirichlet_grid_entry_from_factorization (x1)
  9. L94
    specialize dirichlet_grid_entry_from_factorization (x2)
  10. L95
    specialize dirichlet_grid_entry_from_factorization (x3)
29Use earlier factsL96–105

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

  1. L96
    specialize dirichlet_grid_entry_from_factorization (x4)
  2. L97
    specialize dirichlet_grid_entry_from_factorization (x5)
  3. L98
    apply dirichlet_grid_entry_from_factorization
  4. L99
    exact ha_right
  5. L100
    exact he_right
  6. L101
    exact hd_left_witness
  7. L102
    exact hu_witness
  8. L103
    exact hv_witness
  9. L104
    exact hw_witness
  10. L105
    exact hi_witness
30Use earlier factsL106–106

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

  1. L106
    exact ho_witness
31Construct an explicit witnessL107–107

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

  1. L107
    exists 0
32Use earlier factsL108–114

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

  1. L108
    specialize dirichlet_grid_entry_omitted (F)
  2. L109
    specialize dirichlet_grid_entry_omitted (G)
  3. L110
    specialize dirichlet_grid_entry_omitted (H)
  4. L111
    specialize dirichlet_grid_entry_omitted (n)
  5. L112
    specialize dirichlet_grid_entry_omitted (a)
  6. L113
    specialize dirichlet_grid_entry_omitted (e)
  7. L114
    apply dirichlet_grid_entry_omitted
33Separate the logical casesL115–116

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

  1. L115
    right
  2. L116
    right
34Use earlier factsL117–117

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

  1. L117
    exact hd_right

Library-wide reading audit

Original defined command ledger · 117 lines
  1. 0001intro F
  2. 0002intro G
  3. 0003intro H
  4. 0004intro n
  5. 0005intro a
  6. 0006intro e
  7. 0007intro hF
  8. 0008intro hG
  9. 0009intro hH
  10. 0010have ha : a=0 \/ ~(a=0)
  11. 0011specialize eq_decidable (a)
  12. 0012specialize eq_decidable (0)
  13. 0013apply eq_decidable
  14. 0014cases ha
  15. 0015exists 0
  16. 0016specialize dirichlet_grid_entry_omitted (F)
  17. 0017specialize dirichlet_grid_entry_omitted (G)
  18. 0018specialize dirichlet_grid_entry_omitted (H)
  19. 0019specialize dirichlet_grid_entry_omitted (n)
  20. 0020specialize dirichlet_grid_entry_omitted (a)
  21. 0021specialize dirichlet_grid_entry_omitted (e)
  22. 0022apply dirichlet_grid_entry_omitted
  23. 0023left
  24. 0024exact ha_left
  25. 0025have he : e=0 \/ ~(e=0)
  26. 0026specialize eq_decidable (e)
  27. 0027specialize eq_decidable (0)
  28. 0028apply eq_decidable
  29. 0029cases he
  30. 0030exists 0
  31. 0031specialize dirichlet_grid_entry_omitted (F)
  32. 0032specialize dirichlet_grid_entry_omitted (G)
  33. 0033specialize dirichlet_grid_entry_omitted (H)
  34. 0034specialize dirichlet_grid_entry_omitted (n)
  35. 0035specialize dirichlet_grid_entry_omitted (a)
  36. 0036specialize dirichlet_grid_entry_omitted (e)
  37. 0037apply dirichlet_grid_entry_omitted
  38. 0038right
  39. 0039left
  40. 0040exact he_left
  41. 0041have hd : Dvd(a · e,n) ∨ ¬Dvd(a · e,n)
  42. 0042specialize multiple_decidable_nonzero (a*e)
  43. 0043specialize multiple_decidable_nonzero (n)
  44. 0044apply multiple_decidable_nonzero
  45. 0045intro hmulzero
  46. 0046specialize mul_ne_zero (a)
  47. 0047specialize mul_ne_zero (e)
  48. 0048apply mul_ne_zero
  49. 0049exact ha_right
  50. 0050exact he_right
  51. 0051exact hmulzero
  52. 0052cases hd
  53. 0053cases hd_left
  54. 0054have hu : ∃ z. ArithAt(F,a,z)
  55. 0055specialize signed_table_lookup_any (0)
  56. 0056specialize signed_table_lookup_any (F)
  57. 0057specialize signed_table_lookup_any (a)
  58. 0058apply signed_table_lookup_any
  59. 0059exact hF
  60. 0060cases hu
  61. 0061have hv : ∃ z. ArithAt(H,e,z)
  62. 0062specialize signed_table_lookup_any (0)
  63. 0063specialize signed_table_lookup_any (H)
  64. 0064specialize signed_table_lookup_any (e)
  65. 0065apply signed_table_lookup_any
  66. 0066exact hH
  67. 0067cases hv
  68. 0068have hw : ∃ z. ArithAt(G,x,z)
  69. 0069specialize signed_table_lookup_any (0)
  70. 0070specialize signed_table_lookup_any (G)
  71. 0071specialize signed_table_lookup_any (x)
  72. 0072apply signed_table_lookup_any
  73. 0073exact hG
  74. 0074cases hw
  75. 0075have hi : ∃ r. SignedMul(x2,x3,r)
  76. 0076specialize signed_mul_total (x2)
  77. 0077specialize signed_mul_total (x3)
  78. 0078apply signed_mul_total
  79. 0079cases hi
  80. 0080have ho : ∃ z. SignedMul(x1,x4,z)
  81. 0081specialize signed_mul_total (x1)
  82. 0082specialize signed_mul_total (x4)
  83. 0083apply signed_mul_total
  84. 0084cases ho
  85. 0085exists x5
  86. 0086specialize dirichlet_grid_entry_from_factorization (F)
  87. 0087specialize dirichlet_grid_entry_from_factorization (G)
  88. 0088specialize dirichlet_grid_entry_from_factorization (H)
  89. 0089specialize dirichlet_grid_entry_from_factorization (n)
  90. 0090specialize dirichlet_grid_entry_from_factorization (a)
  91. 0091specialize dirichlet_grid_entry_from_factorization (e)
  92. 0092specialize dirichlet_grid_entry_from_factorization (x)
  93. 0093specialize dirichlet_grid_entry_from_factorization (x1)
  94. 0094specialize dirichlet_grid_entry_from_factorization (x2)
  95. 0095specialize dirichlet_grid_entry_from_factorization (x3)
  96. 0096specialize dirichlet_grid_entry_from_factorization (x4)
  97. 0097specialize dirichlet_grid_entry_from_factorization (x5)
  98. 0098apply dirichlet_grid_entry_from_factorization
  99. 0099exact ha_right
  100. 0100exact he_right
  101. 0101exact hd_left_witness
  102. 0102exact hu_witness
  103. 0103exact hv_witness
  104. 0104exact hw_witness
  105. 0105exact hi_witness
  106. 0106exact ho_witness
  107. 0107exists 0
  108. 0108specialize dirichlet_grid_entry_omitted (F)
  109. 0109specialize dirichlet_grid_entry_omitted (G)
  110. 0110specialize dirichlet_grid_entry_omitted (H)
  111. 0111specialize dirichlet_grid_entry_omitted (n)
  112. 0112specialize dirichlet_grid_entry_omitted (a)
  113. 0113specialize dirichlet_grid_entry_omitted (e)
  114. 0114apply dirichlet_grid_entry_omitted
  115. 0115right
  116. 0116right
  117. 0117exact hd_right