DF0008

dirichlet_grid_flat_entry_exists

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

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. ∀ i. ArithTable(0,F) → ArithTable(0,G) → ArithTable(0,H) → ∃ x. DirichletFlatEntry(F,G,H,n,i,x)

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

Definition DAG

ArithTable(N,F) · 3DirichletGridEntry(F,G,H,n,a,e,z) · 1DirichletFlatEntry(F,G,H,n,i,z) · 1DivRem(n,d,q,r) · 1

Actual proof prerequisites

division_remainder_exists · checked external prerequisitesucc_ne_zero · checked external prerequisitedirichlet_grid_entry_exists
Original expanded first-order 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))))))))

Complete tactic proof in conservative notation

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

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (1)
dirichlet grid entry exists
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 : ∃ a. ∃ e. DivRem(i,S n,a,e)Definitions: DivRem(i,S n,a,e)Original native command in the exact edition
  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(F,G,H,n,x,x1,z)Original native command in the exact edition
  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 defined 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 : ∃ a. ∃ e. DivRem(i,S n,a,e)
  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 : ∃ z. DirichletGridEntry(F,G,H,n,x,x1,z)
  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