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. a = 0 ∨ (e = 0 ∨ ¬Dvd(a · e,n)) → DirichletGridEntry(F,G,H,n,a,e,0)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
none
Original expanded first-order statement
forall F G H n a e. ((a)=0 \/ ((e)=0 \/ ~(exists pvs_factor_omit_guardnondivisor. (n) = ((a)*(e)) * pvs_factor_omit_guardnondivisor))) -> ((((~((a)=0)) /\ (((~((e)=0)) /\ (exists dfg_middle_omit_result dfg_first_omit_result dfg_last_omit_result dfg_value_omit_result. (((n)=((a)*(e))*dfg_middle_omit_result) /\ (((exists dst_positive_code_omit_resultfirst dst_positive_scale_omit_resultfirst dst_negative_code_omit_resultfirst dst_negative_scale_omit_resultfirst dst_positive_omit_resultfirst dst_negative_omit_resultfirst. (((F) = (((((dst_positive_code_omit_resultfirst) + (dst_positive_scale_omit_resultfirst)) * S ((dst_positive_code_omit_resultfirst) + (dst_positive_scale_omit_resultfirst)) + ((dst_positive_scale_omit_resultfirst) + (dst_positive_scale_omit_resultfirst))) + (((dst_negative_code_omit_resultfirst) + (dst_negative_scale_omit_resultfirst)) * S ((dst_negative_code_omit_resultfirst) + (dst_negative_scale_omit_resultfirst)) + ((dst_negative_scale_omit_resultfirst) + (dst_negative_scale_omit_resultfirst)))) * S ((((dst_positive_code_omit_resultfirst) + (dst_positive_scale_omit_resultfirst)) * S ((dst_positive_code_omit_resultfirst) + (dst_positive_scale_omit_resultfirst)) + ((dst_positive_scale_omit_resultfirst) + (dst_positive_scale_omit_resultfirst))) + (((dst_negative_code_omit_resultfirst) + (dst_negative_scale_omit_resultfirst)) * S ((dst_negative_code_omit_resultfirst) + (dst_negative_scale_omit_resultfirst)) + ((dst_negative_scale_omit_resultfirst) + (dst_negative_scale_omit_resultfirst)))) + ((((dst_negative_code_omit_resultfirst) + (dst_negative_scale_omit_resultfirst)) * S ((dst_negative_code_omit_resultfirst) + (dst_negative_scale_omit_resultfirst)) + ((dst_negative_scale_omit_resultfirst) + (dst_negative_scale_omit_resultfirst))) + (((dst_negative_code_omit_resultfirst) + (dst_negative_scale_omit_resultfirst)) * S ((dst_negative_code_omit_resultfirst) + (dst_negative_scale_omit_resultfirst)) + ((dst_negative_scale_omit_resultfirst) + (dst_negative_scale_omit_resultfirst)))))) /\ (((((exists ff_h_pvs_omit_resultfirstpositive. ff_h_pvs_omit_resultfirstpositive + S (dst_positive_omit_resultfirst) = S ((S (a)) * dst_positive_scale_omit_resultfirst)) /\ exists ff_q_pvs_omit_resultfirstpositive. dst_positive_code_omit_resultfirst = ff_q_pvs_omit_resultfirstpositive * S ((S (a)) * dst_positive_scale_omit_resultfirst) + (dst_positive_omit_resultfirst))) /\ (((((exists ff_h_pvs_omit_resultfirstnegative. ff_h_pvs_omit_resultfirstnegative + S (dst_negative_omit_resultfirst) = S ((S (a)) * dst_negative_scale_omit_resultfirst)) /\ exists ff_q_pvs_omit_resultfirstnegative. dst_negative_code_omit_resultfirst = ff_q_pvs_omit_resultfirstnegative * S ((S (a)) * dst_negative_scale_omit_resultfirst) + (dst_negative_omit_resultfirst))) /\ (exists ge_balance_positive_omit_resultfirstvalue ge_balance_negative_omit_resultfirstvalue. (((((dfg_first_omit_result) = 2 * (ge_balance_positive_omit_resultfirstvalue) /\ (ge_balance_negative_omit_resultfirstvalue) = 0) \/ exists ge_signed_half_omit_resultfirstvaluedecode. (((dfg_first_omit_result) = 2 * ge_signed_half_omit_resultfirstvaluedecode + 1 /\ (ge_balance_positive_omit_resultfirstvalue) = 0) /\ (ge_balance_negative_omit_resultfirstvalue) = S ge_signed_half_omit_resultfirstvaluedecode))) /\ ((dst_positive_omit_resultfirst) + ge_balance_negative_omit_resultfirstvalue = (dst_negative_omit_resultfirst) + ge_balance_positive_omit_resultfirstvalue))))))))) /\ (((exists dst_positive_code_omit_resultlast dst_positive_scale_omit_resultlast dst_negative_code_omit_resultlast dst_negative_scale_omit_resultlast dst_positive_omit_resultlast dst_negative_omit_resultlast. (((H) = (((((dst_positive_code_omit_resultlast) + (dst_positive_scale_omit_resultlast)) * S ((dst_positive_code_omit_resultlast) + (dst_positive_scale_omit_resultlast)) + ((dst_positive_scale_omit_resultlast) + (dst_positive_scale_omit_resultlast))) + (((dst_negative_code_omit_resultlast) + (dst_negative_scale_omit_resultlast)) * S ((dst_negative_code_omit_resultlast) + (dst_negative_scale_omit_resultlast)) + ((dst_negative_scale_omit_resultlast) + (dst_negative_scale_omit_resultlast)))) * S ((((dst_positive_code_omit_resultlast) + (dst_positive_scale_omit_resultlast)) * S ((dst_positive_code_omit_resultlast) + (dst_positive_scale_omit_resultlast)) + ((dst_positive_scale_omit_resultlast) + (dst_positive_scale_omit_resultlast))) + (((dst_negative_code_omit_resultlast) + (dst_negative_scale_omit_resultlast)) * S ((dst_negative_code_omit_resultlast) + (dst_negative_scale_omit_resultlast)) + ((dst_negative_scale_omit_resultlast) + (dst_negative_scale_omit_resultlast)))) + ((((dst_negative_code_omit_resultlast) + (dst_negative_scale_omit_resultlast)) * S ((dst_negative_code_omit_resultlast) + (dst_negative_scale_omit_resultlast)) + ((dst_negative_scale_omit_resultlast) + (dst_negative_scale_omit_resultlast))) + (((dst_negative_code_omit_resultlast) + (dst_negative_scale_omit_resultlast)) * S ((dst_negative_code_omit_resultlast) + (dst_negative_scale_omit_resultlast)) + ((dst_negative_scale_omit_resultlast) + (dst_negative_scale_omit_resultlast)))))) /\ (((((exists ff_h_pvs_omit_resultlastpositive. ff_h_pvs_omit_resultlastpositive + S (dst_positive_omit_resultlast) = S ((S (e)) * dst_positive_scale_omit_resultlast)) /\ exists ff_q_pvs_omit_resultlastpositive. dst_positive_code_omit_resultlast = ff_q_pvs_omit_resultlastpositive * S ((S (e)) * dst_positive_scale_omit_resultlast) + (dst_positive_omit_resultlast))) /\ (((((exists ff_h_pvs_omit_resultlastnegative. ff_h_pvs_omit_resultlastnegative + S (dst_negative_omit_resultlast) = S ((S (e)) * dst_negative_scale_omit_resultlast)) /\ exists ff_q_pvs_omit_resultlastnegative. dst_negative_code_omit_resultlast = ff_q_pvs_omit_resultlastnegative * S ((S (e)) * dst_negative_scale_omit_resultlast) + (dst_negative_omit_resultlast))) /\ (exists ge_balance_positive_omit_resultlastvalue ge_balance_negative_omit_resultlastvalue. (((((dfg_last_omit_result) = 2 * (ge_balance_positive_omit_resultlastvalue) /\ (ge_balance_negative_omit_resultlastvalue) = 0) \/ exists ge_signed_half_omit_resultlastvaluedecode. (((dfg_last_omit_result) = 2 * ge_signed_half_omit_resultlastvaluedecode + 1 /\ (ge_balance_positive_omit_resultlastvalue) = 0) /\ (ge_balance_negative_omit_resultlastvalue) = S ge_signed_half_omit_resultlastvaluedecode))) /\ ((dst_positive_omit_resultlast) + ge_balance_negative_omit_resultlastvalue = (dst_negative_omit_resultlast) + ge_balance_positive_omit_resultlastvalue))))))))) /\ (((exists dst_positive_code_omit_resultmiddle dst_positive_scale_omit_resultmiddle dst_negative_code_omit_resultmiddle dst_negative_scale_omit_resultmiddle dst_positive_omit_resultmiddle dst_negative_omit_resultmiddle. (((G) = (((((dst_positive_code_omit_resultmiddle) + (dst_positive_scale_omit_resultmiddle)) * S ((dst_positive_code_omit_resultmiddle) + (dst_positive_scale_omit_resultmiddle)) + ((dst_positive_scale_omit_resultmiddle) + (dst_positive_scale_omit_resultmiddle))) + (((dst_negative_code_omit_resultmiddle) + (dst_negative_scale_omit_resultmiddle)) * S ((dst_negative_code_omit_resultmiddle) + (dst_negative_scale_omit_resultmiddle)) + ((dst_negative_scale_omit_resultmiddle) + (dst_negative_scale_omit_resultmiddle)))) * S ((((dst_positive_code_omit_resultmiddle) + (dst_positive_scale_omit_resultmiddle)) * S ((dst_positive_code_omit_resultmiddle) + (dst_positive_scale_omit_resultmiddle)) + ((dst_positive_scale_omit_resultmiddle) + (dst_positive_scale_omit_resultmiddle))) + (((dst_negative_code_omit_resultmiddle) + (dst_negative_scale_omit_resultmiddle)) * S ((dst_negative_code_omit_resultmiddle) + (dst_negative_scale_omit_resultmiddle)) + ((dst_negative_scale_omit_resultmiddle) + (dst_negative_scale_omit_resultmiddle)))) + ((((dst_negative_code_omit_resultmiddle) + (dst_negative_scale_omit_resultmiddle)) * S ((dst_negative_code_omit_resultmiddle) + (dst_negative_scale_omit_resultmiddle)) + ((dst_negative_scale_omit_resultmiddle) + (dst_negative_scale_omit_resultmiddle))) + (((dst_negative_code_omit_resultmiddle) + (dst_negative_scale_omit_resultmiddle)) * S ((dst_negative_code_omit_resultmiddle) + (dst_negative_scale_omit_resultmiddle)) + ((dst_negative_scale_omit_resultmiddle) + (dst_negative_scale_omit_resultmiddle)))))) /\ (((((exists ff_h_pvs_omit_resultmiddlepositive. ff_h_pvs_omit_resultmiddlepositive + S (dst_positive_omit_resultmiddle) = S ((S (dfg_middle_omit_result)) * dst_positive_scale_omit_resultmiddle)) /\ exists ff_q_pvs_omit_resultmiddlepositive. dst_positive_code_omit_resultmiddle = ff_q_pvs_omit_resultmiddlepositive * S ((S (dfg_middle_omit_result)) * dst_positive_scale_omit_resultmiddle) + (dst_positive_omit_resultmiddle))) /\ (((((exists ff_h_pvs_omit_resultmiddlenegative. ff_h_pvs_omit_resultmiddlenegative + S (dst_negative_omit_resultmiddle) = S ((S (dfg_middle_omit_result)) * dst_negative_scale_omit_resultmiddle)) /\ exists ff_q_pvs_omit_resultmiddlenegative. dst_negative_code_omit_resultmiddle = ff_q_pvs_omit_resultmiddlenegative * S ((S (dfg_middle_omit_result)) * dst_negative_scale_omit_resultmiddle) + (dst_negative_omit_resultmiddle))) /\ (exists ge_balance_positive_omit_resultmiddlevalue ge_balance_negative_omit_resultmiddlevalue. (((((dfg_value_omit_result) = 2 * (ge_balance_positive_omit_resultmiddlevalue) /\ (ge_balance_negative_omit_resultmiddlevalue) = 0) \/ exists ge_signed_half_omit_resultmiddlevaluedecode. (((dfg_value_omit_result) = 2 * ge_signed_half_omit_resultmiddlevaluedecode + 1 /\ (ge_balance_positive_omit_resultmiddlevalue) = 0) /\ (ge_balance_negative_omit_resultmiddlevalue) = S ge_signed_half_omit_resultmiddlevaluedecode))) /\ ((dst_positive_omit_resultmiddle) + ge_balance_negative_omit_resultmiddlevalue = (dst_negative_omit_resultmiddle) + ge_balance_positive_omit_resultmiddlevalue))))))))) /\ (exists dfg_inner_omit_resultproduct. ((exists sto_ap_omit_resultproductinner sto_an_omit_resultproductinner sto_bp_omit_resultproductinner sto_bn_omit_resultproductinner sto_cp_omit_resultproductinner sto_cn_omit_resultproductinner. (((((dfg_last_omit_result) = 2 * (sto_ap_omit_resultproductinner) /\ (sto_an_omit_resultproductinner) = 0) \/ exists ge_signed_half_omit_resultproductinnerleft. (((dfg_last_omit_result) = 2 * ge_signed_half_omit_resultproductinnerleft + 1 /\ (sto_ap_omit_resultproductinner) = 0) /\ (sto_an_omit_resultproductinner) = S ge_signed_half_omit_resultproductinnerleft))) /\ ((((((dfg_value_omit_result) = 2 * (sto_bp_omit_resultproductinner) /\ (sto_bn_omit_resultproductinner) = 0) \/ exists ge_signed_half_omit_resultproductinnerright. (((dfg_value_omit_result) = 2 * ge_signed_half_omit_resultproductinnerright + 1 /\ (sto_bp_omit_resultproductinner) = 0) /\ (sto_bn_omit_resultproductinner) = S ge_signed_half_omit_resultproductinnerright))) /\ ((((((dfg_inner_omit_resultproduct) = 2 * (sto_cp_omit_resultproductinner) /\ (sto_cn_omit_resultproductinner) = 0) \/ exists ge_signed_half_omit_resultproductinneroutput. (((dfg_inner_omit_resultproduct) = 2 * ge_signed_half_omit_resultproductinneroutput + 1 /\ (sto_cp_omit_resultproductinner) = 0) /\ (sto_cn_omit_resultproductinner) = S ge_signed_half_omit_resultproductinneroutput))) /\ ((sto_ap_omit_resultproductinner * sto_bp_omit_resultproductinner + sto_an_omit_resultproductinner * sto_bn_omit_resultproductinner) + sto_cn_omit_resultproductinner = (sto_ap_omit_resultproductinner * sto_bn_omit_resultproductinner + sto_an_omit_resultproductinner * sto_bp_omit_resultproductinner) + sto_cp_omit_resultproductinner))))))) /\ (exists sto_ap_omit_resultproductouter sto_an_omit_resultproductouter sto_bp_omit_resultproductouter sto_bn_omit_resultproductouter sto_cp_omit_resultproductouter sto_cn_omit_resultproductouter. (((((dfg_first_omit_result) = 2 * (sto_ap_omit_resultproductouter) /\ (sto_an_omit_resultproductouter) = 0) \/ exists ge_signed_half_omit_resultproductouterleft. (((dfg_first_omit_result) = 2 * ge_signed_half_omit_resultproductouterleft + 1 /\ (sto_ap_omit_resultproductouter) = 0) /\ (sto_an_omit_resultproductouter) = S ge_signed_half_omit_resultproductouterleft))) /\ ((((((dfg_inner_omit_resultproduct) = 2 * (sto_bp_omit_resultproductouter) /\ (sto_bn_omit_resultproductouter) = 0) \/ exists ge_signed_half_omit_resultproductouterright. (((dfg_inner_omit_resultproduct) = 2 * ge_signed_half_omit_resultproductouterright + 1 /\ (sto_bp_omit_resultproductouter) = 0) /\ (sto_bn_omit_resultproductouter) = S ge_signed_half_omit_resultproductouterright))) /\ ((((((0) = 2 * (sto_cp_omit_resultproductouter) /\ (sto_cn_omit_resultproductouter) = 0) \/ exists ge_signed_half_omit_resultproductouteroutput. (((0) = 2 * ge_signed_half_omit_resultproductouteroutput + 1 /\ (sto_cp_omit_resultproductouter) = 0) /\ (sto_cn_omit_resultproductouter) = S ge_signed_half_omit_resultproductouteroutput))) /\ ((sto_ap_omit_resultproductouter * sto_bp_omit_resultproductouter + sto_an_omit_resultproductouter * sto_bn_omit_resultproductouter) + sto_cn_omit_resultproductouter = (sto_ap_omit_resultproductouter * sto_bn_omit_resultproductouter + sto_an_omit_resultproductouter * sto_bp_omit_resultproductouter) + sto_cp_omit_resultproductouter))))))))))))))))))))) \/ ((((a)=0 \/ ((e)=0 \/ ~(exists pvs_factor_omit_resultomittednondivisor. (n) = ((a)*(e)) * pvs_factor_omit_resultomittednondivisor))) /\ ((0)=0))))Complete tactic proof in conservative notation
All 11 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
11 script commands · 4 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–7
02Separate the logical casesL8–9
03Use earlier factsL10–10
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L10
exact h
04Calculate and transport equalitiesL11–11
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L11
refl