Exact field bookkeeping for one correction cycle #
The residuals in this file are the differentiated nonlinear fields in (32). In particular, changing the wave covariance and changing a mean velocity are not treated as independent black-box state transitions. Every old/new cross term is retained in the displayed residual differences.
Tensor: an abbreviation for Fin 3 → Fin 3 → ScalarField D.
Equations
Instances For
These are changes of the literal covariance terms in (32).
Equations
- NavierStokes.CorrectionStep.thetaCovarianceChange o X = o.radialDiv 2 (X 0 1) + o.dz (X 2 1)
Instances For
Axial covariance change, given by o.radialDiv 1 (X 0 2) + o.dz (X 2 2).
Equations
- NavierStokes.CorrectionStep.axialCovarianceChange o X = o.radialDiv 1 (X 0 2) + o.dz (X 2 2)
Instances For
Radial covariance change, given by -o.radialDiv 1 (X 0 0) - o.dz (X 2 0) + o.invRadius * X 1 1.
Equations
Instances For
A bound on each actual tensor entry. It is not a bound on the resulting residual and contains no update-preservation assertion.
Equations
- NavierStokes.CorrectionStep.TensorClass s α X = ∀ (i j : Fin 3), NavierStokes.WeightedClasses.MeanClass s α (X i j)
Instances For
The full differential residual, before angular averaging #
Exact residual of a perturbation of a fixed base, before the virtual stress and the separately retained base residual are added.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Radial direction, given by (c.operators.eR + (c.operators.radialFrequency n * c.operators.radialProfile x.1) • c.operators.vR, 0).
Equations
Instances For
Axial direction, given by (c.operators.epsilon n • c.operators.eZ, 0).
Equations
Instances For
Angular direction, given by (0, 1).
Equations
Instances For
Time direction, given by (c.operators.fastCoefficient n • c.operators.vT - c.operators.epsilon n • c.operators.eT, 0).
Equations
Instances For
Complex base, given by ![(c.base.radial n x.1 : ℂ), (c.base.angular n x.1 : ℂ), (c.base.axial n x.1 : ℂ)].
Equations
Instances For
Complex perturbation as an element of ComplexVector.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Complex pressure, given by (u.totalPressureIncrement n x : ℝ).
Equations
- NavierStokes.CorrectionStep.complexPressure u n x = ↑(u.totalPressureIncrement n x)
Instances For
Virtual divergence, given by ![0, -(c.operators.radialDiv 2 c.virtualTheta n x.1), -(c.operators.radialDiv 1 c.virtualAxial n x.1)].
Equations
- NavierStokes.CorrectionStep.virtualDivergence c n x = ![0, -c.operators.radialDiv 2 c.virtualTheta n x.1, -c.operators.radialDiv 1 c.virtualAxial n x.1]
Instances For
This field uses actual Fréchet derivatives. The base flat error is restored once, alongside the negative virtual-stress divergence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Full good residual, given by fullResidual c u - u.errors.total.
Equations
Instances For
Angular mean vector, defined pointwise by angularAverage (fun k p => f k p i) n x.
Equations
- NavierStokes.CorrectionStep.angularMeanVector f n x i = NavierStokes.CorrectionState.angularAverage (fun (k : ℕ) (p : D × ℝ) => f k p i) n x
Instances For
Angular nonconstant, defined pointwise by f n x i - angularMeanVector f n x.1 i.
Equations
- NavierStokes.CorrectionStep.angularNonconstant f n x i = f n x i - NavierStokes.CorrectionStep.angularMeanVector f n x.1 i
Instances For
Full good wave residual, given by angularNonconstant (fullGoodResidual c u).
Equations
Instances For
Angular continuous, given by ∀ n x i, Continuous (fun θ : ℝ => u n (x, θ) i).
Equations
- NavierStokes.CorrectionStep.AngularContinuous u = ∀ (n : ℕ) (x : D) (i : Fin 3), Continuous fun (θ : ℝ) => u n (x, θ) i
Instances For
The actual covariance increment contains both cross terms and the entire square of the exact increment.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Complex increment, given by ![(m.radial n x.1 + v n x 0 : ℝ), (m.angular n x.1 + v n x 1 : ℝ), (m.axial n x.1 + v n x 2 : ℝ)].
Equations
Instances For
Complex pressure increment, given by (p n x.1 + q n x : ℝ).
Equations
- NavierStokes.CorrectionStep.complexPressureIncrement p q n x = ↑(p n x.1 + q n x)
Instances For
The differential increment uses the old exact perturbation in both cross terms. The stored excluded residual is not multiplied into the PDE.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Mean bar, defined pointwise by PressureStream.torusAverage (f n) (x.1, x.2.1).
Equations
- NavierStokes.CorrectionStep.meanBar f n x = NavierStokes.PressureStream.torusAverage (f n) (x.1, x.2.1)
Instances For
Temporal pressure change, given by (temporalStage r h axial c u).pressure - u.pressure.
Equations
- NavierStokes.CorrectionStep.temporalPressureChange r h axial c u = (NavierStokes.CorrectionState.temporalStage r h axial c u).pressure - u.pressure
Instances For
The increment bound is proved for the actual inverse and stream, from the current residual classes. No increment or updated-residual class is assumed. The inverse-direction hypothesis is the concrete graph direction.
An actual temporal stage preserves the improved bar exponent whenever that exponent is below its proved differentiated remainder exponent.
The pressure change is bounded by applying the actual compact inverse
to the actual change of gr, whose centrifugal term is retained.
The axial alias remains explicit in the conclusion. Its superflatness is handled separately; it is not erased from the constructed velocity.
One physical field behind the chart family #
The predicate below is deliberately stronger than an indexed collection of unrelated chart solutions. Every chart is tied to the same physical fields by specified maps and the manuscript's velocity, pressure, and residual units. Operator naturality and the concrete chart maps are separate obligations.
Physical fields data, collecting mean, pressure, oscillation, oscillatoryPressure,
baseError, gaussianError and their compatibility conditions.
Mean field of
PhysicalFields, of typeP → Fin 3 → ℝ.- pressure : P → ℝ
Pressure field of
PhysicalFields, of typeP → ℝ. Oscillation of
PhysicalFields, of typeP × ℝ → Fin 3 → ℝ.Oscillatory pressure of
PhysicalFields, of typeP × ℝ → ℝ.Base error of
PhysicalFields, of typeP × ℝ → Fin 3 → ℝ.Gaussian error of
PhysicalFields, of typeP × ℝ → Fin 3 → ℝ.Alias error of
PhysicalFields, of typeP × ℝ → Fin 3 → ℝ.
Instances For
Add, bundling mean, pressure, oscillation, oscillatoryPressure and the required
compatibility proofs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Mean components, given by ![m.radial n x, m.angular n x, m.axial n x].
Equations
Instances For
chart includes the actual torus covering as well as spatial/time
rescaling. domain n specifies where that band is active.
Instances For
Actual addition preserves the specified common physical realization. This does not manufacture a realization for a separately solved chart.
Rank pressure change, given by (rankStage p r axial c u).pressure - u.pressure.
Equations
- NavierStokes.CorrectionStep.rankPressureChange p r axial c u = (NavierStokes.CorrectionState.rankStage p r axial c u).pressure - u.pressure
Instances For
The base error is restored and subtracted exactly once. Gaussian and alias errors remain actual subtracted means, with no zero/flat substitution.
The same cancellation only uses angular continuity on the selected fiber. No regularity outside the current physical domain is needed.
The concrete normalized five-row inverse uses the physical coordinate functions of the current slow point, with no dependence on the torus slot.
Equations
- One or more equations did not get rendered due to their size.
Instances For
All three classes of the actual rank increment follow from the measured
debt. The radial factor is the literal epsilon in rankIncrement.
The pressure estimate is for the pressure actually recomputed after the rank correction. The input is the current radial source, not an assumed bound on the new pressure.
Replace precisely the obsolete radial alias when the pressure has been recomputed. All other accumulated aliases remain in the error field.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The exact current radial alias cancels only the alias part of the reconstructed radial equation; the repaired pressure defect remains.
The right-hand sides for the particular solves are obtained from the literal current nonlinear PDE residual, by differentiating and convolving its stored finite harmonics and then removing the zero harmonic.
Reconstruction retains the actual zero mode and every stored error. No mean equation or error-flatness assertion is hidden in this identity.
The actual angular and reconstructed axial temporal increments have zero torus mean before taking either radial moment.
The zero harmonic of the differentiated coefficient reconstruction is the actual mean equation, with its exact excluded-error subtraction.
Mean lift, defined pointwise by meanComponents m n x.1.
Equations
Instances For
Mean divergence, defined pointwise by c.operators.dr m.radial n x + m.radial n x / c.operators.radius x + c.operators.dz m.axial n x.
Equations
Instances For
Full divergence as an element of OscillatoryScalar D.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Addition preserves actual cylindrical divergence by the derivative sum rule. The correction's divergence is a separate explicit summand.
Pressure reconstruction with the prescribed transported radial data for each band. This is an actual field constructor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Common temporal error as an element of Oscillation (PressureStream.Lift S).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Common temporal stage, constructed using reconstructPressureFamily.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Common temporal pressure change, given by (commonTemporalStage r h index axial c u).pressure - u.pressure.
Equations
- NavierStokes.CorrectionStep.commonTemporalPressureChange r h index axial c u = (NavierStokes.CorrectionStep.commonTemporalStage r h index axial c u).pressure - u.pressure
Instances For
Fast cancellation is now performed at the chosen common index; the remaining angular mean is the original torus bar plus the exact remainder.
Scale triple, bundling radial, angular, axial.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Changing the common clock multiplies the actual inverse and its actual stream realization by the same band scalar.
The common/native gap has no cost in the residual exponent. This statement works on any strip on which the native construction was proved.
Add coefficient families on the same fixed label carrier.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Same carrier data, collecting frequency, phase, angular.
Instances For
The cumulative difference is the literal coefficient difference from the same primary field, including all previous corrections.
Both old/new cross covariances and the entire new-wave square are estimated as actual angular integrals. There is no tensor-update premise.
Substitution of the constructed field into the state's covariance is now paired with the tensor class of its exact change.
The actual residual block retains a target exponent through a mean update. Its change is estimated by the two differentiated cross-advections.
With the cumulative wave exponent 1/2, each actual temporal or rank
mean increment has wave effect of exponent H.
A previously accumulated temporal alias remains subtracted through the rank stage. No size assumption on that unchanged alias is needed here.
Symmetric covariance, given by bilinearCovariance u v + bilinearCovariance v u.
Equations
Instances For
The signed update is separated at the level of actual angular integrals. The square contains the entire tangent plus curl increment.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Sub block, given by { a with velocity := fun n i => a.velocity n i - b.velocity n i pressure := fun n => a.pressure n - b.pressure n }.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The three signed errors have exponents δ+β, α+η, and 2β.
The stronger bound on the old-minus-primary field is used only for the
first term. No class of a resulting covariance is assumed.
Applying the fixed radial derivative loss still leaves the signed
tensor error at the manuscript's .17 improvement.
The native temporal construction is bounded on a genuine open slow domain. The source need not satisfy estimates at nonpositive slow time.
A local source estimate is transported through the actual common-clock inverse and then through the actual stream. No output estimate or global slow-domain extension is a hypothesis.
Recomputed pressure on the same local slow domain. The source change class is derived from the exact nonlinear radial equation.
The class of a literal coefficient difference is transported from the full cylindrical coefficient domain to the actual harmonic blocks.
The tangent and curl-difference blocks used by the tensor estimate are the blocks of the actual signed quotient, homogeneous pressure, cutoff, and curl construction. Their classes are conclusions from primitive data.
Both wave insertions retain their original carrier. This equality is about the actual evaluated fields, not only their coefficient arrays.
Cumulative bounds after the actual two coefficient additions. The reference field in the difference is the same primary tangent throughout.
The common clock cancels the actual local residual. Localization is used only to prove a germ identity for the same torus inverse.
Gauge temporal pressure change, given by `(temporalStageState g h index axial c u).pressure
- u.pressure`.
Equations
- NavierStokes.CorrectionStep.gaugeTemporalPressureChange g h index axial c u = (NavierStokes.VariableGaugeMean.temporalStageState g h index axial c u).pressure - u.pressure
Instances For
Gauge rank pressure change, given by (rankStageState g r axial c u).pressure - u.pressure.
Equations
- NavierStokes.CorrectionStep.gaugeRankPressureChange g r axial c u = (NavierStokes.VariableGaugeMean.rankStageState g r axial c u).pressure - u.pressure
Instances For
The actual gauge stream may differ from the desired axial inverse; its entire fast derivative is retained as the named axial alias.
The actual variable-gauge temporal update has the same differentiated mean remainder as the fixed-gauge update. Its axial alias remains explicit.
Gauge refresh pressure alias as an element of State (PressureStream.Lift S).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Gauge pressure alias block, given by ErrorHarmonics.zeroBlock b.frequency b.phase b.angularFrequency (fun n x => pressureAliasState g c u n (x, 0)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Gauge temporal alias block, given by ErrorHarmonics.zeroBlock b.frequency b.phase b.angularFrequency (fun n x => temporalAliasState g h index c u n (x, 0)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The coefficient/mean/error decomposition is a decomposition of the actual viscosity-one Cartesian residual after the proved graph scaling.
Equality of actual real block fields, together with the literal carrier transformation, determines the transformed source coefficients. Conjugacy is used explicitly to recover the full complex field.
Uniform label bounds and the proved slot overlap bound control the actual state covariance after adding every signed tangent and curl.
The only linear input is a bound on the literal old residual plus the literal linear increment after its Gaussian subtraction. All nonlinear terms of the actual new residual are derived by the harmonic calculus.
Zero triple, given by ⟨0, 0, 0⟩.
Equations
- NavierStokes.CorrectionStep.zeroTriple = { radial := 0, angular := 0, axial := 0 }
Instances For
Insert the actual oscillation and its actual excluded error, then reconstruct pressure from the resulting literal covariance.
Equations
Instances For
Gauge wave pressure change, given by (gaugeWaveStage g c u w q e).pressure - u.pressure.
Equations
- NavierStokes.CorrectionStep.gaugeWavePressureChange g c u w q e = (NavierStokes.CorrectionStep.gaugeWaveStage g c u w q e).pressure - u.pressure
Instances For
Fixed primitive data of one primary signed slot. No output field, output estimate, or state transition is stored in this record.
- base : LinearWaveBounds.WaveCoefficients (D × ℝ)
Base wave coefficients for the signed correction step.
- directions : LinearWaveBounds.GraphDirections (D × ℝ)
Directions of
SignedParameters, of typeLinearWaveBounds.GraphDirections (D × ℝ). - matrix : ℕ → D × ℝ → SignedWaveUpdate.Mat2
Matrix of
SignedParameters, of typeℕ → D × ℝ → SignedWaveUpdate.Mat2. - target : ℕ → D × ℝ → SignedWaveUpdate.Vec2
Target of
SignedParameters, of typeℕ → D × ℝ → SignedWaveUpdate.Vec2. Mask of
SignedParameters, of typeℕ → D × ℝ → ℝ.- fundamental : ℕ → D × ℝ → ProblemStatement.Space
Fundamental of
SignedParameters, of typeℕ → D × ℝ → ProblemStatement.Space. - normalMotion : ℕ → D × ℝ → ProblemStatement.Space
Normal motion of
SignedParameters, of typeℕ → D × ℝ → ProblemStatement.Space. - action : ℕ → D × ℝ → ProblemStatement.Space →L[ℝ] ProblemStatement.Space
Action of
SignedParameters, of typeℕ → D × ℝ → ProblemStatement.Space →L[ℝ] ProblemStatement.Space. Cutoff of
SignedParameters, of typeℕ → D × ℝ → ℝ.Angular frequency of
SignedParameters, of typeℕ → ℤ.- column : Fin 2
Column of
SignedParameters, of typeFin 2.
Instances For
Coefficients, constructed using SignedWaveUpdate.coefficients.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Exact block, constructed using SignedWaveUpdate.blockOfCoefficients.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Tangent block, given by SignedWaveUpdate.blockOfCoefficients ((p.coefficients s request).withCutoff p.cutoff) p.angularFrequency.
Equations
- p.tangentBlock s request = NavierStokes.SignedWaveUpdate.blockOfCoefficients ((p.coefficients s request).withCutoff p.cutoff) p.angularFrequency
Instances For
Curl block, given by subBlock (p.exactBlock s request) (p.tangentBlock s request).
Equations
- p.curlBlock s request = NavierStokes.CorrectionStep.subBlock (p.exactBlock s request) (p.tangentBlock s request)
Instances For
Every output bound here is derived from the same explicit signed quotient and curl, on the exact product strip used by the current state.
Control data, collecting baseBounds, kappa_le_half, covariance, mask, fundamental,
normal and their compatibility conditions.
- baseBounds : LinearWaveBounds.InputBounds (HarmonicWaveInteraction.productStrip s) P₀ α₀ κ p.directions p.base
- covariance : SignedWaveUpdate.CovarianceControl (HarmonicWaveInteraction.productStrip s) p.matrix p.target
- fundamental : WeightedClasses.MemClass (HarmonicWaveInteraction.productStrip s) (fun (n : ℕ) (x : D × ℝ) => P n x.1) 0 p.fundamental
- normalMotion : WeightedClasses.UnweightedClass (HarmonicWaveInteraction.productStrip s) 0 p.normalMotion
- action : WeightedClasses.UnweightedClass (HarmonicWaveInteraction.productStrip s) 0 p.action
- lower : ℝ
Lower of
Control, of typeℝ. - upper : ℝ
Upper of
Control, of typeℝ. - norm_lower (n : ℕ) (x : D × ℝ) : x ∈ (HarmonicWaveInteraction.productStrip s).domain → self.lower ≤ ‖p.base.normal (HarmonicWaveInteraction.productStrip s) p.directions n x‖
- norm_upper (n : ℕ) (x : D × ℝ) : x ∈ (HarmonicWaveInteraction.productStrip s).domain → ‖p.base.normal (HarmonicWaveInteraction.productStrip s) p.directions n x‖ ≤ self.upper
- inverseFrequency : WeightedClasses.BandBound (HarmonicWaveInteraction.productStrip s) (1 / 2) fun (n : ℕ) => 1 / p.base.frequency n
- cutoff : WeightedClasses.UnweightedClass (HarmonicWaveInteraction.productStrip s) 0 p.cutoff
Instances For
State signed block, given by p.exactBlock s (LocalSignedRequest.fullRequest s patch coord c u).
Equations
- NavierStokes.CorrectionStep.stateSignedBlock p s patch coord c u = p.exactBlock s (NavierStokes.LocalSignedRequest.fullRequest s patch coord c u)
Instances For
State signed tangent, given by p.tangentBlock s (LocalSignedRequest.fullRequest s patch coord c u).
Equations
- NavierStokes.CorrectionStep.stateSignedTangent p s patch coord c u = p.tangentBlock s (NavierStokes.LocalSignedRequest.fullRequest s patch coord c u)
Instances For
State signed curl, given by p.curlBlock s (LocalSignedRequest.fullRequest s patch coord c u).
Equations
- NavierStokes.CorrectionStep.stateSignedCurl p s patch coord c u = p.curlBlock s (NavierStokes.LocalSignedRequest.fullRequest s patch coord c u)
Instances For
State signed gaussian, constructed using SignedWaveUpdate.gaussianBlock.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Every signed block and Gaussian field is computed from the actual current residual. The pressure is then recomputed from the updated field.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The requested tensor is not supplied as an arbitrary input: these classes start from the current state's two actual mean residuals.
The actual real linearized cylindrical residual of a block, evaluated with the carrier of the old spatial label.
Equations
- One or more equations did not get rendered due to their size.
Instances For
An actual field cancellation determines every nonzero coefficient.
The Gaussian is subtracted only after its full field is retained in the
identity. The conclusion uses the literal linearGoodBlock.
Context real base, given by ![c.base.radial n x.1, c.base.angular n x.1, c.base.axial n x.1].
Equations
Instances For
Primitive equality of the direction and background data. This record contains no residual identity and no statement about a corrected field.
- time (n : ℕ) : (LinearWaveResidual.timeDirection (s.epsilon n) (d.fastField n) fun (x : D × ℝ) => d.slow) = timeDirection c n
Instances For
Good block, constructed using SignedWaveUpdate.coefficientBlock.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The ODE and phase data of the fixed primary column, before performing any signed update. All equalities concern primitive inputs.
Slope of
Dynamics, of typeℕ → ℝ.- angular : SignedWaveUpdate.AngularInputs (HarmonicWaveInteraction.productStrip s) p.directions p.base p.matrix p.target request p.mask p.fundamental p.normalMotion p.action p.cutoff self.slope
- geometry (n : ℕ) : CurlClassBounds.CylindricalGeometry (HarmonicWaveInteraction.productStrip s).domain (p.base.radius n) (p.directions.radialField n) (fun (x : D × ℝ) => p.directions.angular) (p.directions.axialField (HarmonicWaveInteraction.productStrip s) n)
- matrix_frozen : SignedWaveUpdate.FrozenAlong p.directions.fast p.matrix
- target_frozen : SignedWaveUpdate.FrozenAlong p.directions.fast p.target
- request_frozen : SignedWaveUpdate.FrozenAlong p.directions.fast request
- mask_frozen : SignedWaveUpdate.FrozenAlong p.directions.fast p.mask
- ode (n : ℕ) (x : D × ℝ) : x ∈ (HarmonicWaveInteraction.productStrip s).domain → HarmonicCalculus.along (p.directions.fastField n) (p.fundamental n) x = TangentProjection.projectedRhs (p.base.normal (HarmonicWaveInteraction.productStrip s) p.directions n x) (p.normalMotion n x) (p.fundamental n x) ((p.action n x) (p.fundamental n x)) 0 (s.epsilon n * p.base.frequency n ^ 2 * ‖p.base.normal (HarmonicWaveInteraction.productStrip s) p.directions n x‖ ^ 2)
- action_eq (n : ℕ) (x : D × ℝ) : x ∈ (HarmonicWaveInteraction.productStrip s).domain → CurlClassBounds.complexify ((p.action n x) (p.fundamental n x)) = LinearWaveResidual.shear (p.base.radius n) (p.base.frequencyBase n) (p.base.axialBase n) (p.directions.radialField n) (fun (y : D × ℝ) => CurlClassBounds.complexify (p.fundamental n y)) x
Instances For
Gaussian block, given by SignedWaveUpdate.gaussianBlock (p.coefficients s request) p.directions p.cutoff p.angularFrequency.
Equations
- p.gaussianBlock s request = NavierStokes.SignedWaveUpdate.gaussianBlock (p.coefficients s request) p.directions p.cutoff p.angularFrequency
Instances For
The actual signed field, with the literal Context operators, has the
computed good residual plus its computed Gaussian error.
The literal harmonic linear remainder has the gain proved for the constructed signed coefficient. No output residual class is an input.
Primitive localization data for the already chosen signed cutoff.
Slot of
GaussianControl, of typeGaussianTailFlat.SlotFamily (HarmonicWaveInteraction.productStrip s).Edges of
GaussianControl, of typeGaussianTailFlat.FlatEdges (HarmonicWaveInteraction.productStrip s).Scales of
GaussianControl, of typeGaussianTailFlat.BandScaleControl (HarmonicWaveInteraction.productStrip s).- rate : ℝ
Rate of
GaussianControl, of typeℝ.
Instances For
Slow rank increments preserve an already subtracted temporal alias. The slow axial identity comes from the constructed zero-mass stream.
Gauge supported, given by ∀ n, SupportedGauge a b ell U (f n).
Equations
- NavierStokes.CorrectionStep.GaugeSupported a b ell U f = ∀ (n : ℕ), NavierStokes.VariableGaugeMean.SupportedGauge a b ell U (f n)
Instances For
Gauge supported triple data, collecting radial, angular, axial.
- radial : GaugeSupported a b ell U m.radial
- angular : GaugeSupported a b ell U m.angular
- axial : GaugeSupported a b ell U m.axial
Instances For
The containing fixed annulus supplies smoothness only. The precise support conclusion retains the same moving physical edges.
The pressure difference is computed by the same variable-gauge integral. Both radial-source regularity statements and its class follow from the actual updated mean and unchanged covariance.
Direct pressure bound for the literal temporal stage. No class of a pressure source or pressure output is supplied as a hypothesis.
The same integral update for the literal rank stage, with its full centrifugal source change derived by the nonlinear mean identity.
Full local smoothness of the actual temporal stream components, including the axis where the annular support makes the quotients zero.
The primitive native data of one signed spatial label. Every copy uses the same carrier, base, and graph directions.
- base : LinearWaveBounds.WaveCoefficients (D × ℝ)
Base wave coefficients for the periodized signed correction.
- directions : LinearWaveBounds.GraphDirections (D × ℝ)
Directions of
PeriodizedSignedParameters, of typeLinearWaveBounds.GraphDirections (D × ℝ). - matrix : I → ℕ → D × ℝ → SignedWaveUpdate.Mat2
Matrix of
PeriodizedSignedParameters, of typeI → ℕ → D × ℝ → SignedWaveUpdate.Mat2. - target : I → ℕ → D × ℝ → SignedWaveUpdate.Vec2
Target of
PeriodizedSignedParameters, of typeI → ℕ → D × ℝ → SignedWaveUpdate.Vec2. Mask of
PeriodizedSignedParameters, of typeI → ℕ → D × ℝ → ℝ.- fundamental : I → ℕ → D × ℝ → ProblemStatement.Space
Fundamental of
PeriodizedSignedParameters, of typeI → ℕ → D × ℝ → ProblemStatement.Space. - normalMotion : I → ℕ → D × ℝ → ProblemStatement.Space
Normal motion of
PeriodizedSignedParameters, of typeI → ℕ → D × ℝ → ProblemStatement.Space. - action : I → ℕ → D × ℝ → ProblemStatement.Space →L[ℝ] ProblemStatement.Space
Action of
PeriodizedSignedParameters, of typeI → ℕ → D × ℝ → ProblemStatement.Space →L[ℝ] ProblemStatement.Space. Cutoff of
PeriodizedSignedParameters, of typeI → ℕ → D × ℝ → ℝ.Angular frequency of
PeriodizedSignedParameters, of typeℕ → ℤ.- column : Fin 2
Column of
PeriodizedSignedParameters, of typeFin 2.
Instances For
Native, bundling base, directions, matrix, target and the required compatibility
proofs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The native fields are evaluated from the signed quotient and projected homogeneous pressure before the one native cutoff is applied.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Exact block, constructed using SignedWaveUpdate.blockOfCoefficients.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Tangent block, given by SignedWaveUpdate.blockOfCoefficients (p.copyData s request).common p.angularFrequency.
Equations
- p.tangentBlock s request = NavierStokes.SignedWaveUpdate.blockOfCoefficients (p.copyData s request).common p.angularFrequency
Instances For
Curl block, given by subBlock (p.exactBlock s request) (p.tangentBlock s request).
Equations
- p.curlBlock s request = NavierStokes.CorrectionStep.subBlock (p.exactBlock s request) (p.tangentBlock s request)
Instances For
Good block, constructed using SignedWaveUpdate.coefficientBlock.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Gaussian block, constructed using SignedWaveUpdate.coefficientBlock.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Primitive per-band data of the actual complex Volterra inverse. The interval may vary with the physical clock. No solved field is stored.
- tangent : ℤ → ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space
Tangent of
ParticularParameters, of typeℤ → ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space. - geometry : ℕ → CommonCoverSolve.Geometry
Geometry of
ParticularParameters, of typeℕ → CommonCoverSolve.Geometry. Length of
ParticularParameters, of typeℕ → ℝ.- cutoff : ℕ → TorusInverse.Plane → ℝ
Cutoff of
ParticularParameters, of typeℕ → TorusInverse.Plane → ℝ. - background : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)
Background of
ParticularParameters, of typeLinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane). - directions : LinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane)
Directions of
ParticularParameters, of typeLinearWaveBounds.GraphDirections ((P × ℝ) × TorusInverse.Plane).
Instances For
Copy data, bundling background, amplitude, pressure, cutoff and the required
compatibility proofs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Native strip, given by ParticularWaveBounds.reindexStrip ParticularWaveAssembly.angleShuffle.symm (HarmonicWaveInteraction.productStrip s).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Wave, given by (p.copyData c u b G A j).commonCorrected (nativeStrip s) p.directions.
Equations
- p.wave s c u b G A j = (p.copyData c u b G A j).commonCorrected (NavierStokes.CorrectionStep.ParticularParameters.nativeStrip s) p.directions
Instances For
Update block, constructed using ParticularWaveAssembly.assembledBlock.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Good block, constructed using ParticularWaveAssembly.assembledBlock.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Gaussian block, constructed using ParticularWaveAssembly.assembledBlock.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Cycle point: an abbreviation for LocalSignedRequest.Point.
Instances For
Cycle slow: an abbreviation for ℝ × PressureStream.Plane.
Instances For
Cycle assoc, given by ParticularWaveBounds.liftAssoc PressureStream.Plane.
Equations
Instances For
Finite labeled coefficient data of the current fields. Correct representation is a separate invariant, not part of the construction.
Label type of
CycleCoefficients, of typeℕ → Finset ι.- blocks : ι → CorrectionState.HarmonicBlock CyclePoint
Blocks of
CycleCoefficients, of typeι → HarmonicBlock CyclePoint. - gaussian : ι → HarmonicResidual.BlockCoefficients CyclePoint
Gaussian residual coefficients indexed by harmonic label.
- aliasCoefficients : ι → HarmonicResidual.BlockCoefficients CyclePoint
Alias coefficients of
CycleCoefficients, of typeι → HarmonicResidual.BlockCoefficients CyclePoint. - residualBand : ℕ
Residual band of
CycleCoefficients, of typeℕ.
Instances For
Fixed geometric and primitive solver data for an actual correction cycle. The only state-dependent source is computed inside the stages.
Gauge of
CycleParameters, of typeGaugeData PressureStream.Plane.- strip : WeightedClasses.StripData CyclePoint
Strip of
CycleParameters, of typeStripData CyclePoint. - patch : SignedStressPrimitive.Patch
Patch of
CycleParameters, of typeSignedStressPrimitive.Patch. - coordinate : ℝ
Coordinate of
CycleParameters, of typeℝ. - timeExponent : ℝ
Time exponent of
CycleParameters, of typeℝ. Common index of
CycleParameters, of typeℕ → ℕ.Axial of
CycleParameters, of typePressureStream.Plane × PressureStream.Plane.- particular : ι → ParticularParameters CycleSlow
Particular of
CycleParameters, of typeι → ParticularParameters CycleSlow. - signed : ι → PeriodizedSignedParameters CyclePoint TorusInverse.Frequency
Signed of
CycleParameters, of typeι → PeriodizedSignedParameters CyclePoint TorusInverse.Frequency. Rank of
CycleParameters, of typeRankData PressureStream.Plane.
Instances For
Particular block, constructed using StateReindex.block.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Particular gaussian block, constructed using StateReindex.block.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Particular velocity, given by LabelSumBounds.fieldSum v.labels (fun l => (p.particularBlock v c u l).oscillation).
Equations
- p.particularVelocity v c u = NavierStokes.LabelSumBounds.fieldSum v.labels fun (l : ι) => (p.particularBlock v c u l).oscillation
Instances For
Particular pressure, defined pointwise by ∑ l ∈ v.labels n, (p.particularBlock v c u l).oscillatoryPressure n x.
Equations
- p.particularPressure v c u n x = ∑ l ∈ v.labels n, (p.particularBlock v c u l).oscillatoryPressure n x
Instances For
Particular gaussian, given by LabelSumBounds.fieldSum v.labels (fun l => (p.particularGaussianBlock v c u l).oscillation).
Equations
- p.particularGaussian v c u = NavierStokes.LabelSumBounds.fieldSum v.labels fun (l : ι) => (p.particularGaussianBlock v c u l).oscillation
Instances For
After particular, given by gaugeWaveStage p.gauge c u (p.particularVelocity v c u) (p.particularPressure v c u) ⟨0, p.particularGaussian v c u, 0⟩.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The signed request is recomputed from the actual state after the particular solve; it is not supplied independently.
Equations
- p.signedRequest v c u = NavierStokes.LocalSignedRequest.fullRequest p.strip p.patch p.coordinate c (p.afterParticular v c u)
Instances For
Signed block, given by (p.signed l).exactBlock p.strip (p.signedRequest v c u).
Equations
- p.signedBlock v c u l = (p.signed l).exactBlock p.strip (p.signedRequest v c u)
Instances For
Signed gaussian block, given by (p.signed l).gaussianBlock p.strip (p.signedRequest v c u).
Equations
- p.signedGaussianBlock v c u l = (p.signed l).gaussianBlock p.strip (p.signedRequest v c u)
Instances For
Signed velocity, given by LabelSumBounds.fieldSum v.labels (fun l => (p.signedBlock v c u l).oscillation).
Equations
- p.signedVelocity v c u = NavierStokes.LabelSumBounds.fieldSum v.labels fun (l : ι) => (p.signedBlock v c u l).oscillation
Instances For
Signed pressure, defined pointwise by ∑ l ∈ v.labels n, (p.signedBlock v c u l).oscillatoryPressure n x.
Equations
- p.signedPressure v c u n x = ∑ l ∈ v.labels n, (p.signedBlock v c u l).oscillatoryPressure n x
Instances For
Signed gaussian, given by LabelSumBounds.fieldSum v.labels (fun l => (p.signedGaussianBlock v c u l).oscillation).
Equations
- p.signedGaussian v c u = NavierStokes.LabelSumBounds.fieldSum v.labels fun (l : ι) => (p.signedGaussianBlock v c u l).oscillation
Instances For
After signed, constructed using gaugeWaveStage.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Temporal increment, given by temporalIncrementState p.gauge p.timeExponent p.commonIndex p.axial c (p.afterSigned v c u).
Equations
- p.temporalIncrement v c u = NavierStokes.VariableGaugeMean.temporalIncrementState p.gauge p.timeExponent p.commonIndex p.axial c (p.afterSigned v c u)
Instances For
After temporal, given by temporalStageState p.gauge p.timeExponent p.commonIndex p.axial c (p.afterSigned v c u).
Equations
- p.afterTemporal v c u = NavierStokes.VariableGaugeMean.temporalStageState p.gauge p.timeExponent p.commonIndex p.axial c (p.afterSigned v c u)
Instances For
Rank increment, given by rankIncrementState p.gauge p.rank p.axial c (p.afterTemporal v c u).
Equations
- p.rankIncrement v c u = NavierStokes.VariableGaugeMean.rankIncrementState p.gauge p.rank p.axial c (p.afterTemporal v c u)
Instances For
After rank, given by rankStageState p.gauge p.rank p.axial c (p.afterTemporal v c u).
Equations
- p.afterRank v c u = NavierStokes.VariableGaugeMean.rankStageState p.gauge p.rank p.axial c (p.afterTemporal v c u)
Instances For
Four literal updates followed by replacement of the obsolete radial pressure alias. The current radial alias is recorded exactly once.
Equations
- p.next v c u = NavierStokes.CorrectionStep.gaugeRefreshPressureAlias p.gauge c u (p.afterRank v c u)
Instances For
Final block, given by addBlock (addBlock (v.blocks l) (p.particularBlock v c u l)) (p.signedBlock v c u l).
Equations
- p.finalBlock v c u l = NavierStokes.CorrectionStep.addBlock (NavierStokes.CorrectionStep.addBlock (v.blocks l) (p.particularBlock v c u l)) (p.signedBlock v c u l)
Instances For
Full mean-step bound for the constructed temporal inverse and stream. The increment and pressure-change classes are conclusions.
The actual rank increment and its pressure change are derived from the measured debt. The previous temporal alias stays subtracted.
Both actual conserved masses survive all four stages. All radial integrals are evaluated on the valid local slow region.
The two actual mean stages complete the σ+1/10 mean and debt gains.
Every increment and pressure-change estimate is derived internally from the
post-signed residuals and measured debts.
Only primitive background fields remain in this native family. Its amplitude and pressure are zero, so its bounds assume no constructed output.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Uniform native-copy input data for the signed quotient. The current request is deliberately absent; it is supplied from the measured residual.
- cells : PeriodizedWaveBounds.Cells (D × ℝ) I
Cells of
NativeControl, of typePeriodizedWaveBounds.Cells (D × ℝ) I. Phase patch of
NativeControl, of typeℕ → I → Set (D × ℝ).- background : LocalizedWaveBounds.InputBounds (HarmonicWaveInteraction.productStrip s) self.phasePatch (fun (n : ℕ) (x : I) (x_1 : D × ℝ) => P n x_1.1) 0 κ p.directions (nativeBackground p.base)
- covariance : SignedCopyBounds.NativeCovariance (HarmonicWaveInteraction.productStrip s) self.phasePatch p.matrix p.target
Covariance supplied by
NativeControl. - mask : PeriodizedWaveBounds.LocalJets (HarmonicWaveInteraction.productStrip s) (fun (x : ℕ) (x_1 : D × ℝ) => 1) 0 self.phasePatch fun (n : ℕ) (i : I) => p.mask i n
- fundamental : PeriodizedWaveBounds.LocalJets (HarmonicWaveInteraction.productStrip s) (fun (n : ℕ) (x : D × ℝ) => P n x.1) 0 self.phasePatch fun (n : ℕ) (i : I) => p.fundamental i n
- normalMotion : PeriodizedWaveBounds.LocalJets (HarmonicWaveInteraction.productStrip s) (fun (x : ℕ) (x_1 : D × ℝ) => 1) 0 self.phasePatch fun (n : ℕ) (i : I) => p.normalMotion i n
- action : PeriodizedWaveBounds.LocalJets (HarmonicWaveInteraction.productStrip s) (fun (x : ℕ) (x_1 : D × ℝ) => 1) 0 self.phasePatch fun (n : ℕ) (i : I) => p.action i n
- cutoff : PeriodizedWaveBounds.LocalJets (HarmonicWaveInteraction.productStrip s) (fun (x : ℕ) (x_1 : D × ℝ) => 1) 0 self.phasePatch fun (n : ℕ) (i : I) => p.cutoff i n
- lower : ℝ
Lower of
NativeControl, of typeℝ. - upper : ℝ
Upper of
NativeControl, of typeℝ. - normal_lower (n : ℕ) (i : I) (x : D × ℝ) : x ∈ (HarmonicWaveInteraction.productStrip s).domain → x ∈ self.phasePatch n i → self.lower ≤ ‖p.base.normal (HarmonicWaveInteraction.productStrip s) p.directions n x‖
- normal_upper (n : ℕ) (i : I) (x : D × ℝ) : x ∈ (HarmonicWaveInteraction.productStrip s).domain → x ∈ self.phasePatch n i → ‖p.base.normal (HarmonicWaveInteraction.productStrip s) p.directions n x‖ ≤ self.upper
- inverse_frequency : WeightedClasses.BandBound (HarmonicWaveInteraction.productStrip s) (1 / 2) fun (n : ℕ) => 1 / p.base.frequency n
Instances For
All five full-lift classes are obtained from the actual quotient and uniform native data. Background estimates are used only on the cells.
Native tangent, defined pointwise by ParticularWaveAssembly.angleTangent (p.tangent j n).
Equations
Instances For
Input bounds for the actual complex Volterra solve on all of its native cells. The modal forcing is the literal current residual source.
- cells : PeriodizedWaveBounds.Cells ((Q × ℝ) × TorusInverse.Plane) TorusInverse.Frequency
Cells of
NativeControl, of typePeriodizedWaveBounds.Cells ((Q × ℝ) × Plane) Frequency. - phasePatch : ℕ → TorusInverse.Frequency → Set ((Q × ℝ) × TorusInverse.Plane)
Phase patch of
NativeControl, of typeℕ → Frequency → Set ((Q × ℝ) × Plane). - background : LocalizedWaveBounds.InputBounds (nativeStrip s) self.phasePatch (fun (n : ℕ) (x : TorusInverse.Frequency) => W n) 0 κ p.directions (nativeBackground (p.copyData c u b G A j).background)
Frame of
NativeControl, of typeℕ → PrimaryODE.FrameData ((Q × ℝ) × ℝ).Envelope of
NativeControl, of typeℕ → ℝ → ℝ.- realControl : ParticularCopyBounds.ModalControl (nativeStrip s) α self.frame (fun (n : ℕ) => ParticularWaveBounds.realData (p.nativeTangent j n) ((p.copyData c u b G A j).source n)) j p.geometry p.length self.envelope self.phasePatch
Real control supplied by
NativeControl. - imagControl : ParticularCopyBounds.ModalControl (nativeStrip s) α self.frame (fun (n : ℕ) => ParticularWaveBounds.imagData (p.nativeTangent j n) ((p.copyData c u b G A j).source n)) j p.geometry p.length self.envelope self.phasePatch
Imag control supplied by
NativeControl. - envelope_compare (n : ℕ) (i : TorusInverse.Frequency) (x : (Q × ℝ) × TorusInverse.Plane) : x ∈ (nativeStrip s).domain → x ∈ self.phasePatch n i → self.envelope n ((p.geometry n).coordinates i x.2).2 ≤ W n x
- normal : PeriodizedWaveBounds.LocalJets (nativeStrip s) (fun (x : ℕ) (x_1 : (Q × ℝ) × TorusInverse.Plane) => 1) 0 self.phasePatch fun (n : ℕ) (i : TorusInverse.Frequency) (x : (Q × ℝ) × TorusInverse.Plane) => (p.nativeTangent j n).normal (ParticularWaveBounds.nativePoint (p.geometry n) i x)
- normalMotion : PeriodizedWaveBounds.LocalJets (nativeStrip s) (fun (x : ℕ) (x_1 : (Q × ℝ) × TorusInverse.Plane) => 1) 0 self.phasePatch fun (n : ℕ) (i : TorusInverse.Frequency) (x : (Q × ℝ) × TorusInverse.Plane) => (p.nativeTangent j n).normalDot (ParticularWaveBounds.nativePoint (p.geometry n) i x)
- action : PeriodizedWaveBounds.LocalJets (nativeStrip s) (fun (x : ℕ) (x_1 : (Q × ℝ) × TorusInverse.Plane) => 1) 0 self.phasePatch fun (n : ℕ) (i : TorusInverse.Frequency) (x : (Q × ℝ) × TorusInverse.Plane) => (p.nativeTangent j n).action (ParticularWaveBounds.nativePoint (p.geometry n) i x)
- source : PeriodizedWaveBounds.LocalJets (nativeStrip s) (fun (n : ℕ) (x : (Q × ℝ) × TorusInverse.Plane) => √((nativeStrip s).zeta x) * W n x) α self.phasePatch fun (n : ℕ) (x : TorusInverse.Frequency) => (p.copyData c u b G A j).source n
- cutoff : PeriodizedWaveBounds.LocalJets (nativeStrip s) (fun (x : ℕ) (x_1 : (Q × ℝ) × TorusInverse.Plane) => 1) 0 self.phasePatch (p.copyData c u b G A j).cutoff
- cutoff_support (n : ℕ) (i : TorusInverse.Frequency) : Function.support ((p.copyData c u b G A j).cutoff n i) ⊆ self.cells.carrier n i
- phase_cover (n : ℕ) (i : TorusInverse.Frequency) (x : (Q × ℝ) × TorusInverse.Plane) : x ∈ (nativeStrip s).domain → x ∈ self.cells.carrier n i → x ∈ self.phasePatch n i ∨ ∀ᶠ (y : (Q × ℝ) × TorusInverse.Plane) in nhds x, ((p.geometry n).coordinates i y.2).2 ∈ Set.Icc 0 (p.length n) ∧ ∀ v ∈ Set.Icc 0 (p.length n), (p.copyData c u b G A j).source n (y.1, (p.geometry n).path i y.2 v) = 0
- lower : ℝ
Lower of
NativeControl, of typeℝ. - upper : ℝ
Upper of
NativeControl, of typeℝ. - normal_lower (n : ℕ) (i : TorusInverse.Frequency) (x : (Q × ℝ) × TorusInverse.Plane) : x ∈ (nativeStrip s).domain → x ∈ self.phasePatch n i → self.lower ≤ ‖(p.nativeTangent j n).normal (ParticularWaveBounds.nativePoint (p.geometry n) i x)‖
- normal_upper (n : ℕ) (i : TorusInverse.Frequency) (x : (Q × ℝ) × TorusInverse.Plane) : x ∈ (nativeStrip s).domain → x ∈ self.phasePatch n i → ‖(p.nativeTangent j n).normal (ParticularWaveBounds.nativePoint (p.geometry n) i x)‖ ≤ self.upper
- normal_match (n : ℕ) (i : TorusInverse.Frequency) (x : (Q × ℝ) × TorusInverse.Plane) : x ∈ (nativeStrip s).domain → x ∈ self.phasePatch n i → (p.copyData c u b G A j).background.normal (nativeStrip s) p.directions n x = (p.nativeTangent j n).normal (ParticularWaveBounds.nativePoint (p.geometry n) i x)
- inverse_frequency : WeightedClasses.BandBound (nativeStrip s) (1 / 2) fun (n : ℕ) => 1 / (p.copyData c u b G A j).background.frequency n
Instances For
The global amplitude, pressure, exact curl, and retained linear error are derived from native modal inputs for the same actual residual solve.
Angular and radial geometry of the actual raw copies. The analytic
bounds on the normal and material defect remain restricted to C.
- phase_smooth (n : ℕ) : ContDiffOn ℝ (↑⊤) (a.background.phase n) s.domain
- radial_radius (n : ℕ) (i : I) (x : D) : x ∈ s.domain → x ∈ C n i → HarmonicCalculus.along (d.radialField n) (a.background.radius n) x = 1
- radius (n : ℕ) : CopyAngularInvariance.Invariant d.angular (a.background.radius n)
- radial_base (n : ℕ) : CopyAngularInvariance.Invariant d.angular (a.background.radialBase n)
- frequency_base (n : ℕ) : CopyAngularInvariance.Invariant d.angular (a.background.frequencyBase n)
- axial_base (n : ℕ) : CopyAngularInvariance.Invariant d.angular (a.background.axialBase n)
- radial_field (n : ℕ) : CopyAngularInvariance.Invariant d.angular (d.radialField n)
- phase (n : ℕ) : ∃ (m : ℝ), CopyAngularInvariance.AffinePhase d.angular m (a.background.phase n)
Instances For
The generic local identity is applied only after the primitive raw principal equation has been proved by its actual ODE constructor.
Primitive angular identities and the fixed unit fundamental's ODE. The signed principal equation and every cutoff/curl identity are derived.
Slope of
NativeDynamics, of typeℕ → ℝ.- angular (i : I) : SignedWaveUpdate.AngularInputs (HarmonicWaveInteraction.productStrip s) p.directions p.base (p.matrix i) (p.target i) request (p.mask i) (p.fundamental i) (p.normalMotion i) (p.action i) (p.cutoff i) self.slope
- radial_radius (n : ℕ) (i : I) (x : D × ℝ) : x ∈ (HarmonicWaveInteraction.productStrip s).domain → x ∈ h.phasePatch n i → HarmonicCalculus.along (p.directions.radialField n) (p.base.radius n) x = 1
- matrix_frozen (i : I) : SignedWaveUpdate.FrozenAlong p.directions.fast (p.matrix i)
- target_frozen (i : I) : SignedWaveUpdate.FrozenAlong p.directions.fast (p.target i)
- request_frozen : SignedWaveUpdate.FrozenAlong p.directions.fast request
- mask_frozen (i : I) : SignedWaveUpdate.FrozenAlong p.directions.fast (p.mask i)
- ode (n : ℕ) (i : I) (x : D × ℝ) : x ∈ (HarmonicWaveInteraction.productStrip s).domain → x ∈ h.phasePatch n i → HarmonicCalculus.along (p.directions.fastField n) (p.fundamental i n) x = TangentProjection.projectedRhs (p.base.normal (HarmonicWaveInteraction.productStrip s) p.directions n x) (p.normalMotion i n x) (p.fundamental i n x) ((p.action i n x) (p.fundamental i n x)) 0 (s.epsilon n * p.base.frequency n ^ 2 * ‖p.base.normal (HarmonicWaveInteraction.productStrip s) p.directions n x‖ ^ 2)
- action_eq (n : ℕ) (i : I) (x : D × ℝ) : x ∈ (HarmonicWaveInteraction.productStrip s).domain → x ∈ h.phasePatch n i → CurlClassBounds.complexify ((p.action i n x) (p.fundamental i n x)) = LinearWaveResidual.shear (p.base.radius n) (p.base.frequencyBase n) (p.base.axialBase n) (p.directions.radialField n) (fun (y : D × ℝ) => CurlClassBounds.complexify (p.fundamental i n y)) x
Instances For
The literal signed common curl has its actual retained good term and Gaussian derivative tail on the entire lift. Native ODE input is needed only on the supported phase patches.
Native dynamics data, collecting background, open_patch, frequency_nonzero, damping,
fast, action.
- background : ParticularWaveAssembly.BackgroundControl (nativeStrip s) p.directions p.background b j
- damping (n : ℕ) (i : TorusInverse.Frequency) (x : (Q × ℝ) × TorusInverse.Plane) : x ∈ (nativeStrip s).domain → x ∈ h.phasePatch n i → (p.nativeTangent j n).damping (ParticularWaveBounds.nativePoint (p.geometry n) i x) = s.epsilon n * (↑j * b.frequency n) ^ 2 * ‖(p.copyData c u b G A j).background.normal (nativeStrip s) p.directions n x‖ ^ 2
- fast (n : ℕ) : p.directions.fastScale n • p.directions.fast = (0, ParticularWaveBounds.slotDirection (p.geometry n))
- action (n : ℕ) (i : TorusInverse.Frequency) (x : (Q × ℝ) × TorusInverse.Plane) : x ∈ (nativeStrip s).domain → x ∈ h.phasePatch n i → ∀ (z : ProblemStatement.Space), CurlClassBounds.complexify (((p.nativeTangent j n).action (ParticularWaveBounds.nativePoint (p.geometry n) i x)) z) = LinearWaveResidual.shear (p.background.radius n) (p.background.frequencyBase n) (p.background.axialBase n) (p.directions.radialField n) (fun (x : (Q × ℝ) × TorusInverse.Plane) => CurlClassBounds.complexify z) x
Instances For
The actual inhomogeneous common wave cancels the literal HR source on the whole lift, including the uncovered-source term in its Gaussian.
The periodized signed update satisfies the actual context linear operator, with the computed Gaussian term retained.
This is the literal HWI linear remainder of the constructed common signed block; its class follows from the native quotient and unit ODE.
The current residual is cancelled by the actual finite inverse. The remaining coefficient is precisely the computed retained-good block.
Axisymmetric alias: an abbreviation for ℕ → CyclePoint → Fin 3 → ℝ.
Equations
Instances For
Coefficient field, defined pointwise by (HarmonicFields.field (a n i) (b.frequency n) (b.phase n) (b.angularFrequency n) x).re.
Equations
- NavierStokes.CorrectionStep.coefficientField b a n x i = (NavierStokes.HarmonicFields.field (a n i) (b.frequency n) (b.phase n) (b.angularFrequency n) x).re
Instances For
The axisymmetric alias is kept separately from the spatial labels. No slot support is imposed on a zero angular mode.
- velocity (n : ℕ) (x : CyclePoint × ℝ) (i : Fin 3) : u.oscillation n x i = ∑ l ∈ v.labels n, (v.blocks l).oscillation n x i
- pressure (n : ℕ) (x : CyclePoint × ℝ) : u.oscillatoryPressure n x = ∑ l ∈ v.labels n, (v.blocks l).oscillatoryPressure n x
- aliasError (n : ℕ) (x : CyclePoint × ℝ) (i : Fin 3) : u.errors.aliasError n x i = ∑ l ∈ v.labels n, coefficientField (v.blocks l) (v.aliasCoefficients l) n x i + axis n x.1 i
Instances For
A common integer bound for stored coefficient values, including errors.
- velocityPressure (l : ι) : (v.blocks l).BandLimited v.residualBand
- aliasError (l : ι) (n : ℕ) (i : Fin 3) : HarmonicFields.BandLimited (v.aliasCoefficients l n i) v.residualBand
Instances For
The new nonzero harmonic data are literal sums of the old and constructed coefficients. All new mean aliases remain in the separate field.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Next axisymmetric alias as an element of AxisymmetricAlias.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The residual value bound of the next actual state is derived from stored coefficient bands, independently of a norm estimate.
The represented state and its literal coefficient data evolve together.
- state : CorrectionState.State CyclePoint
State of
CycleState, of typeState CyclePoint. - coefficients : CycleCoefficients ι
Coefficients of
CycleState, of typeCycleCoefficients ι. - axisymmetricAlias : AxisymmetricAlias
Axisymmetric alias of
CycleState, of typeAxisymmetricAlias.
Instances For
Step, bundling state, coefficients, axisymmetricAlias.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Iterate as an element of ℕ → CycleState ι | 0 => seed | n + 1 => (iterate p c seed n).step (p n) c.
Equations
- NavierStokes.CorrectionStep.CycleState.iterate p c seed 0 = seed
- NavierStokes.CorrectionStep.CycleState.iterate p c seed n.succ = NavierStokes.CorrectionStep.CycleState.step (p n) c (NavierStokes.CorrectionStep.CycleState.iterate p c seed n)
Instances For
Coefficient extraction preserves constants chosen before the spatial label. The identity concerns the actual linear field and retained Gaussian.
The exact nonlinear update preserves the joint label/band estimate. All three wave products and the support-local mean interaction are retained.
The unchanged oscillation retains a uniform residual estimate after an actual mean increment; pressure recomputation and axisymmetric aliases may change freely.
Before signed block, given by addBlock (v.blocks l) (p.particularBlock v c u l).
Equations
- p.beforeSignedBlock v c u l = NavierStokes.CorrectionStep.addBlock (v.blocks l) (p.particularBlock v c u l)
Instances For
Signed tangent, given by (p.signed l).tangentBlock p.strip (p.signedRequest v c u).
Equations
- p.signedTangent v c u l = (p.signed l).tangentBlock p.strip (p.signedRequest v c u)
Instances For
Signed curl, given by (p.signed l).curlBlock p.strip (p.signedRequest v c u).
Equations
- p.signedCurl v c u l = (p.signed l).curlBlock p.strip (p.signedRequest v c u)
Instances For
The family in the signed covariance identity is computed from the current cycle, including its actual particular increment and signed curl.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The actual native signed update supplies its pressure, cumulative, mean-residual, and measured-debt bounds from the same covariance.
Joint raw background, given by LocalizedWaveBounds.WaveFamily.ofCoefficients (fun j => {(a j.1).background with amplitude := 0, pressure := 0}).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Joint raw coefficients, given by LocalizedWaveBounds.WaveFamily.ofCoefficients (fun j => (a j.1).raw j.2).
Equations
- NavierStokes.CorrectionStep.jointRawCoefficients a = NavierStokes.LocalizedWaveBounds.WaveFamily.ofCoefficients fun (j : ι × I) => (a j.1).raw j.2
Instances For
The native solver estimates enter before summation over copies or
spatial labels. All bounds on the background remain local to C.
Literal stored coefficients inherit the joint estimates of the actual common solves, including the exact-minus-tangent curl.
Every target band uses the same chosen reference tangent, geometry, clock interval and cutoff. Only the current HR source is supplied at solve time.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Full-lift current-state coherence identifies the actual solved amplitude with the one reference physical wave, before taking a graph restriction.
The actual native signed update supplies its pressure, cumulative, mean-residual, and measured-debt bounds from the same covariance.
The two actual wave updates, temporal inverse, and rank solve form one mean/debt gain. All intermediate residual and flux regularity is derived from the original primitive fields and the actual covariance increments.
The actual two wave increments retain the cumulative bound and the difference from the fixed primary family, with constants before labels.
Apply the complete actual mean increment once to the stored harmonic residual. The pressure-alias refresh contributes only an angular zero mode.
Whole-fiber periodicity of the actual real oscillation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The actual good mean residual gains the requested exponent. New Gaussian means vanish exactly, and the new temporal alias is the same one retained by the mean-stage calculation.
One geometric choice is shared by all four literal stages.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The complete measured-mean gain for next. The signed family is
computed from this cycle's actual particular, tangent, and curl blocks;
its first covariance estimate is derived from the same finite labels.
Primitive regularity is propagated through the literal four-stage state. The rank geometry is reused from the incoming state; its new measured-debt smoothness is proved from the updated primitive fields.
Returning the actual mixed old/new block and its new Gaussian term commutes with the entire nonlinear residual, including all derivatives.
The stored coefficients themselves represent real fields. Retaining this algebraic invariant lets support of the real projection control the same coefficients used in the differentiated interaction estimates.
- velocity (l : ι) (n : ℕ) (i : Fin 3) : HarmonicFields.ConjugateSymmetric ((v.blocks l).velocity n i)
Instances For
The genuine input support controls raw nonzero coefficient germs because their real-projection identity is retained.
The quantitative and local regularity invariant is stated on the
actual stored fields of CycleState, including the independent alias.
Its definition makes no assertion that an arbitrary step preserves it.
- representation : CycleRepresentation x.coefficients x.state x.axisymmetricAlias
- bands : CoefficientBands x.coefficients
- realCoefficients : CycleRealCoefficients x.coefficients
- inputSupport (l : ι) : HarmonicSourceSupport.InputSupportOn G.domain (labelCarrier l) (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l)
- sourceBand (l : ι) : (HarmonicResidual.residualBlock c x.state (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l)).BandLimited x.coefficients.residualBand
- zeroVelocity (l : ι) : HarmonicWaveInteraction.ZeroMode (x.coefficients.blocks l)
- carrier (l : ι) : SameCarrier (x.coefficients.blocks l) (primary l)
- coefficientSmooth (l : ι) (n : ℕ) (i : Fin 3) : HarmonicResidual.SmoothCoefficients G.domain ((x.coefficients.blocks l).velocity n i)
- pressureCoefficientSmooth (l : ι) (n : ℕ) : HarmonicResidual.SmoothCoefficients G.domain ((x.coefficients.blocks l).pressure n)
- gaussianCoefficientSmooth (l : ι) (n : ℕ) (i : Fin 3) : HarmonicResidual.SmoothCoefficients G.domain (x.coefficients.gaussian l n i)
- solenoidal (l : ι) : HarmonicWaveInteraction.ModeSolenoidal G.strip c (x.coefficients.blocks l)
- wave (i : Fin 3) (j : ℤ) : LabelSumBounds.UniformWaveClass G.strip P (1 / 2) fun (l : ι) (n : ℕ) (z : SignedMeanGain.Point) => ((x.coefficients.blocks l).velocity n i).coeff j z
- pressure (j : ℤ) : LabelSumBounds.UniformWaveClass G.strip P 1 fun (l : ι) (n : ℕ) (z : SignedMeanGain.Point) => ((x.coefficients.blocks l).pressure n).coeff j z
- difference (i : Fin 3) (j : ℤ) : LabelSumBounds.UniformWaveClass G.strip P (17 / 25) fun (l : ι) (n : ℕ) (z : SignedMeanGain.Point) => ((x.coefficients.blocks l).velocity n i).coeff j z - ((primary l).velocity n i).coeff j z
- cumulative : CorrectionState.CumulativeBounds G.strip x.state
- covariance (i j : Fin 3) : WeightedClasses.MeanClass G.strip 1 (x.state.covariance i j)
- residual : UniformHarmonicInteraction.UniformVelocity G.strip P (1 / 2 + σ) fun (l : ι) => HarmonicResidual.residualBlock c x.state (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l)
- mean : CorrectionState.MeanResidualBounds G.strip σ c x.state
- meanHypotheses : LiftedMeanResidual.MeanHypotheses G.strip.domain c x.state
- debt : CorrectionState.DefectBounds G.slowStrip σ c x.state
- masses : GaugeMassPreservation.ZeroMassesOn G.region.carrier x.state
- oscillationSmooth : WaveStateRegularity.AngularSmooth G.domain x.state.oscillation
- oscillatoryPressureSmooth (n : ℕ) : ContDiffOn ℝ (↑⊤) (x.state.oscillatoryPressure n) (G.domain ×ˢ Set.univ)
- oscillationPeriodic : OscillationPeriodic G.region.carrier x.state.oscillation
- oscillationSupport : WaveStateRegularity.WaveSupport G.region G.patch.a G.patch.b x.state.oscillation
- gaussianFlat (β : ℝ) (i : Fin 3) (j : ℤ) : LabelSumBounds.UniformClass G.strip (fun (x : ι) (x_1 : ℕ) (z : SignedMeanGain.Point) => √(G.strip.zeta z)) β fun (l : ι) (n : ℕ) (z : SignedMeanGain.Point) => (x.coefficients.gaussian l n i).coeff j z
- axisFlat (β : ℝ) : WeightedClasses.MeanClass G.strip β x.axisymmetricAlias
Instances For
Raw residual classes required by the next signed request are derived from the good-mean invariant and the actual all-power axis alias.
The two constructed linear cancellations give the improved residual of the literal post-signed state, including both nonlinear wave updates. The linear estimates are the native equation/jet outputs, not estimates on either complete updated residual.
The actual full signed request is controlled by the current raw residuals. Their smoothness and support are derived from primitive state regularity and the actual pressure reconstruction.
The first actual wave supplies the current raw residuals and debt used by the signed request. No post-wave residual estimate is assumed.
Mean stages and the alias refresh leave the actual wave covariance unchanged. Both finite wave increments are retained in this identity.
The edge weight is retained in all new Gaussian coefficients.