The actual initialized correction state

This consumer uses the single primary family selected by CorrectionInitialization.ActualPrimary, retaining its exact pressure, Gaussian errors and common-cover chart representations.

@[reducible, inline]

abbrev NavierStokes.ActualInitialization.Point : Type

Point: an abbreviation for LocalSignedRequest.Point.

Equations

• NavierStokes.ActualInitialization.Point = NavierStokes.LocalSignedRequest.Point

@[reducible, inline]

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

Index: an abbreviation for ActualPrimary.Label B N0 × Fin 2.

Equations

• NavierStokes.ActualInitialization.Index B N0 = (NavierStokes.CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2)

noncomputable def NavierStokes.ActualInitialization.primaryPiece {B N0 : ℕ} (l : Index B N0) : CorrectionInitialization.PrimaryPiece (Point × ℝ)

Primary piece, given by ActualPrimary.piece ActualPrimary.standardRegion l.2 l.1.

Equations

• NavierStokes.ActualInitialization.primaryPiece l = NavierStokes.CorrectionInitialization.ActualPrimary.piece NavierStokes.CorrectionInitialization.ActualPrimary.standardRegion l.2 l.1

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

Phase, given by (primaryPiece l).coefficients.phase n (x, 0).

Equations

• NavierStokes.ActualInitialization.phase l n x = (NavierStokes.ActualInitialization.primaryPiece l).coefficients.phase n (x, 0)

noncomputable def NavierStokes.ActualInitialization.angularMode {B N0 : ℕ} (l : Index B N0) (_n : ℕ) : ℤ

Angular mode, constructed using PrimaryGeometryAssembly.angularMode.

Equations

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

noncomputable def NavierStokes.ActualInitialization.primaryBlock {B N0 : ℕ} (l : Index B N0) : CorrectionState.HarmonicBlock Point

Primary block, given by (primaryPiece l).harmonicBlock (phase l) (angularMode l).

Equations

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

noncomputable def NavierStokes.ActualInitialization.tangentBlock {B N0 : ℕ} (l : Index B N0) : CorrectionState.HarmonicBlock Point

Tangent block, given by (primaryPiece l).tangentBlock (phase l) (angularMode l).

Equations

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

noncomputable def NavierStokes.ActualInitialization.curlBlock {B N0 : ℕ} (l : Index B N0) : CorrectionState.HarmonicBlock Point

Curl block, given by (primaryPiece l).differenceBlock (phase l) (angularMode l).

Equations

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

noncomputable def NavierStokes.ActualInitialization.gaussianBlock {B N0 : ℕ} (l : Index B N0) : CorrectionState.HarmonicBlock Point

Gaussian block, given by (primaryPiece l).excludedBlock (phase l) (angularMode l).

Equations

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

theorem NavierStokes.ActualInitialization.angularMode_ne_zero {B N0 : ℕ} (l : Index B N0) (n : ℕ) : angularMode l n ≠ 0

theorem NavierStokes.ActualInitialization.phase_split {B N0 : ℕ} (l : Index B N0) (n : ℕ) (x : Point) (theta : ℝ) : (primaryPiece l).coefficients.frequency n * (primaryPiece l).coefficients.phase n (x, theta) = (primaryPiece l).coefficients.frequency n * phase l n x + ↑(angularMode l n) * theta

theorem NavierStokes.ActualInitialization.cutoff_smooth {B N0 : ℕ} (l : Index B N0) (n : ℕ) : ContDiff ℝ (↑⊤) ((primaryPiece l).cutoff n)

theorem NavierStokes.ActualInitialization.amplitude_angle {B N0 : ℕ} (l : Index B N0) : ErrorHarmonics.AngleIndependent (primaryPiece l).coefficients.amplitude

theorem NavierStokes.ActualInitialization.cutoff_angle {B N0 : ℕ} (l : Index B N0) : ErrorHarmonics.AngleIndependent (primaryPiece l).cutoff

theorem NavierStokes.ActualInitialization.exact_amplitude_angle {B N0 : ℕ} (l : Index B N0) : ErrorHarmonics.AngleIndependent (primaryPiece l).exactCoefficients.amplitude

theorem NavierStokes.ActualInitialization.exact_pressure_angle {B N0 : ℕ} (l : Index B N0) : ErrorHarmonics.AngleIndependent (primaryPiece l).exactCoefficients.pressure

theorem NavierStokes.ActualInitialization.tangent_amplitude_angle {B N0 : ℕ} (l : Index B N0) : ErrorHarmonics.AngleIndependent ((primaryPiece l).coefficients.withCutoff (primaryPiece l).cutoff).amplitude

theorem NavierStokes.ActualInitialization.primaryBlock_represents {B N0 : ℕ} (l : Index B N0) : (primaryBlock l).oscillation = (primaryPiece l).velocity ∧ (primaryBlock l).oscillatoryPressure = (primaryPiece l).pressure

theorem NavierStokes.ActualInitialization.tangentBlock_represents {B N0 : ℕ} (l : Index B N0) : (tangentBlock l).oscillation = (primaryPiece l).tangentVelocity

theorem NavierStokes.ActualInitialization.curlBlock_represents {B N0 : ℕ} (l : Index B N0) : (curlBlock l).oscillation = (primaryPiece l).velocity - (primaryPiece l).tangentVelocity

theorem NavierStokes.ActualInitialization.gaussianBlock_represents {B N0 : ℕ} (l : Index B N0) : (gaussianBlock l).oscillation = (primaryPiece l).excluded

theorem NavierStokes.ActualInitialization.gaussian_mean_zero {B N0 : ℕ} (l : Index B N0) : CorrectionStep.angularMeanVector (primaryPiece l).excluded = 0

theorem NavierStokes.ActualInitialization.gaussian_angularContinuous {B N0 : ℕ} (l : Index B N0) : CorrectionStep.AngularContinuous (primaryPiece l).excluded

theorem NavierStokes.ActualInitialization.primaryBlock_band {B N0 : ℕ} (l : Index B N0) : (primaryBlock l).BandLimited 1

theorem NavierStokes.ActualInitialization.gaussianBlock_band {B N0 : ℕ} (l : Index B N0) : (gaussianBlock l).BandLimited 1

noncomputable def NavierStokes.ActualInitialization.coefficients (B N0 : ℕ) : CorrectionStep.CycleCoefficients (Index B N0)

Coefficients, bundling labels, blocks, gaussian, aliasCoefficients and the required compatibility proofs.

Equations

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

theorem NavierStokes.ActualInitialization.coefficients_band (B N0 : ℕ) : CorrectionStep.CoefficientBands (coefficients B N0)

theorem NavierStokes.ActualInitialization.gaussian_coefficientField {B N0 : ℕ} (l : Index B N0) : CorrectionStep.coefficientField (primaryBlock l) (gaussianBlock l).velocity = (primaryPiece l).excluded

noncomputable def NavierStokes.ActualInitialization.baseError (B : ℕ) : CorrectionState.Oscillation Point

Base error, given by ActualBaseResidual.baseError ActualPrimary.certificate ActualPrimary.modulation ActualPrimary.upper B.

Equations

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

noncomputable def NavierStokes.ActualInitialization.sourceState (B N0 : ℕ) : CorrectionState.State Point

Source state, given by bandSeed (coefficients B N0).labels primaryPiece (baseError B).

Equations

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

noncomputable def NavierStokes.ActualInitialization.primaryState (B N0 : ℕ) : CorrectionState.State Point

Primary state, given by VariableGaugeMean.reconstructState ActualPrimary.commonGauge (ActualPrimary.commonContext B) (sourceState B N0).

Equations

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

noncomputable def NavierStokes.ActualInitialization.axial : TorusInverse.Plane × TorusInverse.Plane

Axial, given by ((0, 1), 0).

Equations

• NavierStokes.ActualInitialization.axial = ((0, 1), 0)

noncomputable def NavierStokes.ActualInitialization.temporalState (B N0 : ℕ) : CorrectionState.State Point

Temporal state, constructed using VariableGaugeMean.temporalStageState.

Equations

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

noncomputable def NavierStokes.ActualInitialization.rankState (B N0 : ℕ) : CorrectionState.State Point

Rank state, constructed using VariableGaugeMean.rankStageState.

Equations

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

noncomputable def NavierStokes.ActualInitialization.initialState (B N0 : ℕ) : CorrectionState.State Point

Initial state, given by GaugeInitialization.retainPressureAlias ActualPrimary.commonGauge (ActualPrimary.commonContext B) (rankState B N0).

Equations

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

noncomputable def NavierStokes.ActualInitialization.initialAlias (B N0 : ℕ) : CorrectionStep.AxisymmetricAlias

Initial alias as an element of CorrectionStep.AxisymmetricAlias.

Equations

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

noncomputable def NavierStokes.ActualInitialization.initialCycleState (B N0 : ℕ) : CorrectionStep.CycleState (Index B N0)

The initial state and its actual harmonic data are constructed together; all later iterations retain these physical labels.

Equations

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

theorem NavierStokes.ActualInitialization.initialState_eq_bands (B N0 : ℕ) : initialState B N0 = CorrectionInitialization.GaugeInitialization.initializedBands CorrectionInitialization.ActualPrimary.commonGauge CorrectionInitialization.ActualPrimary.rankData CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h) axial (CorrectionInitialization.ActualPrimary.commonContext B) (coefficients B N0).labels primaryPiece (baseError B)

theorem NavierStokes.ActualInitialization.initialState_error_components (B N0 : ℕ) : (initialState B N0).errors.base = baseError B ∧ ((initialState B N0).errors.gaussian = LabelSumBounds.fieldSum (coefficients B N0).labels fun (l : Index B N0) => (primaryPiece l).excluded) ∧ (initialState B N0).errors.aliasError = fun (n : ℕ) (x : Point × ℝ) (i : Fin 3) => initialAlias B N0 n x.1 i

theorem NavierStokes.ActualInitialization.initialCycleState_represents (B N0 : ℕ) : CorrectionStep.CycleRepresentation (initialCycleState B N0).coefficients (initialCycleState B N0).state (initialCycleState B N0).axisymmetricAlias

theorem NavierStokes.ActualInitialization.primaryBlock_zeroMode {B N0 : ℕ} (l : Index B N0) : HarmonicWaveInteraction.ZeroMode (primaryBlock l)

theorem NavierStokes.ActualInitialization.primaryBlock_symmetric {B N0 : ℕ} (l : Index B N0) (n : ℕ) (i : Fin 3) : HarmonicFields.ConjugateSymmetric ((primaryBlock l).velocity n i)

theorem NavierStokes.ActualInitialization.sourceState_mean (B N0 : ℕ) : (sourceState B N0).mean = { radial := 0, angular := 0, axial := 0 }

theorem NavierStokes.ActualInitialization.initialState_oscillation (B N0 : ℕ) : (initialState B N0).oscillation = (sourceState B N0).oscillation

theorem NavierStokes.ActualInitialization.initialState_covariance (B N0 : ℕ) : (initialState B N0).covariance = (sourceState B N0).covariance

theorem NavierStokes.ActualInitialization.initialState_reconstructed (B N0 : ℕ) : VariableGaugeMean.reconstructState CorrectionInitialization.ActualPrimary.commonGauge (CorrectionInitialization.ActualPrimary.commonContext B) (initialState B N0) = initialState B N0

noncomputable def NavierStokes.ActualInitialization.initialResidualBlock {B N0 : ℕ} (l : Index B N0) : CorrectionState.HarmonicBlock Point

The actual nonconstant residual coefficients supplied to the first particular solve. The separate axisymmetric alias is removed only by the angular nonconstant projection.

Equations

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

theorem NavierStokes.ActualInitialization.initialResidualBlock_band {B N0 : ℕ} (l : Index B N0) : (initialResidualBlock l).BandLimited 2

theorem NavierStokes.ActualInitialization.initialResidualBlock_zeroMode {B N0 : ℕ} (l : Index B N0) : HarmonicWaveInteraction.ZeroMode (initialResidualBlock l)

theorem NavierStokes.ActualInitialization.initialResidualBlock_symmetric {B N0 : ℕ} (l : Index B N0) (n : ℕ) (i : Fin 3) : HarmonicFields.ConjugateSymmetric ((initialResidualBlock l).velocity n i)

theorem NavierStokes.ActualInitialization.zeroMean_residual_uniform {D : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ι → ℕ → D → ℝ} {κ α γ : ℝ} (c : CorrectionState.Context D) (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hR : ∀ x ∈ s.domain, 0 < c.operators.radius x) (u : CorrectionState.State D) (hm : u.mean = { radial := 0, angular := 0, axial := 0 }) (b : ι → CorrectionState.HarmonicBlock D) (G A : ι → HarmonicResidual.BlockCoefficients D) (hb : UniformHarmonicInteraction.UniformVelocity s P α b) (hzero : ∀ (l : ι), HarmonicWaveInteraction.ZeroMode (b l)) {M : ℕ} (hband : ∀ (l : ι), (b l).BandLimited M) (hphase : ∀ (l : ι) (n : ℕ), ContDiffOn ℝ (↑⊤) ((b l).phase n) s.domain) (hk : ∀ (l : ι) (n : ℕ), (b l).frequency n ≠ 0) (hdiv : ∀ (l : ι), HarmonicWaveInteraction.ModeSolenoidal s c (b l)) (hP0 : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P l n x) (hP1 : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, P l n x ≤ 1) (hA : ∀ (l : ι) (n : ℕ) (i : Fin 3) (j : ℤ), j ≠ 0 → (A l n i).coeff j = 0) (hlinear : UniformHarmonicInteraction.UniformVelocity s P γ fun (l : ι) => HarmonicWaveInteraction.linearGoodBlock c (b l) (b l) (G l)) (hγ : γ ≤ α + α - κ) : UniformHarmonicInteraction.UniformVelocity s P γ fun (l : ι) => HarmonicResidual.residualBlock c u (b l) (G l) (A l)

The actual nonlinear coefficient of a mean-zero state is its linear coefficient plus the solenoidal self-transport. Constants remain uniform before the spatial label.

noncomputable def NavierStokes.ActualInitialization.strip : WeightedClasses.StripData Point

Strip, given by BaseContextAssembly.nativeStrip ActualPrimary.nominal ActualPrimary.standardRegion.

Equations

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

noncomputable def NavierStokes.ActualInitialization.slowStrip : WeightedClasses.StripData TorusInverse.Plane

Slow strip, constructed using PhysicalMeanDomain.localSlowStripData.

Equations

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

noncomputable def NavierStokes.ActualInitialization.envelope {B N0 : ℕ} (l : Index B N0) : ℕ → Point → ℝ

Envelope, given by ActualPrimaryBounds.meanEnvelope (l.2,l.1).

Equations

• NavierStokes.ActualInitialization.envelope l = NavierStokes.ActualPrimaryBounds.meanEnvelope (l.2, l.1)

theorem NavierStokes.ActualInitialization.envelope_nonneg {B N0 : ℕ} (l : Index B N0) (n : ℕ) (x : Point) : 0 ≤ envelope l n x

theorem NavierStokes.ActualInitialization.envelope_le_one {B N0 : ℕ} (l : Index B N0) (n : ℕ) (x : Point) : envelope l n x ≤ 1

theorem NavierStokes.ActualInitialization.operators (B : ℕ) : MeanIncrementBounds.OperatorBounds strip (CorrectionInitialization.ActualPrimary.commonContext B).operators ChartScales.kappa

theorem NavierStokes.ActualInitialization.base_bounds (B : ℕ) : MeanIncrementBounds.BaseBounds strip (CorrectionInitialization.ActualPrimary.commonContext B).base

theorem NavierStokes.ActualInitialization.radius_pos (B : ℕ) (x : Point) (hx : x ∈ strip.domain) : 0 < (CorrectionInitialization.ActualPrimary.commonContext B).operators.radius x

theorem NavierStokes.ActualInitialization.strip_time (x : Point) (hx : x ∈ strip.domain) : 0 < x.2.1.1

theorem NavierStokes.ActualInitialization.tangent_coefficients_uniform (B N0 : ℕ) (i : Fin 3) (j : ℤ) : LabelSumBounds.UniformWaveClass strip envelope (1 / 2) fun (l : Index B N0) (n : ℕ) (x : Point) => ((tangentBlock l).velocity n i).coeff j x

theorem NavierStokes.ActualInitialization.pressure_coefficients_uniform (B N0 : ℕ) (j : ℤ) : LabelSumBounds.UniformWaveClass strip envelope 1 fun (l : Index B N0) (n : ℕ) (x : Point) => ((primaryBlock l).pressure n).coeff j x

The exact curl construction retains the same pressure coefficient.

noncomputable def NavierStokes.ActualInitialization.goodBlock {B N0 : ℕ} (l : Index B N0) : CorrectionState.HarmonicBlock Point

Good block, constructed using SignedWaveUpdate.coefficientBlock.

Equations

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

theorem NavierStokes.ActualInitialization.goodBlock_represents {B N0 : ℕ} (l : Index B N0) : (goodBlock l).oscillation = (primaryPiece l).linearGoodField

theorem NavierStokes.ActualInitialization.goodBlock_symmetric {B N0 : ℕ} (l : Index B N0) (n : ℕ) (i : Fin 3) : HarmonicFields.ConjugateSymmetric ((goodBlock l).velocity n i)

theorem NavierStokes.ActualInitialization.exact_frame_match {B N0 : ℕ} (l : Index B N0) : CorrectionStep.WaveFrameMatch (CorrectionInitialization.ActualPrimary.commonContext B) (primaryPiece l).strip (primaryPiece l).directions (primaryPiece l).exactCoefficients

theorem NavierStokes.ActualInitialization.radialDirection_smooth (B n : ℕ) : ContDiffOn ℝ (↑⊤) (CorrectionStep.radialDirection (CorrectionInitialization.ActualPrimary.commonContext B) n) (HarmonicResidual.liftDomain strip.domain)

theorem NavierStokes.ActualInitialization.axialDirection_smooth (B n : ℕ) : ContDiffOn ℝ (↑⊤) (CorrectionStep.axialDirection (CorrectionInitialization.ActualPrimary.commonContext B) n) (HarmonicResidual.liftDomain strip.domain)

theorem NavierStokes.ActualInitialization.linearBlockField_eq_piece {B N0 : ℕ} (l : Index B N0) (n : ℕ) (hphase : ContDiffOn ℝ (↑⊤) ((primaryPiece l).coefficients.phase n) (HarmonicResidual.liftDomain strip.domain)) (hv : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (x : Point × ℝ) => (primaryPiece l).exactCoefficients.amplitude n x i) (HarmonicResidual.liftDomain strip.domain)) (hp : ContDiffOn ℝ (↑⊤) ((primaryPiece l).exactCoefficients.pressure n) (HarmonicResidual.liftDomain strip.domain)) {x : Point × ℝ} (hx : x ∈ HarmonicResidual.liftDomain strip.domain) (i : Fin 3) : CorrectionStep.linearBlockField (CorrectionInitialization.ActualPrimary.commonContext B) (primaryBlock l) (primaryBlock l) n x i = (primaryPiece l).linearResidual n x i

The real harmonic operator is the operator of the literal corrected coefficient. Only regularity of those actual fields is used here.

theorem NavierStokes.ActualInitialization.initial_residual_uniform_of_primary (B N0 : ℕ) (hprimary : UniformHarmonicInteraction.UniformVelocity strip envelope (1 / 2) primaryBlock) (hlinear : UniformHarmonicInteraction.UniformVelocity strip envelope (7 / 10) fun (l : Index B N0) => HarmonicWaveInteraction.linearGoodBlock (CorrectionInitialization.ActualPrimary.commonContext B) (primaryBlock l) (primaryBlock l) (gaussianBlock l).velocity) (hphase : ∀ (l : Index B N0) (n : ℕ), ContDiffOn ℝ (↑⊤) (phase l n) strip.domain) (hdiv : ∀ (l : Index B N0), HarmonicWaveInteraction.ModeSolenoidal strip (CorrectionInitialization.ActualPrimary.commonContext B) (primaryBlock l)) {C : ℕ → Index B N0 → Set Point} (hNormal : ∀ (i : Fin 3), LocalizedWaveBounds.LocalUnweighted strip C 0 fun (n : ℕ) (l : Index B N0) (x : Point) => (HarmonicMeanInteraction.slowNormal (CorrectionInitialization.ActualPrimary.commonContext B) ⋯ ⋯ (phase l) n x).ofLp i) (hFreq : LocalizedWaveBounds.LocalUnweighted strip C (-(1 / 2)) fun (n : ℕ) (l : Index B N0) (x : Point) => (primaryBlock l).frequency n) (hAng : LocalizedWaveBounds.LocalUnweighted strip C (-(1 / 2)) fun (n : ℕ) (l : Index B N0) (x : Point) => ↑((primaryBlock l).angularFrequency n)) (hz : ∀ (n : ℕ) (l : Index B N0), ∀ x ∈ strip.domain, x ∉ C n l → ∀ (i : Fin 3) (j : ℤ), j ≠ 0 → ((primaryBlock l).velocity n i).coeff j =ᶠ[nhds x] fun (x : Point) => 0) (hmean : CorrectionState.CumulativeBounds strip (initialState B N0)) : UniformHarmonicInteraction.UniformVelocity strip envelope (7 / 10) initialResidualBlock

The actual initialized mean changes the primary residual by a term of order at least nine tenths. The retained axisymmetric aliases do not enter the nonzero harmonic coefficients.

noncomputable def NavierStokes.ActualInitialization.zeroBlock {B N0 : ℕ} (l : Index B N0) : CorrectionState.HarmonicBlock Point

Zero block, given by { primaryBlock l with velocity := 0, pressure := 0 }.

Equations

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

theorem NavierStokes.ActualInitialization.zeroBlock_oscillation {B N0 : ℕ} (l : Index B N0) : (zeroBlock l).oscillation = 0

theorem NavierStokes.ActualInitialization.linearGood_uniform_of_identity (B N0 : ℕ) {γ : ℝ} (hprimary : UniformHarmonicInteraction.UniformVelocity strip envelope (1 / 2) primaryBlock) (hphase : ∀ (l : Index B N0) (n : ℕ), ContDiffOn ℝ (↑⊤) ((primaryPiece l).coefficients.phase n) (HarmonicResidual.liftDomain strip.domain)) (hamp : ∀ (l : Index B N0) (n : ℕ) (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (x : Point × ℝ) => (primaryPiece l).exactCoefficients.amplitude n x i) (HarmonicResidual.liftDomain strip.domain)) (hpressure : ∀ (l : Index B N0) (n : ℕ), ContDiffOn ℝ (↑⊤) ((primaryPiece l).exactCoefficients.pressure n) (HarmonicResidual.liftDomain strip.domain)) (hgood : UniformHarmonicInteraction.UniformVelocity strip envelope γ goodBlock) (hidentity : ∀ (l : Index B N0) (n : ℕ), ∀ x ∈ HarmonicResidual.liftDomain strip.domain, ∀ (i : Fin 3), (primaryPiece l).linearResidual n x i = (primaryPiece l).linearGoodField n x i + (primaryPiece l).excluded n x i) : UniformHarmonicInteraction.UniformVelocity strip envelope γ fun (l : Index B N0) => HarmonicWaveInteraction.linearGoodBlock (CorrectionInitialization.ActualPrimary.commonContext B) (primaryBlock l) (primaryBlock l) (gaussianBlock l).velocity

Extract the actual linear-good coefficient from the proved primary field identity, retaining its literal Gaussian coefficient.

noncomputable def NavierStokes.ActualInitialization.patch : SignedStressPrimitive.Patch

The signed request uses the same active annulus and reserved mean patch.

Equations

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

noncomputable def NavierStokes.ActualInitialization.geometry : SignedMeanGain.Geometry

All stages use one moving strip, common index, and pressure gauge.

Equations

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

theorem NavierStokes.ActualInitialization.geometry_strip : geometry.strip = strip

theorem NavierStokes.ActualInitialization.geometry_slowStrip : geometry.slowStrip = slowStrip

theorem NavierStokes.ActualInitialization.geometry_operators (B : ℕ) : geometry.operators = (CorrectionInitialization.ActualPrimary.commonContext B).operators

theorem NavierStokes.ActualInitialization.initial_primitive (B N0 : ℕ) : MeanStateRegularity.PrimitiveData geometry.region geometry.patch.a geometry.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) (initialState B N0)

theorem NavierStokes.ActualInitialization.initial_on_overlap (B N0 n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) : PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain (ActualInitialCoherence.overlap n m)) (GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m) (GaugeStateCoherence.bandScale n m) (initialState B N0) (initialState B N0) n m

theorem NavierStokes.ActualInitialization.initial_oscillation_smooth (B N0 : ℕ) : WaveStateRegularity.AngularSmooth geometry.domain (initialState B N0).oscillation

theorem NavierStokes.ActualInitialization.initial_oscillation_support (B N0 : ℕ) : WaveStateRegularity.WaveSupport geometry.region geometry.patch.a geometry.patch.b (initialState B N0).oscillation

theorem NavierStokes.ActualInitialization.initial_oscillation_periodic (B N0 : ℕ) : CorrectionStep.OscillationPeriodic geometry.region.carrier (initialState B N0).oscillation

theorem NavierStokes.ActualInitialization.initial_base_angular (B N0 n : ℕ) (x : Point) (hx : x ∈ geometry.domain) (i : Fin 3) : Continuous fun (theta : ℝ) => (initialState B N0).errors.base n (x, theta) i

theorem NavierStokes.ActualInitialization.phase_smooth_full {B N0 : ℕ} (l : Index B N0) (n : ℕ) : ContDiffOn ℝ (↑⊤) ((primaryPiece l).coefficients.phase n) (HarmonicResidual.liftDomain strip.domain)

theorem NavierStokes.ActualInitialization.phase_smooth {B N0 : ℕ} (l : Index B N0) (n : ℕ) : ContDiffOn ℝ (↑⊤) (phase l n) strip.domain

theorem NavierStokes.ActualInitialization.exact_amplitude_smooth_full {B N0 : ℕ} (l : Index B N0) (n : ℕ) (i : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (x : Point × ℝ) => (primaryPiece l).exactCoefficients.amplitude n x i) (HarmonicResidual.liftDomain strip.domain)

theorem NavierStokes.ActualInitialization.exact_pressure_smooth_full {B N0 : ℕ} (l : Index B N0) (n : ℕ) : ContDiffOn ℝ (↑⊤) ((primaryPiece l).exactCoefficients.pressure n) (HarmonicResidual.liftDomain strip.domain)

theorem NavierStokes.ActualInitialization.initial_meanGood (B N0 n : ℕ) {x : Point} (hT : 0 < x.2.1.1) (i : Fin 3) : (initialState B N0).meanGoodResidual (CorrectionInitialization.ActualPrimary.commonContext B) n x i = (initialState B N0).reducedMeanResidual (CorrectionInitialization.ActualPrimary.commonContext B) n x i - initialAlias B N0 n x i

theorem NavierStokes.ActualInitialization.initialAlias_radial (B N0 n : ℕ) (x : Point) : initialAlias B N0 n x 0 = VariableGaugeMean.pressureAliasState CorrectionInitialization.ActualPrimary.commonGauge (CorrectionInitialization.ActualPrimary.commonContext B) (initialState B N0) n (x, 0) 0

theorem NavierStokes.ActualInitialization.initial_radial_mean_class (B N0 : ℕ) {alpha : ℝ} (hdebt : WeightedClasses.UnweightedClass slowStrip alpha (CorrectionState.pressureDefect (CorrectionInitialization.ActualPrimary.commonContext B) (initialState B N0))) : WeightedClasses.MeanClass strip alpha fun (n : ℕ) (x : Point) => (initialState B N0).meanGoodResidual (CorrectionInitialization.ActualPrimary.commonContext B) n x 0

The remaining radial mean is controlled by the actual measured pressure debt.

theorem NavierStokes.ActualInitialization.smooth_conjugatePair {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {f : D → ℂ} (hf : ContDiffOn ℝ (↑⊤) f U) (j : ℤ) : HarmonicResidual.SmoothCoefficients U (ErrorHarmonics.conjugatePair j f)

theorem NavierStokes.ActualInitialization.primary_coefficients_smooth {B N0 : ℕ} (l : Index B N0) (n : ℕ) (i : Fin 3) : HarmonicResidual.SmoothCoefficients strip.domain ((primaryBlock l).velocity n i)

theorem NavierStokes.ActualInitialization.primary_pressure_smooth {B N0 : ℕ} (l : Index B N0) (n : ℕ) : HarmonicResidual.SmoothCoefficients strip.domain ((primaryBlock l).pressure n)

theorem NavierStokes.ActualInitialization.gaussian_coefficients_smooth {B N0 : ℕ} (l : Index B N0) (n : ℕ) (i : Fin 3) : HarmonicResidual.SmoothCoefficients strip.domain ((gaussianBlock l).velocity n i)

theorem NavierStokes.ActualInitialization.primary_modeSolenoidal {B N0 : ℕ} (l : Index B N0) : HarmonicWaveInteraction.ModeSolenoidal strip (CorrectionInitialization.ActualPrimary.commonContext B) (primaryBlock l)

Harmonic solenoidality is extracted from the actual corrected curl.

theorem NavierStokes.ActualInitialization.primary_pressure_zero {B N0 : ℕ} (l : Index B N0) (n : ℕ) : ((primaryBlock l).pressure n).coeff 0 = 0

theorem NavierStokes.ActualInitialization.primary_tangent_carrier {B N0 : ℕ} (l : Index B N0) : CorrectionStep.SameCarrier (primaryBlock l) (tangentBlock l)

theorem NavierStokes.ActualInitialization.initial_extraction_regular (B N0 n : ℕ) : LocalResidualGrouping.ExtractionRegular strip.domain (CorrectionInitialization.ActualPrimary.commonContext B) (initialState B N0) (coefficients B N0).labels (coefficients B N0).blocks (coefficients B N0).gaussian (coefficients B N0).aliasCoefficients n

All assumptions of local harmonic extraction follow from the actual initial state and the proved support separation of its primary pieces.

theorem NavierStokes.ActualInitialization.initial_goodWave_grouped (B N0 n : ℕ) {x : Point × ℝ} (hx : x.1 ∈ strip.domain) (i : Fin 3) : CorrectionStep.fullGoodWaveResidual (CorrectionInitialization.ActualPrimary.commonContext B) (initialState B N0) n x i = ∑ l ∈ (coefficients B N0).labels n, (initialResidualBlock l).oscillation n x i

theorem NavierStokes.ActualInitialization.local_slice_union {D E I J K : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {C : ℕ → J × K → Set (D × ℝ)} {alpha : ℝ} {f : J → ℕ → D × ℝ → E} (e : I → J) (hs : ∀ (l : J) (n : ℕ), ContDiffOn ℝ (↑⊤) (f l n) (HarmonicWaveInteraction.productStrip s).domain) (hf : LocalizedWaveBounds.LocalUnweighted (HarmonicWaveInteraction.productStrip s) C alpha fun (n : ℕ) (i : J × K) (x : D × ℝ) => f i.1 n x) : LocalizedWaveBounds.LocalUnweighted s (fun (n : ℕ) (i : I) => {x : D | ∃ (k : K), (x, 0) ∈ C n (e i, k)}) alpha fun (n : ℕ) (i : I) (x : D) => f (e i) n (x, 0)

Restriction to zero angle and a union of actual copy cells preserve the constants chosen before labels and copies.

noncomputable def NavierStokes.ActualInitialization.fullNormal {B N0 : ℕ} (l : Index B N0) (n : ℕ) : Point × ℝ → ProblemStatement.Space

Full normal, given by (primaryPiece l).coefficients.normal (primaryPiece l).strip (primaryPiece l).directions n.

Equations

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

theorem NavierStokes.ActualInitialization.fullNormal_smooth {B N0 : ℕ} (l : Index B N0) (n : ℕ) : ContDiffOn ℝ (↑⊤) (fullNormal l n) (HarmonicWaveInteraction.productStrip strip).domain

theorem NavierStokes.ActualInitialization.phase_slice_derivative {B N0 : ℕ} (l : Index B N0) (n : ℕ) {x : Point} (hx : x ∈ strip.domain) (v : Point) : (fderiv ℝ (phase l n) x) v = (fderiv ℝ ((primaryPiece l).coefficients.phase n) (x, 0)) (v, 0)

theorem NavierStokes.ActualInitialization.slowNormal_component {B N0 : ℕ} (l : Index B N0) (n : ℕ) {x : Point} (hx : x ∈ strip.domain) (i : Fin 3) : (HarmonicMeanInteraction.slowNormal (CorrectionInitialization.ActualPrimary.commonContext B) ⋯ ⋯ (phase l) n x).ofLp i = if i = 1 then 0 else (fullNormal l n (x, 0)).ofLp i

theorem NavierStokes.ActualInitialization.phase_angular_affine {B N0 : ℕ} (l : Index B N0) (n : ℕ) : CopyAngularInvariance.AffinePhase (0, 1) (↑(angularMode l n) / (primaryPiece l).coefficients.frequency n) ((primaryPiece l).coefficients.phase n)

theorem NavierStokes.ActualInitialization.angularMode_from_normal {B N0 : ℕ} (l : Index B N0) (n : ℕ) {x : Point} (hx : x ∈ strip.domain) : ↑(angularMode l n) = (primaryPiece l).coefficients.frequency n * x.1 * (fullNormal l n (x, 0)).ofLp 1

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

Mean control cell, given by {x | ∃ k : TorusInverse.Frequency, (x,0) ∈ ActualPrimaryBounds.controlCell n ((l.2,l.1), k)}.

Equations

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

theorem NavierStokes.ActualInitialization.fullNormal_slice_local (B N0 : ℕ) (i : Fin 3) : LocalizedWaveBounds.LocalUnweighted strip meanControlCell 0 fun (n : ℕ) (l : Index B N0) (x : Point) => (fullNormal l n (x, 0)).ofLp i

theorem NavierStokes.ActualInitialization.slowNormal_local (B N0 : ℕ) (i : Fin 3) : LocalizedWaveBounds.LocalUnweighted strip meanControlCell 0 fun (n : ℕ) (l : Index B N0) (x : Point) => (HarmonicMeanInteraction.slowNormal (CorrectionInitialization.ActualPrimary.commonContext B) ⋯ ⋯ (phase l) n x).ofLp i

theorem NavierStokes.ActualInitialization.frequency_local (B N0 : ℕ) : LocalizedWaveBounds.LocalUnweighted strip meanControlCell (-(1 / 2)) fun (n : ℕ) (l : Index B N0) (x : Point) => (primaryBlock l).frequency n

theorem NavierStokes.ActualInitialization.angularFrequency_local (B N0 : ℕ) : LocalizedWaveBounds.LocalUnweighted strip meanControlCell (-(1 / 2)) fun (n : ℕ) (l : Index B N0) (x : Point) => ↑((primaryBlock l).angularFrequency n)

theorem NavierStokes.ActualInitialization.primary_zero_germ_outside_control {B N0 : ℕ} (n : ℕ) (l : Index B N0) {x : Point} (hx : x ∈ strip.domain) (hc : x ∉ meanControlCell n l) (i : Fin 3) (j : ℤ) : ((primaryBlock l).velocity n i).coeff j =ᶠ[nhds x] fun (x : Point) => 0

theorem NavierStokes.ActualInitialization.primary_coefficients_uniform (B N0 : ℕ) (i : Fin 3) (j : ℤ) : LabelSumBounds.UniformWaveClass strip envelope (1 / 2) fun (l : Index B N0) (n : ℕ) (x : Point) => ((primaryBlock l).velocity n i).coeff j x

theorem NavierStokes.ActualInitialization.primary_uniform (B N0 : ℕ) : UniformHarmonicInteraction.UniformVelocity strip envelope (1 / 2) primaryBlock

theorem NavierStokes.ActualInitialization.difference_coefficients_uniform (B N0 : ℕ) (i : Fin 3) (j : ℤ) : LabelSumBounds.UniformWaveClass strip envelope (17 / 25) fun (l : Index B N0) (n : ℕ) (x : Point) => ((primaryBlock l).velocity n i).coeff j x - ((tangentBlock l).velocity n i).coeff j x

theorem NavierStokes.ActualInitialization.good_coefficients_uniform (B N0 : ℕ) (i : Fin 3) (j : ℤ) : LabelSumBounds.UniformWaveClass strip envelope (7 / 10) fun (l : Index B N0) (n : ℕ) (x : Point) => ((goodBlock l).velocity n i).coeff j x

theorem NavierStokes.ActualInitialization.linearGood_uniform (B N0 : ℕ) : UniformHarmonicInteraction.UniformVelocity strip envelope (7 / 10) fun (l : Index B N0) => HarmonicWaveInteraction.linearGoodBlock (CorrectionInitialization.ActualPrimary.commonContext B) (primaryBlock l) (primaryBlock l) (gaussianBlock l).velocity

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

Label carrier, given by ActualInitialExcluded.labelCarrier (l.2, l.1) n.

Equations

• NavierStokes.ActualInitialization.labelCarrier l n = NavierStokes.ActualInitialExcluded.labelCarrier (l.2, l.1) n

theorem NavierStokes.ActualInitialization.labelCarrier_closed {B N0 : ℕ} (l : Index B N0) (n : ℕ) : IsClosed (labelCarrier l n)

theorem NavierStokes.ActualInitialization.native_source_core {B N0 : ℕ} (l : Index B N0) (x : ActualSignedGeometry.Native) (hg : CorrectionInitialization.ActualPrimary.gaussian l.1 x ≠ 0) (hr : CorrectionInitialization.ActualPrimary.rawVelocity l.2 l.1 x ≠ 0) : x ∈ ActualGaussianCoverage.actualSourceCore CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared l.1

theorem NavierStokes.ActualInitialization.cut_amplitude_source_support {B N0 : ℕ} (l : Index B N0) (n : ℕ) : Function.support (((primaryPiece l).coefficients.withCutoff (primaryPiece l).cutoff).amplitude n) ⊆ Prod.fst ⁻¹' labelCarrier l n

theorem NavierStokes.ActualInitialization.cut_pressure_source_support {B N0 : ℕ} (l : Index B N0) (n : ℕ) : Function.support ((primaryPiece l).exactCoefficients.pressure n) ⊆ Prod.fst ⁻¹' labelCarrier l n

theorem NavierStokes.ActualInitialization.primary_velocity_zero_outside_source {B N0 : ℕ} (l : Index B N0) (n : ℕ) {x : Point} (hx : x ∉ labelCarrier l n) (theta : ℝ) : (primaryBlock l).oscillation n (x, theta) = 0

theorem NavierStokes.ActualInitialization.primary_pressure_zero_outside_source {B N0 : ℕ} (l : Index B N0) (n : ℕ) {x : Point} (hx : x ∉ labelCarrier l n) (theta : ℝ) : (primaryBlock l).oscillatoryPressure n (x, theta) = 0

theorem NavierStokes.ActualInitialization.gaussian_velocity_zero_outside_source {B N0 : ℕ} (l : Index B N0) (n : ℕ) {x : Point} (hx : x ∉ labelCarrier l n) (theta : ℝ) : (gaussianBlock l).oscillation n (x, theta) = 0

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

theorem NavierStokes.ActualInitialization.gaussian_coefficients_flat (B N0 : ℕ) (beta : ℝ) (i : Fin 3) (j : ℤ) : LabelSumBounds.UniformClass strip (fun (x : Index B N0) (x_1 : ℕ) (x_2 : Point) => √(strip.zeta x_2)) beta fun (l : Index B N0) (n : ℕ) (x : Point) => ((gaussianBlock l).velocity n i).coeff j x

theorem NavierStokes.ActualInitialization.primary_pressure_symmetric {B N0 : ℕ} (l : Index B N0) (n : ℕ) : HarmonicFields.ConjugateSymmetric ((primaryBlock l).pressure n)

theorem NavierStokes.ActualInitialization.gaussian_coefficients_symmetric {B N0 : ℕ} (l : Index B N0) (n : ℕ) (i : Fin 3) : HarmonicFields.ConjugateSymmetric ((gaussianBlock l).velocity n i)

theorem NavierStokes.ActualInitialization.absolute_exact_amplitude_smooth {B N0 : ℕ} (l : Index B N0) : ContDiffOn ℝ (↑⊤) (ActualPrimaryCoherence.absoluteExactAmplitude l.2 l.1) ActualPrimaryCoherence.positiveAbsolute

theorem NavierStokes.ActualInitialization.exact_amplitude_positive_smooth {B N0 : ℕ} (l : Index B N0) (n : ℕ) : ContDiffOn ℝ (↑⊤) ((primaryPiece l).exactCoefficients.amplitude n) ActualPrimaryCoherence.positiveChart

theorem NavierStokes.ActualInitialization.exact_pressure_positive_smooth {B N0 : ℕ} (l : Index B N0) (n : ℕ) : ContDiffOn ℝ (↑⊤) ((primaryPiece l).exactCoefficients.pressure n) ActualPrimaryCoherence.positiveChart

theorem NavierStokes.ActualInitialization.gaussian_positive_smooth {B N0 : ℕ} (l : Index B N0) (n : ℕ) : ContDiffOn ℝ (↑⊤) (ActualInitialExcluded.chartGaussian (l.2, l.1) n) ActualPrimaryCoherence.positiveChart

theorem NavierStokes.ActualInitialization.primary_coefficients_smooth_domain {B N0 : ℕ} (l : Index B N0) (n : ℕ) (i : Fin 3) (j : ℤ) : ContDiffOn ℝ (↑⊤) (((primaryBlock l).velocity n i).coeff j) geometry.domain

theorem NavierStokes.ActualInitialization.pressure_coefficients_smooth_domain {B N0 : ℕ} (l : Index B N0) (n : ℕ) (j : ℤ) : ContDiffOn ℝ (↑⊤) (((primaryBlock l).pressure n).coeff j) geometry.domain

theorem NavierStokes.ActualInitialization.gaussian_coefficients_smooth_domain {B N0 : ℕ} (l : Index B N0) (n : ℕ) (i : Fin 3) (j : ℤ) : ContDiffOn ℝ (↑⊤) (((gaussianBlock l).velocity n i).coeff j) geometry.domain

theorem NavierStokes.ActualInitialization.initial_oscillatoryPressure_smooth (B N0 n : ℕ) : ContDiffOn ℝ (↑⊤) ((initialState B N0).oscillatoryPressure n) (geometry.domain ×ˢ Set.univ)

theorem NavierStokes.ActualInitialization.initial_cumulative (B N0 : ℕ) : CorrectionState.CumulativeBounds strip (initialState B N0)

theorem NavierStokes.ActualInitialization.initial_mean (B N0 : ℕ) : CorrectionState.MeanResidualBounds strip (1 / 5) (CorrectionInitialization.ActualPrimary.commonContext B) (initialState B N0)

theorem NavierStokes.ActualInitialization.initial_debt (B N0 : ℕ) : CorrectionState.DefectBounds slowStrip (1 / 5) (CorrectionInitialization.ActualPrimary.commonContext B) (initialState B N0)

theorem NavierStokes.ActualInitialization.initial_zeroMasses (B N0 : ℕ) : GaugeMassPreservation.ZeroMassesOn geometry.region.carrier (initialState B N0)

theorem NavierStokes.ActualInitialization.initial_covariance (B N0 : ℕ) (i j : Fin 3) : WeightedClasses.MeanClass strip 1 ((initialState B N0).covariance i j)

theorem NavierStokes.ActualInitialization.initial_axis_flat (B N0 : ℕ) (beta : ℝ) : WeightedClasses.MeanClass strip beta (initialAlias B N0)

theorem NavierStokes.ActualInitialization.initial_meanHypotheses (B N0 : ℕ) : LiftedMeanResidual.MeanHypotheses strip.domain (CorrectionInitialization.ActualPrimary.commonContext B) (initialState B N0)

theorem NavierStokes.ActualInitialization.initial_residual_uniform (B N0 : ℕ) : UniformHarmonicInteraction.UniformVelocity strip envelope (7 / 10) initialResidualBlock

theorem NavierStokes.ActualInitialization.gaussianBlock_zeroMode {B N0 : ℕ} (l : Index B N0) : HarmonicWaveInteraction.ZeroMode (gaussianBlock l)

theorem NavierStokes.ActualInitialization.initial_gaussian_mean_zero (B N0 : ℕ) : CorrectionStep.angularMeanVector (initialState B N0).errors.gaussian = 0

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

The literal same-choice initialized state satisfies every analytic, support, regularity, and representation field used by the correction cycle.

theorem NavierStokes.ActualInitialization.initial_mean_all_components (B N0 : ℕ) (i : Fin 3) : WeightedClasses.MeanClass strip (6 / 5) fun (n : ℕ) (x : Point) => (initialState B N0).meanGoodResidual (CorrectionInitialization.ActualPrimary.commonContext B) n x i

The radial component is included: all three actual good mean residuals have exponent six fifths.

theorem NavierStokes.ActualInitialization.initial_fullDivergence (B N0 n : ℕ) {x : Point × ℝ} (hx : x.1 ∈ strip.domain) : CorrectionStep.fullDivergence (CorrectionInitialization.ActualPrimary.commonContext B) (initialState B N0) n x = 0

theorem NavierStokes.ActualInitialization.initial_fullResidual (B N0 n : ℕ) {x : Point × ℝ} (hx : x.1 ∈ strip.domain) (i : Fin 3) : CorrectionStep.fullResidual (CorrectionInitialization.ActualPrimary.commonContext B) (initialState B N0) n x i = ∑ l ∈ (coefficients B N0).labels n, (initialResidualBlock l).oscillation n x i + (initialState B N0).meanGoodResidual (CorrectionInitialization.ActualPrimary.commonContext B) n x.1 i + (initialState B N0).errors.total n x i

Exact decomposition of the actual differentiated PDE, with both the mean and every stored excluded error retained.

theorem NavierStokes.ActualInitialization.initial_excluded_all_gains (B N0 : ℕ) (beta : ℝ) : WeightedClasses.UnweightedClass (HarmonicWaveInteraction.productStrip strip) beta (initialState B N0).errors.total

All derivatives of the complete stored excluded error satisfy estimates for every power on the full angular and auxiliary lift.

theorem NavierStokes.ActualInitialization.initial_excluded_component_all_gains (B N0 : ℕ) (beta : ℝ) (i : Fin 3) : WeightedClasses.UnweightedClass (HarmonicWaveInteraction.productStrip strip) beta fun (n : ℕ) (x : Point × ℝ) => (initialState B N0).errors.total n x i