Coherence of the constructed primary waves

The phase, coefficient, cutoff, and chart in this file are the actual CorrectionInitialization.ActualPrimary constructors. Their differentiated curl correction and Gaussian term are transported on the whole free lift.

theorem NavierStokes.ActualPrimaryCoherence.phaseNormal_equiv {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E ≃L[ℝ] F) {l : ℝ} (hl : l ≠ 0) (r : E → ℝ) (R : F → ℝ) (Sr St Sz : E → E) (Vr Vt Vz : F → F) (hr : ∀ (x : E), R (e x) = l * r x) (hDr : ∀ (x : E), e (Sr x) = l • Vr (e x)) (hDt : ∀ (x : E), e (St x) = Vt (e x)) (hDz : ∀ (x : E), e (Sz x) = l • Vz (e x)) (b : ℝ) (Φ : F → ℝ) (x : E) : HarmonicCalculus.phaseNormal r Sr St Sz (fun (y : E) => b * Φ (e y)) x = (b * l) • HarmonicCalculus.phaseNormal R Vr Vt Vz Φ (e x)

An invertible chart transports the actual derivative, including at points where Lean's derivative is defined to be zero.

theorem NavierStokes.ActualPrimaryCoherence.cylindricalCurl_equiv {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E ≃L[ℝ] F) {l : ℝ} (hl : l ≠ 0) (r : E → ℝ) (R : F → ℝ) (Sr St Sz : E → E) (Vr Vt Vz : F → F) (hr : ∀ (x : E), R (e x) = l * r x) (hDr : ∀ (x : E), e (Sr x) = l • Vr (e x)) (hDt : ∀ (x : E), e (St x) = Vt (e x)) (hDz : ∀ (x : E), e (Sz x) = l • Vz (e x)) (c : ℝ) (a : F → HarmonicCalculus.ComplexVector) (x : E) : CurlClassBounds.cylindricalCurl r Sr St Sz (fun (y : E) => c • a (e y)) x = (c * l) • CurlClassBounds.cylindricalCurl R Vr Vt Vz a (e x)

theorem NavierStokes.ActualPrimaryCoherence.realizedCoefficient_equiv {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E ≃L[ℝ] F) {l b K L : ℝ} (hl : l ≠ 0) (hb : b ≠ 0) (hK : K ≠ 0) (hKL : K * b = L) (r : E → ℝ) (R : F → ℝ) (Sr St Sz : E → E) (Vr Vt Vz : F → F) (hr : ∀ (x : E), R (e x) = l * r x) (hDr : ∀ (x : E), e (Sr x) = l • Vr (e x)) (hDt : ∀ (x : E), e (St x) = Vt (e x)) (hDz : ∀ (x : E), e (Sz x) = l • Vz (e x)) (c : ℝ) (Φ : F → ℝ) (a : F → HarmonicCalculus.ComplexVector) (x : E) : CurlClassBounds.realizedCoefficient K r Sr St Sz (fun (y : E) => b * Φ (e y)) (fun (y : E) => c • a (e y)) x = c • CurlClassBounds.realizedCoefficient L R Vr Vt Vz Φ a (e x)

The literal absolute chart and its directions

@[reducible, inline]

abbrev NavierStokes.ActualPrimaryCoherence.ChartPoint : Type

Chart point: an abbreviation for LocalSignedRequest.Point × ℝ.

Equations

• NavierStokes.ActualPrimaryCoherence.ChartPoint = (NavierStokes.LocalSignedRequest.Point × ℝ)

@[reducible, inline]

abbrev NavierStokes.ActualPrimaryCoherence.Absolute : Type

Absolute: an abbreviation for AbsolutePoint × ℝ.

Equations

• NavierStokes.ActualPrimaryCoherence.Absolute = (NavierStokes.CorrectionInitialization.ActualPrimary.AbsolutePoint × ℝ)

noncomputable def NavierStokes.ActualPrimaryCoherence.absoluteChart (n : ℕ) : ChartPoint ≃L[ℝ] Absolute

Absolute chart, bundling toFun, invFun, left_inv, right_inv and the required compatibility proofs.

Equations

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

@[simp]

theorem NavierStokes.ActualPrimaryCoherence.absoluteChart_apply (n : ℕ) (x : ChartPoint) : (absoluteChart n) x = (CorrectionInitialization.ActualPrimary.toAbsolute n x.1, x.2)

@[simp]

theorem NavierStokes.ActualPrimaryCoherence.absoluteChart_symm_apply (n : ℕ) (x : Absolute) : (absoluteChart n).symm x = (CorrectionInitialization.ActualPrimary.fromAbsolute n x.1, x.2)

noncomputable def NavierStokes.ActualPrimaryCoherence.absoluteRadius (x : Absolute) : ℝ

Absolute radius, given by x.1.1.1.

Equations

• NavierStokes.ActualPrimaryCoherence.absoluteRadius x = x.1.1.1

noncomputable def NavierStokes.ActualPrimaryCoherence.absoluteRadial (x : Absolute) : Absolute

Absolute radial, given by (((1,(0,0)), RadialPullback.radialJacobian (ChartScales.radialExponent h) x.1.1.1 • radialVector), 0).

Equations

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

noncomputable def NavierStokes.ActualPrimaryCoherence.absoluteAxial : Absolute → Absolute

Absolute axial, given by (((0,(1,0)),0),0).

Equations

• NavierStokes.ActualPrimaryCoherence.absoluteAxial x✝ = (((0, 1, 0), 0), 0)

noncomputable def NavierStokes.ActualPrimaryCoherence.absoluteAngular : Absolute → Absolute

Absolute angular, given by (0,1).

Equations

• NavierStokes.ActualPrimaryCoherence.absoluteAngular x✝ = (0, 1)

noncomputable def NavierStokes.ActualPrimaryCoherence.absoluteFast : Absolute → Absolute

Absolute fast, given by (((0,(0,0)),temporalVector),0).

Equations

• NavierStokes.ActualPrimaryCoherence.absoluteFast x✝ = (((0, 0, 0), NavierStokes.CorrectionInitialization.ActualPrimary.temporalVector), 0)

theorem NavierStokes.ActualPrimaryCoherence.cover_inverse_radial (i : ℕ) (a : ℝ) : (CommonCoverSolve.coverPower i).symm ((ChartScales.Lambda ^ i * a) • CorrectionInitialization.ActualPrimary.radialVector) = a • CorrectionInitialization.ActualPrimary.radialVector

theorem NavierStokes.ActualPrimaryCoherence.cover_inverse_temporal (i : ℕ) (a : ℝ) : (CommonCoverSolve.coverPower i).symm ((ChartScales.Tg ^ i * a) • CorrectionInitialization.ActualPrimary.temporalVector) = a • CorrectionInitialization.ActualPrimary.temporalVector

theorem NavierStokes.ActualPrimaryCoherence.sqrt_radialJacobian {q : ℝ} (hq : 0 < q) (d R : ℝ) : q ^ (d / 2) * RadialPullback.radialJacobian d R = √q * RadialPullback.radialJacobian d (√q * R)

theorem NavierStokes.ActualPrimaryCoherence.absoluteChart_radius (n : ℕ) (x : ChartPoint) : absoluteRadius ((absoluteChart n) x) = √(ChartScales.Q n) * x.1.1

theorem NavierStokes.ActualPrimaryCoherence.absoluteChart_radial (B n : ℕ) (x : ChartPoint) : (absoluteChart n) ((PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).radialField n x) = √(ChartScales.Q n) • absoluteRadial ((absoluteChart n) x)

theorem NavierStokes.ActualPrimaryCoherence.absoluteChart_axial (B n : ℕ) (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (x : ChartPoint) : (absoluteChart n) ((PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).axialField (HarmonicWaveInteraction.productStrip (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal U)) n x) = √(ChartScales.Q n) • absoluteAxial ((absoluteChart n) x)

theorem NavierStokes.ActualPrimaryCoherence.absoluteChart_angular (B n : ℕ) (x : ChartPoint) : (absoluteChart n) (PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).angular = absoluteAngular ((absoluteChart n) x)

theorem NavierStokes.ActualPrimaryCoherence.absoluteChart_fast (B n : ℕ) (x : ChartPoint) : (absoluteChart n) ((PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).fastField n x) = ChartScales.Q n ^ (1 + CorrectionInitialization.ActualPrimary.h) • absoluteFast ((absoluteChart n) x)

The actual cut coefficient, corrected wave, and Gaussian field

noncomputable def NavierStokes.ActualPrimaryCoherence.absoluteCutAmplitude {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (x : Absolute) : HarmonicCalculus.ComplexVector

Absolute cut amplitude, given by periodicGaussian j L x.1.2 • absoluteAmplitude j L x.1.

Equations

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

noncomputable def NavierStokes.ActualPrimaryCoherence.absoluteExactAmplitude {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : Absolute → HarmonicCalculus.ComplexVector

Absolute exact amplitude, constructed using CurlClassBounds.realizedCoefficient.

Equations

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

noncomputable def NavierStokes.ActualPrimaryCoherence.absoluteVelocity {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (x : Absolute) : Fin 3 → ℝ

Absolute velocity, defined pointwise by (vectorMode 1 (absolutePhase j L) (absoluteExactAmplitude j L) x i).re.

Equations

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

noncomputable def NavierStokes.ActualPrimaryCoherence.absoluteGaussianCoefficient {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (x : Absolute) : HarmonicCalculus.ComplexVector

Absolute gaussian coefficient, given by along absoluteFast (fun y => periodicGaussian j L y.1.2) x • absoluteAmplitude j L x.1.

Equations

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

noncomputable def NavierStokes.ActualPrimaryCoherence.absoluteGaussian {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (x : Absolute) : Fin 3 → ℝ

Absolute gaussian, defined pointwise by (vectorMode 1 (absolutePhase j L) (absoluteGaussianCoefficient j L) x i).re.

Equations

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

theorem NavierStokes.ActualPrimaryCoherence.cutAmplitude_representation {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).withCutoff (CorrectionInitialization.ActualPrimary.chartCutoff j L)).amplitude n = fun (x : ChartPoint) => ChartScales.Q n ^ CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h • absoluteCutAmplitude j L ((absoluteChart n) x)

theorem NavierStokes.ActualPrimaryCoherence.phase_representation {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : (CorrectionInitialization.ActualPrimary.chartCoefficients j L).phase n = fun (x : ChartPoint) => 1 / ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n) * CorrectionInitialization.ActualPrimary.absolutePhase j L ((absoluteChart n) x)

theorem NavierStokes.ActualPrimaryCoherence.exactAmplitude_representation {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (x : ChartPoint) : (CorrectionInitialization.ActualPrimary.piece U j L).exactCoefficients.amplitude n x = ChartScales.Q n ^ CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h • absoluteExactAmplitude j L ((absoluteChart n) x)

Full-fiber transport of the coefficient actually used by the iteration. No equality of corrected fields, nor a tangency assertion, is an input.

theorem NavierStokes.ActualPrimaryCoherence.piece_velocity_representation {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (x : ChartPoint) : (CorrectionInitialization.ActualPrimary.piece U j L).velocity n x = ChartScales.Q n ^ CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h • absoluteVelocity j L ((absoluteChart n) x)

theorem NavierStokes.ActualPrimaryCoherence.gaussianCoefficient_representation {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (x : ChartPoint) : LinearWaveBounds.excludedSlotError (CorrectionInitialization.ActualPrimary.piece U j L).directions (CorrectionInitialization.ActualPrimary.piece U j L).cutoff (CorrectionInitialization.ActualPrimary.piece U j L).coefficients.amplitude 0 n x = ChartScales.Q n ^ (2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h + 1 / 2) • absoluteGaussianCoefficient j L ((absoluteChart n) x)

theorem NavierStokes.ActualPrimaryCoherence.piece_excluded_representation {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (x : ChartPoint) : (CorrectionInitialization.ActualPrimary.piece U j L).excluded n x = ChartScales.Q n ^ (2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h + 1 / 2) • absoluteGaussian j L ((absoluteChart n) x)

Exact comparison of two genuine common-cover bands

theorem NavierStokes.ActualPrimaryCoherence.band_power_cancel (n m : ℕ) (a : ℝ) : ChartScales.Q m ^ a * (ChartScales.Q n / ChartScales.Q m) ^ a = ChartScales.Q n ^ a

theorem NavierStokes.ActualPrimaryCoherence.toAbsolute_bandChart (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (x : LocalSignedRequest.Point) : CorrectionInitialization.ActualPrimary.toAbsolute m ((GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) x) = CorrectionInitialization.ActualPrimary.toAbsolute n x

theorem NavierStokes.ActualPrimaryCoherence.piece_velocity_band {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (x : ChartPoint) : (CorrectionInitialization.ActualPrimary.piece U j L).velocity n x = GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m • (CorrectionInitialization.ActualPrimary.piece U j L).velocity m ((GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) x.1, x.2)

theorem NavierStokes.ActualPrimaryCoherence.band_pressure_cancel (n m : ℕ) : GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m * GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m * ChartScales.Q m ^ (2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) = ChartScales.Q n ^ (2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h)

theorem NavierStokes.ActualPrimaryCoherence.band_source_cancel (n m : ℕ) : GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m * GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m * GaugeStateCoherence.bandScale n m * ChartScales.Q m ^ (2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h + 1 / 2) = ChartScales.Q n ^ (2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h + 1 / 2)

theorem NavierStokes.ActualPrimaryCoherence.piece_pressure_band {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (x : ChartPoint) : (CorrectionInitialization.ActualPrimary.piece U j L).pressure n x = GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m * GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m * (CorrectionInitialization.ActualPrimary.piece U j L).pressure m ((GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) x.1, x.2)

theorem NavierStokes.ActualPrimaryCoherence.piece_excluded_band {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (x : ChartPoint) : (CorrectionInitialization.ActualPrimary.piece U j L).excluded n x = (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m * GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m * GaugeStateCoherence.bandScale n m) • (CorrectionInitialization.ActualPrimary.piece U j L).excluded m ((GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) x.1, x.2)

Ordinary regularity before restricting to a bounded strip

noncomputable def NavierStokes.ActualPrimaryCoherence.positiveChart : Set ChartPoint

Positive chart, given by {x | 0 < x.1.2.1.1}.

Equations

• NavierStokes.ActualPrimaryCoherence.positiveChart = {x : NavierStokes.ActualPrimaryCoherence.ChartPoint | 0 < x.1.2.1.1}

noncomputable def NavierStokes.ActualPrimaryCoherence.positiveRadialChart : Set ChartPoint

Positive radial chart, given by {x | 0 < x.1.1 ∧ 0 < x.1.2.1.1}.

Equations

• NavierStokes.ActualPrimaryCoherence.positiveRadialChart = {x : NavierStokes.ActualPrimaryCoherence.ChartPoint | 0 < x.1.1 ∧ 0 < x.1.2.1.1}

noncomputable def NavierStokes.ActualPrimaryCoherence.positiveAbsolute : Set Absolute

Positive absolute, given by {x | 0 < x.1.1.2.2}.

Equations

• NavierStokes.ActualPrimaryCoherence.positiveAbsolute = {x : NavierStokes.ActualPrimaryCoherence.Absolute | 0 < x.1.1.2.2}

noncomputable def NavierStokes.ActualPrimaryCoherence.positiveRadialAbsolute : Set Absolute

Positive radial absolute, given by {x | 0 < x.1.1.1 ∧ 0 < x.1.1.2.2}.

Equations

• NavierStokes.ActualPrimaryCoherence.positiveRadialAbsolute = {x : NavierStokes.ActualPrimaryCoherence.Absolute | 0 < x.1.1.1 ∧ 0 < x.1.1.2.2}

theorem NavierStokes.ActualPrimaryCoherence.positiveChart_open : IsOpen positiveChart

theorem NavierStokes.ActualPrimaryCoherence.positiveRadialChart_open : IsOpen positiveRadialChart

theorem NavierStokes.ActualPrimaryCoherence.positiveAbsolute_open : IsOpen positiveAbsolute

theorem NavierStokes.ActualPrimaryCoherence.positiveRadialAbsolute_open : IsOpen positiveRadialAbsolute

theorem NavierStokes.ActualPrimaryCoherence.frequencySlow_smoothAt (B n : ℕ) {p : PhaseCalculus.Slow} (hR : 0 < p.1) (hT : 0 < p.2.2) : ContDiffAt ℝ (↑⊤) (BaseContextAssembly.frequencySlow CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B n) p

theorem NavierStokes.ActualPrimaryCoherence.axialSlow_smoothAt (B n : ℕ) {p : PhaseCalculus.Slow} (hT : 0 < p.2.2) : ContDiffAt ℝ (↑⊤) (BaseContextAssembly.axialSlow CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B n) p

theorem NavierStokes.ActualPrimaryCoherence.absoluteAmplitude_smooth {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : ContDiffOn ℝ (↑⊤) (fun (x : Absolute) => CorrectionInitialization.ActualPrimary.absoluteAmplitude j L x.1) positiveAbsolute

theorem NavierStokes.ActualPrimaryCoherence.absolutePressureCoefficient_smooth {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : ContDiffOn ℝ (↑⊤) (fun (x : Absolute) => CorrectionInitialization.ActualPrimary.absolutePressure j L x.1) positiveAbsolute

theorem NavierStokes.ActualPrimaryCoherence.absoluteCutoff_smooth {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : ContDiff ℝ ↑⊤ fun (x : Absolute) => CorrectionInitialization.ActualPrimary.periodicGaussian j L x.1.2

theorem NavierStokes.ActualPrimaryCoherence.absoluteCutAmplitude_smooth {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : ContDiffOn ℝ (↑⊤) (absoluteCutAmplitude j L) positiveAbsolute

theorem NavierStokes.ActualPrimaryCoherence.absolutePhase_smooth {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : ContDiffOn ℝ (↑⊤) (CorrectionInitialization.ActualPrimary.absolutePhase j L) positiveRadialAbsolute

theorem NavierStokes.ActualPrimaryCoherence.absoluteRadial_smooth : ContDiffOn ℝ (↑⊤) absoluteRadial positiveRadialAbsolute

noncomputable def NavierStokes.ActualPrimaryCoherence.absoluteNormal {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : Absolute → ProblemStatement.Space

Absolute normal, given by phaseNormal absoluteRadius absoluteRadial absoluteAngular absoluteAxial (absolutePhase j L).

Equations

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

theorem NavierStokes.ActualPrimaryCoherence.absoluteNormal_smooth {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : ContDiffOn ℝ (↑⊤) (absoluteNormal j L) positiveRadialAbsolute

theorem NavierStokes.ActualPrimaryCoherence.absolutePhase_angular {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : CopyAngularInvariance.AffinePhase (0, 1) (↑(PrimaryGeometryAssembly.angularMode CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared j L)) (CorrectionInitialization.ActualPrimary.absolutePhase j L)

theorem NavierStokes.ActualPrimaryCoherence.absoluteNormal_ne {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) {x : Absolute} (hx : x ∈ positiveRadialAbsolute) : absoluteNormal j L x ≠ 0

theorem NavierStokes.ActualPrimaryCoherence.absoluteExactAmplitude_smooth {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : ContDiffOn ℝ (↑⊤) (absoluteExactAmplitude j L) positiveRadialAbsolute

theorem NavierStokes.ActualPrimaryCoherence.absoluteVelocity_smooth_radial {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : ContDiffOn ℝ (↑⊤) (absoluteVelocity j L) positiveRadialAbsolute

noncomputable def NavierStokes.ActualPrimaryCoherence.amplitudeRadius {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) (x : Absolute) : ℝ

Amplitude radius, given by PrimaryTargetBounds.profileRadius h (nativeSlow L x.1).

Equations

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

theorem NavierStokes.ActualPrimaryCoherence.amplitudeRadius_smoothAt {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) {x : Absolute} (hx : x ∈ positiveAbsolute) : ContDiffAt ℝ (↑⊤) (amplitudeRadius L) x

theorem NavierStokes.ActualPrimaryCoherence.absoluteAmplitude_zero_outside {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (x : Absolute) (hx : amplitudeRadius L x ∉ Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)) : CorrectionInitialization.ActualPrimary.absoluteAmplitude j L x.1 = 0

theorem NavierStokes.ActualPrimaryCoherence.absolutePressure_zero_outside {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (x : Absolute) (hx : amplitudeRadius L x ∉ Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)) : CorrectionInitialization.ActualPrimary.absolutePressure j L x.1 = 0

theorem NavierStokes.ActualPrimaryCoherence.absolutePair_zero_germ_outside {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) {x : Absolute} (hT : x ∈ positiveAbsolute) (hx : amplitudeRadius L x ∉ Set.Icc (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)) : ((fun (y : Absolute) => CorrectionInitialization.ActualPrimary.absoluteAmplitude j L y.1) =ᶠ[nhds x] fun (x : Absolute) => 0) ∧ (fun (y : Absolute) => CorrectionInitialization.ActualPrimary.absolutePressure j L y.1) =ᶠ[nhds x] fun (x : Absolute) => 0

theorem NavierStokes.ActualPrimaryCoherence.absoluteVelocity_tsupport {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : tsupport (absoluteVelocity j L) ⊆ tsupport (absoluteCutAmplitude j L)

theorem NavierStokes.ActualPrimaryCoherence.absoluteVelocity_zero_germ_outside {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) {x : Absolute} (hT : x ∈ positiveAbsolute) (hx : amplitudeRadius L x ∉ Set.Icc (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)) : absoluteVelocity j L =ᶠ[nhds x] fun (x : Absolute) => 0

theorem NavierStokes.ActualPrimaryCoherence.amplitudeRadius_nonpositive {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) {x : Absolute} (hx : x.1.1.1 ≤ 0) : amplitudeRadius L x ≤ 0

theorem NavierStokes.ActualPrimaryCoherence.amplitudeRadius_outside_nonpositive {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) {x : Absolute} (hx : x.1.1.1 ≤ 0) : amplitudeRadius L x ∉ Set.Icc (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)

theorem NavierStokes.ActualPrimaryCoherence.absoluteVelocity_smooth {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : ContDiffOn ℝ (↑⊤) (absoluteVelocity j L) positiveAbsolute

theorem NavierStokes.ActualPrimaryCoherence.absolutePressureMode_smooth {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : ContDiffOn ℝ (↑⊤) (CorrectionInitialization.ActualPrimary.absolutePressureMode j L) positiveAbsolute

theorem NavierStokes.ActualPrimaryCoherence.piece_velocity_smooth {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : ContDiffOn ℝ (↑⊤) ((CorrectionInitialization.ActualPrimary.piece U j L).velocity n) positiveChart

theorem NavierStokes.ActualPrimaryCoherence.piece_pressure_smooth {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : ContDiffOn ℝ (↑⊤) ((CorrectionInitialization.ActualPrimary.piece U j L).pressure n) positiveChart

theorem NavierStokes.ActualPrimaryCoherence.absoluteTangent_smooth {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : ContDiffOn ℝ (↑⊤) (CorrectionInitialization.ActualPrimary.absoluteTangent j L) positiveAbsolute

theorem NavierStokes.ActualPrimaryCoherence.piece_tangentVelocity_smooth {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : ContDiffOn ℝ (↑⊤) ((CorrectionInitialization.ActualPrimary.piece U j L).tangentVelocity n) positiveChart

theorem NavierStokes.ActualPrimaryCoherence.absoluteGaussianCoefficient_smooth {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : ContDiffOn ℝ (↑⊤) (absoluteGaussianCoefficient j L) positiveAbsolute

theorem NavierStokes.ActualPrimaryCoherence.absoluteGaussian_smooth {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : ContDiffOn ℝ (↑⊤) (absoluteGaussian j L) positiveAbsolute

theorem NavierStokes.ActualPrimaryCoherence.piece_excluded_smooth {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : ContDiffOn ℝ (↑⊤) ((CorrectionInitialization.ActualPrimary.piece U j L).excluded n) positiveChart

theorem NavierStokes.ActualPrimaryCoherence.amplitudeRadius_chart {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) {x : ChartPoint} (hT : 0 < x.1.2.1.1) (hR : 0 < x.1.1) : amplitudeRadius L ((absoluteChart n) x) = x.1.1 / VariableGaugeMean.qLength (2 * CorrectionInitialization.ActualPrimary.h) x.1.2.1

theorem NavierStokes.ActualPrimaryCoherence.piece_velocity_zero_germ_nonpositive {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) {x : ChartPoint} (hT : 0 < x.1.2.1.1) (hR : x.1.1 ≤ 0) : (CorrectionInitialization.ActualPrimary.piece U j L).velocity n =ᶠ[nhds x] fun (x : ChartPoint) => 0

theorem NavierStokes.ActualPrimaryCoherence.piece_velocity_support {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) {x : ChartPoint} (hT : 0 < x.1.2.1.1) (hne : (CorrectionInitialization.ActualPrimary.piece U j L).velocity n x ≠ 0) : x.1.1 ∈ Set.Icc (VariableGaugeMean.qLength (2 * CorrectionInitialization.ActualPrimary.h) x.1.2.1 * PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (VariableGaugeMean.qLength (2 * CorrectionInitialization.ActualPrimary.h) x.1.2.1 * PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)

Periodicity on the genuine common covers

theorem NavierStokes.ActualPrimaryCoherence.along_translate {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (w : E) {f : E → F} {V : E → E} (hf : ∀ (x : E), f (x + w) = f x) (hV : ∀ (x : E), V (x + w) = V x) (x : E) : HarmonicCalculus.along V f (x + w) = HarmonicCalculus.along V f x

theorem NavierStokes.ActualPrimaryCoherence.phaseNormal_translate {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (w : E) {R Φ : E → ℝ} {Vr Vt Vz : E → E} (hR : ∀ (x : E), R (x + w) = R x) (hΦ : ∀ (x : E), Φ (x + w) = Φ x) (hr : ∀ (x : E), Vr (x + w) = Vr x) (ht : ∀ (x : E), Vt (x + w) = Vt x) (hz : ∀ (x : E), Vz (x + w) = Vz x) (x : E) : HarmonicCalculus.phaseNormal R Vr Vt Vz Φ (x + w) = HarmonicCalculus.phaseNormal R Vr Vt Vz Φ x

theorem NavierStokes.ActualPrimaryCoherence.cylindricalCurl_translate {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (w : E) {R : E → ℝ} {Vr Vt Vz : E → E} {a : E → HarmonicCalculus.ComplexVector} (hR : ∀ (x : E), R (x + w) = R x) (ha : ∀ (x : E), a (x + w) = a x) (hr : ∀ (x : E), Vr (x + w) = Vr x) (ht : ∀ (x : E), Vt (x + w) = Vt x) (hz : ∀ (x : E), Vz (x + w) = Vz x) (x : E) : CurlClassBounds.cylindricalCurl R Vr Vt Vz a (x + w) = CurlClassBounds.cylindricalCurl R Vr Vt Vz a x

theorem NavierStokes.ActualPrimaryCoherence.realizedCoefficient_translate {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (w : E) (K : ℝ) {R Φ : E → ℝ} {Vr Vt Vz : E → E} {a : E → HarmonicCalculus.ComplexVector} (hR : ∀ (x : E), R (x + w) = R x) (hΦ : ∀ (x : E), Φ (x + w) = Φ x) (ha : ∀ (x : E), a (x + w) = a x) (hr : ∀ (x : E), Vr (x + w) = Vr x) (ht : ∀ (x : E), Vt (x + w) = Vt x) (hz : ∀ (x : E), Vz (x + w) = Vz x) (x : E) : CurlClassBounds.realizedCoefficient K R Vr Vt Vz Φ a (x + w) = CurlClassBounds.realizedCoefficient K R Vr Vt Vz Φ a x

noncomputable def NavierStokes.ActualPrimaryCoherence.chartDeck (k : TorusInverse.Frequency) : ChartPoint

Chart deck, given by ((0, ((0,0), TorusAverages.latticePoint k)),0).

Equations

• NavierStokes.ActualPrimaryCoherence.chartDeck k = ((0, (0, 0), NavierStokes.TorusAverages.latticePoint k), 0)

theorem NavierStokes.ActualPrimaryCoherence.native_copy_sum_periodic {B N0 : ℕ} {E : Type} [NormedAddCommGroup E] (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)) (f : TorusInverse.Plane → E) (Y : TorusInverse.Plane) (k : TorusInverse.Frequency) : ∑' (a : TorusInverse.Frequency), f ((CorrectionInitialization.ActualPrimary.geometry j L).coordinates a ((CommonCoverSolve.coverPower (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).symm (Y + TorusAverages.latticePoint k))) = ∑' (a : TorusInverse.Frequency), f ((CorrectionInitialization.ActualPrimary.geometry j L).coordinates a ((CommonCoverSolve.coverPower (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).symm Y))

theorem NavierStokes.ActualPrimaryCoherence.native_clock_periodic {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)) (Y : TorusInverse.Plane) (k : TorusInverse.Frequency) : PeriodicPhaseAssembly.periodicClock (CorrectionInitialization.ActualPrimary.geometry j L) (CorrectionInitialization.ActualPrimary.clockWindow L).cutoff ((CommonCoverSolve.coverPower (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).symm (Y + TorusAverages.latticePoint k)) = PeriodicPhaseAssembly.periodicClock (CorrectionInitialization.ActualPrimary.geometry j L) (CorrectionInitialization.ActualPrimary.clockWindow L).cutoff ((CommonCoverSolve.coverPower (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).symm Y)

theorem NavierStokes.ActualPrimaryCoherence.chart_phase_periodic {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)) (k : TorusInverse.Frequency) (x : ChartPoint) : (CorrectionInitialization.ActualPrimary.chartCoefficients j L).phase n (x + chartDeck k) = (CorrectionInitialization.ActualPrimary.chartCoefficients j L).phase n x

theorem NavierStokes.ActualPrimaryCoherence.chart_amplitude_periodic {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)) (k : TorusInverse.Frequency) (x : ChartPoint) : (CorrectionInitialization.ActualPrimary.chartCoefficients j L).amplitude n (x + chartDeck k) = (CorrectionInitialization.ActualPrimary.chartCoefficients j L).amplitude n x

theorem NavierStokes.ActualPrimaryCoherence.chart_pressure_periodic {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)) (k : TorusInverse.Frequency) (x : ChartPoint) : (CorrectionInitialization.ActualPrimary.chartCoefficients j L).pressure n (x + chartDeck k) = (CorrectionInitialization.ActualPrimary.chartCoefficients j L).pressure n x

theorem NavierStokes.ActualPrimaryCoherence.chart_cutoff_periodic {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)) (k : TorusInverse.Frequency) (x : ChartPoint) : CorrectionInitialization.ActualPrimary.chartCutoff j L n (x + chartDeck k) = CorrectionInitialization.ActualPrimary.chartCutoff j L n x

theorem NavierStokes.ActualPrimaryCoherence.chart_radial_periodic (B n : ℕ) (k : TorusInverse.Frequency) (x : ChartPoint) : (PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).radialField n (x + chartDeck k) = (PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).radialField n x

theorem NavierStokes.ActualPrimaryCoherence.piece_exactAmplitude_periodic {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)) (k : TorusInverse.Frequency) (x : ChartPoint) : (CorrectionInitialization.ActualPrimary.piece U j L).exactCoefficients.amplitude n (x + chartDeck k) = (CorrectionInitialization.ActualPrimary.piece U j L).exactCoefficients.amplitude n x

theorem NavierStokes.ActualPrimaryCoherence.piece_velocity_periodic {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)) (k : TorusInverse.Frequency) (x : ChartPoint) : (CorrectionInitialization.ActualPrimary.piece U j L).velocity n (x + chartDeck k) = (CorrectionInitialization.ActualPrimary.piece U j L).velocity n x

theorem NavierStokes.ActualPrimaryCoherence.piece_tangentVelocity_periodic {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)) (k : TorusInverse.Frequency) (x : ChartPoint) : (CorrectionInitialization.ActualPrimary.piece U j L).tangentVelocity n (x + chartDeck k) = (CorrectionInitialization.ActualPrimary.piece U j L).tangentVelocity n x

theorem NavierStokes.ActualPrimaryCoherence.piece_pressure_periodic {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)) (k : TorusInverse.Frequency) (x : ChartPoint) : (CorrectionInitialization.ActualPrimary.piece U j L).pressure n (x + chartDeck k) = (CorrectionInitialization.ActualPrimary.piece U j L).pressure n x

theorem NavierStokes.ActualPrimaryCoherence.piece_excluded_periodic {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)) (k : TorusInverse.Frequency) (x : ChartPoint) : (CorrectionInitialization.ActualPrimary.piece U j L).excluded n (x + chartDeck k) = (CorrectionInitialization.ActualPrimary.piece U j L).excluded n x

theorem NavierStokes.ActualPrimaryCoherence.radius_mem_of_amplitudeRadius_mem {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) {x : ChartPoint} (hT : 0 < x.1.2.1.1) (hm : amplitudeRadius L ((absoluteChart n) x) ∈ Set.Icc (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)) : x.1.1 ∈ Set.Icc (VariableGaugeMean.qLength (2 * CorrectionInitialization.ActualPrimary.h) x.1.2.1 * PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (VariableGaugeMean.qLength (2 * CorrectionInitialization.ActualPrimary.h) x.1.2.1 * PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)

theorem NavierStokes.ActualPrimaryCoherence.piece_pressure_support {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) {x : ChartPoint} (hT : 0 < x.1.2.1.1) (hne : (CorrectionInitialization.ActualPrimary.piece U j L).pressure n x ≠ 0) : x.1.1 ∈ Set.Icc (VariableGaugeMean.qLength (2 * CorrectionInitialization.ActualPrimary.h) x.1.2.1 * PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (VariableGaugeMean.qLength (2 * CorrectionInitialization.ActualPrimary.h) x.1.2.1 * PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)

theorem NavierStokes.ActualPrimaryCoherence.piece_excluded_support {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) {x : ChartPoint} (hT : 0 < x.1.2.1.1) (hne : (CorrectionInitialization.ActualPrimary.piece U j L).excluded n x ≠ 0) : x.1.1 ∈ Set.Icc (VariableGaugeMean.qLength (2 * CorrectionInitialization.ActualPrimary.h) x.1.2.1 * PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (VariableGaugeMean.qLength (2 * CorrectionInitialization.ActualPrimary.h) x.1.2.1 * PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)

Tangency of the actual native pulse

theorem NavierStokes.ActualPrimaryCoherence.constructed_frame_normal {ι : Type} {D : PhaseJetBounds.Domain ι PhaseCalculus.Slow} (P : PrimaryPulseBounds.PhaseConstruction D) (i : ι) {z : PhaseCalculus.Slow × ℝ} (hz : z ∈ (D.slot P.V ⋯).carrier i) : (P.frame i).normal z = P.phase.normal i z

theorem NavierStokes.ActualPrimaryCoherence.native_pulse_tangent {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) {x : ActualSignedGeometry.Native} (hx : x ∈ (ActualSignedGeometry.nativeDomain CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared).carrier L) : inner ℝ ((CorrectionInitialization.ActualPrimary.phases B N0 j).phase.normal L (x.1, x.2.2)) (CorrectionInitialization.ActualPrimary.cutVelocity j L x) = 0

theorem NavierStokes.ActualPrimaryCoherence.cutVelocity_native_mem {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) {x : ActualSignedGeometry.Native} (hT : 0 < x.1.2.2) (hr : PrimaryTargetBounds.profileRadius CorrectionInitialization.ActualPrimary.h x.1 ∈ Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)) (hne : CorrectionInitialization.ActualPrimary.cutVelocity j L x ≠ 0) : x ∈ (ActualSignedGeometry.nativeDomain CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared).carrier L

theorem NavierStokes.ActualPrimaryCoherence.cutVelocity_core {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) {x : ActualSignedGeometry.Native} (hx : CorrectionInitialization.ActualPrimary.cutVelocity j L x ≠ 0) : x.2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow L).core

theorem NavierStokes.ActualPrimaryCoherence.commonAmplitude_eq_copy {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (p : PhaseCalculus.Slow) (Y : TorusInverse.Plane) (k : TorusInverse.Frequency) (hk : CorrectionInitialization.ActualPrimary.cutVelocity j L (p, (CorrectionInitialization.ActualPrimary.geometry j L).coordinates k Y) ≠ 0) : CorrectionInitialization.ActualPrimary.commonAmplitude j L p Y = CurlClassBounds.complexify (CorrectionInitialization.ActualPrimary.cutVelocity j L (p, (CorrectionInitialization.ActualPrimary.geometry j L).coordinates k Y))

theorem NavierStokes.ActualPrimaryCoherence.chart_radial_swap (B n : ℕ) (x : ChartPoint) : PhysicalResidualTZ.swapCylinder ((PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).radialField n x) = (PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).radial (PhysicalResidualTZ.swapCylinder x)

theorem NavierStokes.ActualPrimaryCoherence.chart_axial_swap (B n : ℕ) (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (x : ChartPoint) : PhysicalResidualTZ.swapCylinder ((PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).axialField (HarmonicWaveInteraction.productStrip (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal U)) n x) = (PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).axial (PhysicalResidualTZ.swapCylinder x)

theorem NavierStokes.ActualPrimaryCoherence.chart_normal_view {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)) (x : ChartPoint) : (CorrectionInitialization.ActualPrimary.chartCoefficients j L).normal (CorrectionInitialization.ActualPrimary.piece U j L).strip (CorrectionInitialization.ActualPrimary.piece U j L).directions n x = HarmonicCalculus.phaseNormal PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).axial (ActualSignedGeometry.preparedViewPhase CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.slots (CorrectionInitialization.ActualPrimary.choice B N0).prepared j L n (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)) (PhysicalResidualTZ.swapCylinder x)

theorem NavierStokes.ActualPrimaryCoherence.chart_phase_smooth {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : ContDiffOn ℝ (↑⊤) ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).phase n) positiveRadialChart

theorem NavierStokes.ActualPrimaryCoherence.chart_amplitude_smooth {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : ContDiffOn ℝ (↑⊤) ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).amplitude n) positiveChart

theorem NavierStokes.ActualPrimaryCoherence.chart_cutoff_smooth {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : ContDiff ℝ (↑⊤) (CorrectionInitialization.ActualPrimary.chartCutoff j L n)

theorem NavierStokes.ActualPrimaryCoherence.piece_domain_positive (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) : (HarmonicWaveInteraction.productStrip (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal U)).domain ⊆ positiveRadialChart

theorem NavierStokes.ActualPrimaryCoherence.piece_phase_smooth {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : ContDiffOn ℝ (↑⊤) ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).phase n) (HarmonicWaveInteraction.productStrip (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal U)).domain

theorem NavierStokes.ActualPrimaryCoherence.piece_amplitude_smooth {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : ContDiffOn ℝ (↑⊤) ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).amplitude n) (HarmonicWaveInteraction.productStrip (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal U)).domain

theorem NavierStokes.ActualPrimaryCoherence.chart_normal_copy {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)) (k : TorusInverse.Frequency) (x : ChartPoint) (hx : (CorrectionInitialization.ActualPrimary.nativeSlow L (CorrectionInitialization.ActualPrimary.toAbsolute n x.1), (CorrectionInitialization.ActualPrimary.geometry j L).coordinates k (CorrectionInitialization.ActualPrimary.toAbsolute n x.1).2) ∈ (ActualSignedGeometry.nativeDomain CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared).carrier L) : (CorrectionInitialization.ActualPrimary.chartCoefficients j L).normal (CorrectionInitialization.ActualPrimary.piece U j L).strip (CorrectionInitialization.ActualPrimary.piece U j L).directions n x = PhysicalParticularWave.normalWeight (ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand L)) ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n) ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)) • (CorrectionInitialization.ActualPrimary.phases B N0 j).phase.normal L (CorrectionInitialization.ActualPrimary.nativeSlow L (CorrectionInitialization.ActualPrimary.toAbsolute n x.1), ((CorrectionInitialization.ActualPrimary.geometry j L).coordinates k (CorrectionInitialization.ActualPrimary.toAbsolute n x.1).2).2)

theorem NavierStokes.ActualPrimaryCoherence.cutAmplitude_inside {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (x : ChartPoint) (hr : amplitudeRadius L ((absoluteChart n) x) ∈ Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)) : ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).withCutoff (CorrectionInitialization.ActualPrimary.chartCutoff j L)).amplitude n x = (ChartScales.Q n ^ CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h * ChartScales.Q (BaseChartJets.cellBand L) ^ (-CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h)) • CorrectionInitialization.ActualPrimary.commonAmplitude j L (CorrectionInitialization.ActualPrimary.nativeSlow L (CorrectionInitialization.ActualPrimary.toAbsolute n x.1)) (CorrectionInitialization.ActualPrimary.toAbsolute n x.1).2

theorem NavierStokes.ActualPrimaryCoherence.cutAmplitude_outside {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (x : ChartPoint) (hr : amplitudeRadius L ((absoluteChart n) x) ∉ Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)) : ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).withCutoff (CorrectionInitialization.ActualPrimary.chartCutoff j L)).amplitude n x = 0

theorem NavierStokes.ActualPrimaryCoherence.piece_cutAmplitude_tangent {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)) {x : ChartPoint} (hT : 0 < x.1.2.1.1) : HarmonicCalculus.normalDot ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).normal (CorrectionInitialization.ActualPrimary.piece U j L).strip (CorrectionInitialization.ActualPrimary.piece U j L).directions n x) (((CorrectionInitialization.ActualPrimary.chartCoefficients j L).withCutoff (CorrectionInitialization.ActualPrimary.chartCutoff j L)).amplitude n x) = 0

noncomputable def NavierStokes.ActualPrimaryCoherence.chartRadiusLinear : ChartPoint →L[ℝ] ℝ

Chart radius linear, given by (ContinuousLinearMap.fst ℝ ℝ _).comp (ContinuousLinearMap.fst ℝ _ ℝ).

Equations

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

noncomputable def NavierStokes.ActualPrimaryCoherence.chartRadialCurve (n : ℕ) (r : ℝ) : ChartPoint

Chart radial curve, constructed using PhysicalResidualTZ.swapCylinder.

Equations

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

theorem NavierStokes.ActualPrimaryCoherence.chartRadialCurve_smoothAt (n : ℕ) {r : ℝ} (hr : r ≠ 0) : ContDiffAt ℝ (↑⊤) (chartRadialCurve n) r

theorem NavierStokes.ActualPrimaryCoherence.chart_radial_curve (B n : ℕ) : (PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).radialField n = fun (x : ChartPoint) => chartRadialCurve n (chartRadiusLinear x)

theorem NavierStokes.ActualPrimaryCoherence.chart_radial_aux_derivative (B n : ℕ) {x : ChartPoint} (hx : x.1.1 ≠ 0) (v : ChartPoint) (hv : v.1.1 = 0) : (fderiv ℝ ((PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).radialField n) x) v = 0

theorem NavierStokes.ActualPrimaryCoherence.piece_geometry (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (B n : ℕ) : CurlClassBounds.CylindricalGeometry positiveRadialChart (fun (x : ChartPoint) => x.1.1) ((PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).radialField n) (fun (x : ChartPoint) => (PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).angular) ((PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).axialField (HarmonicWaveInteraction.productStrip (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal U)) n)

theorem NavierStokes.ActualPrimaryCoherence.chart_normal_absolute {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (x : ChartPoint) : (CorrectionInitialization.ActualPrimary.chartCoefficients j L).normal (CorrectionInitialization.ActualPrimary.piece U j L).strip (CorrectionInitialization.ActualPrimary.piece U j L).directions n x = (1 / ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n) * √(ChartScales.Q n)) • absoluteNormal j L ((absoluteChart n) x)

theorem NavierStokes.ActualPrimaryCoherence.absoluteCutAmplitude_tangent {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) {x : Absolute} (hx : x ∈ positiveAbsolute) : HarmonicCalculus.normalDot (absoluteNormal j L x) (absoluteCutAmplitude j L x) = 0

theorem NavierStokes.ActualPrimaryCoherence.piece_tangent {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) {x : ChartPoint} (hx : x ∈ positiveChart) : HarmonicCalculus.normalDot ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).normal (CorrectionInitialization.ActualPrimary.piece U j L).strip (CorrectionInitialization.ActualPrimary.piece U j L).directions n x) (((CorrectionInitialization.ActualPrimary.chartCoefficients j L).withCutoff (CorrectionInitialization.ActualPrimary.chartCutoff j L)).amplitude n x) = 0

Tangency holds on every band. A valid native cover proves it first, then the exact absolute normal and amplitude laws remove any index restriction.

theorem NavierStokes.ActualPrimaryCoherence.piece_normal_ne {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) {x : ChartPoint} (hx : x ∈ positiveRadialChart) : (CorrectionInitialization.ActualPrimary.chartCoefficients j L).normal (CorrectionInitialization.ActualPrimary.piece U j L).strip (CorrectionInitialization.ActualPrimary.piece U j L).directions n x ≠ 0

theorem NavierStokes.ActualPrimaryCoherence.piece_exactAmplitude_smooth {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : ContDiffOn ℝ (↑⊤) ((CorrectionInitialization.ActualPrimary.piece U j L).exactCoefficients.amplitude n) positiveRadialChart

theorem NavierStokes.ActualPrimaryCoherence.piece_complexVelocity_smooth {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : ContDiffOn ℝ (↑⊤) (HarmonicCalculus.vectorMode ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).frequency n) ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).phase n) ((CorrectionInitialization.ActualPrimary.piece U j L).exactCoefficients.amplitude n)) positiveRadialChart

theorem NavierStokes.ActualPrimaryCoherence.piece_complex_divergence {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) {x : ChartPoint} (hx : x ∈ positiveRadialChart) : HarmonicCalculus.cylindricalDivergence (fun (y : ChartPoint) => y.1.1) ((PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).radialField n) (fun (x : ChartPoint) => (PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).angular) ((PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).axialField (CorrectionInitialization.ActualPrimary.piece U j L).strip n) (HarmonicCalculus.vectorMode ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).frequency n) ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).phase n) ((CorrectionInitialization.ActualPrimary.piece U j L).exactCoefficients.amplitude n)) x = 0

theorem NavierStokes.ActualPrimaryCoherence.piece_full_divergence {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) {x : ChartPoint} (hx : x ∈ positiveRadialChart) : HarmonicCalculus.cylindricalDivergence (fun (y : ChartPoint) => y.1.1) ((PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).radialField n) (fun (x : ChartPoint) => (PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).angular) ((PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).axialField (CorrectionInitialization.ActualPrimary.piece U j L).strip n) (fun (y : ChartPoint) (i : Fin 3) => ↑((CorrectionInitialization.ActualPrimary.piece U j L).velocity n y i)) x = 0

Literal real corrected field, with the radial connection term included.

noncomputable def NavierStokes.ActualPrimaryCoherence.physicalLift (z : ProblemStatement.SpaceTime) : Absolute

The absolute free lift evaluated on the actual physical cylindrical graph.

Equations

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

theorem NavierStokes.ActualPrimaryCoherence.absoluteChart_physical (n : ℕ) {z : ProblemStatement.SpaceTime} (hr : 0 < z.2.ofLp 0) : (absoluteChart n) (PhysicalResidualTZ.swapCylinder ((PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).map z)) = physicalLift z

noncomputable def NavierStokes.ActualPrimaryCoherence.physicalPhase {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : ProblemStatement.SpaceTime → ℝ

Physical phase, defined pointwise by absolutePhase j L (physicalLift z).

Equations

• NavierStokes.ActualPrimaryCoherence.physicalPhase j L z = NavierStokes.CorrectionInitialization.ActualPrimary.absolutePhase j L (NavierStokes.ActualPrimaryCoherence.physicalLift z)

noncomputable def NavierStokes.ActualPrimaryCoherence.physicalAmplitude {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector

Physical amplitude, defined pointwise by absoluteCutAmplitude j L (physicalLift z).

Equations

• NavierStokes.ActualPrimaryCoherence.physicalAmplitude j L z = NavierStokes.ActualPrimaryCoherence.absoluteCutAmplitude j L (NavierStokes.ActualPrimaryCoherence.physicalLift z)

noncomputable def NavierStokes.ActualPrimaryCoherence.liftedPhase {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : ChartPoint → ℝ

Lifted phase, defined pointwise by (chartCoefficients j L).phase n (PhysicalResidualTZ.swapCylinder x).

Equations

• NavierStokes.ActualPrimaryCoherence.liftedPhase j L n x = (NavierStokes.CorrectionInitialization.ActualPrimary.chartCoefficients j L).phase n (NavierStokes.PhysicalResidualTZ.swapCylinder x)

noncomputable def NavierStokes.ActualPrimaryCoherence.liftedAmplitude {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : ChartPoint → HarmonicCalculus.ComplexVector

Lifted amplitude, defined pointwise by ((chartCoefficients j L).withCutoff (chartCutoff j L)).amplitude n (PhysicalResidualTZ.swapCylinder x).

Equations

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

noncomputable def NavierStokes.ActualPrimaryCoherence.liftedDomain : Set ChartPoint

Lifted domain, given by PhysicalResidualTZ.swapCylinder ⁻¹' positiveRadialChart.

Equations

• NavierStokes.ActualPrimaryCoherence.liftedDomain = ⇑NavierStokes.PhysicalResidualTZ.swapCylinder ⁻¹' NavierStokes.ActualPrimaryCoherence.positiveRadialChart

theorem NavierStokes.ActualPrimaryCoherence.liftedDomain_open : IsOpen liftedDomain

theorem NavierStokes.ActualPrimaryCoherence.liftedPhase_smooth {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : ContDiffOn ℝ (↑⊤) (liftedPhase j L n) liftedDomain

theorem NavierStokes.ActualPrimaryCoherence.liftedAmplitude_smooth {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : ContDiffOn ℝ (↑⊤) (liftedAmplitude j L n) liftedDomain

theorem NavierStokes.ActualPrimaryCoherence.chart_normal_lifted {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (x : ChartPoint) : (CorrectionInitialization.ActualPrimary.chartCoefficients j L).normal (CorrectionInitialization.ActualPrimary.piece U j L).strip (CorrectionInitialization.ActualPrimary.piece U j L).directions n (PhysicalResidualTZ.swapCylinder x) = HarmonicCalculus.phaseNormal PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).axial (liftedPhase j L n) x

theorem NavierStokes.ActualPrimaryCoherence.lifted_realized {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (x : ChartPoint) : (CorrectionInitialization.ActualPrimary.piece U j L).exactCoefficients.amplitude n (PhysicalResidualTZ.swapCylinder x) = CurlClassBounds.realizedCoefficient ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).frequency n) PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).axial (liftedPhase j L n) (liftedAmplitude j L n) x

theorem NavierStokes.ActualPrimaryCoherence.physicalPhase_eq {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) {z : ProblemStatement.SpaceTime} (hr : 0 < z.2.ofLp 0) : physicalPhase j L z = (CorrectionInitialization.ActualPrimary.chartCoefficients j L).frequency n * liftedPhase j L n ((PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).map z)

theorem NavierStokes.ActualPrimaryCoherence.physicalAmplitude_eq {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) {z : ProblemStatement.SpaceTime} (hr : 0 < z.2.ofLp 0) : physicalAmplitude j L z = ChartScales.Q n ^ (-CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) • liftedAmplitude j L n ((PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).map z)

noncomputable def NavierStokes.ActualPrimaryCoherence.physicalAngular : ProblemStatement.SpaceTime

Physical angular, given by (0,ProblemStatement.coordinateVector 1).

Equations

• NavierStokes.ActualPrimaryCoherence.physicalAngular = (0, NavierStokes.ProblemStatement.coordinateVector 1)

theorem NavierStokes.ActualPrimaryCoherence.physicalLift_angular (z : ProblemStatement.SpaceTime) (s : ℝ) : physicalLift (z + s • physicalAngular) = physicalLift z + s • (0, 1)

theorem NavierStokes.ActualPrimaryCoherence.physicalPhase_angular {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : CopyAngularInvariance.AffinePhase physicalAngular (↑(PrimaryGeometryAssembly.angularMode CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared j L)) (physicalPhase j L)

theorem NavierStokes.ActualPrimaryCoherence.physicalAmplitude_angular {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : CopyAngularInvariance.Invariant physicalAngular (physicalAmplitude j L)

noncomputable def NavierStokes.ActualPrimaryCoherence.physicalPotential {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector

Physical potential, given by PhysicalCurlCovariance.referencePotential 1 (physicalPhase j L) (physicalAmplitude j L).

Equations

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

theorem NavierStokes.ActualPrimaryCoherence.physicalPotential_periodic {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (t r z : ℝ) : Function.Periodic (fun (θ : ℝ) => physicalPotential j L (t, AxisymmetricResidual.pack r θ z)) (2 * Real.pi)

noncomputable def NavierStokes.ActualPrimaryCoherence.physicalAxisRadius {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) : ℝ

One fixed radius for each original label, chosen from its actual physical scale and the positive inner support radius.

Equations

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

theorem NavierStokes.ActualPrimaryCoherence.physicalAxisRadius_pos {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) : 0 < physicalAxisRadius L

theorem NavierStokes.ActualPrimaryCoherence.absoluteAmplitude_zero_mask {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (x : CorrectionInitialization.ActualPrimary.AbsolutePoint) (hx : CorrectionInitialization.ActualPrimary.spatialMask L (CorrectionInitialization.ActualPrimary.nativeSlow L x) = 0) : CorrectionInitialization.ActualPrimary.absoluteAmplitude j L x = 0

theorem NavierStokes.ActualPrimaryCoherence.physicalAmplitude_zero_axis {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (z : ProblemStatement.SpaceTime) (hz : z.2.ofLp 0 ≤ physicalAxisRadius L) : physicalAmplitude j L z = 0

theorem NavierStokes.ActualPrimaryCoherence.physicalPotential_zero_axis {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (z : ProblemStatement.SpaceTime) (hz : z.2.ofLp 0 ≤ physicalAxisRadius L) : physicalPotential j L z = 0

theorem NavierStokes.ActualPrimaryCoherence.periodic_value_of_polar_eq {E : Type} (f : TorusInverse.Plane → E) (hf : ∀ (r : ℝ), Function.Periodic (fun (θ : ℝ) => f (r, θ)) (2 * Real.pi)) {r θ : ℝ} (hr : r ≠ 0) {q : TorusInverse.Plane} (hqr : q.1 = r) (hq : PolarCharts.polar q = PolarCharts.polar (r, θ)) : f q = f (r, θ)

theorem NavierStokes.ActualPrimaryCoherence.globalPotential_forward {a : ℝ} (ha : 0 < a) (B : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector) (hper : ∀ (t r z : ℝ), Function.Periodic (fun (θ : ℝ) => B (t, AxisymmetricResidual.pack r θ z)) (2 * Real.pi)) (hzero : ∀ (z : ProblemStatement.SpaceTime), z.2.ofLp 0 ≤ a → B z = 0) {z : ProblemStatement.SpaceTime} (hr : 0 < z.2.ofLp 0) : PhysicalCurlCovariance.globalCartesianPotential a B (z.1, CylindricalResidual.chart z.2) = (CylindricalResidual.frame (z.2.ofLp 1)) (PhysicalCurlCovariance.realVector (B z))

The complete periodic potential gives a forward representation at every positive cylindrical radius, including angles outside the chosen inverse chart.

theorem NavierStokes.ActualPrimaryCoherence.globalPotential_forward_germ {a : ℝ} (ha : 0 < a) (B : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector) (hper : ∀ (t r z : ℝ), Function.Periodic (fun (θ : ℝ) => B (t, AxisymmetricResidual.pack r θ z)) (2 * Real.pi)) (hzero : ∀ (z : ProblemStatement.SpaceTime), z.2.ofLp 0 ≤ a → B z = 0) {z : ProblemStatement.SpaceTime} (hr : 0 < z.2.ofLp 0) : (fun (y : ProblemStatement.SpaceTime) => PhysicalCurlCovariance.globalCartesianPotential a B (y.1, CylindricalResidual.chart y.2)) =ᶠ[nhds z] fun (y : ProblemStatement.SpaceTime) => (CylindricalResidual.frame (y.2.ofLp 1)) (PhysicalCurlCovariance.realVector (B y))

One actual Cartesian potential for every primary label

theorem NavierStokes.ActualPrimaryCoherence.physical_source (n : ℕ) {z : ProblemStatement.SpaceTime} (ht : z.1 < 1) (hr : 0 < z.2.ofLp 0) : z ∈ (PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).source liftedDomain

theorem NavierStokes.ActualPrimaryCoherence.liftedNormal_ne {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) {x : ChartPoint} (hx : x ∈ liftedDomain) : HarmonicCalculus.phaseNormal PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).axial (liftedPhase j L n) x ≠ 0

theorem NavierStokes.ActualPrimaryCoherence.lifted_tangent {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) {x : ChartPoint} (hx : x ∈ liftedDomain) : HarmonicCalculus.normalDot (HarmonicCalculus.phaseNormal PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).axial (liftedPhase j L n) x) (liftedAmplitude j L n x) = 0

theorem NavierStokes.ActualPrimaryCoherence.liftedPotential_smooth {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : ContDiffOn ℝ (↑⊤) (CurlClassBounds.vectorPotential ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).frequency n) PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).axial (liftedPhase j L n) (liftedAmplitude j L n)) liftedDomain

theorem NavierStokes.ActualPrimaryCoherence.physicalPotential_smooth {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : ContDiffOn ℝ (↑⊤) (physicalPotential j L) {z : ProblemStatement.SpaceTime | z.1 < 1 ∧ 0 < z.2.ofLp 0}

noncomputable def NavierStokes.ActualPrimaryCoherence.cartesianPotential {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : ProblemStatement.VelocityField

No band index occurs in this Cartesian potential. The cutoff is the original periodic Gaussian, and the polar chart is chosen from its full-turn-compatible values.

Equations

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

noncomputable def NavierStokes.ActualPrimaryCoherence.cartesianVelocity {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : ProblemStatement.VelocityField

Cartesian velocity, given by SpatialCurl.spatialCurl (cartesianPotential j L).

Equations

• NavierStokes.ActualPrimaryCoherence.cartesianVelocity j L = NavierStokes.SpatialCurl.spatialCurl (NavierStokes.ActualPrimaryCoherence.cartesianPotential j L)

theorem NavierStokes.ActualPrimaryCoherence.cartesianPotential_smooth {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : ContDiffOn ℝ (↑⊤) (cartesianPotential j L) {z : ProblemStatement.SpaceTime | z.1 < 1}

theorem NavierStokes.ActualPrimaryCoherence.cartesianVelocity_axis_zero {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (t : ℝ) (x : ProblemStatement.Space) (hx : x.ofLp 0 = 0) (hy : x.ofLp 1 = 0) : cartesianVelocity j L (t, x) = 0

theorem NavierStokes.ActualPrimaryCoherence.piece_cartesian_velocity {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) {z : ProblemStatement.SpaceTime} (ht : z.1 < 1) (hr : 0 < z.2.ofLp 0) (i : Fin 3) : (CorrectionInitialization.ActualPrimary.piece U j L).velocity n (PhysicalResidualTZ.swapCylinder ((PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).map z)) i = ChartScales.Q n ^ CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h * ((CylindricalResidual.frame (-z.2.ofLp 1)) (cartesianVelocity j L (z.1, CylindricalResidual.chart z.2))).ofLp i

Every actual band velocity is the rotating-frame representation of the curl of the same constructed Cartesian potential. This includes all positive radii and all angles, without a native-cover restriction.

noncomputable def NavierStokes.ActualPrimaryCoherence.physicalPressure {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : ProblemStatement.SpaceTime → ℝ

Physical pressure, defined pointwise by absolutePressureMode j L (physicalLift z).

Equations

• NavierStokes.ActualPrimaryCoherence.physicalPressure j L z = NavierStokes.CorrectionInitialization.ActualPrimary.absolutePressureMode j L (NavierStokes.ActualPrimaryCoherence.physicalLift z)

theorem NavierStokes.ActualPrimaryCoherence.piece_physical_pressure {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) {z : ProblemStatement.SpaceTime} (hr : 0 < z.2.ofLp 0) : (CorrectionInitialization.ActualPrimary.piece U j L).pressure n (PhysicalResidualTZ.swapCylinder ((PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).map z)) = ChartScales.Q n ^ (2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) * physicalPressure j L z

theorem NavierStokes.ActualPrimaryCoherence.cartesianVelocity_smooth {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : ContDiffOn ℝ (↑⊤) (cartesianVelocity j L) {z : ProblemStatement.SpaceTime | z.1 < 1}

theorem NavierStokes.ActualPrimaryCoherence.cartesianVelocity_divergence {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) {t : ℝ} (ht : t < 1) (x : ProblemStatement.Space) : ProblemStatement.spatialDivergence (cartesianVelocity j L) t x = 0