Lift singular local generators from the reduction modulo p. The remaining error is an explicit multiple of p, with a separate high-order term.

theorem CCDN.exists_integer_hypersurface_generators {p n : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin (n + 1)) ℤ) : ∃ (r : ℕ → ℕ) (g : (k : ℕ) → Fin (r k) → MvPolynomial (Fin (n + 1)) ℤ), (∀ (k : ℕ), r k = Module.finrank (ZMod p) ↥(originLayer ((MvPolynomial.map (Int.castRingHom (ZMod p))) f) k)) ∧ (∀ (k : ℕ) (j : Fin (r k)), (g k j).IsHomogeneous k) ∧ ∀ (N : ℕ) (u : MvPolynomial (Fin (n + 1)) ℤ), ∃ (c : (k : Fin N) → Fin (r ↑k) → ℤ) (h : MvPolynomial (Fin (n + 1)) ℤ) (v : MvPolynomial (Fin (n + 1)) ℤ) (w : MvPolynomial (Fin (n + 1)) ℤ), v ∈ MvPolynomial.idealOfVars (Fin (n + 1)) ℤ ^ N ∧ u - ∑ k : Fin N, ∑ j : Fin (r ↑k), c k j • g (↑k) j = f * h + v + MvPolynomial.C ↑p * w

Integer generators in arbitrary dimension, with the residue-layer Hilbert function as their weight profile.

theorem CCDN.exists_integer_origin_generators {p μ : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin 2) ℤ) (hf : (MvPolynomial.map (Int.castRingHom (ZMod p))) f ∈ MvPolynomial.idealOfVars (Fin 2) (ZMod p) ^ μ) (hμ : (MvPolynomial.homogeneousComponent μ) ((MvPolynomial.map (Int.castRingHom (ZMod p))) f) ≠ 0) : ∃ (r : ℕ → ℕ) (g : (k : ℕ) → Fin (r k) → MvPolynomial (Fin 2) ℤ), (∀ (k : ℕ), r k ≤ μ) ∧ (∀ (k : ℕ) (j : Fin (r k)), (g k j).IsHomogeneous k) ∧ ∀ (N : ℕ) (u : MvPolynomial (Fin 2) ℤ), ∃ (c : (k : Fin N) → Fin (r ↑k) → ℤ) (h : MvPolynomial (Fin 2) ℤ) (v : MvPolynomial (Fin 2) ℤ) (w : MvPolynomial (Fin 2) ℤ), v ∈ MvPolynomial.idealOfVars (Fin 2) ℤ ^ N ∧ u - ∑ k : Fin N, ∑ j : Fin (r ↑k), c k j • g (↑k) j = f * h + v + MvPolynomial.C ↑p * w

The local generators are homogeneous integer polynomials. Their uniform reduction formula separates the defining equation, the origin-adic error, and the p-divisible error.