DF0004

dirichlet_grid_entry_factor_product

Nonzero product cancellation identifies the supplied middle factor; canonical input lookups recover both actual signed products.

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. ∀ c. ∀ u. ∀ v. ∀ w. ∀ z. ¬a = 0 → ¬e = 0 → n = a · e · c → ArithAt(F,a,u) → ArithAt(H,e,v) → ArithAt(G,c,w) → DirichletGridEntry(F,G,H,n,a,e,z) → ∃ x. SignedMul(v,w,x) ∧ SignedMul(u,x,z)

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

Definition DAG

SignedMul(a,b,c) · 2ArithAt(F,i,z) · 3DirichletGridEntry(F,G,H,n,a,e,z) · 1

Actual proof prerequisites

mul_left_cancel_nonzero · checked external prerequisitemul_ne_zero · checked external prerequisitedivisor_signed_table_at_functional · checked external prerequisite
Original expanded first-order statement 
forall F G H n a e c u v w z. ~(a=0) -> ~(e=0) -> n=(a*e)*c -> (exists dst_positive_code_read_first dst_positive_scale_read_first dst_negative_code_read_first dst_negative_scale_read_first dst_positive_read_first dst_negative_read_first. (((F) = (((((dst_positive_code_read_first) + (dst_positive_scale_read_first)) * S ((dst_positive_code_read_first) + (dst_positive_scale_read_first)) + ((dst_positive_scale_read_first) + (dst_positive_scale_read_first))) + (((dst_negative_code_read_first) + (dst_negative_scale_read_first)) * S ((dst_negative_code_read_first) + (dst_negative_scale_read_first)) + ((dst_negative_scale_read_first) + (dst_negative_scale_read_first)))) * S ((((dst_positive_code_read_first) + (dst_positive_scale_read_first)) * S ((dst_positive_code_read_first) + (dst_positive_scale_read_first)) + ((dst_positive_scale_read_first) + (dst_positive_scale_read_first))) + (((dst_negative_code_read_first) + (dst_negative_scale_read_first)) * S ((dst_negative_code_read_first) + (dst_negative_scale_read_first)) + ((dst_negative_scale_read_first) + (dst_negative_scale_read_first)))) + ((((dst_negative_code_read_first) + (dst_negative_scale_read_first)) * S ((dst_negative_code_read_first) + (dst_negative_scale_read_first)) + ((dst_negative_scale_read_first) + (dst_negative_scale_read_first))) + (((dst_negative_code_read_first) + (dst_negative_scale_read_first)) * S ((dst_negative_code_read_first) + (dst_negative_scale_read_first)) + ((dst_negative_scale_read_first) + (dst_negative_scale_read_first)))))) /\ (((((exists ff_h_pvs_read_firstpositive. ff_h_pvs_read_firstpositive + S (dst_positive_read_first) = S ((S (a)) * dst_positive_scale_read_first)) /\ exists ff_q_pvs_read_firstpositive. dst_positive_code_read_first = ff_q_pvs_read_firstpositive * S ((S (a)) * dst_positive_scale_read_first) + (dst_positive_read_first))) /\ (((((exists ff_h_pvs_read_firstnegative. ff_h_pvs_read_firstnegative + S (dst_negative_read_first) = S ((S (a)) * dst_negative_scale_read_first)) /\ exists ff_q_pvs_read_firstnegative. dst_negative_code_read_first = ff_q_pvs_read_firstnegative * S ((S (a)) * dst_negative_scale_read_first) + (dst_negative_read_first))) /\ (exists ge_balance_positive_read_firstvalue ge_balance_negative_read_firstvalue. (((((u) = 2 * (ge_balance_positive_read_firstvalue) /\ (ge_balance_negative_read_firstvalue) = 0) \/ exists ge_signed_half_read_firstvaluedecode. (((u) = 2 * ge_signed_half_read_firstvaluedecode + 1 /\ (ge_balance_positive_read_firstvalue) = 0) /\ (ge_balance_negative_read_firstvalue) = S ge_signed_half_read_firstvaluedecode))) /\ ((dst_positive_read_first) + ge_balance_negative_read_firstvalue = (dst_negative_read_first) + ge_balance_positive_read_firstvalue))))))))) -> (exists dst_positive_code_read_last dst_positive_scale_read_last dst_negative_code_read_last dst_negative_scale_read_last dst_positive_read_last dst_negative_read_last. (((H) = (((((dst_positive_code_read_last) + (dst_positive_scale_read_last)) * S ((dst_positive_code_read_last) + (dst_positive_scale_read_last)) + ((dst_positive_scale_read_last) + (dst_positive_scale_read_last))) + (((dst_negative_code_read_last) + (dst_negative_scale_read_last)) * S ((dst_negative_code_read_last) + (dst_negative_scale_read_last)) + ((dst_negative_scale_read_last) + (dst_negative_scale_read_last)))) * S ((((dst_positive_code_read_last) + (dst_positive_scale_read_last)) * S ((dst_positive_code_read_last) + (dst_positive_scale_read_last)) + ((dst_positive_scale_read_last) + (dst_positive_scale_read_last))) + (((dst_negative_code_read_last) + (dst_negative_scale_read_last)) * S ((dst_negative_code_read_last) + (dst_negative_scale_read_last)) + ((dst_negative_scale_read_last) + (dst_negative_scale_read_last)))) + ((((dst_negative_code_read_last) + (dst_negative_scale_read_last)) * S ((dst_negative_code_read_last) + (dst_negative_scale_read_last)) + ((dst_negative_scale_read_last) + (dst_negative_scale_read_last))) + (((dst_negative_code_read_last) + (dst_negative_scale_read_last)) * S ((dst_negative_code_read_last) + (dst_negative_scale_read_last)) + ((dst_negative_scale_read_last) + (dst_negative_scale_read_last)))))) /\ (((((exists ff_h_pvs_read_lastpositive. ff_h_pvs_read_lastpositive + S (dst_positive_read_last) = S ((S (e)) * dst_positive_scale_read_last)) /\ exists ff_q_pvs_read_lastpositive. dst_positive_code_read_last = ff_q_pvs_read_lastpositive * S ((S (e)) * dst_positive_scale_read_last) + (dst_positive_read_last))) /\ (((((exists ff_h_pvs_read_lastnegative. ff_h_pvs_read_lastnegative + S (dst_negative_read_last) = S ((S (e)) * dst_negative_scale_read_last)) /\ exists ff_q_pvs_read_lastnegative. dst_negative_code_read_last = ff_q_pvs_read_lastnegative * S ((S (e)) * dst_negative_scale_read_last) + (dst_negative_read_last))) /\ (exists ge_balance_positive_read_lastvalue ge_balance_negative_read_lastvalue. (((((v) = 2 * (ge_balance_positive_read_lastvalue) /\ (ge_balance_negative_read_lastvalue) = 0) \/ exists ge_signed_half_read_lastvaluedecode. (((v) = 2 * ge_signed_half_read_lastvaluedecode + 1 /\ (ge_balance_positive_read_lastvalue) = 0) /\ (ge_balance_negative_read_lastvalue) = S ge_signed_half_read_lastvaluedecode))) /\ ((dst_positive_read_last) + ge_balance_negative_read_lastvalue = (dst_negative_read_last) + ge_balance_positive_read_lastvalue))))))))) -> (exists dst_positive_code_read_middle dst_positive_scale_read_middle dst_negative_code_read_middle dst_negative_scale_read_middle dst_positive_read_middle dst_negative_read_middle. (((G) = (((((dst_positive_code_read_middle) + (dst_positive_scale_read_middle)) * S ((dst_positive_code_read_middle) + (dst_positive_scale_read_middle)) + ((dst_positive_scale_read_middle) + (dst_positive_scale_read_middle))) + (((dst_negative_code_read_middle) + (dst_negative_scale_read_middle)) * S ((dst_negative_code_read_middle) + (dst_negative_scale_read_middle)) + ((dst_negative_scale_read_middle) + (dst_negative_scale_read_middle)))) * S ((((dst_positive_code_read_middle) + (dst_positive_scale_read_middle)) * S ((dst_positive_code_read_middle) + (dst_positive_scale_read_middle)) + ((dst_positive_scale_read_middle) + (dst_positive_scale_read_middle))) + (((dst_negative_code_read_middle) + (dst_negative_scale_read_middle)) * S ((dst_negative_code_read_middle) + (dst_negative_scale_read_middle)) + ((dst_negative_scale_read_middle) + (dst_negative_scale_read_middle)))) + ((((dst_negative_code_read_middle) + (dst_negative_scale_read_middle)) * S ((dst_negative_code_read_middle) + (dst_negative_scale_read_middle)) + ((dst_negative_scale_read_middle) + (dst_negative_scale_read_middle))) + (((dst_negative_code_read_middle) + (dst_negative_scale_read_middle)) * S ((dst_negative_code_read_middle) + (dst_negative_scale_read_middle)) + ((dst_negative_scale_read_middle) + (dst_negative_scale_read_middle)))))) /\ (((((exists ff_h_pvs_read_middlepositive. ff_h_pvs_read_middlepositive + S (dst_positive_read_middle) = S ((S (c)) * dst_positive_scale_read_middle)) /\ exists ff_q_pvs_read_middlepositive. dst_positive_code_read_middle = ff_q_pvs_read_middlepositive * S ((S (c)) * dst_positive_scale_read_middle) + (dst_positive_read_middle))) /\ (((((exists ff_h_pvs_read_middlenegative. ff_h_pvs_read_middlenegative + S (dst_negative_read_middle) = S ((S (c)) * dst_negative_scale_read_middle)) /\ exists ff_q_pvs_read_middlenegative. dst_negative_code_read_middle = ff_q_pvs_read_middlenegative * S ((S (c)) * dst_negative_scale_read_middle) + (dst_negative_read_middle))) /\ (exists ge_balance_positive_read_middlevalue ge_balance_negative_read_middlevalue. (((((w) = 2 * (ge_balance_positive_read_middlevalue) /\ (ge_balance_negative_read_middlevalue) = 0) \/ exists ge_signed_half_read_middlevaluedecode. (((w) = 2 * ge_signed_half_read_middlevaluedecode + 1 /\ (ge_balance_positive_read_middlevalue) = 0) /\ (ge_balance_negative_read_middlevalue) = S ge_signed_half_read_middlevaluedecode))) /\ ((dst_positive_read_middle) + ge_balance_negative_read_middlevalue = (dst_negative_read_middle) + ge_balance_positive_read_middlevalue))))))))) -> ((((~((a)=0)) /\ (((~((e)=0)) /\ (exists dfg_middle_read_cell dfg_first_read_cell dfg_last_read_cell dfg_value_read_cell. (((n)=((a)*(e))*dfg_middle_read_cell) /\ (((exists dst_positive_code_read_cellfirst dst_positive_scale_read_cellfirst dst_negative_code_read_cellfirst dst_negative_scale_read_cellfirst dst_positive_read_cellfirst dst_negative_read_cellfirst. (((F) = (((((dst_positive_code_read_cellfirst) + (dst_positive_scale_read_cellfirst)) * S ((dst_positive_code_read_cellfirst) + (dst_positive_scale_read_cellfirst)) + ((dst_positive_scale_read_cellfirst) + (dst_positive_scale_read_cellfirst))) + (((dst_negative_code_read_cellfirst) + (dst_negative_scale_read_cellfirst)) * S ((dst_negative_code_read_cellfirst) + (dst_negative_scale_read_cellfirst)) + ((dst_negative_scale_read_cellfirst) + (dst_negative_scale_read_cellfirst)))) * S ((((dst_positive_code_read_cellfirst) + (dst_positive_scale_read_cellfirst)) * S ((dst_positive_code_read_cellfirst) + (dst_positive_scale_read_cellfirst)) + ((dst_positive_scale_read_cellfirst) + (dst_positive_scale_read_cellfirst))) + (((dst_negative_code_read_cellfirst) + (dst_negative_scale_read_cellfirst)) * S ((dst_negative_code_read_cellfirst) + (dst_negative_scale_read_cellfirst)) + ((dst_negative_scale_read_cellfirst) + (dst_negative_scale_read_cellfirst)))) + ((((dst_negative_code_read_cellfirst) + (dst_negative_scale_read_cellfirst)) * S ((dst_negative_code_read_cellfirst) + (dst_negative_scale_read_cellfirst)) + ((dst_negative_scale_read_cellfirst) + (dst_negative_scale_read_cellfirst))) + (((dst_negative_code_read_cellfirst) + (dst_negative_scale_read_cellfirst)) * S ((dst_negative_code_read_cellfirst) + (dst_negative_scale_read_cellfirst)) + ((dst_negative_scale_read_cellfirst) + (dst_negative_scale_read_cellfirst)))))) /\ (((((exists ff_h_pvs_read_cellfirstpositive. ff_h_pvs_read_cellfirstpositive + S (dst_positive_read_cellfirst) = S ((S (a)) * dst_positive_scale_read_cellfirst)) /\ exists ff_q_pvs_read_cellfirstpositive. dst_positive_code_read_cellfirst = ff_q_pvs_read_cellfirstpositive * S ((S (a)) * dst_positive_scale_read_cellfirst) + (dst_positive_read_cellfirst))) /\ (((((exists ff_h_pvs_read_cellfirstnegative. ff_h_pvs_read_cellfirstnegative + S (dst_negative_read_cellfirst) = S ((S (a)) * dst_negative_scale_read_cellfirst)) /\ exists ff_q_pvs_read_cellfirstnegative. dst_negative_code_read_cellfirst = ff_q_pvs_read_cellfirstnegative * S ((S (a)) * dst_negative_scale_read_cellfirst) + (dst_negative_read_cellfirst))) /\ (exists ge_balance_positive_read_cellfirstvalue ge_balance_negative_read_cellfirstvalue. (((((dfg_first_read_cell) = 2 * (ge_balance_positive_read_cellfirstvalue) /\ (ge_balance_negative_read_cellfirstvalue) = 0) \/ exists ge_signed_half_read_cellfirstvaluedecode. (((dfg_first_read_cell) = 2 * ge_signed_half_read_cellfirstvaluedecode + 1 /\ (ge_balance_positive_read_cellfirstvalue) = 0) /\ (ge_balance_negative_read_cellfirstvalue) = S ge_signed_half_read_cellfirstvaluedecode))) /\ ((dst_positive_read_cellfirst) + ge_balance_negative_read_cellfirstvalue = (dst_negative_read_cellfirst) + ge_balance_positive_read_cellfirstvalue))))))))) /\ (((exists dst_positive_code_read_celllast dst_positive_scale_read_celllast dst_negative_code_read_celllast dst_negative_scale_read_celllast dst_positive_read_celllast dst_negative_read_celllast. (((H) = (((((dst_positive_code_read_celllast) + (dst_positive_scale_read_celllast)) * S ((dst_positive_code_read_celllast) + (dst_positive_scale_read_celllast)) + ((dst_positive_scale_read_celllast) + (dst_positive_scale_read_celllast))) + (((dst_negative_code_read_celllast) + (dst_negative_scale_read_celllast)) * S ((dst_negative_code_read_celllast) + (dst_negative_scale_read_celllast)) + ((dst_negative_scale_read_celllast) + (dst_negative_scale_read_celllast)))) * S ((((dst_positive_code_read_celllast) + (dst_positive_scale_read_celllast)) * S ((dst_positive_code_read_celllast) + (dst_positive_scale_read_celllast)) + ((dst_positive_scale_read_celllast) + (dst_positive_scale_read_celllast))) + (((dst_negative_code_read_celllast) + (dst_negative_scale_read_celllast)) * S ((dst_negative_code_read_celllast) + (dst_negative_scale_read_celllast)) + ((dst_negative_scale_read_celllast) + (dst_negative_scale_read_celllast)))) + ((((dst_negative_code_read_celllast) + (dst_negative_scale_read_celllast)) * S ((dst_negative_code_read_celllast) + (dst_negative_scale_read_celllast)) + ((dst_negative_scale_read_celllast) + (dst_negative_scale_read_celllast))) + (((dst_negative_code_read_celllast) + (dst_negative_scale_read_celllast)) * S ((dst_negative_code_read_celllast) + (dst_negative_scale_read_celllast)) + ((dst_negative_scale_read_celllast) + (dst_negative_scale_read_celllast)))))) /\ (((((exists ff_h_pvs_read_celllastpositive. ff_h_pvs_read_celllastpositive + S (dst_positive_read_celllast) = S ((S (e)) * dst_positive_scale_read_celllast)) /\ exists ff_q_pvs_read_celllastpositive. dst_positive_code_read_celllast = ff_q_pvs_read_celllastpositive * S ((S (e)) * dst_positive_scale_read_celllast) + (dst_positive_read_celllast))) /\ (((((exists ff_h_pvs_read_celllastnegative. ff_h_pvs_read_celllastnegative + S (dst_negative_read_celllast) = S ((S (e)) * dst_negative_scale_read_celllast)) /\ exists ff_q_pvs_read_celllastnegative. dst_negative_code_read_celllast = ff_q_pvs_read_celllastnegative * S ((S (e)) * dst_negative_scale_read_celllast) + (dst_negative_read_celllast))) /\ (exists ge_balance_positive_read_celllastvalue ge_balance_negative_read_celllastvalue. (((((dfg_last_read_cell) = 2 * (ge_balance_positive_read_celllastvalue) /\ (ge_balance_negative_read_celllastvalue) = 0) \/ exists ge_signed_half_read_celllastvaluedecode. (((dfg_last_read_cell) = 2 * ge_signed_half_read_celllastvaluedecode + 1 /\ (ge_balance_positive_read_celllastvalue) = 0) /\ (ge_balance_negative_read_celllastvalue) = S ge_signed_half_read_celllastvaluedecode))) /\ ((dst_positive_read_celllast) + ge_balance_negative_read_celllastvalue = (dst_negative_read_celllast) + ge_balance_positive_read_celllastvalue))))))))) /\ (((exists dst_positive_code_read_cellmiddle dst_positive_scale_read_cellmiddle dst_negative_code_read_cellmiddle dst_negative_scale_read_cellmiddle dst_positive_read_cellmiddle dst_negative_read_cellmiddle. (((G) = (((((dst_positive_code_read_cellmiddle) + (dst_positive_scale_read_cellmiddle)) * S ((dst_positive_code_read_cellmiddle) + (dst_positive_scale_read_cellmiddle)) + ((dst_positive_scale_read_cellmiddle) + (dst_positive_scale_read_cellmiddle))) + (((dst_negative_code_read_cellmiddle) + (dst_negative_scale_read_cellmiddle)) * S ((dst_negative_code_read_cellmiddle) + (dst_negative_scale_read_cellmiddle)) + ((dst_negative_scale_read_cellmiddle) + (dst_negative_scale_read_cellmiddle)))) * S ((((dst_positive_code_read_cellmiddle) + (dst_positive_scale_read_cellmiddle)) * S ((dst_positive_code_read_cellmiddle) + (dst_positive_scale_read_cellmiddle)) + ((dst_positive_scale_read_cellmiddle) + (dst_positive_scale_read_cellmiddle))) + (((dst_negative_code_read_cellmiddle) + (dst_negative_scale_read_cellmiddle)) * S ((dst_negative_code_read_cellmiddle) + (dst_negative_scale_read_cellmiddle)) + ((dst_negative_scale_read_cellmiddle) + (dst_negative_scale_read_cellmiddle)))) + ((((dst_negative_code_read_cellmiddle) + (dst_negative_scale_read_cellmiddle)) * S ((dst_negative_code_read_cellmiddle) + (dst_negative_scale_read_cellmiddle)) + ((dst_negative_scale_read_cellmiddle) + (dst_negative_scale_read_cellmiddle))) + (((dst_negative_code_read_cellmiddle) + (dst_negative_scale_read_cellmiddle)) * S ((dst_negative_code_read_cellmiddle) + (dst_negative_scale_read_cellmiddle)) + ((dst_negative_scale_read_cellmiddle) + (dst_negative_scale_read_cellmiddle)))))) /\ (((((exists ff_h_pvs_read_cellmiddlepositive. ff_h_pvs_read_cellmiddlepositive + S (dst_positive_read_cellmiddle) = S ((S (dfg_middle_read_cell)) * dst_positive_scale_read_cellmiddle)) /\ exists ff_q_pvs_read_cellmiddlepositive. dst_positive_code_read_cellmiddle = ff_q_pvs_read_cellmiddlepositive * S ((S (dfg_middle_read_cell)) * dst_positive_scale_read_cellmiddle) + (dst_positive_read_cellmiddle))) /\ (((((exists ff_h_pvs_read_cellmiddlenegative. ff_h_pvs_read_cellmiddlenegative + S (dst_negative_read_cellmiddle) = S ((S (dfg_middle_read_cell)) * dst_negative_scale_read_cellmiddle)) /\ exists ff_q_pvs_read_cellmiddlenegative. dst_negative_code_read_cellmiddle = ff_q_pvs_read_cellmiddlenegative * S ((S (dfg_middle_read_cell)) * dst_negative_scale_read_cellmiddle) + (dst_negative_read_cellmiddle))) /\ (exists ge_balance_positive_read_cellmiddlevalue ge_balance_negative_read_cellmiddlevalue. (((((dfg_value_read_cell) = 2 * (ge_balance_positive_read_cellmiddlevalue) /\ (ge_balance_negative_read_cellmiddlevalue) = 0) \/ exists ge_signed_half_read_cellmiddlevaluedecode. (((dfg_value_read_cell) = 2 * ge_signed_half_read_cellmiddlevaluedecode + 1 /\ (ge_balance_positive_read_cellmiddlevalue) = 0) /\ (ge_balance_negative_read_cellmiddlevalue) = S ge_signed_half_read_cellmiddlevaluedecode))) /\ ((dst_positive_read_cellmiddle) + ge_balance_negative_read_cellmiddlevalue = (dst_negative_read_cellmiddle) + ge_balance_positive_read_cellmiddlevalue))))))))) /\ (exists dfg_inner_read_cellproduct. ((exists sto_ap_read_cellproductinner sto_an_read_cellproductinner sto_bp_read_cellproductinner sto_bn_read_cellproductinner sto_cp_read_cellproductinner sto_cn_read_cellproductinner. (((((dfg_last_read_cell) = 2 * (sto_ap_read_cellproductinner) /\ (sto_an_read_cellproductinner) = 0) \/ exists ge_signed_half_read_cellproductinnerleft. (((dfg_last_read_cell) = 2 * ge_signed_half_read_cellproductinnerleft + 1 /\ (sto_ap_read_cellproductinner) = 0) /\ (sto_an_read_cellproductinner) = S ge_signed_half_read_cellproductinnerleft))) /\ ((((((dfg_value_read_cell) = 2 * (sto_bp_read_cellproductinner) /\ (sto_bn_read_cellproductinner) = 0) \/ exists ge_signed_half_read_cellproductinnerright. (((dfg_value_read_cell) = 2 * ge_signed_half_read_cellproductinnerright + 1 /\ (sto_bp_read_cellproductinner) = 0) /\ (sto_bn_read_cellproductinner) = S ge_signed_half_read_cellproductinnerright))) /\ ((((((dfg_inner_read_cellproduct) = 2 * (sto_cp_read_cellproductinner) /\ (sto_cn_read_cellproductinner) = 0) \/ exists ge_signed_half_read_cellproductinneroutput. (((dfg_inner_read_cellproduct) = 2 * ge_signed_half_read_cellproductinneroutput + 1 /\ (sto_cp_read_cellproductinner) = 0) /\ (sto_cn_read_cellproductinner) = S ge_signed_half_read_cellproductinneroutput))) /\ ((sto_ap_read_cellproductinner * sto_bp_read_cellproductinner + sto_an_read_cellproductinner * sto_bn_read_cellproductinner) + sto_cn_read_cellproductinner = (sto_ap_read_cellproductinner * sto_bn_read_cellproductinner + sto_an_read_cellproductinner * sto_bp_read_cellproductinner) + sto_cp_read_cellproductinner))))))) /\ (exists sto_ap_read_cellproductouter sto_an_read_cellproductouter sto_bp_read_cellproductouter sto_bn_read_cellproductouter sto_cp_read_cellproductouter sto_cn_read_cellproductouter. (((((dfg_first_read_cell) = 2 * (sto_ap_read_cellproductouter) /\ (sto_an_read_cellproductouter) = 0) \/ exists ge_signed_half_read_cellproductouterleft. (((dfg_first_read_cell) = 2 * ge_signed_half_read_cellproductouterleft + 1 /\ (sto_ap_read_cellproductouter) = 0) /\ (sto_an_read_cellproductouter) = S ge_signed_half_read_cellproductouterleft))) /\ ((((((dfg_inner_read_cellproduct) = 2 * (sto_bp_read_cellproductouter) /\ (sto_bn_read_cellproductouter) = 0) \/ exists ge_signed_half_read_cellproductouterright. (((dfg_inner_read_cellproduct) = 2 * ge_signed_half_read_cellproductouterright + 1 /\ (sto_bp_read_cellproductouter) = 0) /\ (sto_bn_read_cellproductouter) = S ge_signed_half_read_cellproductouterright))) /\ ((((((z) = 2 * (sto_cp_read_cellproductouter) /\ (sto_cn_read_cellproductouter) = 0) \/ exists ge_signed_half_read_cellproductouteroutput. (((z) = 2 * ge_signed_half_read_cellproductouteroutput + 1 /\ (sto_cp_read_cellproductouter) = 0) /\ (sto_cn_read_cellproductouter) = S ge_signed_half_read_cellproductouteroutput))) /\ ((sto_ap_read_cellproductouter * sto_bp_read_cellproductouter + sto_an_read_cellproductouter * sto_bn_read_cellproductouter) + sto_cn_read_cellproductouter = (sto_ap_read_cellproductouter * sto_bn_read_cellproductouter + sto_an_read_cellproductouter * sto_bp_read_cellproductouter) + sto_cp_read_cellproductouter))))))))))))))))))))) \/ ((((a)=0 \/ ((e)=0 \/ ~(exists pvs_factor_read_cellomittednondivisor. (n) = ((a)*(e)) * pvs_factor_read_cellomittednondivisor))) /\ ((z)=0)))) -> (exists dfg_inner_read_product. ((exists sto_ap_read_productinner sto_an_read_productinner sto_bp_read_productinner sto_bn_read_productinner sto_cp_read_productinner sto_cn_read_productinner. (((((v) = 2 * (sto_ap_read_productinner) /\ (sto_an_read_productinner) = 0) \/ exists ge_signed_half_read_productinnerleft. (((v) = 2 * ge_signed_half_read_productinnerleft + 1 /\ (sto_ap_read_productinner) = 0) /\ (sto_an_read_productinner) = S ge_signed_half_read_productinnerleft))) /\ ((((((w) = 2 * (sto_bp_read_productinner) /\ (sto_bn_read_productinner) = 0) \/ exists ge_signed_half_read_productinnerright. (((w) = 2 * ge_signed_half_read_productinnerright + 1 /\ (sto_bp_read_productinner) = 0) /\ (sto_bn_read_productinner) = S ge_signed_half_read_productinnerright))) /\ ((((((dfg_inner_read_product) = 2 * (sto_cp_read_productinner) /\ (sto_cn_read_productinner) = 0) \/ exists ge_signed_half_read_productinneroutput. (((dfg_inner_read_product) = 2 * ge_signed_half_read_productinneroutput + 1 /\ (sto_cp_read_productinner) = 0) /\ (sto_cn_read_productinner) = S ge_signed_half_read_productinneroutput))) /\ ((sto_ap_read_productinner * sto_bp_read_productinner + sto_an_read_productinner * sto_bn_read_productinner) + sto_cn_read_productinner = (sto_ap_read_productinner * sto_bn_read_productinner + sto_an_read_productinner * sto_bp_read_productinner) + sto_cp_read_productinner))))))) /\ (exists sto_ap_read_productouter sto_an_read_productouter sto_bp_read_productouter sto_bn_read_productouter sto_cp_read_productouter sto_cn_read_productouter. (((((u) = 2 * (sto_ap_read_productouter) /\ (sto_an_read_productouter) = 0) \/ exists ge_signed_half_read_productouterleft. (((u) = 2 * ge_signed_half_read_productouterleft + 1 /\ (sto_ap_read_productouter) = 0) /\ (sto_an_read_productouter) = S ge_signed_half_read_productouterleft))) /\ ((((((dfg_inner_read_product) = 2 * (sto_bp_read_productouter) /\ (sto_bn_read_productouter) = 0) \/ exists ge_signed_half_read_productouterright. (((dfg_inner_read_product) = 2 * ge_signed_half_read_productouterright + 1 /\ (sto_bp_read_productouter) = 0) /\ (sto_bn_read_productouter) = S ge_signed_half_read_productouterright))) /\ ((((((z) = 2 * (sto_cp_read_productouter) /\ (sto_cn_read_productouter) = 0) \/ exists ge_signed_half_read_productouteroutput. (((z) = 2 * ge_signed_half_read_productouteroutput + 1 /\ (sto_cp_read_productouter) = 0) /\ (sto_cn_read_productouter) = S ge_signed_half_read_productouteroutput))) /\ ((sto_ap_read_productouter * sto_bp_read_productouter + sto_an_read_productouter * sto_bn_read_productouter) + sto_cn_read_productouter = (sto_ap_read_productouter * sto_bn_read_productouter + sto_an_read_productouter * sto_bp_read_productouter) + sto_cp_read_productouter)))))))))

Complete tactic proof in conservative notation

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

91 script commands · 20 reading checkpoints · 4 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–10

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 c
  8. L8
    intro u
  9. L9
    intro v
  10. L10
    intro w
02Fix variables and assumptionsL11–18

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

  1. L11
    intro z
  2. L12
    intro ha
  3. L13
    intro he
  4. L14
    intro hc
  5. L15
    intro hu
  6. L16
    intro hv
  7. L17
    intro hw
  8. L18
    intro hentry
03Separate the logical casesL19–28

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

  1. L19
    cases hentry
  2. L20
    cases hentry_left
  3. L21
    cases hentry_left_right
  4. L22
    cases hentry_left_right_right
  5. L23
    cases hentry_left_right_right_witness
  6. L24
    cases hentry_left_right_right_witness_witness
  7. L25
    cases hentry_left_right_right_witness_witness_witness
  8. L26
    cases hentry_left_right_right_witness_witness_witness_witness
  9. L27
    cases hentry_left_right_right_witness_witness_witness_witness_right
  10. L28
    cases hentry_left_right_right_witness_witness_witness_witness_right_right
04Separate the logical casesL29–29

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

  1. L29
    cases hentry_left_right_right_witness_witness_witness_witness_right_right_right
05Establish hfactorL30–39

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul left cancel nonzero.

  1. L30
    have hfactor : x=c
  2. L31
    specialize mul_left_cancel_nonzero (a*e)
  3. L32
    specialize mul_left_cancel_nonzero (x)
  4. L33
    specialize mul_left_cancel_nonzero (c)
  5. L34
    apply mul_left_cancel_nonzero
  6. L35
    intro hmulzero
  7. L36
    specialize mul_ne_zero (a)
  8. L37
    specialize mul_ne_zero (e)
  9. L38
    apply mul_ne_zero
  10. L39
    exact ha
06Use earlier factsL40–41

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

  1. L40
    exact he
  2. L41
    exact hmulzero
07Calculate and transport equalitiesL42–43

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

  1. L42
    trans n
  2. L43
    symm
08Use earlier factsL44–45

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

  1. L44
    exact hentry_left_right_right_witness_witness_witness_witness_left
  2. L45
    exact hc
09Calculate and transport equalitiesL46–49

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

  1. L46
    rewrite hfactor at hentry_left_right_right_witness_witness_witness_witness_right_right_right_left
  2. L47
    rewrite hfactor at hentry_left_right_right_witness_witness_witness_witness_right_right_right_left
  3. L48
    rewrite hfactor at hentry_left_right_right_witness_witness_witness_witness_right_right_right_left
  4. L49
    rewrite hfactor at hentry_left_right_right_witness_witness_witness_witness_right_right_right_left
10Establish hx1L50–57

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

  1. L50
    have hx1 : x1=u
  2. L51
    specialize divisor_signed_table_at_functional (F)
  3. L52
    specialize divisor_signed_table_at_functional (a)
  4. L53
    specialize divisor_signed_table_at_functional (x1)
  5. L54
    specialize divisor_signed_table_at_functional (u)
  6. L55
    apply divisor_signed_table_at_functional
  7. L56
    exact hentry_left_right_right_witness_witness_witness_witness_right_left
  8. L57
    exact hu
11Establish hx2L58–65

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

  1. L58
    have hx2 : x2=v
  2. L59
    specialize divisor_signed_table_at_functional (H)
  3. L60
    specialize divisor_signed_table_at_functional (e)
  4. L61
    specialize divisor_signed_table_at_functional (x2)
  5. L62
    specialize divisor_signed_table_at_functional (v)
  6. L63
    apply divisor_signed_table_at_functional
  7. L64
    exact hentry_left_right_right_witness_witness_witness_witness_right_right_left
  8. L65
    exact hv
12Establish hx3L66–75

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

  1. L66
    have hx3 : x3=w
  2. L67
    specialize divisor_signed_table_at_functional (G)
  3. L68
    specialize divisor_signed_table_at_functional (c)
  4. L69
    specialize divisor_signed_table_at_functional (x3)
  5. L70
    specialize divisor_signed_table_at_functional (w)
  6. L71
    apply divisor_signed_table_at_functional
  7. L72
    exact hentry_left_right_right_witness_witness_witness_witness_right_right_right_left
  8. L73
    exact hw
  9. L74
    rewrite hx1 at hentry_left_right_right_witness_witness_witness_witness_right_right_right_right
  10. L75
    rewrite hx1 at hentry_left_right_right_witness_witness_witness_witness_right_right_right_right
13Calculate and transport equalitiesL76–79

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

  1. L76
    rewrite hx2 at hentry_left_right_right_witness_witness_witness_witness_right_right_right_right
  2. L77
    rewrite hx2 at hentry_left_right_right_witness_witness_witness_witness_right_right_right_right
  3. L78
    rewrite hx3 at hentry_left_right_right_witness_witness_witness_witness_right_right_right_right
  4. L79
    rewrite hx3 at hentry_left_right_right_witness_witness_witness_witness_right_right_right_right
14Use earlier factsL80–80

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

  1. L80
    exact hentry_left_right_right_witness_witness_witness_witness_right_right_right_right
15Separate the logical casesL81–83

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

  1. L81
    cases hentry_right
  2. L82
    exfalso
  3. L83
    cases hentry_right_left
16Use earlier factsL84–85

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

  1. L84
    apply ha
  2. L85
    exact hentry_right_left_left
17Separate the logical casesL86–86

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

  1. L86
    cases hentry_right_left_right
18Use earlier factsL87–89

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

  1. L87
    apply he
  2. L88
    exact hentry_right_left_right_left
  3. L89
    apply hentry_right_left_right_right
19Construct an explicit witnessL90–90

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

  1. L90
    exists c
20Use earlier factsL91–91

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

  1. L91
    exact hc

Library-wide reading audit

Original defined command ledger · 91 lines
  1. 0001intro F
  2. 0002intro G
  3. 0003intro H
  4. 0004intro n
  5. 0005intro a
  6. 0006intro e
  7. 0007intro c
  8. 0008intro u
  9. 0009intro v
  10. 0010intro w
  11. 0011intro z
  12. 0012intro ha
  13. 0013intro he
  14. 0014intro hc
  15. 0015intro hu
  16. 0016intro hv
  17. 0017intro hw
  18. 0018intro hentry
  19. 0019cases hentry
  20. 0020cases hentry_left
  21. 0021cases hentry_left_right
  22. 0022cases hentry_left_right_right
  23. 0023cases hentry_left_right_right_witness
  24. 0024cases hentry_left_right_right_witness_witness
  25. 0025cases hentry_left_right_right_witness_witness_witness
  26. 0026cases hentry_left_right_right_witness_witness_witness_witness
  27. 0027cases hentry_left_right_right_witness_witness_witness_witness_right
  28. 0028cases hentry_left_right_right_witness_witness_witness_witness_right_right
  29. 0029cases hentry_left_right_right_witness_witness_witness_witness_right_right_right
  30. 0030have hfactor : x=c
  31. 0031specialize mul_left_cancel_nonzero (a*e)
  32. 0032specialize mul_left_cancel_nonzero (x)
  33. 0033specialize mul_left_cancel_nonzero (c)
  34. 0034apply mul_left_cancel_nonzero
  35. 0035intro hmulzero
  36. 0036specialize mul_ne_zero (a)
  37. 0037specialize mul_ne_zero (e)
  38. 0038apply mul_ne_zero
  39. 0039exact ha
  40. 0040exact he
  41. 0041exact hmulzero
  42. 0042trans n
  43. 0043symm
  44. 0044exact hentry_left_right_right_witness_witness_witness_witness_left
  45. 0045exact hc
  46. 0046rewrite hfactor at hentry_left_right_right_witness_witness_witness_witness_right_right_right_left
  47. 0047rewrite hfactor at hentry_left_right_right_witness_witness_witness_witness_right_right_right_left
  48. 0048rewrite hfactor at hentry_left_right_right_witness_witness_witness_witness_right_right_right_left
  49. 0049rewrite hfactor at hentry_left_right_right_witness_witness_witness_witness_right_right_right_left
  50. 0050have hx1 : x1=u
  51. 0051specialize divisor_signed_table_at_functional (F)
  52. 0052specialize divisor_signed_table_at_functional (a)
  53. 0053specialize divisor_signed_table_at_functional (x1)
  54. 0054specialize divisor_signed_table_at_functional (u)
  55. 0055apply divisor_signed_table_at_functional
  56. 0056exact hentry_left_right_right_witness_witness_witness_witness_right_left
  57. 0057exact hu
  58. 0058have hx2 : x2=v
  59. 0059specialize divisor_signed_table_at_functional (H)
  60. 0060specialize divisor_signed_table_at_functional (e)
  61. 0061specialize divisor_signed_table_at_functional (x2)
  62. 0062specialize divisor_signed_table_at_functional (v)
  63. 0063apply divisor_signed_table_at_functional
  64. 0064exact hentry_left_right_right_witness_witness_witness_witness_right_right_left
  65. 0065exact hv
  66. 0066have hx3 : x3=w
  67. 0067specialize divisor_signed_table_at_functional (G)
  68. 0068specialize divisor_signed_table_at_functional (c)
  69. 0069specialize divisor_signed_table_at_functional (x3)
  70. 0070specialize divisor_signed_table_at_functional (w)
  71. 0071apply divisor_signed_table_at_functional
  72. 0072exact hentry_left_right_right_witness_witness_witness_witness_right_right_right_left
  73. 0073exact hw
  74. 0074rewrite hx1 at hentry_left_right_right_witness_witness_witness_witness_right_right_right_right
  75. 0075rewrite hx1 at hentry_left_right_right_witness_witness_witness_witness_right_right_right_right
  76. 0076rewrite hx2 at hentry_left_right_right_witness_witness_witness_witness_right_right_right_right
  77. 0077rewrite hx2 at hentry_left_right_right_witness_witness_witness_witness_right_right_right_right
  78. 0078rewrite hx3 at hentry_left_right_right_witness_witness_witness_witness_right_right_right_right
  79. 0079rewrite hx3 at hentry_left_right_right_witness_witness_witness_witness_right_right_right_right
  80. 0080exact hentry_left_right_right_witness_witness_witness_witness_right_right_right_right
  81. 0081cases hentry_right
  82. 0082exfalso
  83. 0083cases hentry_right_left
  84. 0084apply ha
  85. 0085exact hentry_right_left_left
  86. 0086cases hentry_right_left_right
  87. 0087apply he
  88. 0088exact hentry_right_left_right_left
  89. 0089apply hentry_right_left_right_right
  90. 0090exists c
  91. 0091exact hc