The arithmetic ledger for actual correction stages

The input of cycle n has accuracy sigma n. Its physical increment has index n+1, while a finite prefix after J cycles has accuracy sigma J. The gain and all physical offsets below are fixed before the stage index. This module does not assert the existence of correction cycles or their native class estimates.

noncomputable def NavierStokes.ActualIterationLedger.sigma (J : ℕ) : ℝ

Accuracy of the state after this many correction cycles.

Equations

• NavierStokes.ActualIterationLedger.sigma J = NavierStokes.ExponentLedger.stageParameter J

noncomputable def NavierStokes.ActualIterationLedger.inputSigma (j : ℕ) : ℝ

The input accuracy used to construct a positive physical increment. The value at zero is unused by the positive-stage estimates.

Equations

• NavierStokes.ActualIterationLedger.inputSigma j = NavierStokes.ActualIterationLedger.sigma (j - 1)

noncomputable def NavierStokes.ActualIterationLedger.gain (h : ℝ) (j : ℕ) : ℝ

One common physical gain for all increment types and finite residuals.

Equations

• NavierStokes.ActualIterationLedger.gain h j = h * ↑j / 10

noncomputable def NavierStokes.ActualIterationLedger.kappa : ℝ

The same admissible loss is used at every cycle.

Equations

• NavierStokes.ActualIterationLedger.kappa = 1 / 100000

@[simp]

theorem NavierStokes.ActualIterationLedger.sigma_zero : sigma 0 = 1 / 5

theorem NavierStokes.ActualIterationLedger.sigma_formula (J : ℕ) : sigma J = 1 / 5 + ↑J / 10

theorem NavierStokes.ActualIterationLedger.sigma_succ (J : ℕ) : sigma (J + 1) = sigma J + 1 / 10

theorem NavierStokes.ActualIterationLedger.sigma_admissible (J : ℕ) : 1 / 5 ≤ sigma J

theorem NavierStokes.ActualIterationLedger.sigma_strictMono : StrictMono sigma

@[simp]

theorem NavierStokes.ActualIterationLedger.inputSigma_succ (j : ℕ) : inputSigma (j + 1) = sigma j

theorem NavierStokes.ActualIterationLedger.inputSigma_formula {j : ℕ} (hj : 1 ≤ j) : inputSigma j = 1 / 10 + ↑j / 10

theorem NavierStokes.ActualIterationLedger.inputSigma_index {j : ℕ} (hj : 1 ≤ j) : inputSigma j + 1 / 10 = sigma j

theorem NavierStokes.ActualIterationLedger.inputSigma_admissible (j : ℕ) : 1 / 5 ≤ inputSigma j

@[simp]

theorem NavierStokes.ActualIterationLedger.gain_zero (h : ℝ) : gain h 0 = 0

theorem NavierStokes.ActualIterationLedger.gain_succ (h : ℝ) (j : ℕ) : gain h (j + 1) = gain h j + h / 10

theorem NavierStokes.ActualIterationLedger.gain_eq_accuracy (h : ℝ) (J : ℕ) : gain h J = h * (sigma J - 1 / 5)

theorem NavierStokes.ActualIterationLedger.gain_nonneg {h : ℝ} (hh : 0 ≤ h) (j : ℕ) : 0 ≤ gain h j

theorem NavierStokes.ActualIterationLedger.gain_pos {h : ℝ} (hh : 0 < h) {j : ℕ} (hj : 1 ≤ j) : 0 < gain h j

theorem NavierStokes.ActualIterationLedger.gain_monotone {h : ℝ} (hh : 0 ≤ h) : Monotone (gain h)

theorem NavierStokes.ActualIterationLedger.gain_strictMono {h : ℝ} (hh : 0 < h) : StrictMono (gain h)

theorem NavierStokes.ActualIterationLedger.gain_add_tendsto_atTop {h : ℝ} (hh : 0 < h) (a : ℝ) : Filter.Tendsto (fun (j : ℕ) => gain h j + a) Filter.atTop Filter.atTop

theorem NavierStokes.ActualIterationLedger.gain_tendsto_atTop {h : ℝ} (hh : 0 < h) : Filter.Tendsto (gain h) Filter.atTop Filter.atTop

theorem NavierStokes.ActualIterationLedger.sigma_tendsto_atTop : Filter.Tendsto sigma Filter.atTop Filter.atTop

theorem NavierStokes.ActualIterationLedger.kappa_admissible : 0 ≤ kappa ∧ kappa ≤ 1 / 100000

theorem NavierStokes.ActualIterationLedger.kappa_pos : 0 < kappa

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

The native increment exponents and their physical comparison

noncomputable def NavierStokes.ActualIterationLedger.waveNative (κ : ℝ) (j : ℕ) : ℝ

Conservative class for the actual wave potential. The local inverse frequency can give an additional half power, which is not needed here.

Equations

• NavierStokes.ActualIterationLedger.waveNative κ j = NavierStokes.ExponentLedger.waveExponent (NavierStokes.ActualIterationLedger.inputSigma j) - κ

noncomputable def NavierStokes.ActualIterationLedger.wavePressureNative (κ : ℝ) (j : ℕ) : ℝ

Wave pressure native, given by waveNative κ j + 1 / 2.

Equations

• NavierStokes.ActualIterationLedger.wavePressureNative κ j = NavierStokes.ActualIterationLedger.waveNative κ j + 1 / 2

noncomputable def NavierStokes.ActualIterationLedger.meanNative (κ : ℝ) (j : ℕ) : ℝ

Mean native, given by ExponentLedger.meanUpdateExponent (inputSigma j) κ.

Equations

• NavierStokes.ActualIterationLedger.meanNative κ j = NavierStokes.ExponentLedger.meanUpdateExponent (NavierStokes.ActualIterationLedger.inputSigma j) κ

noncomputable def NavierStokes.ActualIterationLedger.radialNative (κ : ℝ) (j : ℕ) : ℝ

Radial native, given by meanNative κ j + 1.

Equations

• NavierStokes.ActualIterationLedger.radialNative κ j = NavierStokes.ActualIterationLedger.meanNative κ j + 1

theorem NavierStokes.ActualIterationLedger.waveNative_formula (κ : ℝ) {j : ℕ} (hj : 1 ≤ j) : waveNative κ j = ↑j / 10 + (3 / 5 - κ)

theorem NavierStokes.ActualIterationLedger.wavePressureNative_formula (κ : ℝ) {j : ℕ} (hj : 1 ≤ j) : wavePressureNative κ j = ↑j / 10 + (11 / 10 - κ)

theorem NavierStokes.ActualIterationLedger.meanNative_formula (κ : ℝ) {j : ℕ} (hj : 1 ≤ j) : meanNative κ j = ↑j / 10 + (11 / 10 - 2 * κ)

theorem NavierStokes.ActualIterationLedger.radialNative_formula (κ : ℝ) {j : ℕ} (hj : 1 ≤ j) : radialNative κ j = ↑j / 10 + (21 / 10 - 2 * κ)

theorem NavierStokes.ActualIterationLedger.wave_physical_gap (h κ : ℝ) {j : ℕ} (hj : 1 ≤ j) : h * waveNative κ j = gain h j + h * (3 / 5 - κ)

theorem NavierStokes.ActualIterationLedger.pressure_physical_gap (h κ : ℝ) {j : ℕ} (hj : 1 ≤ j) : h * wavePressureNative κ j = gain h j + h * (11 / 10 - κ)

theorem NavierStokes.ActualIterationLedger.mean_physical_gap (h κ : ℝ) {j : ℕ} (hj : 1 ≤ j) : h * meanNative κ j = gain h j + h * (11 / 10 - 2 * κ)

theorem NavierStokes.ActualIterationLedger.gain_le_wave {h κ : ℝ} (hh : 0 ≤ h) (hκ : κ ≤ 1 / 100000) {j : ℕ} (hj : 1 ≤ j) : gain h j ≤ h * waveNative κ j

theorem NavierStokes.ActualIterationLedger.gain_le_wavePressure {h κ : ℝ} (hh : 0 ≤ h) (hκ : κ ≤ 1 / 100000) {j : ℕ} (hj : 1 ≤ j) : gain h j ≤ h * wavePressureNative κ j

theorem NavierStokes.ActualIterationLedger.gain_le_mean {h κ : ℝ} (hh : 0 ≤ h) (hκ : κ ≤ 1 / 100000) {j : ℕ} (hj : 1 ≤ j) : gain h j ≤ h * meanNative κ j

theorem NavierStokes.ActualIterationLedger.gain_le_radial {h κ : ℝ} (hh : 0 ≤ h) (hκ : κ ≤ 1 / 100000) {j : ℕ} (hj : 1 ≤ j) : gain h j ≤ h * radialNative κ j

structure NavierStokes.ActualIterationLedger.Offsets : Type

Offsets data, collecting wavePotential, meanStream, directAngular, wavePressure, meanPressure.

• wavePotential : ℝ

  Wave potential of Offsets, of type ℝ.

• meanStream : ℝ

  Mean stream of Offsets, of type ℝ.

• directAngular : ℝ

  Direct angular of Offsets, of type ℝ.

• wavePressure : ℝ

  Wave pressure of Offsets, of type ℝ.

• meanPressure : ℝ

  Mean pressure of Offsets, of type ℝ.

noncomputable def NavierStokes.ActualIterationLedger.offsets (h : ℝ) : Offsets

These five constants do not depend on an increment or derivative index.

Equations

• NavierStokes.ActualIterationLedger.offsets h = { wavePotential := h, meanStream := 0, directAngular := 0, wavePressure := 2 * NavierStokes.CoordinateAlgebra.A h, meanPressure := 0 }

theorem NavierStokes.ActualIterationLedger.fixed_offset_inequalities {h κ : ℝ} (hh : 0 ≤ h) (hκ : κ ≤ 1 / 100000) {j : ℕ} (hj : 1 ≤ j) : gain h j ≤ h * waveNative κ j + -h + (offsets h).wavePotential ∧ gain h j ≤ h * meanNative κ j + (offsets h).meanStream ∧ gain h j ≤ h * meanNative κ j + (offsets h).directAngular ∧ gain h j ≤ h * wavePressureNative κ j + -(2 * CoordinateAlgebra.A h) + (offsets h).wavePressure ∧ gain h j ≤ h * meanNative κ j + (offsets h).meanPressure

Residual indexing after a finite number of cycles

noncomputable def NavierStokes.ActualIterationLedger.residualWave (J : ℕ) : ℝ

Residual wave, given by ExponentLedger.waveExponent (sigma J).

Equations

• NavierStokes.ActualIterationLedger.residualWave J = NavierStokes.ExponentLedger.waveExponent (NavierStokes.ActualIterationLedger.sigma J)

noncomputable def NavierStokes.ActualIterationLedger.residualMean (J : ℕ) : ℝ

Residual mean, given by ExponentLedger.meanExponent (sigma J).

Equations

• NavierStokes.ActualIterationLedger.residualMean J = NavierStokes.ExponentLedger.meanExponent (NavierStokes.ActualIterationLedger.sigma J)

theorem NavierStokes.ActualIterationLedger.residualWave_formula (J : ℕ) : residualWave J = ↑J / 10 + 7 / 10

theorem NavierStokes.ActualIterationLedger.residualMean_formula (J : ℕ) : residualMean J = ↑J / 10 + 6 / 5

theorem NavierStokes.ActualIterationLedger.cycle_wave_output (n : ℕ) : ExponentLedger.waveExponent (sigma n) + 1 / 10 = residualWave (n + 1)

theorem NavierStokes.ActualIterationLedger.cycle_mean_output (n : ℕ) : ExponentLedger.meanExponent (sigma n) + 1 / 10 = residualMean (n + 1)

theorem NavierStokes.ActualIterationLedger.residual_minimum (J : ℕ) : min (residualWave J) (residualMean J) = residualWave J

theorem NavierStokes.ActualIterationLedger.residual_physical_gap (h : ℝ) (J : ℕ) : h * residualWave J = gain h J + 7 * h / 10

theorem NavierStokes.ActualIterationLedger.residual_mean_physical_gap (h : ℝ) (J : ℕ) : h * residualMean J = gain h J + 6 * h / 5

theorem NavierStokes.ActualIterationLedger.gain_le_residualWave {h : ℝ} (hh : 0 ≤ h) (J : ℕ) : gain h J ≤ h * residualWave J

theorem NavierStokes.ActualIterationLedger.gain_le_residualMean {h : ℝ} (hh : 0 ≤ h) (J : ℕ) : gain h J ≤ h * residualMean J

theorem NavierStokes.ActualIterationLedger.gain_le_residualMinimum {h : ℝ} (hh : 0 ≤ h) (J : ℕ) : gain h J ≤ h * min (residualWave J) (residualMean J)

theorem NavierStokes.ActualIterationLedger.gain_after_cycle {h : ℝ} (hh : 0 ≤ h) (n : ℕ) : gain h (n + 1) ≤ h * (ExponentLedger.waveExponent (sigma n) + 1 / 10)

noncomputable def NavierStokes.ActualIterationLedger.residualLoss (h beta : ℝ) (m : ℕ) : ℝ

The full-phase derivative cost is a fixed parameter beta, not a stage-dependent loss.

Equations

• NavierStokes.ActualIterationLedger.residualLoss h beta m = NavierStokes.PhysicalGraphBounds.graphLoss m + 1 + (2 * NavierStokes.CoordinateAlgebra.A h + 1 / 2) + beta * ↑m

noncomputable def NavierStokes.ActualIterationLedger.residualRate (h beta : ℝ) (J m : ℕ) : ℝ

Residual rate, given by h * residualWave J - residualLoss h beta m.

Equations

• NavierStokes.ActualIterationLedger.residualRate h beta J m = h * NavierStokes.ActualIterationLedger.residualWave J - NavierStokes.ActualIterationLedger.residualLoss h beta m

theorem NavierStokes.ActualIterationLedger.residualRate_eq (h beta : ℝ) (J m : ℕ) : residualRate h beta J m = gain h J + (7 * h / 10 - residualLoss h beta m)

theorem NavierStokes.ActualIterationLedger.gain_le_residual_rate {h : ℝ} (hh : 0 ≤ h) (beta : ℝ) (J m : ℕ) : gain h J - residualLoss h beta m ≤ residualRate h beta J m

theorem NavierStokes.ActualIterationLedger.residualRate_tendsto_atTop {h : ℝ} (hh : 0 < h) (beta : ℝ) (m : ℕ) : Filter.Tendsto (fun (J : ℕ) => residualRate h beta J m) Filter.atTop Filter.atTop

theorem NavierStokes.ActualIterationLedger.eventually_residualRate_ge {h : ℝ} (hh : 0 < h) (beta : ℝ) (m : ℕ) (a : ℝ) : ∀ᶠ (J : ℕ) in Filter.atTop, a ≤ residualRate h beta J m

theorem NavierStokes.ActualIterationLedger.residual_bound_with_gain {V : Type u_1} [NormedAddCommGroup V] {h beta C q : ℝ} (hh : 0 ≤ h) (hC : 0 ≤ C) (hq : 0 < q) (hq1 : q ≤ 1) (J m : ℕ) {v : V} (hv : ‖v‖ ≤ C * q ^ residualRate h beta J m) : ‖v‖ ≤ C * q ^ (gain h J - residualLoss h beta m)

Binding the ledger to the actual physical-stage interface

structure NavierStokes.ActualIterationLedger.StageMetadata {h : ℝ} {DA DP : Type} [NormedAddCommGroup DA] [NormedSpace ℝ DA] [NormedAddCommGroup DP] [NormedSpace ℝ DP] {IA : Type u_1} {KA : Type u_2} {IP : Type u_3} {KP : Type u_4} (WA : ℕ → PhysicalStageBounds.WaveData h DA IA KA (Fin 3)) (MA : ℕ → PhysicalStageBounds.MeanData h (CoordinateAlgebra.A h - 1 / 2)) (MB : ℕ → PhysicalStageBounds.MeanData h (CoordinateAlgebra.A h)) (WP : ℕ → PhysicalStageBounds.WaveData h DP IP KP Unit) (MP : ℕ → PhysicalStageBounds.MeanData h (2 * CoordinateAlgebra.A h)) (κ : ℝ) : Prop

Only native exponent metadata occur here. The physical fields, charts, regularity and local class estimates are those in the supplied WaveData and MeanData. The sharper potential class may be weakened to B−κ.

• wavePotential (j : ℕ) : 1 ≤ j → waveNative κ j ≤ (WA j).alpha
• wavePotentialShift (j : ℕ) : 1 ≤ j → -h ≤ (WA j).shift
• meanStream (j : ℕ) : 1 ≤ j → meanNative κ j ≤ (MA j).alpha
• directAngular (j : ℕ) : 1 ≤ j → meanNative κ j ≤ (MB j).alpha
• wavePressure (j : ℕ) : 1 ≤ j → wavePressureNative κ j ≤ (WP j).alpha
• wavePressureShift (j : ℕ) : 1 ≤ j → -(2 * CoordinateAlgebra.A h) ≤ (WP j).shift
• meanPressure (j : ℕ) : 1 ≤ j → meanNative κ j ≤ (MP j).alpha

theorem NavierStokes.ActualIterationLedger.StageMetadata.gain_inequalities {h κ : ℝ} {DA DP : Type} [NormedAddCommGroup DA] [NormedSpace ℝ DA] [NormedAddCommGroup DP] [NormedSpace ℝ DP] {IA : Type u_1} {KA : Type u_2} {IP : Type u_3} {KP : Type u_4} {WA : ℕ → PhysicalStageBounds.WaveData h DA IA KA (Fin 3)} {MA : ℕ → PhysicalStageBounds.MeanData h (CoordinateAlgebra.A h - 1 / 2)} {MB : ℕ → PhysicalStageBounds.MeanData h (CoordinateAlgebra.A h)} {WP : ℕ → PhysicalStageBounds.WaveData h DP IP KP Unit} {MP : ℕ → PhysicalStageBounds.MeanData h (2 * CoordinateAlgebra.A h)} (H : StageMetadata WA MA MB WP MP κ) (hh : 0 ≤ h) (hκ : κ ≤ 1 / 100000) : (∀ (j : ℕ), 1 ≤ j → gain h j ≤ h * (WA j).alpha + (WA j).shift + (offsets h).wavePotential) ∧ (∀ (j : ℕ), 1 ≤ j → gain h j ≤ h * (MA j).alpha + (offsets h).meanStream) ∧ (∀ (j : ℕ), 1 ≤ j → gain h j ≤ h * (MB j).alpha + (offsets h).directAngular) ∧ (∀ (j : ℕ), 1 ≤ j → gain h j ≤ h * (WP j).alpha + (WP j).shift + (offsets h).wavePressure) ∧ ∀ (j : ℕ), 1 ≤ j → gain h j ≤ h * (MP j).alpha + (offsets h).meanPressure

theorem NavierStokes.ActualIterationLedger.StageMetadata.derived_stage_inputs {h κ qbig : ℝ} {DA DP : Type} [NormedAddCommGroup DA] [NormedSpace ℝ DA] [NormedAddCommGroup DP] [NormedSpace ℝ DP] {IA : Type u_1} {KA : Type u_2} {IP : Type u_3} {KP : Type u_4} {WA : ℕ → PhysicalStageBounds.WaveData h DA IA KA (Fin 3)} {MA : ℕ → PhysicalStageBounds.MeanData h (CoordinateAlgebra.A h - 1 / 2)} {MB : ℕ → PhysicalStageBounds.MeanData h (CoordinateAlgebra.A h)} {WP : ℕ → PhysicalStageBounds.WaveData h DP IP KP Unit} {MP : ℕ → PhysicalStageBounds.MeanData h (2 * CoordinateAlgebra.A h)} (H : StageMetadata WA MA MB WP MP κ) (hh : 0 < h) (hh1 : h < 1 / 2) (hκ : 0 ≤ κ ∧ κ ≤ 1 / 100000) (baseA : ProblemStatement.VelocityField) (baseP : ProblemStatement.PressureField) (hbaseA : ContDiffOn ℝ (↑⊤) baseA (CutStageEstimates.physicalSublevel h qbig)) (hbaseP : ContDiffOn ℝ (↑⊤) baseP (CutStageEstimates.physicalSublevel h qbig)) (hqA : ∀ (j : ℕ), qbig ≤ ChartScales.Q (MA j).firstBand) (hqB : ∀ (j : ℕ), qbig ≤ ChartScales.Q (MB j).firstBand) (hqP : ∀ (j : ℕ), qbig ≤ ChartScales.Q (MP j).firstBand) : ∃ (CA : ℕ → ℕ → ℝ) (CB : ℕ → ℕ → ℝ) (CP : ℕ → ℕ → ℝ), (∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (PhysicalStageBounds.potentialStages baseA WA MA j) (CutStageEstimates.physicalSublevel h qbig)) ∧ (∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (PhysicalStageBounds.directStages MB j) (CutStageEstimates.physicalSublevel h qbig)) ∧ (∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (PhysicalStageBounds.pressureStages baseP WP MP j) (CutStageEstimates.physicalSublevel h qbig)) ∧ CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ h) (PhysicalStageBounds.potentialStages baseA WA MA) (gain h) (PhysicalStageBounds.potentialLoss h (offsets h).wavePotential (offsets h).meanStream) CA (fun (x x_1 : ℕ) => 0) (PhysicalWaveSum.preterminal ∩ CutStageEstimates.physicalSublevel h qbig) ∧ CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ h) (PhysicalStageBounds.directStages MB) (gain h) (PhysicalStageBounds.directLoss h (offsets h).directAngular) CB (fun (x x_1 : ℕ) => 0) (PhysicalWaveSum.preterminal ∩ CutStageEstimates.physicalSublevel h qbig) ∧ CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ h) (PhysicalStageBounds.pressureStages baseP WP MP) (gain h) (PhysicalStageBounds.pressureLoss h (offsets h).wavePressure (offsets h).meanPressure) CP (fun (x x_1 : ℕ) => 0) (PhysicalWaveSum.preterminal ∩ CutStageEstimates.physicalSublevel h qbig)

All five arithmetic premises of derived_stage_inputs are discharged for the one explicit gain sequence. Analytic input data remain explicit.

theorem NavierStokes.ActualIterationLedger.fixed_ledger {h : ℝ} (hh : 0 < h) : (0 ≤ kappa ∧ kappa ≤ 1 / 100000) ∧ sigma 0 = 1 / 5 ∧ (∀ (n : ℕ), sigma (n + 1) = sigma n + 1 / 10) ∧ gain h 0 = 0 ∧ (∀ (j : ℕ), 1 ≤ j → 0 < gain h j) ∧ Monotone (gain h) ∧ Filter.Tendsto (gain h) Filter.atTop Filter.atTop ∧ ∀ (j : ℕ), 1 ≤ j → gain h j ≤ h * waveNative kappa j + -h + (offsets h).wavePotential ∧ gain h j ≤ h * meanNative kappa j + (offsets h).meanStream ∧ gain h j ≤ h * meanNative kappa j + (offsets h).directAngular ∧ gain h j ≤ h * wavePressureNative kappa j + -(2 * CoordinateAlgebra.A h) + (offsets h).wavePressure ∧ gain h j ≤ h * meanNative kappa j + (offsets h).meanPressure

A single fixed κ, the explicit accuracy sequence, and the explicit gain work simultaneously at every stage. No iteration is asserted here.