DF0005

dirichlet_grid_entry_functional

Each genuine first/last-factor cell has one canonical signed value, without identifying any table representation.

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. ∀ z. ∀ Z. DirichletGridEntry(F,G,H,n,a,e,z) → DirichletGridEntry(F,G,H,n,a,e,Z) → z = Z

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

Definition DAG

SignedMul(a,b,c) · 2DirichletGridEntry(F,G,H,n,a,e,z) · 2

Actual proof prerequisites

dirichlet_grid_entry_factor_productsigned_mul_functional · checked external prerequisitedirichlet_grid_entry_omitted_value
Original expanded first-order statement 
forall F G H n a e z Z. ((((~((a)=0)) /\ (((~((e)=0)) /\ (exists dfg_middle_unique_first dfg_first_unique_first dfg_last_unique_first dfg_value_unique_first. (((n)=((a)*(e))*dfg_middle_unique_first) /\ (((exists dst_positive_code_unique_firstfirst dst_positive_scale_unique_firstfirst dst_negative_code_unique_firstfirst dst_negative_scale_unique_firstfirst dst_positive_unique_firstfirst dst_negative_unique_firstfirst. (((F) = (((((dst_positive_code_unique_firstfirst) + (dst_positive_scale_unique_firstfirst)) * S ((dst_positive_code_unique_firstfirst) + (dst_positive_scale_unique_firstfirst)) + ((dst_positive_scale_unique_firstfirst) + (dst_positive_scale_unique_firstfirst))) + (((dst_negative_code_unique_firstfirst) + (dst_negative_scale_unique_firstfirst)) * S ((dst_negative_code_unique_firstfirst) + (dst_negative_scale_unique_firstfirst)) + ((dst_negative_scale_unique_firstfirst) + (dst_negative_scale_unique_firstfirst)))) * S ((((dst_positive_code_unique_firstfirst) + (dst_positive_scale_unique_firstfirst)) * S ((dst_positive_code_unique_firstfirst) + (dst_positive_scale_unique_firstfirst)) + ((dst_positive_scale_unique_firstfirst) + (dst_positive_scale_unique_firstfirst))) + (((dst_negative_code_unique_firstfirst) + (dst_negative_scale_unique_firstfirst)) * S ((dst_negative_code_unique_firstfirst) + (dst_negative_scale_unique_firstfirst)) + ((dst_negative_scale_unique_firstfirst) + (dst_negative_scale_unique_firstfirst)))) + ((((dst_negative_code_unique_firstfirst) + (dst_negative_scale_unique_firstfirst)) * S ((dst_negative_code_unique_firstfirst) + (dst_negative_scale_unique_firstfirst)) + ((dst_negative_scale_unique_firstfirst) + (dst_negative_scale_unique_firstfirst))) + (((dst_negative_code_unique_firstfirst) + (dst_negative_scale_unique_firstfirst)) * S ((dst_negative_code_unique_firstfirst) + (dst_negative_scale_unique_firstfirst)) + ((dst_negative_scale_unique_firstfirst) + (dst_negative_scale_unique_firstfirst)))))) /\ (((((exists ff_h_pvs_unique_firstfirstpositive. ff_h_pvs_unique_firstfirstpositive + S (dst_positive_unique_firstfirst) = S ((S (a)) * dst_positive_scale_unique_firstfirst)) /\ exists ff_q_pvs_unique_firstfirstpositive. dst_positive_code_unique_firstfirst = ff_q_pvs_unique_firstfirstpositive * S ((S (a)) * dst_positive_scale_unique_firstfirst) + (dst_positive_unique_firstfirst))) /\ (((((exists ff_h_pvs_unique_firstfirstnegative. ff_h_pvs_unique_firstfirstnegative + S (dst_negative_unique_firstfirst) = S ((S (a)) * dst_negative_scale_unique_firstfirst)) /\ exists ff_q_pvs_unique_firstfirstnegative. dst_negative_code_unique_firstfirst = ff_q_pvs_unique_firstfirstnegative * S ((S (a)) * dst_negative_scale_unique_firstfirst) + (dst_negative_unique_firstfirst))) /\ (exists ge_balance_positive_unique_firstfirstvalue ge_balance_negative_unique_firstfirstvalue. (((((dfg_first_unique_first) = 2 * (ge_balance_positive_unique_firstfirstvalue) /\ (ge_balance_negative_unique_firstfirstvalue) = 0) \/ exists ge_signed_half_unique_firstfirstvaluedecode. (((dfg_first_unique_first) = 2 * ge_signed_half_unique_firstfirstvaluedecode + 1 /\ (ge_balance_positive_unique_firstfirstvalue) = 0) /\ (ge_balance_negative_unique_firstfirstvalue) = S ge_signed_half_unique_firstfirstvaluedecode))) /\ ((dst_positive_unique_firstfirst) + ge_balance_negative_unique_firstfirstvalue = (dst_negative_unique_firstfirst) + ge_balance_positive_unique_firstfirstvalue))))))))) /\ (((exists dst_positive_code_unique_firstlast dst_positive_scale_unique_firstlast dst_negative_code_unique_firstlast dst_negative_scale_unique_firstlast dst_positive_unique_firstlast dst_negative_unique_firstlast. (((H) = (((((dst_positive_code_unique_firstlast) + (dst_positive_scale_unique_firstlast)) * S ((dst_positive_code_unique_firstlast) + (dst_positive_scale_unique_firstlast)) + ((dst_positive_scale_unique_firstlast) + (dst_positive_scale_unique_firstlast))) + (((dst_negative_code_unique_firstlast) + (dst_negative_scale_unique_firstlast)) * S ((dst_negative_code_unique_firstlast) + (dst_negative_scale_unique_firstlast)) + ((dst_negative_scale_unique_firstlast) + (dst_negative_scale_unique_firstlast)))) * S ((((dst_positive_code_unique_firstlast) + (dst_positive_scale_unique_firstlast)) * S ((dst_positive_code_unique_firstlast) + (dst_positive_scale_unique_firstlast)) + ((dst_positive_scale_unique_firstlast) + (dst_positive_scale_unique_firstlast))) + (((dst_negative_code_unique_firstlast) + (dst_negative_scale_unique_firstlast)) * S ((dst_negative_code_unique_firstlast) + (dst_negative_scale_unique_firstlast)) + ((dst_negative_scale_unique_firstlast) + (dst_negative_scale_unique_firstlast)))) + ((((dst_negative_code_unique_firstlast) + (dst_negative_scale_unique_firstlast)) * S ((dst_negative_code_unique_firstlast) + (dst_negative_scale_unique_firstlast)) + ((dst_negative_scale_unique_firstlast) + (dst_negative_scale_unique_firstlast))) + (((dst_negative_code_unique_firstlast) + (dst_negative_scale_unique_firstlast)) * S ((dst_negative_code_unique_firstlast) + (dst_negative_scale_unique_firstlast)) + ((dst_negative_scale_unique_firstlast) + (dst_negative_scale_unique_firstlast)))))) /\ (((((exists ff_h_pvs_unique_firstlastpositive. ff_h_pvs_unique_firstlastpositive + S (dst_positive_unique_firstlast) = S ((S (e)) * dst_positive_scale_unique_firstlast)) /\ exists ff_q_pvs_unique_firstlastpositive. dst_positive_code_unique_firstlast = ff_q_pvs_unique_firstlastpositive * S ((S (e)) * dst_positive_scale_unique_firstlast) + (dst_positive_unique_firstlast))) /\ (((((exists ff_h_pvs_unique_firstlastnegative. ff_h_pvs_unique_firstlastnegative + S (dst_negative_unique_firstlast) = S ((S (e)) * dst_negative_scale_unique_firstlast)) /\ exists ff_q_pvs_unique_firstlastnegative. dst_negative_code_unique_firstlast = ff_q_pvs_unique_firstlastnegative * S ((S (e)) * dst_negative_scale_unique_firstlast) + (dst_negative_unique_firstlast))) /\ (exists ge_balance_positive_unique_firstlastvalue ge_balance_negative_unique_firstlastvalue. (((((dfg_last_unique_first) = 2 * (ge_balance_positive_unique_firstlastvalue) /\ (ge_balance_negative_unique_firstlastvalue) = 0) \/ exists ge_signed_half_unique_firstlastvaluedecode. (((dfg_last_unique_first) = 2 * ge_signed_half_unique_firstlastvaluedecode + 1 /\ (ge_balance_positive_unique_firstlastvalue) = 0) /\ (ge_balance_negative_unique_firstlastvalue) = S ge_signed_half_unique_firstlastvaluedecode))) /\ ((dst_positive_unique_firstlast) + ge_balance_negative_unique_firstlastvalue = (dst_negative_unique_firstlast) + ge_balance_positive_unique_firstlastvalue))))))))) /\ (((exists dst_positive_code_unique_firstmiddle dst_positive_scale_unique_firstmiddle dst_negative_code_unique_firstmiddle dst_negative_scale_unique_firstmiddle dst_positive_unique_firstmiddle dst_negative_unique_firstmiddle. (((G) = (((((dst_positive_code_unique_firstmiddle) + (dst_positive_scale_unique_firstmiddle)) * S ((dst_positive_code_unique_firstmiddle) + (dst_positive_scale_unique_firstmiddle)) + ((dst_positive_scale_unique_firstmiddle) + (dst_positive_scale_unique_firstmiddle))) + (((dst_negative_code_unique_firstmiddle) + (dst_negative_scale_unique_firstmiddle)) * S ((dst_negative_code_unique_firstmiddle) + (dst_negative_scale_unique_firstmiddle)) + ((dst_negative_scale_unique_firstmiddle) + (dst_negative_scale_unique_firstmiddle)))) * S ((((dst_positive_code_unique_firstmiddle) + (dst_positive_scale_unique_firstmiddle)) * S ((dst_positive_code_unique_firstmiddle) + (dst_positive_scale_unique_firstmiddle)) + ((dst_positive_scale_unique_firstmiddle) + (dst_positive_scale_unique_firstmiddle))) + (((dst_negative_code_unique_firstmiddle) + (dst_negative_scale_unique_firstmiddle)) * S ((dst_negative_code_unique_firstmiddle) + (dst_negative_scale_unique_firstmiddle)) + ((dst_negative_scale_unique_firstmiddle) + (dst_negative_scale_unique_firstmiddle)))) + ((((dst_negative_code_unique_firstmiddle) + (dst_negative_scale_unique_firstmiddle)) * S ((dst_negative_code_unique_firstmiddle) + (dst_negative_scale_unique_firstmiddle)) + ((dst_negative_scale_unique_firstmiddle) + (dst_negative_scale_unique_firstmiddle))) + (((dst_negative_code_unique_firstmiddle) + (dst_negative_scale_unique_firstmiddle)) * S ((dst_negative_code_unique_firstmiddle) + (dst_negative_scale_unique_firstmiddle)) + ((dst_negative_scale_unique_firstmiddle) + (dst_negative_scale_unique_firstmiddle)))))) /\ (((((exists ff_h_pvs_unique_firstmiddlepositive. ff_h_pvs_unique_firstmiddlepositive + S (dst_positive_unique_firstmiddle) = S ((S (dfg_middle_unique_first)) * dst_positive_scale_unique_firstmiddle)) /\ exists ff_q_pvs_unique_firstmiddlepositive. dst_positive_code_unique_firstmiddle = ff_q_pvs_unique_firstmiddlepositive * S ((S (dfg_middle_unique_first)) * dst_positive_scale_unique_firstmiddle) + (dst_positive_unique_firstmiddle))) /\ (((((exists ff_h_pvs_unique_firstmiddlenegative. ff_h_pvs_unique_firstmiddlenegative + S (dst_negative_unique_firstmiddle) = S ((S (dfg_middle_unique_first)) * dst_negative_scale_unique_firstmiddle)) /\ exists ff_q_pvs_unique_firstmiddlenegative. dst_negative_code_unique_firstmiddle = ff_q_pvs_unique_firstmiddlenegative * S ((S (dfg_middle_unique_first)) * dst_negative_scale_unique_firstmiddle) + (dst_negative_unique_firstmiddle))) /\ (exists ge_balance_positive_unique_firstmiddlevalue ge_balance_negative_unique_firstmiddlevalue. (((((dfg_value_unique_first) = 2 * (ge_balance_positive_unique_firstmiddlevalue) /\ (ge_balance_negative_unique_firstmiddlevalue) = 0) \/ exists ge_signed_half_unique_firstmiddlevaluedecode. (((dfg_value_unique_first) = 2 * ge_signed_half_unique_firstmiddlevaluedecode + 1 /\ (ge_balance_positive_unique_firstmiddlevalue) = 0) /\ (ge_balance_negative_unique_firstmiddlevalue) = S ge_signed_half_unique_firstmiddlevaluedecode))) /\ ((dst_positive_unique_firstmiddle) + ge_balance_negative_unique_firstmiddlevalue = (dst_negative_unique_firstmiddle) + ge_balance_positive_unique_firstmiddlevalue))))))))) /\ (exists dfg_inner_unique_firstproduct. ((exists sto_ap_unique_firstproductinner sto_an_unique_firstproductinner sto_bp_unique_firstproductinner sto_bn_unique_firstproductinner sto_cp_unique_firstproductinner sto_cn_unique_firstproductinner. (((((dfg_last_unique_first) = 2 * (sto_ap_unique_firstproductinner) /\ (sto_an_unique_firstproductinner) = 0) \/ exists ge_signed_half_unique_firstproductinnerleft. (((dfg_last_unique_first) = 2 * ge_signed_half_unique_firstproductinnerleft + 1 /\ (sto_ap_unique_firstproductinner) = 0) /\ (sto_an_unique_firstproductinner) = S ge_signed_half_unique_firstproductinnerleft))) /\ ((((((dfg_value_unique_first) = 2 * (sto_bp_unique_firstproductinner) /\ (sto_bn_unique_firstproductinner) = 0) \/ exists ge_signed_half_unique_firstproductinnerright. (((dfg_value_unique_first) = 2 * ge_signed_half_unique_firstproductinnerright + 1 /\ (sto_bp_unique_firstproductinner) = 0) /\ (sto_bn_unique_firstproductinner) = S ge_signed_half_unique_firstproductinnerright))) /\ ((((((dfg_inner_unique_firstproduct) = 2 * (sto_cp_unique_firstproductinner) /\ (sto_cn_unique_firstproductinner) = 0) \/ exists ge_signed_half_unique_firstproductinneroutput. (((dfg_inner_unique_firstproduct) = 2 * ge_signed_half_unique_firstproductinneroutput + 1 /\ (sto_cp_unique_firstproductinner) = 0) /\ (sto_cn_unique_firstproductinner) = S ge_signed_half_unique_firstproductinneroutput))) /\ ((sto_ap_unique_firstproductinner * sto_bp_unique_firstproductinner + sto_an_unique_firstproductinner * sto_bn_unique_firstproductinner) + sto_cn_unique_firstproductinner = (sto_ap_unique_firstproductinner * sto_bn_unique_firstproductinner + sto_an_unique_firstproductinner * sto_bp_unique_firstproductinner) + sto_cp_unique_firstproductinner))))))) /\ (exists sto_ap_unique_firstproductouter sto_an_unique_firstproductouter sto_bp_unique_firstproductouter sto_bn_unique_firstproductouter sto_cp_unique_firstproductouter sto_cn_unique_firstproductouter. (((((dfg_first_unique_first) = 2 * (sto_ap_unique_firstproductouter) /\ (sto_an_unique_firstproductouter) = 0) \/ exists ge_signed_half_unique_firstproductouterleft. (((dfg_first_unique_first) = 2 * ge_signed_half_unique_firstproductouterleft + 1 /\ (sto_ap_unique_firstproductouter) = 0) /\ (sto_an_unique_firstproductouter) = S ge_signed_half_unique_firstproductouterleft))) /\ ((((((dfg_inner_unique_firstproduct) = 2 * (sto_bp_unique_firstproductouter) /\ (sto_bn_unique_firstproductouter) = 0) \/ exists ge_signed_half_unique_firstproductouterright. (((dfg_inner_unique_firstproduct) = 2 * ge_signed_half_unique_firstproductouterright + 1 /\ (sto_bp_unique_firstproductouter) = 0) /\ (sto_bn_unique_firstproductouter) = S ge_signed_half_unique_firstproductouterright))) /\ ((((((z) = 2 * (sto_cp_unique_firstproductouter) /\ (sto_cn_unique_firstproductouter) = 0) \/ exists ge_signed_half_unique_firstproductouteroutput. (((z) = 2 * ge_signed_half_unique_firstproductouteroutput + 1 /\ (sto_cp_unique_firstproductouter) = 0) /\ (sto_cn_unique_firstproductouter) = S ge_signed_half_unique_firstproductouteroutput))) /\ ((sto_ap_unique_firstproductouter * sto_bp_unique_firstproductouter + sto_an_unique_firstproductouter * sto_bn_unique_firstproductouter) + sto_cn_unique_firstproductouter = (sto_ap_unique_firstproductouter * sto_bn_unique_firstproductouter + sto_an_unique_firstproductouter * sto_bp_unique_firstproductouter) + sto_cp_unique_firstproductouter))))))))))))))))))))) \/ ((((a)=0 \/ ((e)=0 \/ ~(exists pvs_factor_unique_firstomittednondivisor. (n) = ((a)*(e)) * pvs_factor_unique_firstomittednondivisor))) /\ ((z)=0)))) -> ((((~((a)=0)) /\ (((~((e)=0)) /\ (exists dfg_middle_unique_second dfg_first_unique_second dfg_last_unique_second dfg_value_unique_second. (((n)=((a)*(e))*dfg_middle_unique_second) /\ (((exists dst_positive_code_unique_secondfirst dst_positive_scale_unique_secondfirst dst_negative_code_unique_secondfirst dst_negative_scale_unique_secondfirst dst_positive_unique_secondfirst dst_negative_unique_secondfirst. (((F) = (((((dst_positive_code_unique_secondfirst) + (dst_positive_scale_unique_secondfirst)) * S ((dst_positive_code_unique_secondfirst) + (dst_positive_scale_unique_secondfirst)) + ((dst_positive_scale_unique_secondfirst) + (dst_positive_scale_unique_secondfirst))) + (((dst_negative_code_unique_secondfirst) + (dst_negative_scale_unique_secondfirst)) * S ((dst_negative_code_unique_secondfirst) + (dst_negative_scale_unique_secondfirst)) + ((dst_negative_scale_unique_secondfirst) + (dst_negative_scale_unique_secondfirst)))) * S ((((dst_positive_code_unique_secondfirst) + (dst_positive_scale_unique_secondfirst)) * S ((dst_positive_code_unique_secondfirst) + (dst_positive_scale_unique_secondfirst)) + ((dst_positive_scale_unique_secondfirst) + (dst_positive_scale_unique_secondfirst))) + (((dst_negative_code_unique_secondfirst) + (dst_negative_scale_unique_secondfirst)) * S ((dst_negative_code_unique_secondfirst) + (dst_negative_scale_unique_secondfirst)) + ((dst_negative_scale_unique_secondfirst) + (dst_negative_scale_unique_secondfirst)))) + ((((dst_negative_code_unique_secondfirst) + (dst_negative_scale_unique_secondfirst)) * S ((dst_negative_code_unique_secondfirst) + (dst_negative_scale_unique_secondfirst)) + ((dst_negative_scale_unique_secondfirst) + (dst_negative_scale_unique_secondfirst))) + (((dst_negative_code_unique_secondfirst) + (dst_negative_scale_unique_secondfirst)) * S ((dst_negative_code_unique_secondfirst) + (dst_negative_scale_unique_secondfirst)) + ((dst_negative_scale_unique_secondfirst) + (dst_negative_scale_unique_secondfirst)))))) /\ (((((exists ff_h_pvs_unique_secondfirstpositive. ff_h_pvs_unique_secondfirstpositive + S (dst_positive_unique_secondfirst) = S ((S (a)) * dst_positive_scale_unique_secondfirst)) /\ exists ff_q_pvs_unique_secondfirstpositive. dst_positive_code_unique_secondfirst = ff_q_pvs_unique_secondfirstpositive * S ((S (a)) * dst_positive_scale_unique_secondfirst) + (dst_positive_unique_secondfirst))) /\ (((((exists ff_h_pvs_unique_secondfirstnegative. ff_h_pvs_unique_secondfirstnegative + S (dst_negative_unique_secondfirst) = S ((S (a)) * dst_negative_scale_unique_secondfirst)) /\ exists ff_q_pvs_unique_secondfirstnegative. dst_negative_code_unique_secondfirst = ff_q_pvs_unique_secondfirstnegative * S ((S (a)) * dst_negative_scale_unique_secondfirst) + (dst_negative_unique_secondfirst))) /\ (exists ge_balance_positive_unique_secondfirstvalue ge_balance_negative_unique_secondfirstvalue. (((((dfg_first_unique_second) = 2 * (ge_balance_positive_unique_secondfirstvalue) /\ (ge_balance_negative_unique_secondfirstvalue) = 0) \/ exists ge_signed_half_unique_secondfirstvaluedecode. (((dfg_first_unique_second) = 2 * ge_signed_half_unique_secondfirstvaluedecode + 1 /\ (ge_balance_positive_unique_secondfirstvalue) = 0) /\ (ge_balance_negative_unique_secondfirstvalue) = S ge_signed_half_unique_secondfirstvaluedecode))) /\ ((dst_positive_unique_secondfirst) + ge_balance_negative_unique_secondfirstvalue = (dst_negative_unique_secondfirst) + ge_balance_positive_unique_secondfirstvalue))))))))) /\ (((exists dst_positive_code_unique_secondlast dst_positive_scale_unique_secondlast dst_negative_code_unique_secondlast dst_negative_scale_unique_secondlast dst_positive_unique_secondlast dst_negative_unique_secondlast. (((H) = (((((dst_positive_code_unique_secondlast) + (dst_positive_scale_unique_secondlast)) * S ((dst_positive_code_unique_secondlast) + (dst_positive_scale_unique_secondlast)) + ((dst_positive_scale_unique_secondlast) + (dst_positive_scale_unique_secondlast))) + (((dst_negative_code_unique_secondlast) + (dst_negative_scale_unique_secondlast)) * S ((dst_negative_code_unique_secondlast) + (dst_negative_scale_unique_secondlast)) + ((dst_negative_scale_unique_secondlast) + (dst_negative_scale_unique_secondlast)))) * S ((((dst_positive_code_unique_secondlast) + (dst_positive_scale_unique_secondlast)) * S ((dst_positive_code_unique_secondlast) + (dst_positive_scale_unique_secondlast)) + ((dst_positive_scale_unique_secondlast) + (dst_positive_scale_unique_secondlast))) + (((dst_negative_code_unique_secondlast) + (dst_negative_scale_unique_secondlast)) * S ((dst_negative_code_unique_secondlast) + (dst_negative_scale_unique_secondlast)) + ((dst_negative_scale_unique_secondlast) + (dst_negative_scale_unique_secondlast)))) + ((((dst_negative_code_unique_secondlast) + (dst_negative_scale_unique_secondlast)) * S ((dst_negative_code_unique_secondlast) + (dst_negative_scale_unique_secondlast)) + ((dst_negative_scale_unique_secondlast) + (dst_negative_scale_unique_secondlast))) + (((dst_negative_code_unique_secondlast) + (dst_negative_scale_unique_secondlast)) * S ((dst_negative_code_unique_secondlast) + (dst_negative_scale_unique_secondlast)) + ((dst_negative_scale_unique_secondlast) + (dst_negative_scale_unique_secondlast)))))) /\ (((((exists ff_h_pvs_unique_secondlastpositive. ff_h_pvs_unique_secondlastpositive + S (dst_positive_unique_secondlast) = S ((S (e)) * dst_positive_scale_unique_secondlast)) /\ exists ff_q_pvs_unique_secondlastpositive. dst_positive_code_unique_secondlast = ff_q_pvs_unique_secondlastpositive * S ((S (e)) * dst_positive_scale_unique_secondlast) + (dst_positive_unique_secondlast))) /\ (((((exists ff_h_pvs_unique_secondlastnegative. ff_h_pvs_unique_secondlastnegative + S (dst_negative_unique_secondlast) = S ((S (e)) * dst_negative_scale_unique_secondlast)) /\ exists ff_q_pvs_unique_secondlastnegative. dst_negative_code_unique_secondlast = ff_q_pvs_unique_secondlastnegative * S ((S (e)) * dst_negative_scale_unique_secondlast) + (dst_negative_unique_secondlast))) /\ (exists ge_balance_positive_unique_secondlastvalue ge_balance_negative_unique_secondlastvalue. (((((dfg_last_unique_second) = 2 * (ge_balance_positive_unique_secondlastvalue) /\ (ge_balance_negative_unique_secondlastvalue) = 0) \/ exists ge_signed_half_unique_secondlastvaluedecode. (((dfg_last_unique_second) = 2 * ge_signed_half_unique_secondlastvaluedecode + 1 /\ (ge_balance_positive_unique_secondlastvalue) = 0) /\ (ge_balance_negative_unique_secondlastvalue) = S ge_signed_half_unique_secondlastvaluedecode))) /\ ((dst_positive_unique_secondlast) + ge_balance_negative_unique_secondlastvalue = (dst_negative_unique_secondlast) + ge_balance_positive_unique_secondlastvalue))))))))) /\ (((exists dst_positive_code_unique_secondmiddle dst_positive_scale_unique_secondmiddle dst_negative_code_unique_secondmiddle dst_negative_scale_unique_secondmiddle dst_positive_unique_secondmiddle dst_negative_unique_secondmiddle. (((G) = (((((dst_positive_code_unique_secondmiddle) + (dst_positive_scale_unique_secondmiddle)) * S ((dst_positive_code_unique_secondmiddle) + (dst_positive_scale_unique_secondmiddle)) + ((dst_positive_scale_unique_secondmiddle) + (dst_positive_scale_unique_secondmiddle))) + (((dst_negative_code_unique_secondmiddle) + (dst_negative_scale_unique_secondmiddle)) * S ((dst_negative_code_unique_secondmiddle) + (dst_negative_scale_unique_secondmiddle)) + ((dst_negative_scale_unique_secondmiddle) + (dst_negative_scale_unique_secondmiddle)))) * S ((((dst_positive_code_unique_secondmiddle) + (dst_positive_scale_unique_secondmiddle)) * S ((dst_positive_code_unique_secondmiddle) + (dst_positive_scale_unique_secondmiddle)) + ((dst_positive_scale_unique_secondmiddle) + (dst_positive_scale_unique_secondmiddle))) + (((dst_negative_code_unique_secondmiddle) + (dst_negative_scale_unique_secondmiddle)) * S ((dst_negative_code_unique_secondmiddle) + (dst_negative_scale_unique_secondmiddle)) + ((dst_negative_scale_unique_secondmiddle) + (dst_negative_scale_unique_secondmiddle)))) + ((((dst_negative_code_unique_secondmiddle) + (dst_negative_scale_unique_secondmiddle)) * S ((dst_negative_code_unique_secondmiddle) + (dst_negative_scale_unique_secondmiddle)) + ((dst_negative_scale_unique_secondmiddle) + (dst_negative_scale_unique_secondmiddle))) + (((dst_negative_code_unique_secondmiddle) + (dst_negative_scale_unique_secondmiddle)) * S ((dst_negative_code_unique_secondmiddle) + (dst_negative_scale_unique_secondmiddle)) + ((dst_negative_scale_unique_secondmiddle) + (dst_negative_scale_unique_secondmiddle)))))) /\ (((((exists ff_h_pvs_unique_secondmiddlepositive. ff_h_pvs_unique_secondmiddlepositive + S (dst_positive_unique_secondmiddle) = S ((S (dfg_middle_unique_second)) * dst_positive_scale_unique_secondmiddle)) /\ exists ff_q_pvs_unique_secondmiddlepositive. dst_positive_code_unique_secondmiddle = ff_q_pvs_unique_secondmiddlepositive * S ((S (dfg_middle_unique_second)) * dst_positive_scale_unique_secondmiddle) + (dst_positive_unique_secondmiddle))) /\ (((((exists ff_h_pvs_unique_secondmiddlenegative. ff_h_pvs_unique_secondmiddlenegative + S (dst_negative_unique_secondmiddle) = S ((S (dfg_middle_unique_second)) * dst_negative_scale_unique_secondmiddle)) /\ exists ff_q_pvs_unique_secondmiddlenegative. dst_negative_code_unique_secondmiddle = ff_q_pvs_unique_secondmiddlenegative * S ((S (dfg_middle_unique_second)) * dst_negative_scale_unique_secondmiddle) + (dst_negative_unique_secondmiddle))) /\ (exists ge_balance_positive_unique_secondmiddlevalue ge_balance_negative_unique_secondmiddlevalue. (((((dfg_value_unique_second) = 2 * (ge_balance_positive_unique_secondmiddlevalue) /\ (ge_balance_negative_unique_secondmiddlevalue) = 0) \/ exists ge_signed_half_unique_secondmiddlevaluedecode. (((dfg_value_unique_second) = 2 * ge_signed_half_unique_secondmiddlevaluedecode + 1 /\ (ge_balance_positive_unique_secondmiddlevalue) = 0) /\ (ge_balance_negative_unique_secondmiddlevalue) = S ge_signed_half_unique_secondmiddlevaluedecode))) /\ ((dst_positive_unique_secondmiddle) + ge_balance_negative_unique_secondmiddlevalue = (dst_negative_unique_secondmiddle) + ge_balance_positive_unique_secondmiddlevalue))))))))) /\ (exists dfg_inner_unique_secondproduct. ((exists sto_ap_unique_secondproductinner sto_an_unique_secondproductinner sto_bp_unique_secondproductinner sto_bn_unique_secondproductinner sto_cp_unique_secondproductinner sto_cn_unique_secondproductinner. (((((dfg_last_unique_second) = 2 * (sto_ap_unique_secondproductinner) /\ (sto_an_unique_secondproductinner) = 0) \/ exists ge_signed_half_unique_secondproductinnerleft. (((dfg_last_unique_second) = 2 * ge_signed_half_unique_secondproductinnerleft + 1 /\ (sto_ap_unique_secondproductinner) = 0) /\ (sto_an_unique_secondproductinner) = S ge_signed_half_unique_secondproductinnerleft))) /\ ((((((dfg_value_unique_second) = 2 * (sto_bp_unique_secondproductinner) /\ (sto_bn_unique_secondproductinner) = 0) \/ exists ge_signed_half_unique_secondproductinnerright. (((dfg_value_unique_second) = 2 * ge_signed_half_unique_secondproductinnerright + 1 /\ (sto_bp_unique_secondproductinner) = 0) /\ (sto_bn_unique_secondproductinner) = S ge_signed_half_unique_secondproductinnerright))) /\ ((((((dfg_inner_unique_secondproduct) = 2 * (sto_cp_unique_secondproductinner) /\ (sto_cn_unique_secondproductinner) = 0) \/ exists ge_signed_half_unique_secondproductinneroutput. (((dfg_inner_unique_secondproduct) = 2 * ge_signed_half_unique_secondproductinneroutput + 1 /\ (sto_cp_unique_secondproductinner) = 0) /\ (sto_cn_unique_secondproductinner) = S ge_signed_half_unique_secondproductinneroutput))) /\ ((sto_ap_unique_secondproductinner * sto_bp_unique_secondproductinner + sto_an_unique_secondproductinner * sto_bn_unique_secondproductinner) + sto_cn_unique_secondproductinner = (sto_ap_unique_secondproductinner * sto_bn_unique_secondproductinner + sto_an_unique_secondproductinner * sto_bp_unique_secondproductinner) + sto_cp_unique_secondproductinner))))))) /\ (exists sto_ap_unique_secondproductouter sto_an_unique_secondproductouter sto_bp_unique_secondproductouter sto_bn_unique_secondproductouter sto_cp_unique_secondproductouter sto_cn_unique_secondproductouter. (((((dfg_first_unique_second) = 2 * (sto_ap_unique_secondproductouter) /\ (sto_an_unique_secondproductouter) = 0) \/ exists ge_signed_half_unique_secondproductouterleft. (((dfg_first_unique_second) = 2 * ge_signed_half_unique_secondproductouterleft + 1 /\ (sto_ap_unique_secondproductouter) = 0) /\ (sto_an_unique_secondproductouter) = S ge_signed_half_unique_secondproductouterleft))) /\ ((((((dfg_inner_unique_secondproduct) = 2 * (sto_bp_unique_secondproductouter) /\ (sto_bn_unique_secondproductouter) = 0) \/ exists ge_signed_half_unique_secondproductouterright. (((dfg_inner_unique_secondproduct) = 2 * ge_signed_half_unique_secondproductouterright + 1 /\ (sto_bp_unique_secondproductouter) = 0) /\ (sto_bn_unique_secondproductouter) = S ge_signed_half_unique_secondproductouterright))) /\ ((((((Z) = 2 * (sto_cp_unique_secondproductouter) /\ (sto_cn_unique_secondproductouter) = 0) \/ exists ge_signed_half_unique_secondproductouteroutput. (((Z) = 2 * ge_signed_half_unique_secondproductouteroutput + 1 /\ (sto_cp_unique_secondproductouter) = 0) /\ (sto_cn_unique_secondproductouter) = S ge_signed_half_unique_secondproductouteroutput))) /\ ((sto_ap_unique_secondproductouter * sto_bp_unique_secondproductouter + sto_an_unique_secondproductouter * sto_bn_unique_secondproductouter) + sto_cn_unique_secondproductouter = (sto_ap_unique_secondproductouter * sto_bn_unique_secondproductouter + sto_an_unique_secondproductouter * sto_bp_unique_secondproductouter) + sto_cp_unique_secondproductouter))))))))))))))))))))) \/ ((((a)=0 \/ ((e)=0 \/ ~(exists pvs_factor_unique_secondomittednondivisor. (n) = ((a)*(e)) * pvs_factor_unique_secondomittednondivisor))) /\ ((Z)=0)))) -> z=Z

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 · 13 reading checkpoints · 2 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 factor productdirichlet grid entry omitted value
01Fix variables and assumptionsL1–10

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 z
  8. L8
    intro Z
  9. L9
    intro hz
  10. L10
    intro hZ
02Separate the logical casesL11–20

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

  1. L11
    cases hz
  2. L12
    cases hz_left
  3. L13
    cases hz_left_right
  4. L14
    cases hz_left_right_right
  5. L15
    cases hz_left_right_right_witness
  6. L16
    cases hz_left_right_right_witness_witness
  7. L17
    cases hz_left_right_right_witness_witness_witness
  8. L18
    cases hz_left_right_right_witness_witness_witness_witness
  9. L19
    cases hz_left_right_right_witness_witness_witness_witness_right
  10. L20
    cases hz_left_right_right_witness_witness_witness_witness_right_right
03Separate the logical casesL21–21

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

  1. L21
    cases hz_left_right_right_witness_witness_witness_witness_right_right_right
04Establish hotherL22–31

Establish this local claim before using it. It is not an additional assumption.

  1. L22
    have hother : ∃ dfg_inner_unique_other. SignedMul(x2,x3,dfg_inner_unique_other) ∧ SignedMul(x1,dfg_inner_unique_other,Z)Definitions: SignedMul(x2,x3,dfg_inner_unique_other)SignedMul(x1,dfg_inner_unique_other,Z)Original native command in the exact edition
  2. L23
    specialize dirichlet_grid_entry_factor_product (F)
  3. L24
    specialize dirichlet_grid_entry_factor_product (G)
  4. L25
    specialize dirichlet_grid_entry_factor_product (H)
  5. L26
    specialize dirichlet_grid_entry_factor_product (n)
  6. L27
    specialize dirichlet_grid_entry_factor_product (a)
  7. L28
    specialize dirichlet_grid_entry_factor_product (e)
  8. L29
    specialize dirichlet_grid_entry_factor_product (x)
  9. L30
    specialize dirichlet_grid_entry_factor_product (x1)
  10. L31
    specialize dirichlet_grid_entry_factor_product (x2)
05Use earlier factsL32–41

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

  1. L32
    specialize dirichlet_grid_entry_factor_product (x3)
  2. L33
    specialize dirichlet_grid_entry_factor_product (Z)
  3. L34
    apply dirichlet_grid_entry_factor_product
  4. L35
    exact hz_left_left
  5. L36
    exact hz_left_right_left
  6. L37
    exact hz_left_right_right_witness_witness_witness_witness_left
  7. L38
    exact hz_left_right_right_witness_witness_witness_witness_right_left
  8. L39
    exact hz_left_right_right_witness_witness_witness_witness_right_right_left
  9. L40
    exact hz_left_right_right_witness_witness_witness_witness_right_right_right_left
  10. L41
    exact hZ
06Separate the logical casesL42–45

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

  1. L42
    cases hz_left_right_right_witness_witness_witness_witness_right_right_right_right
  2. L43
    cases hz_left_right_right_witness_witness_witness_witness_right_right_right_right_witness
  3. L44
    cases hother
  4. L45
    cases hother_witness
07Establish hinnerL46–55

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

  1. L46
    have hinner : x4=x5
  2. L47
    specialize signed_mul_functional (x2)
  3. L48
    specialize signed_mul_functional (x3)
  4. L49
    specialize signed_mul_functional (x4)
  5. L50
    specialize signed_mul_functional (x5)
  6. L51
    apply signed_mul_functional
  7. L52
    exact hz_left_right_right_witness_witness_witness_witness_right_right_right_right_witness_left
  8. L53
    exact hother_witness_left
  9. L54
    rewrite hinner at hz_left_right_right_witness_witness_witness_witness_right_right_right_right_witness_right
  10. L55
    rewrite hinner at hz_left_right_right_witness_witness_witness_witness_right_right_right_right_witness_right
08Use earlier factsL56–62

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

  1. L56
    specialize signed_mul_functional (x1)
  2. L57
    specialize signed_mul_functional (x5)
  3. L58
    specialize signed_mul_functional (z)
  4. L59
    specialize signed_mul_functional (Z)
  5. L60
    apply signed_mul_functional
  6. L61
    exact hz_left_right_right_witness_witness_witness_witness_right_right_right_right_witness_right
  7. L62
    exact hother_witness_right
09Separate the logical casesL63–63

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

  1. L63
    cases hz_right
10Calculate and transport equalitiesL64–64

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

  1. L64
    trans 0
11Use earlier factsL65–65

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

  1. L65
    exact hz_right_right
12Calculate and transport equalitiesL66–66

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

  1. L66
    symm
13Use earlier factsL67–76

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

  1. L67
    specialize dirichlet_grid_entry_omitted_value (F)
  2. L68
    specialize dirichlet_grid_entry_omitted_value (G)
  3. L69
    specialize dirichlet_grid_entry_omitted_value (H)
  4. L70
    specialize dirichlet_grid_entry_omitted_value (n)
  5. L71
    specialize dirichlet_grid_entry_omitted_value (a)
  6. L72
    specialize dirichlet_grid_entry_omitted_value (e)
  7. L73
    specialize dirichlet_grid_entry_omitted_value (Z)
  8. L74
    apply dirichlet_grid_entry_omitted_value
  9. L75
    exact hz_right_left
  10. L76
    exact hZ

Library-wide reading audit

Original defined command ledger · 76 lines
  1. 0001intro F
  2. 0002intro G
  3. 0003intro H
  4. 0004intro n
  5. 0005intro a
  6. 0006intro e
  7. 0007intro z
  8. 0008intro Z
  9. 0009intro hz
  10. 0010intro hZ
  11. 0011cases hz
  12. 0012cases hz_left
  13. 0013cases hz_left_right
  14. 0014cases hz_left_right_right
  15. 0015cases hz_left_right_right_witness
  16. 0016cases hz_left_right_right_witness_witness
  17. 0017cases hz_left_right_right_witness_witness_witness
  18. 0018cases hz_left_right_right_witness_witness_witness_witness
  19. 0019cases hz_left_right_right_witness_witness_witness_witness_right
  20. 0020cases hz_left_right_right_witness_witness_witness_witness_right_right
  21. 0021cases hz_left_right_right_witness_witness_witness_witness_right_right_right
  22. 0022have hother : ∃ dfg_inner_unique_other. SignedMul(x2,x3,dfg_inner_unique_other) ∧ SignedMul(x1,dfg_inner_unique_other,Z)
  23. 0023specialize dirichlet_grid_entry_factor_product (F)
  24. 0024specialize dirichlet_grid_entry_factor_product (G)
  25. 0025specialize dirichlet_grid_entry_factor_product (H)
  26. 0026specialize dirichlet_grid_entry_factor_product (n)
  27. 0027specialize dirichlet_grid_entry_factor_product (a)
  28. 0028specialize dirichlet_grid_entry_factor_product (e)
  29. 0029specialize dirichlet_grid_entry_factor_product (x)
  30. 0030specialize dirichlet_grid_entry_factor_product (x1)
  31. 0031specialize dirichlet_grid_entry_factor_product (x2)
  32. 0032specialize dirichlet_grid_entry_factor_product (x3)
  33. 0033specialize dirichlet_grid_entry_factor_product (Z)
  34. 0034apply dirichlet_grid_entry_factor_product
  35. 0035exact hz_left_left
  36. 0036exact hz_left_right_left
  37. 0037exact hz_left_right_right_witness_witness_witness_witness_left
  38. 0038exact hz_left_right_right_witness_witness_witness_witness_right_left
  39. 0039exact hz_left_right_right_witness_witness_witness_witness_right_right_left
  40. 0040exact hz_left_right_right_witness_witness_witness_witness_right_right_right_left
  41. 0041exact hZ
  42. 0042cases hz_left_right_right_witness_witness_witness_witness_right_right_right_right
  43. 0043cases hz_left_right_right_witness_witness_witness_witness_right_right_right_right_witness
  44. 0044cases hother
  45. 0045cases hother_witness
  46. 0046have hinner : x4=x5
  47. 0047specialize signed_mul_functional (x2)
  48. 0048specialize signed_mul_functional (x3)
  49. 0049specialize signed_mul_functional (x4)
  50. 0050specialize signed_mul_functional (x5)
  51. 0051apply signed_mul_functional
  52. 0052exact hz_left_right_right_witness_witness_witness_witness_right_right_right_right_witness_left
  53. 0053exact hother_witness_left
  54. 0054rewrite hinner at hz_left_right_right_witness_witness_witness_witness_right_right_right_right_witness_right
  55. 0055rewrite hinner at hz_left_right_right_witness_witness_witness_witness_right_right_right_right_witness_right
  56. 0056specialize signed_mul_functional (x1)
  57. 0057specialize signed_mul_functional (x5)
  58. 0058specialize signed_mul_functional (z)
  59. 0059specialize signed_mul_functional (Z)
  60. 0060apply signed_mul_functional
  61. 0061exact hz_left_right_right_witness_witness_witness_witness_right_right_right_right_witness_right
  62. 0062exact hother_witness_right
  63. 0063cases hz_right
  64. 0064trans 0
  65. 0065exact hz_right_right
  66. 0066symm
  67. 0067specialize dirichlet_grid_entry_omitted_value (F)
  68. 0068specialize dirichlet_grid_entry_omitted_value (G)
  69. 0069specialize dirichlet_grid_entry_omitted_value (H)
  70. 0070specialize dirichlet_grid_entry_omitted_value (n)
  71. 0071specialize dirichlet_grid_entry_omitted_value (a)
  72. 0072specialize dirichlet_grid_entry_omitted_value (e)
  73. 0073specialize dirichlet_grid_entry_omitted_value (Z)
  74. 0074apply dirichlet_grid_entry_omitted_value
  75. 0075exact hz_right_left
  76. 0076exact hZ