DF0003

dirichlet_grid_entry_omitted_value

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Every actually omitted grid cell is zero; a retained factorization cannot coexist with its omitted guard.

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

Exact expanded first-order arithmetic statement

forall F G H n a e z. ((a)=0 \/ ((e)=0 \/ ~(exists pvs_factor_omitted_guardnondivisor. (n) = ((a)*(e)) * pvs_factor_omitted_guardnondivisor))) -> ((((~((a)=0)) /\ (((~((e)=0)) /\ (exists dfg_middle_omitted_cell dfg_first_omitted_cell dfg_last_omitted_cell dfg_value_omitted_cell. (((n)=((a)*(e))*dfg_middle_omitted_cell) /\ (((exists dst_positive_code_omitted_cellfirst dst_positive_scale_omitted_cellfirst dst_negative_code_omitted_cellfirst dst_negative_scale_omitted_cellfirst dst_positive_omitted_cellfirst dst_negative_omitted_cellfirst. (((F) = (((((dst_positive_code_omitted_cellfirst) + (dst_positive_scale_omitted_cellfirst)) * S ((dst_positive_code_omitted_cellfirst) + (dst_positive_scale_omitted_cellfirst)) + ((dst_positive_scale_omitted_cellfirst) + (dst_positive_scale_omitted_cellfirst))) + (((dst_negative_code_omitted_cellfirst) + (dst_negative_scale_omitted_cellfirst)) * S ((dst_negative_code_omitted_cellfirst) + (dst_negative_scale_omitted_cellfirst)) + ((dst_negative_scale_omitted_cellfirst) + (dst_negative_scale_omitted_cellfirst)))) * S ((((dst_positive_code_omitted_cellfirst) + (dst_positive_scale_omitted_cellfirst)) * S ((dst_positive_code_omitted_cellfirst) + (dst_positive_scale_omitted_cellfirst)) + ((dst_positive_scale_omitted_cellfirst) + (dst_positive_scale_omitted_cellfirst))) + (((dst_negative_code_omitted_cellfirst) + (dst_negative_scale_omitted_cellfirst)) * S ((dst_negative_code_omitted_cellfirst) + (dst_negative_scale_omitted_cellfirst)) + ((dst_negative_scale_omitted_cellfirst) + (dst_negative_scale_omitted_cellfirst)))) + ((((dst_negative_code_omitted_cellfirst) + (dst_negative_scale_omitted_cellfirst)) * S ((dst_negative_code_omitted_cellfirst) + (dst_negative_scale_omitted_cellfirst)) + ((dst_negative_scale_omitted_cellfirst) + (dst_negative_scale_omitted_cellfirst))) + (((dst_negative_code_omitted_cellfirst) + (dst_negative_scale_omitted_cellfirst)) * S ((dst_negative_code_omitted_cellfirst) + (dst_negative_scale_omitted_cellfirst)) + ((dst_negative_scale_omitted_cellfirst) + (dst_negative_scale_omitted_cellfirst)))))) /\ (((((exists ff_h_pvs_omitted_cellfirstpositive. ff_h_pvs_omitted_cellfirstpositive + S (dst_positive_omitted_cellfirst) = S ((S (a)) * dst_positive_scale_omitted_cellfirst)) /\ exists ff_q_pvs_omitted_cellfirstpositive. dst_positive_code_omitted_cellfirst = ff_q_pvs_omitted_cellfirstpositive * S ((S (a)) * dst_positive_scale_omitted_cellfirst) + (dst_positive_omitted_cellfirst))) /\ (((((exists ff_h_pvs_omitted_cellfirstnegative. ff_h_pvs_omitted_cellfirstnegative + S (dst_negative_omitted_cellfirst) = S ((S (a)) * dst_negative_scale_omitted_cellfirst)) /\ exists ff_q_pvs_omitted_cellfirstnegative. dst_negative_code_omitted_cellfirst = ff_q_pvs_omitted_cellfirstnegative * S ((S (a)) * dst_negative_scale_omitted_cellfirst) + (dst_negative_omitted_cellfirst))) /\ (exists ge_balance_positive_omitted_cellfirstvalue ge_balance_negative_omitted_cellfirstvalue. (((((dfg_first_omitted_cell) = 2 * (ge_balance_positive_omitted_cellfirstvalue) /\ (ge_balance_negative_omitted_cellfirstvalue) = 0) \/ exists ge_signed_half_omitted_cellfirstvaluedecode. (((dfg_first_omitted_cell) = 2 * ge_signed_half_omitted_cellfirstvaluedecode + 1 /\ (ge_balance_positive_omitted_cellfirstvalue) = 0) /\ (ge_balance_negative_omitted_cellfirstvalue) = S ge_signed_half_omitted_cellfirstvaluedecode))) /\ ((dst_positive_omitted_cellfirst) + ge_balance_negative_omitted_cellfirstvalue = (dst_negative_omitted_cellfirst) + ge_balance_positive_omitted_cellfirstvalue))))))))) /\ (((exists dst_positive_code_omitted_celllast dst_positive_scale_omitted_celllast dst_negative_code_omitted_celllast dst_negative_scale_omitted_celllast dst_positive_omitted_celllast dst_negative_omitted_celllast. (((H) = (((((dst_positive_code_omitted_celllast) + (dst_positive_scale_omitted_celllast)) * S ((dst_positive_code_omitted_celllast) + (dst_positive_scale_omitted_celllast)) + ((dst_positive_scale_omitted_celllast) + (dst_positive_scale_omitted_celllast))) + (((dst_negative_code_omitted_celllast) + (dst_negative_scale_omitted_celllast)) * S ((dst_negative_code_omitted_celllast) + (dst_negative_scale_omitted_celllast)) + ((dst_negative_scale_omitted_celllast) + (dst_negative_scale_omitted_celllast)))) * S ((((dst_positive_code_omitted_celllast) + (dst_positive_scale_omitted_celllast)) * S ((dst_positive_code_omitted_celllast) + (dst_positive_scale_omitted_celllast)) + ((dst_positive_scale_omitted_celllast) + (dst_positive_scale_omitted_celllast))) + (((dst_negative_code_omitted_celllast) + (dst_negative_scale_omitted_celllast)) * S ((dst_negative_code_omitted_celllast) + (dst_negative_scale_omitted_celllast)) + ((dst_negative_scale_omitted_celllast) + (dst_negative_scale_omitted_celllast)))) + ((((dst_negative_code_omitted_celllast) + (dst_negative_scale_omitted_celllast)) * S ((dst_negative_code_omitted_celllast) + (dst_negative_scale_omitted_celllast)) + ((dst_negative_scale_omitted_celllast) + (dst_negative_scale_omitted_celllast))) + (((dst_negative_code_omitted_celllast) + (dst_negative_scale_omitted_celllast)) * S ((dst_negative_code_omitted_celllast) + (dst_negative_scale_omitted_celllast)) + ((dst_negative_scale_omitted_celllast) + (dst_negative_scale_omitted_celllast)))))) /\ (((((exists ff_h_pvs_omitted_celllastpositive. ff_h_pvs_omitted_celllastpositive + S (dst_positive_omitted_celllast) = S ((S (e)) * dst_positive_scale_omitted_celllast)) /\ exists ff_q_pvs_omitted_celllastpositive. dst_positive_code_omitted_celllast = ff_q_pvs_omitted_celllastpositive * S ((S (e)) * dst_positive_scale_omitted_celllast) + (dst_positive_omitted_celllast))) /\ (((((exists ff_h_pvs_omitted_celllastnegative. ff_h_pvs_omitted_celllastnegative + S (dst_negative_omitted_celllast) = S ((S (e)) * dst_negative_scale_omitted_celllast)) /\ exists ff_q_pvs_omitted_celllastnegative. dst_negative_code_omitted_celllast = ff_q_pvs_omitted_celllastnegative * S ((S (e)) * dst_negative_scale_omitted_celllast) + (dst_negative_omitted_celllast))) /\ (exists ge_balance_positive_omitted_celllastvalue ge_balance_negative_omitted_celllastvalue. (((((dfg_last_omitted_cell) = 2 * (ge_balance_positive_omitted_celllastvalue) /\ (ge_balance_negative_omitted_celllastvalue) = 0) \/ exists ge_signed_half_omitted_celllastvaluedecode. (((dfg_last_omitted_cell) = 2 * ge_signed_half_omitted_celllastvaluedecode + 1 /\ (ge_balance_positive_omitted_celllastvalue) = 0) /\ (ge_balance_negative_omitted_celllastvalue) = S ge_signed_half_omitted_celllastvaluedecode))) /\ ((dst_positive_omitted_celllast) + ge_balance_negative_omitted_celllastvalue = (dst_negative_omitted_celllast) + ge_balance_positive_omitted_celllastvalue))))))))) /\ (((exists dst_positive_code_omitted_cellmiddle dst_positive_scale_omitted_cellmiddle dst_negative_code_omitted_cellmiddle dst_negative_scale_omitted_cellmiddle dst_positive_omitted_cellmiddle dst_negative_omitted_cellmiddle. (((G) = (((((dst_positive_code_omitted_cellmiddle) + (dst_positive_scale_omitted_cellmiddle)) * S ((dst_positive_code_omitted_cellmiddle) + (dst_positive_scale_omitted_cellmiddle)) + ((dst_positive_scale_omitted_cellmiddle) + (dst_positive_scale_omitted_cellmiddle))) + (((dst_negative_code_omitted_cellmiddle) + (dst_negative_scale_omitted_cellmiddle)) * S ((dst_negative_code_omitted_cellmiddle) + (dst_negative_scale_omitted_cellmiddle)) + ((dst_negative_scale_omitted_cellmiddle) + (dst_negative_scale_omitted_cellmiddle)))) * S ((((dst_positive_code_omitted_cellmiddle) + (dst_positive_scale_omitted_cellmiddle)) * S ((dst_positive_code_omitted_cellmiddle) + (dst_positive_scale_omitted_cellmiddle)) + ((dst_positive_scale_omitted_cellmiddle) + (dst_positive_scale_omitted_cellmiddle))) + (((dst_negative_code_omitted_cellmiddle) + (dst_negative_scale_omitted_cellmiddle)) * S ((dst_negative_code_omitted_cellmiddle) + (dst_negative_scale_omitted_cellmiddle)) + ((dst_negative_scale_omitted_cellmiddle) + (dst_negative_scale_omitted_cellmiddle)))) + ((((dst_negative_code_omitted_cellmiddle) + (dst_negative_scale_omitted_cellmiddle)) * S ((dst_negative_code_omitted_cellmiddle) + (dst_negative_scale_omitted_cellmiddle)) + ((dst_negative_scale_omitted_cellmiddle) + (dst_negative_scale_omitted_cellmiddle))) + (((dst_negative_code_omitted_cellmiddle) + (dst_negative_scale_omitted_cellmiddle)) * S ((dst_negative_code_omitted_cellmiddle) + (dst_negative_scale_omitted_cellmiddle)) + ((dst_negative_scale_omitted_cellmiddle) + (dst_negative_scale_omitted_cellmiddle)))))) /\ (((((exists ff_h_pvs_omitted_cellmiddlepositive. ff_h_pvs_omitted_cellmiddlepositive + S (dst_positive_omitted_cellmiddle) = S ((S (dfg_middle_omitted_cell)) * dst_positive_scale_omitted_cellmiddle)) /\ exists ff_q_pvs_omitted_cellmiddlepositive. dst_positive_code_omitted_cellmiddle = ff_q_pvs_omitted_cellmiddlepositive * S ((S (dfg_middle_omitted_cell)) * dst_positive_scale_omitted_cellmiddle) + (dst_positive_omitted_cellmiddle))) /\ (((((exists ff_h_pvs_omitted_cellmiddlenegative. ff_h_pvs_omitted_cellmiddlenegative + S (dst_negative_omitted_cellmiddle) = S ((S (dfg_middle_omitted_cell)) * dst_negative_scale_omitted_cellmiddle)) /\ exists ff_q_pvs_omitted_cellmiddlenegative. dst_negative_code_omitted_cellmiddle = ff_q_pvs_omitted_cellmiddlenegative * S ((S (dfg_middle_omitted_cell)) * dst_negative_scale_omitted_cellmiddle) + (dst_negative_omitted_cellmiddle))) /\ (exists ge_balance_positive_omitted_cellmiddlevalue ge_balance_negative_omitted_cellmiddlevalue. (((((dfg_value_omitted_cell) = 2 * (ge_balance_positive_omitted_cellmiddlevalue) /\ (ge_balance_negative_omitted_cellmiddlevalue) = 0) \/ exists ge_signed_half_omitted_cellmiddlevaluedecode. (((dfg_value_omitted_cell) = 2 * ge_signed_half_omitted_cellmiddlevaluedecode + 1 /\ (ge_balance_positive_omitted_cellmiddlevalue) = 0) /\ (ge_balance_negative_omitted_cellmiddlevalue) = S ge_signed_half_omitted_cellmiddlevaluedecode))) /\ ((dst_positive_omitted_cellmiddle) + ge_balance_negative_omitted_cellmiddlevalue = (dst_negative_omitted_cellmiddle) + ge_balance_positive_omitted_cellmiddlevalue))))))))) /\ (exists dfg_inner_omitted_cellproduct. ((exists sto_ap_omitted_cellproductinner sto_an_omitted_cellproductinner sto_bp_omitted_cellproductinner sto_bn_omitted_cellproductinner sto_cp_omitted_cellproductinner sto_cn_omitted_cellproductinner. (((((dfg_last_omitted_cell) = 2 * (sto_ap_omitted_cellproductinner) /\ (sto_an_omitted_cellproductinner) = 0) \/ exists ge_signed_half_omitted_cellproductinnerleft. (((dfg_last_omitted_cell) = 2 * ge_signed_half_omitted_cellproductinnerleft + 1 /\ (sto_ap_omitted_cellproductinner) = 0) /\ (sto_an_omitted_cellproductinner) = S ge_signed_half_omitted_cellproductinnerleft))) /\ ((((((dfg_value_omitted_cell) = 2 * (sto_bp_omitted_cellproductinner) /\ (sto_bn_omitted_cellproductinner) = 0) \/ exists ge_signed_half_omitted_cellproductinnerright. (((dfg_value_omitted_cell) = 2 * ge_signed_half_omitted_cellproductinnerright + 1 /\ (sto_bp_omitted_cellproductinner) = 0) /\ (sto_bn_omitted_cellproductinner) = S ge_signed_half_omitted_cellproductinnerright))) /\ ((((((dfg_inner_omitted_cellproduct) = 2 * (sto_cp_omitted_cellproductinner) /\ (sto_cn_omitted_cellproductinner) = 0) \/ exists ge_signed_half_omitted_cellproductinneroutput. (((dfg_inner_omitted_cellproduct) = 2 * ge_signed_half_omitted_cellproductinneroutput + 1 /\ (sto_cp_omitted_cellproductinner) = 0) /\ (sto_cn_omitted_cellproductinner) = S ge_signed_half_omitted_cellproductinneroutput))) /\ ((sto_ap_omitted_cellproductinner * sto_bp_omitted_cellproductinner + sto_an_omitted_cellproductinner * sto_bn_omitted_cellproductinner) + sto_cn_omitted_cellproductinner = (sto_ap_omitted_cellproductinner * sto_bn_omitted_cellproductinner + sto_an_omitted_cellproductinner * sto_bp_omitted_cellproductinner) + sto_cp_omitted_cellproductinner))))))) /\ (exists sto_ap_omitted_cellproductouter sto_an_omitted_cellproductouter sto_bp_omitted_cellproductouter sto_bn_omitted_cellproductouter sto_cp_omitted_cellproductouter sto_cn_omitted_cellproductouter. (((((dfg_first_omitted_cell) = 2 * (sto_ap_omitted_cellproductouter) /\ (sto_an_omitted_cellproductouter) = 0) \/ exists ge_signed_half_omitted_cellproductouterleft. (((dfg_first_omitted_cell) = 2 * ge_signed_half_omitted_cellproductouterleft + 1 /\ (sto_ap_omitted_cellproductouter) = 0) /\ (sto_an_omitted_cellproductouter) = S ge_signed_half_omitted_cellproductouterleft))) /\ ((((((dfg_inner_omitted_cellproduct) = 2 * (sto_bp_omitted_cellproductouter) /\ (sto_bn_omitted_cellproductouter) = 0) \/ exists ge_signed_half_omitted_cellproductouterright. (((dfg_inner_omitted_cellproduct) = 2 * ge_signed_half_omitted_cellproductouterright + 1 /\ (sto_bp_omitted_cellproductouter) = 0) /\ (sto_bn_omitted_cellproductouter) = S ge_signed_half_omitted_cellproductouterright))) /\ ((((((z) = 2 * (sto_cp_omitted_cellproductouter) /\ (sto_cn_omitted_cellproductouter) = 0) \/ exists ge_signed_half_omitted_cellproductouteroutput. (((z) = 2 * ge_signed_half_omitted_cellproductouteroutput + 1 /\ (sto_cp_omitted_cellproductouter) = 0) /\ (sto_cn_omitted_cellproductouter) = S ge_signed_half_omitted_cellproductouteroutput))) /\ ((sto_ap_omitted_cellproductouter * sto_bp_omitted_cellproductouter + sto_an_omitted_cellproductouter * sto_bn_omitted_cellproductouter) + sto_cn_omitted_cellproductouter = (sto_ap_omitted_cellproductouter * sto_bn_omitted_cellproductouter + sto_an_omitted_cellproductouter * sto_bp_omitted_cellproductouter) + sto_cp_omitted_cellproductouter))))))))))))))))))))) \/ ((((a)=0 \/ ((e)=0 \/ ~(exists pvs_factor_omitted_cellomittednondivisor. (n) = ((a)*(e)) * pvs_factor_omitted_cellomittednondivisor))) /\ ((z)=0)))) -> z=0

Constructive proof overview

Generated structural guide

Every actually omitted grid cell is zero; a retained factorization cannot coexist with its omitted guard.

The unchanged tactic script uses 0 declared prerequisites and contains 32 exact native proof lines.

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

Proof neighborhood

Direct dependencies

none

Direct dependents

DF0005 dirichlet_grid_entry_functional DF0013 dirichlet_grid_nondivisor_row_value_zero

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

32 script commands · 10 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.

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 hv
02Separate the logical casesL10–19

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

  1. L10
    cases hv
  2. L11
    cases hv_left
  3. L12
    cases hv_left_right
  4. L13
    cases hv_left_right_right
  5. L14
    cases hv_left_right_right_witness
  6. L15
    cases hv_left_right_right_witness_witness
  7. L16
    cases hv_left_right_right_witness_witness_witness
  8. L17
    cases hv_left_right_right_witness_witness_witness_witness
  9. L18
    cases hv_left_right_right_witness_witness_witness_witness_right
  10. L19
    cases hv_left_right_right_witness_witness_witness_witness_right_right
03Separate the logical casesL20–22

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

  1. L20
    cases hv_left_right_right_witness_witness_witness_witness_right_right_right
  2. L21
    exfalso
  3. L22
    cases ho
04Use earlier factsL23–24

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

  1. L23
    apply hv_left_left
  2. L24
    exact ho_left
05Separate the logical casesL25–25

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

  1. L25
    cases ho_right
06Use earlier factsL26–28

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

  1. L26
    apply hv_left_right_left
  2. L27
    exact ho_right_left
  3. L28
    apply ho_right_right
07Construct an explicit witnessL29–29

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

  1. L29
    exists x
08Use earlier factsL30–30

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

  1. L30
    exact hv_left_right_right_witness_witness_witness_witness_left
09Separate the logical casesL31–31

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

  1. L31
    cases hv_right
10Use earlier factsL32–32

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

  1. L32
    exact hv_right_right

Library-wide reading audit

Original exact command ledger · 32 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 hv
  10. 0010cases hv
  11. 0011cases hv_left
  12. 0012cases hv_left_right
  13. 0013cases hv_left_right_right
  14. 0014cases hv_left_right_right_witness
  15. 0015cases hv_left_right_right_witness_witness
  16. 0016cases hv_left_right_right_witness_witness_witness
  17. 0017cases hv_left_right_right_witness_witness_witness_witness
  18. 0018cases hv_left_right_right_witness_witness_witness_witness_right
  19. 0019cases hv_left_right_right_witness_witness_witness_witness_right_right
  20. 0020cases hv_left_right_right_witness_witness_witness_witness_right_right_right
  21. 0021exfalso
  22. 0022cases ho
  23. 0023apply hv_left_left
  24. 0024exact ho_left
  25. 0025cases ho_right
  26. 0026apply hv_left_right_left
  27. 0027exact ho_right_left
  28. 0028apply ho_right_right
  29. 0029exists x
  30. 0030exact hv_left_right_right_witness_witness_witness_witness_left
  31. 0031cases hv_right
  32. 0032exact hv_right_right