DF0008

dirichlet_grid_flat_entry_exists

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Actual division by S n decodes every flat index, then the genuinely constructed factor cell supplies its signed value.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Exact expanded first-order arithmetic statement

forall F G H n i. (exists dst_positive_code_flat_F dst_positive_scale_flat_F dst_negative_code_flat_F dst_negative_scale_flat_F. (((F) = (((((dst_positive_code_flat_F) + (dst_positive_scale_flat_F)) * S ((dst_positive_code_flat_F) + (dst_positive_scale_flat_F)) + ((dst_positive_scale_flat_F) + (dst_positive_scale_flat_F))) + (((dst_negative_code_flat_F) + (dst_negative_scale_flat_F)) * S ((dst_negative_code_flat_F) + (dst_negative_scale_flat_F)) + ((dst_negative_scale_flat_F) + (dst_negative_scale_flat_F)))) * S ((((dst_positive_code_flat_F) + (dst_positive_scale_flat_F)) * S ((dst_positive_code_flat_F) + (dst_positive_scale_flat_F)) + ((dst_positive_scale_flat_F) + (dst_positive_scale_flat_F))) + (((dst_negative_code_flat_F) + (dst_negative_scale_flat_F)) * S ((dst_negative_code_flat_F) + (dst_negative_scale_flat_F)) + ((dst_negative_scale_flat_F) + (dst_negative_scale_flat_F)))) + ((((dst_negative_code_flat_F) + (dst_negative_scale_flat_F)) * S ((dst_negative_code_flat_F) + (dst_negative_scale_flat_F)) + ((dst_negative_scale_flat_F) + (dst_negative_scale_flat_F))) + (((dst_negative_code_flat_F) + (dst_negative_scale_flat_F)) * S ((dst_negative_code_flat_F) + (dst_negative_scale_flat_F)) + ((dst_negative_scale_flat_F) + (dst_negative_scale_flat_F)))))) /\ (forall dst_index_flat_F. (exists pvs_le_gap_flat_Fdomain. pvs_le_gap_flat_Fdomain + (dst_index_flat_F) = (0)) -> exists dst_positive_flat_F dst_negative_flat_F dst_value_flat_F. ((((exists ff_h_pvs_flat_Fentrypositive. ff_h_pvs_flat_Fentrypositive + S (dst_positive_flat_F) = S ((S (dst_index_flat_F)) * dst_positive_scale_flat_F)) /\ exists ff_q_pvs_flat_Fentrypositive. dst_positive_code_flat_F = ff_q_pvs_flat_Fentrypositive * S ((S (dst_index_flat_F)) * dst_positive_scale_flat_F) + (dst_positive_flat_F))) /\ (((((exists ff_h_pvs_flat_Fentrynegative. ff_h_pvs_flat_Fentrynegative + S (dst_negative_flat_F) = S ((S (dst_index_flat_F)) * dst_negative_scale_flat_F)) /\ exists ff_q_pvs_flat_Fentrynegative. dst_negative_code_flat_F = ff_q_pvs_flat_Fentrynegative * S ((S (dst_index_flat_F)) * dst_negative_scale_flat_F) + (dst_negative_flat_F))) /\ (exists ge_balance_positive_flat_Fentryvalue ge_balance_negative_flat_Fentryvalue. (((((dst_value_flat_F) = 2 * (ge_balance_positive_flat_Fentryvalue) /\ (ge_balance_negative_flat_Fentryvalue) = 0) \/ exists ge_signed_half_flat_Fentryvaluedecode. (((dst_value_flat_F) = 2 * ge_signed_half_flat_Fentryvaluedecode + 1 /\ (ge_balance_positive_flat_Fentryvalue) = 0) /\ (ge_balance_negative_flat_Fentryvalue) = S ge_signed_half_flat_Fentryvaluedecode))) /\ ((dst_positive_flat_F) + ge_balance_negative_flat_Fentryvalue = (dst_negative_flat_F) + ge_balance_positive_flat_Fentryvalue))))))))) -> (exists dst_positive_code_flat_G dst_positive_scale_flat_G dst_negative_code_flat_G dst_negative_scale_flat_G. (((G) = (((((dst_positive_code_flat_G) + (dst_positive_scale_flat_G)) * S ((dst_positive_code_flat_G) + (dst_positive_scale_flat_G)) + ((dst_positive_scale_flat_G) + (dst_positive_scale_flat_G))) + (((dst_negative_code_flat_G) + (dst_negative_scale_flat_G)) * S ((dst_negative_code_flat_G) + (dst_negative_scale_flat_G)) + ((dst_negative_scale_flat_G) + (dst_negative_scale_flat_G)))) * S ((((dst_positive_code_flat_G) + (dst_positive_scale_flat_G)) * S ((dst_positive_code_flat_G) + (dst_positive_scale_flat_G)) + ((dst_positive_scale_flat_G) + (dst_positive_scale_flat_G))) + (((dst_negative_code_flat_G) + (dst_negative_scale_flat_G)) * S ((dst_negative_code_flat_G) + (dst_negative_scale_flat_G)) + ((dst_negative_scale_flat_G) + (dst_negative_scale_flat_G)))) + ((((dst_negative_code_flat_G) + (dst_negative_scale_flat_G)) * S ((dst_negative_code_flat_G) + (dst_negative_scale_flat_G)) + ((dst_negative_scale_flat_G) + (dst_negative_scale_flat_G))) + (((dst_negative_code_flat_G) + (dst_negative_scale_flat_G)) * S ((dst_negative_code_flat_G) + (dst_negative_scale_flat_G)) + ((dst_negative_scale_flat_G) + (dst_negative_scale_flat_G)))))) /\ (forall dst_index_flat_G. (exists pvs_le_gap_flat_Gdomain. pvs_le_gap_flat_Gdomain + (dst_index_flat_G) = (0)) -> exists dst_positive_flat_G dst_negative_flat_G dst_value_flat_G. ((((exists ff_h_pvs_flat_Gentrypositive. ff_h_pvs_flat_Gentrypositive + S (dst_positive_flat_G) = S ((S (dst_index_flat_G)) * dst_positive_scale_flat_G)) /\ exists ff_q_pvs_flat_Gentrypositive. dst_positive_code_flat_G = ff_q_pvs_flat_Gentrypositive * S ((S (dst_index_flat_G)) * dst_positive_scale_flat_G) + (dst_positive_flat_G))) /\ (((((exists ff_h_pvs_flat_Gentrynegative. ff_h_pvs_flat_Gentrynegative + S (dst_negative_flat_G) = S ((S (dst_index_flat_G)) * dst_negative_scale_flat_G)) /\ exists ff_q_pvs_flat_Gentrynegative. dst_negative_code_flat_G = ff_q_pvs_flat_Gentrynegative * S ((S (dst_index_flat_G)) * dst_negative_scale_flat_G) + (dst_negative_flat_G))) /\ (exists ge_balance_positive_flat_Gentryvalue ge_balance_negative_flat_Gentryvalue. (((((dst_value_flat_G) = 2 * (ge_balance_positive_flat_Gentryvalue) /\ (ge_balance_negative_flat_Gentryvalue) = 0) \/ exists ge_signed_half_flat_Gentryvaluedecode. (((dst_value_flat_G) = 2 * ge_signed_half_flat_Gentryvaluedecode + 1 /\ (ge_balance_positive_flat_Gentryvalue) = 0) /\ (ge_balance_negative_flat_Gentryvalue) = S ge_signed_half_flat_Gentryvaluedecode))) /\ ((dst_positive_flat_G) + ge_balance_negative_flat_Gentryvalue = (dst_negative_flat_G) + ge_balance_positive_flat_Gentryvalue))))))))) -> (exists dst_positive_code_flat_H dst_positive_scale_flat_H dst_negative_code_flat_H dst_negative_scale_flat_H. (((H) = (((((dst_positive_code_flat_H) + (dst_positive_scale_flat_H)) * S ((dst_positive_code_flat_H) + (dst_positive_scale_flat_H)) + ((dst_positive_scale_flat_H) + (dst_positive_scale_flat_H))) + (((dst_negative_code_flat_H) + (dst_negative_scale_flat_H)) * S ((dst_negative_code_flat_H) + (dst_negative_scale_flat_H)) + ((dst_negative_scale_flat_H) + (dst_negative_scale_flat_H)))) * S ((((dst_positive_code_flat_H) + (dst_positive_scale_flat_H)) * S ((dst_positive_code_flat_H) + (dst_positive_scale_flat_H)) + ((dst_positive_scale_flat_H) + (dst_positive_scale_flat_H))) + (((dst_negative_code_flat_H) + (dst_negative_scale_flat_H)) * S ((dst_negative_code_flat_H) + (dst_negative_scale_flat_H)) + ((dst_negative_scale_flat_H) + (dst_negative_scale_flat_H)))) + ((((dst_negative_code_flat_H) + (dst_negative_scale_flat_H)) * S ((dst_negative_code_flat_H) + (dst_negative_scale_flat_H)) + ((dst_negative_scale_flat_H) + (dst_negative_scale_flat_H))) + (((dst_negative_code_flat_H) + (dst_negative_scale_flat_H)) * S ((dst_negative_code_flat_H) + (dst_negative_scale_flat_H)) + ((dst_negative_scale_flat_H) + (dst_negative_scale_flat_H)))))) /\ (forall dst_index_flat_H. (exists pvs_le_gap_flat_Hdomain. pvs_le_gap_flat_Hdomain + (dst_index_flat_H) = (0)) -> exists dst_positive_flat_H dst_negative_flat_H dst_value_flat_H. ((((exists ff_h_pvs_flat_Hentrypositive. ff_h_pvs_flat_Hentrypositive + S (dst_positive_flat_H) = S ((S (dst_index_flat_H)) * dst_positive_scale_flat_H)) /\ exists ff_q_pvs_flat_Hentrypositive. dst_positive_code_flat_H = ff_q_pvs_flat_Hentrypositive * S ((S (dst_index_flat_H)) * dst_positive_scale_flat_H) + (dst_positive_flat_H))) /\ (((((exists ff_h_pvs_flat_Hentrynegative. ff_h_pvs_flat_Hentrynegative + S (dst_negative_flat_H) = S ((S (dst_index_flat_H)) * dst_negative_scale_flat_H)) /\ exists ff_q_pvs_flat_Hentrynegative. dst_negative_code_flat_H = ff_q_pvs_flat_Hentrynegative * S ((S (dst_index_flat_H)) * dst_negative_scale_flat_H) + (dst_negative_flat_H))) /\ (exists ge_balance_positive_flat_Hentryvalue ge_balance_negative_flat_Hentryvalue. (((((dst_value_flat_H) = 2 * (ge_balance_positive_flat_Hentryvalue) /\ (ge_balance_negative_flat_Hentryvalue) = 0) \/ exists ge_signed_half_flat_Hentryvaluedecode. (((dst_value_flat_H) = 2 * ge_signed_half_flat_Hentryvaluedecode + 1 /\ (ge_balance_positive_flat_Hentryvalue) = 0) /\ (ge_balance_negative_flat_Hentryvalue) = S ge_signed_half_flat_Hentryvaluedecode))) /\ ((dst_positive_flat_H) + ge_balance_negative_flat_Hentryvalue = (dst_negative_flat_H) + ge_balance_positive_flat_Hentryvalue))))))))) -> exists z. (exists dfg_flat_row_flat_total dfg_flat_column_flat_total. (((i)=((S (n))*(dfg_flat_row_flat_total)+(dfg_flat_column_flat_total))) /\ (((exists pvs_gap_flat_totalremainder. pvs_gap_flat_totalremainder + S (dfg_flat_column_flat_total) = (S (n))) /\ ((((~((dfg_flat_row_flat_total)=0)) /\ (((~((dfg_flat_column_flat_total)=0)) /\ (exists dfg_middle_flat_totalcell dfg_first_flat_totalcell dfg_last_flat_totalcell dfg_value_flat_totalcell. (((n)=((dfg_flat_row_flat_total)*(dfg_flat_column_flat_total))*dfg_middle_flat_totalcell) /\ (((exists dst_positive_code_flat_totalcellfirst dst_positive_scale_flat_totalcellfirst dst_negative_code_flat_totalcellfirst dst_negative_scale_flat_totalcellfirst dst_positive_flat_totalcellfirst dst_negative_flat_totalcellfirst. (((F) = (((((dst_positive_code_flat_totalcellfirst) + (dst_positive_scale_flat_totalcellfirst)) * S ((dst_positive_code_flat_totalcellfirst) + (dst_positive_scale_flat_totalcellfirst)) + ((dst_positive_scale_flat_totalcellfirst) + (dst_positive_scale_flat_totalcellfirst))) + (((dst_negative_code_flat_totalcellfirst) + (dst_negative_scale_flat_totalcellfirst)) * S ((dst_negative_code_flat_totalcellfirst) + (dst_negative_scale_flat_totalcellfirst)) + ((dst_negative_scale_flat_totalcellfirst) + (dst_negative_scale_flat_totalcellfirst)))) * S ((((dst_positive_code_flat_totalcellfirst) + (dst_positive_scale_flat_totalcellfirst)) * S ((dst_positive_code_flat_totalcellfirst) + (dst_positive_scale_flat_totalcellfirst)) + ((dst_positive_scale_flat_totalcellfirst) + (dst_positive_scale_flat_totalcellfirst))) + (((dst_negative_code_flat_totalcellfirst) + (dst_negative_scale_flat_totalcellfirst)) * S ((dst_negative_code_flat_totalcellfirst) + (dst_negative_scale_flat_totalcellfirst)) + ((dst_negative_scale_flat_totalcellfirst) + (dst_negative_scale_flat_totalcellfirst)))) + ((((dst_negative_code_flat_totalcellfirst) + (dst_negative_scale_flat_totalcellfirst)) * S ((dst_negative_code_flat_totalcellfirst) + (dst_negative_scale_flat_totalcellfirst)) + ((dst_negative_scale_flat_totalcellfirst) + (dst_negative_scale_flat_totalcellfirst))) + (((dst_negative_code_flat_totalcellfirst) + (dst_negative_scale_flat_totalcellfirst)) * S ((dst_negative_code_flat_totalcellfirst) + (dst_negative_scale_flat_totalcellfirst)) + ((dst_negative_scale_flat_totalcellfirst) + (dst_negative_scale_flat_totalcellfirst)))))) /\ (((((exists ff_h_pvs_flat_totalcellfirstpositive. ff_h_pvs_flat_totalcellfirstpositive + S (dst_positive_flat_totalcellfirst) = S ((S (dfg_flat_row_flat_total)) * dst_positive_scale_flat_totalcellfirst)) /\ exists ff_q_pvs_flat_totalcellfirstpositive. dst_positive_code_flat_totalcellfirst = ff_q_pvs_flat_totalcellfirstpositive * S ((S (dfg_flat_row_flat_total)) * dst_positive_scale_flat_totalcellfirst) + (dst_positive_flat_totalcellfirst))) /\ (((((exists ff_h_pvs_flat_totalcellfirstnegative. ff_h_pvs_flat_totalcellfirstnegative + S (dst_negative_flat_totalcellfirst) = S ((S (dfg_flat_row_flat_total)) * dst_negative_scale_flat_totalcellfirst)) /\ exists ff_q_pvs_flat_totalcellfirstnegative. dst_negative_code_flat_totalcellfirst = ff_q_pvs_flat_totalcellfirstnegative * S ((S (dfg_flat_row_flat_total)) * dst_negative_scale_flat_totalcellfirst) + (dst_negative_flat_totalcellfirst))) /\ (exists ge_balance_positive_flat_totalcellfirstvalue ge_balance_negative_flat_totalcellfirstvalue. (((((dfg_first_flat_totalcell) = 2 * (ge_balance_positive_flat_totalcellfirstvalue) /\ (ge_balance_negative_flat_totalcellfirstvalue) = 0) \/ exists ge_signed_half_flat_totalcellfirstvaluedecode. (((dfg_first_flat_totalcell) = 2 * ge_signed_half_flat_totalcellfirstvaluedecode + 1 /\ (ge_balance_positive_flat_totalcellfirstvalue) = 0) /\ (ge_balance_negative_flat_totalcellfirstvalue) = S ge_signed_half_flat_totalcellfirstvaluedecode))) /\ ((dst_positive_flat_totalcellfirst) + ge_balance_negative_flat_totalcellfirstvalue = (dst_negative_flat_totalcellfirst) + ge_balance_positive_flat_totalcellfirstvalue))))))))) /\ (((exists dst_positive_code_flat_totalcelllast dst_positive_scale_flat_totalcelllast dst_negative_code_flat_totalcelllast dst_negative_scale_flat_totalcelllast dst_positive_flat_totalcelllast dst_negative_flat_totalcelllast. (((H) = (((((dst_positive_code_flat_totalcelllast) + (dst_positive_scale_flat_totalcelllast)) * S ((dst_positive_code_flat_totalcelllast) + (dst_positive_scale_flat_totalcelllast)) + ((dst_positive_scale_flat_totalcelllast) + (dst_positive_scale_flat_totalcelllast))) + (((dst_negative_code_flat_totalcelllast) + (dst_negative_scale_flat_totalcelllast)) * S ((dst_negative_code_flat_totalcelllast) + (dst_negative_scale_flat_totalcelllast)) + ((dst_negative_scale_flat_totalcelllast) + (dst_negative_scale_flat_totalcelllast)))) * S ((((dst_positive_code_flat_totalcelllast) + (dst_positive_scale_flat_totalcelllast)) * S ((dst_positive_code_flat_totalcelllast) + (dst_positive_scale_flat_totalcelllast)) + ((dst_positive_scale_flat_totalcelllast) + (dst_positive_scale_flat_totalcelllast))) + (((dst_negative_code_flat_totalcelllast) + (dst_negative_scale_flat_totalcelllast)) * S ((dst_negative_code_flat_totalcelllast) + (dst_negative_scale_flat_totalcelllast)) + ((dst_negative_scale_flat_totalcelllast) + (dst_negative_scale_flat_totalcelllast)))) + ((((dst_negative_code_flat_totalcelllast) + (dst_negative_scale_flat_totalcelllast)) * S ((dst_negative_code_flat_totalcelllast) + (dst_negative_scale_flat_totalcelllast)) + ((dst_negative_scale_flat_totalcelllast) + (dst_negative_scale_flat_totalcelllast))) + (((dst_negative_code_flat_totalcelllast) + (dst_negative_scale_flat_totalcelllast)) * S ((dst_negative_code_flat_totalcelllast) + (dst_negative_scale_flat_totalcelllast)) + ((dst_negative_scale_flat_totalcelllast) + (dst_negative_scale_flat_totalcelllast)))))) /\ (((((exists ff_h_pvs_flat_totalcelllastpositive. ff_h_pvs_flat_totalcelllastpositive + S (dst_positive_flat_totalcelllast) = S ((S (dfg_flat_column_flat_total)) * dst_positive_scale_flat_totalcelllast)) /\ exists ff_q_pvs_flat_totalcelllastpositive. dst_positive_code_flat_totalcelllast = ff_q_pvs_flat_totalcelllastpositive * S ((S (dfg_flat_column_flat_total)) * dst_positive_scale_flat_totalcelllast) + (dst_positive_flat_totalcelllast))) /\ (((((exists ff_h_pvs_flat_totalcelllastnegative. ff_h_pvs_flat_totalcelllastnegative + S (dst_negative_flat_totalcelllast) = S ((S (dfg_flat_column_flat_total)) * dst_negative_scale_flat_totalcelllast)) /\ exists ff_q_pvs_flat_totalcelllastnegative. dst_negative_code_flat_totalcelllast = ff_q_pvs_flat_totalcelllastnegative * S ((S (dfg_flat_column_flat_total)) * dst_negative_scale_flat_totalcelllast) + (dst_negative_flat_totalcelllast))) /\ (exists ge_balance_positive_flat_totalcelllastvalue ge_balance_negative_flat_totalcelllastvalue. (((((dfg_last_flat_totalcell) = 2 * (ge_balance_positive_flat_totalcelllastvalue) /\ (ge_balance_negative_flat_totalcelllastvalue) = 0) \/ exists ge_signed_half_flat_totalcelllastvaluedecode. (((dfg_last_flat_totalcell) = 2 * ge_signed_half_flat_totalcelllastvaluedecode + 1 /\ (ge_balance_positive_flat_totalcelllastvalue) = 0) /\ (ge_balance_negative_flat_totalcelllastvalue) = S ge_signed_half_flat_totalcelllastvaluedecode))) /\ ((dst_positive_flat_totalcelllast) + ge_balance_negative_flat_totalcelllastvalue = (dst_negative_flat_totalcelllast) + ge_balance_positive_flat_totalcelllastvalue))))))))) /\ (((exists dst_positive_code_flat_totalcellmiddle dst_positive_scale_flat_totalcellmiddle dst_negative_code_flat_totalcellmiddle dst_negative_scale_flat_totalcellmiddle dst_positive_flat_totalcellmiddle dst_negative_flat_totalcellmiddle. (((G) = (((((dst_positive_code_flat_totalcellmiddle) + (dst_positive_scale_flat_totalcellmiddle)) * S ((dst_positive_code_flat_totalcellmiddle) + (dst_positive_scale_flat_totalcellmiddle)) + ((dst_positive_scale_flat_totalcellmiddle) + (dst_positive_scale_flat_totalcellmiddle))) + (((dst_negative_code_flat_totalcellmiddle) + (dst_negative_scale_flat_totalcellmiddle)) * S ((dst_negative_code_flat_totalcellmiddle) + (dst_negative_scale_flat_totalcellmiddle)) + ((dst_negative_scale_flat_totalcellmiddle) + (dst_negative_scale_flat_totalcellmiddle)))) * S ((((dst_positive_code_flat_totalcellmiddle) + (dst_positive_scale_flat_totalcellmiddle)) * S ((dst_positive_code_flat_totalcellmiddle) + (dst_positive_scale_flat_totalcellmiddle)) + ((dst_positive_scale_flat_totalcellmiddle) + (dst_positive_scale_flat_totalcellmiddle))) + (((dst_negative_code_flat_totalcellmiddle) + (dst_negative_scale_flat_totalcellmiddle)) * S ((dst_negative_code_flat_totalcellmiddle) + (dst_negative_scale_flat_totalcellmiddle)) + ((dst_negative_scale_flat_totalcellmiddle) + (dst_negative_scale_flat_totalcellmiddle)))) + ((((dst_negative_code_flat_totalcellmiddle) + (dst_negative_scale_flat_totalcellmiddle)) * S ((dst_negative_code_flat_totalcellmiddle) + (dst_negative_scale_flat_totalcellmiddle)) + ((dst_negative_scale_flat_totalcellmiddle) + (dst_negative_scale_flat_totalcellmiddle))) + (((dst_negative_code_flat_totalcellmiddle) + (dst_negative_scale_flat_totalcellmiddle)) * S ((dst_negative_code_flat_totalcellmiddle) + (dst_negative_scale_flat_totalcellmiddle)) + ((dst_negative_scale_flat_totalcellmiddle) + (dst_negative_scale_flat_totalcellmiddle)))))) /\ (((((exists ff_h_pvs_flat_totalcellmiddlepositive. ff_h_pvs_flat_totalcellmiddlepositive + S (dst_positive_flat_totalcellmiddle) = S ((S (dfg_middle_flat_totalcell)) * dst_positive_scale_flat_totalcellmiddle)) /\ exists ff_q_pvs_flat_totalcellmiddlepositive. dst_positive_code_flat_totalcellmiddle = ff_q_pvs_flat_totalcellmiddlepositive * S ((S (dfg_middle_flat_totalcell)) * dst_positive_scale_flat_totalcellmiddle) + (dst_positive_flat_totalcellmiddle))) /\ (((((exists ff_h_pvs_flat_totalcellmiddlenegative. ff_h_pvs_flat_totalcellmiddlenegative + S (dst_negative_flat_totalcellmiddle) = S ((S (dfg_middle_flat_totalcell)) * dst_negative_scale_flat_totalcellmiddle)) /\ exists ff_q_pvs_flat_totalcellmiddlenegative. dst_negative_code_flat_totalcellmiddle = ff_q_pvs_flat_totalcellmiddlenegative * S ((S (dfg_middle_flat_totalcell)) * dst_negative_scale_flat_totalcellmiddle) + (dst_negative_flat_totalcellmiddle))) /\ (exists ge_balance_positive_flat_totalcellmiddlevalue ge_balance_negative_flat_totalcellmiddlevalue. (((((dfg_value_flat_totalcell) = 2 * (ge_balance_positive_flat_totalcellmiddlevalue) /\ (ge_balance_negative_flat_totalcellmiddlevalue) = 0) \/ exists ge_signed_half_flat_totalcellmiddlevaluedecode. (((dfg_value_flat_totalcell) = 2 * ge_signed_half_flat_totalcellmiddlevaluedecode + 1 /\ (ge_balance_positive_flat_totalcellmiddlevalue) = 0) /\ (ge_balance_negative_flat_totalcellmiddlevalue) = S ge_signed_half_flat_totalcellmiddlevaluedecode))) /\ ((dst_positive_flat_totalcellmiddle) + ge_balance_negative_flat_totalcellmiddlevalue = (dst_negative_flat_totalcellmiddle) + ge_balance_positive_flat_totalcellmiddlevalue))))))))) /\ (exists dfg_inner_flat_totalcellproduct. ((exists sto_ap_flat_totalcellproductinner sto_an_flat_totalcellproductinner sto_bp_flat_totalcellproductinner sto_bn_flat_totalcellproductinner sto_cp_flat_totalcellproductinner sto_cn_flat_totalcellproductinner. (((((dfg_last_flat_totalcell) = 2 * (sto_ap_flat_totalcellproductinner) /\ (sto_an_flat_totalcellproductinner) = 0) \/ exists ge_signed_half_flat_totalcellproductinnerleft. (((dfg_last_flat_totalcell) = 2 * ge_signed_half_flat_totalcellproductinnerleft + 1 /\ (sto_ap_flat_totalcellproductinner) = 0) /\ (sto_an_flat_totalcellproductinner) = S ge_signed_half_flat_totalcellproductinnerleft))) /\ ((((((dfg_value_flat_totalcell) = 2 * (sto_bp_flat_totalcellproductinner) /\ (sto_bn_flat_totalcellproductinner) = 0) \/ exists ge_signed_half_flat_totalcellproductinnerright. (((dfg_value_flat_totalcell) = 2 * ge_signed_half_flat_totalcellproductinnerright + 1 /\ (sto_bp_flat_totalcellproductinner) = 0) /\ (sto_bn_flat_totalcellproductinner) = S ge_signed_half_flat_totalcellproductinnerright))) /\ ((((((dfg_inner_flat_totalcellproduct) = 2 * (sto_cp_flat_totalcellproductinner) /\ (sto_cn_flat_totalcellproductinner) = 0) \/ exists ge_signed_half_flat_totalcellproductinneroutput. (((dfg_inner_flat_totalcellproduct) = 2 * ge_signed_half_flat_totalcellproductinneroutput + 1 /\ (sto_cp_flat_totalcellproductinner) = 0) /\ (sto_cn_flat_totalcellproductinner) = S ge_signed_half_flat_totalcellproductinneroutput))) /\ ((sto_ap_flat_totalcellproductinner * sto_bp_flat_totalcellproductinner + sto_an_flat_totalcellproductinner * sto_bn_flat_totalcellproductinner) + sto_cn_flat_totalcellproductinner = (sto_ap_flat_totalcellproductinner * sto_bn_flat_totalcellproductinner + sto_an_flat_totalcellproductinner * sto_bp_flat_totalcellproductinner) + sto_cp_flat_totalcellproductinner))))))) /\ (exists sto_ap_flat_totalcellproductouter sto_an_flat_totalcellproductouter sto_bp_flat_totalcellproductouter sto_bn_flat_totalcellproductouter sto_cp_flat_totalcellproductouter sto_cn_flat_totalcellproductouter. (((((dfg_first_flat_totalcell) = 2 * (sto_ap_flat_totalcellproductouter) /\ (sto_an_flat_totalcellproductouter) = 0) \/ exists ge_signed_half_flat_totalcellproductouterleft. (((dfg_first_flat_totalcell) = 2 * ge_signed_half_flat_totalcellproductouterleft + 1 /\ (sto_ap_flat_totalcellproductouter) = 0) /\ (sto_an_flat_totalcellproductouter) = S ge_signed_half_flat_totalcellproductouterleft))) /\ ((((((dfg_inner_flat_totalcellproduct) = 2 * (sto_bp_flat_totalcellproductouter) /\ (sto_bn_flat_totalcellproductouter) = 0) \/ exists ge_signed_half_flat_totalcellproductouterright. (((dfg_inner_flat_totalcellproduct) = 2 * ge_signed_half_flat_totalcellproductouterright + 1 /\ (sto_bp_flat_totalcellproductouter) = 0) /\ (sto_bn_flat_totalcellproductouter) = S ge_signed_half_flat_totalcellproductouterright))) /\ ((((((z) = 2 * (sto_cp_flat_totalcellproductouter) /\ (sto_cn_flat_totalcellproductouter) = 0) \/ exists ge_signed_half_flat_totalcellproductouteroutput. (((z) = 2 * ge_signed_half_flat_totalcellproductouteroutput + 1 /\ (sto_cp_flat_totalcellproductouter) = 0) /\ (sto_cn_flat_totalcellproductouter) = S ge_signed_half_flat_totalcellproductouteroutput))) /\ ((sto_ap_flat_totalcellproductouter * sto_bp_flat_totalcellproductouter + sto_an_flat_totalcellproductouter * sto_bn_flat_totalcellproductouter) + sto_cn_flat_totalcellproductouter = (sto_ap_flat_totalcellproductouter * sto_bn_flat_totalcellproductouter + sto_an_flat_totalcellproductouter * sto_bp_flat_totalcellproductouter) + sto_cp_flat_totalcellproductouter))))))))))))))))))))) \/ ((((dfg_flat_row_flat_total)=0 \/ ((dfg_flat_column_flat_total)=0 \/ ~(exists pvs_factor_flat_totalcellomittednondivisor. (n) = ((dfg_flat_row_flat_total)*(dfg_flat_column_flat_total)) * pvs_factor_flat_totalcellomittednondivisor))) /\ ((z)=0))))))))

Constructive proof overview

Generated structural guide

Actual division by S n decodes every flat index, then the genuinely constructed factor cell supplies its signed value.

The unchanged tactic script uses 3 declared prerequisites and contains 37 exact native proof lines.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

division_remainder_exists Stable theorem; checked-use authorized succ_ne_zero Stable theorem; checked-use authorized DF0006 dirichlet_grid_entry_exists

Direct dependents

DF000C dirichlet_grid_flat_prefix_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

37 script commands · 11 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.

Named ingredients (1)
dirichlet grid entry exists

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–8

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 i
  6. L6
    intro hF
  7. L7
    intro hG
  8. L8
    intro hH
02Establish hdL9–14

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply division remainder exists.

  1. L9
    have hd : exists a e. ((i=(S n)*a+e) /\ (exists pvs_gap_flat_division. pvs_gap_flat_division + S (e) = (S n)))
  2. L10
    specialize division_remainder_exists (S n)
  3. L11
    specialize division_remainder_exists (i)
  4. L12
    apply division_remainder_exists
  5. L13
    specialize succ_ne_zero (n)
  6. L14
    apply succ_ne_zero
03Separate the logical casesL15–17

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

  1. L15
    cases hd
  2. L16
    cases hd_witness
  3. L17
    cases hd_witness_witness
04Establish hvL18–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet grid entry exists.

  1. L18
    have hv : ∃ z. DirichletGridEntry(F,G,H,n,x,x1,z)Definitions: DirichletGridEntry
  2. L19
    specialize dirichlet_grid_entry_exists (F)
  3. L20
    specialize dirichlet_grid_entry_exists (G)
  4. L21
    specialize dirichlet_grid_entry_exists (H)
  5. L22
    specialize dirichlet_grid_entry_exists (n)
  6. L23
    specialize dirichlet_grid_entry_exists (x)
  7. L24
    specialize dirichlet_grid_entry_exists (x1)
  8. L25
    apply dirichlet_grid_entry_exists
  9. L26
    exact hF
  10. L27
    exact hG
05Use earlier factsL28–28

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

  1. L28
    exact hH
06Separate the logical casesL29–29

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

  1. L29
    cases hv
07Construct an explicit witnessL30–32

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

  1. L30
    exists x2
  2. L31
    exists x
  3. L32
    exists x1
08Separate the logical casesL33–33

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

  1. L33
    split
09Use earlier factsL34–34

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

  1. L34
    exact hd_witness_witness_left
10Separate the logical casesL35–35

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

  1. L35
    split
11Use earlier factsL36–37

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

  1. L36
    exact hd_witness_witness_right
  2. L37
    exact hv_witness

Library-wide reading audit

Original exact command ledger · 37 lines
  1. 0001intro F
  2. 0002intro G
  3. 0003intro H
  4. 0004intro n
  5. 0005intro i
  6. 0006intro hF
  7. 0007intro hG
  8. 0008intro hH
  9. 0009have hd : exists a e. ((i=(S n)*a+e) /\ (exists pvs_gap_flat_division. pvs_gap_flat_division + S (e) = (S n)))
  10. 0010specialize division_remainder_exists (S n)
  11. 0011specialize division_remainder_exists (i)
  12. 0012apply division_remainder_exists
  13. 0013specialize succ_ne_zero (n)
  14. 0014apply succ_ne_zero
  15. 0015cases hd
  16. 0016cases hd_witness
  17. 0017cases hd_witness_witness
  18. 0018have hv : exists z. ((((~((x)=0)) /\ (((~((x1)=0)) /\ (exists dfg_middle_flat_value dfg_first_flat_value dfg_last_flat_value dfg_value_flat_value. (((n)=((x)*(x1))*dfg_middle_flat_value) /\ (((exists dst_positive_code_flat_valuefirst dst_positive_scale_flat_valuefirst dst_negative_code_flat_valuefirst dst_negative_scale_flat_valuefirst dst_positive_flat_valuefirst dst_negative_flat_valuefirst. (((F) = (((((dst_positive_code_flat_valuefirst) + (dst_positive_scale_flat_valuefirst)) * S ((dst_positive_code_flat_valuefirst) + (dst_positive_scale_flat_valuefirst)) + ((dst_positive_scale_flat_valuefirst) + (dst_positive_scale_flat_valuefirst))) + (((dst_negative_code_flat_valuefirst) + (dst_negative_scale_flat_valuefirst)) * S ((dst_negative_code_flat_valuefirst) + (dst_negative_scale_flat_valuefirst)) + ((dst_negative_scale_flat_valuefirst) + (dst_negative_scale_flat_valuefirst)))) * S ((((dst_positive_code_flat_valuefirst) + (dst_positive_scale_flat_valuefirst)) * S ((dst_positive_code_flat_valuefirst) + (dst_positive_scale_flat_valuefirst)) + ((dst_positive_scale_flat_valuefirst) + (dst_positive_scale_flat_valuefirst))) + (((dst_negative_code_flat_valuefirst) + (dst_negative_scale_flat_valuefirst)) * S ((dst_negative_code_flat_valuefirst) + (dst_negative_scale_flat_valuefirst)) + ((dst_negative_scale_flat_valuefirst) + (dst_negative_scale_flat_valuefirst)))) + ((((dst_negative_code_flat_valuefirst) + (dst_negative_scale_flat_valuefirst)) * S ((dst_negative_code_flat_valuefirst) + (dst_negative_scale_flat_valuefirst)) + ((dst_negative_scale_flat_valuefirst) + (dst_negative_scale_flat_valuefirst))) + (((dst_negative_code_flat_valuefirst) + (dst_negative_scale_flat_valuefirst)) * S ((dst_negative_code_flat_valuefirst) + (dst_negative_scale_flat_valuefirst)) + ((dst_negative_scale_flat_valuefirst) + (dst_negative_scale_flat_valuefirst)))))) /\ (((((exists ff_h_pvs_flat_valuefirstpositive. ff_h_pvs_flat_valuefirstpositive + S (dst_positive_flat_valuefirst) = S ((S (x)) * dst_positive_scale_flat_valuefirst)) /\ exists ff_q_pvs_flat_valuefirstpositive. dst_positive_code_flat_valuefirst = ff_q_pvs_flat_valuefirstpositive * S ((S (x)) * dst_positive_scale_flat_valuefirst) + (dst_positive_flat_valuefirst))) /\ (((((exists ff_h_pvs_flat_valuefirstnegative. ff_h_pvs_flat_valuefirstnegative + S (dst_negative_flat_valuefirst) = S ((S (x)) * dst_negative_scale_flat_valuefirst)) /\ exists ff_q_pvs_flat_valuefirstnegative. dst_negative_code_flat_valuefirst = ff_q_pvs_flat_valuefirstnegative * S ((S (x)) * dst_negative_scale_flat_valuefirst) + (dst_negative_flat_valuefirst))) /\ (exists ge_balance_positive_flat_valuefirstvalue ge_balance_negative_flat_valuefirstvalue. (((((dfg_first_flat_value) = 2 * (ge_balance_positive_flat_valuefirstvalue) /\ (ge_balance_negative_flat_valuefirstvalue) = 0) \/ exists ge_signed_half_flat_valuefirstvaluedecode. (((dfg_first_flat_value) = 2 * ge_signed_half_flat_valuefirstvaluedecode + 1 /\ (ge_balance_positive_flat_valuefirstvalue) = 0) /\ (ge_balance_negative_flat_valuefirstvalue) = S ge_signed_half_flat_valuefirstvaluedecode))) /\ ((dst_positive_flat_valuefirst) + ge_balance_negative_flat_valuefirstvalue = (dst_negative_flat_valuefirst) + ge_balance_positive_flat_valuefirstvalue))))))))) /\ (((exists dst_positive_code_flat_valuelast dst_positive_scale_flat_valuelast dst_negative_code_flat_valuelast dst_negative_scale_flat_valuelast dst_positive_flat_valuelast dst_negative_flat_valuelast. (((H) = (((((dst_positive_code_flat_valuelast) + (dst_positive_scale_flat_valuelast)) * S ((dst_positive_code_flat_valuelast) + (dst_positive_scale_flat_valuelast)) + ((dst_positive_scale_flat_valuelast) + (dst_positive_scale_flat_valuelast))) + (((dst_negative_code_flat_valuelast) + (dst_negative_scale_flat_valuelast)) * S ((dst_negative_code_flat_valuelast) + (dst_negative_scale_flat_valuelast)) + ((dst_negative_scale_flat_valuelast) + (dst_negative_scale_flat_valuelast)))) * S ((((dst_positive_code_flat_valuelast) + (dst_positive_scale_flat_valuelast)) * S ((dst_positive_code_flat_valuelast) + (dst_positive_scale_flat_valuelast)) + ((dst_positive_scale_flat_valuelast) + (dst_positive_scale_flat_valuelast))) + (((dst_negative_code_flat_valuelast) + (dst_negative_scale_flat_valuelast)) * S ((dst_negative_code_flat_valuelast) + (dst_negative_scale_flat_valuelast)) + ((dst_negative_scale_flat_valuelast) + (dst_negative_scale_flat_valuelast)))) + ((((dst_negative_code_flat_valuelast) + (dst_negative_scale_flat_valuelast)) * S ((dst_negative_code_flat_valuelast) + (dst_negative_scale_flat_valuelast)) + ((dst_negative_scale_flat_valuelast) + (dst_negative_scale_flat_valuelast))) + (((dst_negative_code_flat_valuelast) + (dst_negative_scale_flat_valuelast)) * S ((dst_negative_code_flat_valuelast) + (dst_negative_scale_flat_valuelast)) + ((dst_negative_scale_flat_valuelast) + (dst_negative_scale_flat_valuelast)))))) /\ (((((exists ff_h_pvs_flat_valuelastpositive. ff_h_pvs_flat_valuelastpositive + S (dst_positive_flat_valuelast) = S ((S (x1)) * dst_positive_scale_flat_valuelast)) /\ exists ff_q_pvs_flat_valuelastpositive. dst_positive_code_flat_valuelast = ff_q_pvs_flat_valuelastpositive * S ((S (x1)) * dst_positive_scale_flat_valuelast) + (dst_positive_flat_valuelast))) /\ (((((exists ff_h_pvs_flat_valuelastnegative. ff_h_pvs_flat_valuelastnegative + S (dst_negative_flat_valuelast) = S ((S (x1)) * dst_negative_scale_flat_valuelast)) /\ exists ff_q_pvs_flat_valuelastnegative. dst_negative_code_flat_valuelast = ff_q_pvs_flat_valuelastnegative * S ((S (x1)) * dst_negative_scale_flat_valuelast) + (dst_negative_flat_valuelast))) /\ (exists ge_balance_positive_flat_valuelastvalue ge_balance_negative_flat_valuelastvalue. (((((dfg_last_flat_value) = 2 * (ge_balance_positive_flat_valuelastvalue) /\ (ge_balance_negative_flat_valuelastvalue) = 0) \/ exists ge_signed_half_flat_valuelastvaluedecode. (((dfg_last_flat_value) = 2 * ge_signed_half_flat_valuelastvaluedecode + 1 /\ (ge_balance_positive_flat_valuelastvalue) = 0) /\ (ge_balance_negative_flat_valuelastvalue) = S ge_signed_half_flat_valuelastvaluedecode))) /\ ((dst_positive_flat_valuelast) + ge_balance_negative_flat_valuelastvalue = (dst_negative_flat_valuelast) + ge_balance_positive_flat_valuelastvalue))))))))) /\ (((exists dst_positive_code_flat_valuemiddle dst_positive_scale_flat_valuemiddle dst_negative_code_flat_valuemiddle dst_negative_scale_flat_valuemiddle dst_positive_flat_valuemiddle dst_negative_flat_valuemiddle. (((G) = (((((dst_positive_code_flat_valuemiddle) + (dst_positive_scale_flat_valuemiddle)) * S ((dst_positive_code_flat_valuemiddle) + (dst_positive_scale_flat_valuemiddle)) + ((dst_positive_scale_flat_valuemiddle) + (dst_positive_scale_flat_valuemiddle))) + (((dst_negative_code_flat_valuemiddle) + (dst_negative_scale_flat_valuemiddle)) * S ((dst_negative_code_flat_valuemiddle) + (dst_negative_scale_flat_valuemiddle)) + ((dst_negative_scale_flat_valuemiddle) + (dst_negative_scale_flat_valuemiddle)))) * S ((((dst_positive_code_flat_valuemiddle) + (dst_positive_scale_flat_valuemiddle)) * S ((dst_positive_code_flat_valuemiddle) + (dst_positive_scale_flat_valuemiddle)) + ((dst_positive_scale_flat_valuemiddle) + (dst_positive_scale_flat_valuemiddle))) + (((dst_negative_code_flat_valuemiddle) + (dst_negative_scale_flat_valuemiddle)) * S ((dst_negative_code_flat_valuemiddle) + (dst_negative_scale_flat_valuemiddle)) + ((dst_negative_scale_flat_valuemiddle) + (dst_negative_scale_flat_valuemiddle)))) + ((((dst_negative_code_flat_valuemiddle) + (dst_negative_scale_flat_valuemiddle)) * S ((dst_negative_code_flat_valuemiddle) + (dst_negative_scale_flat_valuemiddle)) + ((dst_negative_scale_flat_valuemiddle) + (dst_negative_scale_flat_valuemiddle))) + (((dst_negative_code_flat_valuemiddle) + (dst_negative_scale_flat_valuemiddle)) * S ((dst_negative_code_flat_valuemiddle) + (dst_negative_scale_flat_valuemiddle)) + ((dst_negative_scale_flat_valuemiddle) + (dst_negative_scale_flat_valuemiddle)))))) /\ (((((exists ff_h_pvs_flat_valuemiddlepositive. ff_h_pvs_flat_valuemiddlepositive + S (dst_positive_flat_valuemiddle) = S ((S (dfg_middle_flat_value)) * dst_positive_scale_flat_valuemiddle)) /\ exists ff_q_pvs_flat_valuemiddlepositive. dst_positive_code_flat_valuemiddle = ff_q_pvs_flat_valuemiddlepositive * S ((S (dfg_middle_flat_value)) * dst_positive_scale_flat_valuemiddle) + (dst_positive_flat_valuemiddle))) /\ (((((exists ff_h_pvs_flat_valuemiddlenegative. ff_h_pvs_flat_valuemiddlenegative + S (dst_negative_flat_valuemiddle) = S ((S (dfg_middle_flat_value)) * dst_negative_scale_flat_valuemiddle)) /\ exists ff_q_pvs_flat_valuemiddlenegative. dst_negative_code_flat_valuemiddle = ff_q_pvs_flat_valuemiddlenegative * S ((S (dfg_middle_flat_value)) * dst_negative_scale_flat_valuemiddle) + (dst_negative_flat_valuemiddle))) /\ (exists ge_balance_positive_flat_valuemiddlevalue ge_balance_negative_flat_valuemiddlevalue. (((((dfg_value_flat_value) = 2 * (ge_balance_positive_flat_valuemiddlevalue) /\ (ge_balance_negative_flat_valuemiddlevalue) = 0) \/ exists ge_signed_half_flat_valuemiddlevaluedecode. (((dfg_value_flat_value) = 2 * ge_signed_half_flat_valuemiddlevaluedecode + 1 /\ (ge_balance_positive_flat_valuemiddlevalue) = 0) /\ (ge_balance_negative_flat_valuemiddlevalue) = S ge_signed_half_flat_valuemiddlevaluedecode))) /\ ((dst_positive_flat_valuemiddle) + ge_balance_negative_flat_valuemiddlevalue = (dst_negative_flat_valuemiddle) + ge_balance_positive_flat_valuemiddlevalue))))))))) /\ (exists dfg_inner_flat_valueproduct. ((exists sto_ap_flat_valueproductinner sto_an_flat_valueproductinner sto_bp_flat_valueproductinner sto_bn_flat_valueproductinner sto_cp_flat_valueproductinner sto_cn_flat_valueproductinner. (((((dfg_last_flat_value) = 2 * (sto_ap_flat_valueproductinner) /\ (sto_an_flat_valueproductinner) = 0) \/ exists ge_signed_half_flat_valueproductinnerleft. (((dfg_last_flat_value) = 2 * ge_signed_half_flat_valueproductinnerleft + 1 /\ (sto_ap_flat_valueproductinner) = 0) /\ (sto_an_flat_valueproductinner) = S ge_signed_half_flat_valueproductinnerleft))) /\ ((((((dfg_value_flat_value) = 2 * (sto_bp_flat_valueproductinner) /\ (sto_bn_flat_valueproductinner) = 0) \/ exists ge_signed_half_flat_valueproductinnerright. (((dfg_value_flat_value) = 2 * ge_signed_half_flat_valueproductinnerright + 1 /\ (sto_bp_flat_valueproductinner) = 0) /\ (sto_bn_flat_valueproductinner) = S ge_signed_half_flat_valueproductinnerright))) /\ ((((((dfg_inner_flat_valueproduct) = 2 * (sto_cp_flat_valueproductinner) /\ (sto_cn_flat_valueproductinner) = 0) \/ exists ge_signed_half_flat_valueproductinneroutput. (((dfg_inner_flat_valueproduct) = 2 * ge_signed_half_flat_valueproductinneroutput + 1 /\ (sto_cp_flat_valueproductinner) = 0) /\ (sto_cn_flat_valueproductinner) = S ge_signed_half_flat_valueproductinneroutput))) /\ ((sto_ap_flat_valueproductinner * sto_bp_flat_valueproductinner + sto_an_flat_valueproductinner * sto_bn_flat_valueproductinner) + sto_cn_flat_valueproductinner = (sto_ap_flat_valueproductinner * sto_bn_flat_valueproductinner + sto_an_flat_valueproductinner * sto_bp_flat_valueproductinner) + sto_cp_flat_valueproductinner))))))) /\ (exists sto_ap_flat_valueproductouter sto_an_flat_valueproductouter sto_bp_flat_valueproductouter sto_bn_flat_valueproductouter sto_cp_flat_valueproductouter sto_cn_flat_valueproductouter. (((((dfg_first_flat_value) = 2 * (sto_ap_flat_valueproductouter) /\ (sto_an_flat_valueproductouter) = 0) \/ exists ge_signed_half_flat_valueproductouterleft. (((dfg_first_flat_value) = 2 * ge_signed_half_flat_valueproductouterleft + 1 /\ (sto_ap_flat_valueproductouter) = 0) /\ (sto_an_flat_valueproductouter) = S ge_signed_half_flat_valueproductouterleft))) /\ ((((((dfg_inner_flat_valueproduct) = 2 * (sto_bp_flat_valueproductouter) /\ (sto_bn_flat_valueproductouter) = 0) \/ exists ge_signed_half_flat_valueproductouterright. (((dfg_inner_flat_valueproduct) = 2 * ge_signed_half_flat_valueproductouterright + 1 /\ (sto_bp_flat_valueproductouter) = 0) /\ (sto_bn_flat_valueproductouter) = S ge_signed_half_flat_valueproductouterright))) /\ ((((((z) = 2 * (sto_cp_flat_valueproductouter) /\ (sto_cn_flat_valueproductouter) = 0) \/ exists ge_signed_half_flat_valueproductouteroutput. (((z) = 2 * ge_signed_half_flat_valueproductouteroutput + 1 /\ (sto_cp_flat_valueproductouter) = 0) /\ (sto_cn_flat_valueproductouter) = S ge_signed_half_flat_valueproductouteroutput))) /\ ((sto_ap_flat_valueproductouter * sto_bp_flat_valueproductouter + sto_an_flat_valueproductouter * sto_bn_flat_valueproductouter) + sto_cn_flat_valueproductouter = (sto_ap_flat_valueproductouter * sto_bn_flat_valueproductouter + sto_an_flat_valueproductouter * sto_bp_flat_valueproductouter) + sto_cp_flat_valueproductouter))))))))))))))))))))) \/ ((((x)=0 \/ ((x1)=0 \/ ~(exists pvs_factor_flat_valueomittednondivisor. (n) = ((x)*(x1)) * pvs_factor_flat_valueomittednondivisor))) /\ ((z)=0))))
  19. 0019specialize dirichlet_grid_entry_exists (F)
  20. 0020specialize dirichlet_grid_entry_exists (G)
  21. 0021specialize dirichlet_grid_entry_exists (H)
  22. 0022specialize dirichlet_grid_entry_exists (n)
  23. 0023specialize dirichlet_grid_entry_exists (x)
  24. 0024specialize dirichlet_grid_entry_exists (x1)
  25. 0025apply dirichlet_grid_entry_exists
  26. 0026exact hF
  27. 0027exact hG
  28. 0028exact hH
  29. 0029cases hv
  30. 0030exists x2
  31. 0031exists x
  32. 0032exists x1
  33. 0033split
  34. 0034exact hd_witness_witness_left
  35. 0035split
  36. 0036exact hd_witness_witness_right
  37. 0037exact hv_witness