DirichletFlatEntry(F,G,H,n,i,z)

exists dfg_flat_row_dirichlet dfg_flat_column_dirichlet. ((((i))=((S ((n)))*(dfg_flat_row_dirichlet)+(dfg_flat_column_dirichlet))) /\ (((exists pvs_gap_dirichletremainder. pvs_gap_dirichletremainder + S (dfg_flat_column_dirichlet) = (S ((n)))) /\ ((((~((dfg_flat_row_dirichlet)=0)) /\ (((~((dfg_flat_column_dirichlet)=0)) /\ (exists dfg_middle_dirichletcell dfg_first_dirichletcell dfg_last_dirichletcell dfg_value_dirichletcell. ((((n))=((dfg_flat_row_dirichlet)*(dfg_flat_column_dirichlet))*dfg_middle_dirichletcell) /\ (((exists dst_positive_code_dirichletcellfirst dst_positive_scale_dirichletcellfirst dst_negative_code_dirichletcellfirst dst_negative_scale_dirichletcellfirst dst_positive_dirichletcellfirst dst_negative_dirichletcellfirst. ((((F)) = (((((dst_positive_code_dirichletcellfirst) + (dst_positive_scale_dirichletcellfirst)) * S ((dst_positive_code_dirichletcellfirst) + (dst_positive_scale_dirichletcellfirst)) + ((dst_positive_scale_dirichletcellfirst) + (dst_positive_scale_dirichletcellfirst))) + (((dst_negative_code_dirichletcellfirst) + (dst_negative_scale_dirichletcellfirst)) * S ((dst_negative_code_dirichletcellfirst) + (dst_negative_scale_dirichletcellfirst)) + ((dst_negative_scale_dirichletcellfirst) + (dst_negative_scale_dirichletcellfirst)))) * S ((((dst_positive_code_dirichletcellfirst) + (dst_positive_scale_dirichletcellfirst)) * S ((dst_positive_code_dirichletcellfirst) + (dst_positive_scale_dirichletcellfirst)) + ((dst_positive_scale_dirichletcellfirst) + (dst_positive_scale_dirichletcellfirst))) + (((dst_negative_code_dirichletcellfirst) + (dst_negative_scale_dirichletcellfirst)) * S ((dst_negative_code_dirichletcellfirst) + (dst_negative_scale_dirichletcellfirst)) + ((dst_negative_scale_dirichletcellfirst) + (dst_negative_scale_dirichletcellfirst)))) + ((((dst_negative_code_dirichletcellfirst) + (dst_negative_scale_dirichletcellfirst)) * S ((dst_negative_code_dirichletcellfirst) + (dst_negative_scale_dirichletcellfirst)) + ((dst_negative_scale_dirichletcellfirst) + (dst_negative_scale_dirichletcellfirst))) + (((dst_negative_code_dirichletcellfirst) + (dst_negative_scale_dirichletcellfirst)) * S ((dst_negative_code_dirichletcellfirst) + (dst_negative_scale_dirichletcellfirst)) + ((dst_negative_scale_dirichletcellfirst) + (dst_negative_scale_dirichletcellfirst)))))) /\ (((((exists ff_h_pvs_dirichletcellfirstpositive. ff_h_pvs_dirichletcellfirstpositive + S (dst_positive_dirichletcellfirst) = S ((S (dfg_flat_row_dirichlet)) * dst_positive_scale_dirichletcellfirst)) /\ exists ff_q_pvs_dirichletcellfirstpositive. dst_positive_code_dirichletcellfirst = ff_q_pvs_dirichletcellfirstpositive * S ((S (dfg_flat_row_dirichlet)) * dst_positive_scale_dirichletcellfirst) + (dst_positive_dirichletcellfirst))) /\ (((((exists ff_h_pvs_dirichletcellfirstnegative. ff_h_pvs_dirichletcellfirstnegative + S (dst_negative_dirichletcellfirst) = S ((S (dfg_flat_row_dirichlet)) * dst_negative_scale_dirichletcellfirst)) /\ exists ff_q_pvs_dirichletcellfirstnegative. dst_negative_code_dirichletcellfirst = ff_q_pvs_dirichletcellfirstnegative * S ((S (dfg_flat_row_dirichlet)) * dst_negative_scale_dirichletcellfirst) + (dst_negative_dirichletcellfirst))) /\ (exists ge_balance_positive_dirichletcellfirstvalue ge_balance_negative_dirichletcellfirstvalue. (((((dfg_first_dirichletcell) = 2 * (ge_balance_positive_dirichletcellfirstvalue) /\ (ge_balance_negative_dirichletcellfirstvalue) = 0) \/ exists ge_signed_half_dirichletcellfirstvaluedecode. (((dfg_first_dirichletcell) = 2 * ge_signed_half_dirichletcellfirstvaluedecode + 1 /\ (ge_balance_positive_dirichletcellfirstvalue) = 0) /\ (ge_balance_negative_dirichletcellfirstvalue) = S ge_signed_half_dirichletcellfirstvaluedecode))) /\ ((dst_positive_dirichletcellfirst) + ge_balance_negative_dirichletcellfirstvalue = (dst_negative_dirichletcellfirst) + ge_balance_positive_dirichletcellfirstvalue))))))))) /\ (((exists dst_positive_code_dirichletcelllast dst_positive_scale_dirichletcelllast dst_negative_code_dirichletcelllast dst_negative_scale_dirichletcelllast dst_positive_dirichletcelllast dst_negative_dirichletcelllast. ((((H)) = (((((dst_positive_code_dirichletcelllast) + (dst_positive_scale_dirichletcelllast)) * S ((dst_positive_code_dirichletcelllast) + (dst_positive_scale_dirichletcelllast)) + ((dst_positive_scale_dirichletcelllast) + (dst_positive_scale_dirichletcelllast))) + (((dst_negative_code_dirichletcelllast) + (dst_negative_scale_dirichletcelllast)) * S ((dst_negative_code_dirichletcelllast) + (dst_negative_scale_dirichletcelllast)) + ((dst_negative_scale_dirichletcelllast) + (dst_negative_scale_dirichletcelllast)))) * S ((((dst_positive_code_dirichletcelllast) + (dst_positive_scale_dirichletcelllast)) * S ((dst_positive_code_dirichletcelllast) + (dst_positive_scale_dirichletcelllast)) + ((dst_positive_scale_dirichletcelllast) + (dst_positive_scale_dirichletcelllast))) + (((dst_negative_code_dirichletcelllast) + (dst_negative_scale_dirichletcelllast)) * S ((dst_negative_code_dirichletcelllast) + (dst_negative_scale_dirichletcelllast)) + ((dst_negative_scale_dirichletcelllast) + (dst_negative_scale_dirichletcelllast)))) + ((((dst_negative_code_dirichletcelllast) + (dst_negative_scale_dirichletcelllast)) * S ((dst_negative_code_dirichletcelllast) + (dst_negative_scale_dirichletcelllast)) + ((dst_negative_scale_dirichletcelllast) + (dst_negative_scale_dirichletcelllast))) + (((dst_negative_code_dirichletcelllast) + (dst_negative_scale_dirichletcelllast)) * S ((dst_negative_code_dirichletcelllast) + (dst_negative_scale_dirichletcelllast)) + ((dst_negative_scale_dirichletcelllast) + (dst_negative_scale_dirichletcelllast)))))) /\ (((((exists ff_h_pvs_dirichletcelllastpositive. ff_h_pvs_dirichletcelllastpositive + S (dst_positive_dirichletcelllast) = S ((S (dfg_flat_column_dirichlet)) * dst_positive_scale_dirichletcelllast)) /\ exists ff_q_pvs_dirichletcelllastpositive. dst_positive_code_dirichletcelllast = ff_q_pvs_dirichletcelllastpositive * S ((S (dfg_flat_column_dirichlet)) * dst_positive_scale_dirichletcelllast) + (dst_positive_dirichletcelllast))) /\ (((((exists ff_h_pvs_dirichletcelllastnegative. ff_h_pvs_dirichletcelllastnegative + S (dst_negative_dirichletcelllast) = S ((S (dfg_flat_column_dirichlet)) * dst_negative_scale_dirichletcelllast)) /\ exists ff_q_pvs_dirichletcelllastnegative. dst_negative_code_dirichletcelllast = ff_q_pvs_dirichletcelllastnegative * S ((S (dfg_flat_column_dirichlet)) * dst_negative_scale_dirichletcelllast) + (dst_negative_dirichletcelllast))) /\ (exists ge_balance_positive_dirichletcelllastvalue ge_balance_negative_dirichletcelllastvalue. (((((dfg_last_dirichletcell) = 2 * (ge_balance_positive_dirichletcelllastvalue) /\ (ge_balance_negative_dirichletcelllastvalue) = 0) \/ exists ge_signed_half_dirichletcelllastvaluedecode. (((dfg_last_dirichletcell) = 2 * ge_signed_half_dirichletcelllastvaluedecode + 1 /\ (ge_balance_positive_dirichletcelllastvalue) = 0) /\ (ge_balance_negative_dirichletcelllastvalue) = S ge_signed_half_dirichletcelllastvaluedecode))) /\ ((dst_positive_dirichletcelllast) + ge_balance_negative_dirichletcelllastvalue = (dst_negative_dirichletcelllast) + ge_balance_positive_dirichletcelllastvalue))))))))) /\ (((exists dst_positive_code_dirichletcellmiddle dst_positive_scale_dirichletcellmiddle dst_negative_code_dirichletcellmiddle dst_negative_scale_dirichletcellmiddle dst_positive_dirichletcellmiddle dst_negative_dirichletcellmiddle. ((((G)) = (((((dst_positive_code_dirichletcellmiddle) + (dst_positive_scale_dirichletcellmiddle)) * S ((dst_positive_code_dirichletcellmiddle) + (dst_positive_scale_dirichletcellmiddle)) + ((dst_positive_scale_dirichletcellmiddle) + (dst_positive_scale_dirichletcellmiddle))) + (((dst_negative_code_dirichletcellmiddle) + (dst_negative_scale_dirichletcellmiddle)) * S ((dst_negative_code_dirichletcellmiddle) + (dst_negative_scale_dirichletcellmiddle)) + ((dst_negative_scale_dirichletcellmiddle) + (dst_negative_scale_dirichletcellmiddle)))) * S ((((dst_positive_code_dirichletcellmiddle) + (dst_positive_scale_dirichletcellmiddle)) * S ((dst_positive_code_dirichletcellmiddle) + (dst_positive_scale_dirichletcellmiddle)) + ((dst_positive_scale_dirichletcellmiddle) + (dst_positive_scale_dirichletcellmiddle))) + (((dst_negative_code_dirichletcellmiddle) + (dst_negative_scale_dirichletcellmiddle)) * S ((dst_negative_code_dirichletcellmiddle) + (dst_negative_scale_dirichletcellmiddle)) + ((dst_negative_scale_dirichletcellmiddle) + (dst_negative_scale_dirichletcellmiddle)))) + ((((dst_negative_code_dirichletcellmiddle) + (dst_negative_scale_dirichletcellmiddle)) * S ((dst_negative_code_dirichletcellmiddle) + (dst_negative_scale_dirichletcellmiddle)) + ((dst_negative_scale_dirichletcellmiddle) + (dst_negative_scale_dirichletcellmiddle))) + (((dst_negative_code_dirichletcellmiddle) + (dst_negative_scale_dirichletcellmiddle)) * S ((dst_negative_code_dirichletcellmiddle) + (dst_negative_scale_dirichletcellmiddle)) + ((dst_negative_scale_dirichletcellmiddle) + (dst_negative_scale_dirichletcellmiddle)))))) /\ (((((exists ff_h_pvs_dirichletcellmiddlepositive. ff_h_pvs_dirichletcellmiddlepositive + S (dst_positive_dirichletcellmiddle) = S ((S (dfg_middle_dirichletcell)) * dst_positive_scale_dirichletcellmiddle)) /\ exists ff_q_pvs_dirichletcellmiddlepositive. dst_positive_code_dirichletcellmiddle = ff_q_pvs_dirichletcellmiddlepositive * S ((S (dfg_middle_dirichletcell)) * dst_positive_scale_dirichletcellmiddle) + (dst_positive_dirichletcellmiddle))) /\ (((((exists ff_h_pvs_dirichletcellmiddlenegative. ff_h_pvs_dirichletcellmiddlenegative + S (dst_negative_dirichletcellmiddle) = S ((S (dfg_middle_dirichletcell)) * dst_negative_scale_dirichletcellmiddle)) /\ exists ff_q_pvs_dirichletcellmiddlenegative. dst_negative_code_dirichletcellmiddle = ff_q_pvs_dirichletcellmiddlenegative * S ((S (dfg_middle_dirichletcell)) * dst_negative_scale_dirichletcellmiddle) + (dst_negative_dirichletcellmiddle))) /\ (exists ge_balance_positive_dirichletcellmiddlevalue ge_balance_negative_dirichletcellmiddlevalue. (((((dfg_value_dirichletcell) = 2 * (ge_balance_positive_dirichletcellmiddlevalue) /\ (ge_balance_negative_dirichletcellmiddlevalue) = 0) \/ exists ge_signed_half_dirichletcellmiddlevaluedecode. (((dfg_value_dirichletcell) = 2 * ge_signed_half_dirichletcellmiddlevaluedecode + 1 /\ (ge_balance_positive_dirichletcellmiddlevalue) = 0) /\ (ge_balance_negative_dirichletcellmiddlevalue) = S ge_signed_half_dirichletcellmiddlevaluedecode))) /\ ((dst_positive_dirichletcellmiddle) + ge_balance_negative_dirichletcellmiddlevalue = (dst_negative_dirichletcellmiddle) + ge_balance_positive_dirichletcellmiddlevalue))))))))) /\ (exists dfg_inner_dirichletcellproduct. ((exists sto_ap_dirichletcellproductinner sto_an_dirichletcellproductinner sto_bp_dirichletcellproductinner sto_bn_dirichletcellproductinner sto_cp_dirichletcellproductinner sto_cn_dirichletcellproductinner. (((((dfg_last_dirichletcell) = 2 * (sto_ap_dirichletcellproductinner) /\ (sto_an_dirichletcellproductinner) = 0) \/ exists ge_signed_half_dirichletcellproductinnerleft. (((dfg_last_dirichletcell) = 2 * ge_signed_half_dirichletcellproductinnerleft + 1 /\ (sto_ap_dirichletcellproductinner) = 0) /\ (sto_an_dirichletcellproductinner) = S ge_signed_half_dirichletcellproductinnerleft))) /\ ((((((dfg_value_dirichletcell) = 2 * (sto_bp_dirichletcellproductinner) /\ (sto_bn_dirichletcellproductinner) = 0) \/ exists ge_signed_half_dirichletcellproductinnerright. (((dfg_value_dirichletcell) = 2 * ge_signed_half_dirichletcellproductinnerright + 1 /\ (sto_bp_dirichletcellproductinner) = 0) /\ (sto_bn_dirichletcellproductinner) = S ge_signed_half_dirichletcellproductinnerright))) /\ ((((((dfg_inner_dirichletcellproduct) = 2 * (sto_cp_dirichletcellproductinner) /\ (sto_cn_dirichletcellproductinner) = 0) \/ exists ge_signed_half_dirichletcellproductinneroutput. (((dfg_inner_dirichletcellproduct) = 2 * ge_signed_half_dirichletcellproductinneroutput + 1 /\ (sto_cp_dirichletcellproductinner) = 0) /\ (sto_cn_dirichletcellproductinner) = S ge_signed_half_dirichletcellproductinneroutput))) /\ ((sto_ap_dirichletcellproductinner * sto_bp_dirichletcellproductinner + sto_an_dirichletcellproductinner * sto_bn_dirichletcellproductinner) + sto_cn_dirichletcellproductinner = (sto_ap_dirichletcellproductinner * sto_bn_dirichletcellproductinner + sto_an_dirichletcellproductinner * sto_bp_dirichletcellproductinner) + sto_cp_dirichletcellproductinner))))))) /\ (exists sto_ap_dirichletcellproductouter sto_an_dirichletcellproductouter sto_bp_dirichletcellproductouter sto_bn_dirichletcellproductouter sto_cp_dirichletcellproductouter sto_cn_dirichletcellproductouter. (((((dfg_first_dirichletcell) = 2 * (sto_ap_dirichletcellproductouter) /\ (sto_an_dirichletcellproductouter) = 0) \/ exists ge_signed_half_dirichletcellproductouterleft. (((dfg_first_dirichletcell) = 2 * ge_signed_half_dirichletcellproductouterleft + 1 /\ (sto_ap_dirichletcellproductouter) = 0) /\ (sto_an_dirichletcellproductouter) = S ge_signed_half_dirichletcellproductouterleft))) /\ ((((((dfg_inner_dirichletcellproduct) = 2 * (sto_bp_dirichletcellproductouter) /\ (sto_bn_dirichletcellproductouter) = 0) \/ exists ge_signed_half_dirichletcellproductouterright. (((dfg_inner_dirichletcellproduct) = 2 * ge_signed_half_dirichletcellproductouterright + 1 /\ (sto_bp_dirichletcellproductouter) = 0) /\ (sto_bn_dirichletcellproductouter) = S ge_signed_half_dirichletcellproductouterright))) /\ (((((((z)) = 2 * (sto_cp_dirichletcellproductouter) /\ (sto_cn_dirichletcellproductouter) = 0) \/ exists ge_signed_half_dirichletcellproductouteroutput. ((((z)) = 2 * ge_signed_half_dirichletcellproductouteroutput + 1 /\ (sto_cp_dirichletcellproductouter) = 0) /\ (sto_cn_dirichletcellproductouter) = S ge_signed_half_dirichletcellproductouteroutput))) /\ ((sto_ap_dirichletcellproductouter * sto_bp_dirichletcellproductouter + sto_an_dirichletcellproductouter * sto_bn_dirichletcellproductouter) + sto_cn_dirichletcellproductouter = (sto_ap_dirichletcellproductouter * sto_bn_dirichletcellproductouter + sto_an_dirichletcellproductouter * sto_bp_dirichletcellproductouter) + sto_cp_dirichletcellproductouter))))))))))))))))))))) \/ ((((dfg_flat_row_dirichlet)=0 \/ ((dfg_flat_column_dirichlet)=0 \/ ~(exists pvs_factor_dirichletcellomittednondivisor. ((n)) = ((dfg_flat_row_dirichlet)*(dfg_flat_column_dirichlet)) * pvs_factor_dirichletcellomittednondivisor))) /\ (((z))=0)))))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.