Arithmetic of the residual-order ledger

The candidate manuscript, Proposition 10.3, assigns real exponents to analytic estimates. This file checks the arithmetic of those assignments, conditional on the estimates being valid. It does not define the analytic classes, construct a correction, or prove an estimate for a PDE.

The manuscript fixes κ = 10⁻⁵ in §8.1 and again in §10.2. The results below hold uniformly for 0 ≤ κ ≤ 10⁻⁵ and σ ≥ 1/5. Fractions are exact rationals in the real numbers; no floating-point calculation is used.

noncomputable def NavierStokes.ExponentLedger.waveExponent (σ : ℝ) : ℝ

The good-wave residual exponent B = 1/2 + σ.

Equations

• NavierStokes.ExponentLedger.waveExponent σ = 1 / 2 + σ

def NavierStokes.ExponentLedger.meanExponent (σ : ℝ) : ℝ

The mean and defect target exponent C = 1 + σ.

Equations

• NavierStokes.ExponentLedger.meanExponent σ = 1 + σ

def NavierStokes.ExponentLedger.meanUpdateExponent (σ κ : ℝ) : ℝ

The intermediate exponent H₁ = C - 2κ.

Equations

• NavierStokes.ExponentLedger.meanUpdateExponent σ κ = NavierStokes.ExponentLedger.meanExponent σ - 2 * κ

noncomputable def NavierStokes.ExponentLedger.particularGain (σ κ : ℝ) : ℝ

Minimum of the four listed gains for the particular wave correction.

Equations

• NavierStokes.ExponentLedger.particularGain σ κ = min (min (min (1 / 2 - 3 * κ) (1 / 2 - κ)) (NavierStokes.ExponentLedger.waveExponent σ - κ)) (2 / 5)

noncomputable def NavierStokes.ExponentLedger.signedGain (σ κ : ℝ) : ℝ

Minimum of the four listed gains for the signed wave correction.

Equations

• NavierStokes.ExponentLedger.signedGain σ κ = min (min (min (1 / 2 - 4 * κ) (2 / 5 - κ)) (1 / 2 - 2 * κ)) (NavierStokes.ExponentLedger.waveExponent σ - 3 * κ)

noncomputable def NavierStokes.ExponentLedger.signedBarGain (σ κ : ℝ) : ℝ

The five distinct gains listed for the signed bar residual, after divergence. The subtracted bump repeats the fourth bound and so contributes no new minimum.

Equations

• NavierStokes.ExponentLedger.signedBarGain σ κ = min (min (min (min (9 / 50 - 2 * κ) (1 / 2 - 3 * κ)) (σ - 3 * κ)) (1 - κ)) (1 - 2 * κ)

theorem NavierStokes.ExponentLedger.mean_eq_wave_add_half (σ : ℝ) : meanExponent σ = waveExponent σ + 1 / 2

theorem NavierStokes.ExponentLedger.wave_at_least_seven_tenths {σ : ℝ} (hσ : 1 / 5 ≤ σ) : 7 / 10 ≤ waveExponent σ

theorem NavierStokes.ExponentLedger.mean_at_least_six_fifths {σ : ℝ} (hσ : 1 / 5 ≤ σ) : 6 / 5 ≤ meanExponent σ

theorem NavierStokes.ExponentLedger.wave_increment (σ : ℝ) : waveExponent (σ + 1 / 10) = waveExponent σ + 1 / 10

theorem NavierStokes.ExponentLedger.mean_increment (σ : ℝ) : meanExponent (σ + 1 / 10) = meanExponent σ + 1 / 10

theorem NavierStokes.ExponentLedger.parameter_lower_bound_preserved {σ : ℝ} (hσ : 1 / 5 ≤ σ) : 1 / 5 ≤ σ + 1 / 10

Step 1: particular correction

theorem NavierStokes.ExponentLedger.particular_gain_eq {σ κ : ℝ} (hσ : 1 / 5 ≤ σ) (hκ : κ ≤ 1 / 100000) : particularGain σ κ = 2 / 5

The displayed lower bound is in fact equality for the stated parameter range.

theorem NavierStokes.ExponentLedger.particular_linear_margin {σ κ : ℝ} (hκ : κ ≤ 1 / 100000) : waveExponent σ + 2 / 5 ≤ waveExponent σ + 1 / 2 - 3 * κ

theorem NavierStokes.ExponentLedger.particular_old_wave_margin {σ κ : ℝ} (hκ : κ ≤ 1 / 100000) : waveExponent σ + 2 / 5 ≤ waveExponent σ + 1 / 2 - κ

theorem NavierStokes.ExponentLedger.particular_square_margin {σ κ : ℝ} (hσ : 1 / 5 ≤ σ) (hκ : κ ≤ 1 / 100000) : waveExponent σ + 2 / 5 ≤ 2 * waveExponent σ - κ

theorem NavierStokes.ExponentLedger.particular_gain_exceeds_tenth {σ κ : ℝ} (hσ : 1 / 5 ≤ σ) (hκ : κ ≤ 1 / 100000) : waveExponent (σ + 1 / 10) < waveExponent σ + particularGain σ κ

theorem NavierStokes.ExponentLedger.particular_tensor_exponent (σ : ℝ) : waveExponent σ + 1 / 2 = meanExponent σ

Step 2: signed correction

theorem NavierStokes.ExponentLedger.signed_gain_eq {σ κ : ℝ} (hσ : 1 / 5 ≤ σ) (hκ : κ ≤ 1 / 100000) : signedGain σ κ = 2 / 5 - κ

theorem NavierStokes.ExponentLedger.signed_gain_exceeds_tenth {σ κ : ℝ} (hσ : 1 / 5 ≤ σ) (hκ : κ ≤ 1 / 100000) : waveExponent (σ + 1 / 10) < waveExponent σ + signedGain σ κ

theorem NavierStokes.ExponentLedger.signed_old_difference_identity (σ κ : ℝ) : waveExponent σ + 17 / 25 - κ = meanExponent σ + 9 / 50 - κ

theorem NavierStokes.ExponentLedger.signed_square_identity (σ κ : ℝ) : 2 * waveExponent σ - 2 * κ = meanExponent σ + σ - 2 * κ

theorem NavierStokes.ExponentLedger.signed_old_difference_after_divergence (σ κ : ℝ) : waveExponent σ + 17 / 25 - κ - κ = meanExponent σ + (9 / 50 - 2 * κ)

theorem NavierStokes.ExponentLedger.signed_curl_after_divergence (σ κ : ℝ) : meanExponent σ + 1 / 2 - 2 * κ - κ = meanExponent σ + (1 / 2 - 3 * κ)

theorem NavierStokes.ExponentLedger.signed_square_after_divergence (σ κ : ℝ) : 2 * waveExponent σ - 2 * κ - κ = meanExponent σ + (σ - 3 * κ)

theorem NavierStokes.ExponentLedger.old_difference_bar_margin {κ : ℝ} (hκ : κ ≤ 1 / 100000) : 17 / 100 < 9 / 50 - 2 * κ

theorem NavierStokes.ExponentLedger.curl_bar_margin {κ : ℝ} (hκ : κ ≤ 1 / 100000) : 17 / 100 < 1 / 2 - 3 * κ

theorem NavierStokes.ExponentLedger.square_bar_margin {σ κ : ℝ} (hσ : 1 / 5 ≤ σ) (hκ : κ ≤ 1 / 100000) : 17 / 100 < σ - 3 * κ

theorem NavierStokes.ExponentLedger.axial_bar_margin {κ : ℝ} (hκ : κ ≤ 1 / 100000) : 17 / 100 < 1 - κ

theorem NavierStokes.ExponentLedger.pressure_bar_margin {κ : ℝ} (hκ : κ ≤ 1 / 100000) : 17 / 100 < 1 - 2 * κ

theorem NavierStokes.ExponentLedger.signed_bar_gain_exceeds_seventeen_hundredths {σ κ : ℝ} (hσ : 1 / 5 ≤ σ) (hκ : κ ≤ 1 / 100000) : 17 / 100 < signedBarGain σ κ

Every listed contribution exceeds the claimed .17 bar-residual gain.

Steps 3 and 4: mean and defect updates

theorem NavierStokes.ExponentLedger.mean_update_wave_identity (σ κ : ℝ) : meanUpdateExponent σ κ = waveExponent σ + 1 / 2 - 2 * κ

theorem NavierStokes.ExponentLedger.mean_update_wave_margin {σ κ : ℝ} (hκ : κ ≤ 1 / 100000) : waveExponent (σ + 1 / 10) < meanUpdateExponent σ κ

theorem NavierStokes.ExponentLedger.temporal_mean_gain_identity (σ κ : ℝ) : meanUpdateExponent σ κ + 1 - 2 * κ = meanExponent σ + (1 - 4 * κ)

theorem NavierStokes.ExponentLedger.completed_mean_gain_eq {κ : ℝ} (hκ : κ ≤ 1 / 100000) : min (17 / 100) (1 - 4 * κ) = 17 / 100

theorem NavierStokes.ExponentLedger.completed_mean_margin {σ κ : ℝ} (hκ : κ ≤ 1 / 100000) : meanExponent (σ + 1 / 10) < meanExponent σ + min (17 / 100) (1 - 4 * κ)

theorem NavierStokes.ExponentLedger.rank_defect_gain_identity (σ κ : ℝ) : meanUpdateExponent σ κ + 9 / 10 - 2 * κ = meanExponent σ + 9 / 10 - 4 * κ

theorem NavierStokes.ExponentLedger.completed_defect_margin {σ κ : ℝ} (hκ : κ ≤ 1 / 100000) : meanExponent (σ + 1 / 10) < meanExponent σ + 9 / 10 - 4 * κ

Cumulative exponent bounds

theorem NavierStokes.ExponentLedger.signed_increment_lower_bound {σ κ : ℝ} (hσ : 1 / 5 ≤ σ) (hκ : κ ≤ 1 / 100000) : 69999 / 100000 ≤ waveExponent σ - κ

theorem NavierStokes.ExponentLedger.signed_increment_above_cumulative_difference {σ κ : ℝ} (hσ : 1 / 5 ≤ σ) (hκ : κ ≤ 1 / 100000) : 17 / 25 < waveExponent σ - κ

theorem NavierStokes.ExponentLedger.particular_increment_above_cumulative_difference {σ : ℝ} (hσ : 1 / 5 ≤ σ) : 17 / 25 < waveExponent σ

theorem NavierStokes.ExponentLedger.mean_increment_above_cumulative_mean {σ κ : ℝ} (hσ : 1 / 5 ≤ σ) (hκ : κ ≤ 1 / 100000) : 9 / 10 < meanUpdateExponent σ κ

theorem NavierStokes.ExponentLedger.radial_increment_above_cumulative_radial {σ κ : ℝ} (hσ : 1 / 5 ≤ σ) (hκ : κ ≤ 1 / 100000) : 19 / 10 < meanUpdateExponent σ κ + 1

theorem NavierStokes.ExponentLedger.particular_pressure_above_cumulative_mean {σ : ℝ} (hσ : 1 / 5 ≤ σ) : 9 / 10 < waveExponent σ + 1 / 2

theorem NavierStokes.ExponentLedger.signed_pressure_above_cumulative_mean {σ κ : ℝ} (hσ : 1 / 5 ≤ σ) (hκ : κ ≤ 1 / 100000) : 9 / 10 < waveExponent σ - κ + 1 / 2

Exact fixed choice and quantifier bookkeeping

theorem NavierStokes.ExponentLedger.manuscript_kappa_admissible : 0 ≤ 1 / 100000 ∧ 1 / 100000 ≤ 1 / 100000

theorem NavierStokes.ExponentLedger.smaller_kappa_admissible {κ : ℝ} (hκ : κ < 1 / 1000000) : κ ≤ 1 / 100000

A stricter κ < 10⁻⁶ also suffices, but is not the manuscript's choice.

theorem NavierStokes.ExponentLedger.old_difference_bar_margin_iff (κ : ℝ) : 17 / 100 < 9 / 50 - 2 * κ ↔ κ < 1 / 200

The most restrictive .17 bar margin has this exact threshold.

noncomputable def NavierStokes.ExponentLedger.stageParameter (n : ℕ) : ℝ

Iterated accuracy parameters; this does not assert existence of the iterates.

Equations

• NavierStokes.ExponentLedger.stageParameter n = 1 / 5 + ↑n / 10

theorem NavierStokes.ExponentLedger.stage_parameter_zero : stageParameter 0 = 1 / 5

theorem NavierStokes.ExponentLedger.stage_parameter_succ (n : ℕ) : stageParameter (n + 1) = stageParameter n + 1 / 10

theorem NavierStokes.ExponentLedger.stage_parameter_admissible (n : ℕ) : 1 / 5 ≤ stageParameter n

theorem NavierStokes.ExponentLedger.all_stage_arithmetic (n : ℕ) {κ : ℝ} (hκ : κ ≤ 1 / 100000) : waveExponent (stageParameter (n + 1)) < waveExponent (stageParameter n) + particularGain (stageParameter n) κ ∧ waveExponent (stageParameter (n + 1)) < waveExponent (stageParameter n) + signedGain (stageParameter n) κ ∧ waveExponent (stageParameter (n + 1)) < meanUpdateExponent (stageParameter n) κ ∧ meanExponent (stageParameter (n + 1)) < meanExponent (stageParameter n) + min (17 / 100) (1 - 4 * κ) ∧ meanExponent (stageParameter (n + 1)) < meanExponent (stageParameter n) + 9 / 10 - 4 * κ

The same fixed κ works for the numerical comparisons at every finite stage.