Explicit cutoff-independent coefficient and inverse constants in the nonlinear correction estimate.

theorem EulerGevreyUniformConstants.coefficientBlock_zero_le (period : ℝ) {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A) (L : ℝ) (hL : ∀ r ≤ 6, EulerJetProductBounds.boundLevel period K r ≤ L) : EulerH6Pressure.coefficientBlock period K 6 0 ≤ 448 * L

The fixed H⁶ coefficient block is bounded by 448 times the base coefficient bound.

theorem EulerGevreyUniformConstants.weightedCoefficient_le (period : ℝ) {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A) (N : ℕ) (ρ Rc : ℝ) (hρ : 0 < ρ) (hRc : 0 ≤ Rc) (hsmall : ρ * Rc ≤ 1 / 2) (hcoeff : ∀ (l : ℕ), 1 ≤ l → l ≤ N → EulerH6Pressure.coefficientBlock period K 6 l ≤ Rc ^ l * ↑l.factorial ^ 2) : EulerSobolevGevreyOperators.weightedCoefficient period K 6 N ρ ≤ EulerH6Pressure.coefficientBlock period K 6 0 + 2 * (ρ * Rc)

The finite weighted coefficient sum is bounded by its base block and a geometric tail.

theorem EulerGevreyUniformConstants.weightedCoefficient_uniform (period : ℝ) {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A) (N : ℕ) (ρ Rc L : ℝ) (hρ : 0 < ρ) (hRc : 0 ≤ Rc) (hsmall : ρ * Rc ≤ 1 / 2) (hL : ∀ r ≤ 6, EulerJetProductBounds.boundLevel period K r ≤ L) (hcoeff : ∀ (l : ℕ), 1 ≤ l → l ≤ N → EulerH6Pressure.coefficientBlock period K 6 l ≤ Rc ^ l * ↑l.factorial ^ 2) : EulerSobolevGevreyOperators.weightedCoefficient period K 6 N ρ ≤ 448 * L + 1

Under the fixed geometric smallness condition the coefficient multiplier bound is independent of N.

theorem EulerGevreyUniformConstants.baseCoefficientSum_le (period : ℝ) {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection 6 A) (L : ℝ) (hL : ∀ r ≤ 6, EulerJetProductBounds.boundLevel period K r ≤ L) : EulerBasePressureCommutator.baseCoefficientSum period K ≤ 6 * L

Summed positive base coefficient derivatives contribute at most 6L.

theorem EulerGevreyUniformConstants.pressureConstant_le_six (period : ℝ) {q : ℕ} (hq : q ≤ 6) {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q A) (c L : ℝ) (hc : 0 < c) (hL : 1 ≤ L) (hcL : c⁻¹ ≤ L) (hcoeff : ∀ r ≤ q, EulerJetProductBounds.boundLevel period K r ≤ L) : K.pressureConstant c ≤ (9 * L) ^ 729

One explicit polynomial bounds every coercive inverse at base order at most six.

theorem EulerGevreyUniformConstants.fixed_pressure_constants (period : ℝ) {s : ℕ} (hs : 6 ≤ s) {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A) (c L : ℝ) (hc : 0 < c) (hL : 1 ≤ L) (hcL : c⁻¹ ≤ L) (hcoeff : ∀ r ≤ 6, EulerJetProductBounds.boundLevel period K r ≤ L) : (EulerH6Pressure.CoefficientJet.restrict K 5 ⋯).pressureConstant c ≤ (9 * L) ^ 729 ∧ (EulerH6Pressure.CoefficientJet.restrict K 6 hs).pressureConstant c ≤ (9 * L) ^ 729

Both fixed inverse orders needed by the actual pressure forcing have the same cutoff-independent polynomial bound.