DF0013

dirichlet_grid_nondivisor_row_value_zero

A zero or nondivisor first factor forces every actual row cell to zero, independently of input values at zero.

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. a = 0 ∨ ¬Dvd(a,n) → DirichletGridEntry(F,G,H,n,a,e,z) → z = 0

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

Definition DAG

DirichletGridEntry(F,G,H,n,a,e,z) · 1Dvd(d,n) · 1

Actual proof prerequisites

dirichlet_grid_entry_omitted_valuemul_assoc · checked external prerequisite
Original expanded first-order statement 
forall F G H n a e z. (a=0 \/ ~(exists pvs_factor_zero_row_guard. (n) = (a) * pvs_factor_zero_row_guard)) -> ((((~((a)=0)) /\ (((~((e)=0)) /\ (exists dfg_middle_zero_row_cell dfg_first_zero_row_cell dfg_last_zero_row_cell dfg_value_zero_row_cell. (((n)=((a)*(e))*dfg_middle_zero_row_cell) /\ (((exists dst_positive_code_zero_row_cellfirst dst_positive_scale_zero_row_cellfirst dst_negative_code_zero_row_cellfirst dst_negative_scale_zero_row_cellfirst dst_positive_zero_row_cellfirst dst_negative_zero_row_cellfirst. (((F) = (((((dst_positive_code_zero_row_cellfirst) + (dst_positive_scale_zero_row_cellfirst)) * S ((dst_positive_code_zero_row_cellfirst) + (dst_positive_scale_zero_row_cellfirst)) + ((dst_positive_scale_zero_row_cellfirst) + (dst_positive_scale_zero_row_cellfirst))) + (((dst_negative_code_zero_row_cellfirst) + (dst_negative_scale_zero_row_cellfirst)) * S ((dst_negative_code_zero_row_cellfirst) + (dst_negative_scale_zero_row_cellfirst)) + ((dst_negative_scale_zero_row_cellfirst) + (dst_negative_scale_zero_row_cellfirst)))) * S ((((dst_positive_code_zero_row_cellfirst) + (dst_positive_scale_zero_row_cellfirst)) * S ((dst_positive_code_zero_row_cellfirst) + (dst_positive_scale_zero_row_cellfirst)) + ((dst_positive_scale_zero_row_cellfirst) + (dst_positive_scale_zero_row_cellfirst))) + (((dst_negative_code_zero_row_cellfirst) + (dst_negative_scale_zero_row_cellfirst)) * S ((dst_negative_code_zero_row_cellfirst) + (dst_negative_scale_zero_row_cellfirst)) + ((dst_negative_scale_zero_row_cellfirst) + (dst_negative_scale_zero_row_cellfirst)))) + ((((dst_negative_code_zero_row_cellfirst) + (dst_negative_scale_zero_row_cellfirst)) * S ((dst_negative_code_zero_row_cellfirst) + (dst_negative_scale_zero_row_cellfirst)) + ((dst_negative_scale_zero_row_cellfirst) + (dst_negative_scale_zero_row_cellfirst))) + (((dst_negative_code_zero_row_cellfirst) + (dst_negative_scale_zero_row_cellfirst)) * S ((dst_negative_code_zero_row_cellfirst) + (dst_negative_scale_zero_row_cellfirst)) + ((dst_negative_scale_zero_row_cellfirst) + (dst_negative_scale_zero_row_cellfirst)))))) /\ (((((exists ff_h_pvs_zero_row_cellfirstpositive. ff_h_pvs_zero_row_cellfirstpositive + S (dst_positive_zero_row_cellfirst) = S ((S (a)) * dst_positive_scale_zero_row_cellfirst)) /\ exists ff_q_pvs_zero_row_cellfirstpositive. dst_positive_code_zero_row_cellfirst = ff_q_pvs_zero_row_cellfirstpositive * S ((S (a)) * dst_positive_scale_zero_row_cellfirst) + (dst_positive_zero_row_cellfirst))) /\ (((((exists ff_h_pvs_zero_row_cellfirstnegative. ff_h_pvs_zero_row_cellfirstnegative + S (dst_negative_zero_row_cellfirst) = S ((S (a)) * dst_negative_scale_zero_row_cellfirst)) /\ exists ff_q_pvs_zero_row_cellfirstnegative. dst_negative_code_zero_row_cellfirst = ff_q_pvs_zero_row_cellfirstnegative * S ((S (a)) * dst_negative_scale_zero_row_cellfirst) + (dst_negative_zero_row_cellfirst))) /\ (exists ge_balance_positive_zero_row_cellfirstvalue ge_balance_negative_zero_row_cellfirstvalue. (((((dfg_first_zero_row_cell) = 2 * (ge_balance_positive_zero_row_cellfirstvalue) /\ (ge_balance_negative_zero_row_cellfirstvalue) = 0) \/ exists ge_signed_half_zero_row_cellfirstvaluedecode. (((dfg_first_zero_row_cell) = 2 * ge_signed_half_zero_row_cellfirstvaluedecode + 1 /\ (ge_balance_positive_zero_row_cellfirstvalue) = 0) /\ (ge_balance_negative_zero_row_cellfirstvalue) = S ge_signed_half_zero_row_cellfirstvaluedecode))) /\ ((dst_positive_zero_row_cellfirst) + ge_balance_negative_zero_row_cellfirstvalue = (dst_negative_zero_row_cellfirst) + ge_balance_positive_zero_row_cellfirstvalue))))))))) /\ (((exists dst_positive_code_zero_row_celllast dst_positive_scale_zero_row_celllast dst_negative_code_zero_row_celllast dst_negative_scale_zero_row_celllast dst_positive_zero_row_celllast dst_negative_zero_row_celllast. (((H) = (((((dst_positive_code_zero_row_celllast) + (dst_positive_scale_zero_row_celllast)) * S ((dst_positive_code_zero_row_celllast) + (dst_positive_scale_zero_row_celllast)) + ((dst_positive_scale_zero_row_celllast) + (dst_positive_scale_zero_row_celllast))) + (((dst_negative_code_zero_row_celllast) + (dst_negative_scale_zero_row_celllast)) * S ((dst_negative_code_zero_row_celllast) + (dst_negative_scale_zero_row_celllast)) + ((dst_negative_scale_zero_row_celllast) + (dst_negative_scale_zero_row_celllast)))) * S ((((dst_positive_code_zero_row_celllast) + (dst_positive_scale_zero_row_celllast)) * S ((dst_positive_code_zero_row_celllast) + (dst_positive_scale_zero_row_celllast)) + ((dst_positive_scale_zero_row_celllast) + (dst_positive_scale_zero_row_celllast))) + (((dst_negative_code_zero_row_celllast) + (dst_negative_scale_zero_row_celllast)) * S ((dst_negative_code_zero_row_celllast) + (dst_negative_scale_zero_row_celllast)) + ((dst_negative_scale_zero_row_celllast) + (dst_negative_scale_zero_row_celllast)))) + ((((dst_negative_code_zero_row_celllast) + (dst_negative_scale_zero_row_celllast)) * S ((dst_negative_code_zero_row_celllast) + (dst_negative_scale_zero_row_celllast)) + ((dst_negative_scale_zero_row_celllast) + (dst_negative_scale_zero_row_celllast))) + (((dst_negative_code_zero_row_celllast) + (dst_negative_scale_zero_row_celllast)) * S ((dst_negative_code_zero_row_celllast) + (dst_negative_scale_zero_row_celllast)) + ((dst_negative_scale_zero_row_celllast) + (dst_negative_scale_zero_row_celllast)))))) /\ (((((exists ff_h_pvs_zero_row_celllastpositive. ff_h_pvs_zero_row_celllastpositive + S (dst_positive_zero_row_celllast) = S ((S (e)) * dst_positive_scale_zero_row_celllast)) /\ exists ff_q_pvs_zero_row_celllastpositive. dst_positive_code_zero_row_celllast = ff_q_pvs_zero_row_celllastpositive * S ((S (e)) * dst_positive_scale_zero_row_celllast) + (dst_positive_zero_row_celllast))) /\ (((((exists ff_h_pvs_zero_row_celllastnegative. ff_h_pvs_zero_row_celllastnegative + S (dst_negative_zero_row_celllast) = S ((S (e)) * dst_negative_scale_zero_row_celllast)) /\ exists ff_q_pvs_zero_row_celllastnegative. dst_negative_code_zero_row_celllast = ff_q_pvs_zero_row_celllastnegative * S ((S (e)) * dst_negative_scale_zero_row_celllast) + (dst_negative_zero_row_celllast))) /\ (exists ge_balance_positive_zero_row_celllastvalue ge_balance_negative_zero_row_celllastvalue. (((((dfg_last_zero_row_cell) = 2 * (ge_balance_positive_zero_row_celllastvalue) /\ (ge_balance_negative_zero_row_celllastvalue) = 0) \/ exists ge_signed_half_zero_row_celllastvaluedecode. (((dfg_last_zero_row_cell) = 2 * ge_signed_half_zero_row_celllastvaluedecode + 1 /\ (ge_balance_positive_zero_row_celllastvalue) = 0) /\ (ge_balance_negative_zero_row_celllastvalue) = S ge_signed_half_zero_row_celllastvaluedecode))) /\ ((dst_positive_zero_row_celllast) + ge_balance_negative_zero_row_celllastvalue = (dst_negative_zero_row_celllast) + ge_balance_positive_zero_row_celllastvalue))))))))) /\ (((exists dst_positive_code_zero_row_cellmiddle dst_positive_scale_zero_row_cellmiddle dst_negative_code_zero_row_cellmiddle dst_negative_scale_zero_row_cellmiddle dst_positive_zero_row_cellmiddle dst_negative_zero_row_cellmiddle. (((G) = (((((dst_positive_code_zero_row_cellmiddle) + (dst_positive_scale_zero_row_cellmiddle)) * S ((dst_positive_code_zero_row_cellmiddle) + (dst_positive_scale_zero_row_cellmiddle)) + ((dst_positive_scale_zero_row_cellmiddle) + (dst_positive_scale_zero_row_cellmiddle))) + (((dst_negative_code_zero_row_cellmiddle) + (dst_negative_scale_zero_row_cellmiddle)) * S ((dst_negative_code_zero_row_cellmiddle) + (dst_negative_scale_zero_row_cellmiddle)) + ((dst_negative_scale_zero_row_cellmiddle) + (dst_negative_scale_zero_row_cellmiddle)))) * S ((((dst_positive_code_zero_row_cellmiddle) + (dst_positive_scale_zero_row_cellmiddle)) * S ((dst_positive_code_zero_row_cellmiddle) + (dst_positive_scale_zero_row_cellmiddle)) + ((dst_positive_scale_zero_row_cellmiddle) + (dst_positive_scale_zero_row_cellmiddle))) + (((dst_negative_code_zero_row_cellmiddle) + (dst_negative_scale_zero_row_cellmiddle)) * S ((dst_negative_code_zero_row_cellmiddle) + (dst_negative_scale_zero_row_cellmiddle)) + ((dst_negative_scale_zero_row_cellmiddle) + (dst_negative_scale_zero_row_cellmiddle)))) + ((((dst_negative_code_zero_row_cellmiddle) + (dst_negative_scale_zero_row_cellmiddle)) * S ((dst_negative_code_zero_row_cellmiddle) + (dst_negative_scale_zero_row_cellmiddle)) + ((dst_negative_scale_zero_row_cellmiddle) + (dst_negative_scale_zero_row_cellmiddle))) + (((dst_negative_code_zero_row_cellmiddle) + (dst_negative_scale_zero_row_cellmiddle)) * S ((dst_negative_code_zero_row_cellmiddle) + (dst_negative_scale_zero_row_cellmiddle)) + ((dst_negative_scale_zero_row_cellmiddle) + (dst_negative_scale_zero_row_cellmiddle)))))) /\ (((((exists ff_h_pvs_zero_row_cellmiddlepositive. ff_h_pvs_zero_row_cellmiddlepositive + S (dst_positive_zero_row_cellmiddle) = S ((S (dfg_middle_zero_row_cell)) * dst_positive_scale_zero_row_cellmiddle)) /\ exists ff_q_pvs_zero_row_cellmiddlepositive. dst_positive_code_zero_row_cellmiddle = ff_q_pvs_zero_row_cellmiddlepositive * S ((S (dfg_middle_zero_row_cell)) * dst_positive_scale_zero_row_cellmiddle) + (dst_positive_zero_row_cellmiddle))) /\ (((((exists ff_h_pvs_zero_row_cellmiddlenegative. ff_h_pvs_zero_row_cellmiddlenegative + S (dst_negative_zero_row_cellmiddle) = S ((S (dfg_middle_zero_row_cell)) * dst_negative_scale_zero_row_cellmiddle)) /\ exists ff_q_pvs_zero_row_cellmiddlenegative. dst_negative_code_zero_row_cellmiddle = ff_q_pvs_zero_row_cellmiddlenegative * S ((S (dfg_middle_zero_row_cell)) * dst_negative_scale_zero_row_cellmiddle) + (dst_negative_zero_row_cellmiddle))) /\ (exists ge_balance_positive_zero_row_cellmiddlevalue ge_balance_negative_zero_row_cellmiddlevalue. (((((dfg_value_zero_row_cell) = 2 * (ge_balance_positive_zero_row_cellmiddlevalue) /\ (ge_balance_negative_zero_row_cellmiddlevalue) = 0) \/ exists ge_signed_half_zero_row_cellmiddlevaluedecode. (((dfg_value_zero_row_cell) = 2 * ge_signed_half_zero_row_cellmiddlevaluedecode + 1 /\ (ge_balance_positive_zero_row_cellmiddlevalue) = 0) /\ (ge_balance_negative_zero_row_cellmiddlevalue) = S ge_signed_half_zero_row_cellmiddlevaluedecode))) /\ ((dst_positive_zero_row_cellmiddle) + ge_balance_negative_zero_row_cellmiddlevalue = (dst_negative_zero_row_cellmiddle) + ge_balance_positive_zero_row_cellmiddlevalue))))))))) /\ (exists dfg_inner_zero_row_cellproduct. ((exists sto_ap_zero_row_cellproductinner sto_an_zero_row_cellproductinner sto_bp_zero_row_cellproductinner sto_bn_zero_row_cellproductinner sto_cp_zero_row_cellproductinner sto_cn_zero_row_cellproductinner. (((((dfg_last_zero_row_cell) = 2 * (sto_ap_zero_row_cellproductinner) /\ (sto_an_zero_row_cellproductinner) = 0) \/ exists ge_signed_half_zero_row_cellproductinnerleft. (((dfg_last_zero_row_cell) = 2 * ge_signed_half_zero_row_cellproductinnerleft + 1 /\ (sto_ap_zero_row_cellproductinner) = 0) /\ (sto_an_zero_row_cellproductinner) = S ge_signed_half_zero_row_cellproductinnerleft))) /\ ((((((dfg_value_zero_row_cell) = 2 * (sto_bp_zero_row_cellproductinner) /\ (sto_bn_zero_row_cellproductinner) = 0) \/ exists ge_signed_half_zero_row_cellproductinnerright. (((dfg_value_zero_row_cell) = 2 * ge_signed_half_zero_row_cellproductinnerright + 1 /\ (sto_bp_zero_row_cellproductinner) = 0) /\ (sto_bn_zero_row_cellproductinner) = S ge_signed_half_zero_row_cellproductinnerright))) /\ ((((((dfg_inner_zero_row_cellproduct) = 2 * (sto_cp_zero_row_cellproductinner) /\ (sto_cn_zero_row_cellproductinner) = 0) \/ exists ge_signed_half_zero_row_cellproductinneroutput. (((dfg_inner_zero_row_cellproduct) = 2 * ge_signed_half_zero_row_cellproductinneroutput + 1 /\ (sto_cp_zero_row_cellproductinner) = 0) /\ (sto_cn_zero_row_cellproductinner) = S ge_signed_half_zero_row_cellproductinneroutput))) /\ ((sto_ap_zero_row_cellproductinner * sto_bp_zero_row_cellproductinner + sto_an_zero_row_cellproductinner * sto_bn_zero_row_cellproductinner) + sto_cn_zero_row_cellproductinner = (sto_ap_zero_row_cellproductinner * sto_bn_zero_row_cellproductinner + sto_an_zero_row_cellproductinner * sto_bp_zero_row_cellproductinner) + sto_cp_zero_row_cellproductinner))))))) /\ (exists sto_ap_zero_row_cellproductouter sto_an_zero_row_cellproductouter sto_bp_zero_row_cellproductouter sto_bn_zero_row_cellproductouter sto_cp_zero_row_cellproductouter sto_cn_zero_row_cellproductouter. (((((dfg_first_zero_row_cell) = 2 * (sto_ap_zero_row_cellproductouter) /\ (sto_an_zero_row_cellproductouter) = 0) \/ exists ge_signed_half_zero_row_cellproductouterleft. (((dfg_first_zero_row_cell) = 2 * ge_signed_half_zero_row_cellproductouterleft + 1 /\ (sto_ap_zero_row_cellproductouter) = 0) /\ (sto_an_zero_row_cellproductouter) = S ge_signed_half_zero_row_cellproductouterleft))) /\ ((((((dfg_inner_zero_row_cellproduct) = 2 * (sto_bp_zero_row_cellproductouter) /\ (sto_bn_zero_row_cellproductouter) = 0) \/ exists ge_signed_half_zero_row_cellproductouterright. (((dfg_inner_zero_row_cellproduct) = 2 * ge_signed_half_zero_row_cellproductouterright + 1 /\ (sto_bp_zero_row_cellproductouter) = 0) /\ (sto_bn_zero_row_cellproductouter) = S ge_signed_half_zero_row_cellproductouterright))) /\ ((((((z) = 2 * (sto_cp_zero_row_cellproductouter) /\ (sto_cn_zero_row_cellproductouter) = 0) \/ exists ge_signed_half_zero_row_cellproductouteroutput. (((z) = 2 * ge_signed_half_zero_row_cellproductouteroutput + 1 /\ (sto_cp_zero_row_cellproductouter) = 0) /\ (sto_cn_zero_row_cellproductouter) = S ge_signed_half_zero_row_cellproductouteroutput))) /\ ((sto_ap_zero_row_cellproductouter * sto_bp_zero_row_cellproductouter + sto_an_zero_row_cellproductouter * sto_bn_zero_row_cellproductouter) + sto_cn_zero_row_cellproductouter = (sto_ap_zero_row_cellproductouter * sto_bn_zero_row_cellproductouter + sto_an_zero_row_cellproductouter * sto_bp_zero_row_cellproductouter) + sto_cp_zero_row_cellproductouter))))))))))))))))))))) \/ ((((a)=0 \/ ((e)=0 \/ ~(exists pvs_factor_zero_row_cellomittednondivisor. (n) = ((a)*(e)) * pvs_factor_zero_row_cellomittednondivisor))) /\ ((z)=0)))) -> z=0

Complete tactic proof in conservative notation

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

30 script commands · 11 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.

Named ingredients (1)
dirichlet grid entry omitted value
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 ho
  9. L9
    intro hz
02Use earlier factsL10–17

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

  1. L10
    specialize dirichlet_grid_entry_omitted_value (F)
  2. L11
    specialize dirichlet_grid_entry_omitted_value (G)
  3. L12
    specialize dirichlet_grid_entry_omitted_value (H)
  4. L13
    specialize dirichlet_grid_entry_omitted_value (n)
  5. L14
    specialize dirichlet_grid_entry_omitted_value (a)
  6. L15
    specialize dirichlet_grid_entry_omitted_value (e)
  7. L16
    specialize dirichlet_grid_entry_omitted_value (z)
  8. L17
    apply dirichlet_grid_entry_omitted_value
03Separate the logical casesL18–19

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

  1. L18
    cases ho
  2. L19
    left
04Use earlier factsL20–20

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

  1. L20
    exact ho_left
05Separate the logical casesL21–22

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

  1. L21
    right
  2. L22
    right
06Fix variables and assumptionsL23–23

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

  1. L23
    intro hdiv
07Separate the logical casesL24–24

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

  1. L24
    cases hdiv
08Use earlier factsL25–25

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

  1. L25
    apply ho_right
09Construct an explicit witnessL26–26

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

  1. L26
    exists e*x
10Calculate and transport equalitiesL27–27

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

  1. L27
    trans (a*e)*x
11Use earlier factsL28–30

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

  1. L28
    exact hdiv_witness
  2. L29
    apply mul_assoc
  3. L30
    exact hz

Library-wide reading audit

Original defined command ledger · 30 lines
  1. 0001intro F
  2. 0002intro G
  3. 0003intro H
  4. 0004intro n
  5. 0005intro a
  6. 0006intro e
  7. 0007intro z
  8. 0008intro ho
  9. 0009intro hz
  10. 0010specialize dirichlet_grid_entry_omitted_value (F)
  11. 0011specialize dirichlet_grid_entry_omitted_value (G)
  12. 0012specialize dirichlet_grid_entry_omitted_value (H)
  13. 0013specialize dirichlet_grid_entry_omitted_value (n)
  14. 0014specialize dirichlet_grid_entry_omitted_value (a)
  15. 0015specialize dirichlet_grid_entry_omitted_value (e)
  16. 0016specialize dirichlet_grid_entry_omitted_value (z)
  17. 0017apply dirichlet_grid_entry_omitted_value
  18. 0018cases ho
  19. 0019left
  20. 0020exact ho_left
  21. 0021right
  22. 0022right
  23. 0023intro hdiv
  24. 0024cases hdiv
  25. 0025apply ho_right
  26. 0026exists e*x
  27. 0027trans (a*e)*x
  28. 0028exact hdiv_witness
  29. 0029apply mul_assoc
  30. 0030exact hz