Native controls for the actual signed correction

The fixed physical primary labels and their selected frames are reused. The raw signed mask contains only the slow spatial factor. Both compact native factors belong to the cutoff, so no time cutoff is declared frozen along the fast field.

@[reducible, inline]

abbrev NavierStokes.ActualSignedStageControls.Point : Type

Point: an abbreviation for LocalSignedRequest.Point.

Equations

• NavierStokes.ActualSignedStageControls.Point = NavierStokes.LocalSignedRequest.Point

@[reducible, inline]

abbrev NavierStokes.ActualSignedStageControls.FullPoint : Type

Full point: an abbreviation for Point × ℝ.

Equations

• NavierStokes.ActualSignedStageControls.FullPoint = (NavierStokes.ActualSignedStageControls.Point × ℝ)

@[reducible, inline]

abbrev NavierStokes.ActualSignedStageControls.Native : Type

Native: an abbreviation for ActualSignedGeometry.Native.

Equations

• NavierStokes.ActualSignedStageControls.Native = NavierStokes.ActualSignedGeometry.Native

@[reducible, inline]

abbrev NavierStokes.ActualSignedStageControls.Plane : Type

Plane: an abbreviation for TorusInverse.Plane.

Equations

• NavierStokes.ActualSignedStageControls.Plane = NavierStokes.TorusInverse.Plane

@[reducible, inline]

abbrev NavierStokes.ActualSignedStageControls.Frequency : Type

Frequency: an abbreviation for TorusInverse.Frequency.

Equations

• NavierStokes.ActualSignedStageControls.Frequency = NavierStokes.TorusInverse.Frequency

@[reducible, inline]

abbrev NavierStokes.ActualSignedStageControls.Space : Type

Space: an abbreviation for ProblemStatement.Space.

Equations

• NavierStokes.ActualSignedStageControls.Space = NavierStokes.ProblemStatement.Space

@[reducible, inline]

abbrev NavierStokes.ActualSignedStageControls.SignedLabel (B N0 : ℕ) : Type

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

Equations

• NavierStokes.ActualSignedStageControls.SignedLabel B N0 = (NavierStokes.CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2)

noncomputable def NavierStokes.ActualSignedStageControls.directions (B : ℕ) : LinearWaveBounds.GraphDirections (LocalSignedRequest.Point × ℝ)

Directions, given by PrimaryResidualClass.directions (ActualPrimary.commonContext B).

Equations

• NavierStokes.ActualSignedStageControls.directions B = NavierStokes.PrimaryResidualClass.directions (NavierStokes.CorrectionInitialization.ActualPrimary.commonContext B)

noncomputable def NavierStokes.ActualSignedStageControls.nativePoint {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (k : Frequency) (x : FullPoint) : Native

Native point as an element of Native.

Equations

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

noncomputable def NavierStokes.ActualSignedStageControls.coefficientScale {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) : ℝ

Coefficient scale, constructed using PhysicalSignedWave.coefficientScale.

Equations

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

noncomputable def NavierStokes.ActualSignedStageControls.normalScale {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) : ℝ

Normal scale, constructed using PhysicalParticularWave.normalWeight.

Equations

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

noncomputable def NavierStokes.ActualSignedStageControls.clockScale {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) : ℝ

Clock scale, given by PhysicalParticularWave.clockWeight ActualPrimary.h (ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand l.1)).

Equations

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

noncomputable def NavierStokes.ActualSignedStageControls.matrix {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) (n : ℕ) (x : FullPoint) : SignedWaveUpdate.Mat2

Matrix, given by ActualPrimary.covariance B N0 l.1 (nativePoint l n k x).1.

Equations

• NavierStokes.ActualSignedStageControls.matrix l k n x = NavierStokes.CorrectionInitialization.ActualPrimary.covariance B N0 l.1 (NavierStokes.ActualSignedStageControls.nativePoint l n k x).1

noncomputable def NavierStokes.ActualSignedStageControls.target {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) (n : ℕ) (x : FullPoint) : SignedWaveUpdate.Vec2

Target, given by coefficientScale l n ^ 2 • (fun q => PrimaryTargetBounds.actualTarget ActualPrimary.modulation (nativePoint l n k x).1 q).

Equations

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

noncomputable def NavierStokes.ActualSignedStageControls.mask {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) (n : ℕ) (x : FullPoint) : ℝ

Mask, given by ActualPrimary.spatialMask l.1 (nativePoint l n k x).1.

Equations

• NavierStokes.ActualSignedStageControls.mask l k n x = NavierStokes.CorrectionInitialization.ActualPrimary.spatialMask l.1 (NavierStokes.ActualSignedStageControls.nativePoint l n k x).1

noncomputable def NavierStokes.ActualSignedStageControls.fundamental {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) (n : ℕ) (x : FullPoint) : Space

Fundamental, constructed using PrimaryPulseBounds.normalizedPulse.

Equations

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

noncomputable def NavierStokes.ActualSignedStageControls.normalMotion {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) (n : ℕ) (x : FullPoint) : Space

Normal motion as an element of Space.

Equations

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

noncomputable def NavierStokes.ActualSignedStageControls.action {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) (n : ℕ) (x : FullPoint) : Space →L[ℝ] Space

Action, constructed using clockScale.

Equations

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

noncomputable def NavierStokes.ActualSignedStageControls.cutoff {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) (n : ℕ) (x : FullPoint) : ℝ

Cutoff, constructed using PartitionedCovariance.cutoff.

Equations

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

noncomputable def NavierStokes.ActualSignedStageControls.parameters {B N0 : ℕ} (l : SignedLabel B N0) : CorrectionStep.PeriodizedSignedParameters Point Frequency

The literal raw data accepted by the correction stage. The same selected primary frame is used for the matrix, unit pulse, and pressure.

Equations

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

theorem NavierStokes.ActualSignedStageControls.parameters_raw {B N0 : ℕ} (l : SignedLabel B N0) (s : WeightedClasses.StripData Point) (request : ℕ → FullPoint → SignedWaveUpdate.Vec2) (k : Frequency) : ((parameters l).copyData s request).raw k = SignedWaveUpdate.coefficients (CorrectionInitialization.ActualPrimary.chartCoefficients l.2 l.1) (HarmonicWaveInteraction.productStrip s) (directions B) (matrix l k) (target l k) request (mask l k) (fundamental l k) (normalMotion l k) (action l k) l.2

theorem NavierStokes.ActualSignedStageControls.coefficientScale_pos {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) : 0 < coefficientScale l n

theorem NavierStokes.ActualSignedStageControls.nativePoint_slow_auxiliary {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (k : Frequency) (x : FullPoint) (v : Plane) (t : ℝ) : (nativePoint l n k (x + t • ((0, 0, v), 0))).1 = (nativePoint l n k x).1

theorem NavierStokes.ActualSignedStageControls.nativePoint_angle {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (k : Frequency) (x : FullPoint) (t : ℝ) : nativePoint l n k (x + t • (0, 1)) = nativePoint l n k x

theorem NavierStokes.ActualSignedStageControls.directions_fast (B : ℕ) : (directions B).fast = ((0, 0, CorrectionInitialization.ActualPrimary.temporalVector), 0)

theorem NavierStokes.ActualSignedStageControls.matrix_frozen {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) : SignedWaveUpdate.FrozenAlong (directions B).fast (matrix l k)

theorem NavierStokes.ActualSignedStageControls.target_frozen {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) : SignedWaveUpdate.FrozenAlong (directions B).fast (target l k)

theorem NavierStokes.ActualSignedStageControls.mask_frozen {B N0 : ℕ} (l : SignedLabel B N0) (k : Frequency) : SignedWaveUpdate.FrozenAlong (directions B).fast (mask l k)

theorem NavierStokes.ActualSignedStageControls.request_frozen {B : ℕ} (s : WeightedClasses.StripData Point) (P : SignedStressPrimitive.Patch) (coord : ℝ) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) : SignedWaveUpdate.FrozenAlong (directions B).fast (LocalSignedRequest.fullRequest s P coord c u)

The request is estimated from actual current residuals

theorem NavierStokes.ActualSignedStageControls.fullRequest_jets_from_residuals (G : SignedMeanGain.Geometry) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (alpha : ℝ) (H : MeanStateRegularity.PrimitiveData G.region G.patch.a G.patch.b c u) (hfixed : VariableGaugeMean.reconstructState G.gauge c u = u) (hθ : WeightedClasses.MeanClass G.strip alpha (u.thetaResidual c)) (hz : WeightedClasses.MeanClass G.strip alpha (u.axialResidual c)) {Λ I : Type} (K : Λ → ℕ → I → Set FullPoint) (q : Fin 2) : PeriodizedWaveBounds.UniformLocalJets (HarmonicWaveInteraction.productStrip G.strip) (fun (x : Λ) (x_1 : ℕ) (x_2 : SignedMeanGain.Point × ℝ) => G.strip.zeta x_2.1) (alpha - 1) K fun (x : Λ) (n : ℕ) (x_1 : I) (x_2 : SignedMeanGain.Point × ℝ) => LocalSignedRequest.fullRequest G.strip G.patch G.coord c u n x_2 q

theorem NavierStokes.ActualSignedStageControls.fullRequest_jets_from_invariant {ι : Type} (G : SignedMeanGain.Geometry) (c : CorrectionState.Context Point) (primary : ι → CorrectionState.HarmonicBlock Point) (P : ι → ℕ → Point → ℝ) (labelCarrier : ι → ℕ → Set Point) (sigma : ℝ) (u : CorrectionStep.CycleState ι) (H : CorrectionStep.CycleAnalyticInvariant G c primary P labelCarrier sigma u) {Λ I : Type} (K : Λ → ℕ → I → Set FullPoint) (q : Fin 2) : PeriodizedWaveBounds.UniformLocalJets (HarmonicWaveInteraction.productStrip G.strip) (fun (x : Λ) (x_1 : ℕ) (x_2 : SignedMeanGain.Point × ℝ) => G.strip.zeta x_2.1) sigma K fun (x : Λ) (n : ℕ) (x_1 : I) (x_2 : SignedMeanGain.Point × ℝ) => LocalSignedRequest.fullRequest G.strip G.patch G.coord c u.state n x_2 q

The initial cycle invariant gives the request class without assuming any request derivative or signed output bound.

Native input jets on a neighborhood of the closed band

@[reducible, inline]

abbrev NavierStokes.ActualSignedStageControls.PulseLabel (B N0 : ℕ) : Type

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

Equations

• NavierStokes.ActualSignedStageControls.PulseLabel B N0 = (Fin 2 × NavierStokes.CorrectionInitialization.ActualPrimary.Label B N0)

noncomputable def NavierStokes.ActualSignedStageControls.slowJetDomain {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) : PrimaryCopyBounds.JetDomain (PulseLabel B N0) PhaseCalculus.Slow

Slow jet domain, bundling toDomain, growth, scale_le_growth.

Equations

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

theorem NavierStokes.ActualSignedStageControls.slow_geometry {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) : BaseChartJets.GeometryBounds (slowJetDomain U).toDomain CorrectionInitialization.ActualPrimary.h (BaseContextAssembly.geometryRadius CorrectionInitialization.ActualPrimary.nominal U) (BaseContextAssembly.geometryBound CorrectionInitialization.ActualPrimary.nominal U) (U.qlo / 2) (BaseContextAssembly.geometryUpper U) (NominalConeAssembly.activeLeft CorrectionInitialization.ActualPrimary.nominal) (NominalConeAssembly.activeRight CorrectionInitialization.ActualPrimary.nominal)

theorem NavierStokes.ActualSignedStageControls.slow_inverse_edge {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (l : PulseLabel B N0) {p : PhaseCalculus.Slow} (hp : p ∈ (slowJetDomain U).carrier l) : (FinalSlowBase.edgeDistance CorrectionInitialization.ActualPrimary.nominal (BaseChartJets.normalizedCoordinates CorrectionInitialization.ActualPrimary.h p).2)⁻¹ ≤ (slowJetDomain U).growth l p

theorem NavierStokes.ActualSignedStageControls.native_target_jets {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) : PrimaryCopyBounds.NativeJets (slowJetDomain U) (fun (x : PulseLabel B N0) => PrimaryTargetBounds.movingWeight CorrectionInitialization.ActualPrimary.nominal) fun (x : PulseLabel B N0) => PrimaryTargetBounds.actualTarget CorrectionInitialization.ActualPrimary.modulation

theorem NavierStokes.ActualSignedStageControls.native_matrix_jets {B N0 : ℕ} (r c : Fin 2) : PhaseJetBounds.PolynomialJets (PrimaryGeometryAssembly.domain CorrectionInitialization.ActualPrimary.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N) fun (l : PrimaryGeometryAssembly.Index CorrectionInitialization.ActualPrimary.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N) (p : PrimaryGeometryAssembly.Slow) => CorrectionInitialization.ActualPrimary.covariance B N0 l p r c

theorem NavierStokes.ActualSignedStageControls.native_matrix_slot_jets {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (r c : Fin 2) : PhaseJetBounds.PolynomialJets (ActualPhaseDefect.reducedJetDomain U) fun (l : Fin 2 × CorrectionInitialization.ActualPrimary.Label B N0) (z : ActualPhaseDefect.Slow × ℝ) => CorrectionInitialization.ActualPrimary.covariance B N0 l.2 z.1 r c

theorem NavierStokes.ActualSignedStageControls.native_mask_jets {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) : PhaseJetBounds.PolynomialJets (slowJetDomain U).toDomain fun (l : PulseLabel B N0) => CorrectionInitialization.ActualPrimary.spatialMask l.2

noncomputable def NavierStokes.ActualSignedStageControls.unitDomain {B N0 : ℕ} : PrimaryCopyBounds.JetDomain (CorrectionInitialization.ActualPrimary.Label B N0) (PhaseCalculus.Slow × ℝ)

Unit domain, bundling toDomain, growth, scale_le_growth.

Equations

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

noncomputable def NavierStokes.ActualSignedStageControls.nativeUnit {B N0 : ℕ} (l : PulseLabel B N0) : PhaseCalculus.Slow × ℝ → Space

Native unit, constructed using PrimaryPulseBounds.normalizedPulse.

Equations

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

noncomputable def NavierStokes.ActualSignedStageControls.nativeEnvelope {B N0 : ℕ} (l : PulseLabel B N0) (z : PhaseCalculus.Slow × ℝ) : ℝ

Native envelope, constructed using PrimaryPulseBounds.referenceP.

Equations

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

theorem NavierStokes.ActualSignedStageControls.native_unit_jets {B N0 : ℕ} : PrimaryCopyBounds.NativeJets (PrimaryCopyBounds.signDomain unitDomain) nativeEnvelope nativeUnit

noncomputable def NavierStokes.ActualSignedStageControls.nativePhase {B N0 : ℕ} : PhaseJetBounds.PhaseFamily (PulseLabel B N0)

Native phase, bundling epsilon, p, pz, x0 and the required compatibility proofs.

Equations

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

theorem NavierStokes.ActualSignedStageControls.native_phase_jets {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) : PhaseJetBounds.PolynomialJets (ActualPhaseDefect.reducedJetDomain U) nativePhase.normal ∧ PhaseJetBounds.PolynomialJets (ActualPhaseDefect.reducedJetDomain U) nativePhase.velocity ∧ PhaseJetBounds.PolynomialJets (ActualPhaseDefect.reducedJetDomain U) nativePhase.shear

theorem NavierStokes.ActualSignedStageControls.native_action_jets {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) : PhaseJetBounds.PolynomialJets (ActualPhaseDefect.reducedJetDomain U) fun (l : Fin 2 × CorrectionInitialization.ActualPrimary.Label B N0) (z : ActualPhaseDefect.Slow × ℝ) => PrimaryCopyBridge.baseOperator (nativePhase.F l z.1) (nativePhase.shear l z)

The actual band scalars

noncomputable def NavierStokes.ActualSignedStageControls.coefficientLower : ℝ

Coefficient lower as an element of ℝ.

Equations

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

noncomputable def NavierStokes.ActualSignedStageControls.coefficientUpper : ℝ

Coefficient upper, given by ActualSignedGeometry.powerBound (CoordinateAlgebra.A ActualPrimary.h) * ActualSignedGeometry.powerBound (-(ActualPrimary.h / 2)).

Equations

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

theorem NavierStokes.ActualSignedStageControls.coefficientLower_pos : 0 < coefficientLower

theorem NavierStokes.ActualSignedStageControls.coefficientUpper_one : 1 ≤ coefficientUpper

theorem NavierStokes.ActualSignedStageControls.coefficientScale_bounds {B N0 : ℕ} (l : SignedLabel B N0) {n : ℕ} (hnm : n ≤ BaseChartJets.cellBand l.1 + 4) (hmn : BaseChartJets.cellBand l.1 ≤ n + 4) : coefficientLower ≤ coefficientScale l n ∧ coefficientScale l n ≤ coefficientUpper

theorem NavierStokes.ActualSignedStageControls.nativePoint_eq_dynamics {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (k : Frequency) : nativePoint l n k = ActualPrimaryDynamics.copyPoint l.2 l.1 n k

theorem NavierStokes.ActualSignedStageControls.clockScale_eq_dynamics {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) : clockScale l n = ActualPrimaryDynamics.clockScale l.1 n

theorem NavierStokes.ActualSignedStageControls.normalScale_eq_dynamics {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) : normalScale l n = ActualPrimaryDynamics.normalScale l.1 n

One family of support cells in every band

noncomputable def NavierStokes.ActualSignedStageControls.absoluteNative {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (x : FullPoint) : Native

Absolute native, given by (ActualPrimary.nativeSlow l.1 (ActualPrimary.toAbsolute n x.1), (ActualPrimary.toAbsolute n x.1).2).

Equations

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

theorem NavierStokes.ActualSignedStageControls.absoluteNative_smooth {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) : ContDiff ℝ (↑⊤) (absoluteNative l n)

noncomputable def NavierStokes.ActualSignedStageControls.absoluteCells {B N0 : ℕ} (l : SignedLabel B N0) : PeriodizedWaveBounds.Cells Native Frequency

Absolute cells, constructed using PeriodizedWaveBounds.nativeCells.

Equations

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

noncomputable def NavierStokes.ActualSignedStageControls.cells {B N0 : ℕ} (l : SignedLabel B N0) : PeriodizedWaveBounds.Cells FullPoint Frequency

The copy cells use the fixed absolute primary geometry even in bands where the label is inactive. No truncated negative cover gap occurs.

Equations

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

theorem NavierStokes.ActualSignedStageControls.cells_mem {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (k : Frequency) (x : FullPoint) : x ∈ (cells l).carrier n k ↔ (nativePoint l n k x).2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow l.1).core

theorem NavierStokes.ActualSignedStageControls.nativePoint_smooth {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (k : Frequency) : ContDiff ℝ (↑⊤) (nativePoint l n k)

noncomputable def NavierStokes.ActualSignedStageControls.nativeTime {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (k : Frequency) (x : FullPoint) : ℝ

Native time, given by (ActualPrimary.pulseCoordinates l.1 (nativePoint l n k x)).2.

Equations

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

theorem NavierStokes.ActualSignedStageControls.nativeTime_smooth {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (k : Frequency) : ContDiff ℝ (↑⊤) (nativeTime l n k)

theorem NavierStokes.ActualSignedStageControls.cutoff_smooth {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (k : Frequency) : ContDiff ℝ (↑⊤) (cutoff l k n)

theorem NavierStokes.ActualSignedStageControls.cutoff_support {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (k : Frequency) : Function.support (cutoff l k n) ⊆ (cells l).carrier n k

theorem NavierStokes.ActualSignedStageControls.cutoff_zero_germ_outside_time {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (k : Frequency) {x : FullPoint} (hx : nativeTime l n k x ∉ Set.Icc (1 / 10) (9 / 10)) : cutoff l k n =ᶠ[nhds x] fun (x : FullPoint) => 0

Uniform transport on the actual closed control cells

noncomputable def NavierStokes.ActualSignedStageControls.fullStrip : WeightedClasses.StripData FullPoint

Full strip, given by ActualPrimaryBounds.fullStrip.

Equations

• NavierStokes.ActualSignedStageControls.fullStrip = NavierStokes.ActualPrimaryBounds.fullStrip

noncomputable def NavierStokes.ActualSignedStageControls.envelope {B N0 : ℕ} (l : SignedLabel B N0) : ℕ → FullPoint → ℝ

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

Equations

• NavierStokes.ActualSignedStageControls.envelope l = NavierStokes.ActualPrimaryBounds.fullEnvelope (l.2, l.1)

noncomputable def NavierStokes.ActualSignedStageControls.phaseCell {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (k : Frequency) : Set FullPoint

Phase cell, given by {x | x ∈ ActualPrimaryBounds.controlCell n ((l.2, l.1), k) ∧ nativeTime l n k x ∈ Icc (1 / 10 : ℝ) (9 / 10)}.

Equations

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

theorem NavierStokes.ActualSignedStageControls.nativePoint_eq_fullCopy {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (k : Frequency) (hn : ActualPrimaryBounds.near (l.2, l.1) n) : nativePoint l n k = ActualPrimaryBounds.fullCopy (l.2, l.1) n k

theorem NavierStokes.ActualSignedStageControls.phaseCell_time {B N0 : ℕ} {l : SignedLabel B N0} {n : ℕ} {k : Frequency} {x : FullPoint} (hc : x ∈ phaseCell l n k) : nativeTime l n k x ∈ Set.Ioo 0 1

theorem NavierStokes.ActualSignedStageControls.uniform_of_primary {B N0 : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {w : PulseLabel B N0 → ℕ → FullPoint → ℝ} {α : ℝ} {f : ℕ → ActualPrimaryBounds.CopyIndex B N0 → FullPoint → E} (hf : LocalizedWaveBounds.LocalClass fullStrip ActualPrimaryBounds.controlCell (fun (n : ℕ) (i : ActualPrimaryBounds.CopyIndex B N0) => w i.1 n) α f) : PeriodizedWaveBounds.UniformLocalJets fullStrip (fun (l : SignedLabel B N0) => w (l.2, l.1)) α phaseCell fun (l : SignedLabel B N0) (n : ℕ) (k : Frequency) => f n ((l.2, l.1), k)

theorem NavierStokes.ActualSignedStageControls.native_jets_on_phaseCell {B N0 : ℕ} {J D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {V : PrimaryCopyBounds.JetDomain J D} {w : J → D → ℝ} {f : J → D → E} (hf : PrimaryCopyBounds.NativeJets V w f) (index : SignedLabel B N0 → ℕ → J) (L : SignedLabel B N0 → ℕ → Frequency → FullPoint →L[ℝ] D) (c : SignedLabel B N0 → ℕ → Frequency → D) (W : SignedLabel B N0 → ℕ → FullPoint → ℝ) {A H : ℝ} (hA : 1 ≤ A) (hH : 1 ≤ H) (hmap : ∀ (l : SignedLabel B N0) (n : ℕ) (k : Frequency), ∀ x ∈ fullStrip.domain, x ∈ phaseCell l n k → (L l n k) x + c l n k ∈ V.carrier (index l n)) (hgrowth : ∀ (l : SignedLabel B N0) (n : ℕ) (k : Frequency), ∀ x ∈ fullStrip.domain, x ∈ phaseCell l n k → V.growth (index l n) ((L l n k) x + c l n k) ≤ A * fullStrip.growth n x) (hlinear : ∀ (l : SignedLabel B N0) (n : ℕ) (k : Frequency), ∀ x ∈ fullStrip.domain, x ∈ phaseCell l n k → ‖L l n k‖ ≤ H * fullStrip.slow n) (hweight : ∀ (l : SignedLabel B N0) (n : ℕ) (k : Frequency), ∀ x ∈ fullStrip.domain, x ∈ phaseCell l n k → w (index l n) ((L l n k) x + c l n k) ≤ W l n x) : PeriodizedWaveBounds.UniformLocalJets fullStrip W 0 phaseCell fun (l : SignedLabel B N0) (n : ℕ) (k : Frequency) (x : FullPoint) => f (index l n) ((L l n k) x + c l n k)

The affine derivative bound is required only on active cells. The single derivative constant still precedes every label, band and copy.

theorem NavierStokes.ActualSignedStageControls.matrix_local_jets {B N0 : ℕ} (r c : Fin 2) : PeriodizedWaveBounds.UniformLocalJets fullStrip (fun (x : SignedLabel B N0) (x_1 : ℕ) (x_2 : FullPoint) => 1) 0 phaseCell fun (l : SignedLabel B N0) (n : ℕ) (k : Frequency) (x : FullPoint) => matrix l k n x r c

noncomputable def NavierStokes.ActualSignedStageControls.slowLinear {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) : FullPoint →L[ℝ] PhaseCalculus.Slow

Slow linear, given by (ContinuousLinearMap.fst ℝ PhaseCalculus.Slow ℝ).comp (ActualPrimaryBounds.slotLinear (l.2, l.1) n).

Equations

• NavierStokes.ActualSignedStageControls.slowLinear l n = ContinuousLinearMap.fst ℝ NavierStokes.PhaseCalculus.Slow ℝ ∘SL NavierStokes.ActualPrimaryBounds.slotLinear (l.2, l.1) n

theorem NavierStokes.ActualSignedStageControls.slowLinear_bound {B N0 : ℕ} {l : SignedLabel B N0} {n : ℕ} (hn : ActualPrimaryBounds.near (l.2, l.1) n) : ‖slowLinear l n‖ ≤ ActualPrimaryBounds.copyCost * fullStrip.slow n

theorem NavierStokes.ActualSignedStageControls.slowCopy_affine {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (k : Frequency) (x : FullPoint) : (ActualPrimaryBounds.fullCopy (l.2, l.1) n k x).1 = (slowLinear l n) x + (ActualPrimaryBounds.fullCopy (l.2, l.1) n k 0).1

theorem NavierStokes.ActualSignedStageControls.slow_growth_eq {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (l : PulseLabel B N0) (x : Native) : (slowJetDomain U).growth l x.1 = (NativeBandExtension.radialDomain CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared).growth l.2 x

theorem NavierStokes.ActualSignedStageControls.copied_target_jets {B N0 : ℕ} : PeriodizedWaveBounds.UniformLocalJets fullStrip (fun (x : SignedLabel B N0) (x_1 : ℕ) (x_2 : FullPoint) => fullStrip.zeta x_2) 0 phaseCell fun (l : SignedLabel B N0) (n : ℕ) (k : Frequency) (x : FullPoint) => PrimaryTargetBounds.actualTarget CorrectionInitialization.ActualPrimary.modulation (nativePoint l n k x).1

theorem NavierStokes.ActualSignedStageControls.uniform_scalar_mul {B N0 : ℕ} {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {w : SignedLabel B N0 → ℕ → FullPoint → ℝ} {α : ℝ} {r : SignedLabel B N0 → ℕ → Frequency → FullPoint → ℝ} {f : SignedLabel B N0 → ℕ → Frequency → FullPoint → E} (hr : PeriodizedWaveBounds.UniformLocalJets fullStrip (fun (x : SignedLabel B N0) (x_1 : ℕ) (x_2 : FullPoint) => 1) 0 phaseCell r) (hf : PeriodizedWaveBounds.UniformLocalJets fullStrip w α phaseCell f) (hw : ∀ (l : SignedLabel B N0) (n : ℕ), ∀ x ∈ fullStrip.domain, 0 ≤ w l n x) : PeriodizedWaveBounds.UniformLocalJets fullStrip w α phaseCell fun (l : SignedLabel B N0) (n : ℕ) (k : Frequency) (x : FullPoint) => r l n k x • f l n k x

theorem NavierStokes.ActualSignedStageControls.uniform_map {B N0 : ℕ} {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {w : SignedLabel B N0 → ℕ → FullPoint → ℝ} {α : ℝ} {f : SignedLabel B N0 → ℕ → Frequency → FullPoint → E} (hf : PeriodizedWaveBounds.UniformLocalJets fullStrip w α phaseCell f) (hw : ∀ (l : SignedLabel B N0) (n : ℕ), ∀ x ∈ fullStrip.domain, 0 ≤ w l n x) (L : E →L[ℝ] F) : PeriodizedWaveBounds.UniformLocalJets fullStrip w α phaseCell fun (l : SignedLabel B N0) (n : ℕ) (k : Frequency) (x : FullPoint) => L (f l n k x)

theorem NavierStokes.ActualSignedStageControls.coefficientSquare_local_jets {B N0 : ℕ} : PeriodizedWaveBounds.UniformLocalJets fullStrip (fun (x : SignedLabel B N0) (x_1 : ℕ) (x_2 : FullPoint) => 1) 0 phaseCell fun (l : SignedLabel B N0) (n : ℕ) (x : Frequency) (x_1 : FullPoint) => coefficientScale l n ^ 2

theorem NavierStokes.ActualSignedStageControls.target_local_jets {B N0 : ℕ} (q : Fin 2) : PeriodizedWaveBounds.UniformLocalJets fullStrip (fun (x : SignedLabel B N0) (x_1 : ℕ) (x_2 : FullPoint) => fullStrip.zeta x_2) 0 phaseCell fun (l : SignedLabel B N0) (n : ℕ) (k : Frequency) (x : FullPoint) => target l k n x q

theorem NavierStokes.ActualSignedStageControls.mask_local_jets {B N0 : ℕ} : PeriodizedWaveBounds.UniformLocalJets fullStrip (fun (x : SignedLabel B N0) (x_1 : ℕ) (x_2 : FullPoint) => 1) 0 phaseCell fun (l : SignedLabel B N0) (n : ℕ) (k : Frequency) => mask l k n

theorem NavierStokes.ActualSignedStageControls.fullStrip_zeta_pos {x : FullPoint} (hx : x ∈ fullStrip.domain) : 0 < fullStrip.zeta x

theorem NavierStokes.ActualSignedStageControls.covariance_margins {B N0 : ℕ} {l : SignedLabel B N0} {n : ℕ} {k : Frequency} {x : FullPoint} (hx : x ∈ fullStrip.domain) (hc : x ∈ phaseCell l n k) : (1 / 5) ^ 2 * (CorrectionInitialization.ActualPrimary.choice B N0).detGap ≤ |Matrix.det (PrimaryPulseBounds.normalizedMatrix (√(fullStrip.slow n)) (matrix l k n x))| ∧ (∀ (r c : Fin 2), |√(fullStrip.slow n) * matrix l k n x r c| ≤ 5 * (CorrectionInitialization.ActualPrimary.choice B N0).entryBound) ∧ ∀ (j : Fin 2), coefficientLower ^ 2 * (CorrectionInitialization.ActualPrimary.choice B N0).inverseLower * fullStrip.zeta x ≤ SmoothCovariance.weights (matrix l k n x) (target l k n x) j

noncomputable def NavierStokes.ActualSignedStageControls.nativeCovariance (B N0 : ℕ) : SignedCopyBounds.UniformNativeCovariance fullStrip phaseCell matrix target

The uniform covariance record is constructed from the actual selected matrix and leading target, including both closed dyadic endpoints.

Equations

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

noncomputable def NavierStokes.ActualSignedStageControls.normalizeNative {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) : Native →L[ℝ] PhaseCalculus.Slow × ℝ

Normalize native, given by (ContinuousLinearMap.fst ℝ PhaseCalculus.Slow Plane).prod (ActualPrimaryBounds.timeProjection L).

Equations

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

theorem NavierStokes.ActualSignedStageControls.normalizeNative_apply {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) (x : Native) : (normalizeNative L) x = CorrectionInitialization.ActualPrimary.pulseCoordinates L x

theorem NavierStokes.ActualSignedStageControls.normalizeNative_norm {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) : ‖normalizeNative L‖ ≤ (CorrectionInitialization.ActualPrimary.choice B N0).prepared.M

noncomputable def NavierStokes.ActualSignedStageControls.pulseLinear {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) : FullPoint →L[ℝ] PhaseCalculus.Slow × ℝ

Pulse linear, given by (normalizeNative l.1).comp ((ActualPrimaryBounds.copyLinear (l.2, l.1) n).comp ActualPrimaryBounds.nativeOfFull).

Equations

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

theorem NavierStokes.ActualSignedStageControls.pulseLinear_bound {B N0 : ℕ} {l : SignedLabel B N0} {n : ℕ} (hn : ActualPrimaryBounds.near (l.2, l.1) n) : ‖pulseLinear l n‖ ≤ (CorrectionInitialization.ActualPrimary.choice B N0).prepared.M * ActualPrimaryBounds.copyCost * fullStrip.slow n

theorem NavierStokes.ActualSignedStageControls.pulseCopy_affine {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (k : Frequency) (x : FullPoint) : CorrectionInitialization.ActualPrimary.pulseCoordinates l.1 (ActualPrimaryBounds.fullCopy (l.2, l.1) n k x) = (pulseLinear l n) x + CorrectionInitialization.ActualPrimary.pulseCoordinates l.1 (ActualPrimaryBounds.fullCopy (l.2, l.1) n k 0)

theorem NavierStokes.ActualSignedStageControls.nativeEnvelope_copy {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (k : Frequency) (x : FullPoint) : nativeEnvelope (l.2, l.1) (CorrectionInitialization.ActualPrimary.pulseCoordinates l.1 (ActualPrimaryBounds.fullCopy (l.2, l.1) n k x)) = ActualPrimaryBounds.pulseEnvelope (l.2, l.1) (ActualPrimaryBounds.fullCopy (l.2, l.1) n k x).2.2

theorem NavierStokes.ActualSignedStageControls.fundamental_local_jets {B N0 : ℕ} : PeriodizedWaveBounds.UniformLocalJets fullStrip envelope 0 phaseCell fun (l : SignedLabel B N0) (n : ℕ) (k : Frequency) => fundamental l k n

theorem NavierStokes.ActualSignedStageControls.normalScale_local_jets {B N0 : ℕ} : PeriodizedWaveBounds.UniformLocalJets fullStrip (fun (x : SignedLabel B N0) (x_1 : ℕ) (x_2 : FullPoint) => 1) 0 phaseCell fun (l : SignedLabel B N0) (n : ℕ) (x : Frequency) (x_1 : FullPoint) => normalScale l n

theorem NavierStokes.ActualSignedStageControls.clockScale_local_jets {B N0 : ℕ} : PeriodizedWaveBounds.UniformLocalJets fullStrip (fun (x : SignedLabel B N0) (x_1 : ℕ) (x_2 : FullPoint) => 1) 0 phaseCell fun (l : SignedLabel B N0) (n : ℕ) (x : Frequency) (x_1 : FullPoint) => clockScale l n

theorem NavierStokes.ActualSignedStageControls.normal_local_jets {B N0 : ℕ} : PeriodizedWaveBounds.UniformLocalJets fullStrip (fun (x : SignedLabel B N0) (x_1 : ℕ) (x_2 : FullPoint) => 1) 0 phaseCell fun (l : SignedLabel B N0) (n : ℕ) (x : Frequency) => (CorrectionInitialization.ActualPrimary.chartCoefficients l.2 l.1).normal fullStrip (directions B) n

theorem NavierStokes.ActualSignedStageControls.normal_range {B N0 : ℕ} {l : SignedLabel B N0} {n : ℕ} {k : Frequency} {x : FullPoint} (hx : x ∈ fullStrip.domain) (hc : x ∈ phaseCell l n k) : ActualPrimaryBounds.normalFloor B N0 ≤ ‖(CorrectionInitialization.ActualPrimary.chartCoefficients l.2 l.1).normal fullStrip (directions B) n x‖ ∧ ‖(CorrectionInitialization.ActualPrimary.chartCoefficients l.2 l.1).normal fullStrip (directions B) n x‖ ≤ ActualPrimaryBounds.normalCeiling B N0

theorem NavierStokes.ActualSignedStageControls.normalMotion_local_jets {B N0 : ℕ} : PeriodizedWaveBounds.UniformLocalJets fullStrip (fun (x : SignedLabel B N0) (x_1 : ℕ) (x_2 : FullPoint) => 1) 0 phaseCell fun (l : SignedLabel B N0) (n : ℕ) (k : Frequency) => normalMotion l k n

theorem NavierStokes.ActualSignedStageControls.action_local_jets {B N0 : ℕ} : PeriodizedWaveBounds.UniformLocalJets fullStrip (fun (x : SignedLabel B N0) (x_1 : ℕ) (x_2 : FullPoint) => 1) 0 phaseCell fun (l : SignedLabel B N0) (n : ℕ) (k : Frequency) => action l k n

noncomputable def NavierStokes.ActualSignedStageControls.transverseProjection : Native →L[ℝ] ℝ

Transverse projection, given by (ContinuousLinearMap.fst ℝ ℝ ℝ).comp (ContinuousLinearMap.snd ℝ PhaseCalculus.Slow Plane).

Equations

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

theorem NavierStokes.ActualSignedStageControls.transverseProjection_norm : ‖transverseProjection‖ ≤ 1

theorem NavierStokes.ActualSignedStageControls.native_cutoff_jets {B N0 : ℕ} : PrimaryCopyBounds.NativeJets (PrimaryCopyBounds.signDomain (NativeBandExtension.radialDomain CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared)) (fun (x : Fin 2 × PrimaryGeometryAssembly.Index CorrectionInitialization.ActualPrimary.profile.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N) (x_1 : NativeBandExtension.Native) => 1) fun (l : PulseLabel B N0) (x : Native) => PartitionedCovariance.cutoff CorrectionInitialization.ActualPrimary.slots.radius x.2.1 * CorrectionInitialization.ActualPrimary.gaussian l.2 x

noncomputable def NavierStokes.ActualSignedStageControls.fullCopyLinear {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) : FullPoint →L[ℝ] Native

Full copy linear, given by (ActualPrimaryBounds.copyLinear (l.2, l.1) n).comp ActualPrimaryBounds.nativeOfFull.

Equations

• NavierStokes.ActualSignedStageControls.fullCopyLinear l n = NavierStokes.ActualPrimaryBounds.copyLinear (l.2, l.1) n ∘SL NavierStokes.ActualPrimaryBounds.nativeOfFull

theorem NavierStokes.ActualSignedStageControls.fullCopyLinear_bound {B N0 : ℕ} {l : SignedLabel B N0} {n : ℕ} (hn : ActualPrimaryBounds.near (l.2, l.1) n) : ‖fullCopyLinear l n‖ ≤ ActualPrimaryBounds.copyCost * fullStrip.slow n

theorem NavierStokes.ActualSignedStageControls.fullCopy_affine {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (k : Frequency) (x : FullPoint) : ActualPrimaryBounds.fullCopy (l.2, l.1) n k x = (fullCopyLinear l n) x + ActualPrimaryBounds.fullCopy (l.2, l.1) n k 0

theorem NavierStokes.ActualSignedStageControls.cutoff_local_jets {B N0 : ℕ} : PeriodizedWaveBounds.UniformLocalJets fullStrip (fun (x : SignedLabel B N0) (x_1 : ℕ) (x_2 : FullPoint) => 1) 0 phaseCell fun (l : SignedLabel B N0) (n : ℕ) (k : Frequency) => cutoff l k n

theorem NavierStokes.ActualSignedStageControls.uniform_select_two {B N0 : ℕ} {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {w : SignedLabel B N0 → ℕ → FullPoint → ℝ} {α : ℝ} {f : Fin 2 → SignedLabel B N0 → ℕ → Frequency → FullPoint → E} (hf : ∀ (j : Fin 2), PeriodizedWaveBounds.UniformLocalJets fullStrip w α phaseCell (f j)) (hw : ∀ (l : SignedLabel B N0) (n : ℕ), ∀ x ∈ fullStrip.domain, 0 ≤ w l n x) : PeriodizedWaveBounds.UniformLocalJets fullStrip w α phaseCell fun (l : SignedLabel B N0) => f l.2 l

theorem NavierStokes.ActualSignedStageControls.inverse_frequency_uniform {B N0 : ℕ} : UniformPrimaryWeights.UniformBandBound fullStrip (1 / 2) fun (i : SignedLabel B N0 × Frequency) (n : ℕ) => 1 / (CorrectionInitialization.ActualPrimary.chartCoefficients i.1.2 i.1.1).frequency n

theorem NavierStokes.ActualSignedStageControls.raw_coefficients_jets {B N0 : ℕ} {β : ℝ} {request : ℕ → FullPoint → SignedWaveUpdate.Vec2} (hR : ∀ (q : Fin 2), PeriodizedWaveBounds.UniformLocalJets fullStrip (fun (x : SignedLabel B N0) (x_1 : ℕ) (x_2 : FullPoint) => fullStrip.zeta x_2) β phaseCell fun (x : SignedLabel B N0) (n : ℕ) (x_1 : Frequency) (x_2 : FullPoint) => request n x_2 q) : (PeriodizedWaveBounds.UniformLocalJets fullStrip (fun (l : SignedLabel B N0) (n : ℕ) (x : FullPoint) => √(fullStrip.zeta x) * envelope l n x) (β + 1 / 2) phaseCell fun (l : SignedLabel B N0) (n : ℕ) (k : Frequency) => (((parameters l).copyData ActualPrimaryBounds.strip request).raw k).amplitude n) ∧ PeriodizedWaveBounds.UniformLocalJets fullStrip (fun (l : SignedLabel B N0) (n : ℕ) (x : FullPoint) => √(fullStrip.zeta x) * envelope l n x) (β + 1) phaseCell fun (l : SignedLabel B N0) (n : ℕ) (k : Frequency) => (((parameters l).copyData ActualPrimaryBounds.strip request).raw k).pressure n

The selected column is estimated uniformly before the physical label, band, and copy. Every matrix and unit in this theorem is the actual fixed primary construction; only the new signed request varies.

theorem NavierStokes.ActualSignedStageControls.actual_raw_coefficients_jets {B N0 : ℕ} (G : SignedMeanGain.Geometry) (hs : G.strip = ActualPrimaryBounds.strip) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (α : ℝ) (H : MeanStateRegularity.PrimitiveData G.region G.patch.a G.patch.b c u) (hfixed : VariableGaugeMean.reconstructState G.gauge c u = u) (hθ : WeightedClasses.MeanClass G.strip α (u.thetaResidual c)) (hz : WeightedClasses.MeanClass G.strip α (u.axialResidual c)) : (PeriodizedWaveBounds.UniformLocalJets fullStrip (fun (l : SignedLabel B N0) (n : ℕ) (x : FullPoint) => √(fullStrip.zeta x) * envelope l n x) (α - 1 / 2) phaseCell fun (l : SignedLabel B N0) (n : ℕ) (k : Frequency) => (((parameters l).copyData ActualPrimaryBounds.strip (LocalSignedRequest.fullRequest G.strip G.patch G.coord c u)).raw k).amplitude n) ∧ PeriodizedWaveBounds.UniformLocalJets fullStrip (fun (l : SignedLabel B N0) (n : ℕ) (x : FullPoint) => √(fullStrip.zeta x) * envelope l n x) α phaseCell fun (l : SignedLabel B N0) (n : ℕ) (k : Frequency) => (((parameters l).copyData ActualPrimaryBounds.strip (LocalSignedRequest.fullRequest G.strip G.patch G.coord c u)).raw k).pressure n

The actual full request is derived from the current residuals. No request-output class or signed-output estimate is an input.

noncomputable def NavierStokes.ActualSignedStageControls.covarianceAtLabel {B N0 : ℕ} (l : SignedLabel B N0) : SignedCopyBounds.NativeCovariance fullStrip (phaseCell l) (matrix l) (target l)

Covariance at label, bundling matrix_jets, target_jets, zeta_pos, determinantGap and the required compatibility proofs.

Equations

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

theorem NavierStokes.ActualSignedStageControls.primary_weight_pos {B N0 : ℕ} {l : SignedLabel B N0} {n : ℕ} {k : Frequency} {x : FullPoint} (hx : x ∈ fullStrip.domain) (hc : x ∈ phaseCell l n k) (j : Fin 2) : 0 < SmoothCovariance.weights (matrix l k n x) (target l k n x) j

theorem NavierStokes.ActualSignedStageControls.fundamental_eq_unitPulse {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (k : Frequency) : fundamental l k n = ActualSignedDynamics.unitPulse l.2 l.1 n k

theorem NavierStokes.ActualSignedStageControls.normalMotion_eq_unitMotion {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (k : Frequency) : normalMotion l k n = ActualSignedDynamics.unitMotion l.2 l.1 n k

theorem NavierStokes.ActualSignedStageControls.action_eq_unitAction {B N0 : ℕ} (l : SignedLabel B N0) (n : ℕ) (k : Frequency) : action l k n = ActualSignedDynamics.unitAction l.2 l.1 n k

theorem NavierStokes.ActualSignedStageControls.phaseCell_slow {B N0 : ℕ} {l : SignedLabel B N0} {n : ℕ} {k : Frequency} {x : FullPoint} (hc : x ∈ phaseCell l n k) : (nativePoint l n k x).1 ∈ (PrimaryGeometryAssembly.domain CorrectionInitialization.ActualPrimary.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N).carrier l.1

theorem NavierStokes.ActualSignedStageControls.phaseCell_slot {B N0 : ℕ} {l : SignedLabel B N0} {n : ℕ} {k : Frequency} {x : FullPoint} (hc : x ∈ phaseCell l n k) : (nativePoint l n k x).2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow l.1).core

theorem NavierStokes.ActualSignedStageControls.phaseCell_unitTime {B N0 : ℕ} {l : SignedLabel B N0} {n : ℕ} {k : Frequency} {x : FullPoint} (hc : x ∈ phaseCell l n k) : (nativePoint l n k x).2.2 / (CorrectionInitialization.ActualPrimary.phases B N0 l.2).L l.1 ∈ Set.Ioo 0 1

theorem NavierStokes.ActualSignedStageControls.actual_unit_ode {B N0 : ℕ} {l : SignedLabel B N0} {n : ℕ} {k : Frequency} {x : FullPoint} (hx : x ∈ fullStrip.domain) (hc : x ∈ phaseCell l n k) : HarmonicCalculus.along ((directions B).fastField n) (fundamental l k n) x = TangentProjection.projectedRhs ((CorrectionInitialization.ActualPrimary.chartCoefficients l.2 l.1).normal fullStrip (directions B) n x) (normalMotion l k n x) (fundamental l k n x) ((action l k n x) (fundamental l k n x)) 0 (fullStrip.epsilon n * (CorrectionInitialization.ActualPrimary.chartCoefficients l.2 l.1).frequency n ^ 2 * ‖(CorrectionInitialization.ActualPrimary.chartCoefficients l.2 l.1).normal fullStrip (directions B) n x‖ ^ 2)

theorem NavierStokes.ActualSignedStageControls.actual_unit_action {B N0 : ℕ} {l : SignedLabel B N0} {n : ℕ} {k : Frequency} {x : FullPoint} (hx : x ∈ fullStrip.domain) : CurlClassBounds.complexify ((action l k n x) (fundamental l k n x)) = LinearWaveResidual.shear ((CorrectionInitialization.ActualPrimary.chartCoefficients l.2 l.1).radius n) ((CorrectionInitialization.ActualPrimary.chartCoefficients l.2 l.1).frequencyBase n) ((CorrectionInitialization.ActualPrimary.chartCoefficients l.2 l.1).axialBase n) ((directions B).radialField n) (fun (y : CorrectionInitialization.ActualPrimary.FullPoint) => CurlClassBounds.complexify (fundamental l k n y)) x

theorem NavierStokes.ActualSignedStageControls.actual_unit_tangent_germ {B N0 : ℕ} {l : SignedLabel B N0} {n : ℕ} {k : Frequency} {x : FullPoint} (hx : x ∈ fullStrip.domain) (hc : x ∈ phaseCell l n k) : (fun (y : FullPoint) => inner ℝ ((CorrectionInitialization.ActualPrimary.chartCoefficients l.2 l.1).normal fullStrip (directions B) n y) (fundamental l k n y)) =ᶠ[nhds x] fun (x : FullPoint) => 0

theorem NavierStokes.ActualSignedStageControls.raw_tangent_germ {B N0 : ℕ} (request : ℕ → FullPoint → SignedWaveUpdate.Vec2) {l : SignedLabel B N0} {n : ℕ} {k : Frequency} {x : FullPoint} (hx : x ∈ fullStrip.domain) (hc : x ∈ phaseCell l n k) : (fun (y : FullPoint) => HarmonicCalculus.normalDot ((CorrectionInitialization.ActualPrimary.chartCoefficients l.2 l.1).normal fullStrip (directions B) n y) ((((parameters l).copyData ActualPrimaryBounds.strip request).raw k).amplitude n y)) =ᶠ[nhds x] fun (x : FullPoint) => 0

A genuine ambient tangency germ for the actual signed amplitude. It remains valid at the closed transverse and dyadic boundaries.

theorem NavierStokes.ActualSignedStageControls.raw_principal_zero {B N0 : ℕ} {β : ℝ} {request : ℕ → FullPoint → SignedWaveUpdate.Vec2} (hR : ∀ (q : Fin 2), PeriodizedWaveBounds.UniformLocalJets fullStrip (fun (x : SignedLabel B N0) (x_1 : ℕ) (x_2 : FullPoint) => fullStrip.zeta x_2) β phaseCell fun (x : SignedLabel B N0) (n : ℕ) (x_1 : Frequency) (x_2 : FullPoint) => request n x_2 q) (hfrozen : SignedWaveUpdate.FrozenAlong (directions B).fast request) {l : SignedLabel B N0} {n : ℕ} {k : Frequency} {x : FullPoint} (hx : x ∈ fullStrip.domain) (hc : x ∈ phaseCell l n k) : (((parameters l).copyData ActualPrimaryBounds.strip request).raw k).principal fullStrip (directions B) n x = 0

The literal signed quotient satisfies its homogeneous principal equation, with no global covariance-control premise.

theorem NavierStokes.ActualSignedStageControls.fullRequest_principal_zero {B N0 : ℕ} {β : ℝ} (s : WeightedClasses.StripData Point) (P : SignedStressPrimitive.Patch) (coord : ℝ) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (hR : ∀ (q : Fin 2), PeriodizedWaveBounds.UniformLocalJets fullStrip (fun (x : SignedLabel B N0) (x_1 : ℕ) (x_2 : FullPoint) => fullStrip.zeta x_2) β phaseCell fun (x : SignedLabel B N0) (n : ℕ) (x_1 : Frequency) (x_2 : FullPoint) => LocalSignedRequest.fullRequest s P coord c u n x_2 q) {l : SignedLabel B N0} {n : ℕ} {k : Frequency} {x : FullPoint} (hx : x ∈ fullStrip.domain) (hc : x ∈ phaseCell l n k) : (((parameters l).copyData ActualPrimaryBounds.strip (LocalSignedRequest.fullRequest s P coord c u)).raw k).principal fullStrip (directions B) n x = 0

theorem NavierStokes.ActualSignedStageControls.actual_principal_zero {B N0 : ℕ} (G : SignedMeanGain.Geometry) (hs : G.strip = ActualPrimaryBounds.strip) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (α : ℝ) (H : MeanStateRegularity.PrimitiveData G.region G.patch.a G.patch.b c u) (hfixed : VariableGaugeMean.reconstructState G.gauge c u = u) (hθ : WeightedClasses.MeanClass G.strip α (u.thetaResidual c)) (hz : WeightedClasses.MeanClass G.strip α (u.axialResidual c)) {l : SignedLabel B N0} {n : ℕ} {k : Frequency} {x : FullPoint} (hx : x ∈ fullStrip.domain) (hc : x ∈ phaseCell l n k) : (((parameters l).copyData ActualPrimaryBounds.strip (LocalSignedRequest.fullRequest G.strip G.patch G.coord c u)).raw k).principal fullStrip (directions B) n x = 0

The current residuals provide every request estimate needed by the actual homogeneous signed equation.