Construction of the initial correction fields

The operations in this file use the actual shifted pressure primitive, torus inverse, stream potential, and five-row inverse. The covariance identity is also differentiated as an identity of functions, retaining all derivatives of the squared partition. Quantitative initialization is assembled below from the estimates on these same operations.

noncomputable def NavierStokes.CorrectionInitialization.primaryCovariance {X : Type} {D h : ℝ} {vr vt : PartitionedCovariance.Plane} (sys : PartitionedCovariance.SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (N : ℕ) (P : X → (U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U)) (q : X → ℝ) (position : X → SlotColoring.Position) (target : X → PartitionedCovariance.Vec2) (i : Fin 2) (x : X) : ℝ

The actual leading covariance, including all physical partition factors.

Equations

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

theorem NavierStokes.CorrectionInitialization.primaryCovariance_eqOn {X : Type} {D h : ℝ} {vr vt : PartitionedCovariance.Plane} (sys : PartitionedCovariance.SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (N : ℕ) (hN : 1 ≤ N) (P : X → (U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U)) (q : X → ℝ) (position : X → SlotColoring.Position) (target : X → PartitionedCovariance.Vec2) {Ω : Set X} (hq : ∀ x ∈ Ω, 0 < q x) (hupper : ∀ x ∈ Ω, q x ≤ ChartScales.Q N) (hcone : ∀ x ∈ Ω, ∀ (U : PartitionedCovariance.UnsignedLabel), PartitionedCovariance.mask D (PartitionedCovariance.tailLabel N U) (q x) (position x) ≠ 0 → SmoothCovariance.StrictCone (P x U).matrix (PartitionedCovariance.chartTarget h (q x) N (target x) U)) (i : Fin 2) : Set.EqOn (primaryCovariance sys hdet N P q position target i) (fun (x : X) => q x ^ (-PartitionedCovariance.velocityExponent h - 1 / 2) * target x i) Ω

theorem NavierStokes.CorrectionInitialization.primaryCovariance_jets {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {D h : ℝ} {vr vt : PartitionedCovariance.Plane} (sys : PartitionedCovariance.SlotSystem D h vr vt) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (N : ℕ) (hN : 1 ≤ N) (P : X → (U : PartitionedCovariance.UnsignedLabel) → PartitionedCovariance.PairData sys (PartitionedCovariance.tailLabel N U)) (q : X → ℝ) (position : X → SlotColoring.Position) (target : X → PartitionedCovariance.Vec2) {Ω : Set X} (hΩ : IsOpen Ω) (hq : ∀ x ∈ Ω, 0 < q x) (hupper : ∀ x ∈ Ω, q x ≤ ChartScales.Q N) (hcone : ∀ x ∈ Ω, ∀ (U : PartitionedCovariance.UnsignedLabel), PartitionedCovariance.mask D (PartitionedCovariance.tailLabel N U) (q x) (position x) ≠ 0 → SmoothCovariance.StrictCone (P x U).matrix (PartitionedCovariance.chartTarget h (q x) N (target x) U)) (i : Fin 2) {x : X} (hx : x ∈ Ω) (k : ℕ) : iteratedFDeriv ℝ k (primaryCovariance sys hdet N P q position target i) x = iteratedFDeriv ℝ k (fun (x : X) => q x ^ (-PartitionedCovariance.velocityExponent h - 1 / 2) * target x i) x

In particular every derivative of every squared mask is included. No commutation of a derivative with an infinite sum is assumed.

structure NavierStokes.CorrectionInitialization.PrimaryPiece (X : Type) [NormedAddCommGroup X] [NormedSpace ℝ X] : Type

The primitive data of one primary label. Its velocity below is the actual cutoff curl, and its pressure is the actual cutoff pressure mode.

• strip : WeightedClasses.StripData X

  Strip of PrimaryPiece, of type StripData X.

• directions : LinearWaveBounds.GraphDirections X

  Directions of PrimaryPiece, of type GraphDirections X.

• coefficients : LinearWaveBounds.WaveCoefficients X

  Coefficients of PrimaryPiece, of type WaveCoefficients X.

• cutoff : ℕ → X → ℝ

  Cutoff of PrimaryPiece, of type ℕ → X → ℝ.

noncomputable def NavierStokes.CorrectionInitialization.PrimaryPiece.exactCoefficients {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] (p : PrimaryPiece X) : LinearWaveBounds.WaveCoefficients X

Exact coefficients, given by p.coefficients.corrected p.strip p.directions p.cutoff.

Equations

• p.exactCoefficients = p.coefficients.corrected p.strip p.directions p.cutoff

noncomputable def NavierStokes.CorrectionInitialization.PrimaryPiece.velocity {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] (p : PrimaryPiece X) : ℕ → X → Fin 3 → ℝ

Velocity, defined pointwise by (vectorMode (p.coefficients.frequency n) (p.coefficients.phase n) (p.exactCoefficients.amplitude n) x i).re.

Equations

• p.velocity n x i = (NavierStokes.HarmonicCalculus.vectorMode (p.coefficients.frequency n) (p.coefficients.phase n) (p.exactCoefficients.amplitude n) x i).re

noncomputable def NavierStokes.CorrectionInitialization.PrimaryPiece.tangentVelocity {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] (p : PrimaryPiece X) : ℕ → X → Fin 3 → ℝ

Tangent velocity, defined pointwise by (vectorMode (p.coefficients.frequency n) (p.coefficients.phase n) ((p.coefficients.withCutoff p.cutoff).amplitude n) x i).re.

Equations

• p.tangentVelocity n x i = (NavierStokes.HarmonicCalculus.vectorMode (p.coefficients.frequency n) (p.coefficients.phase n) ((p.coefficients.withCutoff p.cutoff).amplitude n) x i).re

noncomputable def NavierStokes.CorrectionInitialization.PrimaryPiece.pressure {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] (p : PrimaryPiece X) : ℕ → X → ℝ

Pressure, defined pointwise by (mode (p.coefficients.frequency n) (p.coefficients.phase n) (p.exactCoefficients.pressure n) x).re.

Equations

• p.pressure n x = (NavierStokes.HarmonicCalculus.mode (p.coefficients.frequency n) (p.coefficients.phase n) (p.exactCoefficients.pressure n) x).re

noncomputable def NavierStokes.CorrectionInitialization.PrimaryPiece.excluded {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] (p : PrimaryPiece X) : ℕ → X → Fin 3 → ℝ

Excluded as an element of ℕ → X → Fin 3 → ℝ.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.PrimaryPiece.linearGood {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] (p : PrimaryPiece X) : ℕ → X → HarmonicCalculus.ComplexVector

Linear good, given by p.coefficients.constructedGood p.strip p.directions p.cutoff.

Equations

• p.linearGood = p.coefficients.constructedGood p.strip p.directions p.cutoff

noncomputable def NavierStokes.CorrectionInitialization.PrimaryPiece.linearGoodField {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] (p : PrimaryPiece X) : ℕ → X → Fin 3 → ℝ

Linear good field, defined pointwise by (vectorMode (p.coefficients.frequency n) (p.coefficients.phase n) (p.linearGood n) x i).re.

Equations

• p.linearGoodField n x i = (NavierStokes.HarmonicCalculus.vectorMode (p.coefficients.frequency n) (p.coefficients.phase n) (p.linearGood n) x i).re

noncomputable def NavierStokes.CorrectionInitialization.PrimaryPiece.linearResidual {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] (p : PrimaryPiece X) : ℕ → X → Fin 3 → ℝ

Linear residual, defined pointwise by (p.exactCoefficients.harmonicResidual p.strip p.directions n x i).re.

Equations

• p.linearResidual n x i = (p.exactCoefficients.harmonicResidual p.strip p.directions n x i).re

theorem NavierStokes.CorrectionInitialization.PrimaryPiece.linear_bound_and_identity {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] (p : PrimaryPiece X) {P : ℕ → X → ℝ} (hp : LinearWaveBounds.InputBounds p.strip P (1 / 2) ChartScales.kappa p.directions p.coefficients) (hcut : WeightedClasses.UnweightedClass p.strip 0 p.cutoff) {R : X → ℝ} (hR : p.coefficients.radius = fun (x : ℕ) => R) (hN : PhaseJetBounds.PolynomialJets (CurlClassBounds.phaseDomain p.strip) (p.coefficients.normal p.strip p.directions)) {b M : ℝ} (hb : 0 < b) (hlo : ∀ (n : ℕ), ∀ x ∈ p.strip.domain, b ≤ ‖p.coefficients.normal p.strip p.directions n x‖) (hhi : ∀ (n : ℕ), ∀ x ∈ p.strip.domain, ‖p.coefficients.normal p.strip p.directions n x‖ ≤ M) (hK : WeightedClasses.BandBound p.strip (1 / 2) fun (n : ℕ) => 1 / p.coefficients.frequency n) (hsolve : ∀ (n : ℕ), ∀ x ∈ p.strip.domain, p.coefficients.principal p.strip p.directions n x = 0) (hg : LinearWaveBounds.ExactConditions p.strip p.directions p.exactCoefficients) : WeightedClasses.WaveClass p.strip P (7 / 10) p.linearGood ∧ ∀ (n : ℕ), ∀ x ∈ p.strip.domain, ∀ (i : Fin 3), p.linearResidual n x i = p.linearGoodField n x i + p.excluded n x i

Primary linear residuals are evaluated on the same constructed curl used by velocity; the Gaussian cutoff derivative remains explicit.

theorem NavierStokes.CorrectionInitialization.PrimaryPiece.cumulative_bounds {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] (p : PrimaryPiece X) {P : ℕ → X → ℝ} (hp : LinearWaveBounds.InputBounds p.strip P (1 / 2) ChartScales.kappa p.directions p.coefficients) (hcut : WeightedClasses.UnweightedClass p.strip 0 p.cutoff) {R : X → ℝ} (hR : p.coefficients.radius = fun (x : ℕ) => R) (hN : PhaseJetBounds.PolynomialJets (CurlClassBounds.phaseDomain p.strip) (p.coefficients.normal p.strip p.directions)) {b M : ℝ} (hb : 0 < b) (hlo : ∀ (n : ℕ), ∀ x ∈ p.strip.domain, b ≤ ‖p.coefficients.normal p.strip p.directions n x‖) (hhi : ∀ (n : ℕ), ∀ x ∈ p.strip.domain, ‖p.coefficients.normal p.strip p.directions n x‖ ≤ M) (hK : WeightedClasses.BandBound p.strip (1 / 2) fun (n : ℕ) => 1 / p.coefficients.frequency n) : (∀ (i : Fin 3), WeightedClasses.WaveClass p.strip P (1 / 2) fun (n : ℕ) (x : X) => p.exactCoefficients.amplitude n x i) ∧ (WeightedClasses.WaveClass p.strip P (17 / 25) fun (n : ℕ) (x : X) => p.exactCoefficients.amplitude n x - (p.coefficients.withCutoff p.cutoff).amplitude n x) ∧ WeightedClasses.WaveClass p.strip P 1 p.exactCoefficients.pressure

These are the cumulative primary bounds, proved from the tangent coefficient and the actual curl remainder.

theorem NavierStokes.CorrectionInitialization.curlCorrection_tsupport_subset {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] (a : LinearWaveBounds.WaveCoefficients X) (s : WeightedClasses.StripData X) (d : LinearWaveBounds.GraphDirections X) (n : ℕ) : tsupport (a.curlCorrection s d n) ⊆ tsupport (a.amplitude n)

Taking the actual curl correction does not enlarge the closed support of its amplitude. This also includes every derivative at a slot boundary.

theorem NavierStokes.CorrectionInitialization.PrimaryPiece.exactAmplitude_tsupport_subset_tangent {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] (p : PrimaryPiece X) (n : ℕ) : tsupport (p.exactCoefficients.amplitude n) ⊆ tsupport ((p.coefficients.withCutoff p.cutoff).amplitude n)

theorem NavierStokes.CorrectionInitialization.PrimaryPiece.velocity_tsupport_subset_tangent {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] (p : PrimaryPiece X) (n : ℕ) : tsupport (p.velocity n) ⊆ tsupport ((p.coefficients.withCutoff p.cutoff).amplitude n)

theorem NavierStokes.CorrectionInitialization.PrimaryPiece.tangentVelocity_tsupport_subset {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] (p : PrimaryPiece X) (n : ℕ) : tsupport (p.tangentVelocity n) ⊆ tsupport ((p.coefficients.withCutoff p.cutoff).amplitude n)

theorem NavierStokes.CorrectionInitialization.PrimaryPiece.exactAmplitude_tsupport_subset {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] (p : PrimaryPiece X) (n : ℕ) : tsupport (p.exactCoefficients.amplitude n) ⊆ tsupport (p.cutoff n)

theorem NavierStokes.CorrectionInitialization.PrimaryPiece.velocity_tsupport_subset {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] (p : PrimaryPiece X) (n : ℕ) : tsupport (p.velocity n) ⊆ tsupport (p.cutoff n)

theorem NavierStokes.CorrectionInitialization.PrimaryPiece.pressure_tsupport_subset {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] (p : PrimaryPiece X) (n : ℕ) : tsupport (p.pressure n) ⊆ tsupport (p.cutoff n)

theorem NavierStokes.CorrectionInitialization.PrimaryPiece.velocity_eq_zero_off_cutoff {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] (p : PrimaryPiece X) (n : ℕ) {x : X} (hx : x ∉ tsupport (p.cutoff n)) : p.velocity n x = 0

theorem NavierStokes.CorrectionInitialization.PrimaryConstruction.increment_twice_target {H : SmoothCovariance.Mat2} {T : SmoothCovariance.Vec2} (hc : SmoothCovariance.StrictCone H T) (j : Fin 2) : SignedCovariance.increment H T (2 • T) j = SmoothCovariance.amplitudes H T j

The signed inverse quotient at twice the primary target is exactly the positive primary square root; this identifies the two actual constructions.

noncomputable def NavierStokes.CorrectionInitialization.PrimaryConstruction.coefficients {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] (a : LinearWaveBounds.WaveCoefficients X) (s : WeightedClasses.StripData X) (d : LinearWaveBounds.GraphDirections X) (H : ℕ → X → SmoothCovariance.Mat2) (T : ℕ → X → SmoothCovariance.Vec2) (mask : ℕ → X → ℝ) (v Ndot : ℕ → X → PrimaryODE.Space) (A : ℕ → X → PrimaryODE.Space →L[ℝ] PrimaryODE.Space) (j : Fin 2) : LinearWaveBounds.WaveCoefficients X

Coefficients, given by SignedWaveUpdate.coefficients a s d H T (fun n x => (2 : ℝ) • T n x) mask v Ndot A j.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.PrimaryConstruction.piece {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] (a : LinearWaveBounds.WaveCoefficients X) (s : WeightedClasses.StripData X) (d : LinearWaveBounds.GraphDirections X) (H : ℕ → X → SmoothCovariance.Mat2) (T : ℕ → X → SmoothCovariance.Vec2) (mask : ℕ → X → ℝ) (v Ndot : ℕ → X → PrimaryODE.Space) (A : ℕ → X → PrimaryODE.Space →L[ℝ] PrimaryODE.Space) (cutoff : ℕ → X → ℝ) (j : Fin 2) : PrimaryPiece X

Piece, given by ⟨s, d, coefficients a s d H T mask v Ndot A j, cutoff⟩.

Equations

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

theorem NavierStokes.CorrectionInitialization.PrimaryConstruction.amplitude_eq_primary {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] (a : LinearWaveBounds.WaveCoefficients X) (s : WeightedClasses.StripData X) (d : LinearWaveBounds.GraphDirections X) (H : ℕ → X → SmoothCovariance.Mat2) (T : ℕ → X → SmoothCovariance.Vec2) (mask : ℕ → X → ℝ) (v Ndot : ℕ → X → PrimaryODE.Space) (A : ℕ → X → PrimaryODE.Space →L[ℝ] PrimaryODE.Space) (j : Fin 2) (n : ℕ) (x : X) (hc : SmoothCovariance.StrictCone (H n x) (T n x)) : (coefficients a s d H T mask v Ndot A j).amplitude n x = PrimaryPulseBounds.primaryCoefficient s H T mask v j n x

theorem NavierStokes.CorrectionInitialization.PrimaryConstruction.twice_target_class {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {s : WeightedClasses.StripData X} {T : ℕ → X → SmoothCovariance.Vec2} (hT : ∀ (i : Fin 2), WeightedClasses.MeanClass s 0 fun (n : ℕ) (x : X) => T n x i) (i : Fin 2) : WeightedClasses.MeanClass s 0 fun (n : ℕ) (x : X) => (2 • T n x) i

theorem NavierStokes.CorrectionInitialization.PrimaryConstruction.inputBounds {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {s : WeightedClasses.StripData X} {d : LinearWaveBounds.GraphDirections X} {a : LinearWaveBounds.WaveCoefficients X} {P₀ P : ℕ → X → ℝ} {α₀ κ : ℝ} (hbase : LinearWaveBounds.InputBounds s P₀ α₀ κ d a) {H : ℕ → X → SmoothCovariance.Mat2} {T : ℕ → X → SmoothCovariance.Vec2} {mask : ℕ → X → ℝ} {v Ndot : ℕ → X → PrimaryODE.Space} {A : ℕ → X → PrimaryODE.Space →L[ℝ] PrimaryODE.Space} (hcov : SignedWaveUpdate.CovarianceControl s H T) (hm : WeightedClasses.UnweightedClass s 0 mask) (hv : WeightedClasses.MemClass s P 0 v) (hN : PhaseJetBounds.PolynomialJets (CurlClassBounds.phaseDomain s) (a.normal s d)) (hNdot : WeightedClasses.UnweightedClass s 0 Ndot) (hA : WeightedClasses.UnweightedClass s 0 A) {b M : ℝ} (hb : 0 < b) (hlo : ∀ (n : ℕ), ∀ x ∈ s.domain, b ≤ ‖a.normal s d n x‖) (hhi : ∀ (n : ℕ), ∀ x ∈ s.domain, ‖a.normal s d n x‖ ≤ M) (hK : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / a.frequency n) (j : Fin 2) : LinearWaveBounds.InputBounds s P (1 / 2) κ d (coefficients a s d H T mask v Ndot A j)

The primary pressure and amplitude estimates come from their formulas; the input record supplies only the fixed background geometry.

theorem NavierStokes.CorrectionInitialization.PrimaryConstruction.phase_principal_zero {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {s : WeightedClasses.StripData X} {d : LinearWaveBounds.GraphDirections X} (a : LinearWaveBounds.WaveCoefficients X) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (pref : Fin 2 → ℕ → ℝ) (χ : ℕ → X → PhaseCalculus.Slow × ℝ) {T : ℕ → X → SmoothCovariance.Vec2} {mask : ℕ → X → ℝ} {Ndot : ℕ → X → PrimaryODE.Space} {A : ℕ → X → PrimaryODE.Space →L[ℝ] PrimaryODE.Space} (hscale : ∀ (n : ℕ), U.scale n = s.slow n) (hχ : PhaseJetBounds.PolynomialJets (PrimaryPulseBounds.phaseDomain s) χ) (hmap : ∀ (n : ℕ), ∀ x ∈ s.domain, χ n x ∈ U.carrier n ×ˢ Set.Ioo 0 1) (hcov : SignedWaveUpdate.CovarianceControl s (SignedWaveUpdate.phaseMatrix F pref χ) T) (hm : WeightedClasses.UnweightedClass s 0 mask) (hHf : SignedWaveUpdate.FrozenAlong d.fast (SignedWaveUpdate.phaseMatrix F pref χ)) (hTf : SignedWaveUpdate.FrozenAlong d.fast T) (hmf : SignedWaveUpdate.FrozenAlong d.fast mask) (hK : ∀ (n : ℕ), a.frequency n ≠ 0) (j : Fin 2) (hcoef : ∀ (n : ℕ), ContinuousOn (((F j).frame n).coefficient 1) (U.carrier n ×ˢ Set.Icc 0 ((F j).L n))) (hkin : ∀ (n : ℕ), ∀ x ∈ s.domain, ((F j).frame n).Kinematics (χ n x).1 (Set.Icc 0 ((F j).L n))) (hclock : ∀ (n : ℕ), ∀ x ∈ s.domain, ∀ (t : ℝ), χ n (x + t • d.fastField n x) = ((χ n x).1, (χ n x).2 + t / (F j).L n)) (hnormal : ∀ (n : ℕ), ∀ x ∈ s.domain, ((F j).frame n).normal ((χ n x).1, (F j).L n * (χ n x).2) = a.normal s d n x) (hmotion : ∀ (n : ℕ), ∀ x ∈ s.domain, ((F j).frame n).normalMotion ((χ n x).1, (F j).L n * (χ n x).2) = Ndot n x) (haction : ∀ (n : ℕ), ∀ x ∈ s.domain, ∀ (z : PrimaryODE.Space), MovingFrameODE.baseAction (((F j).frame n).F ((χ n x).1, (F j).L n * (χ n x).2)) (((F j).frame n).shear ((χ n x).1, (F j).L n * (χ n x).2)) z = (A n x) z) (hdamp : ∀ (n : ℕ), ∀ x ∈ s.domain, ((F j).frame n).viscosity ((χ n x).1, (F j).L n * (χ n x).2) = s.epsilon n * a.frequency n ^ 2 * ‖a.normal s d n x‖ ^ 2) (hphysical : ∀ (n : ℕ), ∀ x ∈ s.domain, CurlClassBounds.complexify ((A n x) (SignedWaveUpdate.phaseFundamental F χ j n x)) = LinearWaveResidual.shear (a.radius n) (a.frequencyBase n) (a.axialBase n) (d.radialField n) (fun (y : X) => CurlClassBounds.complexify (SignedWaveUpdate.phaseFundamental F χ j n y)) x) (n : ℕ) (x : X) : x ∈ s.domain → (coefficients a s d (SignedWaveUpdate.phaseMatrix F pref χ) T mask (SignedWaveUpdate.phaseFundamental F χ j) Ndot A j).principal s d n x = 0

The only ODE used here is the constructed normalized primary fundamental. In particular no principal equation for the output coefficient is assumed.

noncomputable def NavierStokes.CorrectionInitialization.PrimaryConstruction.physicalAction {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] (R F G : X → ℝ) (Vr : X → X) (x : X) : PrimaryODE.Space →L[ℝ] PrimaryODE.Space

The physical shear operator is built from the actual radial derivatives of the two background profiles.

Equations

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

theorem NavierStokes.CorrectionInitialization.PrimaryConstruction.physicalAction_eq_shear {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] (R F G : X → ℝ) (Vr : X → X) (v : X → PrimaryODE.Space) (x : X) : CurlClassBounds.complexify ((physicalAction R F G Vr x) (v x)) = LinearWaveResidual.shear R F G Vr (fun (y : X) => CurlClassBounds.complexify (v y)) x

theorem NavierStokes.CorrectionInitialization.PrimaryConstruction.physicalAction_class {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {s : WeightedClasses.StripData X} {d : LinearWaveBounds.GraphDirections X} {a : LinearWaveBounds.WaveCoefficients X} {P : ℕ → X → ℝ} {α κ : ℝ} (h : LinearWaveBounds.InputBounds s P α κ d a) : WeightedClasses.UnweightedClass s 0 fun (n : ℕ) => physicalAction (a.radius n) (a.frequencyBase n) (a.axialBase n) (d.radialField n)

The physical action has order zero because the fixed background is independent of the radial fast variable.

theorem NavierStokes.CorrectionInitialization.PrimaryConstruction.normal_pullback {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] (χ : X → PhaseCalculus.Slot) (ε p pz x0 : ℝ) (F G : PhaseCalculus.Slow → ℝ) (Vr Vθ Vz : X → X) {x : X} (hχ : DifferentiableAt ℝ χ x) (hF : DifferentiableAt ℝ F (χ x).1) (hG : DifferentiableAt ℝ G (χ x).1) (hr : (fderiv ℝ χ x) (Vr x) = PhaseCalculus.eR) (hθ : (fderiv ℝ χ x) (Vθ x) = PhaseCalculus.eTheta) (hz : (fderiv ℝ χ x) (Vz x) = ε • PhaseCalculus.eZ) : HarmonicCalculus.phaseNormal (fun (y : X) => (χ y).1.1) Vr Vθ Vz (PhaseCalculus.phase ε p pz x0 F G ∘ χ) x = PhaseCalculus.phaseNormal ε p pz x0 F G (χ x)

theorem NavierStokes.CorrectionInitialization.PrimaryConstruction.native_normal {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (P : PrimaryPulseBounds.PhaseConstruction U) (s : WeightedClasses.StripData X) (d : LinearWaveBounds.GraphDirections X) (χ : ℕ → X → PhaseCalculus.Slot) (b : ℕ → PhaseCalculus.Slow → ℝ) (amplitude : ℕ → X → HarmonicCalculus.ComplexVector) (pressure : ℕ → X → ℂ) (frequency : ℕ → ℝ) (hχ : PrimaryMaterialDefect.NativeCoordinates s d χ) (hmap : ∀ (n : ℕ), Set.MapsTo (fun (x : X) => (χ n x).1) s.domain (U.carrier n)) (heps : ∀ (n : ℕ), P.phase.epsilon n = s.epsilon n) (n : ℕ) {x : X} (hx : x ∈ s.domain) : (PrimaryMaterialDefect.coefficients P b χ amplitude pressure frequency).normal s d n x = P.phase.normal n ((χ n x).1, (χ n x).2.2)

theorem NavierStokes.CorrectionInitialization.PrimaryConstruction.native_slow_derivative {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {s : WeightedClasses.StripData X} {d : LinearWaveBounds.GraphDirections X} {χ : ℕ → X → PhaseCalculus.Slot} (hχ : PrimaryMaterialDefect.NativeCoordinates s d χ) (F : ℕ → PhaseCalculus.Slow → ℝ) (n : ℕ) {x : X} (hx : x ∈ s.domain) (hF : DifferentiableAt ℝ (F n) (χ n x).1) : HarmonicCalculus.along (d.radialField n) (fun (y : X) => F n (χ n y).1) x = PhaseCalculus.slowR (F n) (χ n x).1

theorem NavierStokes.CorrectionInitialization.PrimaryConstruction.native_slow_auxiliary {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {s : WeightedClasses.StripData X} {d : LinearWaveBounds.GraphDirections X} {χ : ℕ → X → PhaseCalculus.Slot} (hχ : PrimaryMaterialDefect.NativeCoordinates s d χ) (F : ℕ → PhaseCalculus.Slow → ℝ) (n : ℕ) {x : X} (hx : x ∈ s.domain) (hF : DifferentiableAt ℝ (F n) (χ n x).1) : (fderiv ℝ (fun (y : X) => F n (χ n y).1) x) d.auxiliary = 0

theorem NavierStokes.CorrectionInitialization.PrimaryConstruction.native_normal_jets {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (P : PrimaryPulseBounds.PhaseConstruction U) (s : WeightedClasses.StripData X) (d : LinearWaveBounds.GraphDirections X) (χ : ℕ → X → PhaseCalculus.Slot) (b : ℕ → PhaseCalculus.Slow → ℝ) (amplitude : ℕ → X → HarmonicCalculus.ComplexVector) (pressure : ℕ → X → ℂ) (frequency : ℕ → ℝ) (hχ : PrimaryMaterialDefect.NativeCoordinates s d χ) (hcoords : PhaseJetBounds.PolynomialJets (PrimaryPulseBounds.phaseDomain s) fun (n : ℕ) (x : X) => ((χ n x).1, (χ n x).2.2)) (hscale : ∀ (n : ℕ), U.scale n = s.slow n) (hmap : ∀ (n : ℕ), ∀ x ∈ s.domain, (χ n x).1 ∈ U.carrier n ∧ (χ n x).2.2 ∈ P.V n) (heps : ∀ (n : ℕ), P.phase.epsilon n = s.epsilon n) : PhaseJetBounds.PolynomialJets (CurlClassBounds.phaseDomain s) ((PrimaryMaterialDefect.coefficients P b χ amplitude pressure frequency).normal s d)

theorem NavierStokes.CorrectionInitialization.PrimaryConstruction.native_background_bounds {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (P : PrimaryPulseBounds.PhaseConstruction U) (s : WeightedClasses.StripData X) (d : LinearWaveBounds.GraphDirections X) (χ : ℕ → X → PhaseCalculus.Slot) (b : ℕ → PhaseCalculus.Slow → ℝ) (frequency : ℕ → ℝ) {κ : ℝ} (hχ : PrimaryMaterialDefect.NativeCoordinates s d χ) (hcoords : PhaseJetBounds.PolynomialJets (PrimaryPulseBounds.phaseDomain s) fun (n : ℕ) (x : X) => ((χ n x).1, (χ n x).2.2)) (hscale : ∀ (n : ℕ), U.scale n = s.slow n) (hmap : ∀ (n : ℕ), ∀ x ∈ s.domain, (χ n x).1 ∈ U.carrier n ∧ (χ n x).2.2 ∈ P.V n) (heps : ∀ (n : ℕ), P.phase.epsilon n = s.epsilon n) (hR : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 < (χ n x).1.1) (hζ : ∀ x ∈ s.domain, s.zeta x ≤ 1) (hb : WeightedClasses.UnweightedClass s 1 fun (n : ℕ) (x : X) => b n (χ n x).1) (hbs : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (b n) (U.carrier n)) (hκ : 0 ≤ κ) (hprofile : WeightedClasses.UnweightedClass s 0 fun (x : ℕ) => d.radialProfile) (hradial : WeightedClasses.BandBound s (-κ) d.radialScale) (hfast : WeightedClasses.BandBound s 0 d.fastScale) (hfrequency : WeightedClasses.BandBound s (-(1 / 2)) frequency) : LinearWaveBounds.InputBounds s (fun (x : ℕ) (x_1 : X) => 1) 0 κ d (PrimaryMaterialDefect.coefficients P b χ 0 0 frequency)

A raw background record with zero wave and pressure is verified from the actual phase, base jets and chart. Its material defect and phase-normal bounds are derived here, not supplied as output estimates.

theorem NavierStokes.CorrectionInitialization.PrimaryConstruction.native_normal_range {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (P : PrimaryPulseBounds.PhaseConstruction U) (s : WeightedClasses.StripData X) (d : LinearWaveBounds.GraphDirections X) (χ : ℕ → X → PhaseCalculus.Slot) (b : ℕ → PhaseCalculus.Slow → ℝ) (amplitude : ℕ → X → HarmonicCalculus.ComplexVector) (pressure : ℕ → X → ℂ) (frequency : ℕ → ℝ) (hχ : PrimaryMaterialDefect.NativeCoordinates s d χ) (hmap : ∀ (n : ℕ), ∀ x ∈ s.domain, (χ n x).1 ∈ U.carrier n ∧ (χ n x).2.2 ∈ P.V n) (heps : ∀ (n : ℕ), P.phase.epsilon n = s.epsilon n) (n : ℕ) {x : X} (hx : x ∈ s.domain) : P.b ≤ ‖(PrimaryMaterialDefect.coefficients P b χ amplitude pressure frequency).normal s d n x‖ ∧ ‖(PrimaryMaterialDefect.coefficients P b χ amplitude pressure frequency).normal s d n x‖ ≤ P.M ^ 2 + 3 * P.M

theorem NavierStokes.CorrectionInitialization.PrimaryConstruction.frame_jets {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (P : PrimaryPulseBounds.PhaseConstruction U) : PhaseJetBounds.FrameJets (U.slot P.V ⋯) P.frame

theorem NavierStokes.CorrectionInitialization.PrimaryConstruction.frame_coefficient_continuous {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (P : PrimaryPulseBounds.PhaseConstruction U) (n : ℕ) : ContinuousOn ((P.frame n).coefficient 1) (U.carrier n ×ˢ Set.Icc 0 (P.L n))

theorem NavierStokes.CorrectionInitialization.PrimaryConstruction.frame_tail_ne_zero {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (P : PrimaryPulseBounds.PhaseConstruction U) (n : ℕ) {z : PhaseCalculus.Slow × ℝ} (hz : z ∈ (U.slot P.V ⋯).carrier n) : MovingFrameODE.tail (P.phase.normal n z) ≠ 0

theorem NavierStokes.CorrectionInitialization.PrimaryConstruction.frame_normal {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (P : PrimaryPulseBounds.PhaseConstruction U) (n : ℕ) {z : PhaseCalculus.Slow × ℝ} (hz : z ∈ (U.slot P.V ⋯).carrier n) : (P.frame n).normal z = P.phase.normal n z

theorem NavierStokes.CorrectionInitialization.PrimaryConstruction.frame_kinematics {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (P : PrimaryPulseBounds.PhaseConstruction U) (n : ℕ) {q : PhaseCalculus.Slow} (hq : q ∈ U.carrier n) : (P.frame n).Kinematics q (Set.Icc 0 (P.L n))

theorem NavierStokes.CorrectionInitialization.PrimaryConstruction.frame_normalMotion {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (P : PrimaryPulseBounds.PhaseConstruction U) (n : ℕ) {z : PhaseCalculus.Slow × ℝ} (hz : z ∈ (U.slot P.V ⋯).carrier n) : (P.frame n).normalMotion z = P.phase.velocity n z

theorem NavierStokes.CorrectionInitialization.PrimaryConstruction.native_frame_action {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (P : PrimaryPulseBounds.PhaseConstruction U) (s : WeightedClasses.StripData X) (d : LinearWaveBounds.GraphDirections X) (χ : ℕ → X → PhaseCalculus.Slot) (b : ℕ → PhaseCalculus.Slow → ℝ) (frequency : ℕ → ℝ) (hχ : PrimaryMaterialDefect.NativeCoordinates s d χ) (hmap : ∀ (n : ℕ), Set.MapsTo (fun (x : X) => (χ n x).1) s.domain (U.carrier n)) (n : ℕ) {x : X} (hx : x ∈ s.domain) (v : PrimaryODE.Space) : MovingFrameODE.baseAction ((P.frame n).F ((χ n x).1, (χ n x).2.2)) ((P.frame n).shear ((χ n x).1, (χ n x).2.2)) v = (physicalAction ((PrimaryMaterialDefect.coefficients P b χ 0 0 frequency).radius n) ((PrimaryMaterialDefect.coefficients P b χ 0 0 frequency).frequencyBase n) ((PrimaryMaterialDefect.coefficients P b χ 0 0 frequency).axialBase n) (d.radialField n) x) v

noncomputable def NavierStokes.CorrectionInitialization.PrimaryConstruction.pulseCoordinates {X : Type} {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (P : PrimaryPulseBounds.PhaseConstruction U) (χ : ℕ → X → PhaseCalculus.Slot) : ℕ → X → PhaseCalculus.Slow × ℝ

Pulse coordinates, defined pointwise by ((χ n x).1, (χ n x).2.2 / P.L n).

Equations

• NavierStokes.CorrectionInitialization.PrimaryConstruction.pulseCoordinates P χ n x = ((χ n x).1, (χ n x).2.2 / P.L n)

theorem NavierStokes.CorrectionInitialization.PrimaryConstruction.pulseCoordinates_scaled {X : Type} {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (P : PrimaryPulseBounds.PhaseConstruction U) (χ : ℕ → X → PhaseCalculus.Slot) (n : ℕ) (x : X) : P.L n * (pulseCoordinates P χ n x).2 = (χ n x).2.2

noncomputable def NavierStokes.CorrectionInitialization.PrimaryConstruction.nativeCoefficients {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (pref : Fin 2 → ℕ → ℝ) (s : WeightedClasses.StripData X) (d : LinearWaveBounds.GraphDirections X) (χ : ℕ → X → PhaseCalculus.Slot) (b : ℕ → PhaseCalculus.Slow → ℝ) (frequency : ℕ → ℝ) (T : ℕ → X → SmoothCovariance.Vec2) (mask : ℕ → X → ℝ) (j : Fin 2) : LinearWaveBounds.WaveCoefficients X

Native coefficients as an element of WaveCoefficients X.

Equations

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

theorem NavierStokes.CorrectionInitialization.PrimaryConstruction.native_principal_zero {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (pref : Fin 2 → ℕ → ℝ) (s : WeightedClasses.StripData X) (d : LinearWaveBounds.GraphDirections X) (χ : ℕ → X → PhaseCalculus.Slot) (b : ℕ → PhaseCalculus.Slow → ℝ) (frequency : ℕ → ℝ) (T : ℕ → X → SmoothCovariance.Vec2) (mask : ℕ → X → ℝ) (j : Fin 2) (hχ : PrimaryMaterialDefect.NativeCoordinates s d χ) (hscale : ∀ (n : ℕ), U.scale n = s.slow n) (hcoords : PhaseJetBounds.PolynomialJets (PrimaryPulseBounds.phaseDomain s) (pulseCoordinates (F j) χ)) (hmap : ∀ (n : ℕ), ∀ x ∈ s.domain, (χ n x).1 ∈ U.carrier n ∧ (χ n x).2.2 ∈ Set.Ioo 0 ((F j).L n)) (heps : ∀ (n : ℕ), (F j).phase.epsilon n = s.epsilon n) (hν : ∀ (n : ℕ), (F j).viscosity n = s.epsilon n * frequency n ^ 2) (hcov : SignedWaveUpdate.CovarianceControl s (SignedWaveUpdate.phaseMatrix F pref (pulseCoordinates (F j) χ)) T) (hm : WeightedClasses.UnweightedClass s 0 mask) (hslow : ∀ (n : ℕ) (x : X) (t : ℝ), (χ n (x + t • d.fast)).1 = (χ n x).1) (hTf : SignedWaveUpdate.FrozenAlong d.fast T) (hmf : SignedWaveUpdate.FrozenAlong d.fast mask) (hclock : ∀ (n : ℕ), ∀ x ∈ s.domain, ∀ (t : ℝ), χ n (x + t • d.fastField n x) = ((χ n x).1, (χ n x).2.1, (χ n x).2.2 + t)) (hfrequency : ∀ (n : ℕ), frequency n ≠ 0) (n : ℕ) (x : X) : x ∈ s.domain → (nativeCoefficients F pref s d χ b frequency T mask j).principal s d n x = 0

The native coefficient has its actual primary pressure and satisfies the principal equation by the constructed ODE. All matching assumptions concern the chart, the scalar viscosity and the primitive slow inputs.

theorem NavierStokes.CorrectionInitialization.PrimaryConstruction.native_inputBounds {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (pref : Fin 2 → ℕ → ℝ) (s : WeightedClasses.StripData X) (d : LinearWaveBounds.GraphDirections X) (χ : ℕ → X → PhaseCalculus.Slot) (b : ℕ → PhaseCalculus.Slow → ℝ) (frequency : ℕ → ℝ) (T : ℕ → X → SmoothCovariance.Vec2) (mask : ℕ → X → ℝ) (j : Fin 2) {κ : ℝ} (hχ : PrimaryMaterialDefect.NativeCoordinates s d χ) (hscale : ∀ (n : ℕ), U.scale n = s.slow n) (hnative : PhaseJetBounds.PolynomialJets (PrimaryPulseBounds.phaseDomain s) fun (n : ℕ) (x : X) => ((χ n x).1, (χ n x).2.2)) (hcoords : PhaseJetBounds.PolynomialJets (PrimaryPulseBounds.phaseDomain s) (pulseCoordinates (F j) χ)) (hmap : ∀ (n : ℕ), ∀ x ∈ s.domain, (χ n x).1 ∈ U.carrier n ∧ (χ n x).2.2 ∈ Set.Ioo 0 ((F j).L n)) (heps : ∀ (n : ℕ), (F j).phase.epsilon n = s.epsilon n) (hR : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 < (χ n x).1.1) (hζ : ∀ x ∈ s.domain, s.zeta x ≤ 1) (hb : WeightedClasses.UnweightedClass s 1 fun (n : ℕ) (x : X) => b n (χ n x).1) (hbs : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (b n) (U.carrier n)) (hκ : 0 ≤ κ) (hprofile : WeightedClasses.UnweightedClass s 0 fun (x : ℕ) => d.radialProfile) (hradial : WeightedClasses.BandBound s (-κ) d.radialScale) (hfast : WeightedClasses.BandBound s 0 d.fastScale) (hfrequency : WeightedClasses.BandBound s (-(1 / 2)) frequency) (hK : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / frequency n) (hcov : SignedWaveUpdate.CovarianceControl s (SignedWaveUpdate.phaseMatrix F pref (pulseCoordinates (F j) χ)) T) (hm : WeightedClasses.UnweightedClass s 0 mask) : LinearWaveBounds.InputBounds s (SignedWaveUpdate.phaseEnvelope F (pulseCoordinates (F j) χ) j) (1 / 2) κ d (nativeCoefficients F pref s d χ b frequency T mask j)

All primary coefficient and pressure estimates are derived from the same native ODE and matrix. The background record has zero amplitude and zero pressure, so no primary output estimate is an input.

theorem NavierStokes.CorrectionInitialization.PrimaryConstruction.native_amplitude_eq_uncut {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (pref : Fin 2 → ℕ → ℝ) (s : WeightedClasses.StripData X) (d : LinearWaveBounds.GraphDirections X) (χ : ℕ → X → PhaseCalculus.Slot) (b : ℕ → PhaseCalculus.Slow → ℝ) (frequency : ℕ → ℝ) (T : ℕ → X → SmoothCovariance.Vec2) (mask : ℕ → X → ℝ) (j : Fin 2) (n : ℕ) (x : X) (hc : mask n x ≠ 0 → SmoothCovariance.StrictCone (SignedWaveUpdate.phaseMatrix F pref (pulseCoordinates (F j) χ) n x) (T n x)) : (nativeCoefficients F pref s d χ b frequency T mask j).amplitude n x = PrimaryPulseBounds.uncutPrimaryWave s pref (fun (k : Fin 2) => (F k).frame) (fun (k : Fin 2) => (F k).lam) (fun (k : Fin 2) => (F k).u) (fun (k : Fin 2) => (F k).L) (pulseCoordinates (F j) χ) T mask j n x

theorem NavierStokes.CorrectionInitialization.PrimaryConstruction.native_cutoff_amplitude {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (pref : Fin 2 → ℕ → ℝ) (s : WeightedClasses.StripData X) (d : LinearWaveBounds.GraphDirections X) (χ : ℕ → X → PhaseCalculus.Slot) (b : ℕ → PhaseCalculus.Slow → ℝ) (frequency : ℕ → ℝ) (T : ℕ → X → SmoothCovariance.Vec2) (mask : ℕ → X → ℝ) (j : Fin 2) (n : ℕ) (x : X) (hc : mask n x ≠ 0 → SmoothCovariance.StrictCone (SignedWaveUpdate.phaseMatrix F pref (pulseCoordinates (F j) χ) n x) (T n x)) : ((nativeCoefficients F pref s d χ b frequency T mask j).withCutoff fun (n : ℕ) (x : X) => GaussianTailFlat.profile (pulseCoordinates (F j) χ n x).2).amplitude n x = PrimaryPulseBounds.phaseWave s F pref (pulseCoordinates (F j) χ) T mask j n x

The canonical coefficient and the covariance pulse contain the same Gaussian cutoff, applied exactly once.

theorem NavierStokes.CorrectionInitialization.PrimaryConstruction.native_tangent {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (pref : Fin 2 → ℕ → ℝ) (s : WeightedClasses.StripData X) (d : LinearWaveBounds.GraphDirections X) (χ : ℕ → X → PhaseCalculus.Slot) (b : ℕ → PhaseCalculus.Slow → ℝ) (frequency : ℕ → ℝ) (T : ℕ → X → SmoothCovariance.Vec2) (mask : ℕ → X → ℝ) (j : Fin 2) (hχ : PrimaryMaterialDefect.NativeCoordinates s d χ) (hmap : ∀ (n : ℕ), ∀ x ∈ s.domain, (χ n x).1 ∈ U.carrier n ∧ (χ n x).2.2 ∈ (F j).V n) (heps : ∀ (n : ℕ), (F j).phase.epsilon n = s.epsilon n) (n : ℕ) {x : X} (hx : x ∈ s.domain) : HarmonicCalculus.normalDot ((nativeCoefficients F pref s d χ b frequency T mask j).normal s d n x) ((nativeCoefficients F pref s d χ b frequency T mask j).amplitude n x) = 0

theorem NavierStokes.CorrectionInitialization.PrimaryConstruction.physicalAction_invariant {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {θ : X} {R F G : X → ℝ} {Vr : X → X} (hR : CopyAngularInvariance.Invariant θ R) (hF : CopyAngularInvariance.Invariant θ F) (hG : CopyAngularInvariance.Invariant θ G) (hVr : CopyAngularInvariance.Invariant θ Vr) : CopyAngularInvariance.Invariant θ (physicalAction R F G Vr)

theorem NavierStokes.CorrectionInitialization.PrimaryConstruction.native_angularInputs {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (pref : Fin 2 → ℕ → ℝ) (s : WeightedClasses.StripData X) (d : LinearWaveBounds.GraphDirections X) (χ : ℕ → X → PhaseCalculus.Slot) (b : ℕ → PhaseCalculus.Slow → ℝ) (frequency : ℕ → ℝ) (T : ℕ → X → SmoothCovariance.Vec2) (mask cutoff : ℕ → X → ℝ) (j : Fin 2) (hangle : ∀ (n : ℕ) (x : X) (t : ℝ), χ n (x + t • d.angular) = ((χ n x).1, (χ n x).2.1 + t, (χ n x).2.2)) (hc : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (χ n) s.domain) (hmap : ∀ (n : ℕ), Set.MapsTo (fun (x : X) => (χ n x).1) s.domain (U.carrier n)) (hT : SignedWaveUpdate.FrozenAlong d.angular T) (hm : SignedWaveUpdate.FrozenAlong d.angular mask) (hcut : SignedWaveUpdate.FrozenAlong d.angular cutoff) (hprofile : CopyAngularInvariance.Invariant d.angular d.radialProfile) : have a := PrimaryMaterialDefect.coefficients (F j) b χ 0 0 frequency; have ψ := pulseCoordinates (F j) χ; SignedWaveUpdate.AngularInputs s d a (SignedWaveUpdate.phaseMatrix F pref ψ) T (fun (n : ℕ) (x : X) => 2 • T n x) mask (SignedWaveUpdate.phaseFundamental F ψ j) (fun (n : ℕ) (x : X) => (F j).phase.velocity n ((χ n x).1, (χ n x).2.2)) (fun (n : ℕ) => physicalAction (a.radius n) (a.frequencyBase n) (a.axialBase n) (d.radialField n)) cutoff (F j).phase.p

Angular symmetry is derived from the coordinate translation and the primitive slow data, including the actual reconstructed primary pressure.

noncomputable def NavierStokes.CorrectionInitialization.PrimaryConstruction.sourcePair {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {d h : ℝ} {vr vt : PartitionedCovariance.Plane} (F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (sys : PartitionedCovariance.SlotSystem d h vr vt) (label : PartitionedCovariance.UnsignedLabel) (n : ℕ) (q : PhaseCalculus.Slow) (hq : q ∈ U.carrier n) (stretch : PartitionedCovariance.Vec2) (hci : ∀ (j : Fin 2), 0 < stretch j) (hfits : ∀ (j : Fin 2), (F j).L n ≤ 2 * sys.radius / stretch j) (mode : Fin 2 → ℤ) (hmode : ∀ (j : Fin 2), mode j ≠ 0) (phase : Fin 2 → PartitionedCovariance.Plane → ℝ) : PrimaryFieldAssembly.SourcePair PhaseCalculus.Slow sys label

Both physical columns are constructed from the same native primary frames used above; continuity and kinematics are proved rather than stored as fresh assumptions.

Equations

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

theorem NavierStokes.CorrectionInitialization.PrimaryConstruction.sourcePair_matrix {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {d h : ℝ} {vr vt : PartitionedCovariance.Plane} (F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (sys : PartitionedCovariance.SlotSystem d h vr vt) (label : PartitionedCovariance.UnsignedLabel) (n : ℕ) (q : PhaseCalculus.Slow) (hq : q ∈ U.carrier n) (stretch : PartitionedCovariance.Vec2) (hci : ∀ (j : Fin 2), 0 < stretch j) (hfits : ∀ (j : Fin 2), (F j).L n ≤ 2 * sys.radius / stretch j) (mode : Fin 2 → ℤ) (hmode : ∀ (j : Fin 2), mode j ≠ 0) (phase : Fin 2 → PartitionedCovariance.Plane → ℝ) : (sourcePair F sys label n q hq stretch hci hfits mode hmode phase).sourceMatrix = PrimaryPulseBounds.phaseCovariance F (fun (j : Fin 2) (m : ℕ) => PartitionedCovariance.nativePrefactor vr vt sys.radius * stretch j * (F j).L m) n q

noncomputable def NavierStokes.CorrectionInitialization.PrimaryPiece.excludedBlock {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (p : PrimaryPiece (D × ℝ)) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) : CorrectionState.HarmonicBlock D

Excluded block, given by ErrorHarmonics.gaussianBlock p.directions p.cutoff p.coefficients.amplitude 0 1 p.coefficients.frequency Φ kp.

Equations

• p.excludedBlock Φ kp = NavierStokes.ErrorHarmonics.gaussianBlock p.directions p.cutoff p.coefficients.amplitude 0 1 p.coefficients.frequency Φ kp

theorem NavierStokes.CorrectionInitialization.PrimaryPiece.excludedBlock_represents {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (p : PrimaryPiece (D × ℝ)) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) (hcut : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (p.cutoff n)) (hcutAngle : ErrorHarmonics.AngleIndependent p.cutoff) (ha : ErrorHarmonics.AngleIndependent p.coefficients.amplitude) (hphase : ∀ (n : ℕ) (x : D) (θ : ℝ), p.coefficients.frequency n * p.coefficients.phase n (x, θ) = p.coefficients.frequency n * Φ n x + ↑(kp n) * θ) : (p.excludedBlock Φ kp).oscillation = p.excluded

theorem NavierStokes.CorrectionInitialization.PrimaryPiece.excluded_angularContinuous {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (p : PrimaryPiece (D × ℝ)) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) (hcut : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (p.cutoff n)) (hcutAngle : ErrorHarmonics.AngleIndependent p.cutoff) (ha : ErrorHarmonics.AngleIndependent p.coefficients.amplitude) (hphase : ∀ (n : ℕ) (x : D) (θ : ℝ), p.coefficients.frequency n * p.coefficients.phase n (x, θ) = p.coefficients.frequency n * Φ n x + ↑(kp n) * θ) : CorrectionStep.AngularContinuous p.excluded

theorem NavierStokes.CorrectionInitialization.PrimaryPiece.excluded_mean_zero {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (p : PrimaryPiece (D × ℝ)) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) (hkp : ∀ (n : ℕ), kp n ≠ 0) (hcut : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (p.cutoff n)) (hcutAngle : ErrorHarmonics.AngleIndependent p.cutoff) (ha : ErrorHarmonics.AngleIndependent p.coefficients.amplitude) (hphase : ∀ (n : ℕ) (x : D) (θ : ℝ), p.coefficients.frequency n * p.coefficients.phase n (x, θ) = p.coefficients.frequency n * Φ n x + ↑(kp n) * θ) : CorrectionStep.angularMeanVector p.excluded = 0

The retained primary Gaussian error is a genuine nonzero angular harmonic, so its actual angular mean vanishes exactly.

noncomputable def NavierStokes.CorrectionInitialization.seed {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type} (labels : Finset ι) (pieces : ι → PrimaryPiece (D × ℝ)) (baseError : CorrectionState.Oscillation D) : CorrectionState.State D

Initial mean velocities vanish; the primary fields are actual finite label sums of cutoff curls and their homogeneous pressure modes.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.bandSeed {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type} (labels : ℕ → Finset ι) (pieces : ι → PrimaryPiece (D × ℝ)) (baseError : CorrectionState.Oscillation D) : CorrectionState.State D

The active labels may depend on the chart band. No bound on their total cardinality is inserted into the construction or its class estimates.

Equations

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

theorem NavierStokes.CorrectionInitialization.bandSeed_covariance {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type} (labels : ℕ → Finset ι) (pieces : ι → PrimaryPiece (D × ℝ)) (baseError : CorrectionState.Oscillation D) (i j : Fin 3) : (bandSeed labels pieces baseError).covariance i j = CorrectionState.bilinearCovariance (LabelSumBounds.fieldSum labels fun (l : ι) => (pieces l).velocity) (LabelSumBounds.fieldSum labels fun (l : ι) => (pieces l).velocity) i j

noncomputable def NavierStokes.CorrectionInitialization.primaryStage {ι S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (p : CorrectionState.ReconstructionData) (c : CorrectionState.Context (CorrectionState.Lift S)) (labels : Finset ι) (pieces : ι → PrimaryPiece (CorrectionState.Lift S × ℝ)) (baseError : CorrectionState.Oscillation (CorrectionState.Lift S)) : CorrectionState.State (CorrectionState.Lift S)

Primary stage, given by reconstructPressure p c (seed labels pieces baseError).

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.afterTemporal {ι S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (p : CorrectionState.ReconstructionData) (h : ℝ) (axial : S × PressureStream.Plane) (c : CorrectionState.Context (CorrectionState.Lift S)) (labels : Finset ι) (pieces : ι → PrimaryPiece (CorrectionState.Lift S × ℝ)) (baseError : CorrectionState.Oscillation (CorrectionState.Lift S)) : CorrectionState.State (CorrectionState.Lift S)

After temporal, given by temporalStage p h axial c (primaryStage p c labels pieces baseError).

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.afterRank {ι S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (p : CorrectionState.ReconstructionData) (r : CorrectionState.RankData S) (h : ℝ) (axial : S × PressureStream.Plane) (c : CorrectionState.Context (CorrectionState.Lift S)) (labels : Finset ι) (pieces : ι → PrimaryPiece (CorrectionState.Lift S × ℝ)) (baseError : CorrectionState.Oscillation (CorrectionState.Lift S)) : CorrectionState.State (CorrectionState.Lift S)

After rank, given by rankStage p r axial c (afterTemporal p h axial c labels pieces baseError).

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.retainPressureAlias {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (p : CorrectionState.ReconstructionData) (c : CorrectionState.Context (CorrectionState.Lift S)) (u : CorrectionState.State (CorrectionState.Lift S)) : CorrectionState.State (CorrectionState.Lift S)

The current pressure alias is retained once, after the final pressure reconstruction. Earlier obsolete pressure aliases are not accumulated.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.initialized {ι S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (p : CorrectionState.ReconstructionData) (r : CorrectionState.RankData S) (h : ℝ) (axial : S × PressureStream.Plane) (c : CorrectionState.Context (CorrectionState.Lift S)) (labels : Finset ι) (pieces : ι → PrimaryPiece (CorrectionState.Lift S × ℝ)) (baseError : CorrectionState.Oscillation (CorrectionState.Lift S)) : CorrectionState.State (CorrectionState.Lift S)

Initialized, given by retainPressureAlias p c (afterRank p r h axial c labels pieces baseError).

Equations

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

theorem NavierStokes.CorrectionInitialization.initialized_oscillation {ι S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (p : CorrectionState.ReconstructionData) (r : CorrectionState.RankData S) (h : ℝ) (axial : S × PressureStream.Plane) (c : CorrectionState.Context (CorrectionState.Lift S)) (labels : Finset ι) (pieces : ι → PrimaryPiece (CorrectionState.Lift S × ℝ)) (baseError : CorrectionState.Oscillation (CorrectionState.Lift S)) : (initialized p r h axial c labels pieces baseError).oscillation = ∑ l ∈ labels, (pieces l).velocity

theorem NavierStokes.CorrectionInitialization.initialized_errors {ι S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (p : CorrectionState.ReconstructionData) (r : CorrectionState.RankData S) (h : ℝ) (axial : S × PressureStream.Plane) (c : CorrectionState.Context (CorrectionState.Lift S)) (labels : Finset ι) (pieces : ι → PrimaryPiece (CorrectionState.Lift S × ℝ)) (baseError : CorrectionState.Oscillation (CorrectionState.Lift S)) : (initialized p r h axial c labels pieces baseError).errors.total = baseError + ∑ l ∈ labels, (pieces l).excluded + CorrectionState.temporalAlias p h c (primaryStage p c labels pieces baseError) + CorrectionState.pressureAlias p c (afterRank p r h axial c labels pieces baseError)

theorem NavierStokes.CorrectionInitialization.initialized_error_components {ι S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (p : CorrectionState.ReconstructionData) (r : CorrectionState.RankData S) (h : ℝ) (axial : S × PressureStream.Plane) (c : CorrectionState.Context (CorrectionState.Lift S)) (labels : Finset ι) (pieces : ι → PrimaryPiece (CorrectionState.Lift S × ℝ)) (baseError : CorrectionState.Oscillation (CorrectionState.Lift S)) : (initialized p r h axial c labels pieces baseError).errors.base = baseError ∧ (initialized p r h axial c labels pieces baseError).errors.gaussian = ∑ l ∈ labels, (pieces l).excluded ∧ (initialized p r h axial c labels pieces baseError).errors.aliasError = CorrectionState.temporalAlias p h c (primaryStage p c labels pieces baseError) + CorrectionState.pressureAlias p c (afterRank p r h axial c labels pieces baseError)

theorem NavierStokes.CorrectionInitialization.initialized_reconstructed {ι S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (p : CorrectionState.ReconstructionData) (r : CorrectionState.RankData S) (h : ℝ) (axial : S × PressureStream.Plane) (c : CorrectionState.Context (CorrectionState.Lift S)) (labels : Finset ι) (pieces : ι → PrimaryPiece (CorrectionState.Lift S × ℝ)) (baseError : CorrectionState.Oscillation (CorrectionState.Lift S)) : CorrectionState.reconstructPressure p c (initialized p r h axial c labels pieces baseError) = initialized p r h axial c labels pieces baseError

theorem NavierStokes.CorrectionInitialization.initialized_zeroMasses {ι S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (p : CorrectionState.ReconstructionData) (r : CorrectionState.RankData S) (h : ℝ) (axial : S × PressureStream.Plane) (c : CorrectionState.Context (CorrectionState.Lift S)) (labels : Finset ι) (pieces : ι → PrimaryPiece (CorrectionState.Lift S × ℝ)) (baseError : CorrectionState.Oscillation (CorrectionState.Lift S)) (ha : 0 < p.inner) (hd : 0 < p.exponent) (hθ : ∀ (n : ℕ), ContDiff ℝ (↑⊤) ((primaryStage p c labels pieces baseError).thetaResidual c n)) (hz : ∀ (n : ℕ), ContDiff ℝ (↑⊤) ((primaryStage p c labels pieces baseError).axialResidual c n)) (hpθ : ∀ (n : ℕ), PressureStream.TorusPeriodicLift ((primaryStage p c labels pieces baseError).thetaResidual c n)) (hpz : ∀ (n : ℕ), PressureStream.TorusPeriodicLift ((primaryStage p c labels pieces baseError).axialResidual c n)) (hsz : ∀ (n : ℕ), RadialAlias.RadiallySupported p.inner p.outer ((primaryStage p c labels pieces baseError).axialResidual c n)) (hg : DefectIncrementBounds.RankGeometry p r c (afterTemporal p h axial c labels pieces baseError)) (hm : DefectIncrementBounds.ShellTriple p.inner p.outer (afterTemporal p h axial c labels pieces baseError).mean) (hi : DefectIncrementBounds.ShellTriple p.inner p.outer (CorrectionState.rankIncrement p r axial c (afterTemporal p h axial c labels pieces baseError))) : CorrectionState.ZeroMasses (initialized p r h axial c labels pieces baseError)

The two actual integrated masses remain zero through both updates.

theorem NavierStokes.CorrectionInitialization.initialized_radial_residual {ι S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (p : CorrectionState.ReconstructionData) (r : CorrectionState.RankData S) (h : ℝ) (axial : S × PressureStream.Plane) (c : CorrectionState.Context (CorrectionState.Lift S)) (labels : Finset ι) (pieces : ι → PrimaryPiece (CorrectionState.Lift S × ℝ)) (baseError : CorrectionState.Oscillation (CorrectionState.Lift S)) (ha : 0 < p.inner) (hd : 0 < p.exponent) (hoperator : ∀ (f : CorrectionState.ScalarField (CorrectionState.Lift S)) (n : ℕ) (x : CorrectionState.Lift S), c.operators.dr f n x = PressureStream.graphDr (PressureStream.physicalSpeed p.exponent (p.frequency n)) (0, p.radialDirection) (f n) x) (hsmooth : ∀ (n : ℕ), ContDiff ℝ (↑⊤) ((initialized p r h axial c labels pieces baseError).gr c n)) (hsupport : ∀ (n : ℕ), RadialAlias.RadiallySupported p.inner p.outer ((initialized p r h axial c labels pieces baseError).gr c n)) (n : ℕ) (x : CorrectionState.Lift S) : (initialized p r h axial c labels pieces baseError).radialResidual c n x - CorrectionState.pressureAlias p c (afterRank p r h axial c labels pieces baseError) n (x, 0) 0 = -PressureStream.rho p.inner p.outer ⋯ x.1 * CorrectionState.pressureDefect c (initialized p r h axial c labels pieces baseError) n x.2.1

The actual current pressure reconstruction controls the radial residual by the computed pressure defect, with its exact alias retained.

noncomputable def NavierStokes.CorrectionInitialization.GaugeInitialization.primaryStage {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {ι : Type} (g : VariableGaugeMean.GaugeData S) (c : CorrectionState.Context (PressureStream.Lift S)) (labels : Finset ι) (pieces : ι → PrimaryPiece (PressureStream.Lift S × ℝ)) (baseError : CorrectionState.Oscillation (PressureStream.Lift S)) : CorrectionState.State (PressureStream.Lift S)

The physical-gauge pipeline uses the actual slow-variable-dependent cutoff endpoints and an explicit common torus index at every step.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.GaugeInitialization.afterTemporal {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {ι : Type} (g : VariableGaugeMean.GaugeData S) (h : ℝ) (index : ℕ → ℕ) (axial : S × PressureStream.Plane) (c : CorrectionState.Context (PressureStream.Lift S)) (labels : Finset ι) (pieces : ι → PrimaryPiece (PressureStream.Lift S × ℝ)) (baseError : CorrectionState.Oscillation (PressureStream.Lift S)) : CorrectionState.State (PressureStream.Lift S)

After temporal, given by temporalStageState g h index axial c (primaryStage g c labels pieces baseError).

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.GaugeInitialization.afterRank {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {ι : Type} (g : VariableGaugeMean.GaugeData S) (r : CorrectionState.RankData S) (h : ℝ) (index : ℕ → ℕ) (axial : S × PressureStream.Plane) (c : CorrectionState.Context (PressureStream.Lift S)) (labels : Finset ι) (pieces : ι → PrimaryPiece (PressureStream.Lift S × ℝ)) (baseError : CorrectionState.Oscillation (PressureStream.Lift S)) : CorrectionState.State (PressureStream.Lift S)

After rank, given by rankStageState g r axial c (afterTemporal g h index axial c labels pieces baseError).

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.GaugeInitialization.retainPressureAlias {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (g : VariableGaugeMean.GaugeData S) (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) : CorrectionState.State (PressureStream.Lift S)

Retain pressure alias, given by { u with errors := ⟨u.errors.base, u.errors.gaussian, u.errors.aliasError + pressureAliasState g c u⟩ }.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.GaugeInitialization.initialized {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {ι : Type} (g : VariableGaugeMean.GaugeData S) (r : CorrectionState.RankData S) (h : ℝ) (index : ℕ → ℕ) (axial : S × PressureStream.Plane) (c : CorrectionState.Context (PressureStream.Lift S)) (labels : Finset ι) (pieces : ι → PrimaryPiece (PressureStream.Lift S × ℝ)) (baseError : CorrectionState.Oscillation (PressureStream.Lift S)) : CorrectionState.State (PressureStream.Lift S)

Initialized, given by retainPressureAlias g c (afterRank g r h index axial c labels pieces baseError).

Equations

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

theorem NavierStokes.CorrectionInitialization.GaugeInitialization.initialized_oscillation {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {ι : Type} (g : VariableGaugeMean.GaugeData S) (r : CorrectionState.RankData S) (h : ℝ) (index : ℕ → ℕ) (axial : S × PressureStream.Plane) (c : CorrectionState.Context (PressureStream.Lift S)) (labels : Finset ι) (pieces : ι → PrimaryPiece (PressureStream.Lift S × ℝ)) (baseError : CorrectionState.Oscillation (PressureStream.Lift S)) : (initialized g r h index axial c labels pieces baseError).oscillation = ∑ l ∈ labels, (pieces l).velocity

theorem NavierStokes.CorrectionInitialization.GaugeInitialization.initialized_error_components {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {ι : Type} (g : VariableGaugeMean.GaugeData S) (r : CorrectionState.RankData S) (h : ℝ) (index : ℕ → ℕ) (axial : S × PressureStream.Plane) (c : CorrectionState.Context (PressureStream.Lift S)) (labels : Finset ι) (pieces : ι → PrimaryPiece (PressureStream.Lift S × ℝ)) (baseError : CorrectionState.Oscillation (PressureStream.Lift S)) : (initialized g r h index axial c labels pieces baseError).errors.base = baseError ∧ (initialized g r h index axial c labels pieces baseError).errors.gaussian = ∑ l ∈ labels, (pieces l).excluded ∧ (initialized g r h index axial c labels pieces baseError).errors.aliasError = VariableGaugeMean.temporalAliasState g h index c (primaryStage g c labels pieces baseError) + VariableGaugeMean.pressureAliasState g c (afterRank g r h index axial c labels pieces baseError)

theorem NavierStokes.CorrectionInitialization.GaugeInitialization.initialized_errors {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {ι : Type} (g : VariableGaugeMean.GaugeData S) (r : CorrectionState.RankData S) (h : ℝ) (index : ℕ → ℕ) (axial : S × PressureStream.Plane) (c : CorrectionState.Context (PressureStream.Lift S)) (labels : Finset ι) (pieces : ι → PrimaryPiece (PressureStream.Lift S × ℝ)) (baseError : CorrectionState.Oscillation (PressureStream.Lift S)) : (initialized g r h index axial c labels pieces baseError).errors.total = baseError + ∑ l ∈ labels, (pieces l).excluded + VariableGaugeMean.temporalAliasState g h index c (primaryStage g c labels pieces baseError) + VariableGaugeMean.pressureAliasState g c (afterRank g r h index axial c labels pieces baseError)

theorem NavierStokes.CorrectionInitialization.GaugeInitialization.initialized_reconstructed {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {ι : Type} (g : VariableGaugeMean.GaugeData S) (r : CorrectionState.RankData S) (h : ℝ) (index : ℕ → ℕ) (axial : S × PressureStream.Plane) (c : CorrectionState.Context (PressureStream.Lift S)) (labels : Finset ι) (pieces : ι → PrimaryPiece (PressureStream.Lift S × ℝ)) (baseError : CorrectionState.Oscillation (PressureStream.Lift S)) : VariableGaugeMean.reconstructState g c (initialized g r h index axial c labels pieces baseError) = initialized g r h index axial c labels pieces baseError

noncomputable def NavierStokes.CorrectionInitialization.GaugeInitialization.primaryBands {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {ι : Type} (g : VariableGaugeMean.GaugeData S) (c : CorrectionState.Context (PressureStream.Lift S)) (labels : ℕ → Finset ι) (pieces : ι → PrimaryPiece (PressureStream.Lift S × ℝ)) (baseError : CorrectionState.Oscillation (PressureStream.Lift S)) : CorrectionState.State (PressureStream.Lift S)

Primary bands, given by reconstructState g c (bandSeed labels pieces baseError).

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.GaugeInitialization.temporalBands {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {ι : Type} (g : VariableGaugeMean.GaugeData S) (h : ℝ) (index : ℕ → ℕ) (axial : S × PressureStream.Plane) (c : CorrectionState.Context (PressureStream.Lift S)) (labels : ℕ → Finset ι) (pieces : ι → PrimaryPiece (PressureStream.Lift S × ℝ)) (baseError : CorrectionState.Oscillation (PressureStream.Lift S)) : CorrectionState.State (PressureStream.Lift S)

Temporal bands, given by temporalStageState g h index axial c (primaryBands g c labels pieces baseError).

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.GaugeInitialization.rankBands {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {ι : Type} (g : VariableGaugeMean.GaugeData S) (r : CorrectionState.RankData S) (h : ℝ) (index : ℕ → ℕ) (axial : S × PressureStream.Plane) (c : CorrectionState.Context (PressureStream.Lift S)) (labels : ℕ → Finset ι) (pieces : ι → PrimaryPiece (PressureStream.Lift S × ℝ)) (baseError : CorrectionState.Oscillation (PressureStream.Lift S)) : CorrectionState.State (PressureStream.Lift S)

Rank bands, given by rankStageState g r axial c (temporalBands g h index axial c labels pieces baseError).

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.GaugeInitialization.initializedBands {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {ι : Type} (g : VariableGaugeMean.GaugeData S) (r : CorrectionState.RankData S) (h : ℝ) (index : ℕ → ℕ) (axial : S × PressureStream.Plane) (c : CorrectionState.Context (PressureStream.Lift S)) (labels : ℕ → Finset ι) (pieces : ι → PrimaryPiece (PressureStream.Lift S × ℝ)) (baseError : CorrectionState.Oscillation (PressureStream.Lift S)) : CorrectionState.State (PressureStream.Lift S)

Initialized bands, given by retainPressureAlias g c (rankBands g r h index axial c labels pieces baseError).

Equations

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

theorem NavierStokes.CorrectionInitialization.GaugeInitialization.initializedBands_oscillation {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {ι : Type} (g : VariableGaugeMean.GaugeData S) (r : CorrectionState.RankData S) (h : ℝ) (index : ℕ → ℕ) (axial : S × PressureStream.Plane) (c : CorrectionState.Context (PressureStream.Lift S)) (labels : ℕ → Finset ι) (pieces : ι → PrimaryPiece (PressureStream.Lift S × ℝ)) (baseError : CorrectionState.Oscillation (PressureStream.Lift S)) : (initializedBands g r h index axial c labels pieces baseError).oscillation = LabelSumBounds.fieldSum labels fun (l : ι) => (pieces l).velocity

theorem NavierStokes.CorrectionInitialization.GaugeInitialization.initializedBands_error_components {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {ι : Type} (g : VariableGaugeMean.GaugeData S) (r : CorrectionState.RankData S) (h : ℝ) (index : ℕ → ℕ) (axial : S × PressureStream.Plane) (c : CorrectionState.Context (PressureStream.Lift S)) (labels : ℕ → Finset ι) (pieces : ι → PrimaryPiece (PressureStream.Lift S × ℝ)) (baseError : CorrectionState.Oscillation (PressureStream.Lift S)) : (initializedBands g r h index axial c labels pieces baseError).errors.base = baseError ∧ ((initializedBands g r h index axial c labels pieces baseError).errors.gaussian = LabelSumBounds.fieldSum labels fun (l : ι) => (pieces l).excluded) ∧ (initializedBands g r h index axial c labels pieces baseError).errors.aliasError = VariableGaugeMean.temporalAliasState g h index c (primaryBands g c labels pieces baseError) + VariableGaugeMean.pressureAliasState g c (rankBands g r h index axial c labels pieces baseError)

theorem NavierStokes.CorrectionInitialization.GaugeInitialization.initializedBands_errors {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {ι : Type} (g : VariableGaugeMean.GaugeData S) (r : CorrectionState.RankData S) (h : ℝ) (index : ℕ → ℕ) (axial : S × PressureStream.Plane) (c : CorrectionState.Context (PressureStream.Lift S)) (labels : ℕ → Finset ι) (pieces : ι → PrimaryPiece (PressureStream.Lift S × ℝ)) (baseError : CorrectionState.Oscillation (PressureStream.Lift S)) : (initializedBands g r h index axial c labels pieces baseError).errors.total = (baseError + LabelSumBounds.fieldSum labels fun (l : ι) => (pieces l).excluded) + VariableGaugeMean.temporalAliasState g h index c (primaryBands g c labels pieces baseError) + VariableGaugeMean.pressureAliasState g c (rankBands g r h index axial c labels pieces baseError)

theorem NavierStokes.CorrectionInitialization.GaugeInitialization.initializedBands_reconstructed {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {ι : Type} (g : VariableGaugeMean.GaugeData S) (r : CorrectionState.RankData S) (h : ℝ) (index : ℕ → ℕ) (axial : S × PressureStream.Plane) (c : CorrectionState.Context (PressureStream.Lift S)) (labels : ℕ → Finset ι) (pieces : ι → PrimaryPiece (PressureStream.Lift S × ℝ)) (baseError : CorrectionState.Oscillation (PressureStream.Lift S)) : VariableGaugeMean.reconstructState g c (initializedBands g r h index axial c labels pieces baseError) = initializedBands g r h index axial c labels pieces baseError

theorem NavierStokes.CorrectionInitialization.angularMeanVector_sum {D ι : Type} (labels : Finset ι) (f : ι → CorrectionState.Oscillation D) (hc : ∀ l ∈ labels, CorrectionStep.AngularContinuous (f l)) : CorrectionStep.angularMeanVector (∑ l ∈ labels, f l) = ∑ l ∈ labels, CorrectionStep.angularMeanVector (f l)

theorem NavierStokes.CorrectionInitialization.initialized_meanGood {ι S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (p : CorrectionState.ReconstructionData) (r : CorrectionState.RankData S) (h : ℝ) (axial : S × PressureStream.Plane) (c : CorrectionState.Context (CorrectionState.Lift S)) (labels : Finset ι) (pieces : ι → PrimaryPiece (CorrectionState.Lift S × ℝ)) (baseError : CorrectionState.Oscillation (CorrectionState.Lift S)) (hb : CorrectionStep.AngularContinuous baseError) (hg : ∀ l ∈ labels, CorrectionStep.AngularContinuous (pieces l).excluded) (hz : ∀ l ∈ labels, CorrectionStep.angularMeanVector (pieces l).excluded = 0) : (initialized p r h axial c labels pieces baseError).meanGoodResidual c = (initialized p r h axial c labels pieces baseError).reducedMeanResidual c - fun (n : ℕ) (x : CorrectionState.Lift S) => CorrectionState.temporalAlias p h c (primaryStage p c labels pieces baseError) n (x, 0) + CorrectionState.pressureAlias p c (afterRank p r h axial c labels pieces baseError) n (x, 0)

The stored base error cancels once. The primary Gaussian means vanish, and the two literal alias fields remain with their actual signs.

theorem NavierStokes.CorrectionInitialization.angularMeanVector_fieldSum {D ι : Type} (labels : ℕ → Finset ι) (f : ι → CorrectionState.Oscillation D) (hc : ∀ (n : ℕ), ∀ l ∈ labels n, ∀ (x : D) (i : Fin 3), Continuous fun (θ : ℝ) => f l n (x, θ) i) : CorrectionStep.angularMeanVector (LabelSumBounds.fieldSum labels f) = fun (n : ℕ) (x : D) (i : Fin 3) => ∑ l ∈ labels n, CorrectionStep.angularMeanVector (f l) n x i

theorem NavierStokes.CorrectionInitialization.GaugeInitialization.initializedBands_meanGood {ι S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (g : VariableGaugeMean.GaugeData S) (r : CorrectionState.RankData S) (h : ℝ) (index : ℕ → ℕ) (axial : S × PressureStream.Plane) (c : CorrectionState.Context (CorrectionState.Lift S)) (labels : ℕ → Finset ι) (pieces : ι → PrimaryPiece (CorrectionState.Lift S × ℝ)) (baseError : CorrectionState.Oscillation (CorrectionState.Lift S)) (hb : CorrectionStep.AngularContinuous baseError) (hg : ∀ (n : ℕ), ∀ l ∈ labels n, ∀ (x : CorrectionState.Lift S) (i : Fin 3), Continuous fun (θ : ℝ) => (pieces l).excluded n (x, θ) i) (hz : ∀ (n : ℕ), ∀ l ∈ labels n, ∀ (x : CorrectionState.Lift S), CorrectionStep.angularMeanVector (pieces l).excluded n x = 0) : (initializedBands g r h index axial c labels pieces baseError).meanGoodResidual c = (initializedBands g r h index axial c labels pieces baseError).reducedMeanResidual c - fun (n : ℕ) (x : PressureStream.Lift S) => VariableGaugeMean.temporalAliasState g h index c (primaryBands g c labels pieces baseError) n (x, 0) + VariableGaugeMean.pressureAliasState g c (rankBands g r h index axial c labels pieces baseError) n (x, 0)

The band-dependent physical-gauge construction retains exactly the two current aliases. The base error cancels once and each primary Gaussian has zero actual angular mean.

theorem NavierStokes.CorrectionInitialization.GaugeInitialization.initializedBands_meanResidualBounds {ι S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (g : VariableGaugeMean.GaugeData S) (r : CorrectionState.RankData S) (h : ℝ) (index : ℕ → ℕ) (axial : S × PressureStream.Plane) (c : CorrectionState.Context (CorrectionState.Lift S)) (labels : ℕ → Finset ι) (pieces : ι → PrimaryPiece (CorrectionState.Lift S × ℝ)) (baseError : CorrectionState.Oscillation (CorrectionState.Lift S)) (hb : CorrectionStep.AngularContinuous baseError) (hg : ∀ (n : ℕ), ∀ l ∈ labels n, ∀ (x : CorrectionState.Lift S) (i : Fin 3), Continuous fun (θ : ℝ) => (pieces l).excluded n (x, θ) i) (hz : ∀ (n : ℕ), ∀ l ∈ labels n, ∀ (x : CorrectionState.Lift S), CorrectionStep.angularMeanVector (pieces l).excluded n x = 0) {s : WeightedClasses.StripData (CorrectionState.Lift S)} {σ : ℝ} (hθ : WeightedClasses.MeanClass s (1 + σ) ((rankBands g r h index axial c labels pieces baseError).thetaResidual c)) (hz' : WeightedClasses.MeanClass s (1 + σ) fun (n : ℕ) (x : CorrectionState.Lift S) => (rankBands g r h index axial c labels pieces baseError).axialResidual c n x - VariableGaugeMean.temporalAliasState g h index c (primaryBands g c labels pieces baseError) n (x, 0) 2) : CorrectionState.MeanResidualBounds s σ c (initializedBands g r h index axial c labels pieces baseError)

Bookkeeping for the two tangential estimates after the actual rank stage: no class estimate on either excluded alias is inserted.

noncomputable def NavierStokes.CorrectionInitialization.AngularRestriction.insert {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] : D →L[ℝ] D × ℝ

Insert, given by (ContinuousLinearMap.id ℝ D).prod 0.

Equations

• NavierStokes.CorrectionInitialization.AngularRestriction.insert = (ContinuousLinearMap.id ℝ D).prod 0

@[simp]

theorem NavierStokes.CorrectionInitialization.AngularRestriction.insert_apply {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (x : D) : insert x = (x, 0)

theorem NavierStokes.CorrectionInitialization.AngularRestriction.norm_insert_le {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] : ‖insert‖ ≤ 1

noncomputable def NavierStokes.CorrectionInitialization.AngularRestriction.strip {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData (D × ℝ)) : WeightedClasses.StripData D

The actual coefficient domain on the angular slice.

Equations

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

theorem NavierStokes.CorrectionInitialization.AngularRestriction.class_restrict {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData (D × ℝ)} {w : ℕ → D × ℝ → ℝ} {α : ℝ} {f : ℕ → D × ℝ → E} (hf : WeightedClasses.MemClass s w α f) : WeightedClasses.MemClass (strip s) (fun (n : ℕ) (x : D) => w n (x, 0)) α fun (n : ℕ) (x : D) => f n (x, 0)

Restriction is a genuine linear pullback of every jet, with norm one.

theorem NavierStokes.CorrectionInitialization.AngularRestriction.waveClass_restrict {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData (D × ℝ)} {P : ℕ → D × ℝ → ℝ} {α : ℝ} {f : ℕ → D × ℝ → E} (hf : WeightedClasses.WaveClass s P α f) : WeightedClasses.WaveClass (strip s) (fun (n : ℕ) (x : D) => P n (x, 0)) α fun (n : ℕ) (x : D) => f n (x, 0)

noncomputable def NavierStokes.CorrectionInitialization.PrimaryHarmonics.block {D : Type} (a : LinearWaveBounds.WaveCoefficients (D × ℝ)) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) : CorrectionState.HarmonicBlock D

A primary mode and its pressure, with the actual conjugate negative mode.

Equations

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

theorem NavierStokes.CorrectionInitialization.PrimaryHarmonics.block_band {D : Type} (a : LinearWaveBounds.WaveCoefficients (D × ℝ)) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) : (block a Φ kp).BandLimited 1

theorem NavierStokes.CorrectionInitialization.PrimaryHarmonics.conjugatePair_class {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α : ℝ} (a : ℕ → D → ℂ) (ha : WeightedClasses.WaveClass s P α a) (j m : ℤ) : WeightedClasses.WaveClass s P α fun (n : ℕ) (x : D) => (ErrorHarmonics.conjugatePair j (a n)).coeff m x

theorem NavierStokes.CorrectionInitialization.PrimaryHarmonics.block_coefficient_class {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData (D × ℝ)} {P : ℕ → D × ℝ → ℝ} {α : ℝ} (a : LinearWaveBounds.WaveCoefficients (D × ℝ)) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) (ha : ∀ (i : Fin 3), WeightedClasses.WaveClass s P α fun (n : ℕ) (x : D × ℝ) => a.amplitude n x i) (i : Fin 3) (j : ℤ) : WeightedClasses.WaveClass (AngularRestriction.strip s) (fun (n : ℕ) (x : D) => P n (x, 0)) α fun (n : ℕ) (x : D) => ((block a Φ kp).velocity n i).coeff j x

theorem NavierStokes.CorrectionInitialization.PrimaryHarmonics.block_pressure_class {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData (D × ℝ)} {P : ℕ → D × ℝ → ℝ} {α : ℝ} (a : LinearWaveBounds.WaveCoefficients (D × ℝ)) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) (ha : WeightedClasses.WaveClass s P α a.pressure) (j : ℤ) : WeightedClasses.WaveClass (AngularRestriction.strip s) (fun (n : ℕ) (x : D) => P n (x, 0)) α fun (n : ℕ) (x : D) => ((block a Φ kp).pressure n).coeff j x

theorem NavierStokes.CorrectionInitialization.PrimaryHarmonics.block_velocity_represents {D : Type} (a : LinearWaveBounds.WaveCoefficients (D × ℝ)) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) (ha : ErrorHarmonics.AngleIndependent a.amplitude) (hphase : ∀ (n : ℕ) (x : D) (θ : ℝ), a.frequency n * a.phase n (x, θ) = a.frequency n * Φ n x + ↑(kp n) * θ) (n : ℕ) (x : D × ℝ) (i : Fin 3) : (block a Φ kp).oscillation n x i = (HarmonicCalculus.vectorMode (a.frequency n) (a.phase n) (a.amplitude n) x i).re

theorem NavierStokes.CorrectionInitialization.PrimaryHarmonics.block_pressure_represents {D : Type} (a : LinearWaveBounds.WaveCoefficients (D × ℝ)) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) (ha : ErrorHarmonics.AngleIndependent a.pressure) (hphase : ∀ (n : ℕ) (x : D) (θ : ℝ), a.frequency n * a.phase n (x, θ) = a.frequency n * Φ n x + ↑(kp n) * θ) (n : ℕ) (x : D × ℝ) : (block a Φ kp).oscillatoryPressure n x = (HarmonicCalculus.mode (a.frequency n) (a.phase n) (a.pressure n) x).re

noncomputable def NavierStokes.CorrectionInitialization.PrimaryPiece.harmonicBlock {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (p : PrimaryPiece (D × ℝ)) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) : CorrectionState.HarmonicBlock D

Harmonic block, given by PrimaryHarmonics.block p.exactCoefficients Φ kp.

Equations

• p.harmonicBlock Φ kp = NavierStokes.CorrectionInitialization.PrimaryHarmonics.block p.exactCoefficients Φ kp

noncomputable def NavierStokes.CorrectionInitialization.PrimaryPiece.tangentBlock {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (p : PrimaryPiece (D × ℝ)) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) : CorrectionState.HarmonicBlock D

Tangent block, given by PrimaryHarmonics.block (p.coefficients.withCutoff p.cutoff) Φ kp.

Equations

• p.tangentBlock Φ kp = NavierStokes.CorrectionInitialization.PrimaryHarmonics.block (p.coefficients.withCutoff p.cutoff) Φ kp

noncomputable def NavierStokes.CorrectionInitialization.PrimaryPiece.differenceCoefficients {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (p : PrimaryPiece (D × ℝ)) : LinearWaveBounds.WaveCoefficients (D × ℝ)

Difference coefficients as an element of WaveCoefficients (D × ℝ).

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.PrimaryPiece.differenceBlock {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (p : PrimaryPiece (D × ℝ)) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) : CorrectionState.HarmonicBlock D

Difference block, given by PrimaryHarmonics.block p.differenceCoefficients Φ kp.

Equations

• p.differenceBlock Φ kp = NavierStokes.CorrectionInitialization.PrimaryHarmonics.block p.differenceCoefficients Φ kp

theorem NavierStokes.CorrectionInitialization.PrimaryPiece.harmonicBlock_represents {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (p : PrimaryPiece (D × ℝ)) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) (ha : ErrorHarmonics.AngleIndependent p.exactCoefficients.amplitude) (hp : ErrorHarmonics.AngleIndependent p.exactCoefficients.pressure) (hphase : ∀ (n : ℕ) (x : D) (θ : ℝ), p.coefficients.frequency n * p.coefficients.phase n (x, θ) = p.coefficients.frequency n * Φ n x + ↑(kp n) * θ) : (p.harmonicBlock Φ kp).oscillation = p.velocity ∧ (p.harmonicBlock Φ kp).oscillatoryPressure = p.pressure

theorem NavierStokes.CorrectionInitialization.PrimaryPiece.differenceBlock_represents {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (p : PrimaryPiece (D × ℝ)) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) (ha : ErrorHarmonics.AngleIndependent p.exactCoefficients.amplitude) (ht : ErrorHarmonics.AngleIndependent (p.coefficients.withCutoff p.cutoff).amplitude) (hphase : ∀ (n : ℕ) (x : D) (θ : ℝ), p.coefficients.frequency n * p.coefficients.phase n (x, θ) = p.coefficients.frequency n * Φ n x + ↑(kp n) * θ) : (p.differenceBlock Φ kp).oscillation = p.velocity - p.tangentVelocity

theorem NavierStokes.CorrectionInitialization.PrimaryPiece.harmonic_cumulative_bounds {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (p : PrimaryPiece (D × ℝ)) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) {P : ℕ → D × ℝ → ℝ} (hp : LinearWaveBounds.InputBounds p.strip P (1 / 2) ChartScales.kappa p.directions p.coefficients) (hcut : WeightedClasses.UnweightedClass p.strip 0 p.cutoff) {R : D × ℝ → ℝ} (hR : p.coefficients.radius = fun (x : ℕ) => R) (hN : PhaseJetBounds.PolynomialJets (CurlClassBounds.phaseDomain p.strip) (p.coefficients.normal p.strip p.directions)) {b M : ℝ} (hb : 0 < b) (hlo : ∀ (n : ℕ), ∀ x ∈ p.strip.domain, b ≤ ‖p.coefficients.normal p.strip p.directions n x‖) (hhi : ∀ (n : ℕ), ∀ x ∈ p.strip.domain, ‖p.coefficients.normal p.strip p.directions n x‖ ≤ M) (hK : WeightedClasses.BandBound p.strip (1 / 2) fun (n : ℕ) => 1 / p.coefficients.frequency n) : have s := AngularRestriction.strip p.strip; have P0 := fun (n : ℕ) (x : D) => P n (x, 0); (∀ (i : Fin 3) (j : ℤ), WeightedClasses.WaveClass s P0 (1 / 2) fun (n : ℕ) (x : D) => ((p.harmonicBlock Φ kp).velocity n i).coeff j x) ∧ (∀ (i : Fin 3) (j : ℤ), WeightedClasses.WaveClass s P0 (17 / 25) fun (n : ℕ) (x : D) => ((p.differenceBlock Φ kp).velocity n i).coeff j x) ∧ ∀ (j : ℤ), WeightedClasses.WaveClass s P0 1 fun (n : ℕ) (x : D) => ((p.harmonicBlock Φ kp).pressure n).coeff j x

The cumulative bounds belong to the actual finite harmonic blocks representing the cutoff curl and its difference from the primary tangent.

theorem NavierStokes.CorrectionInitialization.zeroMean_gr {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (hm : u.mean = { radial := 0, angular := 0, axial := 0 }) : u.gr c = -(c.operators.radialDiv 1 (u.covariance 0 0) + c.operators.dz (u.covariance 2 0) - c.operators.invRadius * u.covariance 1 1)

theorem NavierStokes.CorrectionInitialization.zeroMean_theta {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (hm : u.mean = { radial := 0, angular := 0, axial := 0 }) : u.thetaResidual c = c.operators.radialDiv 2 (u.covariance 0 1) + c.operators.dz (u.covariance 2 1) - c.operators.radialDiv 2 c.virtualTheta

theorem NavierStokes.CorrectionInitialization.zeroMean_axial {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (hm : u.mean = { radial := 0, angular := 0, axial := 0 }) : u.axialResidual c = c.operators.radialDiv 1 (u.covariance 0 2) + c.operators.dz (u.covariance 2 2 + u.pressure) - c.operators.radialDiv 1 c.virtualAxial

theorem NavierStokes.CorrectionInitialization.zeroMean_gr_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ : ℝ} (c : CorrectionState.Context D) (u : CorrectionState.State D) (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hm : u.mean = { radial := 0, angular := 0, axial := 0 }) (hW : ∀ (i j : Fin 3), WeightedClasses.MeanClass s 1 (u.covariance i j)) : WeightedClasses.MeanClass s (1 - κ) (u.gr c)

theorem NavierStokes.CorrectionInitialization.zeroMean_theta_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ : ℝ} (c : CorrectionState.Context D) (u : CorrectionState.State D) (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hm : u.mean = { radial := 0, angular := 0, axial := 0 }) (hW : ∀ (i j : Fin 3), WeightedClasses.MeanClass s 1 (u.covariance i j)) (hT : WeightedClasses.MeanClass s 1 c.virtualTheta) : WeightedClasses.MeanClass s (1 - κ) (u.thetaResidual c)

theorem NavierStokes.CorrectionInitialization.zeroMean_axial_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ : ℝ} (c : CorrectionState.Context D) (u : CorrectionState.State D) (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hm : u.mean = { radial := 0, angular := 0, axial := 0 }) (hW : ∀ (i j : Fin 3), WeightedClasses.MeanClass s 1 (u.covariance i j)) (hT : WeightedClasses.MeanClass s 1 c.virtualAxial) (hp : WeightedClasses.MeanClass s (1 - κ) u.pressure) : WeightedClasses.MeanClass s (1 - κ) (u.axialResidual c)

theorem NavierStokes.CorrectionInitialization.zeroMean_gr_shell {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} (ha : 0 < a) (c : CorrectionState.Context (CorrectionState.Lift S)) (u : CorrectionState.State (CorrectionState.Lift S)) (ho : DefectIncrementBounds.PositiveOperators c.operators) (hm : u.mean = { radial := 0, angular := 0, axial := 0 }) (hW : ∀ (i j : Fin 3), DefectIncrementBounds.Shell a b (u.covariance i j)) : DefectIncrementBounds.Shell a b (u.gr c)

theorem NavierStokes.CorrectionInitialization.zeroMean_thetaDefect {S : Type} (c : CorrectionState.Context (CorrectionState.Lift S)) (u : CorrectionState.State (CorrectionState.Lift S)) (hm : u.mean = { radial := 0, angular := 0, axial := 0 }) : CorrectionState.thetaDefect c u = CorrectionState.radialMoment 2 (u.covariance 2 1)

theorem NavierStokes.CorrectionInitialization.zeroMean_axialDefect {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (c : CorrectionState.Context (CorrectionState.Lift S)) (u : CorrectionState.State (CorrectionState.Lift S)) (hm : u.mean = { radial := 0, angular := 0, axial := 0 }) : CorrectionState.axialDefect c u = CorrectionState.radialMoment 1 (u.covariance 2 2) - (1 / 2) • CorrectionState.radialMoment 2 (u.gr c)

theorem NavierStokes.CorrectionInitialization.zeroMean_reconstructed_bounds {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : CorrectionState.ReconstructionData) (ha : 0 < r.inner) (hd : 0 < r.exponent) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (c : CorrectionState.Context (CorrectionState.Lift S)) (u : CorrectionState.State (CorrectionState.Lift S)) (ho : MeanIncrementBounds.OperatorBounds (WeightedRadialPrimitive.logStripData r.inner r.outer cL cR ha hcL hcR ε L hε hεone hL) c.operators ChartScales.kappa) (hop : DefectIncrementBounds.PositiveOperators c.operators) (hm : u.mean = { radial := 0, angular := 0, axial := 0 }) (hW : ∀ (i j : Fin 3), WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData r.inner r.outer cL cR ha hcL hcR ε L hε hεone hL) 1 (u.covariance i j)) (hWs : ∀ (i j : Fin 3), DefectIncrementBounds.Shell r.inner r.outer (u.covariance i j)) (hθ : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData r.inner r.outer cL cR ha hcL hcR ε L hε hεone hL) 1 c.virtualTheta) (hz : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData r.inner r.outer cL cR ha hcL hcR ε L hε hεone hL) 1 c.virtualAxial) : have s := WeightedRadialPrimitive.logStripData r.inner r.outer cL cR ha hcL hcR ε L hε hεone hL; WeightedClasses.MeanClass s (1 - ChartScales.kappa) ((CorrectionState.reconstructPressure r c u).gr c) ∧ WeightedClasses.MeanClass s (1 - ChartScales.kappa) (CorrectionState.reconstructPressure r c u).pressure ∧ WeightedClasses.MeanClass s (1 - ChartScales.kappa) ((CorrectionState.reconstructPressure r c u).thetaResidual c) ∧ WeightedClasses.MeanClass s (1 - ChartScales.kappa) ((CorrectionState.reconstructPressure r c u).axialResidual c) ∧ CorrectionState.CumulativeBounds s (CorrectionState.reconstructPressure r c u)

Before the temporal update, the pressure is the actual compact primitive of the radial equation. Its class is derived from the covariance.

theorem NavierStokes.CorrectionInitialization.zeroMean_debt_mem {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (c : CorrectionState.Context (CorrectionState.Lift S)) (u : CorrectionState.State (CorrectionState.Lift S)) (ho : MeanIncrementBounds.OperatorBounds (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε L hε hεone hL) c.operators ChartScales.kappa) (hop : DefectIncrementBounds.PositiveOperators c.operators) (hm : u.mean = { radial := 0, angular := 0, axial := 0 }) (hW : ∀ (i j : Fin 3), WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε L hε hεone hL) 1 (u.covariance i j)) (hWs : ∀ (i j : Fin 3), DefectIncrementBounds.Shell a b (u.covariance i j)) (i : Fin 3) : WeightedClasses.UnweightedClass (MeanMomentBounds.slowStripData ε L hε hεone hL) (1 - ChartScales.kappa) fun (n : ℕ) (x : S) => CorrectionState.debt c u n x i

All three incoming debts are actual radial moments. No defect bound is an input to this initial estimate.

theorem NavierStokes.CorrectionInitialization.AuxiliaryAverage.periodic_sub {S : Type} {f g : CorrectionState.Lift S → ℝ} (hf : PressureStream.TorusPeriodicLift f) (hg : PressureStream.TorusPeriodicLift g) : PressureStream.TorusPeriodicLift (f - g)

theorem NavierStokes.CorrectionInitialization.AuxiliaryAverage.meanBar_mem {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b cL cR : ℝ} (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) {α : ℝ} {f : CorrectionState.ScalarField (CorrectionState.Lift S)} (hf : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε L hε hεone hL) α f) (hfc : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hp : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (f n)) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε L hε hεone hL) α (StateMomentBalances.meanBar f)

The actual torus average preserves the flat mean class.

theorem NavierStokes.CorrectionInitialization.AuxiliaryAverage.matched_flux_mem {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b cL cR : ℝ} (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (R R0 T T0 : CorrectionState.ScalarField (CorrectionState.Lift S)) (hR : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (R n)) (hR0 : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (R0 n)) (hT : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (T n)) (hT0 : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (T0 n)) (hpR : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (R n)) (hpR0 : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (R0 n)) (hpT : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (T n)) (hpT0 : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (T0 n)) (hcurl : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε L hε hεone hL) (3 / 2 - ChartScales.kappa) (R - R0)) (hvirtual : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε L hε hεone hL) 2 (T - T0)) (hmatch : MeanIncrementBounds.Agree (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε L hε hεone hL).domain (StateMomentBalances.meanBar R0) (StateMomentBalances.meanBar T0)) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε L hε hεone hL) (3 / 2 - ChartScales.kappa) (StateMomentBalances.meanBar R - StateMomentBalances.meanBar T)

Exact leading covariance cancellation transfers the curl-product and higher-virtual-flux orders to the actual averaged radial flux.

theorem NavierStokes.CorrectionInitialization.AuxiliaryAverage.fluxBalance_mem {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b cL cR : ℝ} (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (o : MeanIncrementBounds.Operators (CorrectionState.Lift S)) (hop : DefectIncrementBounds.PositiveOperators o) (ho : MeanIncrementBounds.OperatorBounds (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε L hε hεone hL) o ChartScales.kappa) (hprofile : ∀ (R : ℝ) (z : S) (Y : PressureStream.Plane), o.radialProfile (R, z, Y) = o.radialProfile (R, z, 0)) (R A T : CorrectionState.ScalarField (CorrectionState.Lift S)) (c : ℝ) (hR : DefectIncrementBounds.Shell a b R) (hA : DefectIncrementBounds.Shell a b A) (hT : DefectIncrementBounds.Shell a b T) (hpR : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (R n)) (hpA : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (A n)) (hpT : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (T n)) (hflux : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε L hε hεone hL) (3 / 2 - ChartScales.kappa) (StateMomentBalances.meanBar R - StateMomentBalances.meanBar T)) (haxial : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε L hε hεone hL) (1 - ChartScales.kappa) A) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε L hε hεone hL) (149 / 100) (StateMomentBalances.meanBar (o.radialDiv c R + o.dz A - o.radialDiv c T))

The initial bar exponent 1.49 follows from the actual averaged flux balance, a curl covariance error, and the axial derivative gain.

theorem NavierStokes.CorrectionInitialization.MovingInitialization.zeroMean_gr_supportedGauge {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} {V : Set S} (hV : IsOpen V) {ell : S → ℝ} (hell : ContinuousOn ell V) (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) (hm : u.mean = { radial := 0, angular := 0, axial := 0 }) (hW : ∀ (i j : Fin 3) (n : ℕ), VariableGaugeMean.SupportedGauge a b ell V (u.covariance i j n)) (n : ℕ) : VariableGaugeMean.SupportedGauge a b ell V (u.gr c n)

The literal radial source retains the moving support of the actual covariance, including every differentiated term.

theorem NavierStokes.CorrectionInitialization.MovingInitialization.zeroMean_gr_smooth {coord a b : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (c : CorrectionState.Context LocalSignedRequest.Point) (u : CorrectionState.State LocalSignedRequest.Point) (hop : LocalRankDefect.LocalOperators U.carrier c.operators) (hm : u.mean = { radial := 0, angular := 0, axial := 0 }) (hW : ∀ (i j : Fin 3) (n : ℕ), ContDiffOn ℝ (↑⊤) (u.covariance i j n) (PhysicalMeanDomain.slowDomain U.carrier)) (hWs : ∀ (i j : Fin 3) (n : ℕ), VariableGaugeMean.SupportedGauge a b (VariableGaugeMean.qLength coord) U.carrier (u.covariance i j n)) (n : ℕ) : ContDiffOn ℝ (↑⊤) (u.gr c n) (PhysicalMeanDomain.slowDomain U.carrier)

Smoothness on the full valid slow domain follows from a containing annulus and the actual covariance support; no smooth extension of a positive-time totalization is used.

theorem NavierStokes.CorrectionInitialization.MovingInitialization.zeroMean_reconstructed_bounds {coord cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData PressureStream.Plane) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (c : CorrectionState.Context LocalSignedRequest.Point) (u : CorrectionState.State LocalSignedRequest.Point) (ho : MeanIncrementBounds.OperatorBounds (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) c.operators ChartScales.kappa) (hop : LocalRankDefect.LocalOperators U.carrier c.operators) (hm : u.mean = { radial := 0, angular := 0, axial := 0 }) (hW : ∀ (i j : Fin 3), WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) 1 (u.covariance i j)) (hWc : ∀ (i j : Fin 3) (n : ℕ), ContDiffOn ℝ (↑⊤) (u.covariance i j n) (PhysicalMeanDomain.slowDomain U.carrier)) (hWs : ∀ (i j : Fin 3) (n : ℕ), VariableGaugeMean.SupportedGauge g.radial.inner g.radial.outer (VariableGaugeMean.qLength coord) U.carrier (u.covariance i j n)) (hθ : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) 1 c.virtualTheta) (hz : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) 1 c.virtualAxial) : have st := LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL; WeightedClasses.MeanClass st (1 - ChartScales.kappa) (u.gr c) ∧ WeightedClasses.MeanClass st (1 - ChartScales.kappa) (VariableGaugeMean.reconstructState g c u).pressure ∧ WeightedClasses.MeanClass st (1 - ChartScales.kappa) ((VariableGaugeMean.reconstructState g c u).thetaResidual c) ∧ WeightedClasses.MeanClass st (1 - ChartScales.kappa) ((VariableGaugeMean.reconstructState g c u).axialResidual c) ∧ CorrectionState.CumulativeBounds st (VariableGaugeMean.reconstructState g c u)

Actual moving-gauge initial pressure and raw tangential residuals, derived from the covariance and virtual stresses.

theorem NavierStokes.CorrectionInitialization.MovingInitialization.zeroMean_debt_mem {coord a b cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (c : CorrectionState.Context LocalSignedRequest.Point) (u : CorrectionState.State LocalSignedRequest.Point) (ho : MeanIncrementBounds.OperatorBounds (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) c.operators ChartScales.kappa) (hop : LocalRankDefect.LocalOperators U.carrier c.operators) (hm : u.mean = { radial := 0, angular := 0, axial := 0 }) (hW : ∀ (i j : Fin 3), WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) 1 (u.covariance i j)) (hWc : ∀ (i j : Fin 3) (n : ℕ), ContDiffOn ℝ (↑⊤) (u.covariance i j n) (PhysicalMeanDomain.slowDomain U.carrier)) (hWs : ∀ (i j : Fin 3) (n : ℕ), VariableGaugeMean.SupportedGauge a b (VariableGaugeMean.qLength coord) U.carrier (u.covariance i j n)) (i : Fin 3) : WeightedClasses.UnweightedClass (PhysicalMeanDomain.localSlowStripData U.carrier ⋯ ε L hε hεone hL) (1 - ChartScales.kappa) fun (n : ℕ) (x : LocalSignedRequest.Plane) => CorrectionState.debt c u n x i

All three incoming debts are measured from the same initial fields. There is no assumed debt bound and no change to the moving edge weight.

theorem NavierStokes.CorrectionInitialization.MovingInitialization.LocalAverage.continuous_slice {S : Type} [NormedAddCommGroup S] {V : Set S} {f : PressureStream.Lift S → ℝ} (hf : ContinuousOn f (PhysicalMeanDomain.slowDomain V)) {x : PressureStream.Lift S} (hx : x.2.1 ∈ V) : Continuous fun (Y : PressureStream.Plane) => f (x.1, x.2.1, Y)

theorem NavierStokes.CorrectionInitialization.MovingInitialization.LocalAverage.meanBar_add_on {S : Type} [NormedAddCommGroup S] {V : Set S} (f g : CorrectionState.ScalarField (PressureStream.Lift S)) (hf : ∀ (n : ℕ), ContinuousOn (f n) (PhysicalMeanDomain.slowDomain V)) (hg : ∀ (n : ℕ), ContinuousOn (g n) (PhysicalMeanDomain.slowDomain V)) : MeanIncrementBounds.Agree (PhysicalMeanDomain.slowDomain V) (StateMomentBalances.meanBar (f + g)) (StateMomentBalances.meanBar f + StateMomentBalances.meanBar g)

theorem NavierStokes.CorrectionInitialization.MovingInitialization.LocalAverage.meanBar_sub_on {S : Type} [NormedAddCommGroup S] {V : Set S} (f g : CorrectionState.ScalarField (PressureStream.Lift S)) (hf : ∀ (n : ℕ), ContinuousOn (f n) (PhysicalMeanDomain.slowDomain V)) (hg : ∀ (n : ℕ), ContinuousOn (g n) (PhysicalMeanDomain.slowDomain V)) : MeanIncrementBounds.Agree (PhysicalMeanDomain.slowDomain V) (StateMomentBalances.meanBar (f - g)) (StateMomentBalances.meanBar f - StateMomentBalances.meanBar g)

theorem NavierStokes.CorrectionInitialization.MovingInitialization.LocalAverage.average_derivative_on {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {V : Set S} [FiniteDimensional ℝ S] (hV : IsOpen V) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain V)) (hp : PhysicalMeanDomain.PeriodicOn V f) (v x : PressureStream.Lift S) (hx : x.2.1 ∈ V) : PressureStream.torusAverage (fun (y : PressureStream.Lift S) => (fderiv ℝ f y) v) (x.1, x.2.1) = (fderiv ℝ (MeanMomentBounds.liftedTorusAverage f) x) v

Parameter differentiation of the actual torus average on the open slow domain. The localization equals the original source on a whole fiber germ, so its derivatives introduce no cutoff term.

theorem NavierStokes.CorrectionInitialization.MovingInitialization.LocalAverage.average_linear_on {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {V : Set S} [FiniteDimensional ℝ S] (hV : IsOpen V) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain V)) (hp : PhysicalMeanDomain.PeriodicOn V f) (v w : PressureStream.Lift S) (a b : ℝ × S → ℝ) (x : PressureStream.Lift S) (hx : x.2.1 ∈ V) : PressureStream.torusAverage (fun (y : PressureStream.Lift S) => (fderiv ℝ f y) v + a (y.1, y.2.1) * (fderiv ℝ f y) w + b (y.1, y.2.1) * f y) (x.1, x.2.1) = (fderiv ℝ (MeanMomentBounds.liftedTorusAverage f) x) v + a (x.1, x.2.1) * (fderiv ℝ (MeanMomentBounds.liftedTorusAverage f) x) w + b (x.1, x.2.1) * MeanMomentBounds.liftedTorusAverage f x

theorem NavierStokes.CorrectionInitialization.MovingInitialization.LocalAverage.meanBar_dz_on {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {V : Set S} [FiniteDimensional ℝ S] (hV : IsOpen V) (o : MeanIncrementBounds.Operators (PressureStream.Lift S)) (f : CorrectionState.ScalarField (PressureStream.Lift S)) (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain V)) (hp : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn V (f n)) : MeanIncrementBounds.Agree (PhysicalMeanDomain.slowDomain V) (StateMomentBalances.meanBar (o.dz f)) (o.dz (StateMomentBalances.meanBar f))

theorem NavierStokes.CorrectionInitialization.MovingInitialization.LocalAverage.meanBar_radialDiv_on {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {V : Set S} [FiniteDimensional ℝ S] (hV : IsOpen V) (o : MeanIncrementBounds.Operators (PressureStream.Lift S)) (hradius : o.radius = Prod.fst) (hprofile : ∀ (R : ℝ), ∀ s ∈ V, ∀ (Y : PressureStream.Plane), o.radialProfile (R, s, Y) = o.radialProfile (R, s, 0)) (f : CorrectionState.ScalarField (PressureStream.Lift S)) (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain V)) (hp : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn V (f n)) (c : ℝ) : MeanIncrementBounds.Agree (PhysicalMeanDomain.slowDomain V) (StateMomentBalances.meanBar (o.radialDiv c f)) (o.radialDiv c (StateMomentBalances.meanBar f))

theorem NavierStokes.CorrectionInitialization.MovingInitialization.LocalAverage.continuous_radialDiv_slice {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {V : Set S} (hV : IsOpen V) (o : MeanIncrementBounds.Operators (PressureStream.Lift S)) (hradius : o.radius = Prod.fst) (hprofile : ∀ (R : ℝ), ∀ s ∈ V, ∀ (Y : PressureStream.Plane), o.radialProfile (R, s, Y) = o.radialProfile (R, s, 0)) (f : CorrectionState.ScalarField (PressureStream.Lift S)) (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain V)) (c : ℝ) (n : ℕ) (x : PressureStream.Lift S) (hx : x.2.1 ∈ V) : Continuous fun (Y : PressureStream.Plane) => o.radialDiv c f n (x.1, x.2.1, Y)

theorem NavierStokes.CorrectionInitialization.MovingInitialization.LocalAverage.meanBar_fluxBalance_on {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {V : Set S} [FiniteDimensional ℝ S] (hV : IsOpen V) (o : MeanIncrementBounds.Operators (PressureStream.Lift S)) (hradius : o.radius = Prod.fst) (hprofile : ∀ (R : ℝ), ∀ s ∈ V, ∀ (Y : PressureStream.Plane), o.radialProfile (R, s, Y) = o.radialProfile (R, s, 0)) (R A T : CorrectionState.ScalarField (PressureStream.Lift S)) (c : ℝ) (hR : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (R n) (PhysicalMeanDomain.slowDomain V)) (hA : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (A n) (PhysicalMeanDomain.slowDomain V)) (hT : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (T n) (PhysicalMeanDomain.slowDomain V)) (hpR : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn V (R n)) (hpA : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn V (A n)) (hpT : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn V (T n)) : MeanIncrementBounds.Agree (PhysicalMeanDomain.slowDomain V) (StateMomentBalances.meanBar (o.radialDiv c R + o.dz A - o.radialDiv c T)) (o.radialDiv c (StateMomentBalances.meanBar R - StateMomentBalances.meanBar T) + o.dz (StateMomentBalances.meanBar A))

theorem NavierStokes.CorrectionInitialization.MovingInitialization.matched_flux_mem {coord a b cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (R R₀ T T₀ : CorrectionState.ScalarField LocalSignedRequest.Point) (hR : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (R n) (PhysicalMeanDomain.slowDomain U.carrier)) (hR₀ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (R₀ n) (PhysicalMeanDomain.slowDomain U.carrier)) (hT : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (T n) (PhysicalMeanDomain.slowDomain U.carrier)) (hT₀ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (T₀ n) (PhysicalMeanDomain.slowDomain U.carrier)) (hcurl : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) (3 / 2 - ChartScales.kappa) (R - R₀)) (hvirtual : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) 2 (T - T₀)) (hmatch : MeanIncrementBounds.Agree (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL).domain (StateMomentBalances.meanBar R₀) (StateMomentBalances.meanBar T₀)) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) (3 / 2 - ChartScales.kappa) (StateMomentBalances.meanBar R - StateMomentBalances.meanBar T)

Exact leading covariance cancellation combines with the actual curl covariance error and the higher virtual stress on the moving profile strip.

theorem NavierStokes.CorrectionInitialization.MovingInitialization.fluxBalance_mem {coord a b cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (o : MeanIncrementBounds.Operators LocalSignedRequest.Point) (ho : MeanIncrementBounds.OperatorBounds (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) o ChartScales.kappa) (hradius : o.radius = Prod.fst) (hprofile : ∀ (R : ℝ), ∀ s ∈ U.carrier, ∀ (Y : PressureStream.Plane), o.radialProfile (R, s, Y) = o.radialProfile (R, s, 0)) (R A T : CorrectionState.ScalarField LocalSignedRequest.Point) (c : ℝ) (hR : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (R n) (PhysicalMeanDomain.slowDomain U.carrier)) (hA : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (A n) (PhysicalMeanDomain.slowDomain U.carrier)) (hT : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (T n) (PhysicalMeanDomain.slowDomain U.carrier)) (hpR : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (R n)) (hpA : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (A n)) (hpT : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (T n)) (hflux : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) (3 / 2 - ChartScales.kappa) (StateMomentBalances.meanBar R - StateMomentBalances.meanBar T)) (haxial : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) (1 - ChartScales.kappa) A) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) (149 / 100) (StateMomentBalances.meanBar (o.radialDiv c R + o.dz A - o.radialDiv c T))

theorem NavierStokes.CorrectionInitialization.MovingInitialization.zeroMean_bar_bounds {coord a b cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (c : CorrectionState.Context LocalSignedRequest.Point) (u : CorrectionState.State LocalSignedRequest.Point) (ho : MeanIncrementBounds.OperatorBounds (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) c.operators ChartScales.kappa) (hradius : c.operators.radius = Prod.fst) (hprofile : ∀ (R : ℝ), ∀ s ∈ U.carrier, ∀ (Y : PressureStream.Plane), c.operators.radialProfile (R, s, Y) = c.operators.radialProfile (R, s, 0)) (hm : u.mean = { radial := 0, angular := 0, axial := 0 }) (hW : ∀ (i j : Fin 3), WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) 1 (u.covariance i j)) (hWc : ∀ (i j : Fin 3) (n : ℕ), ContDiffOn ℝ (↑⊤) (u.covariance i j n) (PhysicalMeanDomain.slowDomain U.carrier)) (hWp : ∀ (i j : Fin 3) (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (u.covariance i j n)) (hp : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) (1 - ChartScales.kappa) u.pressure) (hpc : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u.pressure n) (PhysicalMeanDomain.slowDomain U.carrier)) (hpp : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (u.pressure n)) (hθc : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (c.virtualTheta n) (PhysicalMeanDomain.slowDomain U.carrier)) (hθp : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (c.virtualTheta n)) (hzc : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (c.virtualAxial n) (PhysicalMeanDomain.slowDomain U.carrier)) (hzp : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (c.virtualAxial n)) (hθmatch : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) (3 / 2 - ChartScales.kappa) (StateMomentBalances.meanBar (u.covariance 0 1) - StateMomentBalances.meanBar c.virtualTheta)) (hzmatch : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) (3 / 2 - ChartScales.kappa) (StateMomentBalances.meanBar (u.covariance 0 2) - StateMomentBalances.meanBar c.virtualAxial)) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) (149 / 100) (StateMomentBalances.meanBar (u.thetaResidual c)) ∧ WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) (149 / 100) (StateMomentBalances.meanBar (u.axialResidual c))

The actual zero-mean state has both improved bar residuals, once the two leading covariance identities have been applied.

noncomputable def NavierStokes.CorrectionInitialization.NativeResidual.piece {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (pref : Fin 2 → ℕ → ℝ) (s : WeightedClasses.StripData D) (c : CorrectionState.Context D) (χ : ℕ → D × ℝ → PhaseCalculus.Slot) (b : ℕ → PhaseCalculus.Slow → ℝ) (frequency : ℕ → ℝ) (T : ℕ → D × ℝ → SmoothCovariance.Vec2) (mask cutoff : ℕ → D × ℝ → ℝ) (j : Fin 2) : PrimaryPiece (D × ℝ)

Piece, bundling strip, directions, coefficients, cutoff.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.NativeResidual.envelope {D : Type} {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (χ : ℕ → D × ℝ → PhaseCalculus.Slot) (j : Fin 2) : ℕ → D → ℝ

Envelope, defined pointwise by SignedWaveUpdate.phaseEnvelope F (pulseCoordinates (F j) χ) j n (x, 0).

Equations

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

structure NavierStokes.CorrectionInitialization.NativeResidual.Control {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (pref : Fin 2 → ℕ → ℝ) (s : WeightedClasses.StripData D) (c : CorrectionState.Context D) (χ : ℕ → D × ℝ → PhaseCalculus.Slot) (b : ℕ → PhaseCalculus.Slow → ℝ) (frequency : ℕ → ℝ) (T : ℕ → D × ℝ → SmoothCovariance.Vec2) (mask cutoff : ℕ → D × ℝ → ℝ) (j : Fin 2) (kp : ℕ → ℤ) : Type

Native geometric and coefficient data. The principal equation, wave amplitude bounds, homogeneous pressure bounds and nonlinear residual bound are derived below rather than stored in this record.

• operators : MeanIncrementBounds.OperatorBounds s c.operators ChartScales.kappa
• matching : PrimaryResidualClass.Matches s c (PrimaryMaterialDefect.coefficients (F j) b χ 0 0 frequency)
• coordinates : PrimaryMaterialDefect.NativeCoordinates (HarmonicWaveInteraction.productStrip s) (PrimaryResidualClass.directions c) χ
• scale (n : ℕ) : U.scale n = s.slow n
• native_jets : PhaseJetBounds.PolynomialJets (PrimaryPulseBounds.phaseDomain (HarmonicWaveInteraction.productStrip s)) fun (n : ℕ) (x : D × ℝ) => ((χ n x).1, (χ n x).2.2)
• normalized_jets : PhaseJetBounds.PolynomialJets (PrimaryPulseBounds.phaseDomain (HarmonicWaveInteraction.productStrip s)) (PrimaryConstruction.pulseCoordinates (F j) χ)
• chart_smooth (n : ℕ) : ContDiffOn ℝ (↑⊤) (χ n) (HarmonicWaveInteraction.productStrip s).domain
• chart_range (n : ℕ) (x : D × ℝ) : x.1 ∈ s.domain → (χ n x).1 ∈ U.carrier n ∧ (χ n x).2.2 ∈ Set.Ioo 0 ((F j).L n)
• radius_pos (n : ℕ) (x : D × ℝ) : x.1 ∈ s.domain → 0 < (χ n x).1.1
• epsilon (n : ℕ) : (F j).phase.epsilon n = s.epsilon n
• viscosity (n : ℕ) : (F j).viscosity n = s.epsilon n * frequency n ^ 2
• radial_base : WeightedClasses.UnweightedClass (HarmonicWaveInteraction.productStrip s) 1 fun (n : ℕ) (x : D × ℝ) => b n (χ n x).1
• radial_base_smooth (n : ℕ) : ContDiffOn ℝ (↑⊤) (b n) (U.carrier n)
• frequency_bound : WeightedClasses.BandBound s (-(1 / 2)) frequency
• inverse_frequency : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / frequency n
• covariance : SignedWaveUpdate.CovarianceControl (HarmonicWaveInteraction.productStrip s) (SignedWaveUpdate.phaseMatrix F pref (PrimaryConstruction.pulseCoordinates (F j) χ)) T

  Covariance supplied by Control.

• mask_bound : WeightedClasses.UnweightedClass (HarmonicWaveInteraction.productStrip s) 0 mask
• cutoff_bound : WeightedClasses.UnweightedClass (HarmonicWaveInteraction.productStrip s) 0 cutoff
• angle (n : ℕ) (x : D × ℝ) (t : ℝ) : χ n (x + t • (0, 1)) = ((χ n x).1, (χ n x).2.1 + t, (χ n x).2.2)
• target_angle : SignedWaveUpdate.FrozenAlong (0, 1) T
• mask_angle : SignedWaveUpdate.FrozenAlong (0, 1) mask
• cutoff_angle : SignedWaveUpdate.FrozenAlong (0, 1) cutoff
• slow_frozen (n : ℕ) (x : D × ℝ) (t : ℝ) : (χ n (x + t • (PrimaryResidualClass.directions c).fast)).1 = (χ n x).1
• target_frozen : SignedWaveUpdate.FrozenAlong (PrimaryResidualClass.directions c).fast T
• mask_frozen : SignedWaveUpdate.FrozenAlong (PrimaryResidualClass.directions c).fast mask
• clock (n : ℕ) (x : D × ℝ) : x.1 ∈ s.domain → ∀ (t : ℝ), χ n (x + t • (PrimaryResidualClass.directions c).fastField n x) = ((χ n x).1, (χ n x).2.1, (χ n x).2.2 + t)
• angular_frequency (n : ℕ) : frequency n * (F j).phase.p n = ↑(kp n)
• angular_ne (n : ℕ) : kp n ≠ 0
• geometry (n : ℕ) : CurlClassBounds.CylindricalGeometry (HarmonicWaveInteraction.productStrip s).domain (fun (x : D × ℝ) => (χ n x).1.1) ((PrimaryResidualClass.directions c).radialField n) (fun (x : D × ℝ) => (0, 1)) ((PrimaryResidualClass.directions c).axialField (HarmonicWaveInteraction.productStrip s) n)

theorem NavierStokes.CorrectionInitialization.NativeResidual.Control.frequency_ne {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U} {pref : Fin 2 → ℕ → ℝ} {s : WeightedClasses.StripData D} {c : CorrectionState.Context D} {χ : ℕ → D × ℝ → PhaseCalculus.Slot} {b : ℕ → PhaseCalculus.Slow → ℝ} {frequency : ℕ → ℝ} {T : ℕ → D × ℝ → SmoothCovariance.Vec2} {mask cutoff : ℕ → D × ℝ → ℝ} {j : Fin 2} {kp : ℕ → ℤ} (C : Control F pref s c χ b frequency T mask cutoff j kp) (n : ℕ) : frequency n ≠ 0

theorem NavierStokes.CorrectionInitialization.NativeResidual.Control.envelope_eq {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U} {pref : Fin 2 → ℕ → ℝ} {s : WeightedClasses.StripData D} {c : CorrectionState.Context D} {χ : ℕ → D × ℝ → PhaseCalculus.Slot} {b : ℕ → PhaseCalculus.Slow → ℝ} {frequency : ℕ → ℝ} {T : ℕ → D × ℝ → SmoothCovariance.Vec2} {mask cutoff : ℕ → D × ℝ → ℝ} {j : Fin 2} {kp : ℕ → ℤ} (C : Control F pref s c χ b frequency T mask cutoff j kp) : SignedWaveUpdate.phaseEnvelope F (PrimaryConstruction.pulseCoordinates (F j) χ) j = fun (n : ℕ) (p : D × ℝ) => envelope F χ j n p.1

theorem NavierStokes.CorrectionInitialization.NativeResidual.Control.inputBounds {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U} {pref : Fin 2 → ℕ → ℝ} {s : WeightedClasses.StripData D} {c : CorrectionState.Context D} {χ : ℕ → D × ℝ → PhaseCalculus.Slot} {b : ℕ → PhaseCalculus.Slow → ℝ} {frequency : ℕ → ℝ} {T : ℕ → D × ℝ → SmoothCovariance.Vec2} {mask cutoff : ℕ → D × ℝ → ℝ} {j : Fin 2} {kp : ℕ → ℤ} (C : Control F pref s c χ b frequency T mask cutoff j kp) : LinearWaveBounds.InputBounds (HarmonicWaveInteraction.productStrip s) (fun (n : ℕ) (p : D × ℝ) => envelope F χ j n p.1) (1 / 2) ChartScales.kappa (PrimaryResidualClass.directions c) (piece F pref s c χ b frequency T mask cutoff j).coefficients

theorem NavierStokes.CorrectionInitialization.NativeResidual.Control.inputs {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U} {pref : Fin 2 → ℕ → ℝ} {s : WeightedClasses.StripData D} {c : CorrectionState.Context D} {χ : ℕ → D × ℝ → PhaseCalculus.Slot} {b : ℕ → PhaseCalculus.Slow → ℝ} {frequency : ℕ → ℝ} {T : ℕ → D × ℝ → SmoothCovariance.Vec2} {mask cutoff : ℕ → D × ℝ → ℝ} {j : Fin 2} {kp : ℕ → ℤ} (C : Control F pref s c χ b frequency T mask cutoff j kp) : PrimaryResidualClass.Inputs s (envelope F χ j) ChartScales.kappa c (piece F pref s c χ b frequency T mask cutoff j).coefficients cutoff kp

theorem NavierStokes.CorrectionInitialization.NativeResidual.Control.residual_bounds {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U} {pref : Fin 2 → ℕ → ℝ} {s : WeightedClasses.StripData D} {c : CorrectionState.Context D} {χ : ℕ → D × ℝ → PhaseCalculus.Slot} {b : ℕ → PhaseCalculus.Slow → ℝ} {frequency : ℕ → ℝ} {T : ℕ → D × ℝ → SmoothCovariance.Vec2} {mask cutoff : ℕ → D × ℝ → ℝ} {j : Fin 2} {kp : ℕ → ℤ} (C : Control F pref s c χ b frequency T mask cutoff j kp) (u : CorrectionState.State D) (hmean : u.mean = { radial := 0, angular := 0, axial := 0 }) (A : HarmonicResidual.BlockCoefficients D) (hA : ∀ (n : ℕ) (i : Fin 3), HarmonicFields.BandLimited (A n i) 0) : have p := piece F pref s c χ b frequency T mask cutoff j; have Φ := fun (n : ℕ) (x : D) => p.coefficients.phase n (x, 0); CorrectionState.HarmonicBlock.WaveBounds s (envelope F χ j) (7 / 10) (HarmonicResidual.residualBlock c u (p.harmonicBlock Φ kp) (p.excludedBlock Φ kp).velocity A) ∧ (HarmonicResidual.residualBlock c u (p.harmonicBlock Φ kp) (p.excludedBlock Φ kp).velocity A).BandLimited 2

The nonlinear good residual belongs to the actual primary cutoff curl, with its actual Gaussian error and any retained zero-mode alias.

theorem NavierStokes.CorrectionInitialization.AssembledPrimary.conjugatePair_uniform {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type} [Countable ι] [Nonempty ι] {s : WeightedClasses.StripData D} {w : ι → ℕ → D → ℝ} {α : ℝ} {f : ι → ℕ → D → ℂ} (hf : LabelSumBounds.UniformClass s w α f) (j : ℤ) : LabelSumBounds.UniformClass s w α fun (l : ι) (n : ℕ) (x : D) => (ErrorHarmonics.conjugatePair 1 (f l n)).coeff j x

theorem NavierStokes.CorrectionInitialization.AssembledPrimary.block_uniform {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type} [Countable ι] [Nonempty ι] {s : WeightedClasses.StripData D} {P : ι → ℕ → D → ℝ} {α : ℝ} (a : ι → LinearWaveBounds.WaveCoefficients (D × ℝ)) (Φ : ι → ℕ → D → ℝ) (kp : ι → ℕ → ℤ) (ha : LabelSumBounds.UniformWaveClass s P α fun (l : ι) (n : ℕ) (x : D) => (a l).amplitude n (x, 0)) (i : Fin 3) (j : ℤ) : LabelSumBounds.UniformWaveClass s P α fun (l : ι) (n : ℕ) (x : D) => ((PrimaryHarmonics.block (a l) (Φ l) (kp l)).velocity n i).coeff j x

theorem NavierStokes.CorrectionInitialization.AssembledPrimary.covariance_bounds {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type} [Countable ι] [Nonempty ι] {s : WeightedClasses.StripData D} {P : ι → ℕ → D → ℝ} {d h : ℝ} {vr vt : TorusInverse.Plane} (sys : PartitionedCovariance.SlotSystem d h vr vt) (labels : ℕ → Finset ι) (label : ℕ → ι → SlotColoring.Label) (hinj : ∀ (n : ℕ), Set.InjOn (label n) ↑(labels n)) (hlevel : ∀ (n : ℕ), ∀ l ∈ labels n, 1 ≤ (label n l).1) (χ : ℕ → D → LabelSumBounds.WindowPoint) (hχ : ∀ (n : ℕ), ContinuousOn (χ n) s.domain) (Y : ℕ → D → TorusInverse.Plane) (pieces : ι → PrimaryPiece (D × ℝ)) (baseError : CorrectionState.Oscillation D) (Φ : ι → ℕ → D → ℝ) (kp : ι → ℕ → ℤ) (ht : LabelSumBounds.UniformWaveClass s P (1 / 2) fun (l : ι) (n : ℕ) (x : D) => ((pieces l).coefficients.withCutoff (pieces l).cutoff).amplitude n (x, 0)) (hc : LabelSumBounds.UniformWaveClass s P (1 - ChartScales.kappa) fun (l : ι) (n : ℕ) (x : D) => ((pieces l).coefficients.withCutoff (pieces l).cutoff).curlCorrection (pieces l).strip (pieces l).directions n (x, 0)) (hP0 : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P l n x) (hP1 : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, P l n x ≤ 1) (hkp : ∀ (l : ι) (n : ℕ), kp l n ≠ 0) (htAngle : ∀ (l : ι), ErrorHarmonics.AngleIndependent ((pieces l).coefficients.withCutoff (pieces l).cutoff).amplitude) (heAngle : ∀ (l : ι), ErrorHarmonics.AngleIndependent (pieces l).exactCoefficients.amplitude) (hphase : ∀ (l : ι) (n : ℕ) (x : D) (θ : ℝ), (pieces l).coefficients.frequency n * (pieces l).coefficients.phase n (x, θ) = (pieces l).coefficients.frequency n * Φ l n x + ↑(kp l n) * θ) (hsupport : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, ∀ (θ : ℝ), (x, θ) ∈ tsupport (((pieces l).coefficients.withCutoff (pieces l).cutoff).amplitude n) → χ n x ∈ LabelSumBounds.closedWindow d (label n l) ∧ Y n x ∈ SlotGeometry.liftedSupport (SlotColoring.nativeIndex h (label n l).1) (PartitionedCovariance.slotSet h sys.radius vr vt (label n l))) : (∀ (i j : Fin 3), WeightedClasses.MeanClass s 1 ((bandSeed labels pieces baseError).covariance i j)) ∧ ∀ (i j : Fin 3), WeightedClasses.MeanClass s (3 / 2 - ChartScales.kappa) fun (n : ℕ) (x : D) => (bandSeed labels pieces baseError).covariance i j n x - CorrectionState.bilinearCovariance (LabelSumBounds.fieldSum labels fun (l : ι) => (pieces l).tangentVelocity) (LabelSumBounds.fieldSum labels fun (l : ι) => (pieces l).tangentVelocity) i j n x

The actual sum covariance and its tangent-to-curl error. The finite active label set may grow; only the proved slot/window overlap enters the estimate. The support input concerns the explicitly cut amplitude.

theorem NavierStokes.CorrectionInitialization.MovingInitialization.InitialRegularity.periodic_directional {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {V : Set S} (hV : IsOpen V) {f : PressureStream.Lift S → ℝ} (hp : PhysicalMeanDomain.PeriodicOn V f) (v : PressureStream.Lift S) : PhysicalMeanDomain.PeriodicOn V fun (x : PressureStream.Lift S) => (fderiv ℝ f x) v

theorem NavierStokes.CorrectionInitialization.MovingInitialization.InitialRegularity.periodic_radialDiv {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {V : Set S} (hV : IsOpen V) (o : MeanIncrementBounds.Operators (PressureStream.Lift S)) (hR : o.radius = Prod.fst) (hprofile : ∀ (R : ℝ), ∀ s ∈ V, ∀ (Y : PressureStream.Plane), o.radialProfile (R, s, Y) = o.radialProfile (R, s, 0)) {f : CorrectionState.ScalarField (PressureStream.Lift S)} (hp : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn V (f n)) (c : ℝ) (n : ℕ) : PhysicalMeanDomain.PeriodicOn V (o.radialDiv c f n)

theorem NavierStokes.CorrectionInitialization.MovingInitialization.InitialRegularity.periodic_dz {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {V : Set S} (hV : IsOpen V) (o : MeanIncrementBounds.Operators (PressureStream.Lift S)) {f : CorrectionState.ScalarField (PressureStream.Lift S)} (hp : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn V (f n)) (n : ℕ) : PhysicalMeanDomain.PeriodicOn V (o.dz f n)

theorem NavierStokes.CorrectionInitialization.MovingInitialization.InitialRegularity.value_zero_off_gauge {S : Type} {a b : ℝ} {V : Set S} {ell : S → ℝ} {f : PressureStream.Lift S → ℝ} (hf : VariableGaugeMean.SupportedGauge a b ell V f) {x : PressureStream.Lift S} (hx : x.2.1 ∈ V) (hr : x.1 ∉ Set.Icc (ell x.2.1 * a) (ell x.2.1 * b)) : f x = 0

theorem NavierStokes.CorrectionInitialization.MovingInitialization.InitialRegularity.deriv_zero_off_gauge {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} {V : Set S} (hV : IsOpen V) {ell : S → ℝ} (hell : ContinuousOn ell V) {f : PressureStream.Lift S → ℝ} (hf : VariableGaugeMean.SupportedGauge a b ell V f) {x : PressureStream.Lift S} (hx : x.2.1 ∈ V) (hr : x.1 ∉ Set.Icc (ell x.2.1 * a) (ell x.2.1 * b)) (v : PressureStream.Lift S) : (fderiv ℝ f x) v = 0

theorem NavierStokes.CorrectionInitialization.MovingInitialization.zeroMean_gr_periodic {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (c : CorrectionState.Context LocalSignedRequest.Point) (u : CorrectionState.State LocalSignedRequest.Point) (hop : LocalRankDefect.LocalOperators U.carrier c.operators) (hprofile : ∀ (R : ℝ), ∀ s ∈ U.carrier, ∀ (Y : PressureStream.Plane), c.operators.radialProfile (R, s, Y) = c.operators.radialProfile (R, s, 0)) (hm : u.mean = { radial := 0, angular := 0, axial := 0 }) (hWp : ∀ (i j : Fin 3) (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (u.covariance i j n)) (n : ℕ) : PhysicalMeanDomain.PeriodicOn U.carrier (u.gr c n)

theorem NavierStokes.CorrectionInitialization.MovingInitialization.zeroMean_pressure_regular {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData PressureStream.Plane) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (c : CorrectionState.Context LocalSignedRequest.Point) (u : CorrectionState.State LocalSignedRequest.Point) (hop : LocalRankDefect.LocalOperators U.carrier c.operators) (hm : u.mean = { radial := 0, angular := 0, axial := 0 }) (hWc : ∀ (i j : Fin 3) (n : ℕ), ContDiffOn ℝ (↑⊤) (u.covariance i j n) (PhysicalMeanDomain.slowDomain U.carrier)) (hWs : ∀ (i j : Fin 3) (n : ℕ), VariableGaugeMean.SupportedGauge g.radial.inner g.radial.outer (VariableGaugeMean.qLength coord) U.carrier (u.covariance i j n)) : (∀ (n : ℕ), ContDiffOn ℝ (↑⊤) ((VariableGaugeMean.reconstructState g c u).pressure n) (PhysicalMeanDomain.slowDomain U.carrier)) ∧ ∀ (n : ℕ), VariableGaugeMean.SupportedGauge g.radial.inner g.radial.outer (VariableGaugeMean.qLength coord) U.carrier ((VariableGaugeMean.reconstructState g c u).pressure n)

theorem NavierStokes.CorrectionInitialization.MovingInitialization.zeroMean_pressure_periodic {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData PressureStream.Plane) (hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (c : CorrectionState.Context LocalSignedRequest.Point) (u : CorrectionState.State LocalSignedRequest.Point) (hop : LocalRankDefect.LocalOperators U.carrier c.operators) (hprofile : ∀ (R : ℝ), ∀ s ∈ U.carrier, ∀ (Y : PressureStream.Plane), c.operators.radialProfile (R, s, Y) = c.operators.radialProfile (R, s, 0)) (hm : u.mean = { radial := 0, angular := 0, axial := 0 }) (hWp : ∀ (i j : Fin 3) (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (u.covariance i j n)) (n : ℕ) : PhysicalMeanDomain.PeriodicOn U.carrier ((VariableGaugeMean.reconstructState g c u).pressure n)

theorem NavierStokes.CorrectionInitialization.MovingInitialization.zeroMean_raw_smooth {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData PressureStream.Plane) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (c : CorrectionState.Context LocalSignedRequest.Point) (u : CorrectionState.State LocalSignedRequest.Point) (hop : LocalRankDefect.LocalOperators U.carrier c.operators) (hm : u.mean = { radial := 0, angular := 0, axial := 0 }) (hWc : ∀ (i j : Fin 3) (n : ℕ), ContDiffOn ℝ (↑⊤) (u.covariance i j n) (PhysicalMeanDomain.slowDomain U.carrier)) (hWs : ∀ (i j : Fin 3) (n : ℕ), VariableGaugeMean.SupportedGauge g.radial.inner g.radial.outer (VariableGaugeMean.qLength coord) U.carrier (u.covariance i j n)) (hθc : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (c.virtualTheta n) (PhysicalMeanDomain.slowDomain U.carrier)) (hzc : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (c.virtualAxial n) (PhysicalMeanDomain.slowDomain U.carrier)) (hθs : ∀ (n : ℕ), VariableGaugeMean.SupportedGauge g.radial.inner g.radial.outer (VariableGaugeMean.qLength coord) U.carrier (c.virtualTheta n)) (hzs : ∀ (n : ℕ), VariableGaugeMean.SupportedGauge g.radial.inner g.radial.outer (VariableGaugeMean.qLength coord) U.carrier (c.virtualAxial n)) : (∀ (n : ℕ), ContDiffOn ℝ (↑⊤) ((VariableGaugeMean.reconstructState g c u).thetaResidual c n) (PhysicalMeanDomain.slowDomain U.carrier)) ∧ ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) ((VariableGaugeMean.reconstructState g c u).axialResidual c n) (PhysicalMeanDomain.slowDomain U.carrier)

theorem NavierStokes.CorrectionInitialization.MovingInitialization.zeroMean_raw_supported {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData PressureStream.Plane) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (c : CorrectionState.Context LocalSignedRequest.Point) (u : CorrectionState.State LocalSignedRequest.Point) (hop : LocalRankDefect.LocalOperators U.carrier c.operators) (hm : u.mean = { radial := 0, angular := 0, axial := 0 }) (hWc : ∀ (i j : Fin 3) (n : ℕ), ContDiffOn ℝ (↑⊤) (u.covariance i j n) (PhysicalMeanDomain.slowDomain U.carrier)) (hWs : ∀ (i j : Fin 3) (n : ℕ), VariableGaugeMean.SupportedGauge g.radial.inner g.radial.outer (VariableGaugeMean.qLength coord) U.carrier (u.covariance i j n)) (hθs : ∀ (n : ℕ), VariableGaugeMean.SupportedGauge g.radial.inner g.radial.outer (VariableGaugeMean.qLength coord) U.carrier (c.virtualTheta n)) (hzs : ∀ (n : ℕ), VariableGaugeMean.SupportedGauge g.radial.inner g.radial.outer (VariableGaugeMean.qLength coord) U.carrier (c.virtualAxial n)) : (∀ (n : ℕ), VariableGaugeMean.SupportedGauge g.radial.inner g.radial.outer (VariableGaugeMean.qLength coord) U.carrier ((VariableGaugeMean.reconstructState g c u).thetaResidual c n)) ∧ ∀ (n : ℕ), VariableGaugeMean.SupportedGauge g.radial.inner g.radial.outer (VariableGaugeMean.qLength coord) U.carrier ((VariableGaugeMean.reconstructState g c u).axialResidual c n)

theorem NavierStokes.CorrectionInitialization.MovingInitialization.zeroMean_raw_periodic {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData PressureStream.Plane) (hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) (c : CorrectionState.Context LocalSignedRequest.Point) (u : CorrectionState.State LocalSignedRequest.Point) (hop : LocalRankDefect.LocalOperators U.carrier c.operators) (hprofile : ∀ (R : ℝ), ∀ s ∈ U.carrier, ∀ (Y : PressureStream.Plane), c.operators.radialProfile (R, s, Y) = c.operators.radialProfile (R, s, 0)) (hm : u.mean = { radial := 0, angular := 0, axial := 0 }) (hWp : ∀ (i j : Fin 3) (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (u.covariance i j n)) (hθp : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (c.virtualTheta n)) (hzp : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (c.virtualAxial n)) : (∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier ((VariableGaugeMean.reconstructState g c u).thetaResidual c n)) ∧ ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier ((VariableGaugeMean.reconstructState g c u).axialResidual c n)

theorem NavierStokes.CorrectionInitialization.MovingInitialization.zeroMean_temporal_increment_bounds {coord cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData PressureStream.Plane) (ha : 0 < g.radial.inner) (hd : 0 < g.radial.exponent) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord) {h : ℝ} (hh : 0 ≤ h) (hscale : ∀ (n : ℕ), ChartScales.S n ≤ L n) (index : ℕ → ℕ) (D : ℕ) (hgap : ∀ (n : ℕ), ChartScales.nativeIndex h n ≤ index n + D) (axial : PressureStream.Plane × PressureStream.Plane) (c : CorrectionState.Context LocalSignedRequest.Point) (u : CorrectionState.State LocalSignedRequest.Point) (ho : MeanIncrementBounds.OperatorBounds (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) c.operators ChartScales.kappa) (hop : LocalRankDefect.LocalOperators U.carrier c.operators) (hprofile : ∀ (R : ℝ), ∀ s ∈ U.carrier, ∀ (Y : PressureStream.Plane), c.operators.radialProfile (R, s, Y) = c.operators.radialProfile (R, s, 0)) (hm : u.mean = { radial := 0, angular := 0, axial := 0 }) (hW : ∀ (i j : Fin 3), WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) 1 (u.covariance i j)) (hWc : ∀ (i j : Fin 3) (n : ℕ), ContDiffOn ℝ (↑⊤) (u.covariance i j n) (PhysicalMeanDomain.slowDomain U.carrier)) (hWp : ∀ (i j : Fin 3) (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (u.covariance i j n)) (hWs : ∀ (i j : Fin 3) (n : ℕ), VariableGaugeMean.SupportedGauge g.radial.inner g.radial.outer (VariableGaugeMean.qLength coord) U.carrier (u.covariance i j n)) (hθ : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) 1 c.virtualTheta) (hz : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) 1 c.virtualAxial) (hθc : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (c.virtualTheta n) (PhysicalMeanDomain.slowDomain U.carrier)) (hzc : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (c.virtualAxial n) (PhysicalMeanDomain.slowDomain U.carrier)) (hθp : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (c.virtualTheta n)) (hzp : ∀ (n : ℕ), PhysicalMeanDomain.PeriodicOn U.carrier (c.virtualAxial n)) (hθs : ∀ (n : ℕ), VariableGaugeMean.SupportedGauge g.radial.inner g.radial.outer (VariableGaugeMean.qLength coord) U.carrier (c.virtualTheta n)) (hzs : ∀ (n : ℕ), VariableGaugeMean.SupportedGauge g.radial.inner g.radial.outer (VariableGaugeMean.qLength coord) U.carrier (c.virtualAxial n)) : MeanIncrementBounds.IncrementBounds (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) (1 - ChartScales.kappa) (VariableGaugeMean.temporalIncrementState g h index axial c (VariableGaugeMean.reconstructState g c u))

The first temporal increment is bounded by applying the actual moving torus inverse and stream to the residual of the constructed primary state.

theorem NavierStokes.CorrectionInitialization.MovingInitialization.state_debt_mem {coord a b cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (c : CorrectionState.Context LocalSignedRequest.Point) (u : CorrectionState.State LocalSignedRequest.Point) {H : ℝ} (hH : 0 ≤ H) (ho : MeanIncrementBounds.OperatorBounds (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) c.operators ChartScales.kappa) (hb : MeanIncrementBounds.BaseBounds (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) c.base) (hm : MeanIncrementBounds.IncrementBounds (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) H u.mean) (hgr : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) H (u.gr c)) (hop : LocalRankDefect.LocalOperators U.carrier c.operators) (hbc : MeanIncrementBounds.SmoothTriple (LocalRankDefect.positiveDomain U.carrier) c.base) (hmc : MeanIncrementBounds.SmoothTriple (PhysicalMeanDomain.slowDomain U.carrier) u.mean) (hms : CorrectionStep.GaugeSupportedTriple a b (VariableGaugeMean.qLength coord) U.carrier u.mean) (hW : ∀ (i j : Fin 3), WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) H (u.covariance i j)) (hWc : ∀ (i j : Fin 3), MeanIncrementBounds.SmoothOn (PhysicalMeanDomain.slowDomain U.carrier) (u.covariance i j)) (hWs : ∀ (i j : Fin 3), CorrectionStep.GaugeSupported a b (VariableGaugeMean.qLength coord) U.carrier (u.covariance i j)) (i : Fin 3) : WeightedClasses.UnweightedClass (PhysicalMeanDomain.localSlowStripData U.carrier ⋯ ε L hε hεone hL) H fun (n : ℕ) (x : LocalSignedRequest.Plane) => CorrectionState.debt c u n x i

The measured debt after a mean update is controlled by actual source and flux bounds. Its smoothness and support follow from the primitive mean and covariance fields.

theorem NavierStokes.CorrectionInitialization.MovingInitialization.temporal_gr_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData (PressureStream.Lift D)} (g : VariableGaugeMean.GaugeData D) (h : ℝ) (index : ℕ → ℕ) (axial : D × PressureStream.Plane) (c : CorrectionState.Context (PressureStream.Lift D)) (u : CorrectionState.State (PressureStream.Lift D)) {H κ : ℝ} (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hb : MeanIncrementBounds.BaseBounds s c.base) (hm : MeanIncrementBounds.CumulativeBounds s u.mean) (hi : MeanIncrementBounds.IncrementBounds s H (VariableGaugeMean.temporalIncrementState g h index axial c u)) (hH : 9 / 10 ≤ H) (hκ : 2 * κ ≤ 9 / 10) (hW : ∀ (i j : Fin 3), MeanIncrementBounds.SmoothOn s.domain (u.covariance i j)) (hgr : WeightedClasses.MeanClass s H (u.gr c)) : WeightedClasses.MeanClass s H ((VariableGaugeMean.temporalStageState g h index axial c u).gr c)

The literal source of the updated state, including the leading radial term. No source estimate for the output state is an input.

theorem NavierStokes.CorrectionInitialization.MovingInitialization.temporal_rank_increment_bounds {coord A B cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData PressureStream.Plane) (r : CorrectionState.RankData PressureStream.Plane) (ha : 0 < g.radial.inner) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (h : ℝ) (index : ℕ → ℕ) (axial : PressureStream.Plane × PressureStream.Plane) (c : CorrectionState.Context LocalSignedRequest.Point) (u : CorrectionState.State LocalSignedRequest.Point) {H : ℝ} (hH : 9 / 10 ≤ H) (ho : MeanIncrementBounds.OperatorBounds (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) c.operators ChartScales.kappa) (hb : MeanIncrementBounds.BaseBounds (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) c.base) (hm : u.mean = { radial := 0, angular := 0, axial := 0 }) (hi : MeanIncrementBounds.IncrementBounds (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) H (VariableGaugeMean.temporalIncrementState g h index axial c u)) (hgr : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) H (u.gr c)) (hop : LocalRankDefect.LocalOperators U.carrier c.operators) (hbc : MeanIncrementBounds.SmoothTriple (LocalRankDefect.positiveDomain U.carrier) c.base) (hic : MeanIncrementBounds.SmoothTriple (PhysicalMeanDomain.slowDomain U.carrier) (VariableGaugeMean.temporalIncrementState g h index axial c u)) (his : CorrectionStep.GaugeSupportedTriple g.radial.inner g.radial.outer (VariableGaugeMean.qLength coord) U.carrier (VariableGaugeMean.temporalIncrementState g h index axial c u)) (hW : ∀ (i j : Fin 3), WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) H (u.covariance i j)) (hWc : ∀ (i j : Fin 3), MeanIncrementBounds.SmoothOn (PhysicalMeanDomain.slowDomain U.carrier) (u.covariance i j)) (hWs : ∀ (i j : Fin 3), CorrectionStep.GaugeSupported g.radial.inner g.radial.outer (VariableGaugeMean.qLength coord) U.carrier (u.covariance i j)) (hg : LocalRankDefect.RankGeometry g r U.carrier c (VariableGaugeMean.temporalStageState g h index axial c u)) (hparam : RankStateBounds.NormalizedParameters coord A B r U.carrier) (hB : B ≠ 0) (hleft : g.radial.inner < r.inner) (hright : r.outer < g.radial.outer) : MeanIncrementBounds.IncrementBounds (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) H (VariableGaugeMean.rankIncrementState g r axial c (VariableGaugeMean.temporalStageState g h index axial c u))

The first rank correction is obtained from the measured debt of the actual temporal stage. Its velocity bound is derived through the five-row inverse and the moving-support stream estimate.

structure NavierStokes.CorrectionInitialization.MovingInitialization.PrimaryMeanData {coord cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData PressureStream.Plane) (ha : 0 < g.radial.inner) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (c : CorrectionState.Context LocalSignedRequest.Point) (u : CorrectionState.State LocalSignedRequest.Point) : Prop

Data of the base, actual primary covariance, and virtual stress. No bound on the pressure, residual, temporal increment, or rank output is a field.

• exponent_pos : 0 < g.radial.exponent
• gauge_length (n : ℕ) : g.length n = VariableGaugeMean.qLength coord
• operators : MeanIncrementBounds.OperatorBounds (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) c.operators ChartScales.kappa
• base : MeanIncrementBounds.BaseBounds (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) c.base
• localOperators : LocalRankDefect.LocalOperators U.carrier c.operators
• base_smooth : MeanIncrementBounds.SmoothTriple (LocalRankDefect.positiveDomain U.carrier) c.base
• profile (R : ℝ) (s : LocalSignedRequest.Plane) : s ∈ U.carrier → ∀ (Y : PressureStream.Plane), c.operators.radialProfile (R, s, Y) = c.operators.radialProfile (R, s, 0)
• mean_zero : u.mean = { radial := 0, angular := 0, axial := 0 }
• covariance (i j : Fin 3) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) 1 (u.covariance i j)
• covariance_smooth (i j : Fin 3) : MeanIncrementBounds.SmoothOn (PhysicalMeanDomain.slowDomain U.carrier) (u.covariance i j)
• covariance_periodic (i j : Fin 3) (n : ℕ) : PhysicalMeanDomain.PeriodicOn U.carrier (u.covariance i j n)
• covariance_support (i j : Fin 3) : CorrectionStep.GaugeSupported g.radial.inner g.radial.outer (VariableGaugeMean.qLength coord) U.carrier (u.covariance i j)
• theta : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) 1 c.virtualTheta
• axial : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) 1 c.virtualAxial
• theta_smooth : MeanIncrementBounds.SmoothOn (PhysicalMeanDomain.slowDomain U.carrier) c.virtualTheta
• axial_smooth : MeanIncrementBounds.SmoothOn (PhysicalMeanDomain.slowDomain U.carrier) c.virtualAxial
• theta_periodic (n : ℕ) : PhysicalMeanDomain.PeriodicOn U.carrier (c.virtualTheta n)
• axial_periodic (n : ℕ) : PhysicalMeanDomain.PeriodicOn U.carrier (c.virtualAxial n)
• theta_support : CorrectionStep.GaugeSupported g.radial.inner g.radial.outer (VariableGaugeMean.qLength coord) U.carrier c.virtualTheta
• axial_support : CorrectionStep.GaugeSupported g.radial.inner g.radial.outer (VariableGaugeMean.qLength coord) U.carrier c.virtualAxial

structure NavierStokes.CorrectionInitialization.MovingInitialization.TemporalStateBounds {coord cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData PressureStream.Plane) (ha : 0 < g.radial.inner) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (h : ℝ) (index : ℕ → ℕ) (axial : PressureStream.Plane × PressureStream.Plane) (c : CorrectionState.Context LocalSignedRequest.Point) (u : CorrectionState.State LocalSignedRequest.Point) : Prop

All fields are properties of the literal first temporal stage.

• increment : MeanIncrementBounds.IncrementBounds (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) (1 - ChartScales.kappa) (VariableGaugeMean.temporalIncrementState g h index axial c (VariableGaugeMean.reconstructState g c u))
• increment_smooth : MeanIncrementBounds.SmoothTriple (PhysicalMeanDomain.slowDomain U.carrier) (VariableGaugeMean.temporalIncrementState g h index axial c (VariableGaugeMean.reconstructState g c u))
• increment_support : CorrectionStep.GaugeSupportedTriple g.radial.inner g.radial.outer (VariableGaugeMean.qLength coord) U.carrier (VariableGaugeMean.temporalIncrementState g h index axial c (VariableGaugeMean.reconstructState g c u))
• pressure_change : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) (1 - ChartScales.kappa) (CorrectionStep.gaugeTemporalPressureChange g h index axial c (VariableGaugeMean.reconstructState g c u))
• cumulative : CorrectionState.CumulativeBounds (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) (VariableGaugeMean.temporalStageState g h index axial c (VariableGaugeMean.reconstructState g c u))
• theta : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) (149 / 100) ((VariableGaugeMean.temporalStageState g h index axial c (VariableGaugeMean.reconstructState g c u)).thetaResidual c)
• axial : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) (149 / 100) fun (n : ℕ) (x : LocalSignedRequest.Point) => (VariableGaugeMean.temporalStageState g h index axial c (VariableGaugeMean.reconstructState g c u)).axialResidual c n x - VariableGaugeMean.temporalAliasState g h index c (VariableGaugeMean.reconstructState g c u) n (x, 0) 2

theorem NavierStokes.CorrectionInitialization.MovingInitialization.PrimaryMeanData.temporal_bounds {coord cL cR : ℝ} {U : LocalSignedRequest.SlowRegion coord} {g : VariableGaugeMean.GaugeData PressureStream.Plane} {ha : 0 < g.radial.inner} {hcL : 0 < cL} {hcR : 0 < cR} {ε L : ℕ → ℝ} {hε : ∀ (n : ℕ), 0 < ε n} {hεone : ∀ (n : ℕ), ε n ≤ 1} {hL : ∀ (n : ℕ), 1 ≤ L n} {c : CorrectionState.Context LocalSignedRequest.Point} {u : CorrectionState.State LocalSignedRequest.Point} (d : PrimaryMeanData U g ha hcL hcR ε L hε hεone hL c u) {h : ℝ} (hh : 0 ≤ h) (hscale : ∀ (n : ℕ), ChartScales.S n ≤ L n) (index : ℕ → ℕ) (D : ℕ) (hgap : ∀ (n : ℕ), ChartScales.nativeIndex h n ≤ index n + D) (axial : PressureStream.Plane × PressureStream.Plane) (hv : c.operators.vT = (0, 0, TorusInverse.vector TorusInverse.Direction.temporal)) (hfast : ∀ (n : ℕ), c.operators.fastCoefficient n = ChartScales.Tg ^ index n * ChartScales.Q n ^ (1 + h)) (hθmatch : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) (3 / 2 - ChartScales.kappa) (StateMomentBalances.meanBar (u.covariance 0 1) - StateMomentBalances.meanBar c.virtualTheta)) (hzmatch : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) (3 / 2 - ChartScales.kappa) (StateMomentBalances.meanBar (u.covariance 0 2) - StateMomentBalances.meanBar c.virtualAxial)) : TemporalStateBounds U g ha hcL hcR ε L hε hεone hL h index axial c u

structure NavierStokes.CorrectionInitialization.MovingInitialization.InitialRankBounds {coord cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData PressureStream.Plane) (ha : 0 < g.radial.inner) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (r : CorrectionState.RankData PressureStream.Plane) (h : ℝ) (index : ℕ → ℕ) (axial : PressureStream.Plane × PressureStream.Plane) (c : CorrectionState.Context LocalSignedRequest.Point) (u : CorrectionState.State LocalSignedRequest.Point) : Prop

The estimates refer to the actual rank inverse and recomputed pressure. The defect estimate is obtained after the five-row cancellation.

• increment : MeanIncrementBounds.IncrementBounds (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) (1 - ChartScales.kappa) (VariableGaugeMean.rankIncrementState g r axial c (VariableGaugeMean.temporalStageState g h index axial c (VariableGaugeMean.reconstructState g c u)))
• pressure_change : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) (1 - ChartScales.kappa) (CorrectionStep.gaugeRankPressureChange g r axial c (VariableGaugeMean.temporalStageState g h index axial c (VariableGaugeMean.reconstructState g c u)))
• cumulative : CorrectionState.CumulativeBounds (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) (VariableGaugeMean.rankStageState g r axial c (VariableGaugeMean.temporalStageState g h index axial c (VariableGaugeMean.reconstructState g c u)))
• mean_smooth : MeanIncrementBounds.SmoothTriple (PhysicalMeanDomain.slowDomain U.carrier) (VariableGaugeMean.rankStageState g r axial c (VariableGaugeMean.temporalStageState g h index axial c (VariableGaugeMean.reconstructState g c u))).mean
• mean_support : CorrectionStep.GaugeSupportedTriple g.radial.inner g.radial.outer (VariableGaugeMean.qLength coord) U.carrier (VariableGaugeMean.rankStageState g r axial c (VariableGaugeMean.temporalStageState g h index axial c (VariableGaugeMean.reconstructState g c u))).mean
• theta : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) (149 / 100) ((VariableGaugeMean.rankStageState g r axial c (VariableGaugeMean.temporalStageState g h index axial c (VariableGaugeMean.reconstructState g c u))).thetaResidual c)
• axial_residual : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) (149 / 100) fun (n : ℕ) (x : LocalSignedRequest.Point) => (VariableGaugeMean.rankStageState g r axial c (VariableGaugeMean.temporalStageState g h index axial c (VariableGaugeMean.reconstructState g c u))).axialResidual c n x - VariableGaugeMean.temporalAliasState g h index c (VariableGaugeMean.reconstructState g c u) n (x, 0) 2
• defects : CorrectionState.DefectBounds (PhysicalMeanDomain.localSlowStripData U.carrier ⋯ ε L hε hεone hL) (1 / 5) c (VariableGaugeMean.rankStageState g r axial c (VariableGaugeMean.temporalStageState g h index axial c (VariableGaugeMean.reconstructState g c u)))

theorem NavierStokes.CorrectionInitialization.MovingInitialization.PrimaryMeanData.temporal_debt_bounds {coord cL cR : ℝ} {U : LocalSignedRequest.SlowRegion coord} {g : VariableGaugeMean.GaugeData PressureStream.Plane} {ha : 0 < g.radial.inner} {hcL : 0 < cL} {hcR : 0 < cR} {ε L : ℕ → ℝ} {hε : ∀ (n : ℕ), 0 < ε n} {hεone : ∀ (n : ℕ), ε n ≤ 1} {hL : ∀ (n : ℕ), 1 ≤ L n} {c : CorrectionState.Context LocalSignedRequest.Point} {u : CorrectionState.State LocalSignedRequest.Point} (d : PrimaryMeanData U g ha hcL hcR ε L hε hεone hL c u) {h : ℝ} {index : ℕ → ℕ} {axial : PressureStream.Plane × PressureStream.Plane} (t : TemporalStateBounds U g ha hcL hcR ε L hε hεone hL h index axial c u) : WeightedClasses.UnweightedClass (PhysicalMeanDomain.localSlowStripData U.carrier ⋯ ε L hε hεone hL) (1 - ChartScales.kappa) (CorrectionState.debt c (VariableGaugeMean.temporalStageState g h index axial c (VariableGaugeMean.reconstructState g c u)))

theorem NavierStokes.CorrectionInitialization.MovingInitialization.PrimaryMeanData.rank_bounds {coord cL cR : ℝ} {U : LocalSignedRequest.SlowRegion coord} {g : VariableGaugeMean.GaugeData PressureStream.Plane} {ha : 0 < g.radial.inner} {hcL : 0 < cL} {hcR : 0 < cR} {ε L : ℕ → ℝ} {hε : ∀ (n : ℕ), 0 < ε n} {hεone : ∀ (n : ℕ), ε n ≤ 1} {hL : ∀ (n : ℕ), 1 ≤ L n} {c : CorrectionState.Context LocalSignedRequest.Point} {u : CorrectionState.State LocalSignedRequest.Point} (d : PrimaryMeanData U g ha hcL hcR ε L hε hεone hL c u) {h : ℝ} {index : ℕ → ℕ} {axial : PressureStream.Plane × PressureStream.Plane} (t : TemporalStateBounds U g ha hcL hcR ε L hε hεone hL h index axial c u) (r : CorrectionState.RankData PressureStream.Plane) {A B : ℝ} (hg : LocalRankDefect.RankGeometry g r U.carrier c (VariableGaugeMean.temporalStageState g h index axial c (VariableGaugeMean.reconstructState g c u))) (hparam : RankStateBounds.NormalizedParameters coord A B r U.carrier) (hB : B ≠ 0) (hleft : g.radial.inner < r.inner) (hright : r.outer < g.radial.outer) (hfast : c.operators.vT = (0, 0, TorusInverse.vector TorusInverse.Direction.temporal)) (hV : LocalRankDefect.IsSlowOn U.carrier c.base.angular) (hG : LocalRankDefect.IsSlowOn U.carrier c.base.axial) : InitialRankBounds U g ha hcL hcR ε L hε hεone hL r h index axial c u

theorem NavierStokes.CorrectionInitialization.MovingInitialization.PrimaryMeanData.temporal_zeroMasses {coord cL cR : ℝ} {U : LocalSignedRequest.SlowRegion coord} {g : VariableGaugeMean.GaugeData PressureStream.Plane} {ha : 0 < g.radial.inner} {hcL : 0 < cL} {hcR : 0 < cR} {ε L : ℕ → ℝ} {hε : ∀ (n : ℕ), 0 < ε n} {hεone : ∀ (n : ℕ), ε n ≤ 1} {hL : ∀ (n : ℕ), 1 ≤ L n} {c : CorrectionState.Context LocalSignedRequest.Point} {u : CorrectionState.State LocalSignedRequest.Point} (d : PrimaryMeanData U g ha hcL hcR ε L hε hεone hL c u) {h : ℝ} {index : ℕ → ℕ} {axial : PressureStream.Plane × PressureStream.Plane} : GaugeMassPreservation.ZeroMassesOn U.carrier (VariableGaugeMean.temporalStageState g h index axial c (VariableGaugeMean.reconstructState g c u))

theorem NavierStokes.CorrectionInitialization.MovingInitialization.PrimaryMeanData.rank_zeroMasses {coord cL cR : ℝ} {U : LocalSignedRequest.SlowRegion coord} {g : VariableGaugeMean.GaugeData PressureStream.Plane} {ha : 0 < g.radial.inner} {hcL : 0 < cL} {hcR : 0 < cR} {ε L : ℕ → ℝ} {hε : ∀ (n : ℕ), 0 < ε n} {hεone : ∀ (n : ℕ), ε n ≤ 1} {hL : ∀ (n : ℕ), 1 ≤ L n} {c : CorrectionState.Context LocalSignedRequest.Point} {u : CorrectionState.State LocalSignedRequest.Point} (d : PrimaryMeanData U g ha hcL hcR ε L hε hεone hL c u) {h : ℝ} {index : ℕ → ℕ} {axial : PressureStream.Plane × PressureStream.Plane} (t : TemporalStateBounds U g ha hcL hcR ε L hε hεone hL h index axial c u) (r : CorrectionState.RankData PressureStream.Plane) (hg : LocalRankDefect.RankGeometry g r U.carrier c (VariableGaugeMean.temporalStageState g h index axial c (VariableGaugeMean.reconstructState g c u))) : GaugeMassPreservation.ZeroMassesOn U.carrier (VariableGaugeMean.rankStageState g r axial c (VariableGaugeMean.temporalStageState g h index axial c (VariableGaugeMean.reconstructState g c u)))

theorem NavierStokes.CorrectionInitialization.MovingInitialization.initializedBands_mean_defects {coord cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData PressureStream.Plane) (r : CorrectionState.RankData PressureStream.Plane) (ha : 0 < g.radial.inner) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) {ι : Type} (labels : ℕ → Finset ι) (pieces : ι → PrimaryPiece (LocalSignedRequest.Point × ℝ)) (baseError : CorrectionState.Oscillation LocalSignedRequest.Point) (c : CorrectionState.Context LocalSignedRequest.Point) (d : PrimaryMeanData U g ha hcL hcR ε L hε hεone hL c (bandSeed labels pieces baseError)) {h A B : ℝ} (hh : 0 ≤ h) (hscale : ∀ (n : ℕ), ChartScales.S n ≤ L n) (index : ℕ → ℕ) (D : ℕ) (hgap : ∀ (n : ℕ), ChartScales.nativeIndex h n ≤ index n + D) (axial : PressureStream.Plane × PressureStream.Plane) (hv : c.operators.vT = (0, 0, TorusInverse.vector TorusInverse.Direction.temporal)) (hfast : ∀ (n : ℕ), c.operators.fastCoefficient n = ChartScales.Tg ^ index n * ChartScales.Q n ^ (1 + h)) (hθmatch : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) (3 / 2 - ChartScales.kappa) (StateMomentBalances.meanBar ((bandSeed labels pieces baseError).covariance 0 1) - StateMomentBalances.meanBar c.virtualTheta)) (hzmatch : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) (3 / 2 - ChartScales.kappa) (StateMomentBalances.meanBar ((bandSeed labels pieces baseError).covariance 0 2) - StateMomentBalances.meanBar c.virtualAxial)) (hrank : LocalRankDefect.RankGeometry g r U.carrier c (GaugeInitialization.temporalBands g h index axial c labels pieces baseError)) (hparam : RankStateBounds.NormalizedParameters coord A B r U.carrier) (hB : B ≠ 0) (hleft : g.radial.inner < r.inner) (hright : r.outer < g.radial.outer) (hV : LocalRankDefect.IsSlowOn U.carrier c.base.angular) (hG : LocalRankDefect.IsSlowOn U.carrier c.base.axial) (hb : CorrectionStep.AngularContinuous baseError) (hg : ∀ (n : ℕ), ∀ l ∈ labels n, ∀ (x : LocalSignedRequest.Point) (i : Fin 3), Continuous fun (θ : ℝ) => (pieces l).excluded n (x, θ) i) (hz : ∀ (n : ℕ), ∀ l ∈ labels n, ∀ (x : LocalSignedRequest.Point), CorrectionStep.angularMeanVector (pieces l).excluded n x = 0) : CorrectionState.CumulativeBounds (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) (GaugeInitialization.initializedBands g r h index axial c labels pieces baseError) ∧ CorrectionState.MeanResidualBounds (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) (1 / 5) c (GaugeInitialization.initializedBands g r h index axial c labels pieces baseError) ∧ CorrectionState.DefectBounds (PhysicalMeanDomain.localSlowStripData U.carrier ⋯ ε L hε hεone hL) (1 / 5) c (GaugeInitialization.initializedBands g r h index axial c labels pieces baseError) ∧ GaugeMassPreservation.ZeroMassesOn U.carrier (GaugeInitialization.initializedBands g r h index axial c labels pieces baseError)

The actual pressure, temporal, rank, and alias-retention stages meet all mean and defect bounds at sigma=1/5, from primitive primary mean data.

@[irreducible]

noncomputable def NavierStokes.CorrectionInitialization.CommonWindow.levels (n : ℕ) : Finset ℕ

Levels, given by insert n (Finset.Icc (max 1 (n - 2)) (n + 2)).

Equations

• NavierStokes.CorrectionInitialization.CommonWindow.levels n = insert n (Finset.Icc (max 1 (n - 2)) (n + 2))

theorem NavierStokes.CorrectionInitialization.CommonWindow.self_mem (n : ℕ) : n ∈ levels n

theorem NavierStokes.CorrectionInitialization.CommonWindow.levels_nonempty (n : ℕ) : (levels n).Nonempty

theorem NavierStokes.CorrectionInitialization.CommonWindow.distance {n m : ℕ} (hm : m ∈ levels n) : n ≤ m + 4 ∧ m ≤ n + 4

theorem NavierStokes.CorrectionInitialization.CommonWindow.positive {n m : ℕ} (hn : 1 ≤ n) (hm : m ∈ levels n) : 1 ≤ m

noncomputable def NavierStokes.CorrectionInitialization.CommonWindow.index (h : ℝ) (n : ℕ) : ℕ

Index, given by ((levels n).image (ChartScales.nativeIndex h)).min' ((levels_nonempty n).image _).

Equations

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

theorem NavierStokes.CorrectionInitialization.CommonWindow.index_le {h : ℝ} {n m : ℕ} (hm : m ∈ levels n) : index h n ≤ ChartScales.nativeIndex h m

theorem NavierStokes.CorrectionInitialization.CommonWindow.index_le_native (h : ℝ) (n : ℕ) : index h n ≤ ChartScales.nativeIndex h n

noncomputable def NavierStokes.CorrectionInitialization.CommonWindow.gap (h : ℝ) : ℕ

Gap, given by SlotColoring.nativeGap h + ChartScales.nativeIndex h 0.

Equations

• NavierStokes.CorrectionInitialization.CommonWindow.gap h = NavierStokes.SlotColoring.nativeGap h + NavierStokes.ChartScales.nativeIndex h 0

theorem NavierStokes.CorrectionInitialization.CommonWindow.native_le_index_add (h : ℝ) (hh : 0 ≤ h) (n : ℕ) : ChartScales.nativeIndex h n ≤ index h n + gap h

theorem NavierStokes.CorrectionInitialization.CommonWindow.gap_le (h : ℝ) (hh : 0 ≤ h) (n : ℕ) : ChartScales.nativeIndex h n - index h n ≤ gap h

theorem NavierStokes.CorrectionInitialization.CommonWindow.active_level_mem {D q : ℝ} {n : ℕ} {L : SlotColoring.Label} (hq : 0 < q) (hlo : ChartScales.Q n / 2 ≤ q) (hhi : q ≤ 2 * ChartScales.Q n) (hL : 1 ≤ L.1) {x : SlotColoring.Position} (hs : (q, x) ∈ PhysicalWaveSum.labelRegion D L) : L.1 ∈ levels n

The same finite level window contains every actual closed dyadic support meeting the standard chart range. Endpoints are retained.

theorem NavierStokes.CorrectionInitialization.CommonWindow.index_le_active {h D q : ℝ} {n : ℕ} {L : SlotColoring.Label} (hq : 0 < q) (hlo : ChartScales.Q n / 2 ≤ q) (hhi : q ≤ 2 * ChartScales.Q n) (hL : 1 ≤ L.1) {x : SlotColoring.Position} (hs : (q, x) ∈ PhysicalWaveSum.labelRegion D L) : index h n ≤ ChartScales.nativeIndex h L.1

noncomputable def NavierStokes.CorrectionInitialization.CommonWindow.gridRadius (D M : ℝ) (m : ℕ) (j : Fin 3) : ℤ

Grid radius, given by ⌈M / SlotColoring.width D j m + 2⌉.

Equations

• NavierStokes.CorrectionInitialization.CommonWindow.gridRadius D M m j = ⌈M / NavierStokes.SlotColoring.width D j m + 2⌉

noncomputable def NavierStokes.CorrectionInitialization.CommonWindow.grids (D M : ℝ) (m : ℕ) : Finset SlotColoring.Grid

Grids, given by Fintype.piFinset (fun j => Finset.Icc (-gridRadius D M m j) (gridRadius D M m j)).

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.CommonWindow.labels (D M : ℝ) (n : ℕ) : Finset (ℕ × SlotColoring.Grid)

Labels, given by (levels n).biUnion (fun m => (grids D M m).image (fun k => (m, k))).

Equations

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

theorem NavierStokes.CorrectionInitialization.CommonWindow.grid_mem_of_box {D M : ℝ} {m : ℕ} (hm : 1 ≤ m) {k : SlotColoring.Grid} {x : SlotColoring.Position} (hM : ∀ (j : Fin 3), |x j| ≤ M) (hx : x ∈ SlotColoring.physicalBox D (m, k, false)) : k ∈ grids D M m

theorem NavierStokes.CorrectionInitialization.CommonWindow.active_label_mem {D M q : ℝ} {n : ℕ} {l : SlotColoring.Label} (hq : 0 < q) (hlo : ChartScales.Q n / 2 ≤ q) (hhi : q ≤ 2 * ChartScales.Q n) (hl : 1 ≤ l.1) {x : SlotColoring.Position} (hM : ∀ (j : Fin 3), |x j| ≤ M) (hs : (q, x) ∈ PhysicalWaveSum.labelRegion D l) : (l.1, l.2.1) ∈ labels D M n

Every actual label whose closed mask support meets the bounded chart is in the explicit finite family. This is separate from the overlap bound.

theorem NavierStokes.CorrectionInitialization.CommonWindow.indexBounds (h : ℝ) (hh : 0 ≤ h) : CommonBaseContext.IndexBounds h (index h) (gap h)

@[reducible, inline]

noncomputable abbrev NavierStokes.CorrectionInitialization.ActualPrimary.profile : FinalSlowBase.ProfileData

Profile: an abbreviation for FinalSlowBase.actualProfile.

Equations

• NavierStokes.CorrectionInitialization.ActualPrimary.profile = NavierStokes.FinalSlowBase.actualProfile

@[reducible, inline]

noncomputable abbrev NavierStokes.CorrectionInitialization.ActualPrimary.outgoing : OutgoingProfile.Profile

Outgoing: an abbreviation for profile.outgoing.

Equations

• NavierStokes.CorrectionInitialization.ActualPrimary.outgoing = NavierStokes.CorrectionInitialization.ActualPrimary.profile.outgoing

@[reducible, inline]

noncomputable abbrev NavierStokes.CorrectionInitialization.ActualPrimary.nominal : NominalProfile.Witness profile.outgoing

Nominal: an abbreviation for profile.nominal.

Equations

• NavierStokes.CorrectionInitialization.ActualPrimary.nominal = NavierStokes.CorrectionInitialization.ActualPrimary.profile.nominal

@[reducible, inline]

noncomputable abbrev NavierStokes.CorrectionInitialization.ActualPrimary.h : ℝ

H: an abbreviation for outgoing.data.h.

Equations

• NavierStokes.CorrectionInitialization.ActualPrimary.h = NavierStokes.CorrectionInitialization.ActualPrimary.outgoing.data.h

@[reducible, inline]

abbrev NavierStokes.CorrectionInitialization.ActualPrimary.certificate : NominalConeAssembly.Certificate profile.nominal

Certificate: an abbreviation for profile.certificate.

Equations

• NavierStokes.CorrectionInitialization.ActualPrimary.certificate = ⋯

@[reducible, inline]

noncomputable abbrev NavierStokes.CorrectionInitialization.ActualPrimary.modulation : ModulatedProfileAssembly.Witness profile.loop

Modulation: an abbreviation for profile.modulation.

Equations

• NavierStokes.CorrectionInitialization.ActualPrimary.modulation = NavierStokes.CorrectionInitialization.ActualPrimary.profile.modulation

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.radialVector : TorusInverse.Plane

Radial vector, given by TorusInverse.vector .radial.

Equations

• NavierStokes.CorrectionInitialization.ActualPrimary.radialVector = NavierStokes.TorusInverse.vector NavierStokes.TorusInverse.Direction.radial

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.temporalVector : TorusInverse.Plane

Temporal vector, given by TorusInverse.vector .temporal.

Equations

• NavierStokes.CorrectionInitialization.ActualPrimary.temporalVector = NavierStokes.TorusInverse.vector NavierStokes.TorusInverse.Direction.temporal

theorem NavierStokes.CorrectionInitialization.ActualPrimary.vectors_det : radialVector.1 * temporalVector.2 - radialVector.2 * temporalVector.1 ≠ 0

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.slots : PartitionedCovariance.SlotSystem (CoordinateAlgebra.D h) h radialVector temporalVector

Slots, given by PartitionedCovariance.constructedSlotSystem (CoordinateAlgebra.D h) h outgoing.data.h_pos.le radialVector temporalVector.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.upper : ℝ

Upper, given by 2 * NominalConeAssembly.activeRight nominal.

Equations

• NavierStokes.CorrectionInitialization.ActualPrimary.upper = 2 * NavierStokes.NominalConeAssembly.activeRight NavierStokes.CorrectionInitialization.ActualPrimary.nominal

structure NavierStokes.CorrectionInitialization.ActualPrimary.Choice (B N0 : ℕ) : Type

These are selected outputs of the actual same-profile geometry and covariance construction. No matrix or phase estimate is a constructor input.

• prepared : PrimaryGeometryAssembly.Prepared certificate modulation upper B slots.radius N0

  Prepared of Choice, of type PrimaryGeometryAssembly.Prepared certificate modulation upper B slots.radius N0.

• detGap : ℝ

  Det gap of Choice, of type ℝ.

• entryBound : ℝ

  Entry bound of Choice, of type ℝ.

• inverseLower : ℝ

  Inverse lower of Choice, of type ℝ.

• detGap_pos : 0 < self.detGap
• entryBound_ge_one : 1 ≤ self.entryBound
• inverseLower_pos : 0 < self.inverseLower
• covariance (L : PrimaryGeometryAssembly.Index nominal self.prepared.N) (p : PhaseCalculus.Slow) : p ∈ PositiveRepresentatives.positivePart (PrimaryGeometryAssembly.referenceSet nominal) → p ∈ (PrimaryGeometryAssembly.domain nominal self.prepared.N).carrier L → PrimaryCovarianceBounds.ZeroOrderBounds (√(ChartScales.S (BaseChartJets.cellBand L))) self.detGap self.entryBound self.inverseLower (PrimaryTargetBounds.movingWeight nominal p) (PrimaryTargetBounds.preparedCovariance certificate modulation self.prepared radialVector temporalVector L p) fun (j : Fin 2) => (PrimaryTargetBounds.actualTarget modulation p).ofLp j

theorem NavierStokes.CorrectionInitialization.ActualPrimary.choice_nonempty (B N0 : ℕ) : Nonempty (Choice B N0)

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.choice (B N0 : ℕ) : Choice B N0

Choice, given by Classical.choice (choice_nonempty B N0).

Equations

• NavierStokes.CorrectionInitialization.ActualPrimary.choice B N0 = Classical.choice ⋯

@[reducible, inline]

abbrev NavierStokes.CorrectionInitialization.ActualPrimary.Label (B N0 : ℕ) : Type

Label: an abbreviation for PrimaryGeometryAssembly.Index nominal (choice B N0).prepared.N.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.phases (B N0 : ℕ) : Fin 2 → PrimaryPulseBounds.PhaseConstruction (PrimaryGeometryAssembly.domain nominal (choice B N0).prepared.N)

Phases, given by PrimaryGeometryAssembly.construction certificate modulation (choice B N0).prepared slots.radius_pos.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.covariance (B N0 : ℕ) : Label B N0 → PhaseCalculus.Slow → SmoothCovariance.Mat2

Covariance, given by PrimaryTargetBounds.preparedCovariance certificate modulation (choice B N0).prepared radialVector temporalVector.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.prefactor {B N0 : ℕ} (_j : Fin 2) (L : Label B N0) : ℝ

Prefactor, constructed using PartitionedCovariance.nativePrefactor.

Equations

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

theorem NavierStokes.CorrectionInitialization.ActualPrimary.covariance_eq_integral (B N0 : ℕ) : covariance B N0 = PrimaryPulseBounds.primaryCovariance prefactor (fun (j : Fin 2) => (phases B N0 j).frame) (fun (j : Fin 2) => (phases B N0 j).lam) (fun (j : Fin 2) => (phases B N0 j).u) fun (j : Fin 2) => (phases B N0 j).L

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.nativeContext (B : ℕ) : CorrectionState.Context LocalSignedRequest.Point

Native context, given by BaseContextAssembly.nativeContext certificate modulation upper B.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.gauge : VariableGaugeMean.GaugeData TorusInverse.Plane

Gauge, bundling radial, length.

Equations

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

@[simp]

theorem NavierStokes.CorrectionInitialization.ActualPrimary.gauge_length (n : ℕ) : gauge.length n = VariableGaugeMean.qLength (2 * h)

theorem NavierStokes.CorrectionInitialization.ActualPrimary.phase_frequency (B N0 : ℕ) (j : Fin 2) (L : Label B N0) : (phases B N0 j).phase.F L = BaseContextAssembly.frequencySlow certificate modulation upper B (BaseChartJets.cellBand L)

The physical source and every primary phase use exactly the same profile, repaired coefficients, and Borel scale sequence.

theorem NavierStokes.CorrectionInitialization.ActualPrimary.phase_axial (B N0 : ℕ) (j : Fin 2) (L : Label B N0) : (phases B N0 j).phase.G L = BaseContextAssembly.axialSlow certificate modulation upper B (BaseChartJets.cellBand L)

theorem NavierStokes.CorrectionInitialization.ActualPrimary.threshold (B N0 : ℕ) : N0 ≤ (choice B N0).prepared.N

theorem NavierStokes.CorrectionInitialization.ActualPrimary.covariance_bounds (B N0 : ℕ) (L : Label B N0) (p : PhaseCalculus.Slow) (hp : p ∈ PositiveRepresentatives.positivePart (PrimaryGeometryAssembly.referenceSet nominal)) (hL : p ∈ (PrimaryGeometryAssembly.domain nominal (choice B N0).prepared.N).carrier L) : PrimaryCovarianceBounds.ZeroOrderBounds (√(ChartScales.S (BaseChartJets.cellBand L))) (choice B N0).detGap (choice B N0).entryBound (choice B N0).inverseLower (PrimaryTargetBounds.movingWeight nominal p) (covariance B N0 L p) fun (j : Fin 2) => (PrimaryTargetBounds.actualTarget modulation p).ofLp j

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.position {B N0 : ℕ} (L : Label B N0) (p : PhaseCalculus.Slow) : SlotColoring.Position

Position as an element of SlotColoring.Position.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.similarityScale {B N0 : ℕ} (L : Label B N0) (p : PhaseCalculus.Slow) : ℝ

Similarity scale, given by ChartScales.Q (BaseChartJets.cellBand L) * SimilarityCoordinates.coordinateQ (2 * h) (p.2.2, p.2.1).

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.spatialMask {B N0 : ℕ} (L : Label B N0) (p : PhaseCalculus.Slow) : ℝ

Spatial mask, given by PartitionedCovariance.mask (CoordinateAlgebra.D h) (PrimaryGeometryAssembly.label nominal L) (similarityScale L p) (position L p).

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.pulseCoordinates {B N0 : ℕ} (L : Label B N0) (x : PhaseCalculus.Slow × TorusInverse.Plane) : PhaseCalculus.Slow × ℝ

Pulse coordinates, given by (x.1, x.2.2 / (phases B N0 0).L L).

Equations

• NavierStokes.CorrectionInitialization.ActualPrimary.pulseCoordinates L x = (x.1, x.2.2 / (NavierStokes.CorrectionInitialization.ActualPrimary.phases B N0 0).L L)

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.rawVelocity {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (x : PhaseCalculus.Slow × TorusInverse.Plane) : ProblemStatement.Space

Raw velocity, constructed using PartitionedCovariance.amplitude.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.gaussian {B N0 : ℕ} (L : Label B N0) (x : PhaseCalculus.Slow × TorusInverse.Plane) : ℝ

Gaussian, given by GaussianTailFlat.profile (pulseCoordinates L x).2.

Equations

• NavierStokes.CorrectionInitialization.ActualPrimary.gaussian L x = NavierStokes.GaussianTailFlat.profile (NavierStokes.CorrectionInitialization.ActualPrimary.pulseCoordinates L x).2

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.cutVelocity {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (x : PhaseCalculus.Slow × TorusInverse.Plane) : ProblemStatement.Space

Cut velocity, given by gaussian L x • rawVelocity j L x.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.phasePoint {B N0 : ℕ} (_L : Label B N0) (x : PhaseCalculus.Slow × TorusInverse.Plane) : PhaseCalculus.Slow × ℝ

Phase point, given by (x.1, x.2.2).

Equations

• NavierStokes.CorrectionInitialization.ActualPrimary.phasePoint _L x = (x.1, x.2.2)

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.rawPressure {B N0 : ℕ} (j : Fin 2) (L : Label B N0) : PhaseCalculus.Slow × TorusInverse.Plane → ℂ

Raw pressure, constructed using ParticularWaveBounds.projectedPressure.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.cutPressure {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (x : PhaseCalculus.Slow × TorusInverse.Plane) : ℂ

Cut pressure, given by gaussian L x • rawPressure j L x.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.geometry {B N0 : ℕ} (j : Fin 2) (L : Label B N0) : CommonCoverSolve.Geometry

Geometry, bundling gap, basis, center.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.clockWindow {B N0 : ℕ} (L : Label B N0) : PeriodicPhaseAssembly.ClockWindow

Clock window, bundling lower, upper, padding, padding_pos.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.periodicPhase {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (p : PhaseCalculus.Slow) (Y : TorusInverse.Plane) : ℝ

Periodic phase as an element of ℝ.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.commonVelocity {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (p : PhaseCalculus.Slow) (Y : TorusInverse.Plane) : ProblemStatement.Space

Common velocity, given by ∑' k : TorusInverse.Frequency, cutVelocity j L (p, (geometry j L).coordinates k Y).

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.commonPressure {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (p : PhaseCalculus.Slow) (Y : TorusInverse.Plane) : ℂ

Common pressure, given by ∑' k : TorusInverse.Frequency, cutPressure j L (p, (geometry j L).coordinates k Y).

Equations

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

theorem NavierStokes.CorrectionInitialization.ActualPrimary.length_sign {B N0 : ℕ} (j : Fin 2) (L : Label B N0) : (phases B N0 j).L L = (phases B N0 0).L L

Both signs use the identical physical slot length.

theorem NavierStokes.CorrectionInitialization.ActualPrimary.commonVelocity_eq {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (p : PhaseCalculus.Slow) (Y : TorusInverse.Plane) : commonVelocity j L p Y = ∑' (k : TorusInverse.Frequency), gaussian L (p, (geometry j L).coordinates k Y) • rawVelocity j L (p, (geometry j L).coordinates k Y)

The Gaussian cutoff is present exactly once in the common coefficient.

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.sourcePair {B N0 : ℕ} (L : Label B N0) (p : PhaseCalculus.Slow) (hp : p ∈ (PrimaryGeometryAssembly.domain nominal (choice B N0).prepared.N).carrier L) : PrimaryFieldAssembly.SourcePair PhaseCalculus.Slow slots (PrimaryGeometryAssembly.label nominal L)

Source pair, bundling domain, point, point_mem, frame and the required compatibility proofs.

Equations

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

theorem NavierStokes.CorrectionInitialization.ActualPrimary.sourcePair_matrix {B N0 : ℕ} (L : Label B N0) (p : PhaseCalculus.Slow) (hp : p ∈ (PrimaryGeometryAssembly.domain nominal (choice B N0).prepared.N).carrier L) : (sourcePair L p hp).sourceMatrix = covariance B N0 L p

The pair used by the physical partition is the same primary ODE pair whose actual integral matrix was bounded above.

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.unstretchedCoordinates {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (k : TorusInverse.Frequency) (Y : TorusInverse.Plane) : TorusInverse.Plane

Unstretched coordinates as an element of TorusInverse.Plane.

Equations

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

theorem NavierStokes.CorrectionInitialization.ActualPrimary.coordinates_eq {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (k : TorusInverse.Frequency) (Y : TorusInverse.Plane) : (geometry j L).coordinates k Y = ((unstretchedCoordinates j L k Y).1, ((unstretchedCoordinates j L k Y).2 + slots.radius) / ChartScales.timeCoefficient h (BaseChartJets.cellBand L))

theorem NavierStokes.CorrectionInitialization.ActualPrimary.periodicPhase_periodic {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (p : PhaseCalculus.Slow) (Y : TorusInverse.Plane) (k : TorusInverse.Frequency) : periodicPhase j L p (Y + TorusAverages.latticePoint k) = periodicPhase j L p Y

theorem NavierStokes.CorrectionInitialization.ActualPrimary.commonVelocity_periodic {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (p : PhaseCalculus.Slow) (Y : TorusInverse.Plane) (k : TorusInverse.Frequency) : commonVelocity j L p (Y + TorusAverages.latticePoint k) = commonVelocity j L p Y

theorem NavierStokes.CorrectionInitialization.ActualPrimary.commonPressure_periodic {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (p : PhaseCalculus.Slow) (Y : TorusInverse.Plane) (k : TorusInverse.Frequency) : commonPressure j L p (Y + TorusAverages.latticePoint k) = commonPressure j L p Y

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.commonAmplitude {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (p : PhaseCalculus.Slow) (Y : TorusInverse.Plane) : HarmonicCalculus.ComplexVector

Common amplitude, given by ∑' k : TorusInverse.Frequency, CurlClassBounds.complexify (cutVelocity j L (p, (geometry j L).coordinates k Y)).

Equations

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

theorem NavierStokes.CorrectionInitialization.ActualPrimary.cutVelocity_eq_localProfile {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (p : PhaseCalculus.Slow) (z : TorusInverse.Plane) : cutVelocity j L (p, z) = PartitionedCovariance.amplitude (ChartScales.epsilon h (BaseChartJets.cellBand L)) (spatialMask L p) (covariance B N0 L p) (fun (k : Fin 2) => (PrimaryTargetBounds.actualTarget modulation p).ofLp k) j • PrimaryPulseBounds.localPrimaryProfile ((phases B N0 j).frame L) ((phases B N0 j).lam L) ((phases B N0 j).u L) ((phases B N0 j).L L) slots.radius p z

theorem NavierStokes.CorrectionInitialization.ActualPrimary.nativeCoefficient_eq {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (p : PhaseCalculus.Slow) (hp : p ∈ (PrimaryGeometryAssembly.domain nominal (choice B N0).prepared.N).carrier L) (Z : TorusInverse.Plane) : (sourcePair L p hp).nativeCoefficient vectors_det 1 (ChartScales.epsilon h (BaseChartJets.cellBand L)) (fun (k : Fin 2) => (PrimaryTargetBounds.actualTarget modulation p).ofLp k) (similarityScale L p) (position L p) j Z = CurlClassBounds.complexify (cutVelocity j L (p, have z := (TorusAverages.slotChart radialVector temporalVector vectors_det).symm (Z - PartitionedCovariance.slotCenter h (PartitionedCovariance.signedLabel (PrimaryGeometryAssembly.label nominal L) j)); (z.1, (z.2 + slots.radius) / ChartScales.timeCoefficient h (BaseChartJets.cellBand L))))

theorem NavierStokes.CorrectionInitialization.ActualPrimary.commonAmplitude_eq_source {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (p : PhaseCalculus.Slow) (hp : p ∈ (PrimaryGeometryAssembly.domain nominal (choice B N0).prepared.N).carrier L) (Y : TorusInverse.Plane) : commonAmplitude j L p Y = (sourcePair L p hp).actualAmplitude vectors_det 1 (ChartScales.epsilon h (BaseChartJets.cellBand L)) (fun (k : Fin 2) => (PrimaryTargetBounds.actualTarget modulation p).ofLp k) (similarityScale L p) (position L p) j Y

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.commonContext (B : ℕ) : CorrectionState.Context LocalSignedRequest.Point

Common context, given by CommonBaseContext.context certificate modulation upper B (CommonWindow.index h).

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.commonGauge : VariableGaugeMean.GaugeData TorusInverse.Plane

Common gauge, bundling radial, length.

Equations

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

@[simp]

theorem NavierStokes.CorrectionInitialization.ActualPrimary.commonGauge_length (n : ℕ) : commonGauge.length n = VariableGaugeMean.qLength (2 * h)

theorem NavierStokes.CorrectionInitialization.ActualPrimary.position_normalized {B N0 : ℕ} (L : Label B N0) (p : PhaseCalculus.Slow) : PrimaryRepresentatives.normalizedSlow (CoordinateAlgebra.D h) (BaseChartJets.cellBand L) (position L p) = p

theorem NavierStokes.CorrectionInitialization.ActualPrimary.spatialMask_eq {B N0 : ℕ} (L : Label B N0) (p : PhaseCalculus.Slow) : spatialMask L p = SquaredPartition.dyadicProfile (SimilarityCoordinates.coordinateQ (2 * h) (p.2.2, p.2.1)) * PrimaryRepresentatives.nativeMask (BaseChartJets.cellBand L) (PrimaryGeometryAssembly.label nominal L).2 p

theorem NavierStokes.CorrectionInitialization.ActualPrimary.spatialMask_native_support {B N0 : ℕ} (L : Label B N0) (p : PhaseCalculus.Slow) (hm : spatialMask L p ≠ 0) : p ∈ tsupport (PrimaryRepresentatives.nativeMask (BaseChartJets.cellBand L) (PrimaryGeometryAssembly.label nominal L).2)

theorem NavierStokes.CorrectionInitialization.ActualPrimary.spatialMask_q_range {B N0 : ℕ} (L : Label B N0) (p : PhaseCalculus.Slow) (hm : spatialMask L p ≠ 0) : SimilarityCoordinates.coordinateQ (2 * h) (p.2.2, p.2.1) ∈ Set.Ioo (1 / 2) 2

theorem NavierStokes.CorrectionInitialization.ActualPrimary.spatialMask_carrier {B N0 : ℕ} (L : Label B N0) {p : PhaseCalculus.Slow} (hT : 0 < p.2.2) (hm : spatialMask L p ≠ 0) : p ∈ (PrimaryGeometryAssembly.domain nominal (choice B N0).prepared.N).carrier L

theorem NavierStokes.CorrectionInitialization.ActualPrimary.spatialMask_reference {B N0 : ℕ} (L : Label B N0) {p : PhaseCalculus.Slow} (hT : 0 < p.2.2) (hR : 0 ≤ p.1) (hX : (BaseChartJets.normalizedCoordinates h p).2.1 ∈ Set.Icc (NominalConeAssembly.activeLeft nominal) (NominalConeAssembly.activeRight nominal)) (hm : spatialMask L p ≠ 0) : p ∈ PositiveRepresentatives.positivePart (PrimaryGeometryAssembly.referenceSet nominal)

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.rankInner : ℝ

Rank inner, given by ReservedPatches.radialSupportLeft outgoing nominal.controls.radius .mean.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.rankOuter : ℝ

Rank outer, given by ReservedPatches.radialSupportRight outgoing nominal.controls.radius .mean.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.rankAmplitude : ℝ

Rank amplitude, given by ReservedPatches.radialAmplitude outgoing nominal.controls.radius 0.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.rankData : CorrectionState.RankData TorusInverse.Plane

Rank data, given by RankStateBounds.normalizedData (2 * h) (CoordinateAlgebra.A h) rankAmplitude outgoing.data.core.lam rankInner rankOuter.

Equations

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

theorem NavierStokes.CorrectionInitialization.ActualPrimary.rankInner_pos : 0 < rankInner

theorem NavierStokes.CorrectionInitialization.ActualPrimary.rank_radii_ordered : rankInner < rankOuter

theorem NavierStokes.CorrectionInitialization.ActualPrimary.rankAmplitude_pos : 0 < rankAmplitude

theorem NavierStokes.CorrectionInitialization.ActualPrimary.active_left_before_rank : PrimaryTargetBounds.leftRadius nominal < rankInner

theorem NavierStokes.CorrectionInitialization.ActualPrimary.rank_before_active_right : rankOuter < PrimaryTargetBounds.rightRadius nominal

theorem NavierStokes.CorrectionInitialization.ActualPrimary.rankData_parameters (U : Set TorusInverse.Plane) : RankStateBounds.NormalizedParameters (2 * h) (CoordinateAlgebra.A h) rankAmplitude rankData U

theorem NavierStokes.CorrectionInitialization.ActualPrimary.rank_geometry (U : LocalSignedRequest.SlowRegion (2 * h)) (B : ℕ) (u : CorrectionState.State LocalSignedRequest.Point) (hdebt : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (CorrectionState.debt (commonContext B) u n) U.carrier) : LocalRankDefect.RankGeometry commonGauge rankData U.carrier (commonContext B) u

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.nativeChart (B N0 : ℕ) : ActualSignedControl.PreparedChart certificate modulation (choice B N0).prepared ActualSignedGeometry.Native

Native chart, given by ActualSignedGeometry.preparedChart certificate modulation (choice B N0).prepared slots.radius_pos.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.nativeReferenceBounds (B N0 : ℕ) : ActualSignedControl.ReferenceBounds (nativeChart B N0).native (PrimaryGeometryAssembly.domain profile.nominal (choice B N0).prepared.N) (PrimaryGeometryAssembly.construction certificate modulation (choice B N0).prepared ⋯) (PrimaryCopyBounds.preparedPrefactor slots.radius radialVector temporalVector) (nativeChart B N0).coordinate (nativeChart B N0).target (nativeChart B N0).mask (nativeChart B N0).weight

Native reference bounds used in correction initialization.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.nativeBaseVelocity (B N0 : ℕ) (j : Fin 2) : Label B N0 → ActualSignedGeometry.Native → ProblemStatement.Space

Native base velocity, constructed using PrimaryCopyBounds.primaryVelocity.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.nativeEnvelope (B N0 : ℕ) (j : Fin 2) : Label B N0 → ActualSignedGeometry.Native → ℝ

Native envelope, defined pointwise by Real.sqrt ((nativeChart B N0).weight L x) * PrimaryCopyBounds.pulseEnvelope (phases B N0) (nativeChart B N0).coordinate j L x.

Equations

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

theorem NavierStokes.CorrectionInitialization.ActualPrimary.nativeBaseVelocity_jets (B N0 : ℕ) (j : Fin 2) : PrimaryCopyBounds.NativeJets (nativeChart B N0).native (fun (L : PrimaryGeometryAssembly.Index profile.nominal (choice B N0).prepared.N) (x : ActualSignedGeometry.Native) => √(ChartScales.epsilon h (BaseChartJets.cellBand L)) * nativeEnvelope B N0 j L x) (nativeBaseVelocity B N0 j)

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.nativeFactors (B N0 : ℕ) : Label B N0 → ActualSignedGeometry.Native → ℝ

Native factors as an element of Label B N0 → ActualSignedGeometry.Native → ℝ.

Equations

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

theorem NavierStokes.CorrectionInitialization.ActualPrimary.nativeFactors_jets (B N0 : ℕ) : PhaseJetBounds.PolynomialJets (nativeChart B N0).native.toDomain (nativeFactors B N0)

theorem NavierStokes.CorrectionInitialization.ActualPrimary.rawVelocity_eq_native (B N0 : ℕ) (j : Fin 2) (L : Label B N0) (x : ActualSignedGeometry.Native) : rawVelocity j L x = nativeFactors B N0 L x • nativeBaseVelocity B N0 j L x

theorem NavierStokes.CorrectionInitialization.ActualPrimary.rawVelocity_jets (B N0 : ℕ) (j : Fin 2) : PrimaryCopyBounds.NativeJets (nativeChart B N0).native (fun (L : PrimaryGeometryAssembly.Index profile.nominal (choice B N0).prepared.N) (x : ActualSignedGeometry.Native) => √(ChartScales.epsilon h (BaseChartJets.cellBand L)) * nativeEnvelope B N0 j L x) fun (L : PrimaryGeometryAssembly.Index profile.nominal (choice B N0).prepared.N) => rawVelocity j L

theorem NavierStokes.CorrectionInitialization.ActualPrimary.native_phasePoint_eq (B N0 : ℕ) (j : Fin 2) (L : Label B N0) (x : ActualSignedGeometry.Native) : PrimaryCopyBounds.phasePoint (phases B N0 j) (nativeChart B N0).coordinate L x = phasePoint L x

theorem NavierStokes.CorrectionInitialization.ActualPrimary.phasePressure_eq_raw (B N0 : ℕ) (j : Fin 2) (L : Label B N0) (x : ActualSignedGeometry.Native) : PrimaryCopyBounds.phasePressure (phases B N0 j) (nativeChart B N0).coordinate (fun (L : PrimaryGeometryAssembly.Index nominal (choice B N0).prepared.N) => ↑(ChartScales.carrier h (BaseChartJets.cellBand L))) (fun (L : PrimaryGeometryAssembly.Index nominal (choice B N0).prepared.N) => rawVelocity j L) L x = rawPressure j L x

theorem NavierStokes.CorrectionInitialization.ActualPrimary.rawPressure_jets (B N0 : ℕ) (j : Fin 2) : PrimaryCopyBounds.NativeJets (nativeChart B N0).native (fun (L : PrimaryGeometryAssembly.Index profile.nominal (choice B N0).prepared.N) (x : ActualSignedGeometry.Native) => ChartScales.epsilon h (BaseChartJets.cellBand L) * nativeEnvelope B N0 j L x) fun (L : PrimaryGeometryAssembly.Index profile.nominal (choice B N0).prepared.N) => rawPressure j L

theorem NavierStokes.CorrectionInitialization.ActualPrimary.gaussian_jets (B N0 : ℕ) : PhaseJetBounds.PolynomialJets (nativeChart B N0).native.toDomain fun (L : PrimaryGeometryAssembly.Index profile.nominal (choice B N0).prepared.N) => gaussian L

theorem NavierStokes.CorrectionInitialization.ActualPrimary.cutVelocity_jets (B N0 : ℕ) (j : Fin 2) : PrimaryCopyBounds.NativeJets (nativeChart B N0).native (fun (L : PrimaryGeometryAssembly.Index profile.nominal (choice B N0).prepared.N) (x : ActualSignedGeometry.Native) => √(ChartScales.epsilon h (BaseChartJets.cellBand L)) * nativeEnvelope B N0 j L x) fun (L : PrimaryGeometryAssembly.Index profile.nominal (choice B N0).prepared.N) => cutVelocity j L

theorem NavierStokes.CorrectionInitialization.ActualPrimary.cutPressure_jets (B N0 : ℕ) (j : Fin 2) : PrimaryCopyBounds.NativeJets (nativeChart B N0).native (fun (L : PrimaryGeometryAssembly.Index profile.nominal (choice B N0).prepared.N) (x : ActualSignedGeometry.Native) => ChartScales.epsilon h (BaseChartJets.cellBand L) * nativeEnvelope B N0 j L x) fun (L : PrimaryGeometryAssembly.Index profile.nominal (choice B N0).prepared.N) => cutPressure j L

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.tangentMode {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (p : PhaseCalculus.Slow) (Y : TorusInverse.Plane) (theta : ℝ) : Fin 3 → ℝ

Tangent mode as an element of Fin 3 → ℝ.

Equations

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

theorem NavierStokes.CorrectionInitialization.ActualPrimary.tangentMode_eq_source {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (p : PhaseCalculus.Slow) (hp : p ∈ (PrimaryGeometryAssembly.domain nominal (choice B N0).prepared.N).carrier L) (Y : TorusInverse.Plane) (theta : ℝ) : tangentMode j L p Y theta = (sourcePair L p hp).actualVelocity vectors_det 1 (ChartScales.epsilon h (BaseChartJets.cellBand L)) (fun (k : Fin 2) => (PrimaryTargetBounds.actualTarget modulation p).ofLp k) (similarityScale L p) (position L p) j Y theta

theorem NavierStokes.CorrectionInitialization.ActualPrimary.sourcePair_strictCone {B N0 : ℕ} (L : Label B N0) (p : PhaseCalculus.Slow) (hp : p ∈ (PrimaryGeometryAssembly.domain nominal (choice B N0).prepared.N).carrier L) (hK : p ∈ PositiveRepresentatives.positivePart (PrimaryGeometryAssembly.referenceSet nominal)) (hw : 0 < PrimaryTargetBounds.movingWeight nominal p) : SmoothCovariance.StrictCone (sourcePair L p hp).pairData.matrix fun (k : Fin 2) => (PrimaryTargetBounds.actualTarget modulation p).ofLp k

theorem NavierStokes.CorrectionInitialization.ActualPrimary.tangentMode_diagonal_covariance {B N0 : ℕ} (L : Label B N0) (p : PhaseCalculus.Slow) (hp : p ∈ (PrimaryGeometryAssembly.domain nominal (choice B N0).prepared.N).carrier L) (hK : p ∈ PositiveRepresentatives.positivePart (PrimaryGeometryAssembly.referenceSet nominal)) (hw : 0 < PrimaryTargetBounds.movingWeight nominal p) (i : Fin 2) : (∑ j : Fin 2, PartitionedCovariance.doubleAverage fun (Y : PartitionedCovariance.Plane) (theta : ℝ) => tangentMode j L p Y theta 0 * tangentMode j L p Y theta i.succ) = ChartScales.epsilon h (BaseChartJets.cellBand L) * spatialMask L p ^ 2 * (PrimaryTargetBounds.actualTarget modulation p).ofLp i

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.physicalTangentMode {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (p : PhaseCalculus.Slow) (Y : TorusInverse.Plane) (theta : ℝ) : Fin 3 → ℝ

Physical tangent mode, given by ChartScales.Q (BaseChartJets.cellBand L) ^ (-CoordinateAlgebra.A h) • tangentMode j L p Y theta.

Equations

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

theorem NavierStokes.CorrectionInitialization.ActualPrimary.physicalTangentMode_diagonal_covariance {B N0 : ℕ} (L : Label B N0) (p : PhaseCalculus.Slow) (hp : p ∈ (PrimaryGeometryAssembly.domain nominal (choice B N0).prepared.N).carrier L) (hK : p ∈ PositiveRepresentatives.positivePart (PrimaryGeometryAssembly.referenceSet nominal)) (hw : 0 < PrimaryTargetBounds.movingWeight nominal p) (i : Fin 2) : (∑ j : Fin 2, PartitionedCovariance.doubleAverage fun (Y : PartitionedCovariance.Plane) (theta : ℝ) => physicalTangentMode j L p Y theta 0 * physicalTangentMode j L p Y theta i.succ) = (ChartScales.Q (BaseChartJets.cellBand L) ^ (-CoordinateAlgebra.A h)) ^ 2 * ChartScales.epsilon h (BaseChartJets.cellBand L) * spatialMask L p ^ 2 * (PrimaryTargetBounds.actualTarget modulation p).ofLp i

theorem NavierStokes.CorrectionInitialization.ActualPrimary.tangentMode_pair_covariance {B N0 : ℕ} (L : Label B N0) (p : PhaseCalculus.Slow) (hp : p ∈ (PrimaryGeometryAssembly.domain nominal (choice B N0).prepared.N).carrier L) (hK : p ∈ PositiveRepresentatives.positivePart (PrimaryGeometryAssembly.referenceSet nominal)) (hw : 0 < PrimaryTargetBounds.movingWeight nominal p) (i : Fin 2) : (PartitionedCovariance.doubleAverage fun (Y : PartitionedCovariance.Plane) (theta : ℝ) => (∑ j : Fin 2, tangentMode j L p Y theta 0) * ∑ j : Fin 2, tangentMode j L p Y theta i.succ) = ChartScales.epsilon h (BaseChartJets.cellBand L) * spatialMask L p ^ 2 * (PrimaryTargetBounds.actualTarget modulation p).ofLp i

theorem NavierStokes.CorrectionInitialization.ActualPrimary.physical_covariance_factor {B N0 : ℕ} (L : Label B N0) (p : PhaseCalculus.Slow) (hT : 0 < p.2.2) (i : Fin 2) : (ChartScales.Q (BaseChartJets.cellBand L) ^ (-CoordinateAlgebra.A h)) ^ 2 * ChartScales.epsilon h (BaseChartJets.cellBand L) * (PrimaryTargetBounds.actualTarget modulation p).ofLp i = similarityScale L p ^ (-CoordinateAlgebra.A h - 1 / 2) * (ProfileSpectralCone.stressVector modulation.profiles h (BaseChartJets.normalizedCoordinates h p).2).ofLp i

@[reducible, inline]

abbrev NavierStokes.CorrectionInitialization.ActualPrimary.AbsolutePoint : Type

Absolute point: an abbreviation for PhaseCalculus.Slow × TorusInverse.Plane.

Equations

• NavierStokes.CorrectionInitialization.ActualPrimary.AbsolutePoint = (NavierStokes.PhaseCalculus.Slow × NavierStokes.TorusInverse.Plane)

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.toAbsolute (n : ℕ) (x : LocalSignedRequest.Point) : AbsolutePoint

To absolute as an element of AbsolutePoint.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.fromAbsolute (n : ℕ) (x : AbsolutePoint) : LocalSignedRequest.Point

From absolute as an element of LocalSignedRequest.Point.

Equations

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

theorem NavierStokes.CorrectionInitialization.ActualPrimary.toAbsolute_fromAbsolute (n : ℕ) (x : AbsolutePoint) : toAbsolute n (fromAbsolute n x) = x

theorem NavierStokes.CorrectionInitialization.ActualPrimary.fromAbsolute_toAbsolute (n : ℕ) (x : LocalSignedRequest.Point) : fromAbsolute n (toAbsolute n x) = x

theorem NavierStokes.CorrectionInitialization.ActualPrimary.toAbsolute_smooth (n : ℕ) : ContDiff ℝ (↑⊤) (toAbsolute n)

theorem NavierStokes.CorrectionInitialization.ActualPrimary.fromAbsolute_smooth (n : ℕ) : ContDiff ℝ (↑⊤) (fromAbsolute n)

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.chartGeometry {B N0 : ℕ} (n : ℕ) (j : Fin 2) (L : Label B N0) : CommonCoverSolve.Geometry

Chart geometry, given by { geometry j L with gap := ChartScales.nativeIndex h (BaseChartJets.cellBand L) - CommonWindow.index h n }.

Equations

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

theorem NavierStokes.CorrectionInitialization.ActualPrimary.chartGeometry_coordinates {B N0 : ℕ} (n : ℕ) (j : Fin 2) (L : Label B N0) (hi : CommonWindow.index h n ≤ ChartScales.nativeIndex h (BaseChartJets.cellBand L)) (k : TorusInverse.Frequency) (Y : TorusInverse.Plane) : (geometry j L).coordinates k ((CommonCoverSolve.coverPower (CommonWindow.index h n)).symm Y) = (chartGeometry n j L).coordinates k Y

theorem NavierStokes.CorrectionInitialization.ActualPrimary.chartGeometry_coordinates_active {B N0 : ℕ} (n : ℕ) (j : Fin 2) (L : Label B N0) (hL : BaseChartJets.cellBand L ∈ CommonWindow.levels n) (k : TorusInverse.Frequency) (Y : TorusInverse.Plane) : (geometry j L).coordinates k ((CommonCoverSolve.coverPower (CommonWindow.index h n)).symm Y) = (chartGeometry n j L).coordinates k Y

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.outerRawVelocity {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (x : ActualSignedGeometry.Native) : ProblemStatement.Space

Outer raw velocity, given by PrimaryCopyBounds.outerCutoff (pulseCoordinates L x).2 • rawVelocity j L x.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.attachedRawVelocity {B N0 : ℕ} (j : Fin 2) (L : Label B N0) : ActualSignedGeometry.Native → ProblemStatement.Space

Attached raw velocity, given by WaveEdgeExtension.nativeExtension nominal (outerRawVelocity j L).

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.uncutAmplitude {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (p : PhaseCalculus.Slow) (Y : TorusInverse.Plane) : HarmonicCalculus.ComplexVector

Uncut amplitude, given by ∑' k : TorusInverse.Frequency, CurlClassBounds.complexify (attachedRawVelocity j L (p, (geometry j L).coordinates k Y)).

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.periodicGaussian {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (Y : TorusInverse.Plane) : ℝ

Periodic gaussian, given by GaussianTailFlat.profile (PeriodicPhaseAssembly.periodicClock (geometry j L) (clockWindow L).cutoff Y / (phases B N0 0).L L).

Equations

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

theorem NavierStokes.CorrectionInitialization.ActualPrimary.periodicGaussian_smooth {B N0 : ℕ} (j : Fin 2) (L : Label B N0) : ContDiff ℝ (↑⊤) (periodicGaussian j L)

theorem NavierStokes.CorrectionInitialization.ActualPrimary.periodicGaussian_periodic {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (Y : TorusInverse.Plane) (k : TorusInverse.Frequency) : periodicGaussian j L (Y + TorusAverages.latticePoint k) = periodicGaussian j L Y

theorem NavierStokes.CorrectionInitialization.ActualPrimary.uncutAmplitude_periodic {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (p : PhaseCalculus.Slow) (Y : TorusInverse.Plane) (k : TorusInverse.Frequency) : uncutAmplitude j L p (Y + TorusAverages.latticePoint k) = uncutAmplitude j L p Y

theorem NavierStokes.CorrectionInitialization.ActualPrimary.clockWindow_injective {B N0 : ℕ} (j : Fin 2) (L : Label B N0) : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => (geometry j L).center + (geometry j L).basis z) '' (clockWindow L).outer)

theorem NavierStokes.CorrectionInitialization.ActualPrimary.rawVelocity_transverse {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (x : ActualSignedGeometry.Native) (hx : rawVelocity j L x ≠ 0) : x.2.1 ∈ Set.Ioo (-slots.radius) slots.radius

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

theorem NavierStokes.CorrectionInitialization.ActualPrimary.cutVelocity_eq_outer {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (x : ActualSignedGeometry.Native) : cutVelocity j L x = gaussian L x • outerRawVelocity j L x

theorem NavierStokes.CorrectionInitialization.ActualPrimary.periodicGaussian_eq_on_core {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (p : PhaseCalculus.Slow) (Y : TorusInverse.Plane) (k : TorusInverse.Frequency) (hcore : (geometry j L).coordinates k Y ∈ (clockWindow L).core) : periodicGaussian j L Y = gaussian L (p, (geometry j L).coordinates k Y)

theorem NavierStokes.CorrectionInitialization.ActualPrimary.periodicGaussian_outerRaw {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (p : PhaseCalculus.Slow) (Y : TorusInverse.Plane) (k : TorusInverse.Frequency) : periodicGaussian j L Y • outerRawVelocity j L (p, (geometry j L).coordinates k Y) = cutVelocity j L (p, (geometry j L).coordinates k Y)

theorem NavierStokes.CorrectionInitialization.ActualPrimary.periodic_cutoff_amplitude {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (p : PhaseCalculus.Slow) (hp : PrimaryTargetBounds.profileRadius h p ∈ Set.Ioo (PrimaryTargetBounds.leftRadius nominal) (PrimaryTargetBounds.rightRadius nominal)) (Y : TorusInverse.Plane) : periodicGaussian j L Y • uncutAmplitude j L p Y = commonAmplitude j L p Y

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.outerRawPressure {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (x : ActualSignedGeometry.Native) : ℂ

Outer raw pressure, given by PrimaryCopyBounds.outerCutoff (pulseCoordinates L x).2 • rawPressure j L x.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.attachedRawPressure {B N0 : ℕ} (j : Fin 2) (L : Label B N0) : ActualSignedGeometry.Native → ℂ

Attached raw pressure, given by WaveEdgeExtension.nativeExtension nominal (outerRawPressure j L).

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.uncutPressure {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (p : PhaseCalculus.Slow) (Y : TorusInverse.Plane) : ℂ

Uncut pressure, given by ∑' k : TorusInverse.Frequency, attachedRawPressure j L (p, (geometry j L).coordinates k Y).

Equations

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

theorem NavierStokes.CorrectionInitialization.ActualPrimary.rawPressure_zero_of_velocity_zero {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (x : ActualSignedGeometry.Native) (hz : rawVelocity j L x = 0) : rawPressure j L x = 0

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

theorem NavierStokes.CorrectionInitialization.ActualPrimary.cutPressure_eq_outer {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (x : ActualSignedGeometry.Native) : cutPressure j L x = gaussian L x • outerRawPressure j L x

theorem NavierStokes.CorrectionInitialization.ActualPrimary.periodicGaussian_outerPressure {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (p : PhaseCalculus.Slow) (Y : TorusInverse.Plane) (k : TorusInverse.Frequency) : periodicGaussian j L Y • outerRawPressure j L (p, (geometry j L).coordinates k Y) = cutPressure j L (p, (geometry j L).coordinates k Y)

theorem NavierStokes.CorrectionInitialization.ActualPrimary.periodic_cutoff_pressure {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (p : PhaseCalculus.Slow) (hp : PrimaryTargetBounds.profileRadius h p ∈ Set.Ioo (PrimaryTargetBounds.leftRadius nominal) (PrimaryTargetBounds.rightRadius nominal)) (Y : TorusInverse.Plane) : periodicGaussian j L Y • uncutPressure j L p Y = commonPressure j L p Y

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.closedMargins (B N0 : ℕ) : NativeBandExtension.ClosedMargins certificate modulation (choice B N0).prepared radialVector temporalVector

Closed margins, bundling gap, entry, lower, gap_pos and the required compatibility proofs.

Equations

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

theorem NavierStokes.CorrectionInitialization.ActualPrimary.preOuterVelocity_eq {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (x : ActualSignedGeometry.Native) : NativeBandExtension.preOuterVelocity certificate modulation (choice B N0).prepared ⋯ radialVector temporalVector j L x = rawVelocity j L x

theorem NavierStokes.CorrectionInitialization.ActualPrimary.preOuterPressure_eq {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (x : ActualSignedGeometry.Native) : NativeBandExtension.preOuterPressure certificate modulation (choice B N0).prepared ⋯ radialVector temporalVector j L x = rawPressure j L x

theorem NavierStokes.CorrectionInitialization.ActualPrimary.bandVelocity_eq {B N0 : ℕ} (j : Fin 2) (L : Label B N0) : NativeBandExtension.bandVelocity certificate modulation (choice B N0).prepared ⋯ radialVector temporalVector j L = outerRawVelocity j L

theorem NavierStokes.CorrectionInitialization.ActualPrimary.bandPressure_eq {B N0 : ℕ} (j : Fin 2) (L : Label B N0) : NativeBandExtension.bandPressure certificate modulation (choice B N0).prepared ⋯ radialVector temporalVector j L = outerRawPressure j L

theorem NavierStokes.CorrectionInitialization.ActualPrimary.preOuterVelocity_jets (B N0 : ℕ) (j : Fin 2) : PrimaryCopyBounds.NativeJets (ActualSignedGeometry.nativeDomain certificate modulation (choice B N0).prepared) (NativeBandExtension.velocityWeight certificate modulation (choice B N0).prepared ⋯ j) (NativeBandExtension.preOuterVelocity certificate modulation (choice B N0).prepared ⋯ radialVector temporalVector j)

theorem NavierStokes.CorrectionInitialization.ActualPrimary.preOuterPressure_jets (B N0 : ℕ) (j : Fin 2) : PrimaryCopyBounds.NativeJets (ActualSignedGeometry.nativeDomain certificate modulation (choice B N0).prepared) (NativeBandExtension.pressureWeight certificate modulation (choice B N0).prepared ⋯ j) (NativeBandExtension.preOuterPressure certificate modulation (choice B N0).prepared ⋯ radialVector temporalVector j)

theorem NavierStokes.CorrectionInitialization.ActualPrimary.attachedPair_regular (B N0 : ℕ) (j : Fin 2) (L : Label B N0) : WaveEdgeExtension.NativeRegularity nominal (outerRawVelocity j L) ∧ WaveEdgeExtension.NativeRegularity nominal (outerRawPressure j L)

theorem NavierStokes.CorrectionInitialization.ActualPrimary.attachedRawVelocity_smooth (B N0 : ℕ) (j : Fin 2) (L : Label B N0) : ContDiffOn ℝ (↑⊤) (attachedRawVelocity j L) WaveEdgeExtension.nativeSlowDomain

theorem NavierStokes.CorrectionInitialization.ActualPrimary.attachedRawPressure_smooth (B N0 : ℕ) (j : Fin 2) (L : Label B N0) : ContDiffOn ℝ (↑⊤) (attachedRawPressure j L) WaveEdgeExtension.nativeSlowDomain

theorem NavierStokes.CorrectionInitialization.ActualPrimary.attachedPair_band_edge_jets {B N0 : ℕ} (j : Fin 2) (L : Label B N0) {x : ActualSignedGeometry.Native} (hT : 0 < x.1.2.2) (he : SimilarityCoordinates.coordinateQ (2 * h) (x.1.2.2, x.1.2.1) = 1 / 2 ∨ SimilarityCoordinates.coordinateQ (2 * h) (x.1.2.2, x.1.2.1) = 2) (n : ℕ) : iteratedFDeriv ℝ n (attachedRawVelocity j L) x = 0 ∧ iteratedFDeriv ℝ n (attachedRawPressure j L) x = 0

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

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.copyCells {B N0 : ℕ} (j : Fin 2) (L : Label B N0) : PeriodizedWaveBounds.Cells ActualSignedGeometry.Native TorusInverse.Frequency

Copy cells, constructed using PeriodizedWaveBounds.nativeCells.

Equations

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

theorem NavierStokes.CorrectionInitialization.ActualPrimary.nativeCopySum_smooth {B N0 : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (j : Fin 2) (L : Label B N0) (f : ActualSignedGeometry.Native → E) (hf : ContDiffOn ℝ (↑⊤) f WaveEdgeExtension.nativeSlowDomain) (hs : ∀ (x : ActualSignedGeometry.Native), f x ≠ 0 → x.2 ∈ (clockWindow L).core) : ContDiffOn ℝ (↑⊤) (fun (x : ActualSignedGeometry.Native) => ∑' (k : TorusInverse.Frequency), f (x.1, (geometry j L).coordinates k x.2)) WaveEdgeExtension.nativeSlowDomain

theorem NavierStokes.CorrectionInitialization.ActualPrimary.uncutAmplitude_smooth {B N0 : ℕ} (j : Fin 2) (L : Label B N0) : ContDiffOn ℝ (↑⊤) (fun (x : ActualSignedGeometry.Native) => uncutAmplitude j L x.1 x.2) WaveEdgeExtension.nativeSlowDomain

theorem NavierStokes.CorrectionInitialization.ActualPrimary.uncutPressure_smooth {B N0 : ℕ} (j : Fin 2) (L : Label B N0) : ContDiffOn ℝ (↑⊤) (fun (x : ActualSignedGeometry.Native) => uncutPressure j L x.1 x.2) WaveEdgeExtension.nativeSlowDomain

theorem NavierStokes.CorrectionInitialization.ActualPrimary.uncutPressure_periodic {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (p : PhaseCalculus.Slow) (Y : TorusInverse.Plane) (k : TorusInverse.Frequency) : uncutPressure j L p (Y + TorusAverages.latticePoint k) = uncutPressure j L p Y

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.standardRegion : LocalSignedRequest.SlowRegion (2 * h)

Standard region, given by ActualSignedGeometry.standardSlowRegion outgoing.data.h_pos outgoing.data.h_lt_half.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.physicalPosition (n : ℕ) (x : LocalSignedRequest.Point) : SlotColoring.Position

Physical position, given by ![Real.sqrt (ChartScales.Q n) * x.1, ChartScales.Q n ^ CoordinateAlgebra.D h * x.2.1.2, ChartScales.Q n * x.2.1.1].

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.physicalScale (n : ℕ) (x : LocalSignedRequest.Point) : ℝ

Physical scale, given by ChartScales.Q n * SimilarityCoordinates.coordinateQ (2 * h) x.2.1.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.activeLabels (U : LocalSignedRequest.SlowRegion (2 * h)) (B N0 n : ℕ) : Finset (Label B N0 × Fin 2)

Active labels as an element of Finset (Label B N0 × Fin 2).

Equations

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

theorem NavierStokes.CorrectionInitialization.ActualPrimary.mem_activeLabels {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * h)) (n : ℕ) (L : Label B N0) (j : Fin 2) : (L, j) ∈ activeLabels U B N0 n ↔ PrimaryGeometryAssembly.label nominal L ∈ CommonWindow.labels (CoordinateAlgebra.D h) (BaseContextAssembly.geometryBound nominal U) n

theorem NavierStokes.CorrectionInitialization.ActualPrimary.physicalPosition_bound (U : LocalSignedRequest.SlowRegion (2 * h)) (n : ℕ) {x : LocalSignedRequest.Point} (hx : x ∈ (BaseContextAssembly.nativeStrip nominal U).domain) (j : Fin 3) : |physicalPosition n x j| ≤ BaseContextAssembly.geometryBound nominal U

theorem NavierStokes.CorrectionInitialization.ActualPrimary.activeLabels_cover {B N0 : ℕ} (n : ℕ) {x : LocalSignedRequest.Point} (hx : x ∈ (BaseContextAssembly.nativeStrip nominal standardRegion).domain) (L : Label B N0) (j : Fin 2) (hm : (physicalScale n x, physicalPosition n x) ∈ PhysicalWaveSum.labelRegion (CoordinateAlgebra.D h) (PartitionedCovariance.signedLabel (PrimaryGeometryAssembly.label nominal L) j)) : (L, j) ∈ activeLabels standardRegion B N0 n

@[reducible, inline]

abbrev NavierStokes.CorrectionInitialization.ActualPrimary.FullPoint : Type

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

Equations

• NavierStokes.CorrectionInitialization.ActualPrimary.FullPoint = (NavierStokes.LocalSignedRequest.Point × ℝ)

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.nativeSlow {B N0 : ℕ} (L : Label B N0) (x : AbsolutePoint) : PhaseCalculus.Slow

Native slow as an element of PhaseCalculus.Slow.

Equations

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

theorem NavierStokes.CorrectionInitialization.ActualPrimary.nativeSlow_smooth {B N0 : ℕ} (L : Label B N0) : ContDiff ℝ (↑⊤) (nativeSlow L)

theorem NavierStokes.CorrectionInitialization.ActualPrimary.nativeSlow_toAbsolute {B N0 : ℕ} (L : Label B N0) (x : LocalSignedRequest.Point) : nativeSlow L (toAbsolute (BaseChartJets.cellBand L) x) = BaseContextAssembly.slowCoordinates x

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

Absolute amplitude, given by ChartScales.Q (BaseChartJets.cellBand L) ^ (-CoordinateAlgebra.A h) • uncutAmplitude j L (nativeSlow L x) x.2.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.absolutePressure {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (x : AbsolutePoint) : ℂ

Absolute pressure, given by ChartScales.Q (BaseChartJets.cellBand L) ^ (-(2 * CoordinateAlgebra.A h)) • uncutPressure j L (nativeSlow L x) x.2.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.absolutePhase {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (x : AbsolutePoint × ℝ) : ℝ

Absolute phase as an element of ℝ.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.chartCoefficients {B N0 : ℕ} (j : Fin 2) (L : Label B N0) : LinearWaveBounds.WaveCoefficients FullPoint

Chart coefficients, bundling radius, radialBase, frequencyBase, axialBase and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.chartCutoff {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (n : ℕ) (x : FullPoint) : ℝ

Chart cutoff, given by periodicGaussian j L (toAbsolute n x.1).2.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.piece {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * h)) (j : Fin 2) (L : Label B N0) : PrimaryPiece FullPoint

Piece, bundling strip, directions, coefficients, cutoff.

Equations

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

theorem NavierStokes.CorrectionInitialization.ActualPrimary.chartCoefficients_frequency_pos {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (n : ℕ) : 0 < (chartCoefficients j L).frequency n

theorem NavierStokes.CorrectionInitialization.ActualPrimary.chartCoefficients_phase {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (n : ℕ) (x : FullPoint) : (chartCoefficients j L).frequency n * (chartCoefficients j L).phase n x = absolutePhase j L (toAbsolute n x.1, x.2)

theorem NavierStokes.CorrectionInitialization.ActualPrimary.chartCoefficients_matches {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * h)) (j : Fin 2) (L : Label B N0) : PrimaryResidualClass.Matches (BaseContextAssembly.nativeStrip nominal U) (commonContext B) (chartCoefficients j L)

theorem NavierStokes.CorrectionInitialization.ActualPrimary.chartCoefficients_angular {B N0 : ℕ} (j : Fin 2) (L : Label B N0) : PrimaryResidualClass.AngularData (chartCoefficients j L) (chartCutoff j L)

theorem NavierStokes.CorrectionInitialization.ActualPrimary.chartCoefficients_carrier {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (n : ℕ) (x : FullPoint) : HarmonicCalculus.carrier ((chartCoefficients j L).frequency n) ((chartCoefficients j L).phase n) x = HarmonicCalculus.carrier 1 (absolutePhase j L) (toAbsolute n x.1, x.2)

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.absoluteTangent {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (x : AbsolutePoint × ℝ) : Fin 3 → ℝ

Absolute tangent, defined pointwise by (HarmonicCalculus.vectorMode 1 (absolutePhase j L) (fun z => periodicGaussian j L z.1.2 • absoluteAmplitude j L z.1) x i).re.

Equations

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

noncomputable def NavierStokes.CorrectionInitialization.ActualPrimary.absolutePressureMode {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (x : AbsolutePoint × ℝ) : ℝ

Absolute pressure mode, given by (HarmonicCalculus.mode 1 (absolutePhase j L) (fun z => periodicGaussian j L z.1.2 • absolutePressure j L z.1) x).re.

Equations

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

theorem NavierStokes.CorrectionInitialization.ActualPrimary.piece_tangent_representation {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * h)) (j : Fin 2) (L : Label B N0) (n : ℕ) (x : FullPoint) : (piece U j L).tangentVelocity n x = ChartScales.Q n ^ CoordinateAlgebra.A h • absoluteTangent j L (toAbsolute n x.1, x.2)

theorem NavierStokes.CorrectionInitialization.ActualPrimary.piece_pressure_representation {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * h)) (j : Fin 2) (L : Label B N0) (n : ℕ) (x : FullPoint) : (piece U j L).pressure n x = ChartScales.Q n ^ (2 * CoordinateAlgebra.A h) * absolutePressureMode j L (toAbsolute n x.1, x.2)

theorem NavierStokes.CorrectionInitialization.ActualPrimary.absoluteTangent_eq {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (x : AbsolutePoint × ℝ) (hx : PrimaryTargetBounds.profileRadius h (nativeSlow L x.1) ∈ Set.Ioo (PrimaryTargetBounds.leftRadius nominal) (PrimaryTargetBounds.rightRadius nominal)) : absoluteTangent j L x = physicalTangentMode j L (nativeSlow L x.1) x.1.2 x.2

theorem NavierStokes.CorrectionInitialization.ActualPrimary.nativeSlow_toAbsolute_eq_slowChange {B N0 : ℕ} (L : Label B N0) (n : ℕ) (x : LocalSignedRequest.Point) : nativeSlow L (toAbsolute n x) = (ActualSignedGeometry.slowChange h (ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand L))) (BaseContextAssembly.slowCoordinates x)

theorem NavierStokes.CorrectionInitialization.ActualPrimary.periodicClock_toAbsolute {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (n : ℕ) (hi : CommonWindow.index h n ≤ ChartScales.nativeIndex h (BaseChartJets.cellBand L)) (Y : TorusInverse.Plane) : PeriodicPhaseAssembly.periodicClock (geometry j L) (clockWindow L).cutoff ((CommonCoverSolve.coverPower (CommonWindow.index h n)).symm Y) = PeriodicPhaseAssembly.periodicClock (ActualSignedGeometry.slotGeometry slots vectors_det (PartitionedCovariance.signedLabel (PrimaryGeometryAssembly.label nominal L) j) 0) (clockWindow L).cutoff ((CommonCoverSolve.coverPower (ChartScales.nativeIndex h (BaseChartJets.cellBand L) - CommonWindow.index h n)) Y)

theorem NavierStokes.CorrectionInitialization.ActualPrimary.chartCoefficients_phase_view {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (n : ℕ) (hi : CommonWindow.index h n ≤ ChartScales.nativeIndex h (BaseChartJets.cellBand L)) (x : FullPoint) : (chartCoefficients j L).phase n x = ActualSignedGeometry.preparedViewPhase certificate modulation slots (choice B N0).prepared j L n (CommonWindow.index h n) (PhysicalResidualTZ.swapCylinder x)

theorem NavierStokes.CorrectionInitialization.ActualPrimary.chart_nativePoint {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (n : ℕ) (hi : CommonWindow.index h n ≤ ChartScales.nativeIndex h (BaseChartJets.cellBand L)) (k : TorusInverse.Frequency) (x : LocalSignedRequest.Point) : (nativeSlow L (toAbsolute n x), (geometry j L).coordinates k (toAbsolute n x).2) = ActualSignedGeometry.copyPoint slots vectors_det (PartitionedCovariance.signedLabel (PrimaryGeometryAssembly.label nominal L) j) n (CommonWindow.index h n) k (ActualSignedGeometry.meanEquiv.symm x)

theorem NavierStokes.CorrectionInitialization.ActualPrimary.chartCoefficients_amplitude_copies {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (n : ℕ) (hi : CommonWindow.index h n ≤ ChartScales.nativeIndex h (BaseChartJets.cellBand L)) (x : FullPoint) : (chartCoefficients j L).amplitude n x = (ChartScales.Q n ^ CoordinateAlgebra.A h * ChartScales.Q (BaseChartJets.cellBand L) ^ (-CoordinateAlgebra.A h)) • ∑' (k : TorusInverse.Frequency), CurlClassBounds.complexify (attachedRawVelocity j L (ActualSignedGeometry.copyPoint slots vectors_det (PartitionedCovariance.signedLabel (PrimaryGeometryAssembly.label nominal L) j) n (CommonWindow.index h n) k (ActualSignedGeometry.meanEquiv.symm x.1)))

theorem NavierStokes.CorrectionInitialization.ActualPrimary.chartCoefficients_pressure_copies {B N0 : ℕ} (j : Fin 2) (L : Label B N0) (n : ℕ) (hi : CommonWindow.index h n ≤ ChartScales.nativeIndex h (BaseChartJets.cellBand L)) (x : FullPoint) : (chartCoefficients j L).pressure n x = (ChartScales.Q n ^ (2 * CoordinateAlgebra.A h) * ChartScales.Q (BaseChartJets.cellBand L) ^ (-(2 * CoordinateAlgebra.A h))) • ∑' (k : TorusInverse.Frequency), attachedRawPressure j L (ActualSignedGeometry.copyPoint slots vectors_det (PartitionedCovariance.signedLabel (PrimaryGeometryAssembly.label nominal L) j) n (CommonWindow.index h n) k (ActualSignedGeometry.meanEquiv.symm x.1))

theorem NavierStokes.CorrectionInitialization.ActualPrimary.periodic_cutoff_sum {B N0 : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (j : Fin 2) (L : Label B N0) (p : PhaseCalculus.Slow) (Y : TorusInverse.Plane) (f : TorusInverse.Frequency → E) (hs : ∀ (k : TorusInverse.Frequency), f k ≠ 0 → (geometry j L).coordinates k Y ∈ (clockWindow L).core) : periodicGaussian j L Y • ∑' (k : TorusInverse.Frequency), f k = ∑' (k : TorusInverse.Frequency), gaussian L (p, (geometry j L).coordinates k Y) • f k

The same periodic cutoff identity applies to a primary or signed native coefficient; only the actual native support is used.

theorem NavierStokes.CorrectionInitialization.ActualPrimary.periodic_cutoff_scalar_sum {B N0 : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (j : Fin 2) (L : Label B N0) (p : PhaseCalculus.Slow) (Y : TorusInverse.Plane) (a : ℝ) (f : TorusInverse.Frequency → E) (hs : ∀ (k : TorusInverse.Frequency), f k ≠ 0 → (geometry j L).coordinates k Y ∈ (clockWindow L).core) : periodicGaussian j L Y • a • ∑' (k : TorusInverse.Frequency), f k = ∑' (k : TorusInverse.Frequency), a • gaussian L (p, (geometry j L).coordinates k Y) • f k

A shared signed scalar stays outside the genuine lattice sum. It may be the current-state request evaluated at the common chart point.