The actual initial support retains its radial and native dyadic cores

The broad source carrier retains the slow spatial mask and the fast source rectangle. The actual fields have two further cutoffs: the moving radial attachment and the original label's dyadic cutoff. We keep their closed cores in a fixed carrier and take the ambient closure of its positive-time part. No continuity of the totalized similarity coordinate at time zero is used.

@[reducible, inline]

abbrev NavierStokes.ActualCoreSupport.Point : Type

Point: an abbreviation for LocalSignedRequest.Point.

Equations

• NavierStokes.ActualCoreSupport.Point = NavierStokes.LocalSignedRequest.Point

@[reducible, inline]

abbrev NavierStokes.ActualCoreSupport.Index (B N0 : ℕ) : Type

Index: an abbreviation for ActualInitialization.Index B N0.

Equations

• NavierStokes.ActualCoreSupport.Index B N0 = NavierStokes.ActualInitialization.Index B N0

noncomputable def NavierStokes.ActualCoreSupport.radialRatio (x : Point) : ℝ

Radial ratio, given by x.1 / VariableGaugeMean.qLength (2 * ActualPrimary.h) x.2.1.

Equations

• NavierStokes.ActualCoreSupport.radialRatio x = x.1 / NavierStokes.VariableGaugeMean.qLength (2 * NavierStokes.CorrectionInitialization.ActualPrimary.h) x.2.1

noncomputable def NavierStokes.ActualCoreSupport.nativeQ {B N0 : ℕ} (l : Index B N0) (n : ℕ) (x : Point) : ℝ

This is the original label's native similarity scale, not the scale in the current chart.

Equations

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

noncomputable def NavierStokes.ActualCoreSupport.positiveCore {B N0 : ℕ} (l : Index B N0) (n : ℕ) : Set Point

Positive core as an element of Set Point.

Equations

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

noncomputable def NavierStokes.ActualCoreSupport.refinedCarrier {B N0 : ℕ} (l : Index B N0) (n : ℕ) : Set Point

Refined carrier, given by closure (positiveCore l n).

Equations

• NavierStokes.ActualCoreSupport.refinedCarrier l n = closure (NavierStokes.ActualCoreSupport.positiveCore l n)

theorem NavierStokes.ActualCoreSupport.refinedCarrier_closed {B N0 : ℕ} (l : Index B N0) (n : ℕ) : IsClosed (refinedCarrier l n)

theorem NavierStokes.ActualCoreSupport.refinedCarrier_subset_broad {B N0 : ℕ} (l : Index B N0) (n : ℕ) : refinedCarrier l n ⊆ ActualInitialization.labelCarrier l n

theorem NavierStokes.ActualCoreSupport.refinedCarrier_nonnegative_time {B N0 : ℕ} (l : Index B N0) (n : ℕ) : refinedCarrier l n ⊆ {x : Point | 0 ≤ x.2.1.1}

theorem NavierStokes.ActualCoreSupport.radialRatio_continuousAt {x : Point} (hT : 0 < x.2.1.1) : ContinuousAt radialRatio x

theorem NavierStokes.ActualCoreSupport.nativeQ_continuousAt {B N0 : ℕ} (l : Index B N0) (n : ℕ) {x : Point} (hT : 0 < x.2.1.1) : ContinuousAt (nativeQ l n) x

theorem NavierStokes.ActualCoreSupport.mem_refinedCarrier_iff {B N0 : ℕ} (l : Index B N0) (n : ℕ) {x : Point} (hT : 0 < x.2.1.1) : x ∈ refinedCarrier l n ↔ x ∈ ActualInitialization.labelCarrier l n ∧ radialRatio x ∈ Set.Icc (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal) ∧ nativeQ l n x ∈ Set.Icc (1 / 2) 2

Taking ambient closure adds no extra points at positive time.

theorem NavierStokes.ActualCoreSupport.mem_refinedCarrier_of_mem {B N0 : ℕ} (l : Index B N0) (n : ℕ) {x : Point} (hT : 0 < x.2.1.1) (hb : x ∈ ActualInitialization.labelCarrier l n) (hr : radialRatio x ∈ Set.Icc (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)) (hq : nativeQ l n x ∈ Set.Icc (1 / 2) 2) : x ∈ refinedCarrier l n

theorem NavierStokes.ActualCoreSupport.radialRatio_fast (x : Point) (Y : TorusInverse.Plane) : radialRatio (x.1, x.2.1, Y) = radialRatio x

theorem NavierStokes.ActualCoreSupport.nativeQ_fast {B N0 : ℕ} (l : Index B N0) (n : ℕ) (x : Point) (Y : TorusInverse.Plane) : nativeQ l n (x.1, x.2.1, Y) = nativeQ l n x

theorem NavierStokes.ActualCoreSupport.rawVelocity_nativeQ {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) {x : ActualSignedGeometry.Native} (hx : CorrectionInitialization.ActualPrimary.rawVelocity j L x ≠ 0) : SimilarityHomogeneity.chartQ CorrectionInitialization.ActualPrimary.h x.1 ∈ Set.Ioo (1 / 2) 2

theorem NavierStokes.ActualCoreSupport.attached_velocity_core {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) {x : ActualSignedGeometry.Native} (hx : CorrectionInitialization.ActualPrimary.attachedRawVelocity j L x ≠ 0) : WaveEdgeExtension.nativeRadius CorrectionInitialization.ActualPrimary.h x ∈ Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal) ∧ SimilarityHomogeneity.chartQ CorrectionInitialization.ActualPrimary.h x.1 ∈ Set.Ioo (1 / 2) 2

Both extra constraints come from actual factors of the attached field.

theorem NavierStokes.ActualCoreSupport.attached_pressure_core {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) {x : ActualSignedGeometry.Native} (hx : CorrectionInitialization.ActualPrimary.attachedRawPressure j L x ≠ 0) : WaveEdgeExtension.nativeRadius CorrectionInitialization.ActualPrimary.h x ∈ Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal) ∧ SimilarityHomogeneity.chartQ CorrectionInitialization.ActualPrimary.h x.1 ∈ Set.Ioo (1 / 2) 2

theorem NavierStokes.ActualCoreSupport.copy_radial_core {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hT : 0 < x.1.2.1.1) (hx : WaveEdgeExtension.nativeRadius CorrectionInitialization.ActualPrimary.h (ActualPrimaryDynamics.copyPoint j L n k x) ∈ Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)) : radialRatio x.1 ∈ Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)

theorem NavierStokes.ActualCoreSupport.cut_amplitude_mem_refined {B N0 : ℕ} (l : Index B N0) (n : ℕ) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hT : 0 < x.1.2.1.1) (hx : x ∈ Function.support (((ActualInitialization.primaryPiece l).coefficients.withCutoff (ActualInitialization.primaryPiece l).cutoff).amplitude n)) : x.1 ∈ refinedCarrier l n

theorem NavierStokes.ActualCoreSupport.cut_pressure_mem_refined {B N0 : ℕ} (l : Index B N0) (n : ℕ) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hT : 0 < x.1.2.1.1) (hx : x ∈ Function.support ((ActualInitialization.primaryPiece l).exactCoefficients.pressure n)) : x.1 ∈ refinedCarrier l n

theorem NavierStokes.ActualCoreSupport.cut_amplitude_zero_germ {B N0 : ℕ} (l : Index B N0) (n : ℕ) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hT : 0 < x.1.2.1.1) (hx : x.1 ∉ refinedCarrier l n) : ((ActualInitialization.primaryPiece l).coefficients.withCutoff (ActualInitialization.primaryPiece l).cutoff).amplitude n =ᶠ[nhds x] fun (x : CorrectionInitialization.ActualPrimary.FullPoint) => 0

theorem NavierStokes.ActualCoreSupport.primary_velocity_zero {B N0 : ℕ} (l : Index B N0) (n : ℕ) {x : Point} (hT : 0 < x.2.1.1) (hx : x ∉ refinedCarrier l n) (θ : ℝ) : (ActualInitialization.primaryBlock l).oscillation n (x, θ) = 0

theorem NavierStokes.ActualCoreSupport.primary_pressure_zero {B N0 : ℕ} (l : Index B N0) (n : ℕ) {x : Point} (hT : 0 < x.2.1.1) (hx : x ∉ refinedCarrier l n) (θ : ℝ) : (ActualInitialization.primaryBlock l).oscillatoryPressure n (x, θ) = 0

theorem NavierStokes.ActualCoreSupport.chartGaussian_mem_refined {B N0 : ℕ} (l : Index B N0) (n : ℕ) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hT : 0 < x.1.2.1.1) (hx : ActualInitialExcluded.chartGaussian (l.2, l.1) n x ≠ 0) : x.1 ∈ refinedCarrier l n

theorem NavierStokes.ActualCoreSupport.gaussian_velocity_zero {B N0 : ℕ} (l : Index B N0) (n : ℕ) {x : Point} (hT : 0 < x.2.1.1) (hx : x ∉ refinedCarrier l n) (θ : ℝ) : (ActualInitialization.gaussianBlock l).oscillation n (x, θ) = 0

theorem NavierStokes.ActualCoreSupport.initial_inputSupport {B N0 : ℕ} (l : Index B N0) : HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (refinedCarrier l) (ActualInitialization.primaryBlock l) (ActualInitialization.gaussianBlock l).velocity 0

This is proved for the literal seed velocity, pressure, Gaussian and alias coefficients. The stronger support is not an initialization premise.

theorem NavierStokes.ActualCoreSupport.initial_invariant (B N0 : ℕ) : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope refinedCarrier (1 / 5) (ActualInitialization.initialCycleState B N0)

Reuse the actual initialized state and every established invariant field. Only its support certificate is strengthened.