Preservation by the actual correction cycle #
The fixed parameters, current residual, signed request, and comparison primary are those of the existing initialization. The concrete wave constructions supply the inputs to the generic analytic step.
The actual signed mean cross and its physical scale #
The fixed comparison primary is the actual tangent block, and every signed
coefficient uses the same selected matrix, pulse and once-applied cutoff.
The physical partition scale is Q n * q_normalized; finite low bands retain
their partition factor.
Frequency: an abbreviation for TorusInverse.Frequency /-! ## The legacy normalized-tail input cannot describe this chart -/.
Instances For
The legacy normalized-tail input cannot describe this chart #
Shared matrix, scaled target and ratio of the signed coefficients #
Velocity scale, given by PhysicalParticularWave.velocityWeight h (ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand L)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Common matrix, given by covariance B N0 L (nativePoint n x L).
Equations
Instances For
Reference target, defined pointwise by PrimaryTargetBounds.actualTarget modulation (nativePoint n x L) i.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Common target, given by (ActualSignedStageControls.coefficientScale (L, (0 : Fin 2)) n) ^ 2 • referenceTarget L n x.
Equations
Instances For
Signed ratio, constructed using SignedCovariance.increment.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The actual once-cutoff coefficients #
Individual primary modes at the actual common cover #
The literal requested field and its finite covariance sum #
Actual request, constructed using LocalSignedRequest.fullRequest.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Actual signed block, given by (ActualSignedStageControls.parameters l).tangentBlock ActualInitialization.geometry.strip (actualRequest c u).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Actual primary field, given by LabelSumBounds.fieldSum (activeLabels standardRegion B N0) (fun l => (ActualInitialization.tangentBlock l).oscillation).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Actual signed field, given by LabelSumBounds.fieldSum (activeLabels standardRegion B N0) (fun l => (actualSignedBlock c u l).oscillation).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Actual cross, given by LabelSumBounds.symmetricCovariance (actualPrimaryField B N0) (actualSignedField B N0 c u).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Exact physical partition factor, and exact cancellation on its tail #
The physical scale, and therefore this threshold, is shared by every signed request made from the fixed primary choice.
Earlier bands retain their actual cutoff deficit. In particular this theorem makes no assertion of cancellation on every normalized band.
Binding to the signed family of the literal correction cycle #
This is the actual cycle constructor with its particular solver left as a parameter. Both fixed and state-dependent actual particular solvers use this very signed subsystem.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The cycle field identity is stated without expanding its quantitative
SignedFamily proof object. Its coefficient projections are all that the
covariance uses.
Only stored coefficient projections identify the quantitative family.
For the literal CycleParameters.signedFamily, these equalities are rfl.
Every requested exponent follows for the literal finite-head defects. The analytic inputs are the usual supported residual/coefficient estimates, not an assumption on the cross defect or its vanishing.
Gaussian cutoff errors of the actual signed correction #
The transverse cutoff and the Gaussian cutoff remain in the literal native cutoff. The transverse factor has zero fast derivative. Thus the actual error vanishes on the central Gaussian plateau and retains the exact square-root edge weight at every decay exponent.
Copies, given by (parameters l).copyData ActualPrimaryBounds.strip request.
Equations
Instances For
Local gaussian, given by (copies request l).localGaussian (directions B) n k.
Equations
- NavierStokes.ActualSignedGaussian.localGaussian request l n k = (NavierStokes.ActualSignedGaussian.copies request l).localGaussian (NavierStokes.ActualSignedStageControls.directions B) n k
Instances For
Transverse, given by PartitionedCovariance.cutoff ActualPrimary.slots.radius (nativePoint l n k x).2.1.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Only the native clock changes along the fast direction.
The product cutoff is differentiated literally. The transverse derivative term vanishes; no cutoff factor is silently moved into the mask.
The central Gaussian plateau kills the actual error even when the transverse cutoff is strictly between zero and one.
Band scales, bundling power, epsilon_eq, boundConstant, constant_one_le and the
required compatibility proofs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Uniform Gaussian absorption with the edge weight retained #
All joint jets of the literal local Gaussian error have every epsilon exponent, with exactly the square-root edge weight.
Global gaussian, given by (copies request l).globalGaussian (directions B).
Equations
Instances For
The actual periodized Gaussian coefficient, including its source complement, has the exact weighted class. The signed source is identically zero.
This is the precise Fourier-coefficient class required by the signed
Gaussian field of CorrectionAnalyticStep.WaveData.
Actual current residuals and primitive identities supply the request jet premise; no signed Gaussian output estimate is an input.
Measured debt before the actual rank correction #
The first-wave debt, the signed covariance change, and the temporal mean change are evaluated on the literal intermediate states. No estimate of the post-temporal debt is supplied as a premise.
Signed velocity: an abbreviation for (ActualCycleParameters.fixedParameters B N0).signedVelocity x.coefficients (ActualPrimary.commonContext B) x.state.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Signed pressure: an abbreviation for (ActualCycleParameters.fixedParameters B N0).signedPressure x.coefficients (ActualPrimary.commonContext B) x.state.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Signed gaussian: an abbreviation for (ActualCycleParameters.fixedParameters B N0).signedGaussian x.coefficients (ActualPrimary.commonContext B) x.state.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Post signed: an abbreviation for (ActualCycleParameters.fixedParameters B N0).afterSigned x.coefficients (ActualPrimary.commonContext B) x.state.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Temporal increment: an abbreviation for (ActualCycleParameters.fixedParameters B N0).temporalIncrement x.coefficients (ActualPrimary.commonContext B) x.state.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Post temporal: an abbreviation for (ActualCycleParameters.fixedParameters B N0).afterTemporal x.coefficients (ActualPrimary.commonContext B) x.state.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Both intermediate debts are measured from the actual state. The signed stage loses one operator exponent, while the temporal change retains the exponent of its genuine mean increment.
Concrete factory-facing form. Both covariance and temporal estimates are derived from the checked step data, and the initial intermediate debt is derived from the particular inputs.
The full three-component slow source used by the actual rank repair.
Index: an abbreviation for ActualInitialization.Index local notation "G" => ActualInitialization.geometry local notation "κ" => ChartScales.kappa.
Instances For
One fixed similarity geometry and the actual base/rank parameters work at every correction stage.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Debt regularity comes from the current primitive invariant; the reserved pure-power base model is the already proved actual base.
The actual label set is unchanged by every correction.
State, constructed using CycleState.iterate.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The fixed comparison primary is the original finite tangent field.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A true source core with its native dyadic restriction lies in the existing quantitative control cell on the evaluation strip.
Restrict a local estimate only on the actual evaluation domain.
The cycle keeps the actual closed radial and native dyadic cores.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Existing estimates stated on the broad carrier apply by inclusion; the stronger support is still retained by the cycle invariant.
The strengthened support is already proved for the literal initial state.
Every supported label belongs to the literal finite sum in that band, including at the two closed radial edges.
Step data of waves used in actual cycle preservation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
In a band with no compatible common cover, the actual incoming source has a zero germ throughout the complete slow cylinder.
Native particular data used in actual cycle preservation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Step data of particular, given by stepDataOfWaves H hN hσ hl (waveData_of_particular H hN hσ P).
Equations
- NavierStokes.ActualCyclePreservation.stepDataOfParticular H hN hσ hl P = NavierStokes.ActualCyclePreservation.stepDataOfWaves H hN hσ hl ⋯
Instances For
The actual run retains analytic bounds, full chart coherence, and individual torus periods as distinct, proved invariants.
- analytic : Invariant σ x
- coherent : ActualCycleCoherence.Coherent x
- periodic : ActualCyclePeriodicity.Periodic x
Instances For
Every stage belongs to the same fixed construction, with no wave, regularity, covariance, or periodicity output supplied as an assumption.
State step data, constructed using stepDataOfParticular.