DF0009

dirichlet_grid_flat_entry_coordinates

Uniqueness of the actual quotient and strict remainder recovers the specified grid coordinates, rather than assuming a decoding oracle.

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

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

Every grid, slice, row sum and intermediate table is constructed. Retained cells have witnessed n=(a*e)*c and value F(a)*(H(e)*G(c)). The flat endpoint is unused. Table associativity includes N=0 and compares only positive values, not encodings. Full G009 remains broader.

Exact theorem in conservative defined notation

∀ F. ∀ G. ∀ H. ∀ n. ∀ a. ∀ e. ∀ z. Lt(e,S n) → DirichletFlatEntry(F,G,H,n,S n · a + e,z) → DirichletGridEntry(F,G,H,n,a,e,z)

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

Definition DAG

DirichletGridEntry(F,G,H,n,a,e,z) · 1DirichletFlatEntry(F,G,H,n,i,z) · 1Lt(a,b) · 1

Actual proof prerequisites

division_remainder_unique · checked external prerequisite
Original expanded first-order statement 
forall F G H n a e z. (exists pvs_gap_flat_read_bound. pvs_gap_flat_read_bound + S (e) = (S n)) -> (exists dfg_flat_row_flat_read_source dfg_flat_column_flat_read_source. ((((S (n))*(a)+(e))=((S (n))*(dfg_flat_row_flat_read_source)+(dfg_flat_column_flat_read_source))) /\ (((exists pvs_gap_flat_read_sourceremainder. pvs_gap_flat_read_sourceremainder + S (dfg_flat_column_flat_read_source) = (S (n))) /\ ((((~((dfg_flat_row_flat_read_source)=0)) /\ (((~((dfg_flat_column_flat_read_source)=0)) /\ (exists dfg_middle_flat_read_sourcecell dfg_first_flat_read_sourcecell dfg_last_flat_read_sourcecell dfg_value_flat_read_sourcecell. (((n)=((dfg_flat_row_flat_read_source)*(dfg_flat_column_flat_read_source))*dfg_middle_flat_read_sourcecell) /\ (((exists dst_positive_code_flat_read_sourcecellfirst dst_positive_scale_flat_read_sourcecellfirst dst_negative_code_flat_read_sourcecellfirst dst_negative_scale_flat_read_sourcecellfirst dst_positive_flat_read_sourcecellfirst dst_negative_flat_read_sourcecellfirst. (((F) = (((((dst_positive_code_flat_read_sourcecellfirst) + (dst_positive_scale_flat_read_sourcecellfirst)) * S ((dst_positive_code_flat_read_sourcecellfirst) + (dst_positive_scale_flat_read_sourcecellfirst)) + ((dst_positive_scale_flat_read_sourcecellfirst) + (dst_positive_scale_flat_read_sourcecellfirst))) + (((dst_negative_code_flat_read_sourcecellfirst) + (dst_negative_scale_flat_read_sourcecellfirst)) * S ((dst_negative_code_flat_read_sourcecellfirst) + (dst_negative_scale_flat_read_sourcecellfirst)) + ((dst_negative_scale_flat_read_sourcecellfirst) + (dst_negative_scale_flat_read_sourcecellfirst)))) * S ((((dst_positive_code_flat_read_sourcecellfirst) + (dst_positive_scale_flat_read_sourcecellfirst)) * S ((dst_positive_code_flat_read_sourcecellfirst) + (dst_positive_scale_flat_read_sourcecellfirst)) + ((dst_positive_scale_flat_read_sourcecellfirst) + (dst_positive_scale_flat_read_sourcecellfirst))) + (((dst_negative_code_flat_read_sourcecellfirst) + (dst_negative_scale_flat_read_sourcecellfirst)) * S ((dst_negative_code_flat_read_sourcecellfirst) + (dst_negative_scale_flat_read_sourcecellfirst)) + ((dst_negative_scale_flat_read_sourcecellfirst) + (dst_negative_scale_flat_read_sourcecellfirst)))) + ((((dst_negative_code_flat_read_sourcecellfirst) + (dst_negative_scale_flat_read_sourcecellfirst)) * S ((dst_negative_code_flat_read_sourcecellfirst) + (dst_negative_scale_flat_read_sourcecellfirst)) + ((dst_negative_scale_flat_read_sourcecellfirst) + (dst_negative_scale_flat_read_sourcecellfirst))) + (((dst_negative_code_flat_read_sourcecellfirst) + (dst_negative_scale_flat_read_sourcecellfirst)) * S ((dst_negative_code_flat_read_sourcecellfirst) + (dst_negative_scale_flat_read_sourcecellfirst)) + ((dst_negative_scale_flat_read_sourcecellfirst) + (dst_negative_scale_flat_read_sourcecellfirst)))))) /\ (((((exists ff_h_pvs_flat_read_sourcecellfirstpositive. ff_h_pvs_flat_read_sourcecellfirstpositive + S (dst_positive_flat_read_sourcecellfirst) = S ((S (dfg_flat_row_flat_read_source)) * dst_positive_scale_flat_read_sourcecellfirst)) /\ exists ff_q_pvs_flat_read_sourcecellfirstpositive. dst_positive_code_flat_read_sourcecellfirst = ff_q_pvs_flat_read_sourcecellfirstpositive * S ((S (dfg_flat_row_flat_read_source)) * dst_positive_scale_flat_read_sourcecellfirst) + (dst_positive_flat_read_sourcecellfirst))) /\ (((((exists ff_h_pvs_flat_read_sourcecellfirstnegative. ff_h_pvs_flat_read_sourcecellfirstnegative + S (dst_negative_flat_read_sourcecellfirst) = S ((S (dfg_flat_row_flat_read_source)) * dst_negative_scale_flat_read_sourcecellfirst)) /\ exists ff_q_pvs_flat_read_sourcecellfirstnegative. dst_negative_code_flat_read_sourcecellfirst = ff_q_pvs_flat_read_sourcecellfirstnegative * S ((S (dfg_flat_row_flat_read_source)) * dst_negative_scale_flat_read_sourcecellfirst) + (dst_negative_flat_read_sourcecellfirst))) /\ (exists ge_balance_positive_flat_read_sourcecellfirstvalue ge_balance_negative_flat_read_sourcecellfirstvalue. (((((dfg_first_flat_read_sourcecell) = 2 * (ge_balance_positive_flat_read_sourcecellfirstvalue) /\ (ge_balance_negative_flat_read_sourcecellfirstvalue) = 0) \/ exists ge_signed_half_flat_read_sourcecellfirstvaluedecode. (((dfg_first_flat_read_sourcecell) = 2 * ge_signed_half_flat_read_sourcecellfirstvaluedecode + 1 /\ (ge_balance_positive_flat_read_sourcecellfirstvalue) = 0) /\ (ge_balance_negative_flat_read_sourcecellfirstvalue) = S ge_signed_half_flat_read_sourcecellfirstvaluedecode))) /\ ((dst_positive_flat_read_sourcecellfirst) + ge_balance_negative_flat_read_sourcecellfirstvalue = (dst_negative_flat_read_sourcecellfirst) + ge_balance_positive_flat_read_sourcecellfirstvalue))))))))) /\ (((exists dst_positive_code_flat_read_sourcecelllast dst_positive_scale_flat_read_sourcecelllast dst_negative_code_flat_read_sourcecelllast dst_negative_scale_flat_read_sourcecelllast dst_positive_flat_read_sourcecelllast dst_negative_flat_read_sourcecelllast. (((H) = (((((dst_positive_code_flat_read_sourcecelllast) + (dst_positive_scale_flat_read_sourcecelllast)) * S ((dst_positive_code_flat_read_sourcecelllast) + (dst_positive_scale_flat_read_sourcecelllast)) + ((dst_positive_scale_flat_read_sourcecelllast) + (dst_positive_scale_flat_read_sourcecelllast))) + (((dst_negative_code_flat_read_sourcecelllast) + (dst_negative_scale_flat_read_sourcecelllast)) * S ((dst_negative_code_flat_read_sourcecelllast) + (dst_negative_scale_flat_read_sourcecelllast)) + ((dst_negative_scale_flat_read_sourcecelllast) + (dst_negative_scale_flat_read_sourcecelllast)))) * S ((((dst_positive_code_flat_read_sourcecelllast) + (dst_positive_scale_flat_read_sourcecelllast)) * S ((dst_positive_code_flat_read_sourcecelllast) + (dst_positive_scale_flat_read_sourcecelllast)) + ((dst_positive_scale_flat_read_sourcecelllast) + (dst_positive_scale_flat_read_sourcecelllast))) + (((dst_negative_code_flat_read_sourcecelllast) + (dst_negative_scale_flat_read_sourcecelllast)) * S ((dst_negative_code_flat_read_sourcecelllast) + (dst_negative_scale_flat_read_sourcecelllast)) + ((dst_negative_scale_flat_read_sourcecelllast) + (dst_negative_scale_flat_read_sourcecelllast)))) + ((((dst_negative_code_flat_read_sourcecelllast) + (dst_negative_scale_flat_read_sourcecelllast)) * S ((dst_negative_code_flat_read_sourcecelllast) + (dst_negative_scale_flat_read_sourcecelllast)) + ((dst_negative_scale_flat_read_sourcecelllast) + (dst_negative_scale_flat_read_sourcecelllast))) + (((dst_negative_code_flat_read_sourcecelllast) + (dst_negative_scale_flat_read_sourcecelllast)) * S ((dst_negative_code_flat_read_sourcecelllast) + (dst_negative_scale_flat_read_sourcecelllast)) + ((dst_negative_scale_flat_read_sourcecelllast) + (dst_negative_scale_flat_read_sourcecelllast)))))) /\ (((((exists ff_h_pvs_flat_read_sourcecelllastpositive. ff_h_pvs_flat_read_sourcecelllastpositive + S (dst_positive_flat_read_sourcecelllast) = S ((S (dfg_flat_column_flat_read_source)) * dst_positive_scale_flat_read_sourcecelllast)) /\ exists ff_q_pvs_flat_read_sourcecelllastpositive. dst_positive_code_flat_read_sourcecelllast = ff_q_pvs_flat_read_sourcecelllastpositive * S ((S (dfg_flat_column_flat_read_source)) * dst_positive_scale_flat_read_sourcecelllast) + (dst_positive_flat_read_sourcecelllast))) /\ (((((exists ff_h_pvs_flat_read_sourcecelllastnegative. ff_h_pvs_flat_read_sourcecelllastnegative + S (dst_negative_flat_read_sourcecelllast) = S ((S (dfg_flat_column_flat_read_source)) * dst_negative_scale_flat_read_sourcecelllast)) /\ exists ff_q_pvs_flat_read_sourcecelllastnegative. dst_negative_code_flat_read_sourcecelllast = ff_q_pvs_flat_read_sourcecelllastnegative * S ((S (dfg_flat_column_flat_read_source)) * dst_negative_scale_flat_read_sourcecelllast) + (dst_negative_flat_read_sourcecelllast))) /\ (exists ge_balance_positive_flat_read_sourcecelllastvalue ge_balance_negative_flat_read_sourcecelllastvalue. (((((dfg_last_flat_read_sourcecell) = 2 * (ge_balance_positive_flat_read_sourcecelllastvalue) /\ (ge_balance_negative_flat_read_sourcecelllastvalue) = 0) \/ exists ge_signed_half_flat_read_sourcecelllastvaluedecode. (((dfg_last_flat_read_sourcecell) = 2 * ge_signed_half_flat_read_sourcecelllastvaluedecode + 1 /\ (ge_balance_positive_flat_read_sourcecelllastvalue) = 0) /\ (ge_balance_negative_flat_read_sourcecelllastvalue) = S ge_signed_half_flat_read_sourcecelllastvaluedecode))) /\ ((dst_positive_flat_read_sourcecelllast) + ge_balance_negative_flat_read_sourcecelllastvalue = (dst_negative_flat_read_sourcecelllast) + ge_balance_positive_flat_read_sourcecelllastvalue))))))))) /\ (((exists dst_positive_code_flat_read_sourcecellmiddle dst_positive_scale_flat_read_sourcecellmiddle dst_negative_code_flat_read_sourcecellmiddle dst_negative_scale_flat_read_sourcecellmiddle dst_positive_flat_read_sourcecellmiddle dst_negative_flat_read_sourcecellmiddle. (((G) = (((((dst_positive_code_flat_read_sourcecellmiddle) + (dst_positive_scale_flat_read_sourcecellmiddle)) * S ((dst_positive_code_flat_read_sourcecellmiddle) + (dst_positive_scale_flat_read_sourcecellmiddle)) + ((dst_positive_scale_flat_read_sourcecellmiddle) + (dst_positive_scale_flat_read_sourcecellmiddle))) + (((dst_negative_code_flat_read_sourcecellmiddle) + (dst_negative_scale_flat_read_sourcecellmiddle)) * S ((dst_negative_code_flat_read_sourcecellmiddle) + (dst_negative_scale_flat_read_sourcecellmiddle)) + ((dst_negative_scale_flat_read_sourcecellmiddle) + (dst_negative_scale_flat_read_sourcecellmiddle)))) * S ((((dst_positive_code_flat_read_sourcecellmiddle) + (dst_positive_scale_flat_read_sourcecellmiddle)) * S ((dst_positive_code_flat_read_sourcecellmiddle) + (dst_positive_scale_flat_read_sourcecellmiddle)) + ((dst_positive_scale_flat_read_sourcecellmiddle) + (dst_positive_scale_flat_read_sourcecellmiddle))) + (((dst_negative_code_flat_read_sourcecellmiddle) + (dst_negative_scale_flat_read_sourcecellmiddle)) * S ((dst_negative_code_flat_read_sourcecellmiddle) + (dst_negative_scale_flat_read_sourcecellmiddle)) + ((dst_negative_scale_flat_read_sourcecellmiddle) + (dst_negative_scale_flat_read_sourcecellmiddle)))) + ((((dst_negative_code_flat_read_sourcecellmiddle) + (dst_negative_scale_flat_read_sourcecellmiddle)) * S ((dst_negative_code_flat_read_sourcecellmiddle) + (dst_negative_scale_flat_read_sourcecellmiddle)) + ((dst_negative_scale_flat_read_sourcecellmiddle) + (dst_negative_scale_flat_read_sourcecellmiddle))) + (((dst_negative_code_flat_read_sourcecellmiddle) + (dst_negative_scale_flat_read_sourcecellmiddle)) * S ((dst_negative_code_flat_read_sourcecellmiddle) + (dst_negative_scale_flat_read_sourcecellmiddle)) + ((dst_negative_scale_flat_read_sourcecellmiddle) + (dst_negative_scale_flat_read_sourcecellmiddle)))))) /\ (((((exists ff_h_pvs_flat_read_sourcecellmiddlepositive. ff_h_pvs_flat_read_sourcecellmiddlepositive + S (dst_positive_flat_read_sourcecellmiddle) = S ((S (dfg_middle_flat_read_sourcecell)) * dst_positive_scale_flat_read_sourcecellmiddle)) /\ exists ff_q_pvs_flat_read_sourcecellmiddlepositive. dst_positive_code_flat_read_sourcecellmiddle = ff_q_pvs_flat_read_sourcecellmiddlepositive * S ((S (dfg_middle_flat_read_sourcecell)) * dst_positive_scale_flat_read_sourcecellmiddle) + (dst_positive_flat_read_sourcecellmiddle))) /\ (((((exists ff_h_pvs_flat_read_sourcecellmiddlenegative. ff_h_pvs_flat_read_sourcecellmiddlenegative + S (dst_negative_flat_read_sourcecellmiddle) = S ((S (dfg_middle_flat_read_sourcecell)) * dst_negative_scale_flat_read_sourcecellmiddle)) /\ exists ff_q_pvs_flat_read_sourcecellmiddlenegative. dst_negative_code_flat_read_sourcecellmiddle = ff_q_pvs_flat_read_sourcecellmiddlenegative * S ((S (dfg_middle_flat_read_sourcecell)) * dst_negative_scale_flat_read_sourcecellmiddle) + (dst_negative_flat_read_sourcecellmiddle))) /\ (exists ge_balance_positive_flat_read_sourcecellmiddlevalue ge_balance_negative_flat_read_sourcecellmiddlevalue. (((((dfg_value_flat_read_sourcecell) = 2 * (ge_balance_positive_flat_read_sourcecellmiddlevalue) /\ (ge_balance_negative_flat_read_sourcecellmiddlevalue) = 0) \/ exists ge_signed_half_flat_read_sourcecellmiddlevaluedecode. (((dfg_value_flat_read_sourcecell) = 2 * ge_signed_half_flat_read_sourcecellmiddlevaluedecode + 1 /\ (ge_balance_positive_flat_read_sourcecellmiddlevalue) = 0) /\ (ge_balance_negative_flat_read_sourcecellmiddlevalue) = S ge_signed_half_flat_read_sourcecellmiddlevaluedecode))) /\ ((dst_positive_flat_read_sourcecellmiddle) + ge_balance_negative_flat_read_sourcecellmiddlevalue = (dst_negative_flat_read_sourcecellmiddle) + ge_balance_positive_flat_read_sourcecellmiddlevalue))))))))) /\ (exists dfg_inner_flat_read_sourcecellproduct. ((exists sto_ap_flat_read_sourcecellproductinner sto_an_flat_read_sourcecellproductinner sto_bp_flat_read_sourcecellproductinner sto_bn_flat_read_sourcecellproductinner sto_cp_flat_read_sourcecellproductinner sto_cn_flat_read_sourcecellproductinner. (((((dfg_last_flat_read_sourcecell) = 2 * (sto_ap_flat_read_sourcecellproductinner) /\ (sto_an_flat_read_sourcecellproductinner) = 0) \/ exists ge_signed_half_flat_read_sourcecellproductinnerleft. (((dfg_last_flat_read_sourcecell) = 2 * ge_signed_half_flat_read_sourcecellproductinnerleft + 1 /\ (sto_ap_flat_read_sourcecellproductinner) = 0) /\ (sto_an_flat_read_sourcecellproductinner) = S ge_signed_half_flat_read_sourcecellproductinnerleft))) /\ ((((((dfg_value_flat_read_sourcecell) = 2 * (sto_bp_flat_read_sourcecellproductinner) /\ (sto_bn_flat_read_sourcecellproductinner) = 0) \/ exists ge_signed_half_flat_read_sourcecellproductinnerright. (((dfg_value_flat_read_sourcecell) = 2 * ge_signed_half_flat_read_sourcecellproductinnerright + 1 /\ (sto_bp_flat_read_sourcecellproductinner) = 0) /\ (sto_bn_flat_read_sourcecellproductinner) = S ge_signed_half_flat_read_sourcecellproductinnerright))) /\ ((((((dfg_inner_flat_read_sourcecellproduct) = 2 * (sto_cp_flat_read_sourcecellproductinner) /\ (sto_cn_flat_read_sourcecellproductinner) = 0) \/ exists ge_signed_half_flat_read_sourcecellproductinneroutput. (((dfg_inner_flat_read_sourcecellproduct) = 2 * ge_signed_half_flat_read_sourcecellproductinneroutput + 1 /\ (sto_cp_flat_read_sourcecellproductinner) = 0) /\ (sto_cn_flat_read_sourcecellproductinner) = S ge_signed_half_flat_read_sourcecellproductinneroutput))) /\ ((sto_ap_flat_read_sourcecellproductinner * sto_bp_flat_read_sourcecellproductinner + sto_an_flat_read_sourcecellproductinner * sto_bn_flat_read_sourcecellproductinner) + sto_cn_flat_read_sourcecellproductinner = (sto_ap_flat_read_sourcecellproductinner * sto_bn_flat_read_sourcecellproductinner + sto_an_flat_read_sourcecellproductinner * sto_bp_flat_read_sourcecellproductinner) + sto_cp_flat_read_sourcecellproductinner))))))) /\ (exists sto_ap_flat_read_sourcecellproductouter sto_an_flat_read_sourcecellproductouter sto_bp_flat_read_sourcecellproductouter sto_bn_flat_read_sourcecellproductouter sto_cp_flat_read_sourcecellproductouter sto_cn_flat_read_sourcecellproductouter. (((((dfg_first_flat_read_sourcecell) = 2 * (sto_ap_flat_read_sourcecellproductouter) /\ (sto_an_flat_read_sourcecellproductouter) = 0) \/ exists ge_signed_half_flat_read_sourcecellproductouterleft. (((dfg_first_flat_read_sourcecell) = 2 * ge_signed_half_flat_read_sourcecellproductouterleft + 1 /\ (sto_ap_flat_read_sourcecellproductouter) = 0) /\ (sto_an_flat_read_sourcecellproductouter) = S ge_signed_half_flat_read_sourcecellproductouterleft))) /\ ((((((dfg_inner_flat_read_sourcecellproduct) = 2 * (sto_bp_flat_read_sourcecellproductouter) /\ (sto_bn_flat_read_sourcecellproductouter) = 0) \/ exists ge_signed_half_flat_read_sourcecellproductouterright. (((dfg_inner_flat_read_sourcecellproduct) = 2 * ge_signed_half_flat_read_sourcecellproductouterright + 1 /\ (sto_bp_flat_read_sourcecellproductouter) = 0) /\ (sto_bn_flat_read_sourcecellproductouter) = S ge_signed_half_flat_read_sourcecellproductouterright))) /\ ((((((z) = 2 * (sto_cp_flat_read_sourcecellproductouter) /\ (sto_cn_flat_read_sourcecellproductouter) = 0) \/ exists ge_signed_half_flat_read_sourcecellproductouteroutput. (((z) = 2 * ge_signed_half_flat_read_sourcecellproductouteroutput + 1 /\ (sto_cp_flat_read_sourcecellproductouter) = 0) /\ (sto_cn_flat_read_sourcecellproductouter) = S ge_signed_half_flat_read_sourcecellproductouteroutput))) /\ ((sto_ap_flat_read_sourcecellproductouter * sto_bp_flat_read_sourcecellproductouter + sto_an_flat_read_sourcecellproductouter * sto_bn_flat_read_sourcecellproductouter) + sto_cn_flat_read_sourcecellproductouter = (sto_ap_flat_read_sourcecellproductouter * sto_bn_flat_read_sourcecellproductouter + sto_an_flat_read_sourcecellproductouter * sto_bp_flat_read_sourcecellproductouter) + sto_cp_flat_read_sourcecellproductouter))))))))))))))))))))) \/ ((((dfg_flat_row_flat_read_source)=0 \/ ((dfg_flat_column_flat_read_source)=0 \/ ~(exists pvs_factor_flat_read_sourcecellomittednondivisor. (n) = ((dfg_flat_row_flat_read_source)*(dfg_flat_column_flat_read_source)) * pvs_factor_flat_read_sourcecellomittednondivisor))) /\ ((z)=0)))))))) -> ((((~((a)=0)) /\ (((~((e)=0)) /\ (exists dfg_middle_flat_read_target dfg_first_flat_read_target dfg_last_flat_read_target dfg_value_flat_read_target. (((n)=((a)*(e))*dfg_middle_flat_read_target) /\ (((exists dst_positive_code_flat_read_targetfirst dst_positive_scale_flat_read_targetfirst dst_negative_code_flat_read_targetfirst dst_negative_scale_flat_read_targetfirst dst_positive_flat_read_targetfirst dst_negative_flat_read_targetfirst. (((F) = (((((dst_positive_code_flat_read_targetfirst) + (dst_positive_scale_flat_read_targetfirst)) * S ((dst_positive_code_flat_read_targetfirst) + (dst_positive_scale_flat_read_targetfirst)) + ((dst_positive_scale_flat_read_targetfirst) + (dst_positive_scale_flat_read_targetfirst))) + (((dst_negative_code_flat_read_targetfirst) + (dst_negative_scale_flat_read_targetfirst)) * S ((dst_negative_code_flat_read_targetfirst) + (dst_negative_scale_flat_read_targetfirst)) + ((dst_negative_scale_flat_read_targetfirst) + (dst_negative_scale_flat_read_targetfirst)))) * S ((((dst_positive_code_flat_read_targetfirst) + (dst_positive_scale_flat_read_targetfirst)) * S ((dst_positive_code_flat_read_targetfirst) + (dst_positive_scale_flat_read_targetfirst)) + ((dst_positive_scale_flat_read_targetfirst) + (dst_positive_scale_flat_read_targetfirst))) + (((dst_negative_code_flat_read_targetfirst) + (dst_negative_scale_flat_read_targetfirst)) * S ((dst_negative_code_flat_read_targetfirst) + (dst_negative_scale_flat_read_targetfirst)) + ((dst_negative_scale_flat_read_targetfirst) + (dst_negative_scale_flat_read_targetfirst)))) + ((((dst_negative_code_flat_read_targetfirst) + (dst_negative_scale_flat_read_targetfirst)) * S ((dst_negative_code_flat_read_targetfirst) + (dst_negative_scale_flat_read_targetfirst)) + ((dst_negative_scale_flat_read_targetfirst) + (dst_negative_scale_flat_read_targetfirst))) + (((dst_negative_code_flat_read_targetfirst) + (dst_negative_scale_flat_read_targetfirst)) * S ((dst_negative_code_flat_read_targetfirst) + (dst_negative_scale_flat_read_targetfirst)) + ((dst_negative_scale_flat_read_targetfirst) + (dst_negative_scale_flat_read_targetfirst)))))) /\ (((((exists ff_h_pvs_flat_read_targetfirstpositive. ff_h_pvs_flat_read_targetfirstpositive + S (dst_positive_flat_read_targetfirst) = S ((S (a)) * dst_positive_scale_flat_read_targetfirst)) /\ exists ff_q_pvs_flat_read_targetfirstpositive. dst_positive_code_flat_read_targetfirst = ff_q_pvs_flat_read_targetfirstpositive * S ((S (a)) * dst_positive_scale_flat_read_targetfirst) + (dst_positive_flat_read_targetfirst))) /\ (((((exists ff_h_pvs_flat_read_targetfirstnegative. ff_h_pvs_flat_read_targetfirstnegative + S (dst_negative_flat_read_targetfirst) = S ((S (a)) * dst_negative_scale_flat_read_targetfirst)) /\ exists ff_q_pvs_flat_read_targetfirstnegative. dst_negative_code_flat_read_targetfirst = ff_q_pvs_flat_read_targetfirstnegative * S ((S (a)) * dst_negative_scale_flat_read_targetfirst) + (dst_negative_flat_read_targetfirst))) /\ (exists ge_balance_positive_flat_read_targetfirstvalue ge_balance_negative_flat_read_targetfirstvalue. (((((dfg_first_flat_read_target) = 2 * (ge_balance_positive_flat_read_targetfirstvalue) /\ (ge_balance_negative_flat_read_targetfirstvalue) = 0) \/ exists ge_signed_half_flat_read_targetfirstvaluedecode. (((dfg_first_flat_read_target) = 2 * ge_signed_half_flat_read_targetfirstvaluedecode + 1 /\ (ge_balance_positive_flat_read_targetfirstvalue) = 0) /\ (ge_balance_negative_flat_read_targetfirstvalue) = S ge_signed_half_flat_read_targetfirstvaluedecode))) /\ ((dst_positive_flat_read_targetfirst) + ge_balance_negative_flat_read_targetfirstvalue = (dst_negative_flat_read_targetfirst) + ge_balance_positive_flat_read_targetfirstvalue))))))))) /\ (((exists dst_positive_code_flat_read_targetlast dst_positive_scale_flat_read_targetlast dst_negative_code_flat_read_targetlast dst_negative_scale_flat_read_targetlast dst_positive_flat_read_targetlast dst_negative_flat_read_targetlast. (((H) = (((((dst_positive_code_flat_read_targetlast) + (dst_positive_scale_flat_read_targetlast)) * S ((dst_positive_code_flat_read_targetlast) + (dst_positive_scale_flat_read_targetlast)) + ((dst_positive_scale_flat_read_targetlast) + (dst_positive_scale_flat_read_targetlast))) + (((dst_negative_code_flat_read_targetlast) + (dst_negative_scale_flat_read_targetlast)) * S ((dst_negative_code_flat_read_targetlast) + (dst_negative_scale_flat_read_targetlast)) + ((dst_negative_scale_flat_read_targetlast) + (dst_negative_scale_flat_read_targetlast)))) * S ((((dst_positive_code_flat_read_targetlast) + (dst_positive_scale_flat_read_targetlast)) * S ((dst_positive_code_flat_read_targetlast) + (dst_positive_scale_flat_read_targetlast)) + ((dst_positive_scale_flat_read_targetlast) + (dst_positive_scale_flat_read_targetlast))) + (((dst_negative_code_flat_read_targetlast) + (dst_negative_scale_flat_read_targetlast)) * S ((dst_negative_code_flat_read_targetlast) + (dst_negative_scale_flat_read_targetlast)) + ((dst_negative_scale_flat_read_targetlast) + (dst_negative_scale_flat_read_targetlast)))) + ((((dst_negative_code_flat_read_targetlast) + (dst_negative_scale_flat_read_targetlast)) * S ((dst_negative_code_flat_read_targetlast) + (dst_negative_scale_flat_read_targetlast)) + ((dst_negative_scale_flat_read_targetlast) + (dst_negative_scale_flat_read_targetlast))) + (((dst_negative_code_flat_read_targetlast) + (dst_negative_scale_flat_read_targetlast)) * S ((dst_negative_code_flat_read_targetlast) + (dst_negative_scale_flat_read_targetlast)) + ((dst_negative_scale_flat_read_targetlast) + (dst_negative_scale_flat_read_targetlast)))))) /\ (((((exists ff_h_pvs_flat_read_targetlastpositive. ff_h_pvs_flat_read_targetlastpositive + S (dst_positive_flat_read_targetlast) = S ((S (e)) * dst_positive_scale_flat_read_targetlast)) /\ exists ff_q_pvs_flat_read_targetlastpositive. dst_positive_code_flat_read_targetlast = ff_q_pvs_flat_read_targetlastpositive * S ((S (e)) * dst_positive_scale_flat_read_targetlast) + (dst_positive_flat_read_targetlast))) /\ (((((exists ff_h_pvs_flat_read_targetlastnegative. ff_h_pvs_flat_read_targetlastnegative + S (dst_negative_flat_read_targetlast) = S ((S (e)) * dst_negative_scale_flat_read_targetlast)) /\ exists ff_q_pvs_flat_read_targetlastnegative. dst_negative_code_flat_read_targetlast = ff_q_pvs_flat_read_targetlastnegative * S ((S (e)) * dst_negative_scale_flat_read_targetlast) + (dst_negative_flat_read_targetlast))) /\ (exists ge_balance_positive_flat_read_targetlastvalue ge_balance_negative_flat_read_targetlastvalue. (((((dfg_last_flat_read_target) = 2 * (ge_balance_positive_flat_read_targetlastvalue) /\ (ge_balance_negative_flat_read_targetlastvalue) = 0) \/ exists ge_signed_half_flat_read_targetlastvaluedecode. (((dfg_last_flat_read_target) = 2 * ge_signed_half_flat_read_targetlastvaluedecode + 1 /\ (ge_balance_positive_flat_read_targetlastvalue) = 0) /\ (ge_balance_negative_flat_read_targetlastvalue) = S ge_signed_half_flat_read_targetlastvaluedecode))) /\ ((dst_positive_flat_read_targetlast) + ge_balance_negative_flat_read_targetlastvalue = (dst_negative_flat_read_targetlast) + ge_balance_positive_flat_read_targetlastvalue))))))))) /\ (((exists dst_positive_code_flat_read_targetmiddle dst_positive_scale_flat_read_targetmiddle dst_negative_code_flat_read_targetmiddle dst_negative_scale_flat_read_targetmiddle dst_positive_flat_read_targetmiddle dst_negative_flat_read_targetmiddle. (((G) = (((((dst_positive_code_flat_read_targetmiddle) + (dst_positive_scale_flat_read_targetmiddle)) * S ((dst_positive_code_flat_read_targetmiddle) + (dst_positive_scale_flat_read_targetmiddle)) + ((dst_positive_scale_flat_read_targetmiddle) + (dst_positive_scale_flat_read_targetmiddle))) + (((dst_negative_code_flat_read_targetmiddle) + (dst_negative_scale_flat_read_targetmiddle)) * S ((dst_negative_code_flat_read_targetmiddle) + (dst_negative_scale_flat_read_targetmiddle)) + ((dst_negative_scale_flat_read_targetmiddle) + (dst_negative_scale_flat_read_targetmiddle)))) * S ((((dst_positive_code_flat_read_targetmiddle) + (dst_positive_scale_flat_read_targetmiddle)) * S ((dst_positive_code_flat_read_targetmiddle) + (dst_positive_scale_flat_read_targetmiddle)) + ((dst_positive_scale_flat_read_targetmiddle) + (dst_positive_scale_flat_read_targetmiddle))) + (((dst_negative_code_flat_read_targetmiddle) + (dst_negative_scale_flat_read_targetmiddle)) * S ((dst_negative_code_flat_read_targetmiddle) + (dst_negative_scale_flat_read_targetmiddle)) + ((dst_negative_scale_flat_read_targetmiddle) + (dst_negative_scale_flat_read_targetmiddle)))) + ((((dst_negative_code_flat_read_targetmiddle) + (dst_negative_scale_flat_read_targetmiddle)) * S ((dst_negative_code_flat_read_targetmiddle) + (dst_negative_scale_flat_read_targetmiddle)) + ((dst_negative_scale_flat_read_targetmiddle) + (dst_negative_scale_flat_read_targetmiddle))) + (((dst_negative_code_flat_read_targetmiddle) + (dst_negative_scale_flat_read_targetmiddle)) * S ((dst_negative_code_flat_read_targetmiddle) + (dst_negative_scale_flat_read_targetmiddle)) + ((dst_negative_scale_flat_read_targetmiddle) + (dst_negative_scale_flat_read_targetmiddle)))))) /\ (((((exists ff_h_pvs_flat_read_targetmiddlepositive. ff_h_pvs_flat_read_targetmiddlepositive + S (dst_positive_flat_read_targetmiddle) = S ((S (dfg_middle_flat_read_target)) * dst_positive_scale_flat_read_targetmiddle)) /\ exists ff_q_pvs_flat_read_targetmiddlepositive. dst_positive_code_flat_read_targetmiddle = ff_q_pvs_flat_read_targetmiddlepositive * S ((S (dfg_middle_flat_read_target)) * dst_positive_scale_flat_read_targetmiddle) + (dst_positive_flat_read_targetmiddle))) /\ (((((exists ff_h_pvs_flat_read_targetmiddlenegative. ff_h_pvs_flat_read_targetmiddlenegative + S (dst_negative_flat_read_targetmiddle) = S ((S (dfg_middle_flat_read_target)) * dst_negative_scale_flat_read_targetmiddle)) /\ exists ff_q_pvs_flat_read_targetmiddlenegative. dst_negative_code_flat_read_targetmiddle = ff_q_pvs_flat_read_targetmiddlenegative * S ((S (dfg_middle_flat_read_target)) * dst_negative_scale_flat_read_targetmiddle) + (dst_negative_flat_read_targetmiddle))) /\ (exists ge_balance_positive_flat_read_targetmiddlevalue ge_balance_negative_flat_read_targetmiddlevalue. (((((dfg_value_flat_read_target) = 2 * (ge_balance_positive_flat_read_targetmiddlevalue) /\ (ge_balance_negative_flat_read_targetmiddlevalue) = 0) \/ exists ge_signed_half_flat_read_targetmiddlevaluedecode. (((dfg_value_flat_read_target) = 2 * ge_signed_half_flat_read_targetmiddlevaluedecode + 1 /\ (ge_balance_positive_flat_read_targetmiddlevalue) = 0) /\ (ge_balance_negative_flat_read_targetmiddlevalue) = S ge_signed_half_flat_read_targetmiddlevaluedecode))) /\ ((dst_positive_flat_read_targetmiddle) + ge_balance_negative_flat_read_targetmiddlevalue = (dst_negative_flat_read_targetmiddle) + ge_balance_positive_flat_read_targetmiddlevalue))))))))) /\ (exists dfg_inner_flat_read_targetproduct. ((exists sto_ap_flat_read_targetproductinner sto_an_flat_read_targetproductinner sto_bp_flat_read_targetproductinner sto_bn_flat_read_targetproductinner sto_cp_flat_read_targetproductinner sto_cn_flat_read_targetproductinner. (((((dfg_last_flat_read_target) = 2 * (sto_ap_flat_read_targetproductinner) /\ (sto_an_flat_read_targetproductinner) = 0) \/ exists ge_signed_half_flat_read_targetproductinnerleft. (((dfg_last_flat_read_target) = 2 * ge_signed_half_flat_read_targetproductinnerleft + 1 /\ (sto_ap_flat_read_targetproductinner) = 0) /\ (sto_an_flat_read_targetproductinner) = S ge_signed_half_flat_read_targetproductinnerleft))) /\ ((((((dfg_value_flat_read_target) = 2 * (sto_bp_flat_read_targetproductinner) /\ (sto_bn_flat_read_targetproductinner) = 0) \/ exists ge_signed_half_flat_read_targetproductinnerright. (((dfg_value_flat_read_target) = 2 * ge_signed_half_flat_read_targetproductinnerright + 1 /\ (sto_bp_flat_read_targetproductinner) = 0) /\ (sto_bn_flat_read_targetproductinner) = S ge_signed_half_flat_read_targetproductinnerright))) /\ ((((((dfg_inner_flat_read_targetproduct) = 2 * (sto_cp_flat_read_targetproductinner) /\ (sto_cn_flat_read_targetproductinner) = 0) \/ exists ge_signed_half_flat_read_targetproductinneroutput. (((dfg_inner_flat_read_targetproduct) = 2 * ge_signed_half_flat_read_targetproductinneroutput + 1 /\ (sto_cp_flat_read_targetproductinner) = 0) /\ (sto_cn_flat_read_targetproductinner) = S ge_signed_half_flat_read_targetproductinneroutput))) /\ ((sto_ap_flat_read_targetproductinner * sto_bp_flat_read_targetproductinner + sto_an_flat_read_targetproductinner * sto_bn_flat_read_targetproductinner) + sto_cn_flat_read_targetproductinner = (sto_ap_flat_read_targetproductinner * sto_bn_flat_read_targetproductinner + sto_an_flat_read_targetproductinner * sto_bp_flat_read_targetproductinner) + sto_cp_flat_read_targetproductinner))))))) /\ (exists sto_ap_flat_read_targetproductouter sto_an_flat_read_targetproductouter sto_bp_flat_read_targetproductouter sto_bn_flat_read_targetproductouter sto_cp_flat_read_targetproductouter sto_cn_flat_read_targetproductouter. (((((dfg_first_flat_read_target) = 2 * (sto_ap_flat_read_targetproductouter) /\ (sto_an_flat_read_targetproductouter) = 0) \/ exists ge_signed_half_flat_read_targetproductouterleft. (((dfg_first_flat_read_target) = 2 * ge_signed_half_flat_read_targetproductouterleft + 1 /\ (sto_ap_flat_read_targetproductouter) = 0) /\ (sto_an_flat_read_targetproductouter) = S ge_signed_half_flat_read_targetproductouterleft))) /\ ((((((dfg_inner_flat_read_targetproduct) = 2 * (sto_bp_flat_read_targetproductouter) /\ (sto_bn_flat_read_targetproductouter) = 0) \/ exists ge_signed_half_flat_read_targetproductouterright. (((dfg_inner_flat_read_targetproduct) = 2 * ge_signed_half_flat_read_targetproductouterright + 1 /\ (sto_bp_flat_read_targetproductouter) = 0) /\ (sto_bn_flat_read_targetproductouter) = S ge_signed_half_flat_read_targetproductouterright))) /\ ((((((z) = 2 * (sto_cp_flat_read_targetproductouter) /\ (sto_cn_flat_read_targetproductouter) = 0) \/ exists ge_signed_half_flat_read_targetproductouteroutput. (((z) = 2 * ge_signed_half_flat_read_targetproductouteroutput + 1 /\ (sto_cp_flat_read_targetproductouter) = 0) /\ (sto_cn_flat_read_targetproductouter) = S ge_signed_half_flat_read_targetproductouteroutput))) /\ ((sto_ap_flat_read_targetproductouter * sto_bp_flat_read_targetproductouter + sto_an_flat_read_targetproductouter * sto_bn_flat_read_targetproductouter) + sto_cn_flat_read_targetproductouter = (sto_ap_flat_read_targetproductouter * sto_bn_flat_read_targetproductouter + sto_an_flat_read_targetproductouter * sto_bp_flat_read_targetproductouter) + sto_cp_flat_read_targetproductouter))))))))))))))))))))) \/ ((((a)=0 \/ ((e)=0 \/ ~(exists pvs_factor_flat_read_targetomittednondivisor. (n) = ((a)*(e)) * pvs_factor_flat_read_targetomittednondivisor))) /\ ((z)=0))))

Complete tactic proof in conservative notation

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

43 script commands · 9 reading checkpoints · 1 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.

01Fix variables and assumptionsL1–9

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

  1. L1
    intro F
  2. L2
    intro G
  3. L3
    intro H
  4. L4
    intro n
  5. L5
    intro a
  6. L6
    intro e
  7. L7
    intro z
  8. L8
    intro he
  9. L9
    intro hv
02Separate the logical casesL10–13

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

  1. L10
    cases hv
  2. L11
    cases hv_witness
  3. L12
    cases hv_witness_witness
  4. L13
    cases hv_witness_witness_right
03Establish hcoordinatesL14–23

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

  1. L14
    have hcoordinates : x=a /\ x1=e
  2. L15
    specialize division_remainder_unique (S n)
  3. L16
    specialize division_remainder_unique ((S (n))*(a)+(e))
  4. L17
    specialize division_remainder_unique (x)
  5. L18
    specialize division_remainder_unique (x1)
  6. L19
    specialize division_remainder_unique (a)
  7. L20
    specialize division_remainder_unique (e)
  8. L21
    apply division_remainder_unique
  9. L22
    exact hv_witness_witness_left
  10. L23
    exact hv_witness_witness_right_left
04Calculate and transport equalitiesL24–24

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

  1. L24
    refl
05Use earlier factsL25–25

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

  1. L25
    exact he
06Separate the logical casesL26–26

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

  1. L26
    cases hcoordinates
07Calculate and transport equalitiesL27–36

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

  1. L27
    rewrite hcoordinates_left at hv_witness_witness_right_right
  2. L28
    rewrite hcoordinates_left at hv_witness_witness_right_right
  3. L29
    rewrite hcoordinates_left at hv_witness_witness_right_right
  4. L30
    rewrite hcoordinates_left at hv_witness_witness_right_right
  5. L31
    rewrite hcoordinates_left at hv_witness_witness_right_right
  6. L32
    rewrite hcoordinates_left at hv_witness_witness_right_right
  7. L33
    rewrite hcoordinates_left at hv_witness_witness_right_right
  8. L34
    rewrite hcoordinates_left at hv_witness_witness_right_right
  9. L35
    rewrite hcoordinates_right at hv_witness_witness_right_right
  10. L36
    rewrite hcoordinates_right at hv_witness_witness_right_right
08Calculate and transport equalitiesL37–42

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

  1. L37
    rewrite hcoordinates_right at hv_witness_witness_right_right
  2. L38
    rewrite hcoordinates_right at hv_witness_witness_right_right
  3. L39
    rewrite hcoordinates_right at hv_witness_witness_right_right
  4. L40
    rewrite hcoordinates_right at hv_witness_witness_right_right
  5. L41
    rewrite hcoordinates_right at hv_witness_witness_right_right
  6. L42
    rewrite hcoordinates_right at hv_witness_witness_right_right
09Use earlier factsL43–43

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

  1. L43
    exact hv_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 43 lines
  1. 0001intro F
  2. 0002intro G
  3. 0003intro H
  4. 0004intro n
  5. 0005intro a
  6. 0006intro e
  7. 0007intro z
  8. 0008intro he
  9. 0009intro hv
  10. 0010cases hv
  11. 0011cases hv_witness
  12. 0012cases hv_witness_witness
  13. 0013cases hv_witness_witness_right
  14. 0014have hcoordinates : x=a /\ x1=e
  15. 0015specialize division_remainder_unique (S n)
  16. 0016specialize division_remainder_unique ((S (n))*(a)+(e))
  17. 0017specialize division_remainder_unique (x)
  18. 0018specialize division_remainder_unique (x1)
  19. 0019specialize division_remainder_unique (a)
  20. 0020specialize division_remainder_unique (e)
  21. 0021apply division_remainder_unique
  22. 0022exact hv_witness_witness_left
  23. 0023exact hv_witness_witness_right_left
  24. 0024refl
  25. 0025exact he
  26. 0026cases hcoordinates
  27. 0027rewrite hcoordinates_left at hv_witness_witness_right_right
  28. 0028rewrite hcoordinates_left at hv_witness_witness_right_right
  29. 0029rewrite hcoordinates_left at hv_witness_witness_right_right
  30. 0030rewrite hcoordinates_left at hv_witness_witness_right_right
  31. 0031rewrite hcoordinates_left at hv_witness_witness_right_right
  32. 0032rewrite hcoordinates_left at hv_witness_witness_right_right
  33. 0033rewrite hcoordinates_left at hv_witness_witness_right_right
  34. 0034rewrite hcoordinates_left at hv_witness_witness_right_right
  35. 0035rewrite hcoordinates_right at hv_witness_witness_right_right
  36. 0036rewrite hcoordinates_right at hv_witness_witness_right_right
  37. 0037rewrite hcoordinates_right at hv_witness_witness_right_right
  38. 0038rewrite hcoordinates_right at hv_witness_witness_right_right
  39. 0039rewrite hcoordinates_right at hv_witness_witness_right_right
  40. 0040rewrite hcoordinates_right at hv_witness_witness_right_right
  41. 0041rewrite hcoordinates_right at hv_witness_witness_right_right
  42. 0042rewrite hcoordinates_right at hv_witness_witness_right_right
  43. 0043exact hv_witness_witness_right_right