DL0072

integer_vector_equal_zero_from_same_components

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

An equal-component product represents every actual zero vector, including all noncanonical zero pair encodings.

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 original first-admission records.

Exact expanded first-order arithmetic statement

forall b c pb pc nb nc l. (forall ics_index_zero_target ics_value0_zero_target ics_value1_zero_target. (exists ics_gap_zero_target_bound. ics_gap_zero_target_bound + S (ics_index_zero_target) = (l)) -> (((exists fs_h_ics_zero_target_at0. fs_h_ics_zero_target_at0 + S (ics_value0_zero_target) = S ((S (ics_index_zero_target)) * pc)) /\ exists fs_q_ics_zero_target_at0. pb = fs_q_ics_zero_target_at0 * S ((S (ics_index_zero_target)) * pc) + (ics_value0_zero_target))) -> (((exists fs_h_ics_zero_target_at1. fs_h_ics_zero_target_at1 + S (ics_value1_zero_target) = S ((S (ics_index_zero_target)) * nc)) /\ exists fs_q_ics_zero_target_at1. nb = fs_q_ics_zero_target_at1 * S ((S (ics_index_zero_target)) * nc) + (ics_value1_zero_target))) -> ics_value0_zero_target = ics_value1_zero_target) -> (forall ics_index_zero_same_target ics_value0_zero_same_target ics_value1_zero_same_target ics_value2_zero_same_target ics_value3_zero_same_target. (exists ics_gap_zero_same_target_bound. ics_gap_zero_same_target_bound + S (ics_index_zero_same_target) = (l)) -> (((exists fs_h_ics_zero_same_target_at0. fs_h_ics_zero_same_target_at0 + S (ics_value0_zero_same_target) = S ((S (ics_index_zero_same_target)) * c)) /\ exists fs_q_ics_zero_same_target_at0. b = fs_q_ics_zero_same_target_at0 * S ((S (ics_index_zero_same_target)) * c) + (ics_value0_zero_same_target))) -> (((exists fs_h_ics_zero_same_target_at1. fs_h_ics_zero_same_target_at1 + S (ics_value1_zero_same_target) = S ((S (ics_index_zero_same_target)) * c)) /\ exists fs_q_ics_zero_same_target_at1. b = fs_q_ics_zero_same_target_at1 * S ((S (ics_index_zero_same_target)) * c) + (ics_value1_zero_same_target))) -> (((exists fs_h_ics_zero_same_target_at2. fs_h_ics_zero_same_target_at2 + S (ics_value2_zero_same_target) = S ((S (ics_index_zero_same_target)) * pc)) /\ exists fs_q_ics_zero_same_target_at2. pb = fs_q_ics_zero_same_target_at2 * S ((S (ics_index_zero_same_target)) * pc) + (ics_value2_zero_same_target))) -> (((exists fs_h_ics_zero_same_target_at3. fs_h_ics_zero_same_target_at3 + S (ics_value3_zero_same_target) = S ((S (ics_index_zero_same_target)) * nc)) /\ exists fs_q_ics_zero_same_target_at3. nb = fs_q_ics_zero_same_target_at3 * S ((S (ics_index_zero_same_target)) * nc) + (ics_value3_zero_same_target))) -> ics_value0_zero_same_target + ics_value3_zero_same_target = ics_value2_zero_same_target + ics_value1_zero_same_target)

Constructive proof overview

Generated structural guide

An equal-component product represents every actual zero vector, including all noncanonical zero pair encodings.

The unchanged tactic script uses 2 declared prerequisites and contains 38 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_at_unique Stable theorem; checked-use authorized add_comm Stable theorem; checked-use authorized

Direct dependents

DL0079 integer_matrix_vector_product_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

38 script commands · 5 reading checkpoints · 2 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–10

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro pb
  4. L4
    intro pc
  5. L5
    intro nb
  6. L6
    intro nc
  7. L7
    intro l
  8. L8
    intro hzero
  9. L9
    intro i
  10. L10
    intro u
02Fix variables and assumptionsL11–18

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

  1. L11
    intro v
  2. L12
    intro p
  3. L13
    intro n
  4. L14
    intro hi
  5. L15
    intro hu
  6. L16
    intro hv
  7. L17
    intro hp
  8. L18
    intro hn
03Establish hsameL19–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L19
    have hsame : u = v
  2. L20
    specialize beta_at_unique (b)
  3. L21
    specialize beta_at_unique (c)
  4. L22
    specialize beta_at_unique (i)
  5. L23
    specialize beta_at_unique (u)
  6. L24
    specialize beta_at_unique (v)
  7. L25
    apply beta_at_unique
  8. L26
    exact hu
  9. L27
    exact hv
04Establish hzL28–37

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hzero.

  1. L28
    have hz : p = n
  2. L29
    specialize hzero (i)
  3. L30
    specialize hzero (p)
  4. L31
    specialize hzero (n)
  5. L32
    apply hzero
  6. L33
    exact hi
  7. L34
    exact hp
  8. L35
    exact hn
  9. L36
    rewrite hsame
  10. L37
    rewrite hz
05Use earlier factsL38–38

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

  1. L38
    apply add_comm

Library-wide reading audit

Original exact command ledger · 38 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro pb
  4. 0004intro pc
  5. 0005intro nb
  6. 0006intro nc
  7. 0007intro l
  8. 0008intro hzero
  9. 0009intro i
  10. 0010intro u
  11. 0011intro v
  12. 0012intro p
  13. 0013intro n
  14. 0014intro hi
  15. 0015intro hu
  16. 0016intro hv
  17. 0017intro hp
  18. 0018intro hn
  19. 0019have hsame : u = v
  20. 0020specialize beta_at_unique (b)
  21. 0021specialize beta_at_unique (c)
  22. 0022specialize beta_at_unique (i)
  23. 0023specialize beta_at_unique (u)
  24. 0024specialize beta_at_unique (v)
  25. 0025apply beta_at_unique
  26. 0026exact hu
  27. 0027exact hv
  28. 0028have hz : p = n
  29. 0029specialize hzero (i)
  30. 0030specialize hzero (p)
  31. 0031specialize hzero (n)
  32. 0032apply hzero
  33. 0033exact hi
  34. 0034exact hp
  35. 0035exact hn
  36. 0036rewrite hsame
  37. 0037rewrite hz
  38. 0038apply add_comm