Principal equations on actual native cells #
The signed coefficient uses the literal covariance quotient, and the particular coefficient uses the literal finite-path modal solve. All regularity needed in these equations is obtained on the selected native cell. No global covariance-control or solved-output class is required.
theorem
NavierStokes.NativePrincipalEquations.signed_coefficients_principal_at
{D I : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{K : ℕ → I → Set D}
{a : I → LinearWaveBounds.WaveCoefficients D}
{dirs : I → LinearWaveBounds.GraphDirections D}
{H : I → ℕ → D → SignedWaveUpdate.Mat2}
{T R : I → ℕ → D → SignedWaveUpdate.Vec2}
{mask : I → ℕ → D → ℝ}
{v Ndot : I → ℕ → D → ProblemStatement.Space}
{A : I → ℕ → D → ProblemStatement.Space →L[ℝ] ProblemStatement.Space}
{W : ℕ → D → ℝ}
{β : ℝ}
(hcov : SignedCopyBounds.NativeCovariance s K H T)
(hR :
∀ (q : Fin 2),
PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => s.zeta x_1) β K fun (n : ℕ) (i : I) (x : D) => R i n x q)
(hm : PeriodizedWaveBounds.LocalJets s (fun (x : ℕ) (x_1 : D) => 1) 0 K fun (n : ℕ) (i : I) => mask i n)
(hv : PeriodizedWaveBounds.LocalJets s W 0 K fun (n : ℕ) (i : I) => v i n)
(j : Fin 2)
(n : ℕ)
(i : I)
{x : D}
(hx : x ∈ s.domain)
(hi : x ∈ K n i)
(hHf : SignedWaveUpdate.FrozenAlong (dirs i).fast (H i))
(hTf : SignedWaveUpdate.FrozenAlong (dirs i).fast (T i))
(hRf : SignedWaveUpdate.FrozenAlong (dirs i).fast (R i))
(hmf : SignedWaveUpdate.FrozenAlong (dirs i).fast (mask i))
(hfrequency : (a i).frequency n ≠ 0)
(hode :
HarmonicCalculus.along ((dirs i).fastField n) (v i n) x = TangentProjection.projectedRhs ((a i).normal s (dirs i) n x) (Ndot i n x) (v i n x) ((A i n x) (v i n x)) 0
(s.epsilon n * (a i).frequency n ^ 2 * ‖(a i).normal s (dirs i) n x‖ ^ 2))
(haction :
CurlClassBounds.complexify ((A i n x) (v i n x)) = LinearWaveResidual.shear ((a i).radius n) ((a i).frequencyBase n) ((a i).axialBase n) ((dirs i).radialField n)
(fun (y : D) => CurlClassBounds.complexify (v i n y)) x)
:
(SignedWaveUpdate.coefficients (a i) s (dirs i) (H i) (T i) (R i) (mask i) (v i) (Ndot i) (A i) j).principal s (dirs i)
n x = 0
The homogeneous principal equation for the actual signed quotient at a native-cell point. The only equation supplied as input is the primitive unit fundamental's projected equation; the signed equation is derived.
theorem
NavierStokes.NativePrincipalEquations.complexCopyCoefficients_principal_at
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{s : WeightedClasses.StripData (P × TorusInverse.Plane)}
{α : ℝ}
{dirs : LinearWaveBounds.GraphDirections (P × TorusInverse.Plane)}
{frame : ℕ → PrimaryODE.FrameData (P × ℝ)}
{t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space}
{source : ℕ → P × TorusInverse.Plane → CurlClassBounds.ComplexVector}
{harmonic : ℤ}
{g : ℕ → CommonCoverSolve.Geometry}
{L : ℕ → ℝ}
{envelope : ℕ → ℝ → ℝ}
{K : ℕ → TorusInverse.Frequency → Set (P × TorusInverse.Plane)}
(base : LinearWaveBounds.WaveCoefficients (P × TorusInverse.Plane))
(hL : ∀ (n : ℕ), 0 < L n)
(hr :
ParticularCopyBounds.ModalControl s α frame (fun (n : ℕ) => ParticularWaveBounds.realData (t n) (source n)) harmonic g
L envelope K)
(hi :
ParticularCopyBounds.ModalControl s α frame (fun (n : ℕ) => ParticularWaveBounds.imagData (t n) (source n)) harmonic g
L envelope K)
(n : ℕ)
(k : TorusInverse.Frequency)
{x : P × TorusInverse.Plane}
(hx : x ∈ s.domain)
(hk : x ∈ K n k)
(hfrequency : base.frequency n ≠ 0)
(hN : base.normal s dirs n x = (t n).normal (ParticularWaveBounds.nativePoint (g n) k x))
(hδ :
(t n).damping (ParticularWaveBounds.nativePoint (g n) k x) = s.epsilon n * base.frequency n ^ 2 * ‖base.normal s dirs n x‖ ^ 2)
(hfast : dirs.fastScale n • dirs.fast = (0, ParticularWaveBounds.slotDirection (g n)))
(hA :
∀ (z : ProblemStatement.Space),
CurlClassBounds.complexify (((t n).action (ParticularWaveBounds.nativePoint (g n) k x)) z) = LinearWaveResidual.shear (base.radius n) (base.frequencyBase n) (base.axialBase n) (dirs.radialField n)
(fun (x : P × TorusInverse.Plane) => CurlClassBounds.complexify z) x)
:
(ParticularWaveBounds.complexCopyCoefficients base t source g (fun (x : ℕ) => k) L hL).principal s dirs n x = -source n x
The complex finite-path solve satisfies its inhomogeneous principal equation at each native-cell point. Real and imaginary modal neighborhoods may differ: their intersection supplies the required common path domain.