Support of the actual current-band waves

The refined source carrier contains the fixed profile annulus. Its strict exterior supplies zero germs of the literal current-band Volterra outputs. The physical support argument uses the continuous Cartesian radius divided by the square root of the physical similarity scale. In particular, it does not differentiate a polar chart at the axis or use an excluded dyadic face of a fixed reference formula.

@[reducible, inline]

abbrev NavierStokes.ActualCurrentWaveSupport.Point : Type

Point: an abbreviation for LocalSignedRequest.Point.

Equations

• NavierStokes.ActualCurrentWaveSupport.Point = NavierStokes.LocalSignedRequest.Point

@[reducible, inline]

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

Index: an abbreviation for ActualInitialization.Index B N0.

Equations

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

noncomputable def NavierStokes.ActualCurrentWaveSupport.profileRadius (h : ℝ) (w : ProblemStatement.SpaceTime) : ℝ

The profile radius in physical coordinates, independent of the valid dyadic chart used to evaluate a wave.

Equations

• NavierStokes.ActualCurrentWaveSupport.profileRadius h w = NavierStokes.AnnularEndpoint.radius w / √(NavierStokes.PhysicalWaveSum.physicalQ h w)

theorem NavierStokes.ActualCurrentWaveSupport.profileRadius_continuousAt {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {w : ProblemStatement.SpaceTime} (ht : w.1 < 1) : ContinuousAt (profileRadius h) w

theorem NavierStokes.ActualCurrentWaveSupport.profileRadius_zero_of_axis (h : ℝ) {w : ProblemStatement.SpaceTime} (ha : PhysicalGraphBounds.radialProjection w = 0) : profileRadius h w = 0

theorem NavierStokes.ActualCurrentWaveSupport.profileRadius_sq {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {w : ProblemStatement.SpaceTime} (ht : w.1 < 1) : profileRadius h w ^ 2 / 2 = (SlowBorelBase.cartesianChart h w).2.1

theorem NavierStokes.ActualCurrentWaveSupport.profileRadius_mem_iff_active {w : ProblemStatement.SpaceTime} (ht : w.1 < 1) : profileRadius CorrectionInitialization.ActualPrimary.h w ∈ Set.Icc (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal) ↔ (SlowBorelBase.cartesianChart CorrectionInitialization.ActualPrimary.h w).2.1 ∈ Set.Icc (NominalConeAssembly.activeLeft CorrectionInitialization.ActualPrimary.nominal) (NominalConeAssembly.activeRight CorrectionInitialization.ActualPrimary.nominal)

The sharp profile-radius support is exactly the nominal active annulus in the physical similarity variable X.

theorem NavierStokes.ActualCurrentWaveSupport.graph_profileRadius_eq {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (n d : ℕ) {w : ProblemStatement.SpaceTime} (ht : w.1 < 1) : (PhysicalMeanJetBounds.graph h n d w).1 / VariableGaugeMean.qLength (2 * h) (PhysicalMeanJetBounds.graph h n d w).2.1 = profileRadius h w

The normalized radius of the actual scaled graph agrees with the band-independent physical ratio, also at the axis.

def NavierStokes.ActualCurrentWaveSupport.BandAnnulus {E : Type u_1} [NormedAddCommGroup E] (h a b : ℝ) (N : ℕ) (f : ℕ → ProblemStatement.SpaceTime → E) : Prop

A support assertion only on the open validity region of each band. It makes no assertion about the totalized formula at an excluded face.

Equations

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

theorem NavierStokes.ActualCurrentWaveSupport.BandAnnulus.zero_of_exterior {E : Type u_1} [NormedAddCommGroup E] {h a b : ℝ} {N n : ℕ} {f : ℕ → ProblemStatement.SpaceTime → E} (hs : BandAnnulus h a b N f) (hn : N ≤ n) {w : ProblemStatement.SpaceTime} (hw : w ∈ ValidDyadicBandCover.band h n) (hr : profileRadius h w ∉ Set.Icc a b) : f n w = 0

theorem NavierStokes.ActualCurrentWaveSupport.BandAnnulus.zero_germ {E : Type u_1} [NormedAddCommGroup E] {h a b : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {N n : ℕ} {f : ℕ → ProblemStatement.SpaceTime → E} (hs : BandAnnulus h a b N f) (hn : N ≤ n) {w : ProblemStatement.SpaceTime} (hw : w ∈ ValidDyadicBandCover.band h n) (hr : profileRadius h w ∉ Set.Icc a b) : f n =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.ActualCurrentWaveSupport.BandAnnulus.axis_zero_germ {E : Type u_1} [NormedAddCommGroup E] {h a b : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) {N n : ℕ} {f : ℕ → ProblemStatement.SpaceTime → E} (hs : BandAnnulus h a b N f) (hn : N ≤ n) {w : ProblemStatement.SpaceTime} (hw : w ∈ ValidDyadicBandCover.band h n) (haxis : PhysicalGraphBounds.radialProjection w = 0) : f n =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.ActualCurrentWaveSupport.BandAnnulus.map_zero {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] {h a b : ℝ} {N : ℕ} {f : ℕ → ProblemStatement.SpaceTime → E} (hs : BandAnnulus h a b N f) (T : ℕ → ProblemStatement.SpaceTime → E → F) (hT : ∀ (n : ℕ) (w : ProblemStatement.SpaceTime), T n w 0 = 0) : BandAnnulus h a b N fun (n : ℕ) (w : ProblemStatement.SpaceTime) => T n w (f n w)

theorem NavierStokes.ActualCurrentWaveSupport.BandAnnulus.add {E : Type u_1} [NormedAddCommGroup E] {h a b : ℝ} {N : ℕ} {f g : ℕ → ProblemStatement.SpaceTime → E} (hf : BandAnnulus h a b N f) (hg : BandAnnulus h a b N g) : BandAnnulus h a b N fun (n : ℕ) (w : ProblemStatement.SpaceTime) => f n w + g n w

theorem NavierStokes.ActualCurrentWaveSupport.BandAnnulus.finset_sum {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} {h a b : ℝ} {N : ℕ} {f : ι → ℕ → ProblemStatement.SpaceTime → E} (s : ℕ → Finset ι) (hs : ∀ (i : ι), BandAnnulus h a b N (f i)) : BandAnnulus h a b N fun (n : ℕ) (w : ProblemStatement.SpaceTime) => ∑ i ∈ s n, f i n w

theorem NavierStokes.ActualCurrentWaveSupport.BandAnnulus.field_zero_germ {E : Type u_1} [NormedAddCommGroup E] {h a b qbig : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {N : ℕ} {f : ℕ → ProblemStatement.SpaceTime → E} (hs : BandAnnulus h a b N f) (hf : ValidDyadicBandCover.Compatible h N f) (hqbig : qbig ≤ ChartScales.Q N) {w : ProblemStatement.SpaceTime} (hw : w ∈ CutStageEstimates.physicalSublevel h qbig) (hr : profileRadius h w ∉ Set.Icc a b) : ValidDyadicBandCover.field h N f =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.ActualCurrentWaveSupport.BandAnnulus.field_support {E : Type u_1} [NormedAddCommGroup E] {h a b qbig : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {N : ℕ} {f : ℕ → ProblemStatement.SpaceTime → E} (hs : BandAnnulus h a b N f) (hf : ValidDyadicBandCover.Compatible h N f) (hqbig : qbig ≤ ChartScales.Q N) : MixedDiagonalExtensions.SublevelShrinkingSupport h b qbig (ValidDyadicBandCover.field h N f)

theorem NavierStokes.ActualCurrentWaveSupport.BandAnnulus.field_axisZeroOn {h a b qbig : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) {N : ℕ} {f : ℕ → ProblemStatement.VelocityField} (hs : BandAnnulus h a b N f) (hf : ValidDyadicBandCover.Compatible h N f) (hqbig : qbig ≤ ChartScales.Q N) : GermCandidateAssembly.AxisZeroOn (MixedAxisPreservation.localDomain h qbig) (ValidDyadicBandCover.field h N f)

theorem NavierStokes.ActualCurrentWaveSupport.rightRadius_le_actualOuterConstant : PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal ≤ PhysicalStageSupport.actualOuterConstant

The common outer constant used by the actual physical stage assembly is larger than the fixed profile outer radius.

theorem NavierStokes.ActualCurrentWaveSupport.not_mem_refinedCarrier_of_radius {B N0 : ℕ} (l : Index B N0) (n : ℕ) {x : Point} (hT : 0 < x.2.1.1) (hr : ActualCoreSupport.radialRatio x ∉ Set.Icc (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)) : x ∉ ActualCoreSupport.refinedCarrier l n

theorem NavierStokes.ActualCurrentWaveSupport.particular_radial_zero_germs {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : Index B N0) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (b : CorrectionState.HarmonicBlock Point) (G A : HarmonicResidual.BlockCoefficients Point) (hs : HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualCoreSupport.refinedCarrier l) b G A) (j : ℤ) (s : WeightedClasses.StripData ((CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane)) (n : ℕ) {z : (CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane} (hz : z.1.1 ∈ ActualCarrierTransportBase.parameterDomain) (hr : ActualCoreSupport.radialRatio (ActualCarrierTransportBase.associatedPoint z.1.1 z.2) ∉ Set.Icc (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)) : have p := ActualParticularStageControls.canonicalParameters (l.2, l.1); have a := p.copyData (StateReindex.context CorrectionStep.cycleAssoc.symm c) (StateReindex.state CorrectionStep.cycleAssoc.symm u) (StateReindex.block CorrectionStep.cycleAssoc.symm b) (StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm G) (StateReindex.blockCoefficients CorrectionStep.cycleAssoc.symm A) j; (a.common.amplitude n =ᶠ[nhds z] fun (x : (CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane) => 0) ∧ ((a.commonCorrected s p.directions).amplitude n =ᶠ[nhds z] fun (x : (CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane) => 0) ∧ (a.common.pressure n =ᶠ[nhds z] fun (x : (CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane) => 0) ∧ a.globalGaussian p.directions n =ᶠ[nhds z] fun (x : (CorrectionStep.CycleSlow × ℝ) × TorusInverse.Plane) => 0

Strict radial exterior of the actual refined input carrier. All outputs are the same current-band copy solve used by the iteration.

theorem NavierStokes.ActualCurrentWaveSupport.nativePoint_radius (n : ℕ) (w : ProblemStatement.SpaceTime) : (ActualCurrentParticularPhysical.nativePoint n w).1.1.1 = ChartScales.Q n ^ (-(1 / 2)) * AnnularEndpoint.radius w

theorem NavierStokes.ActualCurrentWaveSupport.nativePoint_slow (n : ℕ) (w : ProblemStatement.SpaceTime) : (ActualCurrentParticularPhysical.nativePoint n w).1.1.2 = ((1 - w.1) / ChartScales.Q n, ChartScales.Q n ^ (-CoordinateAlgebra.D CorrectionInitialization.ActualPrimary.h) * w.2.ofLp 2)

theorem NavierStokes.ActualCurrentWaveSupport.nativePoint_slow_eq_graph (n : ℕ) (w : ProblemStatement.SpaceTime) : (ActualCurrentParticularPhysical.nativePoint n w).1.1.2 = (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n 0 w).2.1

theorem NavierStokes.ActualCurrentWaveSupport.nativePoint_coordinateQ (n : ℕ) {w : ProblemStatement.SpaceTime} (ht : w.1 < 1) : SimilarityCoordinates.coordinateQ (2 * CorrectionInitialization.ActualPrimary.h) (ActualCurrentParticularPhysical.nativePoint n w).1.1.2 = PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w / ChartScales.Q n

theorem NavierStokes.ActualCurrentWaveSupport.nativePoint_parameterDomain (n : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) : (ActualCurrentParticularPhysical.nativePoint n w).1.1 ∈ ActualCarrierTransportBase.parameterDomain

theorem NavierStokes.ActualCurrentWaveSupport.nativePoint_radius_eq_graph (n : ℕ) (w : ProblemStatement.SpaceTime) : (ActualCurrentParticularPhysical.nativePoint n w).1.1.1 = (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n 0 w).1

theorem NavierStokes.ActualCurrentWaveSupport.nativePoint_profileRadius (n : ℕ) {w : ProblemStatement.SpaceTime} (ht : w.1 < 1) : ActualCoreSupport.radialRatio (ActualCarrierTransportBase.associatedPoint (ActualCurrentParticularPhysical.nativePoint n w).1.1 (ActualCurrentParticularPhysical.nativePoint n w).2) = profileRadius CorrectionInitialization.ActualPrimary.h w

theorem NavierStokes.ActualCurrentWaveSupport.current_raw_pressure_zero_germs {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (x : CorrectionStep.CycleState (ActualCurrentParticularPhysical.Label B N0)) (l : ActualCurrentParticularPhysical.Label B N0) (hs : HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualCoreSupport.refinedCarrier (l.2, l.1)) (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l)) (j : ℤ) (n : ℕ) {z : ActualCurrentParticularPhysical.Native} (hz : z.1.1 ∈ ActualCarrierTransportBase.parameterDomain) (hr : ActualCoreSupport.radialRatio (ActualCarrierTransportBase.associatedPoint z.1.1 z.2) ∉ Set.Icc (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)) : ((ActualCurrentParticularPhysical.copyData x l j).common.amplitude n =ᶠ[nhds z] fun (x : ActualCurrentParticularPhysical.Native) => 0) ∧ (ActualCurrentParticularPhysical.copyData x l j).common.pressure n =ᶠ[nhds z] fun (x : ActualCurrentParticularPhysical.Native) => 0

theorem NavierStokes.ActualCurrentWaveSupport.current_raw_pressure_annulus {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (x : CorrectionStep.CycleState (ActualCurrentParticularPhysical.Label B N0)) (l : ActualCurrentParticularPhysical.Label B N0) (hs : HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualCoreSupport.refinedCarrier (l.2, l.1)) (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l)) (j : ℤ) (n : ℕ) {z : ActualCurrentParticularPhysical.Native} (hz : z.1.1 ∈ ActualCarrierTransportBase.parameterDomain) : ((ActualCurrentParticularPhysical.copyData x l j).common.amplitude n z ≠ 0 → ActualCoreSupport.radialRatio (ActualCarrierTransportBase.associatedPoint z.1.1 z.2) ∈ Set.Icc (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)) ∧ ((ActualCurrentParticularPhysical.copyData x l j).common.pressure n z ≠ 0 → ActualCoreSupport.radialRatio (ActualCarrierTransportBase.associatedPoint z.1.1 z.2) ∈ Set.Icc (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal))

theorem NavierStokes.ActualCurrentWaveSupport.current_native_zero_germs {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (x : CorrectionStep.CycleState (ActualCurrentParticularPhysical.Label B N0)) (l : ActualCurrentParticularPhysical.Label B N0) (hs : HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualCoreSupport.refinedCarrier (l.2, l.1)) (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l)) (j : ℤ) (n : ℕ) {z : ActualCurrentParticularPhysical.Native} (hz : z.1.1 ∈ ActualCarrierTransportBase.parameterDomain) (hr : ActualCoreSupport.radialRatio (ActualCarrierTransportBase.associatedPoint z.1.1 z.2) ∉ Set.Icc (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)) : (ActualCurrentParticularPhysical.nativePotential x l j n =ᶠ[nhds z] fun (x : ActualCurrentParticularPhysical.Native) => 0) ∧ ActualCurrentParticularPhysical.nativePressure x l j n =ᶠ[nhds z] fun (x : ActualCurrentParticularPhysical.Native) => 0

theorem NavierStokes.ActualCurrentWaveSupport.current_native_zero_germs_off_carrier {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (x : CorrectionStep.CycleState (ActualCurrentParticularPhysical.Label B N0)) (l : ActualCurrentParticularPhysical.Label B N0) (hs : HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualCoreSupport.refinedCarrier (l.2, l.1)) (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l)) (j : ℤ) (n : ℕ) {z : ActualCurrentParticularPhysical.Native} (hz : z.1.1 ∈ ActualCarrierTransportBase.parameterDomain) (hn : ActualCarrierTransportBase.associatedPoint z.1.1 z.2 ∉ ActualCoreSupport.refinedCarrier (l.2, l.1) n) : (ActualCurrentParticularPhysical.nativePotential x l j n =ᶠ[nhds z] fun (x : ActualCurrentParticularPhysical.Native) => 0) ∧ ActualCurrentParticularPhysical.nativePressure x l j n =ᶠ[nhds z] fun (x : ActualCurrentParticularPhysical.Native) => 0

The full refined carrier is retained, including its original slow mask and native dyadic cutoff, rather than just its radial projection.

theorem NavierStokes.ActualCurrentWaveSupport.modes_zero_of_native {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualCurrentParticularPhysical.Label B N0)) (l : ActualCurrentParticularPhysical.Label B N0) (j : ℤ) (n : ℕ) (w : ProblemStatement.SpaceTime) (ha : ActualCurrentParticularPhysical.nativePotential x l j n (ActualCurrentParticularPhysical.nativePoint n w) = 0) (hp : ActualCurrentParticularPhysical.nativePressure x l j n (ActualCurrentParticularPhysical.nativePoint n w) = 0) : ActualCurrentParticularPhysical.localPotentialMode x l j n w = 0 ∧ ActualCurrentParticularPhysical.localPressureMode x l j n w = 0

theorem NavierStokes.ActualCurrentWaveSupport.current_modes_zero_off_carrier {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (x : CorrectionStep.CycleState (ActualCurrentParticularPhysical.Label B N0)) (l : ActualCurrentParticularPhysical.Label B N0) (hs : HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualCoreSupport.refinedCarrier (l.2, l.1)) (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l)) (j : ℤ) (n : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) (hn : ActualCarrierTransportBase.associatedPoint (ActualCurrentParticularPhysical.nativePoint n w).1.1 (ActualCurrentParticularPhysical.nativePoint n w).2 ∉ ActualCoreSupport.refinedCarrier (l.2, l.1) n) : ActualCurrentParticularPhysical.localPotentialMode x l j n w = 0 ∧ ActualCurrentParticularPhysical.localPressureMode x l j n w = 0

theorem NavierStokes.ActualCurrentWaveSupport.current_modes_support {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (x : CorrectionStep.CycleState (ActualCurrentParticularPhysical.Label B N0)) (l : ActualCurrentParticularPhysical.Label B N0) (hs : HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualCoreSupport.refinedCarrier (l.2, l.1)) (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l)) (j : ℤ) (n : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) : (ActualCurrentParticularPhysical.localPotentialMode x l j n w ≠ 0 → ActualCarrierTransportBase.associatedPoint (ActualCurrentParticularPhysical.nativePoint n w).1.1 (ActualCurrentParticularPhysical.nativePoint n w).2 ∈ ActualCoreSupport.refinedCarrier (l.2, l.1) n) ∧ (ActualCurrentParticularPhysical.localPressureMode x l j n w ≠ 0 → ActualCarrierTransportBase.associatedPoint (ActualCurrentParticularPhysical.nativePoint n w).1.1 (ActualCurrentParticularPhysical.nativePoint n w).2 ∈ ActualCoreSupport.refinedCarrier (l.2, l.1) n)

theorem NavierStokes.ActualCurrentWaveSupport.current_modes_zero {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (x : CorrectionStep.CycleState (ActualCurrentParticularPhysical.Label B N0)) (l : ActualCurrentParticularPhysical.Label B N0) (hs : HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualCoreSupport.refinedCarrier (l.2, l.1)) (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l)) (j : ℤ) (n : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) (hr : profileRadius CorrectionInitialization.ActualPrimary.h w ∉ Set.Icc (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)) : ActualCurrentParticularPhysical.localPotentialMode x l j n w = 0 ∧ ActualCurrentParticularPhysical.localPressureMode x l j n w = 0

Pointwise zero passes through the actual normal coefficient, phase, Cartesian frame rotation and physical scaling. No continuity of a chosen polar angle is needed here.

theorem NavierStokes.ActualCurrentWaveSupport.current_mode_annulus {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (x : CorrectionStep.CycleState (ActualCurrentParticularPhysical.Label B N0)) (l : ActualCurrentParticularPhysical.Label B N0) (hs : HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualCoreSupport.refinedCarrier (l.2, l.1)) (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l)) (j : ℤ) (N : ℕ) : BandAnnulus CorrectionInitialization.ActualPrimary.h (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal) N (ActualCurrentParticularPhysical.localPotentialMode x l j) ∧ BandAnnulus CorrectionInitialization.ActualPrimary.h (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal) N (ActualCurrentParticularPhysical.localPressureMode x l j)

theorem NavierStokes.ActualCurrentWaveSupport.current_annulus {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (x : CorrectionStep.CycleState (ActualCurrentParticularPhysical.Label B N0)) (hs : ∀ (l : ActualCurrentParticularPhysical.Label B N0), HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualCoreSupport.refinedCarrier (l.2, l.1)) (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l)) (N : ℕ) : BandAnnulus CorrectionInitialization.ActualPrimary.h (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal) N (ActualCurrentParticularPhysical.localPotential x) ∧ BandAnnulus CorrectionInitialization.ActualPrimary.h (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal) N (ActualCurrentParticularPhysical.localPressure x)

Every actual finite label and harmonic sum retains the same sharp annulus; this statement has no copy-count or mode-count factor.

theorem NavierStokes.ActualCurrentWaveSupport.current_local_active_zero {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (x : CorrectionStep.CycleState (ActualCurrentParticularPhysical.Label B N0)) (hs : ∀ (l : ActualCurrentParticularPhysical.Label B N0), HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualCoreSupport.refinedCarrier (l.2, l.1)) (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l)) (n : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) (hX : (SlowBorelBase.cartesianChart CorrectionInitialization.ActualPrimary.h w).2.1 ∉ Set.Icc (NominalConeAssembly.activeLeft CorrectionInitialization.ActualPrimary.nominal) (NominalConeAssembly.activeRight CorrectionInitialization.ActualPrimary.nominal)) : ActualCurrentParticularPhysical.localPotential x n w = 0 ∧ ActualCurrentParticularPhysical.localPressure x n w = 0

theorem NavierStokes.ActualCurrentWaveSupport.current_local_axis_germs {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (x : CorrectionStep.CycleState (ActualCurrentParticularPhysical.Label B N0)) (hs : ∀ (l : ActualCurrentParticularPhysical.Label B N0), HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualCoreSupport.refinedCarrier (l.2, l.1)) (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l)) (n : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n) (haxis : PhysicalGraphBounds.radialProjection w = 0) : (ActualCurrentParticularPhysical.localPotential x n =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0) ∧ ActualCurrentParticularPhysical.localPressure x n =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.ActualCurrentWaveSupport.current_field_active_germs {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (x : CorrectionStep.CycleState (ActualCurrentParticularPhysical.Label B N0)) (hs : ∀ (l : ActualCurrentParticularPhysical.Label B N0), HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualCoreSupport.refinedCarrier (l.2, l.1)) (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l)) {N : ℕ} {qbig : ℝ} (hA : ValidDyadicBandCover.Compatible CorrectionInitialization.ActualPrimary.h N (ActualCurrentParticularPhysical.localPotential x)) (hP : ValidDyadicBandCover.Compatible CorrectionInitialization.ActualPrimary.h N (ActualCurrentParticularPhysical.localPressure x)) (hqbig : qbig ≤ ChartScales.Q N) {w : ProblemStatement.SpaceTime} (hw : w ∈ CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig) (hX : (SlowBorelBase.cartesianChart CorrectionInitialization.ActualPrimary.h w).2.1 ∉ Set.Icc (NominalConeAssembly.activeLeft CorrectionInitialization.ActualPrimary.nominal) (NominalConeAssembly.activeRight CorrectionInitialization.ActualPrimary.nominal)) : (ValidDyadicBandCover.field CorrectionInitialization.ActualPrimary.h N (ActualCurrentParticularPhysical.localPotential x) =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0) ∧ ValidDyadicBandCover.field CorrectionInitialization.ActualPrimary.h N (ActualCurrentParticularPhysical.localPressure x) =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

Sharp active-annulus zero germs of the actual representative. These are stronger than the common outer-support bound used at the terminal plane.

theorem NavierStokes.ActualCurrentWaveSupport.current_field_active_zero {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (x : CorrectionStep.CycleState (ActualCurrentParticularPhysical.Label B N0)) (hs : ∀ (l : ActualCurrentParticularPhysical.Label B N0), HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualCoreSupport.refinedCarrier (l.2, l.1)) (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l)) {N : ℕ} {qbig : ℝ} (hA : ValidDyadicBandCover.Compatible CorrectionInitialization.ActualPrimary.h N (ActualCurrentParticularPhysical.localPotential x)) (hP : ValidDyadicBandCover.Compatible CorrectionInitialization.ActualPrimary.h N (ActualCurrentParticularPhysical.localPressure x)) (hqbig : qbig ≤ ChartScales.Q N) {w : ProblemStatement.SpaceTime} (hw : w ∈ CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig) (hX : (SlowBorelBase.cartesianChart CorrectionInitialization.ActualPrimary.h w).2.1 ∉ Set.Icc (NominalConeAssembly.activeLeft CorrectionInitialization.ActualPrimary.nominal) (NominalConeAssembly.activeRight CorrectionInitialization.ActualPrimary.nominal)) : ValidDyadicBandCover.field CorrectionInitialization.ActualPrimary.h N (ActualCurrentParticularPhysical.localPotential x) w = 0 ∧ ValidDyadicBandCover.field CorrectionInitialization.ActualPrimary.h N (ActualCurrentParticularPhysical.localPressure x) w = 0

theorem NavierStokes.ActualCurrentWaveSupport.current_field_support {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (x : CorrectionStep.CycleState (ActualCurrentParticularPhysical.Label B N0)) (hs : ∀ (l : ActualCurrentParticularPhysical.Label B N0), HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualCoreSupport.refinedCarrier (l.2, l.1)) (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l)) {N : ℕ} {qbig : ℝ} (hA : ValidDyadicBandCover.Compatible CorrectionInitialization.ActualPrimary.h N (ActualCurrentParticularPhysical.localPotential x)) (hP : ValidDyadicBandCover.Compatible CorrectionInitialization.ActualPrimary.h N (ActualCurrentParticularPhysical.localPressure x)) (hqbig : qbig ≤ ChartScales.Q N) : MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h PhysicalStageSupport.actualOuterConstant qbig (ValidDyadicBandCover.field CorrectionInitialization.ActualPrimary.h N (ActualCurrentParticularPhysical.localPotential x)) ∧ MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h PhysicalStageSupport.actualOuterConstant qbig (ValidDyadicBandCover.field CorrectionInitialization.ActualPrimary.h N (ActualCurrentParticularPhysical.localPressure x))

theorem NavierStokes.ActualCurrentWaveSupport.current_field_axisZeroOn {B N0 : ℕ} (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (x : CorrectionStep.CycleState (ActualCurrentParticularPhysical.Label B N0)) (hs : ∀ (l : ActualCurrentParticularPhysical.Label B N0), HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (ActualCoreSupport.refinedCarrier (l.2, l.1)) (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l)) {N : ℕ} {qbig : ℝ} (hA : ValidDyadicBandCover.Compatible CorrectionInitialization.ActualPrimary.h N (ActualCurrentParticularPhysical.localPotential x)) (hqbig : qbig ≤ ChartScales.Q N) : GermCandidateAssembly.AxisZeroOn (MixedAxisPreservation.localDomain CorrectionInitialization.ActualPrimary.h qbig) (ValidDyadicBandCover.field CorrectionInitialization.ActualPrimary.h N (ActualCurrentParticularPhysical.localPotential x))