DF000C

dirichlet_grid_flat_prefix_exists

Ordinary induction constructs each actual inclusive flat prefix, with an independently witnessed quotient, remainder and signed value at every extension.

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

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

Definition DAG

ArithTable(N,F) · 4ArithAt(F,i,z) · 3DirichletFlatEntry(F,G,H,n,i,z) · 2DirichletFlatPrefix(F,G,H,n,l,T) · 3Lt(a,b) · 1

Actual proof prerequisites

dirichlet_grid_flat_entry_existsarithmetic_signed_table_singleton · checked external prerequisitedirichlet_grid_flat_prefix_zerodirichlet_grid_flat_prefix_append
Original expanded first-order statement 
forall F G H n l. (exists dst_positive_code_prefix_F dst_positive_scale_prefix_F dst_negative_code_prefix_F dst_negative_scale_prefix_F. (((F) = (((((dst_positive_code_prefix_F) + (dst_positive_scale_prefix_F)) * S ((dst_positive_code_prefix_F) + (dst_positive_scale_prefix_F)) + ((dst_positive_scale_prefix_F) + (dst_positive_scale_prefix_F))) + (((dst_negative_code_prefix_F) + (dst_negative_scale_prefix_F)) * S ((dst_negative_code_prefix_F) + (dst_negative_scale_prefix_F)) + ((dst_negative_scale_prefix_F) + (dst_negative_scale_prefix_F)))) * S ((((dst_positive_code_prefix_F) + (dst_positive_scale_prefix_F)) * S ((dst_positive_code_prefix_F) + (dst_positive_scale_prefix_F)) + ((dst_positive_scale_prefix_F) + (dst_positive_scale_prefix_F))) + (((dst_negative_code_prefix_F) + (dst_negative_scale_prefix_F)) * S ((dst_negative_code_prefix_F) + (dst_negative_scale_prefix_F)) + ((dst_negative_scale_prefix_F) + (dst_negative_scale_prefix_F)))) + ((((dst_negative_code_prefix_F) + (dst_negative_scale_prefix_F)) * S ((dst_negative_code_prefix_F) + (dst_negative_scale_prefix_F)) + ((dst_negative_scale_prefix_F) + (dst_negative_scale_prefix_F))) + (((dst_negative_code_prefix_F) + (dst_negative_scale_prefix_F)) * S ((dst_negative_code_prefix_F) + (dst_negative_scale_prefix_F)) + ((dst_negative_scale_prefix_F) + (dst_negative_scale_prefix_F)))))) /\ (forall dst_index_prefix_F. (exists pvs_le_gap_prefix_Fdomain. pvs_le_gap_prefix_Fdomain + (dst_index_prefix_F) = (0)) -> exists dst_positive_prefix_F dst_negative_prefix_F dst_value_prefix_F. ((((exists ff_h_pvs_prefix_Fentrypositive. ff_h_pvs_prefix_Fentrypositive + S (dst_positive_prefix_F) = S ((S (dst_index_prefix_F)) * dst_positive_scale_prefix_F)) /\ exists ff_q_pvs_prefix_Fentrypositive. dst_positive_code_prefix_F = ff_q_pvs_prefix_Fentrypositive * S ((S (dst_index_prefix_F)) * dst_positive_scale_prefix_F) + (dst_positive_prefix_F))) /\ (((((exists ff_h_pvs_prefix_Fentrynegative. ff_h_pvs_prefix_Fentrynegative + S (dst_negative_prefix_F) = S ((S (dst_index_prefix_F)) * dst_negative_scale_prefix_F)) /\ exists ff_q_pvs_prefix_Fentrynegative. dst_negative_code_prefix_F = ff_q_pvs_prefix_Fentrynegative * S ((S (dst_index_prefix_F)) * dst_negative_scale_prefix_F) + (dst_negative_prefix_F))) /\ (exists ge_balance_positive_prefix_Fentryvalue ge_balance_negative_prefix_Fentryvalue. (((((dst_value_prefix_F) = 2 * (ge_balance_positive_prefix_Fentryvalue) /\ (ge_balance_negative_prefix_Fentryvalue) = 0) \/ exists ge_signed_half_prefix_Fentryvaluedecode. (((dst_value_prefix_F) = 2 * ge_signed_half_prefix_Fentryvaluedecode + 1 /\ (ge_balance_positive_prefix_Fentryvalue) = 0) /\ (ge_balance_negative_prefix_Fentryvalue) = S ge_signed_half_prefix_Fentryvaluedecode))) /\ ((dst_positive_prefix_F) + ge_balance_negative_prefix_Fentryvalue = (dst_negative_prefix_F) + ge_balance_positive_prefix_Fentryvalue))))))))) -> (exists dst_positive_code_prefix_G dst_positive_scale_prefix_G dst_negative_code_prefix_G dst_negative_scale_prefix_G. (((G) = (((((dst_positive_code_prefix_G) + (dst_positive_scale_prefix_G)) * S ((dst_positive_code_prefix_G) + (dst_positive_scale_prefix_G)) + ((dst_positive_scale_prefix_G) + (dst_positive_scale_prefix_G))) + (((dst_negative_code_prefix_G) + (dst_negative_scale_prefix_G)) * S ((dst_negative_code_prefix_G) + (dst_negative_scale_prefix_G)) + ((dst_negative_scale_prefix_G) + (dst_negative_scale_prefix_G)))) * S ((((dst_positive_code_prefix_G) + (dst_positive_scale_prefix_G)) * S ((dst_positive_code_prefix_G) + (dst_positive_scale_prefix_G)) + ((dst_positive_scale_prefix_G) + (dst_positive_scale_prefix_G))) + (((dst_negative_code_prefix_G) + (dst_negative_scale_prefix_G)) * S ((dst_negative_code_prefix_G) + (dst_negative_scale_prefix_G)) + ((dst_negative_scale_prefix_G) + (dst_negative_scale_prefix_G)))) + ((((dst_negative_code_prefix_G) + (dst_negative_scale_prefix_G)) * S ((dst_negative_code_prefix_G) + (dst_negative_scale_prefix_G)) + ((dst_negative_scale_prefix_G) + (dst_negative_scale_prefix_G))) + (((dst_negative_code_prefix_G) + (dst_negative_scale_prefix_G)) * S ((dst_negative_code_prefix_G) + (dst_negative_scale_prefix_G)) + ((dst_negative_scale_prefix_G) + (dst_negative_scale_prefix_G)))))) /\ (forall dst_index_prefix_G. (exists pvs_le_gap_prefix_Gdomain. pvs_le_gap_prefix_Gdomain + (dst_index_prefix_G) = (0)) -> exists dst_positive_prefix_G dst_negative_prefix_G dst_value_prefix_G. ((((exists ff_h_pvs_prefix_Gentrypositive. ff_h_pvs_prefix_Gentrypositive + S (dst_positive_prefix_G) = S ((S (dst_index_prefix_G)) * dst_positive_scale_prefix_G)) /\ exists ff_q_pvs_prefix_Gentrypositive. dst_positive_code_prefix_G = ff_q_pvs_prefix_Gentrypositive * S ((S (dst_index_prefix_G)) * dst_positive_scale_prefix_G) + (dst_positive_prefix_G))) /\ (((((exists ff_h_pvs_prefix_Gentrynegative. ff_h_pvs_prefix_Gentrynegative + S (dst_negative_prefix_G) = S ((S (dst_index_prefix_G)) * dst_negative_scale_prefix_G)) /\ exists ff_q_pvs_prefix_Gentrynegative. dst_negative_code_prefix_G = ff_q_pvs_prefix_Gentrynegative * S ((S (dst_index_prefix_G)) * dst_negative_scale_prefix_G) + (dst_negative_prefix_G))) /\ (exists ge_balance_positive_prefix_Gentryvalue ge_balance_negative_prefix_Gentryvalue. (((((dst_value_prefix_G) = 2 * (ge_balance_positive_prefix_Gentryvalue) /\ (ge_balance_negative_prefix_Gentryvalue) = 0) \/ exists ge_signed_half_prefix_Gentryvaluedecode. (((dst_value_prefix_G) = 2 * ge_signed_half_prefix_Gentryvaluedecode + 1 /\ (ge_balance_positive_prefix_Gentryvalue) = 0) /\ (ge_balance_negative_prefix_Gentryvalue) = S ge_signed_half_prefix_Gentryvaluedecode))) /\ ((dst_positive_prefix_G) + ge_balance_negative_prefix_Gentryvalue = (dst_negative_prefix_G) + ge_balance_positive_prefix_Gentryvalue))))))))) -> (exists dst_positive_code_prefix_H dst_positive_scale_prefix_H dst_negative_code_prefix_H dst_negative_scale_prefix_H. (((H) = (((((dst_positive_code_prefix_H) + (dst_positive_scale_prefix_H)) * S ((dst_positive_code_prefix_H) + (dst_positive_scale_prefix_H)) + ((dst_positive_scale_prefix_H) + (dst_positive_scale_prefix_H))) + (((dst_negative_code_prefix_H) + (dst_negative_scale_prefix_H)) * S ((dst_negative_code_prefix_H) + (dst_negative_scale_prefix_H)) + ((dst_negative_scale_prefix_H) + (dst_negative_scale_prefix_H)))) * S ((((dst_positive_code_prefix_H) + (dst_positive_scale_prefix_H)) * S ((dst_positive_code_prefix_H) + (dst_positive_scale_prefix_H)) + ((dst_positive_scale_prefix_H) + (dst_positive_scale_prefix_H))) + (((dst_negative_code_prefix_H) + (dst_negative_scale_prefix_H)) * S ((dst_negative_code_prefix_H) + (dst_negative_scale_prefix_H)) + ((dst_negative_scale_prefix_H) + (dst_negative_scale_prefix_H)))) + ((((dst_negative_code_prefix_H) + (dst_negative_scale_prefix_H)) * S ((dst_negative_code_prefix_H) + (dst_negative_scale_prefix_H)) + ((dst_negative_scale_prefix_H) + (dst_negative_scale_prefix_H))) + (((dst_negative_code_prefix_H) + (dst_negative_scale_prefix_H)) * S ((dst_negative_code_prefix_H) + (dst_negative_scale_prefix_H)) + ((dst_negative_scale_prefix_H) + (dst_negative_scale_prefix_H)))))) /\ (forall dst_index_prefix_H. (exists pvs_le_gap_prefix_Hdomain. pvs_le_gap_prefix_Hdomain + (dst_index_prefix_H) = (0)) -> exists dst_positive_prefix_H dst_negative_prefix_H dst_value_prefix_H. ((((exists ff_h_pvs_prefix_Hentrypositive. ff_h_pvs_prefix_Hentrypositive + S (dst_positive_prefix_H) = S ((S (dst_index_prefix_H)) * dst_positive_scale_prefix_H)) /\ exists ff_q_pvs_prefix_Hentrypositive. dst_positive_code_prefix_H = ff_q_pvs_prefix_Hentrypositive * S ((S (dst_index_prefix_H)) * dst_positive_scale_prefix_H) + (dst_positive_prefix_H))) /\ (((((exists ff_h_pvs_prefix_Hentrynegative. ff_h_pvs_prefix_Hentrynegative + S (dst_negative_prefix_H) = S ((S (dst_index_prefix_H)) * dst_negative_scale_prefix_H)) /\ exists ff_q_pvs_prefix_Hentrynegative. dst_negative_code_prefix_H = ff_q_pvs_prefix_Hentrynegative * S ((S (dst_index_prefix_H)) * dst_negative_scale_prefix_H) + (dst_negative_prefix_H))) /\ (exists ge_balance_positive_prefix_Hentryvalue ge_balance_negative_prefix_Hentryvalue. (((((dst_value_prefix_H) = 2 * (ge_balance_positive_prefix_Hentryvalue) /\ (ge_balance_negative_prefix_Hentryvalue) = 0) \/ exists ge_signed_half_prefix_Hentryvaluedecode. (((dst_value_prefix_H) = 2 * ge_signed_half_prefix_Hentryvaluedecode + 1 /\ (ge_balance_positive_prefix_Hentryvalue) = 0) /\ (ge_balance_negative_prefix_Hentryvalue) = S ge_signed_half_prefix_Hentryvaluedecode))) /\ ((dst_positive_prefix_H) + ge_balance_negative_prefix_Hentryvalue = (dst_negative_prefix_H) + ge_balance_positive_prefix_Hentryvalue))))))))) -> exists T. (((exists dst_positive_code_prefix_resulttable dst_positive_scale_prefix_resulttable dst_negative_code_prefix_resulttable dst_negative_scale_prefix_resulttable. (((T) = (((((dst_positive_code_prefix_resulttable) + (dst_positive_scale_prefix_resulttable)) * S ((dst_positive_code_prefix_resulttable) + (dst_positive_scale_prefix_resulttable)) + ((dst_positive_scale_prefix_resulttable) + (dst_positive_scale_prefix_resulttable))) + (((dst_negative_code_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)) * S ((dst_negative_code_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)) + ((dst_negative_scale_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)))) * S ((((dst_positive_code_prefix_resulttable) + (dst_positive_scale_prefix_resulttable)) * S ((dst_positive_code_prefix_resulttable) + (dst_positive_scale_prefix_resulttable)) + ((dst_positive_scale_prefix_resulttable) + (dst_positive_scale_prefix_resulttable))) + (((dst_negative_code_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)) * S ((dst_negative_code_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)) + ((dst_negative_scale_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)))) + ((((dst_negative_code_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)) * S ((dst_negative_code_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)) + ((dst_negative_scale_prefix_resulttable) + (dst_negative_scale_prefix_resulttable))) + (((dst_negative_code_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)) * S ((dst_negative_code_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)) + ((dst_negative_scale_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)))))) /\ (forall dst_index_prefix_resulttable. (exists pvs_le_gap_prefix_resulttabledomain. pvs_le_gap_prefix_resulttabledomain + (dst_index_prefix_resulttable) = (l)) -> exists dst_positive_prefix_resulttable dst_negative_prefix_resulttable dst_value_prefix_resulttable. ((((exists ff_h_pvs_prefix_resulttableentrypositive. ff_h_pvs_prefix_resulttableentrypositive + S (dst_positive_prefix_resulttable) = S ((S (dst_index_prefix_resulttable)) * dst_positive_scale_prefix_resulttable)) /\ exists ff_q_pvs_prefix_resulttableentrypositive. dst_positive_code_prefix_resulttable = ff_q_pvs_prefix_resulttableentrypositive * S ((S (dst_index_prefix_resulttable)) * dst_positive_scale_prefix_resulttable) + (dst_positive_prefix_resulttable))) /\ (((((exists ff_h_pvs_prefix_resulttableentrynegative. ff_h_pvs_prefix_resulttableentrynegative + S (dst_negative_prefix_resulttable) = S ((S (dst_index_prefix_resulttable)) * dst_negative_scale_prefix_resulttable)) /\ exists ff_q_pvs_prefix_resulttableentrynegative. dst_negative_code_prefix_resulttable = ff_q_pvs_prefix_resulttableentrynegative * S ((S (dst_index_prefix_resulttable)) * dst_negative_scale_prefix_resulttable) + (dst_negative_prefix_resulttable))) /\ (exists ge_balance_positive_prefix_resulttableentryvalue ge_balance_negative_prefix_resulttableentryvalue. (((((dst_value_prefix_resulttable) = 2 * (ge_balance_positive_prefix_resulttableentryvalue) /\ (ge_balance_negative_prefix_resulttableentryvalue) = 0) \/ exists ge_signed_half_prefix_resulttableentryvaluedecode. (((dst_value_prefix_resulttable) = 2 * ge_signed_half_prefix_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_prefix_resulttableentryvalue) = 0) /\ (ge_balance_negative_prefix_resulttableentryvalue) = S ge_signed_half_prefix_resulttableentryvaluedecode))) /\ ((dst_positive_prefix_resulttable) + ge_balance_negative_prefix_resulttableentryvalue = (dst_negative_prefix_resulttable) + ge_balance_positive_prefix_resulttableentryvalue))))))))) /\ (forall dfg_flat_index_prefix_result dfg_flat_value_prefix_result. (exists pvs_le_gap_prefix_resultbound. pvs_le_gap_prefix_resultbound + (dfg_flat_index_prefix_result) = (l)) -> (exists dst_positive_code_prefix_resultlookup dst_positive_scale_prefix_resultlookup dst_negative_code_prefix_resultlookup dst_negative_scale_prefix_resultlookup dst_positive_prefix_resultlookup dst_negative_prefix_resultlookup. (((T) = (((((dst_positive_code_prefix_resultlookup) + (dst_positive_scale_prefix_resultlookup)) * S ((dst_positive_code_prefix_resultlookup) + (dst_positive_scale_prefix_resultlookup)) + ((dst_positive_scale_prefix_resultlookup) + (dst_positive_scale_prefix_resultlookup))) + (((dst_negative_code_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)) * S ((dst_negative_code_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)) + ((dst_negative_scale_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)))) * S ((((dst_positive_code_prefix_resultlookup) + (dst_positive_scale_prefix_resultlookup)) * S ((dst_positive_code_prefix_resultlookup) + (dst_positive_scale_prefix_resultlookup)) + ((dst_positive_scale_prefix_resultlookup) + (dst_positive_scale_prefix_resultlookup))) + (((dst_negative_code_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)) * S ((dst_negative_code_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)) + ((dst_negative_scale_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)))) + ((((dst_negative_code_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)) * S ((dst_negative_code_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)) + ((dst_negative_scale_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup))) + (((dst_negative_code_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)) * S ((dst_negative_code_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)) + ((dst_negative_scale_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)))))) /\ (((((exists ff_h_pvs_prefix_resultlookuppositive. ff_h_pvs_prefix_resultlookuppositive + S (dst_positive_prefix_resultlookup) = S ((S (dfg_flat_index_prefix_result)) * dst_positive_scale_prefix_resultlookup)) /\ exists ff_q_pvs_prefix_resultlookuppositive. dst_positive_code_prefix_resultlookup = ff_q_pvs_prefix_resultlookuppositive * S ((S (dfg_flat_index_prefix_result)) * dst_positive_scale_prefix_resultlookup) + (dst_positive_prefix_resultlookup))) /\ (((((exists ff_h_pvs_prefix_resultlookupnegative. ff_h_pvs_prefix_resultlookupnegative + S (dst_negative_prefix_resultlookup) = S ((S (dfg_flat_index_prefix_result)) * dst_negative_scale_prefix_resultlookup)) /\ exists ff_q_pvs_prefix_resultlookupnegative. dst_negative_code_prefix_resultlookup = ff_q_pvs_prefix_resultlookupnegative * S ((S (dfg_flat_index_prefix_result)) * dst_negative_scale_prefix_resultlookup) + (dst_negative_prefix_resultlookup))) /\ (exists ge_balance_positive_prefix_resultlookupvalue ge_balance_negative_prefix_resultlookupvalue. (((((dfg_flat_value_prefix_result) = 2 * (ge_balance_positive_prefix_resultlookupvalue) /\ (ge_balance_negative_prefix_resultlookupvalue) = 0) \/ exists ge_signed_half_prefix_resultlookupvaluedecode. (((dfg_flat_value_prefix_result) = 2 * ge_signed_half_prefix_resultlookupvaluedecode + 1 /\ (ge_balance_positive_prefix_resultlookupvalue) = 0) /\ (ge_balance_negative_prefix_resultlookupvalue) = S ge_signed_half_prefix_resultlookupvaluedecode))) /\ ((dst_positive_prefix_resultlookup) + ge_balance_negative_prefix_resultlookupvalue = (dst_negative_prefix_resultlookup) + ge_balance_positive_prefix_resultlookupvalue))))))))) -> (exists dfg_flat_row_prefix_resultentry dfg_flat_column_prefix_resultentry. (((dfg_flat_index_prefix_result)=((S (n))*(dfg_flat_row_prefix_resultentry)+(dfg_flat_column_prefix_resultentry))) /\ (((exists pvs_gap_prefix_resultentryremainder. pvs_gap_prefix_resultentryremainder + S (dfg_flat_column_prefix_resultentry) = (S (n))) /\ ((((~((dfg_flat_row_prefix_resultentry)=0)) /\ (((~((dfg_flat_column_prefix_resultentry)=0)) /\ (exists dfg_middle_prefix_resultentrycell dfg_first_prefix_resultentrycell dfg_last_prefix_resultentrycell dfg_value_prefix_resultentrycell. (((n)=((dfg_flat_row_prefix_resultentry)*(dfg_flat_column_prefix_resultentry))*dfg_middle_prefix_resultentrycell) /\ (((exists dst_positive_code_prefix_resultentrycellfirst dst_positive_scale_prefix_resultentrycellfirst dst_negative_code_prefix_resultentrycellfirst dst_negative_scale_prefix_resultentrycellfirst dst_positive_prefix_resultentrycellfirst dst_negative_prefix_resultentrycellfirst. (((F) = (((((dst_positive_code_prefix_resultentrycellfirst) + (dst_positive_scale_prefix_resultentrycellfirst)) * S ((dst_positive_code_prefix_resultentrycellfirst) + (dst_positive_scale_prefix_resultentrycellfirst)) + ((dst_positive_scale_prefix_resultentrycellfirst) + (dst_positive_scale_prefix_resultentrycellfirst))) + (((dst_negative_code_prefix_resultentrycellfirst) + (dst_negative_scale_prefix_resultentrycellfirst)) * S ((dst_negative_code_prefix_resultentrycellfirst) + (dst_negative_scale_prefix_resultentrycellfirst)) + ((dst_negative_scale_prefix_resultentrycellfirst) + (dst_negative_scale_prefix_resultentrycellfirst)))) * S ((((dst_positive_code_prefix_resultentrycellfirst) + (dst_positive_scale_prefix_resultentrycellfirst)) * S ((dst_positive_code_prefix_resultentrycellfirst) + (dst_positive_scale_prefix_resultentrycellfirst)) + ((dst_positive_scale_prefix_resultentrycellfirst) + (dst_positive_scale_prefix_resultentrycellfirst))) + (((dst_negative_code_prefix_resultentrycellfirst) + (dst_negative_scale_prefix_resultentrycellfirst)) * S ((dst_negative_code_prefix_resultentrycellfirst) + (dst_negative_scale_prefix_resultentrycellfirst)) + ((dst_negative_scale_prefix_resultentrycellfirst) + (dst_negative_scale_prefix_resultentrycellfirst)))) + ((((dst_negative_code_prefix_resultentrycellfirst) + (dst_negative_scale_prefix_resultentrycellfirst)) * S ((dst_negative_code_prefix_resultentrycellfirst) + (dst_negative_scale_prefix_resultentrycellfirst)) + ((dst_negative_scale_prefix_resultentrycellfirst) + (dst_negative_scale_prefix_resultentrycellfirst))) + (((dst_negative_code_prefix_resultentrycellfirst) + (dst_negative_scale_prefix_resultentrycellfirst)) * S ((dst_negative_code_prefix_resultentrycellfirst) + (dst_negative_scale_prefix_resultentrycellfirst)) + ((dst_negative_scale_prefix_resultentrycellfirst) + (dst_negative_scale_prefix_resultentrycellfirst)))))) /\ (((((exists ff_h_pvs_prefix_resultentrycellfirstpositive. ff_h_pvs_prefix_resultentrycellfirstpositive + S (dst_positive_prefix_resultentrycellfirst) = S ((S (dfg_flat_row_prefix_resultentry)) * dst_positive_scale_prefix_resultentrycellfirst)) /\ exists ff_q_pvs_prefix_resultentrycellfirstpositive. dst_positive_code_prefix_resultentrycellfirst = ff_q_pvs_prefix_resultentrycellfirstpositive * S ((S (dfg_flat_row_prefix_resultentry)) * dst_positive_scale_prefix_resultentrycellfirst) + (dst_positive_prefix_resultentrycellfirst))) /\ (((((exists ff_h_pvs_prefix_resultentrycellfirstnegative. ff_h_pvs_prefix_resultentrycellfirstnegative + S (dst_negative_prefix_resultentrycellfirst) = S ((S (dfg_flat_row_prefix_resultentry)) * dst_negative_scale_prefix_resultentrycellfirst)) /\ exists ff_q_pvs_prefix_resultentrycellfirstnegative. dst_negative_code_prefix_resultentrycellfirst = ff_q_pvs_prefix_resultentrycellfirstnegative * S ((S (dfg_flat_row_prefix_resultentry)) * dst_negative_scale_prefix_resultentrycellfirst) + (dst_negative_prefix_resultentrycellfirst))) /\ (exists ge_balance_positive_prefix_resultentrycellfirstvalue ge_balance_negative_prefix_resultentrycellfirstvalue. (((((dfg_first_prefix_resultentrycell) = 2 * (ge_balance_positive_prefix_resultentrycellfirstvalue) /\ (ge_balance_negative_prefix_resultentrycellfirstvalue) = 0) \/ exists ge_signed_half_prefix_resultentrycellfirstvaluedecode. (((dfg_first_prefix_resultentrycell) = 2 * ge_signed_half_prefix_resultentrycellfirstvaluedecode + 1 /\ (ge_balance_positive_prefix_resultentrycellfirstvalue) = 0) /\ (ge_balance_negative_prefix_resultentrycellfirstvalue) = S ge_signed_half_prefix_resultentrycellfirstvaluedecode))) /\ ((dst_positive_prefix_resultentrycellfirst) + ge_balance_negative_prefix_resultentrycellfirstvalue = (dst_negative_prefix_resultentrycellfirst) + ge_balance_positive_prefix_resultentrycellfirstvalue))))))))) /\ (((exists dst_positive_code_prefix_resultentrycelllast dst_positive_scale_prefix_resultentrycelllast dst_negative_code_prefix_resultentrycelllast dst_negative_scale_prefix_resultentrycelllast dst_positive_prefix_resultentrycelllast dst_negative_prefix_resultentrycelllast. (((H) = (((((dst_positive_code_prefix_resultentrycelllast) + (dst_positive_scale_prefix_resultentrycelllast)) * S ((dst_positive_code_prefix_resultentrycelllast) + (dst_positive_scale_prefix_resultentrycelllast)) + ((dst_positive_scale_prefix_resultentrycelllast) + (dst_positive_scale_prefix_resultentrycelllast))) + (((dst_negative_code_prefix_resultentrycelllast) + (dst_negative_scale_prefix_resultentrycelllast)) * S ((dst_negative_code_prefix_resultentrycelllast) + (dst_negative_scale_prefix_resultentrycelllast)) + ((dst_negative_scale_prefix_resultentrycelllast) + (dst_negative_scale_prefix_resultentrycelllast)))) * S ((((dst_positive_code_prefix_resultentrycelllast) + (dst_positive_scale_prefix_resultentrycelllast)) * S ((dst_positive_code_prefix_resultentrycelllast) + (dst_positive_scale_prefix_resultentrycelllast)) + ((dst_positive_scale_prefix_resultentrycelllast) + (dst_positive_scale_prefix_resultentrycelllast))) + (((dst_negative_code_prefix_resultentrycelllast) + (dst_negative_scale_prefix_resultentrycelllast)) * S ((dst_negative_code_prefix_resultentrycelllast) + (dst_negative_scale_prefix_resultentrycelllast)) + ((dst_negative_scale_prefix_resultentrycelllast) + (dst_negative_scale_prefix_resultentrycelllast)))) + ((((dst_negative_code_prefix_resultentrycelllast) + (dst_negative_scale_prefix_resultentrycelllast)) * S ((dst_negative_code_prefix_resultentrycelllast) + (dst_negative_scale_prefix_resultentrycelllast)) + ((dst_negative_scale_prefix_resultentrycelllast) + (dst_negative_scale_prefix_resultentrycelllast))) + (((dst_negative_code_prefix_resultentrycelllast) + (dst_negative_scale_prefix_resultentrycelllast)) * S ((dst_negative_code_prefix_resultentrycelllast) + (dst_negative_scale_prefix_resultentrycelllast)) + ((dst_negative_scale_prefix_resultentrycelllast) + (dst_negative_scale_prefix_resultentrycelllast)))))) /\ (((((exists ff_h_pvs_prefix_resultentrycelllastpositive. ff_h_pvs_prefix_resultentrycelllastpositive + S (dst_positive_prefix_resultentrycelllast) = S ((S (dfg_flat_column_prefix_resultentry)) * dst_positive_scale_prefix_resultentrycelllast)) /\ exists ff_q_pvs_prefix_resultentrycelllastpositive. dst_positive_code_prefix_resultentrycelllast = ff_q_pvs_prefix_resultentrycelllastpositive * S ((S (dfg_flat_column_prefix_resultentry)) * dst_positive_scale_prefix_resultentrycelllast) + (dst_positive_prefix_resultentrycelllast))) /\ (((((exists ff_h_pvs_prefix_resultentrycelllastnegative. ff_h_pvs_prefix_resultentrycelllastnegative + S (dst_negative_prefix_resultentrycelllast) = S ((S (dfg_flat_column_prefix_resultentry)) * dst_negative_scale_prefix_resultentrycelllast)) /\ exists ff_q_pvs_prefix_resultentrycelllastnegative. dst_negative_code_prefix_resultentrycelllast = ff_q_pvs_prefix_resultentrycelllastnegative * S ((S (dfg_flat_column_prefix_resultentry)) * dst_negative_scale_prefix_resultentrycelllast) + (dst_negative_prefix_resultentrycelllast))) /\ (exists ge_balance_positive_prefix_resultentrycelllastvalue ge_balance_negative_prefix_resultentrycelllastvalue. (((((dfg_last_prefix_resultentrycell) = 2 * (ge_balance_positive_prefix_resultentrycelllastvalue) /\ (ge_balance_negative_prefix_resultentrycelllastvalue) = 0) \/ exists ge_signed_half_prefix_resultentrycelllastvaluedecode. (((dfg_last_prefix_resultentrycell) = 2 * ge_signed_half_prefix_resultentrycelllastvaluedecode + 1 /\ (ge_balance_positive_prefix_resultentrycelllastvalue) = 0) /\ (ge_balance_negative_prefix_resultentrycelllastvalue) = S ge_signed_half_prefix_resultentrycelllastvaluedecode))) /\ ((dst_positive_prefix_resultentrycelllast) + ge_balance_negative_prefix_resultentrycelllastvalue = (dst_negative_prefix_resultentrycelllast) + ge_balance_positive_prefix_resultentrycelllastvalue))))))))) /\ (((exists dst_positive_code_prefix_resultentrycellmiddle dst_positive_scale_prefix_resultentrycellmiddle dst_negative_code_prefix_resultentrycellmiddle dst_negative_scale_prefix_resultentrycellmiddle dst_positive_prefix_resultentrycellmiddle dst_negative_prefix_resultentrycellmiddle. (((G) = (((((dst_positive_code_prefix_resultentrycellmiddle) + (dst_positive_scale_prefix_resultentrycellmiddle)) * S ((dst_positive_code_prefix_resultentrycellmiddle) + (dst_positive_scale_prefix_resultentrycellmiddle)) + ((dst_positive_scale_prefix_resultentrycellmiddle) + (dst_positive_scale_prefix_resultentrycellmiddle))) + (((dst_negative_code_prefix_resultentrycellmiddle) + (dst_negative_scale_prefix_resultentrycellmiddle)) * S ((dst_negative_code_prefix_resultentrycellmiddle) + (dst_negative_scale_prefix_resultentrycellmiddle)) + ((dst_negative_scale_prefix_resultentrycellmiddle) + (dst_negative_scale_prefix_resultentrycellmiddle)))) * S ((((dst_positive_code_prefix_resultentrycellmiddle) + (dst_positive_scale_prefix_resultentrycellmiddle)) * S ((dst_positive_code_prefix_resultentrycellmiddle) + (dst_positive_scale_prefix_resultentrycellmiddle)) + ((dst_positive_scale_prefix_resultentrycellmiddle) + (dst_positive_scale_prefix_resultentrycellmiddle))) + (((dst_negative_code_prefix_resultentrycellmiddle) + (dst_negative_scale_prefix_resultentrycellmiddle)) * S ((dst_negative_code_prefix_resultentrycellmiddle) + (dst_negative_scale_prefix_resultentrycellmiddle)) + ((dst_negative_scale_prefix_resultentrycellmiddle) + (dst_negative_scale_prefix_resultentrycellmiddle)))) + ((((dst_negative_code_prefix_resultentrycellmiddle) + (dst_negative_scale_prefix_resultentrycellmiddle)) * S ((dst_negative_code_prefix_resultentrycellmiddle) + (dst_negative_scale_prefix_resultentrycellmiddle)) + ((dst_negative_scale_prefix_resultentrycellmiddle) + (dst_negative_scale_prefix_resultentrycellmiddle))) + (((dst_negative_code_prefix_resultentrycellmiddle) + (dst_negative_scale_prefix_resultentrycellmiddle)) * S ((dst_negative_code_prefix_resultentrycellmiddle) + (dst_negative_scale_prefix_resultentrycellmiddle)) + ((dst_negative_scale_prefix_resultentrycellmiddle) + (dst_negative_scale_prefix_resultentrycellmiddle)))))) /\ (((((exists ff_h_pvs_prefix_resultentrycellmiddlepositive. ff_h_pvs_prefix_resultentrycellmiddlepositive + S (dst_positive_prefix_resultentrycellmiddle) = S ((S (dfg_middle_prefix_resultentrycell)) * dst_positive_scale_prefix_resultentrycellmiddle)) /\ exists ff_q_pvs_prefix_resultentrycellmiddlepositive. dst_positive_code_prefix_resultentrycellmiddle = ff_q_pvs_prefix_resultentrycellmiddlepositive * S ((S (dfg_middle_prefix_resultentrycell)) * dst_positive_scale_prefix_resultentrycellmiddle) + (dst_positive_prefix_resultentrycellmiddle))) /\ (((((exists ff_h_pvs_prefix_resultentrycellmiddlenegative. ff_h_pvs_prefix_resultentrycellmiddlenegative + S (dst_negative_prefix_resultentrycellmiddle) = S ((S (dfg_middle_prefix_resultentrycell)) * dst_negative_scale_prefix_resultentrycellmiddle)) /\ exists ff_q_pvs_prefix_resultentrycellmiddlenegative. dst_negative_code_prefix_resultentrycellmiddle = ff_q_pvs_prefix_resultentrycellmiddlenegative * S ((S (dfg_middle_prefix_resultentrycell)) * dst_negative_scale_prefix_resultentrycellmiddle) + (dst_negative_prefix_resultentrycellmiddle))) /\ (exists ge_balance_positive_prefix_resultentrycellmiddlevalue ge_balance_negative_prefix_resultentrycellmiddlevalue. (((((dfg_value_prefix_resultentrycell) = 2 * (ge_balance_positive_prefix_resultentrycellmiddlevalue) /\ (ge_balance_negative_prefix_resultentrycellmiddlevalue) = 0) \/ exists ge_signed_half_prefix_resultentrycellmiddlevaluedecode. (((dfg_value_prefix_resultentrycell) = 2 * ge_signed_half_prefix_resultentrycellmiddlevaluedecode + 1 /\ (ge_balance_positive_prefix_resultentrycellmiddlevalue) = 0) /\ (ge_balance_negative_prefix_resultentrycellmiddlevalue) = S ge_signed_half_prefix_resultentrycellmiddlevaluedecode))) /\ ((dst_positive_prefix_resultentrycellmiddle) + ge_balance_negative_prefix_resultentrycellmiddlevalue = (dst_negative_prefix_resultentrycellmiddle) + ge_balance_positive_prefix_resultentrycellmiddlevalue))))))))) /\ (exists dfg_inner_prefix_resultentrycellproduct. ((exists sto_ap_prefix_resultentrycellproductinner sto_an_prefix_resultentrycellproductinner sto_bp_prefix_resultentrycellproductinner sto_bn_prefix_resultentrycellproductinner sto_cp_prefix_resultentrycellproductinner sto_cn_prefix_resultentrycellproductinner. (((((dfg_last_prefix_resultentrycell) = 2 * (sto_ap_prefix_resultentrycellproductinner) /\ (sto_an_prefix_resultentrycellproductinner) = 0) \/ exists ge_signed_half_prefix_resultentrycellproductinnerleft. (((dfg_last_prefix_resultentrycell) = 2 * ge_signed_half_prefix_resultentrycellproductinnerleft + 1 /\ (sto_ap_prefix_resultentrycellproductinner) = 0) /\ (sto_an_prefix_resultentrycellproductinner) = S ge_signed_half_prefix_resultentrycellproductinnerleft))) /\ ((((((dfg_value_prefix_resultentrycell) = 2 * (sto_bp_prefix_resultentrycellproductinner) /\ (sto_bn_prefix_resultentrycellproductinner) = 0) \/ exists ge_signed_half_prefix_resultentrycellproductinnerright. (((dfg_value_prefix_resultentrycell) = 2 * ge_signed_half_prefix_resultentrycellproductinnerright + 1 /\ (sto_bp_prefix_resultentrycellproductinner) = 0) /\ (sto_bn_prefix_resultentrycellproductinner) = S ge_signed_half_prefix_resultentrycellproductinnerright))) /\ ((((((dfg_inner_prefix_resultentrycellproduct) = 2 * (sto_cp_prefix_resultentrycellproductinner) /\ (sto_cn_prefix_resultentrycellproductinner) = 0) \/ exists ge_signed_half_prefix_resultentrycellproductinneroutput. (((dfg_inner_prefix_resultentrycellproduct) = 2 * ge_signed_half_prefix_resultentrycellproductinneroutput + 1 /\ (sto_cp_prefix_resultentrycellproductinner) = 0) /\ (sto_cn_prefix_resultentrycellproductinner) = S ge_signed_half_prefix_resultentrycellproductinneroutput))) /\ ((sto_ap_prefix_resultentrycellproductinner * sto_bp_prefix_resultentrycellproductinner + sto_an_prefix_resultentrycellproductinner * sto_bn_prefix_resultentrycellproductinner) + sto_cn_prefix_resultentrycellproductinner = (sto_ap_prefix_resultentrycellproductinner * sto_bn_prefix_resultentrycellproductinner + sto_an_prefix_resultentrycellproductinner * sto_bp_prefix_resultentrycellproductinner) + sto_cp_prefix_resultentrycellproductinner))))))) /\ (exists sto_ap_prefix_resultentrycellproductouter sto_an_prefix_resultentrycellproductouter sto_bp_prefix_resultentrycellproductouter sto_bn_prefix_resultentrycellproductouter sto_cp_prefix_resultentrycellproductouter sto_cn_prefix_resultentrycellproductouter. (((((dfg_first_prefix_resultentrycell) = 2 * (sto_ap_prefix_resultentrycellproductouter) /\ (sto_an_prefix_resultentrycellproductouter) = 0) \/ exists ge_signed_half_prefix_resultentrycellproductouterleft. (((dfg_first_prefix_resultentrycell) = 2 * ge_signed_half_prefix_resultentrycellproductouterleft + 1 /\ (sto_ap_prefix_resultentrycellproductouter) = 0) /\ (sto_an_prefix_resultentrycellproductouter) = S ge_signed_half_prefix_resultentrycellproductouterleft))) /\ ((((((dfg_inner_prefix_resultentrycellproduct) = 2 * (sto_bp_prefix_resultentrycellproductouter) /\ (sto_bn_prefix_resultentrycellproductouter) = 0) \/ exists ge_signed_half_prefix_resultentrycellproductouterright. (((dfg_inner_prefix_resultentrycellproduct) = 2 * ge_signed_half_prefix_resultentrycellproductouterright + 1 /\ (sto_bp_prefix_resultentrycellproductouter) = 0) /\ (sto_bn_prefix_resultentrycellproductouter) = S ge_signed_half_prefix_resultentrycellproductouterright))) /\ ((((((dfg_flat_value_prefix_result) = 2 * (sto_cp_prefix_resultentrycellproductouter) /\ (sto_cn_prefix_resultentrycellproductouter) = 0) \/ exists ge_signed_half_prefix_resultentrycellproductouteroutput. (((dfg_flat_value_prefix_result) = 2 * ge_signed_half_prefix_resultentrycellproductouteroutput + 1 /\ (sto_cp_prefix_resultentrycellproductouter) = 0) /\ (sto_cn_prefix_resultentrycellproductouter) = S ge_signed_half_prefix_resultentrycellproductouteroutput))) /\ ((sto_ap_prefix_resultentrycellproductouter * sto_bp_prefix_resultentrycellproductouter + sto_an_prefix_resultentrycellproductouter * sto_bn_prefix_resultentrycellproductouter) + sto_cn_prefix_resultentrycellproductouter = (sto_ap_prefix_resultentrycellproductouter * sto_bn_prefix_resultentrycellproductouter + sto_an_prefix_resultentrycellproductouter * sto_bp_prefix_resultentrycellproductouter) + sto_cp_prefix_resultentrycellproductouter))))))))))))))))))))) \/ ((((dfg_flat_row_prefix_resultentry)=0 \/ ((dfg_flat_column_prefix_resultentry)=0 \/ ~(exists pvs_factor_prefix_resultentrycellomittednondivisor. (n) = ((dfg_flat_row_prefix_resultentry)*(dfg_flat_column_prefix_resultentry)) * pvs_factor_prefix_resultentrycellomittednondivisor))) /\ ((dfg_flat_value_prefix_result)=0)))))))))))

Complete tactic proof in conservative notation

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

71 script commands · 18 reading checkpoints · 5 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 (3)
dirichlet grid flat entry existsdirichlet grid flat prefix zerodirichlet grid flat prefix append
01Fix variables and assumptionsL1–5

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 l
02Induction on lL6–9

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L6
    induction l
  2. L7
    intro hF
  3. L8
    intro hG
  4. L9
    intro hH
03Establish hvL10–19

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

  1. L10
    have hv : ∃ z. DirichletFlatEntry(F,G,H,n,0,z)Definitions: DirichletFlatEntry(F,G,H,n,0,z)Original native command in the exact edition
  2. L11
    specialize dirichlet_grid_flat_entry_exists (F)
  3. L12
    specialize dirichlet_grid_flat_entry_exists (G)
  4. L13
    specialize dirichlet_grid_flat_entry_exists (H)
  5. L14
    specialize dirichlet_grid_flat_entry_exists (n)
  6. L15
    specialize dirichlet_grid_flat_entry_exists (0)
  7. L16
    apply dirichlet_grid_flat_entry_exists
  8. L17
    exact hF
  9. L18
    exact hG
  10. L19
    exact hH
04Separate the logical casesL20–20

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

  1. L20
    cases hv
05Establish htL21–23

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

  1. L21
    have ht : ∃ T. ArithTable(0,T) ∧ ArithAt(T,0,x)Definitions: ArithTable(0,T)ArithAt(T,0,x)Original native command in the exact edition
  2. L22
    specialize arithmetic_signed_table_singleton (x)
  3. L23
    apply arithmetic_signed_table_singleton
06Separate the logical casesL24–25

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

  1. L24
    cases ht
  2. L25
    cases ht_witness
07Construct an explicit witnessL26–26

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

  1. L26
    exists x1
08Use earlier factsL27–36

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

  1. L27
    specialize dirichlet_grid_flat_prefix_zero (F)
  2. L28
    specialize dirichlet_grid_flat_prefix_zero (G)
  3. L29
    specialize dirichlet_grid_flat_prefix_zero (H)
  4. L30
    specialize dirichlet_grid_flat_prefix_zero (n)
  5. L31
    specialize dirichlet_grid_flat_prefix_zero (x1)
  6. L32
    specialize dirichlet_grid_flat_prefix_zero (x)
  7. L33
    apply dirichlet_grid_flat_prefix_zero
  8. L34
    exact ht_witness_left
  9. L35
    exact ht_witness_right
  10. L36
    exact hv_witness
09Fix variables and assumptionsL37–39

Work with arbitrary variables or the premises of the current implication.

  1. L37
    intro hF
  2. L38
    intro hG
  3. L39
    intro hH
10Establish hpL40–44

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

  1. L40
    have hp : ∃ T. DirichletFlatPrefix(F,G,H,n,l,T)Definitions: DirichletFlatPrefix(F,G,H,n,l,T)Original native command in the exact edition
  2. L41
    apply IH
  3. L42
    exact hF
  4. L43
    exact hG
  5. L44
    exact hH
11Separate the logical casesL45–45

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

  1. L45
    cases hp
12Establish hvL46–55

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

  1. L46
    have hv : ∃ z. DirichletFlatEntry(F,G,H,n,S l,z)Definitions: DirichletFlatEntry(F,G,H,n,S l,z)Original native command in the exact edition
  2. L47
    specialize dirichlet_grid_flat_entry_exists (F)
  3. L48
    specialize dirichlet_grid_flat_entry_exists (G)
  4. L49
    specialize dirichlet_grid_flat_entry_exists (H)
  5. L50
    specialize dirichlet_grid_flat_entry_exists (n)
  6. L51
    specialize dirichlet_grid_flat_entry_exists (S l)
  7. L52
    apply dirichlet_grid_flat_entry_exists
  8. L53
    exact hF
  9. L54
    exact hG
  10. L55
    exact hH
13Separate the logical casesL56–56

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

  1. L56
    cases hv
14Establish hextL57–66

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

  1. L57
    have hext : ∃ U. DirichletFlatPrefix(F,G,H,n,S l,U) ∧ (∀ y. ∀ z. ∀ m. Lt(y,S l) → ArithAt(x,y,z) → ArithAt(U,y,m) → z = m)Definitions: DirichletFlatPrefix(F,G,H,n,S l,U)Lt(y,S l)ArithAt(x,y,z)ArithAt(U,y,m)Original native command in the exact edition
  2. L58
    specialize dirichlet_grid_flat_prefix_append (F)
  3. L59
    specialize dirichlet_grid_flat_prefix_append (G)
  4. L60
    specialize dirichlet_grid_flat_prefix_append (H)
  5. L61
    specialize dirichlet_grid_flat_prefix_append (n)
  6. L62
    specialize dirichlet_grid_flat_prefix_append (l)
  7. L63
    specialize dirichlet_grid_flat_prefix_append (x)
  8. L64
    specialize dirichlet_grid_flat_prefix_append (x1)
  9. L65
    apply dirichlet_grid_flat_prefix_append
  10. L66
    exact hp_witness
15Use earlier factsL67–67

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

  1. L67
    exact hv_witness
16Separate the logical casesL68–69

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

  1. L68
    cases hext
  2. L69
    cases hext_witness
17Construct an explicit witnessL70–70

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

  1. L70
    exists x2
18Use earlier factsL71–71

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

  1. L71
    exact hext_witness_left

Library-wide reading audit

Original defined command ledger · 71 lines
  1. 0001intro F
  2. 0002intro G
  3. 0003intro H
  4. 0004intro n
  5. 0005intro l
  6. 0006induction l
  7. 0007intro hF
  8. 0008intro hG
  9. 0009intro hH
  10. 0010have hv : ∃ z. DirichletFlatEntry(F,G,H,n,0,z)
  11. 0011specialize dirichlet_grid_flat_entry_exists (F)
  12. 0012specialize dirichlet_grid_flat_entry_exists (G)
  13. 0013specialize dirichlet_grid_flat_entry_exists (H)
  14. 0014specialize dirichlet_grid_flat_entry_exists (n)
  15. 0015specialize dirichlet_grid_flat_entry_exists (0)
  16. 0016apply dirichlet_grid_flat_entry_exists
  17. 0017exact hF
  18. 0018exact hG
  19. 0019exact hH
  20. 0020cases hv
  21. 0021have ht : ∃ T. ArithTable(0,T) ∧ ArithAt(T,0,x)
  22. 0022specialize arithmetic_signed_table_singleton (x)
  23. 0023apply arithmetic_signed_table_singleton
  24. 0024cases ht
  25. 0025cases ht_witness
  26. 0026exists x1
  27. 0027specialize dirichlet_grid_flat_prefix_zero (F)
  28. 0028specialize dirichlet_grid_flat_prefix_zero (G)
  29. 0029specialize dirichlet_grid_flat_prefix_zero (H)
  30. 0030specialize dirichlet_grid_flat_prefix_zero (n)
  31. 0031specialize dirichlet_grid_flat_prefix_zero (x1)
  32. 0032specialize dirichlet_grid_flat_prefix_zero (x)
  33. 0033apply dirichlet_grid_flat_prefix_zero
  34. 0034exact ht_witness_left
  35. 0035exact ht_witness_right
  36. 0036exact hv_witness
  37. 0037intro hF
  38. 0038intro hG
  39. 0039intro hH
  40. 0040have hp : ∃ T. DirichletFlatPrefix(F,G,H,n,l,T)
  41. 0041apply IH
  42. 0042exact hF
  43. 0043exact hG
  44. 0044exact hH
  45. 0045cases hp
  46. 0046have hv : ∃ z. DirichletFlatEntry(F,G,H,n,S l,z)
  47. 0047specialize dirichlet_grid_flat_entry_exists (F)
  48. 0048specialize dirichlet_grid_flat_entry_exists (G)
  49. 0049specialize dirichlet_grid_flat_entry_exists (H)
  50. 0050specialize dirichlet_grid_flat_entry_exists (n)
  51. 0051specialize dirichlet_grid_flat_entry_exists (S l)
  52. 0052apply dirichlet_grid_flat_entry_exists
  53. 0053exact hF
  54. 0054exact hG
  55. 0055exact hH
  56. 0056cases hv
  57. 0057have hext : ∃ U. DirichletFlatPrefix(F,G,H,n,S l,U) ∧ (∀ y. ∀ z. ∀ m. Lt(y,S l) → ArithAt(x,y,z) → ArithAt(U,y,m) → z = m)
  58. 0058specialize dirichlet_grid_flat_prefix_append (F)
  59. 0059specialize dirichlet_grid_flat_prefix_append (G)
  60. 0060specialize dirichlet_grid_flat_prefix_append (H)
  61. 0061specialize dirichlet_grid_flat_prefix_append (n)
  62. 0062specialize dirichlet_grid_flat_prefix_append (l)
  63. 0063specialize dirichlet_grid_flat_prefix_append (x)
  64. 0064specialize dirichlet_grid_flat_prefix_append (x1)
  65. 0065apply dirichlet_grid_flat_prefix_append
  66. 0066exact hp_witness
  67. 0067exact hv_witness
  68. 0068cases hext
  69. 0069cases hext_witness
  70. 0070exists x2
  71. 0071exact hext_witness_left