Coordinate invariance of geometric bad reduction and coefficient height, with the exact bad-prime charge in standard Fin-indexed coordinates.

theorem CCDN.hypersurfaceBadReduction_renameEquiv {σ : Type u_1} {τ : Type u_2} (e : σ ≃ τ) (f : MvPolynomial σ ℤ) (p : ℕ) : HypersurfaceBadReduction ((MvPolynomial.rename ⇑e) f) p ↔ HypersurfaceBadReduction f p

Geometric bad reduction at p is invariant under a bijective renaming of the variables.

theorem CCDN.polynomial_coefficient_bound_renameEquiv {σ : Type u_1} {τ : Type u_2} (e : σ ≃ τ) (f : MvPolynomial σ ℤ) (H : ℝ) (hf : CoefficientHeightLE f H) : CoefficientHeightLE ((MvPolynomial.rename ⇑e) f) H

A bound H on the coefficients of f also bounds the coefficients of f after a bijective renaming of the variables.

theorem CCDN.exists_fin_hypersurface_bad_prime_charge {L : Type u_1} [Field L] [CharZero L] [IsAlgClosed L] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) ℤ) (hf : Irreducible ((MvPolynomial.map (Int.castRingHom L)) f)) (hpos : 0 < f.totalDegree) (H : ℝ) (hH : 1 ≤ H) (hcoeff : CoefficientHeightLE f H) : ∃ (bad : Finset ℕ), (∀ (p : ℕ), p ∈ bad ↔ stepanovThreshold f.totalDegree < p ∧ HypersurfaceBadReduction f p) ∧ ∑ p ∈ bad, Real.log ↑p / ↑p ≤ Real.log (hypersurfaceHeightConstant (n + 1) * (1 + Real.log H / ↑f.totalDegree ^ 2)) + 2 * mertensError + 1

The exact geometric bad-prime set exists, and its charge is bounded.

theorem CCDN.finite_fin_hypersurface_bad_primes {L : Type u_1} [Field L] [CharZero L] [IsAlgClosed L] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) ℤ) (hf : Irreducible ((MvPolynomial.map (Int.castRingHom L)) f)) (hpos : 0 < f.totalDegree) : {p : ℕ | stepanovThreshold f.totalDegree < p ∧ HypersurfaceBadReduction f p}.Finite

Finiteness is invariant under the standard Fin-to-Option reindexing.

theorem CCDN.homogeneous_hypersurfaceBadReduction_iff {σ : Type u_1} {d : ℕ} (f : MvPolynomial σ ℤ) (hf : f.IsHomogeneous d) (hf0 : f ≠ 0) (p : ℕ) [Fact (Nat.Prime p)] : HypersurfaceBadReduction f p ↔ ¬Irreducible ((MvPolynomial.map (Int.castRingHom (AlgebraicClosure (ZMod p)))) f)

For a nonzero homogeneous equation, degree loss is already included in failure of geometric irreducibility, so the predicate agrees with the paper.

theorem CCDN.hypersurface_good_reduction {σ : Type u_1} (f : MvPolynomial σ ℤ) (p : ℕ) [Fact (Nat.Prime p)] (hgood : ¬HypersurfaceBadReduction f p) : HasGoodReduction f p

Outside the bad-prime predicate, both full degree and geometric irreducibility hold for the coefficient reduction.

theorem CCDN.exists_hypersurface_bad_prime_finset {L : Type u_1} [Field L] [CharZero L] [IsAlgClosed L] {n d : ℕ} (f : MvPolynomial (Fin (n + 1)) ℤ) (hf : f.IsHomogeneous d) (hd : 0 < d) (hir : Irreducible ((MvPolynomial.map (Int.castRingHom L)) f)) : ∃ (bad : Finset ℕ), ∀ (p : ℕ), p ∈ bad ↔ stepanovThreshold d < p ∧ HypersurfaceBadReduction f p

The finite set of primes p > 27 d ^ 4 of bad reduction of an absolutely irreducible form of degree d > 0.

theorem CCDN.hasGoodReduction_of_not_mem {σ : Type u_1} {f : MvPolynomial σ ℤ} {d : ℕ} {bad : Finset ℕ} (hbad : ∀ (p : ℕ), p ∈ bad ↔ stepanovThreshold d < p ∧ HypersurfaceBadReduction f p) (p : ℕ) [Fact (Nat.Prime p)] (hp : p ∉ bad) (hcut : stepanovThreshold ↑d < ↑p) : HasGoodReduction f p

A prime above the cutoff outside the bad-prime set has good reduction.