Coherence of the actual correction recurrence

The incoming chart comparisons retain every radial, free auxiliary and angular variable. The actual initialized state and labeled coefficients start the induction together. The two literal wave constructions supply the transport used by the mean, pressure, and alias operations.

Full-fiber coherence of the actual signed Gaussian error

The differentiated native cutoff is transported before the copy sum is taken. The source complement is retained, and the same copy index is used throughout. The final field is the actual conjugate-pair Gaussian block, with its full angular variable.

theorem NavierStokes.ActualSignedGaussianCoherence.fast_cutoff_equiv {D E I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃L[ℝ] E) (d : LinearWaveBounds.GraphDirections D) (dr : LinearWaveBounds.GraphDirections E) (a : PeriodizedWaveBounds.CopyData D I) (b : PeriodizedWaveBounds.CopyData E I) (n m : ℕ) (rate : ℝ) (i : I) (x : D) (hcutoff : a.cutoff n i = fun (y : D) => b.cutoff m i (e y)) (hfast : e (d.fastField n x) = rate • dr.fastField m (e x)) : d.Dfast (fun (j : ℕ) => a.cutoff j i) n x = rate * dr.Dfast (fun (j : ℕ) => b.cutoff j i) m (e x)

The invertible chart transports the actual directional derivative, including the totalized derivative at a nonsmooth point.

theorem NavierStokes.ActualSignedGaussianCoherence.globalGaussian_equiv {D E I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃L[ℝ] E) (d : LinearWaveBounds.GraphDirections D) (dr : LinearWaveBounds.GraphDirections E) (a : PeriodizedWaveBounds.CopyData D I) (b : PeriodizedWaveBounds.CopyData E I) (n m : ℕ) (rate c : ℝ) (x : D) (hcutoff : ∀ (i : I), a.cutoff n i = fun (y : D) => b.cutoff m i (e y)) (hfast : e (d.fastField n x) = rate • dr.fastField m (e x)) (hamplitude : ∀ (i : I), dr.Dfast (fun (j : ℕ) => b.cutoff j i) m (e x) ≠ 0 → a.amplitude n i x = c • b.amplitude m i (e x)) (hsource : a.source n x = (rate * c) • b.source m (e x)) : a.globalGaussian d n x = (rate * c) • b.globalGaussian dr m (e x)

Exact transport of the computed Gaussian error. Only copies with a nonzero differentiated reference cutoff require an amplitude comparison.

theorem NavierStokes.ActualSignedGaussianCoherence.gaussianWeight_swap (exponent : ℝ) (n m : ℕ) : (GaugeStateCoherence.bandVelocityScale exponent n m * GaugeStateCoherence.bandVelocityScale exponent n m * GaugeStateCoherence.bandScale n m)⁻¹ = GaugeStateCoherence.bandVelocityScale exponent m n * GaugeStateCoherence.bandVelocityScale exponent m n * GaugeStateCoherence.bandScale m n

Exchanging the two bands inverts the physical Gaussian weight.

theorem NavierStokes.ActualSignedGaussianCoherence.gaussianBlock_formula {B N0 : ℕ} (l : ActualSignedStageControls.SignedLabel B N0) (s : WeightedClasses.StripData LocalSignedRequest.Point) (request : ℕ → LocalSignedRequest.Point × ℝ → SignedWaveUpdate.Vec2) (n : ℕ) (x : LocalSignedRequest.Point) (theta : ℝ) (i : Fin 3) : ((ActualSignedStageControls.parameters l).gaussianBlock s request).oscillation n (x, theta) i = (((ActualSignedStageControls.parameters l).copyData s request).globalGaussian (ActualSignedStageControls.directions B) n (x, 0) i * HarmonicFields.character 1 ((CorrectionInitialization.ActualPrimary.chartCoefficients l.2 l.1).frequency n * (CorrectionInitialization.ActualPrimary.chartCoefficients l.2 l.1).phase n (x, 0) + ↑((ActualSignedStageControls.parameters l).angularFrequency n) * theta)).re

Expansion of the literal Gaussian block at an arbitrary angle. The coefficient is the actual periodized error on the zero-angle section.

theorem NavierStokes.ActualSignedGaussianCoherence.gaussian_transport_of_request {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State ActualSignedCoherence.Point) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (x : ActualSignedCoherence.FullPoint) (hR : ActualSignedCoherence.request B u n x = ActualSignedCoherence.coefficientWeight n m ^ 2 • ActualSignedCoherence.request B u m ((ActualSignedCoherence.chart n m k) x)) : (ActualSignedCoherence.copies l u).globalGaussian (ActualSignedStageControls.directions B) n x = (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m * GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m * GaugeStateCoherence.bandScale n m) • (ActualSignedCoherence.copies l u).globalGaussian (ActualSignedStageControls.directions B) m ((ActualSignedCoherence.chart n m k) x)

The signed request is the only coefficient input to this comparison. The same literal native copy and cutoff occur on both sides.

theorem NavierStokes.ActualSignedGaussianCoherence.gaussian_transport {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State ActualSignedCoherence.Point) (H : MeanStateRegularity.PrimitiveData ActualInitialization.geometry.region ActualInitialization.geometry.patch.a ActualInitialization.geometry.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hfixed : (VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u).pressure = u.pressure) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (HS : 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) u u n m) (x : ActualSignedCoherence.FullPoint) (hx : x.1.2.1 ∈ ActualInitialCoherence.overlap n m) : (ActualSignedCoherence.copies l u).globalGaussian (ActualSignedStageControls.directions B) n x = (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m * GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m * GaugeStateCoherence.bandScale n m) • (ActualSignedCoherence.copies l u).globalGaussian (ActualSignedStageControls.directions B) m ((ActualSignedCoherence.chart n m k) x)

Full-fiber covariance derived from the actual incoming state and primitive identities. No covariance of a signed output is assumed.

theorem NavierStokes.ActualSignedGaussianCoherence.gaussian_transport_symm {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State ActualSignedCoherence.Point) (H : MeanStateRegularity.PrimitiveData ActualInitialization.geometry.region ActualInitialization.geometry.patch.a ActualInitialization.geometry.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hfixed : (VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u).pressure = u.pressure) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (HS : 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) u u n m) (x : ActualSignedCoherence.FullPoint) (hx : ((ActualSignedCoherence.chart n m k).symm x).1.2.1 ∈ ActualInitialCoherence.overlap n m) : (ActualSignedCoherence.copies l u).globalGaussian (ActualSignedStageControls.directions B) m x = (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h m n * GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h m n * GaugeStateCoherence.bandScale m n) • (ActualSignedCoherence.copies l u).globalGaussian (ActualSignedStageControls.directions B) n ((ActualSignedCoherence.chart n m k).symm x)

Reverse transport of the actual complex Gaussian coefficient on the image of the same overlap, with the reciprocal physical weight.

theorem NavierStokes.ActualSignedGaussianCoherence.gaussianBlock_transport {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State ActualSignedCoherence.Point) (H : MeanStateRegularity.PrimitiveData ActualInitialization.geometry.region ActualInitialization.geometry.patch.a ActualInitialization.geometry.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hfixed : (VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u).pressure = u.pressure) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (HS : 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) u u n m) (x : ActualSignedCoherence.Point) (hx : x ∈ PhysicalMeanDomain.slowDomain (ActualInitialCoherence.overlap n m)) (theta : ℝ) (i : Fin 3) : ((ActualSignedStageControls.parameters l).gaussianBlock ActualInitialization.geometry.strip (ActualSignedCoherence.request B u)).oscillation n (x, theta) i = GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m * GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m * GaugeStateCoherence.bandScale n m * ((ActualSignedStageControls.parameters l).gaussianBlock ActualInitialization.geometry.strip (ActualSignedCoherence.request B u)).oscillation m ((GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) x, theta) i

The Gaussian component of WaveOn, for the actual signed Fourier block, on all radial and free auxiliary fibers and at every angle.

theorem NavierStokes.ActualSignedGaussianCoherence.gaussianBlock_transport_symm {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State ActualSignedCoherence.Point) (H : MeanStateRegularity.PrimitiveData ActualInitialization.geometry.region ActualInitialization.geometry.patch.a ActualInitialization.geometry.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hfixed : (VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u).pressure = u.pressure) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (HS : 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) u u n m) (x : ActualSignedCoherence.Point) (hx : (GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k).symm x ∈ PhysicalMeanDomain.slowDomain (ActualInitialCoherence.overlap n m)) (theta : ℝ) (i : Fin 3) : ((ActualSignedStageControls.parameters l).gaussianBlock ActualInitialization.geometry.strip (ActualSignedCoherence.request B u)).oscillation m (x, theta) i = GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h m n * GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h m n * GaugeStateCoherence.bandScale m n * ((ActualSignedStageControls.parameters l).gaussianBlock ActualInitialization.geometry.strip (ActualSignedCoherence.request B u)).oscillation n ((GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k).symm x, theta) i

The same field comparison in the reverse common-chart direction. Its domain is the exact image of the forward overlap.

@[reducible, inline]

abbrev NavierStokes.ActualCycleCoherence.Point : Type

Point: an abbreviation for ActualInitialization.Point.

Equations

• NavierStokes.ActualCycleCoherence.Point = NavierStokes.ActualInitialization.Point

@[reducible, inline]

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

Index: an abbreviation for ActualInitialization.Index.

Equations

• NavierStokes.ActualCycleCoherence.Index = NavierStokes.ActualInitialization.Index

@[reducible, inline]

noncomputable abbrev NavierStokes.ActualCycleCoherence.geometry : CycleStateCoherence.Geometry

Geometry: an abbreviation for ActualMeanPhysicalData.initialGeometry.

Equations

• NavierStokes.ActualCycleCoherence.geometry = NavierStokes.ActualMeanPhysicalData.initialGeometry

@[reducible, inline]

abbrev NavierStokes.ActualCycleCoherence.overlap (n m : ℕ) : Set ActualInitialCoherence.Plane

Overlap: an abbreviation for ActualInitialCoherence.overlap.

Equations

• NavierStokes.ActualCycleCoherence.overlap = NavierStokes.ActualInitialCoherence.overlap

def NavierStokes.ActualCycleCoherence.StateCoherent (u : CorrectionState.State Point) : Prop

Every comparison is on the intersection of the two actual normalized slow charts; the radial and torus fibers are unrestricted.

Equations

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

def NavierStokes.ActualCycleCoherence.BlocksCoherent {ι : Type} (v : CorrectionStep.CycleCoefficients ι) : Prop

Individual input fields are compared, including the Gaussian and nonzero harmonic alias inputs used by the next particular solve.

Equations

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

def NavierStokes.ActualCycleCoherence.AxisCoherent (a : CorrectionStep.AxisymmetricAlias) : Prop

Axis coherent, given by ∀ n m k, CommonWindow.index h n + k = CommonWindow.index h m → CycleStateCoherence.AxisBand geometry (overlap n m) n m k a.

Equations

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

structure NavierStokes.ActualCycleCoherence.Coherent {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) : Prop

The geometric induction invariant, separate from all quantitative residual estimates. The label set is the initializer's fixed choice.

• state : StateCoherent x.state
• blocks : BlocksCoherent x.coefficients
• axis : AxisCoherent x.axisymmetricAlias
• labels : x.coefficients.labels = CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0

theorem NavierStokes.ActualCycleCoherence.realizes (B N0 : ℕ) : CycleStateCoherence.Realizes geometry (ActualCycleParameters.fixedParameters B N0) (CorrectionInitialization.ActualPrimary.commonContext B)

theorem NavierStokes.ActualCycleCoherence.context (B n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) : CycleStateCoherence.ContextBand geometry (overlap n m) n m k (CorrectionInitialization.ActualPrimary.commonContext B)

theorem NavierStokes.ActualCycleCoherence.initial_state (B N0 : ℕ) : StateCoherent (ActualInitialization.initialState B N0)

theorem NavierStokes.ActualCycleCoherence.initial_blocks (B N0 : ℕ) : BlocksCoherent (ActualInitialization.coefficients B N0)

theorem NavierStokes.ActualCycleCoherence.initial_axis (B N0 : ℕ) : AxisCoherent (ActualInitialization.initialAlias B N0)

theorem NavierStokes.ActualCycleCoherence.initial (B N0 : ℕ) : Coherent (ActualInitialization.initialCycleState B N0)

theorem NavierStokes.ActualCycleCoherence.BlocksCoherent.reindex {ι κ : Type} (e : κ ≃ ι) {v : CorrectionStep.CycleCoefficients ι} (H : BlocksCoherent v) : BlocksCoherent (ActualCycleParameters.reindexCoefficients e v)

theorem NavierStokes.ActualCycleCoherence.Coherent.particular_state {B N0 : ℕ} {x : CorrectionStep.CycleState (Index B N0)} (H : Coherent x) : StateCoherent (ActualCycleParameters.particularState x).state

theorem NavierStokes.ActualCycleCoherence.Coherent.particular_blocks {B N0 : ℕ} {x : CorrectionStep.CycleState (Index B N0)} (H : Coherent x) : BlocksCoherent (ActualCycleParameters.particularState x).coefficients

theorem NavierStokes.ActualCycleCoherence.StateCoherent.atlas {u : CorrectionState.State Point} (H : StateCoherent u) (N : ℕ) : (ActualMeanPhysicalData.initialAtlas N).StateOverlap CorrectionInitialization.ActualPrimary.standardRegion.carrier u

theorem NavierStokes.ActualCycleCoherence.Coherent.reference_state {B N0 : ℕ} {x : CorrectionStep.CycleState (Index B N0)} (H : Coherent x) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) : ActualReferenceRebase.StateComparison (ActualCycleParameters.particularState x) (overlap n m) n m k

theorem NavierStokes.ActualCycleCoherence.Coherent.reference_block {B N0 : ℕ} {x : CorrectionStep.CycleState (Index B N0)} (H : Coherent x) (l : ActualParticularStageControls.Label B N0) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) : ActualReferenceRebase.BlockComparison (ActualCycleParameters.particularState x) l (overlap n m) n m k

Omitted labels vanish by their primitive support and zero modes

theorem NavierStokes.ActualCycleCoherence.field_zero_of_support {U K : Set Point} (a : HarmonicFields.Coefficients Point) (hs : HarmonicSourceSupport.NonzeroSupportedOn U K (HarmonicResidual.realCoefficients a)) (hzero : a.coeff 0 = 0) (frequency : ℝ) (phase : Point → ℝ) (angular : ℤ) {x : Point} (hx : x ∈ U) (hn : x ∉ K) (theta : ℝ) : (HarmonicFields.field a frequency phase angular (x, theta)).re = 0

theorem NavierStokes.ActualCycleCoherence.wave_fields_zero_of_support {U : Set Point} {K : ℕ → Set Point} (b g : CorrectionState.HarmonicBlock Point) (hs : HarmonicSourceSupport.InputSupportOn U K b g.velocity 0) (hv : HarmonicWaveInteraction.ZeroMode b) (hp : ∀ (n : ℕ), (b.pressure n).coeff 0 = 0) (hg : HarmonicWaveInteraction.ZeroMode g) (n : ℕ) {x : Point} (hx : x ∈ U) (hn : x ∉ K n) (theta : ℝ) : b.oscillation n (x, theta) = 0 ∧ b.oscillatoryPressure n (x, theta) = 0 ∧ g.oscillation n (x, theta) = 0

theorem NavierStokes.ActualCycleCoherence.label_waves_of_support {ι : Type} (labels : ℕ → Finset ι) (b g : ι → CorrectionState.HarmonicBlock Point) (S : ι → ℕ → Set Point) (hs : ∀ (l : ι), HarmonicSourceSupport.InputSupportOn ActualInitialization.geometry.domain (S l) (b l) (g l).velocity 0) (hv : ∀ (l : ι), HarmonicWaveInteraction.ZeroMode (b l)) (hp : ∀ (l : ι) (n : ℕ), ((b l).pressure n).coeff 0 = 0) (hg : ∀ (l : ι), HarmonicWaveInteraction.ZeroMode (g l)) (hcover : ∀ (l : ι) (n : ℕ), ∀ x ∈ ActualInitialization.geometry.domain, x ∈ S l n → l ∈ labels n) (n m k : ℕ) (HW : ∀ (l : ι), CycleStateCoherence.WaveOn (PhysicalMeanDomain.slowDomain (overlap n m)) (GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m) (GaugeStateCoherence.bandScale n m) (b l).oscillation (b l).oscillatoryPressure (g l).oscillation (b l).oscillation (b l).oscillatoryPressure (g l).oscillation n m) : CycleStateCoherence.LabelWavesOn (PhysicalMeanDomain.slowDomain (overlap n m)) (GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m) (GaugeStateCoherence.bandScale n m) labels b g n m

The actual source on every fast-variable fiber

noncomputable def NavierStokes.ActualCycleCoherence.particularSource {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) : PhysicalParticularWave.Parameter × PressureStream.Plane → HarmonicCalculus.ComplexVector

Particular source, constructed using ParticularWaveAssembly.residualSource.

Equations

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

theorem NavierStokes.ActualCycleCoherence.particularSource_eq {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) : particularSource x l j n = ParticularWaveAssembly.residualSource (ActualParticularStageControls.assembly (ActualCycleParameters.particularState x) l).context (ActualParticularStageControls.assembly (ActualCycleParameters.particularState x) l).state (ActualParticularStageControls.assembly (ActualCycleParameters.particularState x) l).carrierBlock (ActualParticularStageControls.assembly (ActualCycleParameters.particularState x) l).gaussianInput (ActualParticularStageControls.assembly (ActualCycleParameters.particularState x) l).aliasInput j n

theorem NavierStokes.ActualCycleCoherence.core_ordered {B N0 : ℕ} (l : Index B N0) (n : ℕ) {z : Point} (hz : z ∈ ActualInitialization.geometry.domain) (hc : z ∈ ActualCoreSupport.refinedCarrier l n) : ActualWaveRegularityData.Ordered l n

theorem NavierStokes.ActualCycleCoherence.core_radius_pos {B N0 : ℕ} (l : Index B N0) (n : ℕ) {z : Point} (hz : z ∈ ActualInitialization.geometry.domain) (hc : z ∈ ActualCoreSupport.refinedCarrier l n) : 0 < z.1

theorem NavierStokes.ActualCycleCoherence.signed_wave_on {B N0 : ℕ} (l : Index B N0) (u : CorrectionState.State Point) (H : MeanStateRegularity.PrimitiveData ActualInitialization.geometry.region ActualInitialization.geometry.patch.a ActualInitialization.geometry.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hfixed : (VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u).pressure = u.pressure) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (HS : PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain (overlap n m)) (GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m) (GaugeStateCoherence.bandScale n m) u u n m) : CycleStateCoherence.WaveOn (PhysicalMeanDomain.slowDomain (overlap n m)) (GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m) (GaugeStateCoherence.bandScale n m) ((ActualSignedStageControls.parameters l).exactBlock ActualInitialization.geometry.strip (ActualSignedCoherence.request B u)).oscillation ((ActualSignedStageControls.parameters l).exactBlock ActualInitialization.geometry.strip (ActualSignedCoherence.request B u)).oscillatoryPressure ((ActualSignedStageControls.parameters l).gaussianBlock ActualInitialization.geometry.strip (ActualSignedCoherence.request B u)).oscillation ((ActualSignedStageControls.parameters l).exactBlock ActualInitialization.geometry.strip (ActualSignedCoherence.request B u)).oscillation ((ActualSignedStageControls.parameters l).exactBlock ActualInitialization.geometry.strip (ActualSignedCoherence.request B u)).oscillatoryPressure ((ActualSignedStageControls.parameters l).gaussianBlock ActualInitialization.geometry.strip (ActualSignedCoherence.request B u)).oscillation n m

All three fields of the actual signed insertion transform on the same overlap. The Gaussian term is the differentiated-cutoff error.

noncomputable def NavierStokes.ActualCycleCoherence.particularPoint (z : Point) : PhysicalParticularWave.WaveSpace

Particular point, given by ParticularWaveAssembly.angleShuffle (cycleAssoc z, 0).

Equations

• NavierStokes.ActualCycleCoherence.particularPoint z = NavierStokes.ParticularWaveAssembly.angleShuffle (NavierStokes.CorrectionStep.cycleAssoc z, 0)

theorem NavierStokes.ActualCycleCoherence.particularPoint_chart (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (z : Point) : (ActualParticularCoherence.bandMap n m) (particularPoint z) = particularPoint ((GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) z)

theorem NavierStokes.ActualCycleCoherence.particular_pressure_weight (n m : ℕ) : PhysicalParticularWave.pressureWeight CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q m) = GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m * GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m

theorem NavierStokes.ActualCycleCoherence.literal_particular_velocity {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) (l : Index B N0) (n : ℕ) (z : Point) (theta : ℝ) (i : Fin 3) : ((ActualCycleParameters.parameters x).particularBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state l).oscillation n (z, theta) i = ∑ j ∈ ParticularWaveAssembly.modes x.coefficients.residualBand, ((ActualParticularCoherence.corrected (ActualCycleParameters.particularState x) (l.2, l.1) j).amplitude n (particularPoint z) i * HarmonicFields.character j ((x.coefficients.blocks l).frequency n * (x.coefficients.blocks l).phase n z + ↑((x.coefficients.blocks l).angularFrequency n) * theta)).re

theorem NavierStokes.ActualCycleCoherence.literal_particular_pressure {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) (l : Index B N0) (n : ℕ) (z : Point) (theta : ℝ) : ((ActualCycleParameters.parameters x).particularBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state l).oscillatoryPressure n (z, theta) = ∑ j ∈ ParticularWaveAssembly.modes x.coefficients.residualBand, ((ActualParticularCoherence.corrected (ActualCycleParameters.particularState x) (l.2, l.1) j).pressure n (particularPoint z) * HarmonicFields.character j ((x.coefficients.blocks l).frequency n * (x.coefficients.blocks l).phase n z + ↑((x.coefficients.blocks l).angularFrequency n) * theta)).re

theorem NavierStokes.ActualCycleCoherence.literal_particular_gaussian {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) (l : Index B N0) (n : ℕ) (z : Point) (theta : ℝ) (i : Fin 3) : ((ActualCycleParameters.parameters x).particularGaussianBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state l).oscillation n (z, theta) i = ∑ j ∈ ParticularWaveAssembly.modes x.coefficients.residualBand, ((ActualParticularCoherence.copyData (ActualCycleParameters.particularState x) (l.2, l.1) j).globalGaussian ActualParticularStageControls.directions n (particularPoint z) i * HarmonicFields.character j ((x.coefficients.blocks l).frequency n * (x.coefficients.blocks l).phase n z + ↑((x.coefficients.blocks l).angularFrequency n) * theta)).re

Algebraic propagation after the two actual wave laws are derived

theorem NavierStokes.ActualCycleCoherence.source_support {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} {S : Index B N0 → ℕ → Set Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (hS : ∀ (l : Index B N0) (n : ℕ), IsClosed (S l n)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) {p : PhysicalParticularWave.Parameter} (hp : p.2 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier) {Y : PressureStream.Plane} (hne : particularSource x l j n (p, Y) ≠ 0) : CorrectionStep.cycleAssoc.symm (p, Y) ∈ S (l.2, l.1) n

theorem NavierStokes.ActualCycleCoherence.source_positive_smooth {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} {S : Index B N0 → ℕ → Set Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (l : Index B N0) (j : ℤ) (n : ℕ) : ContDiffOn ℝ (↑⊤) (ParticularWaveAssembly.residualSource (CorrectionInitialization.ActualPrimary.commonContext B) x.state (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l) j n) (LocalRankDefect.positiveDomain CorrectionInitialization.ActualPrimary.standardRegion.carrier)

theorem NavierStokes.ActualCycleCoherence.source_smooth {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} {S : Index B N0 → ℕ → Set Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (hS : ∀ (l : Index B N0) (n : ℕ), IsClosed (S l n)) (hpos : ∀ (l : Index B N0) (n : ℕ), ∀ z ∈ ActualInitialization.geometry.domain, z ∈ S l n → 0 < z.1) (l : Index B N0) (j : ℤ) (n : ℕ) : ContDiffOn ℝ (↑⊤) (ParticularWaveAssembly.residualSource (CorrectionInitialization.ActualPrimary.commonContext B) x.state (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l) j n) ActualInitialization.geometry.domain

theorem NavierStokes.ActualCycleCoherence.particularSource_smooth {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} {S : Index B N0 → ℕ → Set Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (hS : ∀ (l : Index B N0) (n : ℕ), IsClosed (S l n)) (hpos : ∀ (l : Index B N0) (n : ℕ), ∀ z ∈ ActualInitialization.geometry.domain, z ∈ S l n → 0 < z.1) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) : ContDiffOn ℝ (↑⊤) (particularSource x l j n) {z : PhysicalParticularWave.Parameter × PressureStream.Plane | z.1.2 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier}

theorem NavierStokes.ActualCycleCoherence.source_fiber_continuous {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} {S : Index B N0 → ℕ → Set Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (hS : ∀ (l : Index B N0) (n : ℕ), IsClosed (S l n)) (hpos : ∀ (l : Index B N0) (n : ℕ), ∀ z ∈ ActualInitialization.geometry.domain, z ∈ S l n → 0 < z.1) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) (p : PhysicalParticularWave.Parameter) (hp : p.2 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier) : Continuous fun (Y : PressureStream.Plane) => particularSource x l j n (p, Y)

theorem NavierStokes.ActualCycleCoherence.source_ordered {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} {S : Index B N0 → ℕ → Set Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (hS : ∀ (l : Index B N0) (n : ℕ), IsClosed (S l n)) (hcore : ∀ (l : Index B N0) (n : ℕ), S l n ⊆ ActualCoreSupport.refinedCarrier l n) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) (p : PhysicalParticularWave.Parameter) (hp : p.2 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier) (hne : ∃ (Y : PressureStream.Plane), particularSource x l j n (p, Y) ≠ 0) : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2)

theorem NavierStokes.ActualCycleCoherence.particular_source_inputs {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} {S : Index B N0 → ℕ → Set Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (hS : ∀ (l : Index B N0) (n : ℕ), IsClosed (S l n)) (hcore : ∀ (l : Index B N0) (n : ℕ), S l n ⊆ ActualCoreSupport.refinedCarrier l n) (l : ActualParticularStageControls.Label B N0) : ActualParticularCoherence.SourceInputs (ActualCycleParameters.particularState x) l

theorem NavierStokes.ActualCycleCoherence.covariance_moving {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} {S : Index B N0 → ℕ → Set Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (W : CorrectionAnalyticStep.WaveData ActualInitialization.geometry (ActualCycleParameters.fixedParameters B N0) x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state ActualInitialization.envelope S σ ChartScales.kappa) : (∀ (i j : Fin 3), GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion geometry.inner geometry.outer (SignedMeanGain.covarianceIncrement x.state.oscillation ((ActualCycleParameters.fixedParameters B N0).particularVelocity x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state) i j)) ∧ ∀ (i j : Fin 3), GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion geometry.inner geometry.outer (SignedMeanGain.covarianceIncrement ((ActualCycleParameters.fixedParameters B N0).afterParticular x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state).oscillation ((ActualCycleParameters.fixedParameters B N0).signedVelocity x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state) i j)

theorem NavierStokes.ActualCycleCoherence.rank_geometry {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} {S : Index B N0 → ℕ → Set Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) : LocalRankDefect.RankGeometry (ActualCycleParameters.fixedParameters B N0).gauge (ActualCycleParameters.fixedParameters B N0).rank CorrectionInitialization.ActualPrimary.standardRegion.carrier (CorrectionInitialization.ActualPrimary.commonContext B) x.state

theorem NavierStokes.ActualCycleCoherence.stage_primitives {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} {S : Index B N0 → ℕ → Set Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (W : CorrectionAnalyticStep.WaveData ActualInitialization.geometry (ActualCycleParameters.fixedParameters B N0) x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state ActualInitialization.envelope S σ ChartScales.kappa) : CycleStateCoherence.StagePrimitives geometry (ActualCycleParameters.fixedParameters B N0) x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state CorrectionInitialization.ActualPrimary.standardRegion

theorem NavierStokes.ActualCycleCoherence.afterParticular_primitive {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} {S : Index B N0 → ℕ → Set Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (W : CorrectionAnalyticStep.WaveData ActualInitialization.geometry (ActualCycleParameters.fixedParameters B N0) x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state ActualInitialization.envelope S σ ChartScales.kappa) : MeanStateRegularity.PrimitiveData ActualInitialization.geometry.region ActualInitialization.geometry.patch.a ActualInitialization.geometry.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) ((ActualCycleParameters.fixedParameters B N0).afterParticular x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state)

theorem NavierStokes.ActualCycleCoherence.afterParticular_pressure {B N0 : ℕ} {x : CorrectionStep.CycleState (Index B N0)} : (VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) ((ActualCycleParameters.fixedParameters B N0).afterParticular x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state)).pressure = ((ActualCycleParameters.fixedParameters B N0).afterParticular x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state).pressure

theorem NavierStokes.ActualCycleCoherence.signed_cycle_wave_on {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} {S : Index B N0 → ℕ → Set Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (W : CorrectionAnalyticStep.WaveData ActualInitialization.geometry (ActualCycleParameters.fixedParameters B N0) x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state ActualInitialization.envelope S σ ChartScales.kappa) (l : Index B N0) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (HS : PhysicalResidualNaturality.StateOn (PhysicalMeanDomain.slowDomain (overlap n m)) (GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m) (GaugeStateCoherence.bandScale n m) ((ActualCycleParameters.fixedParameters B N0).afterParticular x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state) ((ActualCycleParameters.fixedParameters B N0).afterParticular x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state) n m) : CycleStateCoherence.WaveOn (PhysicalMeanDomain.slowDomain (overlap n m)) (GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m) (GaugeStateCoherence.bandScale n m) ((ActualCycleParameters.fixedParameters B N0).signedBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state l).oscillation ((ActualCycleParameters.fixedParameters B N0).signedBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state l).oscillatoryPressure ((ActualCycleParameters.fixedParameters B N0).signedGaussianBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state l).oscillation ((ActualCycleParameters.fixedParameters B N0).signedBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state l).oscillation ((ActualCycleParameters.fixedParameters B N0).signedBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state l).oscillatoryPressure ((ActualCycleParameters.fixedParameters B N0).signedGaussianBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state l).oscillation n m

theorem NavierStokes.ActualCycleCoherence.particular_pressure_zero {B N0 : ℕ} (p : CorrectionStep.CycleParameters (Index B N0)) (v : CorrectionStep.CycleCoefficients (Index B N0)) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (l : Index B N0) (n : ℕ) : ((p.particularBlock v c u l).pressure n).coeff 0 = 0

theorem NavierStokes.ActualCycleCoherence.particular_wave_on {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} {S : Index B N0 → ℕ → Set Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (C : Coherent x) (hS : ∀ (l : Index B N0) (n : ℕ), IsClosed (S l n)) (hcore : ∀ (l : Index B N0) (n : ℕ), S l n ⊆ ActualCoreSupport.refinedCarrier l n) (l : Index B N0) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) : CycleStateCoherence.WaveOn (PhysicalMeanDomain.slowDomain (overlap n m)) (GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m) (GaugeStateCoherence.bandScale n m) ((ActualCycleParameters.fixedParameters B N0).particularBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state l).oscillation ((ActualCycleParameters.fixedParameters B N0).particularBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state l).oscillatoryPressure ((ActualCycleParameters.fixedParameters B N0).particularGaussianBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state l).oscillation ((ActualCycleParameters.fixedParameters B N0).particularBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state l).oscillation ((ActualCycleParameters.fixedParameters B N0).particularBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state l).oscillatoryPressure ((ActualCycleParameters.fixedParameters B N0).particularGaussianBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state l).oscillation n m

theorem NavierStokes.ActualCycleCoherence.particular_label_waves {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} {S : Index B N0 → ℕ → Set Point} (W : CorrectionAnalyticStep.WaveData ActualInitialization.geometry (ActualCycleParameters.fixedParameters B N0) x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state ActualInitialization.envelope S σ ChartScales.kappa) (hcover : ∀ (l : Index B N0) (n : ℕ), ∀ z ∈ ActualInitialization.geometry.domain, z ∈ S l n → l ∈ x.coefficients.labels n) (n m k : ℕ) (HP : ∀ (l : ActualCycleParameters.Index B N0), CycleStateCoherence.WaveOn (PhysicalMeanDomain.slowDomain (overlap n m)) (GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m) (GaugeStateCoherence.bandScale n m) ((ActualCycleParameters.fixedParameters B N0).particularBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state l).oscillation ((ActualCycleParameters.fixedParameters B N0).particularBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state l).oscillatoryPressure ((ActualCycleParameters.fixedParameters B N0).particularGaussianBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state l).oscillation ((ActualCycleParameters.fixedParameters B N0).particularBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state l).oscillation ((ActualCycleParameters.fixedParameters B N0).particularBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state l).oscillatoryPressure ((ActualCycleParameters.fixedParameters B N0).particularGaussianBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state l).oscillation n m) : CycleStateCoherence.LabelWavesOn (PhysicalMeanDomain.slowDomain (overlap n m)) (GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m) (GaugeStateCoherence.bandScale n m) x.coefficients.labels ((ActualCycleParameters.fixedParameters B N0).particularBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state) ((ActualCycleParameters.fixedParameters B N0).particularGaussianBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state) n m

theorem NavierStokes.ActualCycleCoherence.signed_label_waves {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} {S : Index B N0 → ℕ → Set Point} (W : CorrectionAnalyticStep.WaveData ActualInitialization.geometry (ActualCycleParameters.fixedParameters B N0) x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state ActualInitialization.envelope S σ ChartScales.kappa) (hcover : ∀ (l : Index B N0) (n : ℕ), ∀ z ∈ ActualInitialization.geometry.domain, z ∈ S l n → l ∈ x.coefficients.labels n) (n m k : ℕ) (HS : ∀ (l : ActualCycleParameters.Index B N0), CycleStateCoherence.WaveOn (PhysicalMeanDomain.slowDomain (overlap n m)) (GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m) (GaugeStateCoherence.bandScale n m) ((ActualCycleParameters.fixedParameters B N0).signedBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state l).oscillation ((ActualCycleParameters.fixedParameters B N0).signedBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state l).oscillatoryPressure ((ActualCycleParameters.fixedParameters B N0).signedGaussianBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state l).oscillation ((ActualCycleParameters.fixedParameters B N0).signedBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state l).oscillation ((ActualCycleParameters.fixedParameters B N0).signedBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state l).oscillatoryPressure ((ActualCycleParameters.fixedParameters B N0).signedGaussianBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state l).oscillation n m) : CycleStateCoherence.LabelWavesOn (PhysicalMeanDomain.slowDomain (overlap n m)) (GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m) (GaugeStateCoherence.bandScale n m) x.coefficients.labels ((ActualCycleParameters.fixedParameters B N0).signedBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state) ((ActualCycleParameters.fixedParameters B N0).signedGaussianBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state) n m

theorem NavierStokes.ActualCycleCoherence.transport_of_waves {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} {S : Index B N0 → ℕ → Set Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (W : CorrectionAnalyticStep.WaveData ActualInitialization.geometry (ActualCycleParameters.fixedParameters B N0) x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state ActualInitialization.envelope S σ ChartScales.kappa) (C : Coherent x) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) (HW : CycleStateCoherence.CycleWavesOn geometry (ActualCycleParameters.fixedParameters B N0) x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state (overlap n m) n m k) : CycleStateCoherence.CycleTransport geometry (ActualCycleParameters.fixedParameters B N0) x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state (overlap n m) n m k

theorem NavierStokes.ActualCycleCoherence.afterParticular_coherent {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} {S : Index B N0 → ℕ → Set Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (W : CorrectionAnalyticStep.WaveData ActualInitialization.geometry (ActualCycleParameters.fixedParameters B N0) x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state ActualInitialization.envelope S σ ChartScales.kappa) (C : Coherent x) (HP : ∀ (n m k : ℕ), CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m → CycleStateCoherence.LabelWavesOn (PhysicalMeanDomain.slowDomain (overlap n m)) (GaugeStateCoherence.bandChartEquiv CorrectionInitialization.ActualPrimary.h n m k) (GaugeStateCoherence.bandVelocityScale CorrectionInitialization.ActualPrimary.h n m) (GaugeStateCoherence.bandScale n m) x.coefficients.labels ((ActualCycleParameters.fixedParameters B N0).particularBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state) ((ActualCycleParameters.fixedParameters B N0).particularGaussianBlock x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state) n m) : StateCoherent ((ActualCycleParameters.fixedParameters B N0).afterParticular x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state)

theorem NavierStokes.ActualCycleCoherence.waves {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} {S : Index B N0 → ℕ → Set Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (W : CorrectionAnalyticStep.WaveData ActualInitialization.geometry (ActualCycleParameters.fixedParameters B N0) x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state ActualInitialization.envelope S σ ChartScales.kappa) (C : Coherent x) (hcover : ∀ (l : Index B N0) (n : ℕ), ∀ z ∈ ActualInitialization.geometry.domain, z ∈ S l n → l ∈ x.coefficients.labels n) (hS : ∀ (l : Index B N0) (n : ℕ), IsClosed (S l n)) (hcore : ∀ (l : Index B N0) (n : ℕ), S l n ⊆ ActualCoreSupport.refinedCarrier l n) (n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) : CycleStateCoherence.CycleWavesOn geometry (ActualCycleParameters.fixedParameters B N0) x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state (overlap n m) n m k

The two literal wave insertions have the required transport law. Every source and coefficient comparison is derived from the incoming state, its support, and the actual solver primitives.

theorem NavierStokes.ActualCycleCoherence.step_of_waves {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} {S : Index B N0 → ℕ → Set Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (W : CorrectionAnalyticStep.WaveData ActualInitialization.geometry (ActualCycleParameters.fixedParameters B N0) x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state ActualInitialization.envelope S σ ChartScales.kappa) (C : Coherent x) (HW : ∀ (n m k : ℕ), CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m → CycleStateCoherence.CycleWavesOn geometry (ActualCycleParameters.fixedParameters B N0) x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state (overlap n m) n m k) : Coherent (CorrectionStep.CycleState.step (ActualCycleParameters.fixedParameters B N0) (CorrectionInitialization.ActualPrimary.commonContext B) x)

theorem NavierStokes.ActualCycleCoherence.step {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} {S : Index B N0 → ℕ → Set Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (W : CorrectionAnalyticStep.WaveData ActualInitialization.geometry (ActualCycleParameters.fixedParameters B N0) x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state ActualInitialization.envelope S σ ChartScales.kappa) (C : Coherent x) (hcover : ∀ (l : Index B N0) (n : ℕ), ∀ z ∈ ActualInitialization.geometry.domain, z ∈ S l n → l ∈ x.coefficients.labels n) (hS : ∀ (l : Index B N0) (n : ℕ), IsClosed (S l n)) (hcore : ∀ (l : Index B N0) (n : ℕ), S l n ⊆ ActualCoreSupport.refinedCarrier l n) : Coherent (CorrectionStep.CycleState.step (ActualCycleParameters.fixedParameters B N0) (CorrectionInitialization.ActualPrimary.commonContext B) x)

Simultaneous propagation of the actual state, stored blocks, Gaussian/alias data, and the initializer's finite label choice.

theorem NavierStokes.ActualCycleCoherence.next_primitive {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} {S : Index B N0 → ℕ → Set Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (W : CorrectionAnalyticStep.WaveData ActualInitialization.geometry (ActualCycleParameters.fixedParameters B N0) x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state ActualInitialization.envelope S σ ChartScales.kappa) : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion geometry.inner geometry.outer (CorrectionInitialization.ActualPrimary.commonContext B) (CorrectionStep.CycleState.step (ActualCycleParameters.fixedParameters B N0) (CorrectionInitialization.ActualPrimary.commonContext B) x).state

theorem NavierStokes.ActualCycleCoherence.temporal_potential_overlap {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} {S : Index B N0 → ℕ → Set Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (W : CorrectionAnalyticStep.WaveData ActualInitialization.geometry (ActualCycleParameters.fixedParameters B N0) x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state ActualInitialization.envelope S σ ChartScales.kappa) (C : Coherent x) (N : ℕ) (HW : ∀ (n m k : ℕ), CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m → CycleStateCoherence.CycleWavesOn geometry (ActualCycleParameters.fixedParameters B N0) x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state (overlap n m) n m k) : (ActualMeanPhysicalData.initialAtlas N).OverlapLaw CorrectionInitialization.ActualPrimary.standardRegion.carrier (CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h - 1 / 2) (VariableGaugeMean.temporalPotential (ActualCycleParameters.fixedParameters B N0).gauge (ActualCycleParameters.fixedParameters B N0).timeExponent (ActualCycleParameters.fixedParameters B N0).commonIndex (CorrectionInitialization.ActualPrimary.commonContext B) ((ActualCycleParameters.fixedParameters B N0).afterSigned x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state))

theorem NavierStokes.ActualCycleCoherence.rank_potential_overlap {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} {S : Index B N0 → ℕ → Set Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (W : CorrectionAnalyticStep.WaveData ActualInitialization.geometry (ActualCycleParameters.fixedParameters B N0) x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state ActualInitialization.envelope S σ ChartScales.kappa) (C : Coherent x) (N : ℕ) (HW : ∀ (n m k : ℕ), CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m → CycleStateCoherence.CycleWavesOn geometry (ActualCycleParameters.fixedParameters B N0) x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state (overlap n m) n m k) : (ActualMeanPhysicalData.initialAtlas N).OverlapLaw CorrectionInitialization.ActualPrimary.standardRegion.carrier (CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h - 1 / 2) (VariableGaugeMean.rankPotential (ActualCycleParameters.fixedParameters B N0).gauge (ActualCycleParameters.fixedParameters B N0).rank (CorrectionInitialization.ActualPrimary.commonContext B) ((ActualCycleParameters.fixedParameters B N0).afterTemporal x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state))

The fixed actual recurrence and the mean atlas input

noncomputable def NavierStokes.ActualCycleCoherence.state (B N0 a✝ : ℕ) : CorrectionStep.CycleState (Index B N0)

State, constructed using CycleState.iterate.

Equations

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

theorem NavierStokes.ActualCycleCoherence.state_zero (B N0 : ℕ) : state B N0 0 = ActualInitialization.initialCycleState B N0

theorem NavierStokes.ActualCycleCoherence.state_succ (B N0 j : ℕ) : state B N0 (j + 1) = CorrectionStep.CycleState.step (ActualCycleParameters.fixedParameters B N0) (CorrectionInitialization.ActualPrimary.commonContext B) (state B N0 j)

theorem NavierStokes.ActualCycleCoherence.state_labels (B N0 j : ℕ) : (state B N0 j).coefficients.labels = CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0

theorem NavierStokes.ActualCycleCoherence.state_aliasCoefficients (B N0 j : ℕ) : (state B N0 j).coefficients.aliasCoefficients = 0

theorem NavierStokes.ActualCycleCoherence.mean_input_of_transport (B N0 N : ℕ) (sigma : ℕ → ℝ) (S : Index B N0 → ℕ → Set Point) (H : ∀ (j : ℕ), CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S (sigma j) (state B N0 j)) (W : ∀ (j : ℕ), CorrectionAnalyticStep.WaveData ActualInitialization.geometry (ActualCycleParameters.fixedParameters B N0) (state B N0 j).coefficients (CorrectionInitialization.ActualPrimary.commonContext B) (state B N0 j).state ActualInitialization.envelope S (sigma j) ChartScales.kappa) (HW : ∀ (j n m k : ℕ), CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m → CycleStateCoherence.CycleWavesOn geometry (ActualCycleParameters.fixedParameters B N0) (state B N0 j).coefficients (CorrectionInitialization.ActualPrimary.commonContext B) (state B N0 j).state (overlap n m) n m k) : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0

Collection of the already proved actual transport laws into precisely the input used by the physical mean atlas. Its covariance fields are derived from the same stage data as the analytic induction.

theorem NavierStokes.ActualCycleCoherence.iterate_coherent (B N0 : ℕ) (sigma : ℕ → ℝ) (S : Index B N0 → ℕ → Set Point) (H : ∀ (j : ℕ), CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S (sigma j) (state B N0 j)) (W : ∀ (j : ℕ), CorrectionAnalyticStep.WaveData ActualInitialization.geometry (ActualCycleParameters.fixedParameters B N0) (state B N0 j).coefficients (CorrectionInitialization.ActualPrimary.commonContext B) (state B N0 j).state ActualInitialization.envelope S (sigma j) ChartScales.kappa) (hS : ∀ (l : Index B N0) (n : ℕ), IsClosed (S l n)) (hcore : ∀ (l : Index B N0) (n : ℕ), S l n ⊆ ActualCoreSupport.refinedCarrier l n) (hcover : ∀ (l : Index B N0) (n : ℕ), ∀ z ∈ ActualInitialization.geometry.domain, z ∈ S l n → l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n) (j : ℕ) : Coherent (state B N0 j)

The geometric induction uses the same fixed recurrence and supplied analytic stage data; no sequence of coherent states is assumed.

theorem NavierStokes.ActualCycleCoherence.iterate_waves (B N0 : ℕ) (sigma : ℕ → ℝ) (S : Index B N0 → ℕ → Set Point) (H : ∀ (j : ℕ), CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S (sigma j) (state B N0 j)) (W : ∀ (j : ℕ), CorrectionAnalyticStep.WaveData ActualInitialization.geometry (ActualCycleParameters.fixedParameters B N0) (state B N0 j).coefficients (CorrectionInitialization.ActualPrimary.commonContext B) (state B N0 j).state ActualInitialization.envelope S (sigma j) ChartScales.kappa) (hS : ∀ (l : Index B N0) (n : ℕ), IsClosed (S l n)) (hcore : ∀ (l : Index B N0) (n : ℕ), S l n ⊆ ActualCoreSupport.refinedCarrier l n) (hcover : ∀ (l : Index B N0) (n : ℕ), ∀ z ∈ ActualInitialization.geometry.domain, z ∈ S l n → l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n) (j n m k : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m) : CycleStateCoherence.CycleWavesOn geometry (ActualCycleParameters.fixedParameters B N0) (state B N0 j).coefficients (CorrectionInitialization.ActualPrimary.commonContext B) (state B N0 j).state (overlap n m) n m k

theorem NavierStokes.ActualCycleCoherence.mean_input (B N0 : ℕ) (sigma : ℕ → ℝ) (S : Index B N0 → ℕ → Set Point) (H : ∀ (j : ℕ), CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S (sigma j) (state B N0 j)) (W : ∀ (j : ℕ), CorrectionAnalyticStep.WaveData ActualInitialization.geometry (ActualCycleParameters.fixedParameters B N0) (state B N0 j).coefficients (CorrectionInitialization.ActualPrimary.commonContext B) (state B N0 j).state ActualInitialization.envelope S (sigma j) ChartScales.kappa) (hS : ∀ (l : Index B N0) (n : ℕ), IsClosed (S l n)) (hcore : ∀ (l : Index B N0) (n : ℕ), S l n ⊆ ActualCoreSupport.refinedCarrier l n) (hcover : ∀ (l : Index B N0) (n : ℕ), ∀ z ∈ ActualInitialization.geometry.domain, z ∈ S l n → l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n) (N : ℕ) : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0

The actual mean-atlas input is derived from the same analytic recurrence; its wave and covariance transports are conclusions.