def GBUniqueness.h0_multiset (s : Multiset ℤ) (m : ℤ) : ℕ

Sum of h^0 dimensions across a multiset of twist degrees: for a multiset s of integers, returns ∑_{d ∈ s} max(d + m + 1, 0), modeling the dimension of H^0 of ⊕ O(d_i)(m) on P^1.

def GBUniqueness.h0z (s : Multiset ℤ) (m : ℤ) : ℤ

Integer-valued variant of h0_multiset, summing (d + m + 1).toNat viewed as integers.

theorem GBUniqueness.h0z_eq_cast (s : Multiset ℤ) (m : ℤ) : h0z s m = ↑(h0_multiset s m)

The integer version h0z equals the natural-number h0_multiset cast to ℤ.

theorem GBUniqueness.h0z_cons (a : ℤ) (s : Multiset ℤ) (m : ℤ) : h0z (a ::ₘ s) m = ↑(a + m + 1).toNat + h0z s m

Cons-recurrence for h0z: adding a degree a to the multiset adds (a + m + 1).toNat.

theorem GBUniqueness.h0_multiset_cons (a : ℤ) (s : Multiset ℤ) (m : ℤ) : h0_multiset (a ::ₘ s) m = (a + m + 1).toNat + h0_multiset s m

Cons-recurrence for h0_multiset matching h0z_cons.

theorem GBUniqueness.single_second_diff (d' d : ℤ) : ↑(d' - d + 1).toNat - 2 * ↑(d' - d).toNat + ↑(d' - d - 1).toNat = if d' = d then 1 else 0

Pointwise discrete second difference: (d' - d + 1).toNat - 2 (d' - d).toNat + (d' - d - 1).toNat equals 1 iff d' = d, otherwise 0.

theorem GBUniqueness.second_diff_eq_count (s : Multiset ℤ) (d : ℤ) : h0z s (-d) - 2 * h0z s (-d - 1) + h0z s (-d - 2) = ↑(Multiset.count d s)

Key recovery lemma: the discrete second difference of h0z s at -d equals the multiplicity of d in s. This lets us reconstruct a multiset of splitting degrees from its h^0 data.

theorem GBUniqueness.h0z_determines_multiset (s t : Multiset ℤ) (h : ∀ (m : ℤ), h0z s m = h0z t m) : s = t

Uniqueness: two multisets of integers with identical h0z data are equal.

theorem GBUniqueness.h0_multiset_determines_multiset (s t : Multiset ℤ) (h : ∀ (m : ℤ), h0_multiset s m = h0_multiset t m) : s = t

Natural-number version: two multisets with identical h0_multiset data are equal.

def GBUniqueness.degreesToMultiset {n : ℕ} (degrees : Fin n → ℤ) : Multiset ℤ

Turn a tuple of degrees degrees : Fin n → ℤ into the corresponding multiset of values.

theorem GBUniqueness.h0_twisted_eq_h0_multiset {n : ℕ} (s : GBExistence.SplittingType n) (t : ℤ) : s.h0_twisted t = h0_multiset (degreesToMultiset s.degrees) t

Bridge between the splitting-type h0_twisted formula and the multiset-level h0_multiset.

theorem GBUniqueness.splitting_uniqueness_multiset {n : ℕ} (s₁ s₂ : GBExistence.SplittingType n) (h : ∀ (t : ℤ), s₁.h0_twisted t = s₂.h0_twisted t) : degreesToMultiset s₁.degrees = degreesToMultiset s₂.degrees

Grothendieck-Birkhoff uniqueness at the multiset level: two splitting types that yield the same twisted h^0 data must define the same multiset of summand degrees.

theorem GBUniqueness.sorted_eq_of_multiset_eq {n : ℕ} (f g : Fin n → ℤ) (hf : ∀ (i j : Fin n), i ≤ j → g j ≤ g i) (hg : ∀ (i j : Fin n), i ≤ j → f j ≤ f i) (hmulti : degreesToMultiset f = degreesToMultiset g) : f = g

Two decreasing tuples Fin n → ℤ that determine the same multiset are equal pointwise.

theorem GBUniqueness.splitting_uniqueness_sorted {n : ℕ} (s₁ s₂ : GBExistence.SplittingType n) (h : ∀ (t : ℤ), s₁.h0_twisted t = s₂.h0_twisted t) : s₁.degrees = s₂.degrees

Grothendieck-Birkhoff uniqueness in sorted form (Thm 24.1): the decreasing splitting tuple is uniquely determined by the twisted h^0 data.

theorem GBUniqueness.h0_directsum_formula {n : ℕ} (degrees : Fin n → ℤ) (m : ℤ) : ∑ i : Fin n, GBExistence.h0_dim (degrees i + m) = h0_multiset (degreesToMultiset degrees) m

H^0 direct-sum formula: summing h^0 of summands O(d_i)(m) agrees with the multiset formula h0_multiset applied to the multiset of degrees.

def GBUniqueness.h1_multiset (s : Multiset ℤ) (m : ℤ) : ℕ

Multiset-level h^1 formula: for splitting degrees d_i, the dimension of H^1 of ⊕ O(d_i)(m) on P^1 is ∑ max(-d_i - m - 1, 0).

theorem GBUniqueness.h1_directsum_formula {n : ℕ} (degrees : Fin n → ℤ) (m : ℤ) : ∑ i : Fin n, GBExistence.h1_dim (degrees i + m) = h1_multiset (degreesToMultiset degrees) m

H^1 direct-sum formula matching h0_directsum_formula.

theorem GBUniqueness.second_diff_eq_count_nat (s : Multiset ℤ) (d : ℤ) : h0_multiset s (-d) + h0_multiset s (-d - 2) - 2 * h0_multiset s (-d - 1) = Multiset.count d s

Natural-number version of second_diff_eq_count: the discrete second difference of h0_multiset at -d returns the multiplicity of d.