Translation and residue-block assembly for the singular local plane-curve determinant theorem.

theorem CCDN.singular_plane_chart_det_divisibility_mod {p μ s : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin 2) ℤ) (F : Fin s → MvPolynomial (Fin 2) ℤ) (x : Fin s → Fin 2 → ℤ) (a : Fin 2 → ℤ) (hf : (MvPolynomial.map (Int.castRingHom (ZMod p))) ((originShift a) f) ∈ MvPolynomial.idealOfVars (Fin 2) (ZMod p) ^ μ) (hμ : (MvPolynomial.homogeneousComponent μ) ((MvPolynomial.map (Int.castRingHom (ZMod p))) ((originShift a) f)) ≠ 0) (hx : ∀ (i : Fin s) (j : Fin 2), ↑p ∣ x i j - a j) (hfx : ∀ (i : Fin s), ↑p ^ multiplicityExponent s μ ∣ (MvPolynomial.eval (x i)) f) : ↑p ^ multiplicityExponent s μ ∣ (Matrix.of fun (i j : Fin s) => (MvPolynomial.eval (x i)) (F j)).det

Singular local divisibility at an arbitrary integral representative of a residue point; multiplicity is measured on the translated reduction.

theorem CCDN.singular_plane_residue_minorGcd {p c s N : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin 2) ℤ) (F : Fin N → MvPolynomial (Fin 2) ℤ) (x : Fin s → Fin 2 → ℤ) (label : Fin s → Fin c) (a : Fin c → Fin 2 → ℤ) (μ : Fin c → ℕ) (hf : ∀ (i : Fin c), (MvPolynomial.map (Int.castRingHom (ZMod p))) ((originShift (a i)) f) ∈ MvPolynomial.idealOfVars (Fin 2) (ZMod p) ^ μ i) (hμ : ∀ (i : Fin c), (MvPolynomial.homogeneousComponent (μ i)) ((MvPolynomial.map (Int.castRingHom (ZMod p))) ((originShift (a i)) f)) ≠ 0) (hx : ∀ (i : Fin s) (j : Fin 2), ↑p ∣ x i j - a (label i) j) (hfx : ∀ (i : Fin s), (MvPolynomial.eval (x i)) f = 0) : ↑p ^ ∑ i : Fin c, multiplicityExponent (Fintype.card { k : Fin s // label k = i }) (μ i) ∣ Int.Matrix.minorGcd (Matrix.of fun (i : Fin s) (j : Fin N) => (MvPolynomial.eval (x i)) (F j))

Summed multiplicity exponents for arbitrary residue blocks, including singular blocks. Each local hypothesis describes the reduced equation.