A rank-two numerical lattice model

A deliberately concrete stand-in for K_num(Ku(X)) ≅ ℤ².

This is not the Kuznetsov component's numerical Grothendieck group. It is the rank-2 torsion-free lattice that group is isomorphic to, and every lemma here is a statement about that lattice alone. The identification itself is geometry, lives upstream of anything Mathlib can express today, and is tracked as an assumption-frontier obligation — never discharged here.

Keeping the two apart is the whole point: a proof over Fin 2 → ℤ is a theorem about any rank-2 torsion-free lattice, not yet a theorem about a surface.

@[reducible, inline]

abbrev IntegralLattice.NumLattice : Type

The rank-2 numerical lattice model.

Equations

• IntegralLattice.NumLattice = (Fin 2 → ℤ)

theorem IntegralLattice.finrank_numLattice : Module.finrank ℤ NumLattice = 2

theorem IntegralLattice.ne_zero_of_apply_ne_zero {v : NumLattice} {i : Fin 2} (h : v i ≠ 0) : v ≠ 0

Rank-component non-vanishing: a lattice vector with any nonzero component is nonzero. The §8 "rank component does not vanish" step.

theorem IntegralLattice.eq_zero_of_two_zsmul_eq_zero_num {v : NumLattice} (h : 2 • v = 0) : v = 0

The doubling step, specialised to the rank-2 model.