DF0002

dirichlet_grid_entry_from_factorization

A real three-factor equation, three actual signed lookups and two actual products construct a retained grid cell.

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

none
Original expanded first-order statement 
forall F G H n a e c u v w r z. ~(a=0) -> ~(e=0) -> n=(a*e)*c -> (exists dst_positive_code_factor_first dst_positive_scale_factor_first dst_negative_code_factor_first dst_negative_scale_factor_first dst_positive_factor_first dst_negative_factor_first. (((F) = (((((dst_positive_code_factor_first) + (dst_positive_scale_factor_first)) * S ((dst_positive_code_factor_first) + (dst_positive_scale_factor_first)) + ((dst_positive_scale_factor_first) + (dst_positive_scale_factor_first))) + (((dst_negative_code_factor_first) + (dst_negative_scale_factor_first)) * S ((dst_negative_code_factor_first) + (dst_negative_scale_factor_first)) + ((dst_negative_scale_factor_first) + (dst_negative_scale_factor_first)))) * S ((((dst_positive_code_factor_first) + (dst_positive_scale_factor_first)) * S ((dst_positive_code_factor_first) + (dst_positive_scale_factor_first)) + ((dst_positive_scale_factor_first) + (dst_positive_scale_factor_first))) + (((dst_negative_code_factor_first) + (dst_negative_scale_factor_first)) * S ((dst_negative_code_factor_first) + (dst_negative_scale_factor_first)) + ((dst_negative_scale_factor_first) + (dst_negative_scale_factor_first)))) + ((((dst_negative_code_factor_first) + (dst_negative_scale_factor_first)) * S ((dst_negative_code_factor_first) + (dst_negative_scale_factor_first)) + ((dst_negative_scale_factor_first) + (dst_negative_scale_factor_first))) + (((dst_negative_code_factor_first) + (dst_negative_scale_factor_first)) * S ((dst_negative_code_factor_first) + (dst_negative_scale_factor_first)) + ((dst_negative_scale_factor_first) + (dst_negative_scale_factor_first)))))) /\ (((((exists ff_h_pvs_factor_firstpositive. ff_h_pvs_factor_firstpositive + S (dst_positive_factor_first) = S ((S (a)) * dst_positive_scale_factor_first)) /\ exists ff_q_pvs_factor_firstpositive. dst_positive_code_factor_first = ff_q_pvs_factor_firstpositive * S ((S (a)) * dst_positive_scale_factor_first) + (dst_positive_factor_first))) /\ (((((exists ff_h_pvs_factor_firstnegative. ff_h_pvs_factor_firstnegative + S (dst_negative_factor_first) = S ((S (a)) * dst_negative_scale_factor_first)) /\ exists ff_q_pvs_factor_firstnegative. dst_negative_code_factor_first = ff_q_pvs_factor_firstnegative * S ((S (a)) * dst_negative_scale_factor_first) + (dst_negative_factor_first))) /\ (exists ge_balance_positive_factor_firstvalue ge_balance_negative_factor_firstvalue. (((((u) = 2 * (ge_balance_positive_factor_firstvalue) /\ (ge_balance_negative_factor_firstvalue) = 0) \/ exists ge_signed_half_factor_firstvaluedecode. (((u) = 2 * ge_signed_half_factor_firstvaluedecode + 1 /\ (ge_balance_positive_factor_firstvalue) = 0) /\ (ge_balance_negative_factor_firstvalue) = S ge_signed_half_factor_firstvaluedecode))) /\ ((dst_positive_factor_first) + ge_balance_negative_factor_firstvalue = (dst_negative_factor_first) + ge_balance_positive_factor_firstvalue))))))))) -> (exists dst_positive_code_factor_last dst_positive_scale_factor_last dst_negative_code_factor_last dst_negative_scale_factor_last dst_positive_factor_last dst_negative_factor_last. (((H) = (((((dst_positive_code_factor_last) + (dst_positive_scale_factor_last)) * S ((dst_positive_code_factor_last) + (dst_positive_scale_factor_last)) + ((dst_positive_scale_factor_last) + (dst_positive_scale_factor_last))) + (((dst_negative_code_factor_last) + (dst_negative_scale_factor_last)) * S ((dst_negative_code_factor_last) + (dst_negative_scale_factor_last)) + ((dst_negative_scale_factor_last) + (dst_negative_scale_factor_last)))) * S ((((dst_positive_code_factor_last) + (dst_positive_scale_factor_last)) * S ((dst_positive_code_factor_last) + (dst_positive_scale_factor_last)) + ((dst_positive_scale_factor_last) + (dst_positive_scale_factor_last))) + (((dst_negative_code_factor_last) + (dst_negative_scale_factor_last)) * S ((dst_negative_code_factor_last) + (dst_negative_scale_factor_last)) + ((dst_negative_scale_factor_last) + (dst_negative_scale_factor_last)))) + ((((dst_negative_code_factor_last) + (dst_negative_scale_factor_last)) * S ((dst_negative_code_factor_last) + (dst_negative_scale_factor_last)) + ((dst_negative_scale_factor_last) + (dst_negative_scale_factor_last))) + (((dst_negative_code_factor_last) + (dst_negative_scale_factor_last)) * S ((dst_negative_code_factor_last) + (dst_negative_scale_factor_last)) + ((dst_negative_scale_factor_last) + (dst_negative_scale_factor_last)))))) /\ (((((exists ff_h_pvs_factor_lastpositive. ff_h_pvs_factor_lastpositive + S (dst_positive_factor_last) = S ((S (e)) * dst_positive_scale_factor_last)) /\ exists ff_q_pvs_factor_lastpositive. dst_positive_code_factor_last = ff_q_pvs_factor_lastpositive * S ((S (e)) * dst_positive_scale_factor_last) + (dst_positive_factor_last))) /\ (((((exists ff_h_pvs_factor_lastnegative. ff_h_pvs_factor_lastnegative + S (dst_negative_factor_last) = S ((S (e)) * dst_negative_scale_factor_last)) /\ exists ff_q_pvs_factor_lastnegative. dst_negative_code_factor_last = ff_q_pvs_factor_lastnegative * S ((S (e)) * dst_negative_scale_factor_last) + (dst_negative_factor_last))) /\ (exists ge_balance_positive_factor_lastvalue ge_balance_negative_factor_lastvalue. (((((v) = 2 * (ge_balance_positive_factor_lastvalue) /\ (ge_balance_negative_factor_lastvalue) = 0) \/ exists ge_signed_half_factor_lastvaluedecode. (((v) = 2 * ge_signed_half_factor_lastvaluedecode + 1 /\ (ge_balance_positive_factor_lastvalue) = 0) /\ (ge_balance_negative_factor_lastvalue) = S ge_signed_half_factor_lastvaluedecode))) /\ ((dst_positive_factor_last) + ge_balance_negative_factor_lastvalue = (dst_negative_factor_last) + ge_balance_positive_factor_lastvalue))))))))) -> (exists dst_positive_code_factor_middle dst_positive_scale_factor_middle dst_negative_code_factor_middle dst_negative_scale_factor_middle dst_positive_factor_middle dst_negative_factor_middle. (((G) = (((((dst_positive_code_factor_middle) + (dst_positive_scale_factor_middle)) * S ((dst_positive_code_factor_middle) + (dst_positive_scale_factor_middle)) + ((dst_positive_scale_factor_middle) + (dst_positive_scale_factor_middle))) + (((dst_negative_code_factor_middle) + (dst_negative_scale_factor_middle)) * S ((dst_negative_code_factor_middle) + (dst_negative_scale_factor_middle)) + ((dst_negative_scale_factor_middle) + (dst_negative_scale_factor_middle)))) * S ((((dst_positive_code_factor_middle) + (dst_positive_scale_factor_middle)) * S ((dst_positive_code_factor_middle) + (dst_positive_scale_factor_middle)) + ((dst_positive_scale_factor_middle) + (dst_positive_scale_factor_middle))) + (((dst_negative_code_factor_middle) + (dst_negative_scale_factor_middle)) * S ((dst_negative_code_factor_middle) + (dst_negative_scale_factor_middle)) + ((dst_negative_scale_factor_middle) + (dst_negative_scale_factor_middle)))) + ((((dst_negative_code_factor_middle) + (dst_negative_scale_factor_middle)) * S ((dst_negative_code_factor_middle) + (dst_negative_scale_factor_middle)) + ((dst_negative_scale_factor_middle) + (dst_negative_scale_factor_middle))) + (((dst_negative_code_factor_middle) + (dst_negative_scale_factor_middle)) * S ((dst_negative_code_factor_middle) + (dst_negative_scale_factor_middle)) + ((dst_negative_scale_factor_middle) + (dst_negative_scale_factor_middle)))))) /\ (((((exists ff_h_pvs_factor_middlepositive. ff_h_pvs_factor_middlepositive + S (dst_positive_factor_middle) = S ((S (c)) * dst_positive_scale_factor_middle)) /\ exists ff_q_pvs_factor_middlepositive. dst_positive_code_factor_middle = ff_q_pvs_factor_middlepositive * S ((S (c)) * dst_positive_scale_factor_middle) + (dst_positive_factor_middle))) /\ (((((exists ff_h_pvs_factor_middlenegative. ff_h_pvs_factor_middlenegative + S (dst_negative_factor_middle) = S ((S (c)) * dst_negative_scale_factor_middle)) /\ exists ff_q_pvs_factor_middlenegative. dst_negative_code_factor_middle = ff_q_pvs_factor_middlenegative * S ((S (c)) * dst_negative_scale_factor_middle) + (dst_negative_factor_middle))) /\ (exists ge_balance_positive_factor_middlevalue ge_balance_negative_factor_middlevalue. (((((w) = 2 * (ge_balance_positive_factor_middlevalue) /\ (ge_balance_negative_factor_middlevalue) = 0) \/ exists ge_signed_half_factor_middlevaluedecode. (((w) = 2 * ge_signed_half_factor_middlevaluedecode + 1 /\ (ge_balance_positive_factor_middlevalue) = 0) /\ (ge_balance_negative_factor_middlevalue) = S ge_signed_half_factor_middlevaluedecode))) /\ ((dst_positive_factor_middle) + ge_balance_negative_factor_middlevalue = (dst_negative_factor_middle) + ge_balance_positive_factor_middlevalue))))))))) -> (exists sto_ap_factor_inner sto_an_factor_inner sto_bp_factor_inner sto_bn_factor_inner sto_cp_factor_inner sto_cn_factor_inner. (((((v) = 2 * (sto_ap_factor_inner) /\ (sto_an_factor_inner) = 0) \/ exists ge_signed_half_factor_innerleft. (((v) = 2 * ge_signed_half_factor_innerleft + 1 /\ (sto_ap_factor_inner) = 0) /\ (sto_an_factor_inner) = S ge_signed_half_factor_innerleft))) /\ ((((((w) = 2 * (sto_bp_factor_inner) /\ (sto_bn_factor_inner) = 0) \/ exists ge_signed_half_factor_innerright. (((w) = 2 * ge_signed_half_factor_innerright + 1 /\ (sto_bp_factor_inner) = 0) /\ (sto_bn_factor_inner) = S ge_signed_half_factor_innerright))) /\ ((((((r) = 2 * (sto_cp_factor_inner) /\ (sto_cn_factor_inner) = 0) \/ exists ge_signed_half_factor_inneroutput. (((r) = 2 * ge_signed_half_factor_inneroutput + 1 /\ (sto_cp_factor_inner) = 0) /\ (sto_cn_factor_inner) = S ge_signed_half_factor_inneroutput))) /\ ((sto_ap_factor_inner * sto_bp_factor_inner + sto_an_factor_inner * sto_bn_factor_inner) + sto_cn_factor_inner = (sto_ap_factor_inner * sto_bn_factor_inner + sto_an_factor_inner * sto_bp_factor_inner) + sto_cp_factor_inner))))))) -> (exists sto_ap_factor_outer sto_an_factor_outer sto_bp_factor_outer sto_bn_factor_outer sto_cp_factor_outer sto_cn_factor_outer. (((((u) = 2 * (sto_ap_factor_outer) /\ (sto_an_factor_outer) = 0) \/ exists ge_signed_half_factor_outerleft. (((u) = 2 * ge_signed_half_factor_outerleft + 1 /\ (sto_ap_factor_outer) = 0) /\ (sto_an_factor_outer) = S ge_signed_half_factor_outerleft))) /\ ((((((r) = 2 * (sto_bp_factor_outer) /\ (sto_bn_factor_outer) = 0) \/ exists ge_signed_half_factor_outerright. (((r) = 2 * ge_signed_half_factor_outerright + 1 /\ (sto_bp_factor_outer) = 0) /\ (sto_bn_factor_outer) = S ge_signed_half_factor_outerright))) /\ ((((((z) = 2 * (sto_cp_factor_outer) /\ (sto_cn_factor_outer) = 0) \/ exists ge_signed_half_factor_outeroutput. (((z) = 2 * ge_signed_half_factor_outeroutput + 1 /\ (sto_cp_factor_outer) = 0) /\ (sto_cn_factor_outer) = S ge_signed_half_factor_outeroutput))) /\ ((sto_ap_factor_outer * sto_bp_factor_outer + sto_an_factor_outer * sto_bn_factor_outer) + sto_cn_factor_outer = (sto_ap_factor_outer * sto_bn_factor_outer + sto_an_factor_outer * sto_bp_factor_outer) + sto_cp_factor_outer))))))) -> ((((~((a)=0)) /\ (((~((e)=0)) /\ (exists dfg_middle_factor_result dfg_first_factor_result dfg_last_factor_result dfg_value_factor_result. (((n)=((a)*(e))*dfg_middle_factor_result) /\ (((exists dst_positive_code_factor_resultfirst dst_positive_scale_factor_resultfirst dst_negative_code_factor_resultfirst dst_negative_scale_factor_resultfirst dst_positive_factor_resultfirst dst_negative_factor_resultfirst. (((F) = (((((dst_positive_code_factor_resultfirst) + (dst_positive_scale_factor_resultfirst)) * S ((dst_positive_code_factor_resultfirst) + (dst_positive_scale_factor_resultfirst)) + ((dst_positive_scale_factor_resultfirst) + (dst_positive_scale_factor_resultfirst))) + (((dst_negative_code_factor_resultfirst) + (dst_negative_scale_factor_resultfirst)) * S ((dst_negative_code_factor_resultfirst) + (dst_negative_scale_factor_resultfirst)) + ((dst_negative_scale_factor_resultfirst) + (dst_negative_scale_factor_resultfirst)))) * S ((((dst_positive_code_factor_resultfirst) + (dst_positive_scale_factor_resultfirst)) * S ((dst_positive_code_factor_resultfirst) + (dst_positive_scale_factor_resultfirst)) + ((dst_positive_scale_factor_resultfirst) + (dst_positive_scale_factor_resultfirst))) + (((dst_negative_code_factor_resultfirst) + (dst_negative_scale_factor_resultfirst)) * S ((dst_negative_code_factor_resultfirst) + (dst_negative_scale_factor_resultfirst)) + ((dst_negative_scale_factor_resultfirst) + (dst_negative_scale_factor_resultfirst)))) + ((((dst_negative_code_factor_resultfirst) + (dst_negative_scale_factor_resultfirst)) * S ((dst_negative_code_factor_resultfirst) + (dst_negative_scale_factor_resultfirst)) + ((dst_negative_scale_factor_resultfirst) + (dst_negative_scale_factor_resultfirst))) + (((dst_negative_code_factor_resultfirst) + (dst_negative_scale_factor_resultfirst)) * S ((dst_negative_code_factor_resultfirst) + (dst_negative_scale_factor_resultfirst)) + ((dst_negative_scale_factor_resultfirst) + (dst_negative_scale_factor_resultfirst)))))) /\ (((((exists ff_h_pvs_factor_resultfirstpositive. ff_h_pvs_factor_resultfirstpositive + S (dst_positive_factor_resultfirst) = S ((S (a)) * dst_positive_scale_factor_resultfirst)) /\ exists ff_q_pvs_factor_resultfirstpositive. dst_positive_code_factor_resultfirst = ff_q_pvs_factor_resultfirstpositive * S ((S (a)) * dst_positive_scale_factor_resultfirst) + (dst_positive_factor_resultfirst))) /\ (((((exists ff_h_pvs_factor_resultfirstnegative. ff_h_pvs_factor_resultfirstnegative + S (dst_negative_factor_resultfirst) = S ((S (a)) * dst_negative_scale_factor_resultfirst)) /\ exists ff_q_pvs_factor_resultfirstnegative. dst_negative_code_factor_resultfirst = ff_q_pvs_factor_resultfirstnegative * S ((S (a)) * dst_negative_scale_factor_resultfirst) + (dst_negative_factor_resultfirst))) /\ (exists ge_balance_positive_factor_resultfirstvalue ge_balance_negative_factor_resultfirstvalue. (((((dfg_first_factor_result) = 2 * (ge_balance_positive_factor_resultfirstvalue) /\ (ge_balance_negative_factor_resultfirstvalue) = 0) \/ exists ge_signed_half_factor_resultfirstvaluedecode. (((dfg_first_factor_result) = 2 * ge_signed_half_factor_resultfirstvaluedecode + 1 /\ (ge_balance_positive_factor_resultfirstvalue) = 0) /\ (ge_balance_negative_factor_resultfirstvalue) = S ge_signed_half_factor_resultfirstvaluedecode))) /\ ((dst_positive_factor_resultfirst) + ge_balance_negative_factor_resultfirstvalue = (dst_negative_factor_resultfirst) + ge_balance_positive_factor_resultfirstvalue))))))))) /\ (((exists dst_positive_code_factor_resultlast dst_positive_scale_factor_resultlast dst_negative_code_factor_resultlast dst_negative_scale_factor_resultlast dst_positive_factor_resultlast dst_negative_factor_resultlast. (((H) = (((((dst_positive_code_factor_resultlast) + (dst_positive_scale_factor_resultlast)) * S ((dst_positive_code_factor_resultlast) + (dst_positive_scale_factor_resultlast)) + ((dst_positive_scale_factor_resultlast) + (dst_positive_scale_factor_resultlast))) + (((dst_negative_code_factor_resultlast) + (dst_negative_scale_factor_resultlast)) * S ((dst_negative_code_factor_resultlast) + (dst_negative_scale_factor_resultlast)) + ((dst_negative_scale_factor_resultlast) + (dst_negative_scale_factor_resultlast)))) * S ((((dst_positive_code_factor_resultlast) + (dst_positive_scale_factor_resultlast)) * S ((dst_positive_code_factor_resultlast) + (dst_positive_scale_factor_resultlast)) + ((dst_positive_scale_factor_resultlast) + (dst_positive_scale_factor_resultlast))) + (((dst_negative_code_factor_resultlast) + (dst_negative_scale_factor_resultlast)) * S ((dst_negative_code_factor_resultlast) + (dst_negative_scale_factor_resultlast)) + ((dst_negative_scale_factor_resultlast) + (dst_negative_scale_factor_resultlast)))) + ((((dst_negative_code_factor_resultlast) + (dst_negative_scale_factor_resultlast)) * S ((dst_negative_code_factor_resultlast) + (dst_negative_scale_factor_resultlast)) + ((dst_negative_scale_factor_resultlast) + (dst_negative_scale_factor_resultlast))) + (((dst_negative_code_factor_resultlast) + (dst_negative_scale_factor_resultlast)) * S ((dst_negative_code_factor_resultlast) + (dst_negative_scale_factor_resultlast)) + ((dst_negative_scale_factor_resultlast) + (dst_negative_scale_factor_resultlast)))))) /\ (((((exists ff_h_pvs_factor_resultlastpositive. ff_h_pvs_factor_resultlastpositive + S (dst_positive_factor_resultlast) = S ((S (e)) * dst_positive_scale_factor_resultlast)) /\ exists ff_q_pvs_factor_resultlastpositive. dst_positive_code_factor_resultlast = ff_q_pvs_factor_resultlastpositive * S ((S (e)) * dst_positive_scale_factor_resultlast) + (dst_positive_factor_resultlast))) /\ (((((exists ff_h_pvs_factor_resultlastnegative. ff_h_pvs_factor_resultlastnegative + S (dst_negative_factor_resultlast) = S ((S (e)) * dst_negative_scale_factor_resultlast)) /\ exists ff_q_pvs_factor_resultlastnegative. dst_negative_code_factor_resultlast = ff_q_pvs_factor_resultlastnegative * S ((S (e)) * dst_negative_scale_factor_resultlast) + (dst_negative_factor_resultlast))) /\ (exists ge_balance_positive_factor_resultlastvalue ge_balance_negative_factor_resultlastvalue. (((((dfg_last_factor_result) = 2 * (ge_balance_positive_factor_resultlastvalue) /\ (ge_balance_negative_factor_resultlastvalue) = 0) \/ exists ge_signed_half_factor_resultlastvaluedecode. (((dfg_last_factor_result) = 2 * ge_signed_half_factor_resultlastvaluedecode + 1 /\ (ge_balance_positive_factor_resultlastvalue) = 0) /\ (ge_balance_negative_factor_resultlastvalue) = S ge_signed_half_factor_resultlastvaluedecode))) /\ ((dst_positive_factor_resultlast) + ge_balance_negative_factor_resultlastvalue = (dst_negative_factor_resultlast) + ge_balance_positive_factor_resultlastvalue))))))))) /\ (((exists dst_positive_code_factor_resultmiddle dst_positive_scale_factor_resultmiddle dst_negative_code_factor_resultmiddle dst_negative_scale_factor_resultmiddle dst_positive_factor_resultmiddle dst_negative_factor_resultmiddle. (((G) = (((((dst_positive_code_factor_resultmiddle) + (dst_positive_scale_factor_resultmiddle)) * S ((dst_positive_code_factor_resultmiddle) + (dst_positive_scale_factor_resultmiddle)) + ((dst_positive_scale_factor_resultmiddle) + (dst_positive_scale_factor_resultmiddle))) + (((dst_negative_code_factor_resultmiddle) + (dst_negative_scale_factor_resultmiddle)) * S ((dst_negative_code_factor_resultmiddle) + (dst_negative_scale_factor_resultmiddle)) + ((dst_negative_scale_factor_resultmiddle) + (dst_negative_scale_factor_resultmiddle)))) * S ((((dst_positive_code_factor_resultmiddle) + (dst_positive_scale_factor_resultmiddle)) * S ((dst_positive_code_factor_resultmiddle) + (dst_positive_scale_factor_resultmiddle)) + ((dst_positive_scale_factor_resultmiddle) + (dst_positive_scale_factor_resultmiddle))) + (((dst_negative_code_factor_resultmiddle) + (dst_negative_scale_factor_resultmiddle)) * S ((dst_negative_code_factor_resultmiddle) + (dst_negative_scale_factor_resultmiddle)) + ((dst_negative_scale_factor_resultmiddle) + (dst_negative_scale_factor_resultmiddle)))) + ((((dst_negative_code_factor_resultmiddle) + (dst_negative_scale_factor_resultmiddle)) * S ((dst_negative_code_factor_resultmiddle) + (dst_negative_scale_factor_resultmiddle)) + ((dst_negative_scale_factor_resultmiddle) + (dst_negative_scale_factor_resultmiddle))) + (((dst_negative_code_factor_resultmiddle) + (dst_negative_scale_factor_resultmiddle)) * S ((dst_negative_code_factor_resultmiddle) + (dst_negative_scale_factor_resultmiddle)) + ((dst_negative_scale_factor_resultmiddle) + (dst_negative_scale_factor_resultmiddle)))))) /\ (((((exists ff_h_pvs_factor_resultmiddlepositive. ff_h_pvs_factor_resultmiddlepositive + S (dst_positive_factor_resultmiddle) = S ((S (dfg_middle_factor_result)) * dst_positive_scale_factor_resultmiddle)) /\ exists ff_q_pvs_factor_resultmiddlepositive. dst_positive_code_factor_resultmiddle = ff_q_pvs_factor_resultmiddlepositive * S ((S (dfg_middle_factor_result)) * dst_positive_scale_factor_resultmiddle) + (dst_positive_factor_resultmiddle))) /\ (((((exists ff_h_pvs_factor_resultmiddlenegative. ff_h_pvs_factor_resultmiddlenegative + S (dst_negative_factor_resultmiddle) = S ((S (dfg_middle_factor_result)) * dst_negative_scale_factor_resultmiddle)) /\ exists ff_q_pvs_factor_resultmiddlenegative. dst_negative_code_factor_resultmiddle = ff_q_pvs_factor_resultmiddlenegative * S ((S (dfg_middle_factor_result)) * dst_negative_scale_factor_resultmiddle) + (dst_negative_factor_resultmiddle))) /\ (exists ge_balance_positive_factor_resultmiddlevalue ge_balance_negative_factor_resultmiddlevalue. (((((dfg_value_factor_result) = 2 * (ge_balance_positive_factor_resultmiddlevalue) /\ (ge_balance_negative_factor_resultmiddlevalue) = 0) \/ exists ge_signed_half_factor_resultmiddlevaluedecode. (((dfg_value_factor_result) = 2 * ge_signed_half_factor_resultmiddlevaluedecode + 1 /\ (ge_balance_positive_factor_resultmiddlevalue) = 0) /\ (ge_balance_negative_factor_resultmiddlevalue) = S ge_signed_half_factor_resultmiddlevaluedecode))) /\ ((dst_positive_factor_resultmiddle) + ge_balance_negative_factor_resultmiddlevalue = (dst_negative_factor_resultmiddle) + ge_balance_positive_factor_resultmiddlevalue))))))))) /\ (exists dfg_inner_factor_resultproduct. ((exists sto_ap_factor_resultproductinner sto_an_factor_resultproductinner sto_bp_factor_resultproductinner sto_bn_factor_resultproductinner sto_cp_factor_resultproductinner sto_cn_factor_resultproductinner. (((((dfg_last_factor_result) = 2 * (sto_ap_factor_resultproductinner) /\ (sto_an_factor_resultproductinner) = 0) \/ exists ge_signed_half_factor_resultproductinnerleft. (((dfg_last_factor_result) = 2 * ge_signed_half_factor_resultproductinnerleft + 1 /\ (sto_ap_factor_resultproductinner) = 0) /\ (sto_an_factor_resultproductinner) = S ge_signed_half_factor_resultproductinnerleft))) /\ ((((((dfg_value_factor_result) = 2 * (sto_bp_factor_resultproductinner) /\ (sto_bn_factor_resultproductinner) = 0) \/ exists ge_signed_half_factor_resultproductinnerright. (((dfg_value_factor_result) = 2 * ge_signed_half_factor_resultproductinnerright + 1 /\ (sto_bp_factor_resultproductinner) = 0) /\ (sto_bn_factor_resultproductinner) = S ge_signed_half_factor_resultproductinnerright))) /\ ((((((dfg_inner_factor_resultproduct) = 2 * (sto_cp_factor_resultproductinner) /\ (sto_cn_factor_resultproductinner) = 0) \/ exists ge_signed_half_factor_resultproductinneroutput. (((dfg_inner_factor_resultproduct) = 2 * ge_signed_half_factor_resultproductinneroutput + 1 /\ (sto_cp_factor_resultproductinner) = 0) /\ (sto_cn_factor_resultproductinner) = S ge_signed_half_factor_resultproductinneroutput))) /\ ((sto_ap_factor_resultproductinner * sto_bp_factor_resultproductinner + sto_an_factor_resultproductinner * sto_bn_factor_resultproductinner) + sto_cn_factor_resultproductinner = (sto_ap_factor_resultproductinner * sto_bn_factor_resultproductinner + sto_an_factor_resultproductinner * sto_bp_factor_resultproductinner) + sto_cp_factor_resultproductinner))))))) /\ (exists sto_ap_factor_resultproductouter sto_an_factor_resultproductouter sto_bp_factor_resultproductouter sto_bn_factor_resultproductouter sto_cp_factor_resultproductouter sto_cn_factor_resultproductouter. (((((dfg_first_factor_result) = 2 * (sto_ap_factor_resultproductouter) /\ (sto_an_factor_resultproductouter) = 0) \/ exists ge_signed_half_factor_resultproductouterleft. (((dfg_first_factor_result) = 2 * ge_signed_half_factor_resultproductouterleft + 1 /\ (sto_ap_factor_resultproductouter) = 0) /\ (sto_an_factor_resultproductouter) = S ge_signed_half_factor_resultproductouterleft))) /\ ((((((dfg_inner_factor_resultproduct) = 2 * (sto_bp_factor_resultproductouter) /\ (sto_bn_factor_resultproductouter) = 0) \/ exists ge_signed_half_factor_resultproductouterright. (((dfg_inner_factor_resultproduct) = 2 * ge_signed_half_factor_resultproductouterright + 1 /\ (sto_bp_factor_resultproductouter) = 0) /\ (sto_bn_factor_resultproductouter) = S ge_signed_half_factor_resultproductouterright))) /\ ((((((z) = 2 * (sto_cp_factor_resultproductouter) /\ (sto_cn_factor_resultproductouter) = 0) \/ exists ge_signed_half_factor_resultproductouteroutput. (((z) = 2 * ge_signed_half_factor_resultproductouteroutput + 1 /\ (sto_cp_factor_resultproductouter) = 0) /\ (sto_cn_factor_resultproductouter) = S ge_signed_half_factor_resultproductouteroutput))) /\ ((sto_ap_factor_resultproductouter * sto_bp_factor_resultproductouter + sto_an_factor_resultproductouter * sto_bn_factor_resultproductouter) + sto_cn_factor_resultproductouter = (sto_ap_factor_resultproductouter * sto_bn_factor_resultproductouter + sto_an_factor_resultproductouter * sto_bp_factor_resultproductouter) + sto_cp_factor_resultproductouter))))))))))))))))))))) \/ ((((a)=0 \/ ((e)=0 \/ ~(exists pvs_factor_factor_resultomittednondivisor. (n) = ((a)*(e)) * pvs_factor_factor_resultomittednondivisor))) /\ ((z)=0))))

Complete tactic proof in conservative notation

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

41 script commands · 18 reading checkpoints · 0 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–20

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

  1. L11
    intro r
  2. L12
    intro z
  3. L13
    intro ha
  4. L14
    intro he
  5. L15
    intro hc
  6. L16
    intro hu
  7. L17
    intro hv
  8. L18
    intro hw
  9. L19
    intro hr
  10. L20
    intro hz
03Separate the logical casesL21–22

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

  1. L21
    left
  2. L22
    split
04Use earlier factsL23–23

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

  1. L23
    exact ha
05Separate the logical casesL24–24

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

  1. L24
    split
06Use earlier factsL25–25

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

  1. L25
    exact he
07Construct an explicit witnessL26–29

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

  1. L26
    exists c
  2. L27
    exists u
  3. L28
    exists v
  4. L29
    exists w
08Separate the logical casesL30–30

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

  1. L30
    split
09Use earlier factsL31–31

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

  1. L31
    exact hc
10Separate the logical casesL32–32

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

  1. L32
    split
11Use earlier factsL33–33

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

  1. L33
    exact hu
12Separate the logical casesL34–34

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

  1. L34
    split
13Use earlier factsL35–35

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

  1. L35
    exact hv
14Separate the logical casesL36–36

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

  1. L36
    split
15Use earlier factsL37–37

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

  1. L37
    exact hw
16Construct an explicit witnessL38–38

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

  1. L38
    exists r
17Separate the logical casesL39–39

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

  1. L39
    split
18Use earlier factsL40–41

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

  1. L40
    exact hr
  2. L41
    exact hz

Library-wide reading audit

Original defined command ledger · 41 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 r
  12. 0012intro z
  13. 0013intro ha
  14. 0014intro he
  15. 0015intro hc
  16. 0016intro hu
  17. 0017intro hv
  18. 0018intro hw
  19. 0019intro hr
  20. 0020intro hz
  21. 0021left
  22. 0022split
  23. 0023exact ha
  24. 0024split
  25. 0025exact he
  26. 0026exists c
  27. 0027exists u
  28. 0028exists v
  29. 0029exists w
  30. 0030split
  31. 0031exact hc
  32. 0032split
  33. 0033exact hu
  34. 0034split
  35. 0035exact hv
  36. 0036split
  37. 0037exact hw
  38. 0038exists r
  39. 0039split
  40. 0040exact hr
  41. 0041exact hz