Sharp leading term for the hypersurface local determinant exponent. The linear error depends on dimension alone, not on singular multiplicity.

theorem CCDN.local_exponent_separated_lower_bound (m s e : ℕ) (hm : 0 < m) {μ : ℕ} (hμ : 0 < μ) (hcutoff : ∀ (K : ℕ), s * K ≤ e + μ * (m + K).choose (m + 1)) : (↑m.factorial / ↑μ) ^ (1 / ↑m) * ↑m / (↑m + 1) * ↑s ^ (1 + 1 / ↑m) - (↑m + 1) * ↑s ≤ ↑e

Under the binomial cutoff hypothesis, (m!/μ)^(1/m) · m/(m+1) · s^(1+1/m) − (m+1)s ≤ e: the local exponent bound in the paper's separated-power notation. The error constant m+1 is uniform in both the equation and its multiplicity.

theorem CCDN.hypersurfaceMultiplicityExponent_cutoff_pos (m s K : ℕ) (hm : 0 < m) {μ : ℕ} (hμ : 0 < μ) : s * K ≤ hypersurfaceMultiplicityExponent m μ s + μ * (m + K).choose (m + 1)

The local hypersurface profile satisfies the cutoff hypothesis in every positive dimension.

theorem CCDN.hypersurfaceMultiplicityExponent_lower_bound (m s : ℕ) (hm : 0 < m) {μ : ℕ} (hμ : 0 < μ) : (↑m.factorial / ↑μ) ^ (1 / ↑m) * ↑m / (↑m + 1) * ↑s ^ (1 + 1 / ↑m) - (↑m + 1) * ↑s ≤ ↑(hypersurfaceMultiplicityExponent m μ s)

The sharp local estimate in the paper's separated-power notation.