Actual common signed-wave equations #
The native closed-cell equations are joined through the literal common copy construction. The complement is handled by actual input zero germs.
noncomputable def
NavierStokes.ActualSignedCommonDynamics.slope
{B N0 : ℕ}
(l : ActualSignedStageControls.SignedLabel B N0)
(n : ℕ)
:
Slope, given by ((parameters l).angularFrequency n : ℝ) / (parameters l).base.frequency n.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ActualSignedCommonDynamics.phase_smooth
{B N0 : ℕ}
(l : ActualSignedStageControls.SignedLabel B N0)
(n : ℕ)
:
theorem
NavierStokes.ActualSignedCommonDynamics.frequency_ne
{B N0 : ℕ}
(l : ActualSignedStageControls.SignedLabel B N0)
(n : ℕ)
:
theorem
NavierStokes.ActualSignedCommonDynamics.angular_ne
{B N0 : ℕ}
(l : ActualSignedStageControls.SignedLabel B N0)
(n : ℕ)
:
theorem
NavierStokes.ActualSignedCommonDynamics.frequency_slope
{B N0 : ℕ}
(l : ActualSignedStageControls.SignedLabel B N0)
(n : ℕ)
:
theorem
NavierStokes.ActualSignedCommonDynamics.angularInputs
{B N0 : ℕ}
(request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2)
(hangle : ∀ (n : ℕ), CopyAngularInvariance.Invariant (0, 1) (request n))
(l : ActualSignedStageControls.SignedLabel B N0)
(k : ActualSignedStageControls.Frequency)
:
SignedWaveUpdate.AngularInputs ActualSignedStageControls.fullStrip (ActualSignedStageControls.directions B)
(ActualSignedStageControls.parameters l).base (ActualSignedStageControls.matrix l k)
(ActualSignedStageControls.target l k) request (ActualSignedStageControls.mask l k)
(ActualSignedStageControls.fundamental l k) (ActualSignedStageControls.normalMotion l k)
(ActualSignedStageControls.action l k) (ActualSignedStageControls.cutoff l k) (slope l)
theorem
NavierStokes.ActualSignedCommonDynamics.angularData
{B N0 : ℕ}
(request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2)
(hangle : ∀ (n : ℕ), CopyAngularInvariance.Invariant (0, 1) (request n))
(l : ActualSignedStageControls.SignedLabel B N0)
(n : ℕ)
(k : ActualSignedStageControls.Frequency)
:
theorem
NavierStokes.ActualSignedCommonDynamics.geometry
{B : ℕ}
(n : ℕ)
:
CurlClassBounds.CylindricalGeometry ActualSignedStageControls.fullStrip.domain
(fun (x : ActualSignedStageControls.FullPoint) => x.1.1) ((ActualSignedStageControls.directions B).radialField n)
(fun (x : ActualSignedStageControls.FullPoint) => (ActualSignedStageControls.directions B).angular)
((ActualSignedStageControls.directions B).axialField ActualSignedStageControls.fullStrip n)
theorem
NavierStokes.ActualSignedCommonDynamics.geometryAt
{B : ℕ}
(n : ℕ)
{x : ActualSignedStageControls.FullPoint}
(hx : x ∈ ActualSignedStageControls.fullStrip.domain)
:
ClosedNativeWaveIdentities.GeometryAt (fun (x : ActualSignedStageControls.FullPoint) => x.1.1)
((ActualSignedStageControls.directions B).radialField n)
(fun (x : ActualSignedStageControls.FullPoint) => (ActualSignedStageControls.directions B).angular)
((ActualSignedStageControls.directions B).axialField ActualSignedStageControls.fullStrip n) x
theorem
NavierStokes.ActualSignedCommonDynamics.rawJets
{B N0 : ℕ}
{β : ℝ}
{request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2}
(hR :
∀ (q : Fin 2),
PeriodizedWaveBounds.UniformLocalJets ActualSignedStageControls.fullStrip
(fun (x : ActualSignedStageControls.SignedLabel B N0) (x_1 : ℕ) (x_2 : ActualSignedStageControls.FullPoint) =>
ActualSignedStageControls.fullStrip.zeta x_2)
β ActualSignedStageControls.phaseCell
fun (x : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (x_1 : ActualSignedStageControls.Frequency)
(x_2 : ActualSignedStageControls.FullPoint) =>
request n x_2 q)
{l : ActualSignedStageControls.SignedLabel B N0}
{n : ℕ}
{k : ActualSignedStageControls.Frequency}
{x : ActualSignedStageControls.FullPoint}
(hx : x ∈ ActualSignedStageControls.fullStrip.domain)
(hc : x ∈ ActualSignedStageControls.phaseCell l n k)
:
theorem
NavierStokes.ActualSignedCommonDynamics.local_equation
{B N0 : ℕ}
{β : ℝ}
{request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2}
(hR :
∀ (q : Fin 2),
PeriodizedWaveBounds.UniformLocalJets ActualSignedStageControls.fullStrip
(fun (x : ActualSignedStageControls.SignedLabel B N0) (x_1 : ℕ) (x_2 : ActualSignedStageControls.FullPoint) =>
ActualSignedStageControls.fullStrip.zeta x_2)
β ActualSignedStageControls.phaseCell
fun (x : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (x_1 : ActualSignedStageControls.Frequency)
(x_2 : ActualSignedStageControls.FullPoint) =>
request n x_2 q)
(hangle : ∀ (n : ℕ), CopyAngularInvariance.Invariant (0, 1) (request n))
(hfrozen : SignedWaveUpdate.FrozenAlong (ActualSignedStageControls.directions B).fast request)
{l : ActualSignedStageControls.SignedLabel B N0}
{n : ℕ}
{k : ActualSignedStageControls.Frequency}
{x : ActualSignedStageControls.FullPoint}
(hx : x ∈ ActualSignedStageControls.fullStrip.domain)
(hc : x ∈ ActualSignedStageControls.phaseCell l n k)
:
(((ActualSignedOutputBounds.copies request l).corrected ActualSignedStageControls.fullStrip
(ActualSignedStageControls.directions B) k).harmonicResidual
ActualSignedStageControls.fullStrip (ActualSignedStageControls.directions B) n x + fun (j : Fin 3) =>
(ActualSignedOutputBounds.copies request l).source n x j * HarmonicCalculus.carrier ((ActualSignedStageControls.parameters l).base.frequency n)
((ActualSignedStageControls.parameters l).base.phase n) x) = fun (j : Fin 3) =>
((ActualSignedOutputBounds.copies request l).localGood ActualSignedStageControls.fullStrip
(ActualSignedStageControls.directions B) n k x j + (ActualSignedOutputBounds.copies request l).localGaussian (ActualSignedStageControls.directions B) n k x j) * HarmonicCalculus.carrier ((ActualSignedStageControls.parameters l).base.frequency n)
((ActualSignedStageControls.parameters l).base.phase n) x
theorem
NavierStokes.ActualSignedCommonDynamics.common_equation
{B N0 : ℕ}
{β : ℝ}
{request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2}
(hR :
∀ (q : Fin 2),
PeriodizedWaveBounds.UniformLocalJets ActualSignedStageControls.fullStrip
(fun (x : ActualSignedStageControls.SignedLabel B N0) (x_1 : ℕ) (x_2 : ActualSignedStageControls.FullPoint) =>
ActualSignedStageControls.fullStrip.zeta x_2)
β ActualSignedStageControls.phaseCell
fun (x : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (x_1 : ActualSignedStageControls.Frequency)
(x_2 : ActualSignedStageControls.FullPoint) =>
request n x_2 q)
(hangle : ∀ (n : ℕ), CopyAngularInvariance.Invariant (0, 1) (request n))
(hfrozen : SignedWaveUpdate.FrozenAlong (ActualSignedStageControls.directions B).fast request)
(l : ActualSignedStageControls.SignedLabel B N0)
(n : ℕ)
{x : ActualSignedStageControls.FullPoint}
(hx : x ∈ ActualSignedStageControls.fullStrip.domain)
:
((ActualSignedOutputBounds.copies request l).commonCorrected ActualSignedStageControls.fullStrip
(ActualSignedStageControls.directions B)).harmonicResidual
ActualSignedStageControls.fullStrip (ActualSignedStageControls.directions B) n x = fun (j : Fin 3) =>
((ActualSignedOutputBounds.copies request l).globalGood ActualSignedStageControls.fullStrip
(ActualSignedStageControls.directions B) n x j + (ActualSignedOutputBounds.copies request l).globalGaussian (ActualSignedStageControls.directions B) n x j) * HarmonicCalculus.carrier ((ActualSignedStageControls.parameters l).base.frequency n)
((ActualSignedStageControls.parameters l).base.phase n) x
theorem
NavierStokes.ActualSignedCommonDynamics.common_curl_and_divergence
{B N0 : ℕ}
{β : ℝ}
{request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2}
(hR :
∀ (q : Fin 2),
PeriodizedWaveBounds.UniformLocalJets ActualSignedStageControls.fullStrip
(fun (x : ActualSignedStageControls.SignedLabel B N0) (x_1 : ℕ) (x_2 : ActualSignedStageControls.FullPoint) =>
ActualSignedStageControls.fullStrip.zeta x_2)
β ActualSignedStageControls.phaseCell
fun (x : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (x_1 : ActualSignedStageControls.Frequency)
(x_2 : ActualSignedStageControls.FullPoint) =>
request n x_2 q)
(l : ActualSignedStageControls.SignedLabel B N0)
(n : ℕ)
{x : ActualSignedStageControls.FullPoint}
(hx : x ∈ ActualSignedStageControls.fullStrip.domain)
:
CurlClassBounds.cylindricalCurl ((ActualSignedStageControls.parameters l).base.radius n)
((ActualSignedStageControls.directions B).radialField n)
(fun (x : ActualSignedStageControls.Point × ℝ) => (ActualSignedStageControls.directions B).angular)
((ActualSignedStageControls.directions B).axialField ActualSignedStageControls.fullStrip n)
((ActualSignedOutputBounds.copies request l).common.curlPotential ActualSignedStageControls.fullStrip
(ActualSignedStageControls.directions B) n)
x = HarmonicCalculus.vectorMode ((ActualSignedStageControls.parameters l).base.frequency n)
((ActualSignedStageControls.parameters l).base.phase n)
(((ActualSignedOutputBounds.copies request l).commonCorrected ActualSignedStageControls.fullStrip
(ActualSignedStageControls.directions B)).amplitude
n)
x ∧ HarmonicCalculus.cylindricalDivergence ((ActualSignedStageControls.parameters l).base.radius n)
((ActualSignedStageControls.directions B).radialField n)
(fun (x : ActualSignedStageControls.Point × ℝ) => (ActualSignedStageControls.directions B).angular)
((ActualSignedStageControls.directions B).axialField ActualSignedStageControls.fullStrip n)
(HarmonicCalculus.vectorMode ((ActualSignedStageControls.parameters l).base.frequency n)
((ActualSignedStageControls.parameters l).base.phase n)
(((ActualSignedOutputBounds.copies request l).commonCorrected ActualSignedStageControls.fullStrip
(ActualSignedStageControls.directions B)).amplitude
n))
x = 0
theorem
NavierStokes.ActualSignedCommonDynamics.phase_split
{B N0 : ℕ}
(request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2)
(hangle : ∀ (n : ℕ), CopyAngularInvariance.Invariant (0, 1) (request n))
(l : ActualSignedStageControls.SignedLabel B N0)
(n : ℕ)
(x : ActualSignedStageControls.Point)
(θ : ℝ)
:
(ActualSignedStageControls.parameters l).base.frequency n * (ActualSignedStageControls.parameters l).base.phase n (x, θ) = (ActualSignedStageControls.parameters l).base.frequency n * (ActualSignedStageControls.parameters l).base.phase n (x, 0) + ↑((ActualSignedStageControls.parameters l).angularFrequency n) * θ
theorem
NavierStokes.ActualSignedCommonDynamics.common_pressure_invariant
{B N0 : ℕ}
(request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2)
(hangle : ∀ (n : ℕ), CopyAngularInvariance.Invariant (0, 1) (request n))
(l : ActualSignedStageControls.SignedLabel B N0)
(n : ℕ)
:
CopyAngularInvariance.Invariant (0, 1) ((ActualSignedOutputBounds.copies request l).common.pressure n)
theorem
NavierStokes.ActualSignedCommonDynamics.corrected_invariant
{B N0 : ℕ}
(request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2)
(hangle : ∀ (n : ℕ), CopyAngularInvariance.Invariant (0, 1) (request n))
(l : ActualSignedStageControls.SignedLabel B N0)
(n : ℕ)
:
theorem
NavierStokes.ActualSignedCommonDynamics.good_invariant
{B N0 : ℕ}
(request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2)
(hangle : ∀ (n : ℕ), CopyAngularInvariance.Invariant (0, 1) (request n))
(l : ActualSignedStageControls.SignedLabel B N0)
(n : ℕ)
:
theorem
NavierStokes.ActualSignedCommonDynamics.gaussian_invariant
{B N0 : ℕ}
(request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2)
(hangle : ∀ (n : ℕ), CopyAngularInvariance.Invariant (0, 1) (request n))
(l : ActualSignedStageControls.SignedLabel B N0)
(n : ℕ)
:
theorem
NavierStokes.ActualSignedCommonDynamics.exact_represents
{B N0 : ℕ}
(request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2)
(hangle : ∀ (n : ℕ), CopyAngularInvariance.Invariant (0, 1) (request n))
(l : ActualSignedStageControls.SignedLabel B N0)
:
have z :=
(ActualSignedOutputBounds.copies request l).commonCorrected ActualSignedStageControls.fullStrip
(ActualSignedStageControls.directions B);
(((ActualSignedStageControls.parameters l).exactBlock ActualPrimaryBounds.strip request).oscillation = fun (n : ℕ) (x : ActualSignedStageControls.Point × ℝ) (i : Fin 3) =>
(HarmonicCalculus.vectorMode ((ActualSignedStageControls.parameters l).base.frequency n)
((ActualSignedStageControls.parameters l).base.phase n) (z.amplitude n) x i).re) ∧ ((ActualSignedStageControls.parameters l).exactBlock ActualPrimaryBounds.strip request).oscillatoryPressure = fun (n : ℕ) (x : ActualSignedStageControls.Point × ℝ) =>
(HarmonicCalculus.mode ((ActualSignedStageControls.parameters l).base.frequency n)
((ActualSignedStageControls.parameters l).base.phase n) (z.pressure n) x).re
theorem
NavierStokes.ActualSignedCommonDynamics.good_represents
{B N0 : ℕ}
(request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2)
(hangle : ∀ (n : ℕ), CopyAngularInvariance.Invariant (0, 1) (request n))
(l : ActualSignedStageControls.SignedLabel B N0)
:
((ActualSignedStageControls.parameters l).goodBlock ActualPrimaryBounds.strip request).oscillation = fun (n : ℕ) (x : ActualSignedStageControls.FullPoint) (i : Fin 3) =>
((ActualSignedOutputBounds.copies request l).globalGood ActualSignedStageControls.fullStrip
(ActualSignedStageControls.directions B) n x i * HarmonicCalculus.carrier ((ActualSignedStageControls.parameters l).base.frequency n)
((ActualSignedStageControls.parameters l).base.phase n) x).re
theorem
NavierStokes.ActualSignedCommonDynamics.gaussian_represents
{B N0 : ℕ}
(request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2)
(hangle : ∀ (n : ℕ), CopyAngularInvariance.Invariant (0, 1) (request n))
(l : ActualSignedStageControls.SignedLabel B N0)
:
((ActualSignedStageControls.parameters l).gaussianBlock ActualPrimaryBounds.strip request).oscillation = fun (n : ℕ) (x : ActualSignedStageControls.FullPoint) (i : Fin 3) =>
((ActualSignedOutputBounds.copies request l).globalGaussian (ActualSignedStageControls.directions B) n x i * HarmonicCalculus.carrier ((ActualSignedStageControls.parameters l).base.frequency n)
((ActualSignedStageControls.parameters l).base.phase n) x).re
theorem
NavierStokes.ActualSignedCommonDynamics.frame_match
{B N0 : ℕ}
(l : ActualSignedStageControls.SignedLabel B N0)
:
theorem
NavierStokes.ActualSignedCommonDynamics.context_linear_identity
{B N0 : ℕ}
{β : ℝ}
{request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2}
(hR :
∀ (q : Fin 2),
PeriodizedWaveBounds.UniformLocalJets ActualSignedStageControls.fullStrip
(fun (x : ActualSignedStageControls.SignedLabel B N0) (x_1 : ℕ) (x_2 : ActualSignedStageControls.FullPoint) =>
ActualSignedStageControls.fullStrip.zeta x_2)
β ActualSignedStageControls.phaseCell
fun (x : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (x_1 : ActualSignedStageControls.Frequency)
(x_2 : ActualSignedStageControls.FullPoint) =>
request n x_2 q)
(hangle : ∀ (n : ℕ), CopyAngularInvariance.Invariant (0, 1) (request n))
(hfrozen : SignedWaveUpdate.FrozenAlong (ActualSignedStageControls.directions B).fast request)
(l : ActualSignedStageControls.SignedLabel B N0)
(a : CorrectionState.HarmonicBlock ActualSignedStageControls.Point)
(hc :
CorrectionStep.SameCarrier a ((ActualSignedStageControls.parameters l).exactBlock ActualPrimaryBounds.strip request))
(n : ℕ)
(x : ActualSignedStageControls.FullPoint)
(hx : x.1 ∈ ActualPrimaryBounds.strip.domain)
:
CorrectionStep.linearBlockField (CorrectionInitialization.ActualPrimary.commonContext B) a
((ActualSignedStageControls.parameters l).exactBlock ActualPrimaryBounds.strip request) n x = ((ActualSignedStageControls.parameters l).goodBlock ActualPrimaryBounds.strip request).oscillation n x + ((ActualSignedStageControls.parameters l).gaussianBlock ActualPrimaryBounds.strip request).oscillation n x
theorem
NavierStokes.ActualSignedCommonDynamics.full_divergence_zero
{B N0 : ℕ}
{β : ℝ}
{request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2}
(hR :
∀ (q : Fin 2),
PeriodizedWaveBounds.UniformLocalJets ActualSignedStageControls.fullStrip
(fun (x : ActualSignedStageControls.SignedLabel B N0) (x_1 : ℕ) (x_2 : ActualSignedStageControls.FullPoint) =>
ActualSignedStageControls.fullStrip.zeta x_2)
β ActualSignedStageControls.phaseCell
fun (x : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (x_1 : ActualSignedStageControls.Frequency)
(x_2 : ActualSignedStageControls.FullPoint) =>
request n x_2 q)
(hangle : ∀ (n : ℕ), CopyAngularInvariance.Invariant (0, 1) (request n))
(l : ActualSignedStageControls.SignedLabel B N0)
(n : ℕ)
(x : ActualSignedStageControls.FullPoint)
(hx : x.1 ∈ ActualPrimaryBounds.strip.domain)
:
HarmonicCalculus.cylindricalDivergence
(fun (q : LocalSignedRequest.Point × ℝ) =>
(CorrectionInitialization.ActualPrimary.commonContext B).operators.radius q.1)
(CorrectionStep.radialDirection (CorrectionInitialization.ActualPrimary.commonContext B) n)
CorrectionStep.angularDirection
(CorrectionStep.axialDirection (CorrectionInitialization.ActualPrimary.commonContext B) n)
(fun (q : LocalSignedRequest.Point × ℝ) (i : Fin 3) =>
↑(((ActualSignedStageControls.parameters l).exactBlock ActualPrimaryBounds.strip request).oscillation n q i))
x = 0
theorem
NavierStokes.ActualSignedCommonDynamics.modeSolenoidal
{B N0 : ℕ}
{β : ℝ}
{request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2}
(hR :
∀ (q : Fin 2),
PeriodizedWaveBounds.UniformLocalJets ActualSignedStageControls.fullStrip
(fun (x : ActualSignedStageControls.SignedLabel B N0) (x_1 : ℕ) (x_2 : ActualSignedStageControls.FullPoint) =>
ActualSignedStageControls.fullStrip.zeta x_2)
β ActualSignedStageControls.phaseCell
fun (x : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (x_1 : ActualSignedStageControls.Frequency)
(x_2 : ActualSignedStageControls.FullPoint) =>
request n x_2 q)
(hangle : ∀ (n : ℕ), CopyAngularInvariance.Invariant (0, 1) (request n))
(l : ActualSignedStageControls.SignedLabel B N0)
:
theorem
NavierStokes.ActualSignedCommonDynamics.linearGood_bounds
{B N0 : ℕ}
{β : ℝ}
{request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2}
(hR :
∀ (q : Fin 2),
PeriodizedWaveBounds.UniformLocalJets ActualSignedStageControls.fullStrip
(fun (x : ActualSignedStageControls.SignedLabel B N0) (x_1 : ℕ) (x_2 : ActualSignedStageControls.FullPoint) =>
ActualSignedStageControls.fullStrip.zeta x_2)
β ActualSignedStageControls.phaseCell
fun (x : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (x_1 : ActualSignedStageControls.Frequency)
(x_2 : ActualSignedStageControls.FullPoint) =>
request n x_2 q)
(hangle : ∀ (n : ℕ), CopyAngularInvariance.Invariant (0, 1) (request n))
(hfrozen : SignedWaveUpdate.FrozenAlong (ActualSignedStageControls.directions B).fast request)
(a : ActualSignedStageControls.SignedLabel B N0 → CorrectionState.HarmonicBlock ActualSignedStageControls.Point)
(hc :
∀ (l : ActualSignedStageControls.SignedLabel B N0),
CorrectionStep.SameCarrier (a l)
((ActualSignedStageControls.parameters l).exactBlock ActualPrimaryBounds.strip request))
:
UniformHarmonicInteraction.UniformVelocity ActualPrimaryBounds.strip ActualInitialization.envelope
(β + 1 - 3 * ChartScales.kappa) fun (l : ActualInitialization.Index B N0) =>
HarmonicWaveInteraction.linearGoodBlock (CorrectionInitialization.ActualPrimary.commonContext B) (a l)
((ActualSignedStageControls.parameters l).exactBlock ActualPrimaryBounds.strip request)
((ActualSignedStageControls.parameters l).gaussianBlock ActualPrimaryBounds.strip request).velocity
The actual context-linear remainder is obtained from the common PDE identity and the already proved native good-term estimates.
theorem
NavierStokes.ActualSignedCommonDynamics.actual_request_jets
{B N0 : ℕ}
(G : SignedMeanGain.Geometry)
(hs : G.strip = ActualPrimaryBounds.strip)
(u : CorrectionState.State ActualSignedStageControls.Point)
(α : ℝ)
(H :
MeanStateRegularity.PrimitiveData G.region G.patch.a G.patch.b
(CorrectionInitialization.ActualPrimary.commonContext B) u)
(hfixed : VariableGaugeMean.reconstructState G.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u = u)
(hθ : WeightedClasses.MeanClass G.strip α (u.thetaResidual (CorrectionInitialization.ActualPrimary.commonContext B)))
(hz : WeightedClasses.MeanClass G.strip α (u.axialResidual (CorrectionInitialization.ActualPrimary.commonContext B)))
(q : Fin 2)
:
PeriodizedWaveBounds.UniformLocalJets ActualSignedStageControls.fullStrip
(fun (x : ActualSignedStageControls.SignedLabel B N0) (x_1 : ℕ) (x_2 : ActualSignedStageControls.FullPoint) =>
ActualSignedStageControls.fullStrip.zeta x_2)
(α - 1) ActualSignedStageControls.phaseCell
fun (x : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (x_1 : ActualSignedStageControls.Frequency)
(x_2 : ActualSignedStageControls.FullPoint) =>
LocalSignedRequest.fullRequest G.strip G.patch G.coord (CorrectionInitialization.ActualPrimary.commonContext B) u n
x_2 q
theorem
NavierStokes.ActualSignedCommonDynamics.actual_modeSolenoidal
{B N0 : ℕ}
(G : SignedMeanGain.Geometry)
(hs : G.strip = ActualPrimaryBounds.strip)
(u : CorrectionState.State ActualSignedStageControls.Point)
(α : ℝ)
(H :
MeanStateRegularity.PrimitiveData G.region G.patch.a G.patch.b
(CorrectionInitialization.ActualPrimary.commonContext B) u)
(hfixed : VariableGaugeMean.reconstructState G.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u = u)
(hθ : WeightedClasses.MeanClass G.strip α (u.thetaResidual (CorrectionInitialization.ActualPrimary.commonContext B)))
(hz : WeightedClasses.MeanClass G.strip α (u.axialResidual (CorrectionInitialization.ActualPrimary.commonContext B)))
(l : ActualSignedStageControls.SignedLabel B N0)
:
HarmonicWaveInteraction.ModeSolenoidal ActualPrimaryBounds.strip
(CorrectionInitialization.ActualPrimary.commonContext B)
((ActualSignedStageControls.parameters l).exactBlock ActualPrimaryBounds.strip
(LocalSignedRequest.fullRequest G.strip G.patch G.coord (CorrectionInitialization.ActualPrimary.commonContext B) u))
The exact signed harmonic block from the current residual is solenoidal. No output divergence or global native-control record is used.
theorem
NavierStokes.ActualSignedCommonDynamics.actual_linearGood_bounds
{B N0 : ℕ}
(G : SignedMeanGain.Geometry)
(hs : G.strip = ActualPrimaryBounds.strip)
(u : CorrectionState.State ActualSignedStageControls.Point)
(α : ℝ)
(H :
MeanStateRegularity.PrimitiveData G.region G.patch.a G.patch.b
(CorrectionInitialization.ActualPrimary.commonContext B) u)
(hfixed : VariableGaugeMean.reconstructState G.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u = u)
(hθ : WeightedClasses.MeanClass G.strip α (u.thetaResidual (CorrectionInitialization.ActualPrimary.commonContext B)))
(hz : WeightedClasses.MeanClass G.strip α (u.axialResidual (CorrectionInitialization.ActualPrimary.commonContext B)))
(a : ActualSignedStageControls.SignedLabel B N0 → CorrectionState.HarmonicBlock ActualSignedStageControls.Point)
(hc :
∀ (l : ActualSignedStageControls.SignedLabel B N0),
CorrectionStep.SameCarrier (a l)
((ActualSignedStageControls.parameters l).exactBlock ActualPrimaryBounds.strip
(LocalSignedRequest.fullRequest G.strip G.patch G.coord (CorrectionInitialization.ActualPrimary.commonContext B)
u)))
:
UniformHarmonicInteraction.UniformVelocity ActualPrimaryBounds.strip ActualInitialization.envelope
(α - 3 * ChartScales.kappa) fun (l : ActualInitialization.Index B N0) =>
HarmonicWaveInteraction.linearGoodBlock (CorrectionInitialization.ActualPrimary.commonContext B) (a l)
((ActualSignedStageControls.parameters l).exactBlock ActualPrimaryBounds.strip
(LocalSignedRequest.fullRequest G.strip G.patch G.coord (CorrectionInitialization.ActualPrimary.commonContext B)
u))
((ActualSignedStageControls.parameters l).gaussianBlock ActualPrimaryBounds.strip
(LocalSignedRequest.fullRequest G.strip G.patch G.coord (CorrectionInitialization.ActualPrimary.commonContext B)
u)).velocity
The signed linear gain needed by the actual correction cycle. Only the incoming residual bounds, reconstruction, and carrier match are supplied. The Gaussian block is the literal computed one.