The actual signed coefficients with only the dyadic factor removed

The matrix, target, current request, normalized pulse and pressure operator are unchanged. The spatial mask is replaced by its actual native grid factor. All estimates are on the original native control cells.

@[reducible, inline]

abbrev NavierStokes.ActualSignedUnmaskedBounds.Label (B N0 : ℕ) : Type

Label: an abbreviation for ActualSignedStageControls.SignedLabel B N0.

Equations

• NavierStokes.ActualSignedUnmaskedBounds.Label B N0 = NavierStokes.ActualSignedStageControls.SignedLabel B N0

@[reducible, inline]

abbrev NavierStokes.ActualSignedUnmaskedBounds.Full : Type

Full: an abbreviation for ActualSignedStageControls.FullPoint.

Equations

• NavierStokes.ActualSignedUnmaskedBounds.Full = NavierStokes.ActualSignedStageControls.FullPoint

@[reducible, inline]

abbrev NavierStokes.ActualSignedUnmaskedBounds.Copy : Type

Copy: an abbreviation for TorusInverse.Frequency.

Equations

• NavierStokes.ActualSignedUnmaskedBounds.Copy = NavierStokes.TorusInverse.Frequency

@[reducible, inline]

abbrev NavierStokes.ActualSignedUnmaskedBounds.CV : Type

CV: an abbreviation for CurlClassBounds.ComplexVector.

Equations

• NavierStokes.ActualSignedUnmaskedBounds.CV = NavierStokes.CurlClassBounds.ComplexVector

noncomputable def NavierStokes.ActualSignedUnmaskedBounds.gridMask {B N0 : ℕ} (l : Label B N0) (k : Copy) (n : ℕ) (x : Full) : ℝ

Grid mask, constructed using PrimaryRepresentatives.nativeMask.

Equations

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

noncomputable def NavierStokes.ActualSignedUnmaskedBounds.dyadicFactor {B N0 : ℕ} (l : Label B N0) (k : Copy) (n : ℕ) (x : Full) : ℝ

Dyadic factor, constructed using SquaredPartition.dyadicProfile.

Equations

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

theorem NavierStokes.ActualSignedUnmaskedBounds.mask_factor {B N0 : ℕ} (l : Label B N0) (k : Copy) (n : ℕ) (x : Full) : ActualSignedStageControls.mask l k n x = dyadicFactor l k n x * gridMask l k n x

noncomputable def NavierStokes.ActualSignedUnmaskedBounds.coefficients {B N0 : ℕ} (request : ℕ → Full → SignedWaveUpdate.Vec2) (l : Label B N0) (k : Copy) : LinearWaveBounds.WaveCoefficients Full

The actual signed solve, changing only its slow mask.

Equations

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

noncomputable def NavierStokes.ActualSignedUnmaskedBounds.amplitude {B N0 : ℕ} (request : ℕ → Full → SignedWaveUpdate.Vec2) (l : Label B N0) (k : Copy) (n : ℕ) (x : Full) : CV

Amplitude, given by cutoff l k n x • (coefficients request l k).amplitude n x.

Equations

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

noncomputable def NavierStokes.ActualSignedUnmaskedBounds.pressure {B N0 : ℕ} (request : ℕ → Full → SignedWaveUpdate.Vec2) (l : Label B N0) (k : Copy) (n : ℕ) (x : Full) : ℂ

Pressure, given by cutoff l k n x • (coefficients request l k).pressure n x.

Equations

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

noncomputable def NavierStokes.ActualSignedUnmaskedBounds.potential {B N0 : ℕ} (request : ℕ → Full → SignedWaveUpdate.Vec2) (l : Label B N0) (k : Copy) (n : ℕ) (x : Full) : CV

Potential, constructed using CurlClassBounds.inverseCarrier.

Equations

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

theorem NavierStokes.ActualSignedUnmaskedBounds.scalar_factor {B N0 : ℕ} (request : ℕ → Full → SignedWaveUpdate.Vec2) (l : Label B N0) (k : Copy) (n : ℕ) (x : Full) : SignedWaveUpdate.signedScalar ActualSignedStageControls.fullStrip (ActualSignedStageControls.matrix l k) (ActualSignedStageControls.target l k) request (ActualSignedStageControls.mask l k) l.2 n x = dyadicFactor l k n x * SignedWaveUpdate.signedScalar ActualSignedStageControls.fullStrip (ActualSignedStageControls.matrix l k) (ActualSignedStageControls.target l k) request (gridMask l k) l.2 n x

theorem NavierStokes.ActualSignedUnmaskedBounds.raw_amplitude_factor {B N0 : ℕ} (request : ℕ → Full → SignedWaveUpdate.Vec2) (l : Label B N0) (k : Copy) (n : ℕ) (x : Full) : (((ActualSignedStageControls.parameters l).copyData ActualPrimaryBounds.strip request).raw k).amplitude n x = dyadicFactor l k n x • (coefficients request l k).amplitude n x

theorem NavierStokes.ActualSignedUnmaskedBounds.raw_pressure_factor {B N0 : ℕ} (request : ℕ → Full → SignedWaveUpdate.Vec2) (l : Label B N0) (k : Copy) (n : ℕ) (x : Full) : (((ActualSignedStageControls.parameters l).copyData ActualPrimaryBounds.strip request).raw k).pressure n x = dyadicFactor l k n x • (coefficients request l k).pressure n x

theorem NavierStokes.ActualSignedUnmaskedBounds.amplitude_factor {B N0 : ℕ} (request : ℕ → Full → SignedWaveUpdate.Vec2) (l : Label B N0) (k : Copy) (n : ℕ) (x : Full) : (((ActualSignedStageControls.parameters l).copyData ActualPrimaryBounds.strip request).localized k).amplitude n x = dyadicFactor l k n x • amplitude request l k n x

The original once-localized velocity retains precisely one Gaussian.

theorem NavierStokes.ActualSignedUnmaskedBounds.pressure_factor {B N0 : ℕ} (request : ℕ → Full → SignedWaveUpdate.Vec2) (l : Label B N0) (k : Copy) (n : ℕ) (x : Full) : (((ActualSignedStageControls.parameters l).copyData ActualPrimaryBounds.strip request).localized k).pressure n x = dyadicFactor l k n x • pressure request l k n x

theorem NavierStokes.ActualSignedUnmaskedBounds.potential_factor {B N0 : ℕ} (request : ℕ → Full → SignedWaveUpdate.Vec2) (l : Label B N0) (k : Copy) (n : ℕ) (x : Full) : CurlClassBounds.inverseCarrier ((CorrectionInitialization.ActualPrimary.chartCoefficients l.2 l.1).frequency n) • CurlClassBounds.normalCoefficient ((CorrectionInitialization.ActualPrimary.chartCoefficients l.2 l.1).normal ActualSignedStageControls.fullStrip (ActualSignedStageControls.directions B) n x) ((((ActualSignedStageControls.parameters l).copyData ActualPrimaryBounds.strip request).localized k).amplitude n x) = dyadicFactor l k n x • potential request l k n x

theorem NavierStokes.ActualSignedUnmaskedBounds.grid_native_jets {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) : PhaseJetBounds.PolynomialJets (ActualSignedStageControls.slowJetDomain U).toDomain fun (l : ActualSignedStageControls.PulseLabel B N0) => PrimaryRepresentatives.nativeMask (BaseChartJets.cellBand l.2) (PrimaryGeometryAssembly.label CorrectionInitialization.ActualPrimary.nominal l.2).2

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

The native grid bound is independent of the dyadic profile, including all of its derivatives. Its constants precede labels and copies.

theorem NavierStokes.ActualSignedUnmaskedBounds.raw_jets {B N0 : ℕ} {β : ℝ} {request : ℕ → Full → 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) : (PeriodizedWaveBounds.UniformLocalJets ActualSignedStageControls.fullStrip (fun (l : Label B N0) (n : ℕ) (x : ActualSignedStageControls.FullPoint) => √(ActualSignedStageControls.fullStrip.zeta x) * ActualSignedStageControls.envelope l n x) (β + 1 / 2) ActualSignedStageControls.phaseCell fun (l : Label B N0) (n : ℕ) (k : ActualSignedStageControls.Frequency) => (coefficients request l k).amplitude n) ∧ PeriodizedWaveBounds.UniformLocalJets ActualSignedStageControls.fullStrip (fun (l : Label B N0) (n : ℕ) (x : ActualSignedStageControls.FullPoint) => √(ActualSignedStageControls.fullStrip.zeta x) * ActualSignedStageControls.envelope l n x) (β + 1) ActualSignedStageControls.phaseCell fun (l : Label B N0) (n : ℕ) (k : ActualSignedStageControls.Frequency) => (coefficients request l k).pressure n

Cramer's quotient and the actual normalized homogeneous pulse give the unmasked amplitude and pressure bounds; no output bound is an input.

theorem NavierStokes.ActualSignedUnmaskedBounds.localized_jets {B N0 : ℕ} {β : ℝ} {request : ℕ → Full → 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) : (PeriodizedWaveBounds.UniformLocalJets ActualSignedStageControls.fullStrip (fun (l : Label B N0) (n : ℕ) (x : ActualSignedStageControls.FullPoint) => √(ActualSignedStageControls.fullStrip.zeta x) * ActualSignedStageControls.envelope l n x) (β + 1 / 2) ActualSignedStageControls.phaseCell fun (l : Label B N0) (n : ℕ) (k : ActualSignedStageControls.Frequency) => amplitude request l k n) ∧ PeriodizedWaveBounds.UniformLocalJets ActualSignedStageControls.fullStrip (fun (l : Label B N0) (n : ℕ) (x : ActualSignedStageControls.FullPoint) => √(ActualSignedStageControls.fullStrip.zeta x) * ActualSignedStageControls.envelope l n x) (β + 1) ActualSignedStageControls.phaseCell fun (l : Label B N0) (n : ℕ) (k : ActualSignedStageControls.Frequency) => pressure request l k n

theorem NavierStokes.ActualSignedUnmaskedBounds.potential_jets {B N0 : ℕ} {β : ℝ} {request : ℕ → Full → 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) : PeriodizedWaveBounds.UniformLocalJets ActualSignedStageControls.fullStrip (fun (l : Label B N0) (n : ℕ) (x : ActualSignedStageControls.FullPoint) => √(ActualSignedStageControls.fullStrip.zeta x) * ActualSignedStageControls.envelope l n x) (β + 1) ActualSignedStageControls.phaseCell fun (l : Label B N0) (n : ℕ) (k : ActualSignedStageControls.Frequency) => potential request l k n

Removing the cutoff preserves the literal own-band zero germs

noncomputable def NavierStokes.ActualSignedUnmaskedBounds.reference {B N0 : ℕ} (l : Label B N0) : ℕ

Reference, given by BaseChartJets.cellBand l.1.

Equations

• NavierStokes.ActualSignedUnmaskedBounds.reference l = NavierStokes.BaseChartJets.cellBand l.1

theorem NavierStokes.ActualSignedUnmaskedBounds.dyadicFactor_reference {B N0 : ℕ} (l : Label B N0) (k : Copy) (x : Full) : dyadicFactor l k (reference l) x = SquaredPartition.dyadicProfile (SimilarityCoordinates.coordinateQ (2 * CorrectionInitialization.ActualPrimary.h) x.1.2.1)

theorem NavierStokes.ActualSignedUnmaskedBounds.dyadic_reference_nonzero {B N0 : ℕ} (l : Label B N0) (k : Copy) {x : Full} (hx : x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion) : dyadicFactor l k (reference l) x ≠ 0

theorem NavierStokes.ActualSignedUnmaskedBounds.dyadic_reference_nonzero_germ {B N0 : ℕ} (l : Label B N0) (k : Copy) {x : Full} (hx : x ∈ ActualSignedStageControls.fullStrip.domain) : ∀ᶠ (y : Full) in nhds x, dyadicFactor l k (reference l) y ≠ 0

theorem NavierStokes.ActualSignedUnmaskedBounds.own_phaseCell_or_zero {B N0 : ℕ} (request : ℕ → Full → SignedWaveUpdate.Vec2) (l : Label B N0) (k : Copy) {x : Full} (hx : x ∈ ActualSignedStageControls.fullStrip.domain) : x ∈ ActualSignedStageControls.phaseCell l (reference l) k ∨ (amplitude request l k (reference l) =ᶠ[nhds x] fun (x : Full) => 0) ∧ (pressure request l k (reference l) =ᶠ[nhds x] fun (x : Full) => 0) ∧ potential request l k (reference l) =ᶠ[nhds x] fun (x : Full) => 0

noncomputable def NavierStokes.ActualSignedUnmaskedBounds.ownField {B N0 : ℕ} {E : Type} [Zero E] (f : Label B N0 → Copy → ℕ → Full → E) (i : Label B N0 × Copy) (n : ℕ) (x : Full) : E

The band index is frozen only discretely, at the original label's own reference. This is not an extension of a fixed reference to all bands.

Equations

• NavierStokes.ActualSignedUnmaskedBounds.ownField f i n x = if n = NavierStokes.ActualSignedUnmaskedBounds.reference i.1 then f i.1 i.2 n x else 0

theorem NavierStokes.ActualSignedUnmaskedBounds.ownField_reference {B N0 : ℕ} {E : Type} [Zero E] (f : Label B N0 → Copy → ℕ → Full → E) (i : Label B N0 × Copy) : ownField f i (reference i.1) = f i.1 i.2 (reference i.1)

theorem NavierStokes.ActualSignedUnmaskedBounds.ownField_other {B N0 : ℕ} {E : Type} [Zero E] (f : Label B N0 → Copy → ℕ → Full → E) (i : Label B N0 × Copy) {n : ℕ} (hn : n ≠ reference i.1) : ownField f i n = fun (x : Full) => 0

theorem NavierStokes.ActualSignedUnmaskedBounds.ownField_uniform {B N0 : ℕ} {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : Label B N0 → Copy → ℕ → Full → E} {α : ℝ} {w : Label B N0 → ℕ → Full → ℝ} (hw : ∀ (l : Label B N0) (n : ℕ), ∀ x ∈ ActualSignedStageControls.fullStrip.domain, 0 ≤ w l n x) (hf : PeriodizedWaveBounds.UniformLocalJets ActualSignedStageControls.fullStrip w α ActualSignedStageControls.phaseCell fun (l : Label B N0) (n : ℕ) (k : ActualSignedStageControls.Frequency) => f l k n) (hc : ∀ (l : ActualSignedStageControls.SignedLabel B N0) (k : ActualSignedStageControls.Frequency), ∀ x ∈ ActualSignedStageControls.fullStrip.domain, x ∈ ActualSignedStageControls.phaseCell l (reference l) k ∨ f l k (reference l) =ᶠ[nhds x] fun (x : ActualSignedStageControls.FullPoint) => 0) : LabelSumBounds.UniformClass ActualSignedStageControls.fullStrip (fun (i : Label B N0 × Copy) => w i.1) α (ownField f)

theorem NavierStokes.ActualSignedUnmaskedBounds.own_potential_pressure_class {B N0 : ℕ} {β : ℝ} {request : ℕ → Full → 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) : LabelSumBounds.UniformClass ActualSignedStageControls.fullStrip (fun (i : Label B N0 × Copy) (n : ℕ) (x : ActualSignedStageControls.FullPoint) => √(ActualSignedStageControls.fullStrip.zeta x) * ActualSignedStageControls.envelope i.1 n x) (β + 1) (ownField (potential request)) ∧ LabelSumBounds.UniformClass ActualSignedStageControls.fullStrip (fun (i : Label B N0 × Copy) (n : ℕ) (x : ActualSignedStageControls.FullPoint) => √(ActualSignedStageControls.fullStrip.zeta x) * ActualSignedStageControls.envelope i.1 n x) (β + 1) (ownField (pressure request))

theorem NavierStokes.ActualSignedUnmaskedBounds.own_zero_outside {B N0 : ℕ} (request : ℕ → Full → SignedWaveUpdate.Vec2) (l : Label B N0) (k : Copy) {x : Full} (hx : x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion) (hout : ActualWaveRegularityData.radius x ∉ Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)) : amplitude request l k (reference l) x = 0 ∧ pressure request l k (reference l) x = 0 ∧ potential request l k (reference l) x = 0

theorem NavierStokes.ActualSignedUnmaskedBounds.ownFields_zero_outside {B N0 : ℕ} (request : ℕ → Full → SignedWaveUpdate.Vec2) (i : Label B N0 × Copy) (n : ℕ) {x : Full} (hx : x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion) (hout : ActualWaveRegularityData.radius x ∉ Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)) : ownField (amplitude request) i n x = 0 ∧ ownField (pressure request) i n x = 0 ∧ ownField (potential request) i n x = 0

The full-strip families supplied to radial continuation have literal zero values outside the original open radial interval, in every band.

The request is the measured current residual

theorem NavierStokes.ActualSignedUnmaskedBounds.actual_own_potential_pressure_class {B N0 : ℕ} (G : SignedMeanGain.Geometry) (hs : G.strip = ActualPrimaryBounds.strip) (c : CorrectionState.Context ActualSignedStageControls.Point) (u : CorrectionState.State ActualSignedStageControls.Point) (α : ℝ) (H : MeanStateRegularity.PrimitiveData G.region G.patch.a G.patch.b c u) (hfixed : VariableGaugeMean.reconstructState G.gauge c u = u) (hθ : WeightedClasses.MeanClass G.strip α (u.thetaResidual c)) (hz : WeightedClasses.MeanClass G.strip α (u.axialResidual c)) : have request := LocalSignedRequest.fullRequest G.strip G.patch G.coord c u; LabelSumBounds.UniformClass ActualSignedStageControls.fullStrip (fun (i : Label B N0 × Copy) (n : ℕ) (x : ActualSignedStageControls.FullPoint) => √(ActualSignedStageControls.fullStrip.zeta x) * ActualSignedStageControls.envelope i.1 n x) α (ownField (potential request)) ∧ LabelSumBounds.UniformClass ActualSignedStageControls.fullStrip (fun (i : Label B N0 × Copy) (n : ℕ) (x : ActualSignedStageControls.FullPoint) => √(ActualSignedStageControls.fullStrip.zeta x) * ActualSignedStageControls.envelope i.1 n x) α (ownField (pressure request))

The actual residual-to-request construction supplies the unmasked potential and pressure estimates. No bound for either output is assumed.

theorem NavierStokes.ActualSignedUnmaskedBounds.invariant_own_potential_pressure_class {B N0 : ℕ} {ι : Type} (G : SignedMeanGain.Geometry) (hs : G.strip = ActualPrimaryBounds.strip) (c : CorrectionState.Context ActualSignedStageControls.Point) (primary : ι → CorrectionState.HarmonicBlock ActualSignedStageControls.Point) (P : ι → ℕ → ActualSignedStageControls.Point → ℝ) (labelCarrier : ι → ℕ → Set ActualSignedStageControls.Point) (σ : ℝ) (u : CorrectionStep.CycleState ι) (H : CorrectionStep.CycleAnalyticInvariant G c primary P labelCarrier σ u) : have request := LocalSignedRequest.fullRequest G.strip G.patch G.coord c u.state; LabelSumBounds.UniformClass ActualSignedStageControls.fullStrip (fun (i : Label B N0 × Copy) (n : ℕ) (x : ActualSignedStageControls.FullPoint) => √(ActualSignedStageControls.fullStrip.zeta x) * ActualSignedStageControls.envelope i.1 n x) (1 + σ) (ownField (potential request)) ∧ LabelSumBounds.UniformClass ActualSignedStageControls.fullStrip (fun (i : Label B N0 × Copy) (n : ℕ) (x : ActualSignedStageControls.FullPoint) => √(ActualSignedStageControls.fullStrip.zeta x) * ActualSignedStageControls.envelope i.1 n x) (1 + σ) (ownField (pressure request))

In particular the literal reconstructed cycle invariant is sufficient; the only analytic output used is its already measured residual class.