DL0072

integer_vector_equal_zero_from_same_components

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

Alpha v34 checked-use · first admitted v27 · 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. Exact original first-admission records.

This branch proves the finite determinant/rank/span substrate. It does not claim Smith or Hermite normal form, lattice index equals determinant, determinant multiplicativity, lattice reduction, or geometry-of-numbers theorems.

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ pb. ∀ pc. ∀ nb. ∀ nc. ∀ l. IntegerVectorZero(pb,pc,nb,nc,l) → IntegerVectorEqual(b,c,b,c,pb,pc,nb,nc,l)

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

Definition DAG

IntegerVectorEqual(ab,ac,db,dc,eb,ec,fb,fc,l) · 1IntegerVectorZero(ab,ac,db,dc,l) · 1

Actual proof prerequisites

beta_at_unique · checked external prerequisiteadd_comm · checked external prerequisite
Original expanded first-order 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)

Complete tactic proof in conservative notation

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

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.

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 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 defined 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