The actual native chart scales

The floor index is the one defined from the manuscript's logarithmic formula in SlotColoring. This module derives the coefficient comparisons in (25), their reciprocal bounds, the rounded carrier scale, and polynomial/exponential decay along the actual dyadic sequence.

Physical grid labels, bounded degree, and an explicit finite coloring

Labels consist of a dyadic level, three integer grid coordinates, and a sign. The physical mesh at exponent a is 2^(-n*a)/n^6, namely the mesh S_n^-3 with S_n=n², rescaled by Q_n^a with Q_n=2^-n. Closed boxes of two mesh widths include the fixed small enlargement of the one-mesh supports in the manuscript.

@[reducible, inline]

abbrev NavierStokes.SlotColoring.Grid : Type

Grid: an abbreviation for Fin 3 → ℤ.

Equations

• NavierStokes.SlotColoring.Grid = (Fin 3 → ℤ)

@[reducible, inline]

abbrev NavierStokes.SlotColoring.Position : Type

Position: an abbreviation for Fin 3 → ℝ.

Equations

• NavierStokes.SlotColoring.Position = (Fin 3 → ℝ)

@[reducible, inline]

abbrev NavierStokes.SlotColoring.Label : Type

Label: an abbreviation for ℕ × (Grid × Bool).

Equations

• NavierStokes.SlotColoring.Label = (ℕ × NavierStokes.SlotColoring.Grid × Bool)

noncomputable def NavierStokes.SlotColoring.dyadicQ (n : ℕ) : ℝ

Dyadic Q, given by (2 : ℝ) ^ (-(n : ℝ)).

Equations

• NavierStokes.SlotColoring.dyadicQ n = 2 ^ (-↑n)

noncomputable def NavierStokes.SlotColoring.spacing (a : ℝ) (n : ℕ) : ℝ

Spacing, given by (2 : ℝ) ^ (-(n : ℝ) * a) / (n : ℝ) ^ 6.

Equations

• NavierStokes.SlotColoring.spacing a n = 2 ^ (-↑n * a) / ↑n ^ 6

theorem NavierStokes.SlotColoring.spacing_eq_scaled_mesh (a : ℝ) (n : ℕ) : spacing a n = dyadicQ n ^ a * (1 / (↑n ^ 2) ^ 3)

theorem NavierStokes.SlotColoring.spacing_pos (a : ℝ) {n : ℕ} (hn : 1 ≤ n) : 0 < spacing a n

theorem NavierStokes.SlotColoring.spacing_ratio (a : ℝ) {n m : ℕ} (hn : 1 ≤ n) (hm : 1 ≤ m) : spacing a n / spacing a m = (↑m / ↑n) ^ 6 * 2 ^ ((↑m - ↑n) * a)

theorem NavierStokes.SlotColoring.spacing_ratio_le (a A : ℝ) {n m : ℕ} (hn : 1 ≤ n) (hm : 1 ≤ m) (hnm : n ≤ m + 4) (hmn : m ≤ n + 4) (ha : |a| ≤ A) : spacing a n / spacing a m ≤ 5 ^ 6 * 2 ^ (4 * A)

The mesh ratio is uniform across levels at distance at most four.

noncomputable def NavierStokes.SlotColoring.axisExponent (D : ℝ) : Fin 3 → ℝ

Axis exponent, given by ![1 / 2, D, 1].

Equations

• NavierStokes.SlotColoring.axisExponent D = ![1 / 2, D, 1]

noncomputable def NavierStokes.SlotColoring.width (D : ℝ) (j : Fin 3) (n : ℕ) : ℝ

Width, given by spacing (axisExponent D j) n.

Equations

• NavierStokes.SlotColoring.width D j n = NavierStokes.SlotColoring.spacing (NavierStokes.SlotColoring.axisExponent D j) n

noncomputable def NavierStokes.SlotColoring.ratioBound (D : ℝ) : ℝ

Ratio bound, given by (5 : ℝ) ^ 6 * (2 : ℝ) ^ (4 * (1 + |D|)).

Equations

• NavierStokes.SlotColoring.ratioBound D = 5 ^ 6 * 2 ^ (4 * (1 + |D|))

theorem NavierStokes.SlotColoring.width_pos (D : ℝ) (j : Fin 3) {n : ℕ} (hn : 1 ≤ n) : 0 < width D j n

theorem NavierStokes.SlotColoring.width_ratio_le (D : ℝ) (j : Fin 3) {n m : ℕ} (hn : 1 ≤ n) (hm : 1 ≤ m) (hnm : n ≤ m + 4) (hmn : m ≤ n + 4) : width D j n / width D j m ≤ ratioBound D

def NavierStokes.SlotColoring.physicalBox (D : ℝ) (L : Label) : Set Position

Physical box, given by {x | ∀ j, |x j - width D j L.1 * (L.2.1 j : ℝ)| ≤ 2 * width D j L.1}.

Equations

• One or more equations did not get rendered due to their size.

structure NavierStokes.SlotColoring.Adj (D : ℝ) (L M : Label) : Prop

The exact enlarged-box interaction relation used for coloring.

• left_positive : 1 ≤ L.1
• right_positive : 1 ≤ M.1
• distinct : L ≠ M
• left_level_le : L.1 ≤ M.1 + 4
• right_level_le : M.1 ≤ L.1 + 4
• overlap : (physicalBox D L ∩ physicalBox D M).Nonempty

theorem NavierStokes.SlotColoring.overlapping_centers (D : ℝ) (L M : Label) (hov : (physicalBox D L ∩ physicalBox D M).Nonempty) (j : Fin 3) : |width D j L.1 * ↑(L.2.1 j) - width D j M.1 * ↑(M.2.1 j)| ≤ 2 * (width D j L.1 + width D j M.1)

theorem NavierStokes.SlotColoring.same_level_grid_gap (D : ℝ) (L M : Label) (hn : 1 ≤ L.1) (hl : L.1 = M.1) (hov : (physicalBox D L ∩ physicalBox D M).Nonempty) (j : Fin 3) : |L.2.1 j - M.2.1 j| ≤ 4

def NavierStokes.SlotColoring.intColor (z : ℤ) : Fin 5

Int color as an element of Fin 5.

Equations

• NavierStokes.SlotColoring.intColor z = ⟨(z % 5).toNat, ⋯⟩

theorem NavierStokes.SlotColoring.intColor_eq_of_close {z w : ℤ} (hc : intColor z = intColor w) (hd : |z - w| ≤ 4) : z = w

@[reducible, inline]

abbrev NavierStokes.SlotColoring.Palette : Type

Palette: an abbreviation for Fin 9 × ((Fin 3 → Fin 5) × Bool).

Equations

• NavierStokes.SlotColoring.Palette = (Fin 9 × (Fin 3 → Fin 5) × Bool)

def NavierStokes.SlotColoring.colorData (L : Label) : Palette

Color data, given by (⟨L.1 % 9, Nat.mod_lt _ (by norm_num)⟩, (fun j => intColor (L.2.1 j), L.2.2)).

Equations

• NavierStokes.SlotColoring.colorData L = (⟨L.1 % 9, ⋯⟩, fun (j : Fin 3) => NavierStokes.SlotColoring.intColor (L.2.1 j), L.2.2)

theorem NavierStokes.SlotColoring.palette_card : Fintype.card Palette = 2250

theorem NavierStokes.SlotColoring.colorData_proper (D : ℝ) {L M : Label} (h : Adj D L M) : colorData L ≠ colorData M

This is a constructed coloring, not a coloring hypothesis.

noncomputable def NavierStokes.SlotColoring.color (L : Label) : Fin (Fintype.card Palette)

Color, given by (Fintype.equivFin Palette) (colorData L).

Equations

• NavierStokes.SlotColoring.color L = (Fintype.equivFin NavierStokes.SlotColoring.Palette) (NavierStokes.SlotColoring.colorData L)

theorem NavierStokes.SlotColoring.color_proper (D : ℝ) {L M : Label} (h : Adj D L M) : color L ≠ color M

theorem NavierStokes.SlotColoring.normalized_index_gap (h h' B : ℝ) (i j : ℤ) (hh' : 0 < h') (hratio : h / h' ≤ B) (hgap : |h * ↑i - h' * ↑j| ≤ 2 * (h + h')) : |h / h' * ↑i - ↑j| ≤ 2 * (B + 1)

A reusable one-dimensional bound: overlapping intervals force the finer grid index to lie within a fixed distance of the rescaled reference index.

theorem NavierStokes.SlotColoring.index_near_floor (c A : ℝ) (j : ℤ) (K : ℕ) (hgap : |c - ↑j| ≤ A) (hK : A + 1 ≤ ↑K) : |j - ⌊c⌋| ≤ ↑K

noncomputable def NavierStokes.SlotColoring.indexRadius (D : ℝ) : ℕ

Index radius, given by ⌈2 * (ratioBound D + 1) + 1⌉₊.

Equations

• NavierStokes.SlotColoring.indexRadius D = ⌈2 * (NavierStokes.SlotColoring.ratioBound D + 1) + 1⌉₊

noncomputable def NavierStokes.SlotColoring.indexCenter (D : ℝ) (L : Label) (m : ℕ) (j : Fin 3) : ℤ

Index center, given by ⌊width D j L.1 / width D j m * (L.2.1 j : ℝ)⌋.

Equations

• NavierStokes.SlotColoring.indexCenter D L m j = ⌊NavierStokes.SlotColoring.width D j L.1 / NavierStokes.SlotColoring.width D j m * ↑(L.2.1 j)⌋

noncomputable def NavierStokes.SlotColoring.candidateGrids (D : ℝ) (L : Label) (m : ℕ) : Finset Grid

Candidate grids, given by Fintype.piFinset (fun j => Finset.Icc (indexCenter D L m j - (indexRadius D : ℤ)) (indexCenter D L m j + (indexRadius D : ℤ))).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.SlotColoring.candidatesAtLevel (D : ℝ) (L : Label) (m : ℕ) : Finset Label

Candidates at level, given by ((candidateGrids D L m).product (Finset.univ : Finset Bool)).image (fun gs => (m, gs)).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.SlotColoring.candidates (D : ℝ) (L : Label) : Finset Label

Candidates, given by (Finset.Icc (L.1 - 4) (L.1 + 4)).biUnion (candidatesAtLevel D L).

Equations

• NavierStokes.SlotColoring.candidates D L = (Finset.Icc (L.1 - 4) (L.1 + 4)).biUnion (NavierStokes.SlotColoring.candidatesAtLevel D L)

theorem NavierStokes.SlotColoring.adj_index_bound (D : ℝ) {L M : Label} (h : Adj D L M) (j : Fin 3) : |M.2.1 j - indexCenter D L M.1 j| ≤ ↑(indexRadius D)

theorem NavierStokes.SlotColoring.adj_mem_candidates (D : ℝ) {L M : Label} (h : Adj D L M) : M ∈ candidates D L

theorem NavierStokes.SlotColoring.integer_interval_card (c : ℤ) (K : ℕ) : (Finset.Icc (c - ↑K) (c + ↑K)).card = 2 * K + 1

theorem NavierStokes.SlotColoring.candidateGrids_card (D : ℝ) (L : Label) (m : ℕ) : (candidateGrids D L m).card = (2 * indexRadius D + 1) ^ 3

theorem NavierStokes.SlotColoring.candidatesAtLevel_card_le (D : ℝ) (L : Label) (m : ℕ) : (candidatesAtLevel D L m).card ≤ (2 * indexRadius D + 1) ^ 3 * 2

noncomputable def NavierStokes.SlotColoring.degreeBound (D : ℝ) : ℕ

Degree bound, given by 18 * (2 * indexRadius D + 1) ^ 3.

Equations

• NavierStokes.SlotColoring.degreeBound D = 18 * (2 * NavierStokes.SlotColoring.indexRadius D + 1) ^ 3

theorem NavierStokes.SlotColoring.candidates_card_le (D : ℝ) (L : Label) : (candidates D L).card ≤ degreeBound D

noncomputable def NavierStokes.SlotColoring.neighbors (D : ℝ) (L : Label) : Finset Label

The actual finite neighbor set, obtained by filtering an explicit finite box.

Equations

• NavierStokes.SlotColoring.neighbors D L = Finset.filter (NavierStokes.SlotColoring.Adj D L) (NavierStokes.SlotColoring.candidates D L)

theorem NavierStokes.SlotColoring.mem_neighbors_iff (D : ℝ) (L M : Label) : M ∈ neighbors D L ↔ Adj D L M

theorem NavierStokes.SlotColoring.neighbors_card_le (D : ℝ) (L : Label) : (neighbors D L).card ≤ degreeBound D

Uniform degree control for every dyadic level, grid point, and sign.

theorem NavierStokes.SlotColoring.label_type_countable : Countable Label

noncomputable def NavierStokes.SlotColoring.coverGrowth : ℝ

The expanding eigenvalue of the actual covering matrix.

Equations

• NavierStokes.SlotColoring.coverGrowth = 4 + √2

theorem NavierStokes.SlotColoring.log_coverGrowth_pos : 0 < Real.log coverGrowth

noncomputable def NavierStokes.SlotColoring.nativeArgument (h : ℝ) (n : ℕ) : ℝ

The real expression whose floor defines the manuscript's native index.

Equations

• NavierStokes.SlotColoring.nativeArgument h n = Real.log (NavierStokes.SlotColoring.dyadicQ n ^ (-1 - h) / ↑n ^ 2) / Real.log NavierStokes.SlotColoring.coverGrowth

noncomputable def NavierStokes.SlotColoring.nativeIndex (h : ℝ) (n : ℕ) : ℕ

Native index, given by ⌊nativeArgument h n⌋₊.

Equations

• NavierStokes.SlotColoring.nativeIndex h n = ⌊NavierStokes.SlotColoring.nativeArgument h n⌋₊

theorem NavierStokes.SlotColoring.nativeArgument_expanded (h : ℝ) {n : ℕ} (hn : 1 ≤ n) : nativeArgument h n = (↑n * (1 + h) * Real.log 2 - 2 * Real.log ↑n) / Real.log coverGrowth

noncomputable def NavierStokes.SlotColoring.nativeGapBudget (h : ℝ) : ℝ

Native gap budget, given by (4 * (1 + h) * Real.log 2 + 2 * Real.log 5) / Real.log coverGrowth.

Equations

• NavierStokes.SlotColoring.nativeGapBudget h = (4 * (1 + h) * Real.log 2 + 2 * Real.log 5) / Real.log NavierStokes.SlotColoring.coverGrowth

noncomputable def NavierStokes.SlotColoring.nativeGap (h : ℝ) : ℕ

Native gap, given by ⌈nativeGapBudget h⌉₊ + 1.

Equations

• NavierStokes.SlotColoring.nativeGap h = ⌈NavierStokes.SlotColoring.nativeGapBudget h⌉₊ + 1

theorem NavierStokes.SlotColoring.log_level_gap {n m : ℕ} (hn : 1 ≤ n) (hm : 1 ≤ m) (hnm : n ≤ m + 4) (hmn : m ≤ n + 4) : |Real.log ↑n - Real.log ↑m| ≤ Real.log 5

theorem NavierStokes.SlotColoring.nativeArgument_gap (h : ℝ) (hh : 0 ≤ h) {n m : ℕ} (hn : 1 ≤ n) (hm : 1 ≤ m) (hnm : n ≤ m + 4) (hmn : m ≤ n + 4) : |nativeArgument h n - nativeArgument h m| ≤ nativeGapBudget h

theorem NavierStokes.SlotColoring.natFloor_gap_le (u v C : ℝ) (h : u - v ≤ C) : ⌊u⌋₊ ≤ ⌊v⌋₊ + (⌈C⌉₊ + 1)

theorem NavierStokes.SlotColoring.nativeIndex_gap (h : ℝ) (hh : 0 ≤ h) {n m : ℕ} (hn : 1 ≤ n) (hm : 1 ≤ m) (hnm : n ≤ m + 4) (hmn : m ≤ n + 4) : nativeIndex h n ≤ nativeIndex h m + nativeGap h ∧ nativeIndex h m ≤ nativeIndex h n + nativeGap h

The actual adjacent native indices have an explicit uniform gap.

theorem NavierStokes.SlotColoring.nat_square_le_two_pow {n : ℕ} (hn : 4 ≤ n) : n ^ 2 ≤ 2 ^ n

theorem NavierStokes.SlotColoring.nativeArgument_nonneg (h : ℝ) (hh : 0 ≤ h) {n : ℕ} (hn : 4 ≤ n) : 0 ≤ nativeArgument h n

n=4 is already a valid uniform threshold for nonnegative native indices when h≥0; the manuscript subsequently retains still larger bands.

theorem NavierStokes.SlotColoring.nativeIndex_eq_integer_floor (h : ℝ) (hh : 0 ≤ h) {n : ℕ} (hn : 4 ≤ n) : ↑(nativeIndex h n) = ⌊nativeArgument h n⌋

theorem NavierStokes.SlotColoring.physical_labels_have_auxiliary_slots (D h : ℝ) (hh : 0 ≤ h) (a b : SlotGeometry.Plane) : ∃ (r : ℝ), 0 < r ∧ ∀ (L M : Label), Adj D L M → Disjoint (SlotGeometry.liftedSupport (nativeIndex h L.1) (SlotGeometry.orientedRectangle (SlotGeometry.center (Fintype.card Palette) (nativeGap h) (color L)) a b (2 * r))) (SlotGeometry.liftedSupport (nativeIndex h M.1) (SlotGeometry.orientedRectangle (SlotGeometry.center (Fintype.card Palette) (nativeGap h) (color M)) a b (2 * r)))

The constructed finite coloring feeds the proved rational-slot geometry using the manuscript's actual native covering index, with no coloring or native-index-gap assumption.

@[reducible, inline]

noncomputable abbrev NavierStokes.ChartScales.Tg : ℝ

Tg: an abbreviation for SlotColoring.coverGrowth.

Equations

• NavierStokes.ChartScales.Tg = NavierStokes.SlotColoring.coverGrowth

noncomputable def NavierStokes.ChartScales.Lambda : ℝ

Lambda, given by 4 - Real.sqrt 2.

Equations

• NavierStokes.ChartScales.Lambda = 4 - √2

noncomputable def NavierStokes.ChartScales.rho : ℝ

Rho, given by Real.log Lambda / Real.log Tg.

Equations

• NavierStokes.ChartScales.rho = Real.log NavierStokes.ChartScales.Lambda / Real.log NavierStokes.ChartScales.Tg

noncomputable def NavierStokes.ChartScales.kappa : ℝ

Kappa, given by 1 / 100000.

Equations

• NavierStokes.ChartScales.kappa = 1 / 100000

noncomputable def NavierStokes.ChartScales.radialExponent (h : ℝ) : ℝ

Radial exponent, given by 2 * ((1 + h) * rho - h * kappa).

Equations

• NavierStokes.ChartScales.radialExponent h = 2 * ((1 + h) * NavierStokes.ChartScales.rho - h * NavierStokes.ChartScales.kappa)

@[reducible, inline]

noncomputable abbrev NavierStokes.ChartScales.Q (n : ℕ) : ℝ

Q: an abbreviation for SlotColoring.dyadicQ n.

Equations

• NavierStokes.ChartScales.Q n = NavierStokes.SlotColoring.dyadicQ n

def NavierStokes.ChartScales.S (n : ℕ) : ℝ

S, given by (n : ℝ) ^ 2.

Equations

• NavierStokes.ChartScales.S n = ↑n ^ 2

noncomputable def NavierStokes.ChartScales.epsilon (h : ℝ) (n : ℕ) : ℝ

Epsilon, given by Q n ^ h.

Equations

• NavierStokes.ChartScales.epsilon h n = NavierStokes.ChartScales.Q n ^ h

@[reducible, inline]

noncomputable abbrev NavierStokes.ChartScales.nativeIndex (h : ℝ) (n : ℕ) : ℕ

Native index: an abbreviation for SlotColoring.nativeIndex h n.

Equations

• NavierStokes.ChartScales.nativeIndex h n = NavierStokes.SlotColoring.nativeIndex h n

noncomputable def NavierStokes.ChartScales.timeCoefficient (h : ℝ) (n : ℕ) : ℝ

Time coefficient, given by Tg ^ nativeIndex h n * Q n ^ (1 + h).

Equations

• NavierStokes.ChartScales.timeCoefficient h n = NavierStokes.ChartScales.Tg ^ NavierStokes.ChartScales.nativeIndex h n * NavierStokes.ChartScales.Q n ^ (1 + h)

noncomputable def NavierStokes.ChartScales.radialCoefficient (h : ℝ) (n : ℕ) : ℝ

Radial coefficient, given by Lambda ^ nativeIndex h n * Q n ^ (radialExponent h / 2).

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.ChartScales.sqrt_two_lt_two : √2 < 2

theorem NavierStokes.ChartScales.Tg_one_lt : 1 < Tg

theorem NavierStokes.ChartScales.Tg_pos : 0 < Tg

theorem NavierStokes.ChartScales.log_Tg_pos : 0 < Real.log Tg

theorem NavierStokes.ChartScales.Lambda_two_lt : 2 < Lambda

theorem NavierStokes.ChartScales.Lambda_pos : 0 < Lambda

theorem NavierStokes.ChartScales.log_Lambda_pos : 0 < Real.log Lambda

theorem NavierStokes.ChartScales.rho_lower : 1 / 3 ≤ rho

A coarse explicit bound suffices to show that the radial power is positive.

theorem NavierStokes.ChartScales.rho_pos : 0 < rho

theorem NavierStokes.ChartScales.radialExponent_pos (h : ℝ) (hh : 0 ≤ h) : 0 < radialExponent h

This includes the manuscript's range 0<h<1/2, and in fact every h≥0.

theorem NavierStokes.ChartScales.Q_pos (n : ℕ) : 0 < Q n

theorem NavierStokes.ChartScales.Q_le_one (n : ℕ) : Q n ≤ 1

theorem NavierStokes.ChartScales.S_pos {n : ℕ} (hn : 1 ≤ n) : 0 < S n

theorem NavierStokes.ChartScales.epsilon_pos (h : ℝ) (n : ℕ) : 0 < epsilon h n

theorem NavierStokes.ChartScales.epsilon_le_one (h : ℝ) (hh : 0 ≤ h) (n : ℕ) : epsilon h n ≤ 1

theorem NavierStokes.ChartScales.timeCoefficient_pos (h : ℝ) (n : ℕ) : 0 < timeCoefficient h n

theorem NavierStokes.ChartScales.radialCoefficient_pos (h : ℝ) (n : ℕ) : 0 < radialCoefficient h n

theorem NavierStokes.ChartScales.Tg_rpow_rho : Tg ^ rho = Lambda

theorem NavierStokes.ChartScales.Lambda_pow_eq (n : ℕ) : Lambda ^ n = (Tg ^ n) ^ rho

theorem NavierStokes.ChartScales.native_power_bounds (h : ℝ) (hh : 0 ≤ h) {n : ℕ} (hn : 4 ≤ n) : Tg ^ nativeIndex h n ≤ Q n ^ (-1 - h) / S n ∧ Q n ^ (-1 - h) / S n ≤ Tg * Tg ^ nativeIndex h n

theorem NavierStokes.ChartScales.timeCoefficient_bounds (h : ℝ) (hh : 0 ≤ h) {n : ℕ} (hn : 4 ≤ n) : 1 / (Tg * S n) ≤ timeCoefficient h n ∧ timeCoefficient h n ≤ 1 / S n

The actual floor index gives the complete c_i comparison in (25).

theorem NavierStokes.ChartScales.radialCoefficient_eq (h : ℝ) (n : ℕ) : radialCoefficient h n = epsilon h n ^ (-kappa) * timeCoefficient h n ^ rho

The radial coefficient is an exact power of the time coefficient, with the explicit small-viscosity loss.

theorem NavierStokes.ChartScales.radialCoefficient_bounds (h : ℝ) (hh : 0 ≤ h) {n : ℕ} (hn : 4 ≤ n) : epsilon h n ^ (-kappa) * S n ^ (-rho) / Lambda ≤ radialCoefficient h n ∧ radialCoefficient h n ≤ epsilon h n ^ (-kappa) * S n ^ (-rho)

The full M_i comparison in (25), obtained from the actual native index.

theorem NavierStokes.ChartScales.timeCoefficient_inv_upper (h : ℝ) (hh : 0 ≤ h) {n : ℕ} (hn : 4 ≤ n) : (timeCoefficient h n)⁻¹ ≤ Tg * S n

theorem NavierStokes.ChartScales.radialCoefficient_inv_upper (h : ℝ) (hh : 0 ≤ h) {n : ℕ} (hn : 4 ≤ n) : (radialCoefficient h n)⁻¹ ≤ Lambda * epsilon h n ^ kappa * S n ^ rho

theorem NavierStokes.ChartScales.timeCoefficient_inv_lower (h : ℝ) (hh : 0 ≤ h) {n : ℕ} (hn : 4 ≤ n) : S n ≤ (timeCoefficient h n)⁻¹

noncomputable def NavierStokes.ChartScales.slotLength (r0 h : ℝ) (n : ℕ) : ℝ

Slot length, given by 2 * r0 / timeCoefficient h n.

Equations

• NavierStokes.ChartScales.slotLength r0 h n = 2 * r0 / NavierStokes.ChartScales.timeCoefficient h n

theorem NavierStokes.ChartScales.slotLength_bounds (r0 h : ℝ) (hr : 0 ≤ r0) (hh : 0 ≤ h) {n : ℕ} (hn : 4 ≤ n) : 2 * r0 * S n ≤ slotLength r0 h n ∧ slotLength r0 h n ≤ 2 * r0 * Tg * S n

The native slot has length comparable to the actual slow scale n².

noncomputable def NavierStokes.ChartScales.carrier (h : ℝ) (n : ℕ) : ℕ

The carrier is the genuine rounded integer frequency used in the manuscript.

Equations

• NavierStokes.ChartScales.carrier h n = NavierStokes.Scaling.carrierFrequency (NavierStokes.ChartScales.epsilon h n)

theorem NavierStokes.ChartScales.carrier_viscosity_bounds (h : ℝ) (hh : 0 ≤ h) (n : ℕ) : 1 ≤ epsilon h n * ↑(carrier h n) ^ 2 ∧ epsilon h n * ↑(carrier h n) ^ 2 ≤ 4

theorem NavierStokes.ChartScales.carrier_inv_bounds (h : ℝ) (hh : 0 ≤ h) (n : ℕ) : √(epsilon h n) / 2 ≤ 1 / ↑(carrier h n) ∧ 1 / ↑(carrier h n) ≤ √(epsilon h n)

theorem NavierStokes.ChartScales.slow_power_epsilon_identity (h a b : ℝ) (n : ℕ) : S n ^ a * epsilon h n ^ b = ↑n ^ (2 * a) * Real.exp (-(h * b * Real.log 2) * ↑n)

theorem NavierStokes.ChartScales.slow_power_epsilon_tendsto_zero (h : ℝ) (hh : 0 < h) (a b : ℝ) (hb : 0 < b) : Filter.Tendsto (fun (n : ℕ) => S n ^ a * epsilon h n ^ b) Filter.atTop (nhds 0)

Every fixed real power of the slow scale is dominated by every positive power of the actual small-viscosity scale, provided h>0.

theorem NavierStokes.ChartScales.eventually_slow_power_epsilon_lt (h : ℝ) (hh : 0 < h) (a b δ : ℝ) (hb : 0 < b) (hδ : 0 < δ) : ∀ᶠ (n : ℕ) in Filter.atTop, S n ^ a * epsilon h n ^ b < δ

theorem NavierStokes.ChartScales.exists_slow_power_epsilon_cutoff (h : ℝ) (hh : 0 < h) (a b δ : ℝ) (hb : 0 < b) (hδ : 0 < δ) : ∃ (N : ℕ), ∀ n ≥ N, S n ^ a * epsilon h n ^ b < δ

theorem NavierStokes.ChartScales.slow_power_div_carrier_tendsto_zero (h : ℝ) (hh : 0 < h) (a : ℝ) : Filter.Tendsto (fun (n : ℕ) => S n ^ a / ↑(carrier h n)) Filter.atTop (nhds 0)

The rounding error 1/k, multiplied by any fixed slow power, also vanishes along the actual dyadic sequence.