Rational auxiliary slots separated under bounded covering powers

This file constructs the rational centers required in Lemma 8.3 for the specific covering matrix J = [[3,1],[1,5]]. The centers are explicit. Finite-dimensional continuity then gives a single positive rectangle radius, including padding and injectivity modulo the integer lattice.

@[reducible, inline]

abbrev NavierStokes.SlotGeometry.Plane : Type

Plane: an abbreviation for ℝ × ℝ.

Equations

• NavierStokes.SlotGeometry.Plane = (ℝ × ℝ)

def NavierStokes.SlotGeometry.cover : Plane →L[ℝ] Plane

The actual integer covering matrix from the manuscript.

Equations

• NavierStokes.SlotGeometry.cover = (3 • ContinuousLinearMap.fst ℝ ℝ ℝ + ContinuousLinearMap.snd ℝ ℝ ℝ).prod (ContinuousLinearMap.fst ℝ ℝ ℝ + 5 • ContinuousLinearMap.snd ℝ ℝ ℝ)

@[simp]

theorem NavierStokes.SlotGeometry.cover_apply (x : Plane) : cover x = (3 * x.1 + x.2, x.1 + 5 * x.2)

theorem NavierStokes.SlotGeometry.cover_injective : Function.Injective ⇑cover

theorem NavierStokes.SlotGeometry.cover_pow_injective (n : ℕ) : Function.Injective ⇑(cover ^ n)

theorem NavierStokes.SlotGeometry.norm_cover_le (x : Plane) : ‖cover x‖ ≤ 6 * ‖x‖

theorem NavierStokes.SlotGeometry.norm_cover_pow_le (n : ℕ) (x : Plane) : ‖(cover ^ n) x‖ ≤ 6 ^ n * ‖x‖

theorem NavierStokes.SlotGeometry.cover_pow_positive (n : ℕ) (x : Plane) (hx : 0 < x.1) (hy : 0 ≤ x.2) : 0 < ((cover ^ n) x).1 ∧ 0 ≤ ((cover ^ n) x).2

theorem NavierStokes.SlotGeometry.cover_pow_second_positive {n : ℕ} (hn : 0 < n) (x : Plane) (hx : 0 < x.1) (hy : 0 ≤ x.2) : 0 < ((cover ^ n) x).2

def NavierStokes.SlotGeometry.denominator (m D : ℕ) : ℝ

Denominator, given by ((m : ℝ) + 1) * (6 : ℝ) ^ D.

Equations

• NavierStokes.SlotGeometry.denominator m D = (↑m + 1) * 6 ^ D

theorem NavierStokes.SlotGeometry.denominator_pos (m D : ℕ) : 0 < denominator m D

noncomputable def NavierStokes.SlotGeometry.center (m D : ℕ) (i : Fin m) : Plane

Explicit rational centers: they lie on the horizontal line Y₂=0.

Equations

• NavierStokes.SlotGeometry.center m D i = ((↑↑i + 1) / NavierStokes.SlotGeometry.denominator m D, 0)

theorem NavierStokes.SlotGeometry.center_rational (m D : ℕ) (i : Fin m) : ∃ (a : ℚ) (b : ℚ), center m D i = (↑a, ↑b)

theorem NavierStokes.SlotGeometry.center_first_pos (m D : ℕ) (i : Fin m) : 0 < (center m D i).1

theorem NavierStokes.SlotGeometry.center_norm (m D : ℕ) (i : Fin m) : ‖center m D i‖ = (center m D i).1

theorem NavierStokes.SlotGeometry.scaled_center_lt_one (m D : ℕ) (i : Fin m) : 6 ^ D * ‖center m D i‖ < 1

theorem NavierStokes.SlotGeometry.center_injective (m D : ℕ) : Function.Injective (center m D)

def NavierStokes.SlotGeometry.lattice : Set Plane

Lattice, given by (Set.range (Int.cast : ℤ → ℝ)) ×ˢ (Set.range (Int.cast : ℤ → ℝ)).

Equations

• NavierStokes.SlotGeometry.lattice = Set.range Int.cast ×ˢ Set.range Int.cast

def NavierStokes.SlotGeometry.torusEq (x y : Plane) : Prop

Equality on the torus, stated on its universal cover.

Equations

• NavierStokes.SlotGeometry.torusEq x y = (x - y ∈ NavierStokes.SlotGeometry.lattice)

theorem NavierStokes.SlotGeometry.isClosed_lattice : IsClosed lattice

theorem NavierStokes.SlotGeometry.lattice_norm_lt_one {x : Plane} (hx : x ∈ lattice) (hn : ‖x‖ < 1) : x = 0

theorem NavierStokes.SlotGeometry.torusEq_of_unit_square {x y : Plane} (hxy : torusEq x y) (hx1 : 0 ≤ x.1) (hx2 : 0 ≤ x.2) (hy1 : 0 ≤ y.1) (hy2 : 0 ≤ y.2) (hx : ‖x‖ < 1) (hy : ‖y‖ < 1) : x = y

theorem NavierStokes.SlotGeometry.cover_center_norm_lt_one (m D : ℕ) (i : Fin m) (n : ℕ) (hn : n ≤ D) : ‖(cover ^ n) (center m D i)‖ < 1

theorem NavierStokes.SlotGeometry.centers_avoid_covering (m D : ℕ) (i j : Fin m) (n : ℕ) (hn : n ≤ D) (hij : 0 < n ∨ i ≠ j) : ¬torusEq ((cover ^ n) (center m D i)) (center m D j)

All forbidden coincidences are ruled out for the explicit centers, including self-coincidence under every positive allowed covering power.

def NavierStokes.SlotGeometry.rectangle (c : Plane) (r : ℝ) : Set Plane

Closed rectangles in the product supremum norm.

Equations

• NavierStokes.SlotGeometry.rectangle c r = {x : NavierStokes.SlotGeometry.Plane | ‖x - c‖ ≤ r}

theorem NavierStokes.SlotGeometry.exists_common_radius (m D : ℕ) : ∃ (r : ℝ), 0 < r ∧ (∀ n ≤ D, ∀ (i j : Fin m), 0 < n ∨ i ≠ j → ∀ x ∈ rectangle (center m D i) (2 * r), ∀ y ∈ rectangle (center m D j) (2 * r), ¬torusEq ((cover ^ n) x) y) ∧ ∀ n ≤ D, ∀ (i : Fin m), ∀ x ∈ rectangle (center m D i) (2 * r), ∀ y ∈ rectangle (center m D i) (2 * r), torusEq ((cover ^ n) x) ((cover ^ n) y) → x = y

A common positive radius exists for the explicit rational centers. The rectangles of radius 2*r already include fixed padding.

Distinct colors have disjoint slots at equal levels, and every positive covering difference up to D separates even equal colors. Every covering power up to D is also injective modulo the lattice on each padded slot.

theorem NavierStokes.SlotGeometry.torusEq_refl (x : Plane) : torusEq x x

theorem NavierStokes.SlotGeometry.torusEq_symm {x y : Plane} (h : torusEq x y) : torusEq y x

theorem NavierStokes.SlotGeometry.torusEq_trans {x y z : Plane} (hxy : torusEq x y) (hyz : torusEq y z) : torusEq x z

theorem NavierStokes.SlotGeometry.cover_torusEq {x y : Plane} (h : torusEq x y) : torusEq (cover x) (cover y)

The covering preserves the integer lattice and therefore torus equality.

theorem NavierStokes.SlotGeometry.cover_pow_torusEq (n : ℕ) {x y : Plane} (h : torusEq x y) : torusEq ((cover ^ n) x) ((cover ^ n) y)

def NavierStokes.SlotGeometry.liftedSupport (level : ℕ) (slot : Set Plane) : Set Plane

All periodically reindexed copies of a native slot, on the absolute lift.

Equations

• NavierStokes.SlotGeometry.liftedSupport level slot = {Y : NavierStokes.SlotGeometry.Plane | ∃ x ∈ slot, NavierStokes.SlotGeometry.torusEq ((NavierStokes.SlotGeometry.cover ^ level) Y) x}

theorem NavierStokes.SlotGeometry.liftedSupport_disjoint_of_separation (level n : ℕ) (S T : Set Plane) (hsep : ∀ x ∈ S, ∀ y ∈ T, ¬torusEq ((cover ^ n) x) y) : Disjoint (liftedSupport level S) (liftedSupport (level + n) T)

theorem NavierStokes.SlotGeometry.exists_disjoint_lifted_slots (m D : ℕ) : ∃ (r : ℝ), 0 < r ∧ ∀ (level n : ℕ), n ≤ D → ∀ (i j : Fin m), 0 < n ∨ i ≠ j → Disjoint (liftedSupport level (rectangle (center m D i) (2 * r))) (liftedSupport (level + n) (rectangle (center m D j) (2 * r)))

The padded native slots are disjoint on the actual absolute lift, at arbitrary levels whose difference is at most D.

def NavierStokes.SlotGeometry.orientedRectangle (c a b : Plane) (r : ℝ) : Set Plane

A rectangle in any two prescribed auxiliary directions.

Equations

• NavierStokes.SlotGeometry.orientedRectangle c a b r = {x : NavierStokes.SlotGeometry.Plane | ∃ (ξ : ℝ) (η : ℝ), |ξ| ≤ r ∧ |η| ≤ r ∧ x = c + ξ • a + η • b}

theorem NavierStokes.SlotGeometry.orientedRectangle_subset (c a b : Plane) (r : ℝ) (hr : 0 ≤ r) : orientedRectangle c a b (r / (1 + ‖a‖ + ‖b‖)) ⊆ rectangle c r

theorem NavierStokes.SlotGeometry.exists_oriented_slots (m D : ℕ) (a b : Plane) : ∃ (r : ℝ), 0 < r ∧ (∀ (level n : ℕ), n ≤ D → ∀ (i j : Fin m), 0 < n ∨ i ≠ j → Disjoint (liftedSupport level (orientedRectangle (center m D i) a b (2 * r))) (liftedSupport (level + n) (orientedRectangle (center m D j) a b (2 * r)))) ∧ ∀ n ≤ D, ∀ (i : Fin m), ∀ x ∈ orientedRectangle (center m D i) a b (2 * r), ∀ y ∈ orientedRectangle (center m D i) a b (2 * r), torusEq ((cover ^ n) x) ((cover ^ n) y) → x = y

In particular this applies to the manuscript's two eigendirections. The same coordinate radius works for all colors, levels, and padded slots.

theorem NavierStokes.SlotGeometry.rotated_axes_injective (β : ℝ) : Function.Injective fun (q : Plane) => q.1 • (1, -β) + q.2 • (β, 1)

The manuscript's axes are (1,-β) and (β,1), with β=sqrt(2)-1. They define genuine coordinates for every real β.

theorem NavierStokes.SlotGeometry.colored_labels_have_slots {Label : Type u_1} (m D : ℕ) (a b : Plane) (Adj : Label → Label → Prop) (color : Label → Fin m) (level : Label → ℕ) (hcolor : ∀ (i j : Label), Adj i j → color i ≠ color j) (hlevel : ∀ (i j : Label), Adj i j → level i ≤ level j + D ∧ level j ≤ level i + D) : ∃ (r : ℝ), 0 < r ∧ ∀ (i j : Label), Adj i j → Disjoint (liftedSupport (level i) (orientedRectangle (center m D (color i)) a b (2 * r))) (liftedSupport (level j) (orientedRectangle (center m D (color j)) a b (2 * r)))

Application to any label family with a finite proper coloring and a bounded difference of interacting levels. Constructing that coloring from the physical grid is a separate combinatorial obligation.