Exact core and carrier scaling

Real-power identities and the integer-frequency estimate in Appendix A, Proposition A.2 and Remark 8.6 of the candidate manuscript. These are scalar scaling facts; they do not supply a Navier--Stokes solution or analytic estimates for its profiles. The arbitrary envelope is kept in the carrier Reynolds product.

noncomputable def NavierStokes.Scaling.coreVelocity (q h : ℝ) : ℝ

The core velocity scale, with the fixed profile coefficient omitted.

Equations

• NavierStokes.Scaling.coreVelocity q h = q ^ (-(1 / 2 + h))

noncomputable def NavierStokes.Scaling.radialLength (q : ℝ) : ℝ

The radial length scale.

Equations

• NavierStokes.Scaling.radialLength q = q ^ (1 / 2)

noncomputable def NavierStokes.Scaling.axialLength (q h : ℝ) : ℝ

The axial length scale.

Equations

• NavierStokes.Scaling.axialLength q h = q ^ (1 / 2 - h)

def NavierStokes.Scaling.reynolds (velocity length : ℝ) : ℝ

Reynolds number at physical viscosity one.

Equations

• NavierStokes.Scaling.reynolds velocity length = velocity * length

theorem NavierStokes.Scaling.core_radial_reynolds {q : ℝ} (hq : 0 < q) (h : ℝ) : reynolds (coreVelocity q h) (radialLength q) = q ^ (-h)

theorem NavierStokes.Scaling.core_axial_reynolds {q : ℝ} (hq : 0 < q) (h : ℝ) : reynolds (coreVelocity q h) (axialLength q h) = q ^ (-2 * h)

theorem NavierStokes.Scaling.normalized_viscosity {Q : ℝ} (hQ : 0 < Q) (h : ℝ) : Q ^ (-(1 / 2 + h) - 1) / Q ^ (-2 * (1 / 2 + h) - 1 / 2) = Q ^ h

Dividing the diffusion scale by the inertial scale yields Q ^ h.

theorem NavierStokes.Scaling.sqrt_viscosity {Q : ℝ} (hQ : 0 < Q) (h : ℝ) : √(Q ^ h) = Q ^ (h / 2)

theorem NavierStokes.Scaling.wave_amplitude_power {Q : ℝ} (hQ : 0 < Q) (h : ℝ) : coreVelocity Q h * √(Q ^ h) = Q ^ (-1 / 2 - h / 2)

The physical amplitude prefactor of the primary wave.

theorem NavierStokes.Scaling.wave_length_power {Q : ℝ} (hQ : 0 < Q) (h : ℝ) : radialLength Q * √(Q ^ h) = Q ^ (1 / 2 + h / 2)

The continuum wavelength scale, before rounding the frequency.

theorem NavierStokes.Scaling.wave_power_cancellation {Q : ℝ} (hQ : 0 < Q) (h : ℝ) : Q ^ (-1 / 2 - h / 2) * Q ^ (1 / 2 + h / 2) = 1

noncomputable def NavierStokes.Scaling.carrierFrequency (ε : ℝ) : ℕ

The integer carrier frequency is the natural ceiling of ε ^ (-1/2).

Equations

• NavierStokes.Scaling.carrierFrequency ε = ⌈ε ^ (-(1 / 2))⌉₊

theorem NavierStokes.Scaling.inverse_sqrt_power {ε : ℝ} (hε : 0 < ε) : ε ^ (-(1 / 2)) = (√ε)⁻¹

theorem NavierStokes.Scaling.carrier_frequency_sqrt_bounds {ε : ℝ} (hε : 0 < ε) : 1 ≤ ↑(carrierFrequency ε) * √ε ∧ ↑(carrierFrequency ε) * √ε ≤ 1 + √ε

Integer rounding changes k √ε by at most √ε.

theorem NavierStokes.Scaling.carrier_frequency_pos {ε : ℝ} (hε : 0 < ε) : 0 < ↑(carrierFrequency ε)

theorem NavierStokes.Scaling.carrier_viscosity_bounds {ε : ℝ} (hε : 0 < ε) : 1 ≤ ε * ↑(carrierFrequency ε) ^ 2 ∧ ε * ↑(carrierFrequency ε) ^ 2 ≤ (1 + √ε) ^ 2

The lower and upper viscosity bounds include the integer ceiling error.

theorem NavierStokes.Scaling.one_add_sqrt_sq_le_four {ε : ℝ} (hε₁ : ε ≤ 1) : (1 + √ε) ^ 2 ≤ 4

theorem NavierStokes.Scaling.order_one_viscosity {ε : ℝ} (hε : 0 < ε) (hε₁ : ε ≤ 1) : 1 ≤ ε * ↑(carrierFrequency ε) ^ 2 ∧ ε * ↑(carrierFrequency ε) ^ 2 ≤ (1 + √ε) ^ 2 ∧ (1 + √ε) ^ 2 ≤ 4

The manuscript's complete inequality, for 0 < ε ≤ 1.

theorem NavierStokes.Scaling.reciprocal_frequency_bounds {ε : ℝ} (hε : 0 < ε) (hε₁ : ε ≤ 1) : √ε / 2 ≤ 1 / ↑(carrierFrequency ε) ∧ 1 / ↑(carrierFrequency ε) ≤ √ε

noncomputable def NavierStokes.Scaling.waveLength (Q h : ℝ) : ℝ

The physical wavelength with the actual integer carrier frequency.

Equations

• NavierStokes.Scaling.waveLength Q h = NavierStokes.Scaling.radialLength Q / ↑(NavierStokes.Scaling.carrierFrequency (Q ^ h))

theorem NavierStokes.Scaling.wave_length_bounds {Q h : ℝ} (hQ : 0 < Q) (hε : Q ^ h ≤ 1) : Q ^ (1 / 2 + h / 2) / 2 ≤ waveLength Q h ∧ waveLength Q h ≤ Q ^ (1 / 2 + h / 2)

Integer rounding changes the nominal wavelength by a factor in [1/2,1].

noncomputable def NavierStokes.Scaling.waveVelocity (Q h envelope : ℝ) : ℝ

The primary velocity includes an arbitrary real envelope coefficient.

Equations

• NavierStokes.Scaling.waveVelocity Q h envelope = NavierStokes.Scaling.coreVelocity Q h * √(Q ^ h) * envelope

theorem NavierStokes.Scaling.wave_reynolds_exact {Q : ℝ} (hQ : 0 < Q) (h envelope : ℝ) : reynolds (waveVelocity Q h envelope) (waveLength Q h) = envelope / (↑(carrierFrequency (Q ^ h)) * √(Q ^ h))

Exact cancellation leaves the envelope and a bounded rounding factor.

theorem NavierStokes.Scaling.wave_reynolds_bounds {Q h envelope : ℝ} (hQ : 0 < Q) (hε : Q ^ h ≤ 1) (he : 0 ≤ envelope) : envelope / 2 ≤ reynolds (waveVelocity Q h envelope) (waveLength Q h) ∧ reynolds (waveVelocity Q h envelope) (waveLength Q h) ≤ envelope

A positive envelope gives quantitative bounds with no extra power of Q.

theorem NavierStokes.Scaling.wave_reynolds_zero_envelope (Q h : ℝ) : reynolds (waveVelocity Q h 0) (waveLength Q h) = 0

The scaling computation does not imply a lower bound at envelope zeros.