Physical wave data for the actual signed cycle fields

The native family is the family in ActualSignedExterior. Geometry, profiles and native source bounds are assembled before any physical estimate is applied.

Joint native bounds for the actual signed physical sources

The sources are the literal masked sources of the canonical dependent family. Bounds are uniform before selecting an outer label, a harmonic, a band, or a lattice copy. No physical derivative estimate is assumed.

@[reducible, inline]

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

Label: an abbreviation for ActualSignedPhysicalBinding.Label.

Equations

• NavierStokes.ActualSignedNativeBounds.Label = NavierStokes.ActualSignedPhysicalBinding.Label

@[reducible, inline]

abbrev NavierStokes.ActualSignedNativeBounds.Native : Type

Native: an abbreviation for ActualSignedPhysicalData.Native.

Equations

• NavierStokes.ActualSignedNativeBounds.Native = NavierStokes.ActualSignedPhysicalData.Native

@[reducible, inline]

abbrev NavierStokes.ActualSignedNativeBounds.Full : Type

Full: an abbreviation for ActualSignedStageControls.FullPoint.

Equations

• NavierStokes.ActualSignedNativeBounds.Full = NavierStokes.ActualSignedStageControls.FullPoint

@[reducible, inline]

abbrev NavierStokes.ActualSignedNativeBounds.Copy : Type

Copy: an abbreviation for TorusInverse.Frequency.

Equations

• NavierStokes.ActualSignedNativeBounds.Copy = NavierStokes.TorusInverse.Frequency

@[reducible, inline]

abbrev NavierStokes.ActualSignedNativeBounds.SourceIndex : Type

Source index: an abbreviation for Σ (_ : PhysicalWaveSum.BandLabel), ActualSignedPhysicalData.SourceIndex.

Equations

• NavierStokes.ActualSignedNativeBounds.SourceIndex = ((_ : NavierStokes.PhysicalWaveSum.BandLabel) × NavierStokes.ActualSignedPhysicalData.SourceIndex)

noncomputable def NavierStokes.ActualSignedNativeBounds.family {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State LocalSignedRequest.Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) : DependentSignedPhysicalFamily.Family

Family, given by ActualSignedExterior.family (fun l : Label B N0 => ActualSignedPhysicalBinding.nativeStateData l P u H hp).

Equations

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

noncomputable def NavierStokes.ActualSignedNativeBounds.potentialSource {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State LocalSignedRequest.Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) : SourceIndex → ℕ → Native → HarmonicCalculus.ComplexVector

Potential source, given by DependentSignedPhysicalFamily.jointSource ((family (N0 := N0) P u H hp).potentialSource slots outgoing.data.h_pos.le).

Equations

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

noncomputable def NavierStokes.ActualSignedNativeBounds.pressureSource {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State LocalSignedRequest.Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) : SourceIndex → ℕ → Native → ℂ

Pressure source, given by DependentSignedPhysicalFamily.jointSource ((family (N0 := N0) P u H hp).pressureSource slots outgoing.data.h_pos.le).

Equations

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

noncomputable def NavierStokes.ActualSignedNativeBounds.weight : SourceIndex → ℕ → (y : Native) → ℝ

Weight, given by Real.sqrt (ActualPrimaryBounds.strip.zeta y) /-! ## The reference pullback is a contraction on the free coordinates -/.

Equations

• NavierStokes.ActualSignedNativeBounds.weight x✝¹ x✝ y = √(NavierStokes.ActualPrimaryBounds.strip.zeta y)

The reference pullback is a contraction on the free coordinates

theorem NavierStokes.ActualSignedNativeBounds.norm_coverEquiv_symm_le (y : TorusInverse.Plane) : ‖CommonCoverSolve.coverEquiv.symm y‖ ≤ ‖y‖

theorem NavierStokes.ActualSignedNativeBounds.norm_coverPower_symm_le (d : ℕ) (y : TorusInverse.Plane) : ‖(CommonCoverSolve.coverPower d).symm y‖ ≤ ‖y‖

noncomputable def NavierStokes.ActualSignedNativeBounds.nativeToCommon {B N0 : ℕ} (l : Label B N0) : Native →L[ℝ] Full

Native to common as an element of Native →L[ℝ] Full.

Equations

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

theorem NavierStokes.ActualSignedNativeBounds.nativeToCommon_eq {B N0 : ℕ} (l : Label B N0) (y : Native) : (nativeToCommon l) y = (ActualSignedPhysicalBinding.toCommonCylinder l) (ActualSignedPhysicalData.nativeCylinder y)

theorem NavierStokes.ActualSignedNativeBounds.nativeToCommon_apply {B N0 : ℕ} (l : Label B N0) (y : Native) : (nativeToCommon l) y = ((y.1, y.2.1, (CommonCoverSolve.coverPower (ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (ActualSignedPhysicalBinding.reference l) - CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h (ActualSignedPhysicalBinding.reference l))).symm y.2.2), 0)

theorem NavierStokes.ActualSignedNativeBounds.norm_nativeToCommon_le {B N0 : ℕ} (l : Label B N0) : ‖nativeToCommon l‖ ≤ 1

theorem NavierStokes.ActualSignedNativeBounds.nativeToCommon_mem {B N0 : ℕ} (l : Label B N0) {y : Native} (hy : y ∈ ActualPrimaryBounds.strip.domain) : (nativeToCommon l) y ∈ ActualSignedStageControls.fullStrip.domain

theorem NavierStokes.ActualSignedNativeBounds.nativeToCommon_majorant {B N0 : ℕ} (l : Label B N0) (α C : ℝ) (p n : ℕ) (y : Native) : WeightedClasses.majorant ActualSignedStageControls.fullStrip (fun (x : ℕ) (x_1 : ActualSignedStageControls.FullPoint) => √(ActualSignedStageControls.fullStrip.zeta x_1)) α C p n ((nativeToCommon l) y) = WeightedClasses.majorant ActualPrimaryBounds.strip (fun (x : ℕ) (x_1 : ActualPrimaryBounds.Point) => √(ActualPrimaryBounds.strip.zeta x_1)) α C p n y

theorem NavierStokes.ActualSignedNativeBounds.uniform_nativeToCommon {B N0 : ℕ} {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {α : ℝ} {f : Label B N0 × Copy → ℕ → Full → E} (hf : LabelSumBounds.UniformClass ActualSignedStageControls.fullStrip (fun (x : Label B N0 × Copy) (x_1 : ℕ) (x_2 : ActualSignedStageControls.FullPoint) => √(ActualSignedStageControls.fullStrip.zeta x_2)) α f) : LabelSumBounds.UniformClass ActualPrimaryBounds.strip (fun (x : Label B N0 × Copy) (x_1 : ℕ) (y : ActualPrimaryBounds.Point) => √(ActualPrimaryBounds.strip.zeta y)) α fun (i : Label B N0 × Copy) (n : ℕ) (y : ActualPrimaryBounds.Point) => f i n ((nativeToCommon i.1) y)

The masked native coefficients on their complete own-band strip

noncomputable def NavierStokes.ActualSignedNativeBounds.ownPotential {B N0 : ℕ} (request : ℕ → Full → SignedWaveUpdate.Vec2) : Label B N0 × Copy → ℕ → Full → HarmonicCalculus.ComplexVector

Own potential, given by ActualSignedUnmaskedBounds.ownField (fun l k n => ActualSignedOutputBounds.localPotential request l n k).

Equations

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

noncomputable def NavierStokes.ActualSignedNativeBounds.ownPressure {B N0 : ℕ} (request : ℕ → Full → SignedWaveUpdate.Vec2) : Label B N0 × Copy → ℕ → Full → ℂ

Own pressure, given by ActualSignedUnmaskedBounds.ownField (fun l k n => ((ActualSignedOutputBounds.copies request l).localized k).pressure n).

Equations

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

theorem NavierStokes.ActualSignedNativeBounds.localPotential_zero_germ {B N0 : ℕ} (request : ℕ → Full → SignedWaveUpdate.Vec2) (l : Label B N0) (n : ℕ) (k : Copy) {x : Full} (ha : ((ActualSignedOutputBounds.copies request l).localized k).amplitude n =ᶠ[nhds x] fun (x : Full) => 0) : ActualSignedOutputBounds.localPotential request l n k =ᶠ[nhds x] fun (x : Full) => 0

theorem NavierStokes.ActualSignedNativeBounds.own_potential_pressure_uniform {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 (x : Label B N0 × Copy) (x_1 : ℕ) (x_2 : ActualSignedStageControls.FullPoint) => √(ActualSignedStageControls.fullStrip.zeta x_2)) (β + 1) (ownPotential request) ∧ LabelSumBounds.UniformClass ActualSignedStageControls.fullStrip (fun (x : Label B N0 × Copy) (x_1 : ℕ) (x_2 : ActualSignedStageControls.FullPoint) => √(ActualSignedStageControls.fullStrip.zeta x_2)) (β + 1) (ownPressure request)

noncomputable def NavierStokes.ActualSignedNativeBounds.request {B : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State LocalSignedRequest.Point) : ℕ → Full → SignedWaveUpdate.Vec2

Request, given by LocalSignedRequest.fullRequest ActualPrimaryBounds.strip P (2 * h) (commonContext B) u.

Equations

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

noncomputable def NavierStokes.ActualSignedNativeBounds.nativePotentialCoefficient {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State LocalSignedRequest.Point) (k : Copy) (z : ActualSignedPhysicalBinding.Cylinder) : HarmonicCalculus.ComplexVector

Native potential coefficient, constructed using ActualSignedPhysicalData.potentialMap.

Equations

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

noncomputable def NavierStokes.ActualSignedNativeBounds.nativePressureCoefficient {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State LocalSignedRequest.Point) (k : Copy) (z : ActualSignedPhysicalBinding.Cylinder) : ℂ

Native pressure coefficient, given by ((ActualSignedPhysicalBinding.nativeCopies l P u).localized k).pressure (ActualSignedPhysicalBinding.reference l) z.

Equations

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

theorem NavierStokes.ActualSignedNativeBounds.native_cutoff {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State LocalSignedRequest.Point) (n : ℕ) (k : Copy) (z : ActualSignedPhysicalBinding.Cylinder) : (ActualSignedPhysicalBinding.nativeCopies l P u).cutoff n k z = ActualSignedPhysicalData.waveMask CorrectionInitialization.ActualPrimary.slots (ActualSignedPhysicalBinding.spatialLabel l) ((ActualSignedPhysicalBinding.geometry l).coordinates k z.1.2.2)

theorem NavierStokes.ActualSignedNativeBounds.native_raw_amplitude {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State LocalSignedRequest.Point) (k : Copy) (z : ActualSignedPhysicalBinding.Cylinder) : (ActualSignedPhysicalBinding.nativeCopies l P u).amplitude (ActualSignedPhysicalBinding.reference l) k z = ActualPeriodizedSignedRealization.referenceScalar (ActualSignedPhysicalBinding.primary l) (ActualSignedPhysicalBinding.nativeRequest l P u) l.2 (ActualSignedPhysicalBinding.reference l) z • CurlClassBounds.complexify (ActualPeriodizedSignedRealization.referenceNativeUnit (ActualSignedPhysicalBinding.primary l) (ActualSignedPhysicalBinding.layout l) l.2 (ActualSignedPhysicalBinding.reference l) k z)

theorem NavierStokes.ActualSignedNativeBounds.native_raw_pressure {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State LocalSignedRequest.Point) (k : Copy) (z : ActualSignedPhysicalBinding.Cylinder) : (ActualSignedPhysicalBinding.nativeCopies l P u).pressure (ActualSignedPhysicalBinding.reference l) k z = ActualPeriodizedSignedRealization.referenceScalar (ActualSignedPhysicalBinding.primary l) (ActualSignedPhysicalBinding.nativeRequest l P u) l.2 (ActualSignedPhysicalBinding.reference l) z • ActualPeriodizedSignedRealization.homogeneousPressure ((ActualSignedPhysicalBinding.primary l).base.frequency (ActualSignedPhysicalBinding.reference l)) ((ActualSignedPhysicalBinding.primary l).base.normal (ActualSignedPhysicalBinding.primary l).strip (ActualSignedPhysicalBinding.primary l).directions (ActualSignedPhysicalBinding.reference l) z) ((ActualSignedPhysicalBinding.primary l).normalMotion (ActualSignedPhysicalBinding.reference l) z) ((ActualSignedPhysicalBinding.primary l).action (ActualSignedPhysicalBinding.reference l) z) (ActualPeriodizedSignedRealization.referenceNativeUnit (ActualSignedPhysicalBinding.primary l) (ActualSignedPhysicalBinding.layout l) l.2 (ActualSignedPhysicalBinding.reference l) k z)

theorem NavierStokes.ActualSignedNativeBounds.localPotential_reference {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State LocalSignedRequest.Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (k : Copy) (z : ActualSignedPhysicalBinding.Cylinder) : ActualSignedOutputBounds.localPotential (request P u) l (ActualSignedPhysicalBinding.reference l) k ((ActualSignedPhysicalBinding.toCommonCylinder l) z) = nativePotentialCoefficient l P u k z

theorem NavierStokes.ActualSignedNativeBounds.localPressure_reference {B N0 : ℕ} (l : Label B N0) (P : SignedStressPrimitive.Patch) (u : CorrectionState.State LocalSignedRequest.Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (k : Copy) (z : ActualSignedPhysicalBinding.Cylinder) : ((ActualSignedOutputBounds.copies (request P u) l).localized k).pressure (ActualSignedPhysicalBinding.reference l) ((ActualSignedPhysicalBinding.toCommonCylinder l) z) = nativePressureCoefficient l P u k z

theorem NavierStokes.ActualSignedNativeBounds.singleton_referenceRequest {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State LocalSignedRequest.Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (l : Label B N0) : (((family P u H hp).singleton (ActualSignedExterior.nativeLabel l)).state ((family P u H hp).singletonLabel (ActualSignedExterior.nativeLabel l))).referenceRequest = ActualSignedPhysicalBinding.nativeRequest l P u

theorem NavierStokes.ActualSignedNativeBounds.singleton_rawPotential {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State LocalSignedRequest.Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (l : Label B N0) (k : Copy) (z : ActualSignedPhysicalBinding.Cylinder) : ActualSignedPhysicalData.rawPotential CorrectionInitialization.ActualPrimary.slots ⋯ ((family P u H hp).singleton (ActualSignedExterior.nativeLabel l)) ((family P u H hp).singletonLabel (ActualSignedExterior.nativeLabel l)) k z = (ActualSignedPhysicalData.potentialMap ((ActualSignedPhysicalBinding.primary l).base.frequency (ActualSignedPhysicalBinding.reference l)) ((ActualSignedPhysicalBinding.primary l).base.normal (ActualSignedPhysicalBinding.primary l).strip (ActualSignedPhysicalBinding.primary l).directions (ActualSignedPhysicalBinding.reference l) z)) ((ActualSignedPhysicalBinding.nativeCopies l P u).amplitude (ActualSignedPhysicalBinding.reference l) k z)

theorem NavierStokes.ActualSignedNativeBounds.singleton_rawPressure {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State LocalSignedRequest.Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (l : Label B N0) (k : Copy) (z : ActualSignedPhysicalBinding.Cylinder) : ActualSignedPhysicalData.rawPressure CorrectionInitialization.ActualPrimary.slots ⋯ ((family P u H hp).singleton (ActualSignedExterior.nativeLabel l)) ((family P u H hp).singletonLabel (ActualSignedExterior.nativeLabel l)) k z = (ActualSignedPhysicalBinding.nativeCopies l P u).pressure (ActualSignedPhysicalBinding.reference l) k z

theorem NavierStokes.ActualSignedNativeBounds.nativePotentialCoefficient_eq {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State LocalSignedRequest.Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (l : Label B N0) (k : Copy) (z : ActualSignedPhysicalBinding.Cylinder) : nativePotentialCoefficient l P u k z = ActualSignedPhysicalData.waveMask CorrectionInitialization.ActualPrimary.slots (ActualSignedPhysicalBinding.spatialLabel l) ((ActualSignedPhysicalBinding.geometry l).coordinates k z.1.2.2) • ActualSignedPhysicalData.rawPotential CorrectionInitialization.ActualPrimary.slots ⋯ ((family P u H hp).singleton (ActualSignedExterior.nativeLabel l)) ((family P u H hp).singletonLabel (ActualSignedExterior.nativeLabel l)) k z

theorem NavierStokes.ActualSignedNativeBounds.nativePressureCoefficient_eq {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State LocalSignedRequest.Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (l : Label B N0) (k : Copy) (z : ActualSignedPhysicalBinding.Cylinder) : nativePressureCoefficient l P u k z = ActualSignedPhysicalData.waveMask CorrectionInitialization.ActualPrimary.slots (ActualSignedPhysicalBinding.spatialLabel l) ((ActualSignedPhysicalBinding.geometry l).coordinates k z.1.2.2) • ActualSignedPhysicalData.rawPressure CorrectionInitialization.ActualPrimary.slots ⋯ ((family P u H hp).singleton (ActualSignedExterior.nativeLabel l)) ((family P u H hp).singletonLabel (ActualSignedExterior.nativeLabel l)) k z

theorem NavierStokes.ActualSignedNativeBounds.potentialSource_on_label {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State LocalSignedRequest.Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (l : Label B N0) (j : PhysicalWaveSum.Harmonic 1) (k : Copy) (n : ℕ) (y : Native) : potentialSource P u H hp ⟨ActualSignedExterior.bandLabel l, ((ActualSignedExterior.bandLabel l, j), k)⟩ n y = if ↑j = 1 ∧ n = ActualSignedPhysicalBinding.reference l then nativePotentialCoefficient l P u k (ActualSignedPhysicalData.nativeCylinder y) else 0

theorem NavierStokes.ActualSignedNativeBounds.pressureSource_on_label {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State LocalSignedRequest.Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (l : Label B N0) (j : PhysicalWaveSum.Harmonic 1) (k : Copy) (n : ℕ) (y : Native) : pressureSource P u H hp ⟨ActualSignedExterior.bandLabel l, ((ActualSignedExterior.bandLabel l, j), k)⟩ n y = if ↑j = 1 ∧ n = ActualSignedPhysicalBinding.reference l then nativePressureCoefficient l P u k (ActualSignedPhysicalData.nativeCylinder y) else 0

Joint selection, with literal zeros at every omitted index

noncomputable def NavierStokes.ActualSignedNativeBounds.selection {B N0 : ℕ} {E : Type u_1} [Zero E] (g : Label B N0 × Copy → ℕ → Native → E) (I : SourceIndex) (n : ℕ) (y : Native) : E

Selection as an element of E.

Equations

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

theorem NavierStokes.ActualSignedNativeBounds.selection_on_label {B N0 : ℕ} {E : Type u_1} [Zero E] (g : Label B N0 × Copy → ℕ → Native → E) (l : Label B N0) (j : PhysicalWaveSum.Harmonic 1) (k : Copy) (n : ℕ) (y : Native) : selection g ⟨ActualSignedExterior.bandLabel l, ((ActualSignedExterior.bandLabel l, j), k)⟩ n y = if ↑j = 1 then g (l, k) n y else 0

theorem NavierStokes.ActualSignedNativeBounds.selection_inactive {B N0 : ℕ} {E : Type u_1} [Zero E] (g : Label B N0 × Copy → ℕ → Native → E) (L : PhysicalWaveSum.BandLabel) (I : ActualSignedPhysicalData.SourceIndex) (n : ℕ) (y : Native) (hL : L ∉ ActualSignedExterior.labels B N0) : selection g ⟨L, I⟩ n y = 0

theorem NavierStokes.ActualSignedNativeBounds.selection_other_label {B N0 : ℕ} {E : Type u_1} [Zero E] (g : Label B N0 × Copy → ℕ → Native → E) (L : PhysicalWaveSum.BandLabel) (I : ActualSignedPhysicalData.SourceIndex) (n : ℕ) (y : Native) (hI : I.1.1 ≠ L) : selection g ⟨L, I⟩ n y = 0

theorem NavierStokes.ActualSignedNativeBounds.selection_active_function {B N0 : ℕ} {E : Type u_1} [Zero E] (g : Label B N0 × Copy → ℕ → Native → E) (I : SourceIndex) (n : ℕ) (hL : I.fst ∈ ActualSignedExterior.labels B N0) (hI : I.snd.1.1 = I.fst ∧ ↑I.snd.1.2 = 1) : selection g I n = g (ActualSignedExterior.actualLabel { val := ↑I.fst, property := ⋯, mem := hL }, I.snd.2) n

theorem NavierStokes.ActualSignedNativeBounds.selection_zero_function {B N0 : ℕ} {E : Type u_1} [Zero E] (g : Label B N0 × Copy → ℕ → Native → E) (I : SourceIndex) (n : ℕ) (hz : I.fst ∉ ActualSignedExterior.labels B N0 ∨ ¬(I.snd.1.1 = I.fst ∧ ↑I.snd.1.2 = 1)) : selection g I n = fun (x : Native) => 0

theorem NavierStokes.ActualSignedNativeBounds.selection_uniform {B N0 : ℕ} {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {α : ℝ} {g : Label B N0 × Copy → ℕ → Native → E} (hg : LabelSumBounds.UniformClass ActualPrimaryBounds.strip (fun (x : Label B N0 × Copy) (x_1 : ℕ) (y : ActualPrimaryBounds.Point) => √(ActualPrimaryBounds.strip.zeta y)) α g) : LabelSumBounds.UniformClass ActualPrimaryBounds.strip weight α (selection g)

theorem NavierStokes.ActualSignedNativeBounds.potentialSource_inactive {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State LocalSignedRequest.Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (L : PhysicalWaveSum.BandLabel) (I : ActualSignedPhysicalData.SourceIndex) (n : ℕ) (y : Native) (hL : L ∉ ActualSignedExterior.labels B N0) : potentialSource P u H hp ⟨L, I⟩ n y = 0

theorem NavierStokes.ActualSignedNativeBounds.pressureSource_inactive {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State LocalSignedRequest.Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (L : PhysicalWaveSum.BandLabel) (I : ActualSignedPhysicalData.SourceIndex) (n : ℕ) (y : Native) (hL : L ∉ ActualSignedExterior.labels B N0) : pressureSource P u H hp ⟨L, I⟩ n y = 0

theorem NavierStokes.ActualSignedNativeBounds.potentialSource_other_label {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State LocalSignedRequest.Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (L : PhysicalWaveSum.BandLabel) (I : ActualSignedPhysicalData.SourceIndex) (n : ℕ) (y : Native) (hI : I.1.1 ≠ L) : potentialSource P u H hp ⟨L, I⟩ n y = 0

theorem NavierStokes.ActualSignedNativeBounds.pressureSource_other_label {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State LocalSignedRequest.Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (L : PhysicalWaveSum.BandLabel) (I : ActualSignedPhysicalData.SourceIndex) (n : ℕ) (y : Native) (hI : I.1.1 ≠ L) : pressureSource P u H hp ⟨L, I⟩ n y = 0

theorem NavierStokes.ActualSignedNativeBounds.potentialSource_eq_selection {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State LocalSignedRequest.Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) : potentialSource P u H hp = selection fun (i : Label B N0 × Copy) (n : ℕ) (y : Native) => ownPotential (request P u) i n ((nativeToCommon i.1) y)

theorem NavierStokes.ActualSignedNativeBounds.pressureSource_eq_selection {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State LocalSignedRequest.Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) : pressureSource P u H hp = selection fun (i : Label B N0 × Copy) (n : ℕ) (y : Native) => ownPressure (request P u) i n ((nativeToCommon i.1) y)

Joint bounds for the literal sources

theorem NavierStokes.ActualSignedNativeBounds.source_uniform {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State LocalSignedRequest.Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) {β : ℝ} (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 P u n x_2 q) : LabelSumBounds.UniformClass ActualPrimaryBounds.strip weight (β + 1) (potentialSource P u H hp) ∧ LabelSumBounds.UniformClass ActualPrimaryBounds.strip weight (β + 1) (pressureSource P u H hp)

One set of constants controls every outer label, inner label, harmonic, reference band and lattice copy of the actual native sources.

theorem NavierStokes.ActualSignedNativeBounds.native_source_bounds {E I : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {α : ℝ} {f : I → ℕ → Native → E} (hf : LabelSumBounds.UniformClass ActualPrimaryBounds.strip (fun (x : I) (x_1 : ℕ) (x_2 : ActualPrimaryBounds.Point) => √(ActualPrimaryBounds.strip.zeta x_2)) α f) : LocalPhysicalCopyBounds.LocalSourceBounds ActualPrimaryBounds.strip CorrectionInitialization.ActualPrimary.h α (fun (x : I) (x_1 : ℕ) (x_2 : ActualPrimaryBounds.Point) => √(ActualPrimaryBounds.strip.zeta x_2)) f

The fixed native strip supplies the geometric components of the physical source interface at every real exponent.

theorem NavierStokes.ActualSignedNativeBounds.source_bounds {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State LocalSignedRequest.Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) {β : ℝ} (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 P u n x_2 q) : LocalPhysicalCopyBounds.LocalSourceBounds ActualPrimaryBounds.strip CorrectionInitialization.ActualPrimary.h (β + 1) weight (potentialSource P u H hp) ∧ LocalPhysicalCopyBounds.LocalSourceBounds ActualPrimaryBounds.strip CorrectionInitialization.ActualPrimary.h (β + 1) weight (pressureSource P u H hp)

theorem NavierStokes.ActualSignedNativeBounds.source_bounds_from_residuals {B N0 : ℕ} (u : CorrectionState.State LocalSignedRequest.Point) (α : ℝ) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b u.pressure) (hfixed : VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u = u) (hθ : WeightedClasses.MeanClass ActualInitialization.geometry.strip α (u.thetaResidual (CorrectionInitialization.ActualPrimary.commonContext B))) (hz : WeightedClasses.MeanClass ActualInitialization.geometry.strip α (u.axialResidual (CorrectionInitialization.ActualPrimary.commonContext B))) : LocalPhysicalCopyBounds.LocalSourceBounds ActualPrimaryBounds.strip CorrectionInitialization.ActualPrimary.h α weight (potentialSource ActualInitialization.patch u H hp) ∧ LocalPhysicalCopyBounds.LocalSourceBounds ActualPrimaryBounds.strip CorrectionInitialization.ActualPrimary.h α weight (pressureSource ActualInitialization.patch u H hp)

The request premise can itself be discharged by the measured theta and axial residual classes of this same reconstructed state.

Positive lift-time localization of actual copy amplitudes

The gate changes only the amplitude outside positive lift time. The physical common lift has positive time exactly before terminal time, so all physical copy fields and their ambient jets agree there with the original fields.

@[reducible, inline]

abbrev NavierStokes.PositiveTimeCopyFamily.LiftPoint : Type

Lift point: an abbreviation for PhysicalGraphBounds.LiftPoint.

Equations

• NavierStokes.PositiveTimeCopyFamily.LiftPoint = NavierStokes.PhysicalGraphBounds.LiftPoint

def NavierStokes.PositiveTimeCopyFamily.liftPast : Set LiftPoint

Lift past, given by {x | 0 < x.1.1}.

Equations

• NavierStokes.PositiveTimeCopyFamily.liftPast = {x : NavierStokes.PositiveTimeCopyFamily.LiftPoint | 0 < x.1.1}

theorem NavierStokes.PositiveTimeCopyFamily.liftPast_open : IsOpen liftPast

noncomputable def NavierStokes.PositiveTimeCopyFamily.gate {H : ℕ} {K : Type u_1} (f : PhysicalCopyBounds.CopyFamily H K) : PhysicalCopyBounds.CopyFamily H K

The carrier and gap are unchanged. Only the amplitude is extended by zero outside positive native lift time.

Equations

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

@[simp]

theorem NavierStokes.PositiveTimeCopyFamily.gate_gap {H : ℕ} {K : Type u_1} (f : PhysicalCopyBounds.CopyFamily H K) : (gate f).gap = f.gap

@[simp]

theorem NavierStokes.PositiveTimeCopyFamily.gate_carrier {H : ℕ} {K : Type u_1} (f : PhysicalCopyBounds.CopyFamily H K) : (gate f).carrier = f.carrier

theorem NavierStokes.PositiveTimeCopyFamily.gate_amplitude_eq {H : ℕ} {K : Type u_1} (f : PhysicalCopyBounds.CopyFamily H K) (k : K) (I : PhysicalWaveSum.WaveIndex H) {x : LiftPoint} (hx : x ∈ liftPast) : (gate f).amplitude k I x = f.amplitude k I x

theorem NavierStokes.PositiveTimeCopyFamily.gate_amplitude_zero {H : ℕ} {K : Type u_1} (f : PhysicalCopyBounds.CopyFamily H K) (k : K) (I : PhysicalWaveSum.WaveIndex H) {x : LiftPoint} (hx : x ∉ liftPast) : (gate f).amplitude k I x = 0

theorem NavierStokes.PositiveTimeCopyFamily.gate_amplitude_ne_zero_iff {H : ℕ} {K : Type u_1} (f : PhysicalCopyBounds.CopyFamily H K) (k : K) (I : PhysicalWaveSum.WaveIndex H) (x : LiftPoint) : (gate f).amplitude k I x ≠ 0 ↔ x ∈ liftPast ∧ f.amplitude k I x ≠ 0

theorem NavierStokes.PositiveTimeCopyFamily.gate_amplitude_germ {H : ℕ} {K : Type u_1} (f : PhysicalCopyBounds.CopyFamily H K) (k : K) (I : PhysicalWaveSum.WaveIndex H) {x : LiftPoint} (hx : x ∈ liftPast) : (gate f).amplitude k I =ᶠ[nhds x] f.amplitude k I

theorem NavierStokes.PositiveTimeCopyFamily.gate_amplitude_jets {H : ℕ} {K : Type u_1} (f : PhysicalCopyBounds.CopyFamily H K) (k : K) (I : PhysicalWaveSum.WaveIndex H) {x : LiftPoint} (hx : x ∈ liftPast) (m : ℕ) : iteratedFDeriv ℝ m ((gate f).amplitude k I) x = iteratedFDeriv ℝ m (f.amplitude k I) x

theorem NavierStokes.PositiveTimeCopyFamily.gate_amplitude_support_subset {H : ℕ} {K : Type u_1} (f : PhysicalCopyBounds.CopyFamily H K) (k : K) (I : PhysicalWaveSum.WaveIndex H) : Function.support ((gate f).amplitude k I) ⊆ Function.support (f.amplitude k I)

noncomputable def NavierStokes.PositiveTimeCopyFamily.gateCells {H : ℕ} {K : Type u_1} {f : PhysicalCopyBounds.CopyFamily H K} (hc : PhysicalCopyBounds.SupportCells f) : PhysicalCopyBounds.SupportCells (gate f)

The original closed copy cells still contain the gated amplitude.

Equations

• NavierStokes.PositiveTimeCopyFamily.gateCells hc = { cells := hc.cells, support := ⋯ }

@[simp]

theorem NavierStokes.PositiveTimeCopyFamily.gateCells_cells {H : ℕ} {K : Type u_1} {f : PhysicalCopyBounds.CopyFamily H K} (hc : PhysicalCopyBounds.SupportCells f) : (gateCells hc).cells = hc.cells

noncomputable def NavierStokes.PositiveTimeCopyFamily.gateCarrier {H : ℕ} {K : Type u_1} {f : PhysicalCopyBounds.CopyFamily H K} (hc : PhysicalCopyBounds.SupportCells f) {a b h r0 : ℝ} (hb : PhysicalCopyBounds.CarrierBounds f hc a b h r0) : PhysicalCopyBounds.CarrierBounds (gate f) (gateCells hc) a b h r0

Carrier bounds refer to the same carrier and the same cells.

Equations

• NavierStokes.PositiveTimeCopyFamily.gateCarrier hc hb = { region := hb.region, open_region := ⋯, jets := ⋯, contains := ⋯ }

@[simp]

theorem NavierStokes.PositiveTimeCopyFamily.gateCarrier_region {H : ℕ} {K : Type u_1} {f : PhysicalCopyBounds.CopyFamily H K} (hc : PhysicalCopyBounds.SupportCells f) {a b h r0 : ℝ} (hb : PhysicalCopyBounds.CarrierBounds f hc a b h r0) : (gateCarrier hc hb).region = hb.region

theorem NavierStokes.PositiveTimeCopyFamily.commonLift_time (h : ℝ) (n d : ℕ) (w : ProblemStatement.SpaceTime) : (PhysicalWaveSum.commonLift h n d w).1.1 = (1 - w.1) / ChartScales.Q n

theorem NavierStokes.PositiveTimeCopyFamily.commonLift_mem_liftPast_iff (h : ℝ) (n d : ℕ) (w : ProblemStatement.SpaceTime) : PhysicalWaveSum.commonLift h n d w ∈ liftPast ↔ w ∈ PhysicalWaveSum.preterminal

This identity also holds on the axis and for arbitrary cover gap.

theorem NavierStokes.PositiveTimeCopyFamily.commonLift_mem_liftPast (h : ℝ) (n d : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : PhysicalWaveSum.commonLift h n d w ∈ liftPast

theorem NavierStokes.PositiveTimeCopyFamily.term_eq {H : ℕ} {K : Type u_1} (f : PhysicalCopyBounds.CopyFamily H K) (a h r0 : ℝ) (I : PhysicalWaveSum.WaveIndex H) (k : K) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : (gate f).term a h r0 I k w = f.term a h r0 I k w

theorem NavierStokes.PositiveTimeCopyFamily.term_zero {H : ℕ} {K : Type u_1} (f : PhysicalCopyBounds.CopyFamily H K) (a h r0 : ℝ) (I : PhysicalWaveSum.WaveIndex H) (k : K) {w : ProblemStatement.SpaceTime} (hw : w ∉ PhysicalWaveSum.preterminal) : (gate f).term a h r0 I k w = 0

theorem NavierStokes.PositiveTimeCopyFamily.term_germ {H : ℕ} {K : Type u_1} (f : PhysicalCopyBounds.CopyFamily H K) (a h r0 : ℝ) (I : PhysicalWaveSum.WaveIndex H) (k : K) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : (gate f).term a h r0 I k =ᶠ[nhds w] f.term a h r0 I k

theorem NavierStokes.PositiveTimeCopyFamily.term_jets {H : ℕ} {K : Type u_1} (f : PhysicalCopyBounds.CopyFamily H K) (a h r0 : ℝ) (I : PhysicalWaveSum.WaveIndex H) (k : K) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (m : ℕ) : iteratedFDeriv ℝ m ((gate f).term a h r0 I k) w = iteratedFDeriv ℝ m (f.term a h r0 I k) w

theorem NavierStokes.PositiveTimeCopyFamily.term_support_subset {H : ℕ} {K : Type u_1} (f : PhysicalCopyBounds.CopyFamily H K) (a h r0 : ℝ) (I : PhysicalWaveSum.WaveIndex H) (k : K) : Function.support ((gate f).term a h r0 I k) ⊆ Function.support (f.term a h r0 I k)

theorem NavierStokes.PositiveTimeCopyFamily.term_tsupport_subset {H : ℕ} {K : Type u_1} (f : PhysicalCopyBounds.CopyFamily H K) (a h r0 : ℝ) (I : PhysicalWaveSum.WaveIndex H) (k : K) : tsupport ((gate f).term a h r0 I k) ⊆ tsupport (f.term a h r0 I k)

theorem NavierStokes.PositiveTimeCopyFamily.periodized_eq {H : ℕ} {K : Type u_1} (f : PhysicalCopyBounds.CopyFamily H K) (a h r0 : ℝ) (I : PhysicalWaveSum.WaveIndex H) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : (gate f).periodized a h r0 I w = f.periodized a h r0 I w

theorem NavierStokes.PositiveTimeCopyFamily.periodized_zero {H : ℕ} {K : Type u_1} (f : PhysicalCopyBounds.CopyFamily H K) (a h r0 : ℝ) (I : PhysicalWaveSum.WaveIndex H) {w : ProblemStatement.SpaceTime} (hw : w ∉ PhysicalWaveSum.preterminal) : (gate f).periodized a h r0 I w = 0

theorem NavierStokes.PositiveTimeCopyFamily.periodized_germ {H : ℕ} {K : Type u_1} (f : PhysicalCopyBounds.CopyFamily H K) (a h r0 : ℝ) (I : PhysicalWaveSum.WaveIndex H) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : (gate f).periodized a h r0 I =ᶠ[nhds w] f.periodized a h r0 I

theorem NavierStokes.PositiveTimeCopyFamily.periodized_jets {H : ℕ} {K : Type u_1} (f : PhysicalCopyBounds.CopyFamily H K) (a h r0 : ℝ) (I : PhysicalWaveSum.WaveIndex H) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (m : ℕ) : iteratedFDeriv ℝ m ((gate f).periodized a h r0 I) w = iteratedFDeriv ℝ m (f.periodized a h r0 I) w

theorem NavierStokes.PositiveTimeCopyFamily.sum_eq {H : ℕ} {K : Type u_1} (f : PhysicalCopyBounds.CopyFamily H K) (a h r0 : ℝ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : (gate f).sum a h r0 w = f.sum a h r0 w

theorem NavierStokes.PositiveTimeCopyFamily.sum_zero {H : ℕ} {K : Type u_1} (f : PhysicalCopyBounds.CopyFamily H K) (a h r0 : ℝ) {w : ProblemStatement.SpaceTime} (hw : w ∉ PhysicalWaveSum.preterminal) : (gate f).sum a h r0 w = 0

theorem NavierStokes.PositiveTimeCopyFamily.sum_germ {H : ℕ} {K : Type u_1} (f : PhysicalCopyBounds.CopyFamily H K) (a h r0 : ℝ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : (gate f).sum a h r0 =ᶠ[nhds w] f.sum a h r0

theorem NavierStokes.PositiveTimeCopyFamily.sum_jets {H : ℕ} {K : Type u_1} (f : PhysicalCopyBounds.CopyFamily H K) (a h r0 : ℝ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (m : ℕ) : iteratedFDeriv ℝ m ((gate f).sum a h r0) w = iteratedFDeriv ℝ m (f.sum a h r0) w

theorem NavierStokes.PositiveTimeCopyFamily.vectorSum_eq {H : ℕ} {K : Type u_1} (f : Fin 3 → PhysicalCopyBounds.CopyFamily H K) (a h r0 : ℝ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : PhysicalCopyBounds.vectorSum (fun (i : Fin 3) => gate (f i)) a h r0 w = PhysicalCopyBounds.vectorSum f a h r0 w

theorem NavierStokes.PositiveTimeCopyFamily.vectorSum_zero {H : ℕ} {K : Type u_1} (f : Fin 3 → PhysicalCopyBounds.CopyFamily H K) (a h r0 : ℝ) {w : ProblemStatement.SpaceTime} (hw : w ∉ PhysicalWaveSum.preterminal) : PhysicalCopyBounds.vectorSum (fun (i : Fin 3) => gate (f i)) a h r0 w = 0

theorem NavierStokes.PositiveTimeCopyFamily.vectorSum_germ {H : ℕ} {K : Type u_1} (f : Fin 3 → PhysicalCopyBounds.CopyFamily H K) (a h r0 : ℝ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : PhysicalCopyBounds.vectorSum (fun (i : Fin 3) => gate (f i)) a h r0 =ᶠ[nhds w] PhysicalCopyBounds.vectorSum f a h r0

theorem NavierStokes.PositiveTimeCopyFamily.vectorSum_jets {H : ℕ} {K : Type u_1} (f : Fin 3 → PhysicalCopyBounds.CopyFamily H K) (a h r0 : ℝ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (m : ℕ) : iteratedFDeriv ℝ m (PhysicalCopyBounds.vectorSum (fun (i : Fin 3) => gate (f i)) a h r0) w = iteratedFDeriv ℝ m (PhysicalCopyBounds.vectorSum f a h r0) w

Signed physical data from positive native time

The native signed sources are used only at positive native time. Their totalized formula need not vanish in the past of that domain. This module uses an explicit zero extension of the physical copy amplitudes outside positive native time, while retaining the original masks, sources, and carrier profiles on their genuine domains.

Localization of the actual signed inputs at positive native time

The fixed primary's mask and target localize its native point. Positive native time is an explicit premise; no support assertion is made for the totalized formulas outside that domain.

@[reducible, inline]

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

Label: an abbreviation for ActualSignedPhysicalBinding.Label.

Equations

• NavierStokes.PositiveTimeSignedLocalization.Label = NavierStokes.ActualSignedPhysicalBinding.Label

@[reducible, inline]

abbrev NavierStokes.PositiveTimeSignedLocalization.Native : Type

Native: an abbreviation for ActualSignedPhysicalData.Native.

Equations

• NavierStokes.PositiveTimeSignedLocalization.Native = NavierStokes.ActualSignedPhysicalData.Native

theorem NavierStokes.PositiveTimeSignedLocalization.profileRadius_eq (y : Native) : PrimaryTargetBounds.profileRadius CorrectionInitialization.ActualPrimary.h (ActualSignedPhysicalData.nativeSlow y) = y.1 / √(SimilarityCoordinates.coordinateQ (2 * CorrectionInitialization.ActualPrimary.h) y.2.1)

theorem NavierStokes.PositiveTimeSignedLocalization.mask_q_mem {B N0 : ℕ} (l : Label B N0) (y : Native) (hm : (ActualSignedPhysicalBinding.primary l).mask (ActualSignedPhysicalBinding.reference l) (ActualSignedPhysicalData.nativeCylinder y) ≠ 0) : SimilarityCoordinates.coordinateQ (2 * CorrectionInitialization.ActualPrimary.h) y.2.1 ∈ Set.Ioo (1 / 2) 2

The actual dyadic mask is supported strictly inside its two endpoints.

theorem NavierStokes.PositiveTimeSignedLocalization.mask_radius_pos {B N0 : ℕ} (l : Label B N0) (y : Native) (hT : 0 < y.2.1.1) (hm : (ActualSignedPhysicalBinding.primary l).mask (ActualSignedPhysicalBinding.reference l) (ActualSignedPhysicalData.nativeCylinder y) ≠ 0) : 0 < y.1

Positivity comes from the same chosen prepared carrier, without an additional nondegeneracy premise on the signed output.

theorem NavierStokes.PositiveTimeSignedLocalization.normalized_radius_mem {B N0 : ℕ} (l : Label B N0) (y : Native) (hT : 0 < y.2.1.1) (hm : (ActualSignedPhysicalBinding.primary l).mask (ActualSignedPhysicalBinding.reference l) (ActualSignedPhysicalData.nativeCylinder y) ≠ 0) (ht : (ActualSignedPhysicalBinding.primary l).target (ActualSignedPhysicalBinding.reference l) (ActualSignedPhysicalData.nativeCylinder y) ≠ 0) : y.1 / √(SimilarityCoordinates.coordinateQ (2 * CorrectionInitialization.ActualPrimary.h) y.2.1) ∈ Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)

Nonzero actual target forces the normalized radius into the open nominal active annulus. The endpoint zeros are used exactly.

theorem NavierStokes.PositiveTimeSignedLocalization.normalized_bounds {B N0 : ℕ} (l : Label B N0) (y : Native) (hT : 0 < y.2.1.1) (hm : (ActualSignedPhysicalBinding.primary l).mask (ActualSignedPhysicalBinding.reference l) (ActualSignedPhysicalData.nativeCylinder y) ≠ 0) (ht : (ActualSignedPhysicalBinding.primary l).target (ActualSignedPhysicalBinding.reference l) (ActualSignedPhysicalData.nativeCylinder y) ≠ 0) : 1 / 2 ≤ SimilarityCoordinates.coordinateQ (2 * CorrectionInitialization.ActualPrimary.h) y.2.1 ∧ SimilarityCoordinates.coordinateQ (2 * CorrectionInitialization.ActualPrimary.h) y.2.1 ≤ 2 ∧ PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal ≤ y.1 / √(SimilarityCoordinates.coordinateQ (2 * CorrectionInitialization.ActualPrimary.h) y.2.1) ∧ y.1 / √(SimilarityCoordinates.coordinateQ (2 * CorrectionInitialization.ActualPrimary.h) y.2.1) ≤ PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal

The inequalities in the positive-time localization interface.

theorem NavierStokes.PositiveTimeSignedLocalization.native_mem_strip {B N0 : ℕ} (l : Label B N0) (y : Native) (hT : 0 < y.2.1.1) (hm : (ActualSignedPhysicalBinding.primary l).mask (ActualSignedPhysicalBinding.reference l) (ActualSignedPhysicalData.nativeCylinder y) ≠ 0) (ht : (ActualSignedPhysicalBinding.primary l).target (ActualSignedPhysicalBinding.reference l) (ActualSignedPhysicalData.nativeCylinder y) ≠ 0) : y ∈ ActualPrimaryBounds.strip.domain

Membership is in the actual moving strip, with the same fixed primary annulus and slow region used by the native signed estimates.

theorem NavierStokes.PositiveTimeSignedLocalization.mask_pullback {B N0 : ℕ} (l : Label B N0) (w : ProblemStatement.SpaceTime) (hw : w ∈ PhysicalWaveSum.preterminal) : (ActualSignedPhysicalBinding.primary l).mask (ActualSignedPhysicalBinding.reference l) (ActualSignedPhysicalData.cylinderZero (PhysicalGraphBounds.physicalLift CorrectionInitialization.ActualPrimary.h (ActualSignedPhysicalBinding.reference l) w)) = PhysicalWaveSum.physicalMask (CoordinateAlgebra.D CorrectionInitialization.ActualPrimary.h) (ActualSignedPhysicalBinding.spatialLabel l) (PhysicalWaveSum.physicalParams CorrectionInitialization.ActualPrimary.h w)

The same selected mask pulls back to the literal physical label mask at every preterminal Cartesian point.

structure NavierStokes.PositiveTimeSignedData.PrimitiveLocalization {h : ℝ} {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : ActualSignedPhysicalData.SignedFamily U) (a b : ℝ) (s : WeightedClasses.StripData ActualSignedPhysicalData.Native) : Prop

The original mask and target localize the native source only where native time is positive. The time hypothesis is explicit in both fields.

• normalized (L : ActualSignedPhysicalData.NativeLabel f.active) (y : ActualSignedPhysicalData.Native) : y ∈ ActualSignedPhysicalData.nativePast → 0 ≤ y.1 → (f.primary L).mask L.val.1 (ActualSignedPhysicalData.nativeCylinder y) ≠ 0 → (f.primary L).target L.val.1 (ActualSignedPhysicalData.nativeCylinder y) ≠ 0 → 1 / 2 ≤ SimilarityCoordinates.coordinateQ (2 * h) y.2.1 ∧ SimilarityCoordinates.coordinateQ (2 * h) y.2.1 ≤ 2 ∧ a ≤ y.1 / √(SimilarityCoordinates.coordinateQ (2 * h) y.2.1) ∧ y.1 / √(SimilarityCoordinates.coordinateQ (2 * h) y.2.1) ≤ b
• domain (L : ActualSignedPhysicalData.NativeLabel f.active) (y : ActualSignedPhysicalData.Native) : y ∈ ActualSignedPhysicalData.nativePast → 0 ≤ y.1 → (f.primary L).mask L.val.1 (ActualSignedPhysicalData.nativeCylinder y) ≠ 0 → (f.primary L).target L.val.1 (ActualSignedPhysicalData.nativeCylinder y) ≠ 0 → y ∈ s.domain
• mask_pullback (L : ActualSignedPhysicalData.NativeLabel f.active) (w : ProblemStatement.SpaceTime) : w ∈ PhysicalWaveSum.preterminal → (f.primary L).mask L.val.1 (ActualSignedPhysicalData.cylinderZero (PhysicalGraphBounds.physicalLift h L.val.1 w)) = PhysicalWaveSum.physicalMask (CoordinateAlgebra.D h) L.val (PhysicalWaveSum.physicalParams h w)

theorem NavierStokes.PositiveTimeSignedData.primitive_annulus {h a b : ℝ} {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {f : ActualSignedPhysicalData.SignedFamily U} {s : WeightedClasses.StripData ActualSignedPhysicalData.Native} (hloc : PrimitiveLocalization f a b s) (hh0 : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hb : 0 < b) (L : ActualSignedPhysicalData.NativeLabel f.active) (x : ActualSignedPhysicalData.LiftPoint) (hx : 0 < x.1.1) (hm : (f.primary L).mask L.val.1 (ActualSignedPhysicalData.cylinderZero x) ≠ 0) (hT : (f.primary L).target L.val.1 (ActualSignedPhysicalData.cylinderZero x) ≠ 0) : PhysicalGraphBounds.liftXY x ∈ PhysicalGraphBounds.annulus (a / 4) (2 * b) ∧ ‖PhysicalGraphBounds.liftZT x‖ ≤ 2

Positive-time primitive localization supplies the actual Cartesian annulus and slow-coordinate bound.

theorem NavierStokes.PositiveTimeSignedData.primitive_domain {h a b : ℝ} {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {f : ActualSignedPhysicalData.SignedFamily U} {s : WeightedClasses.StripData ActualSignedPhysicalData.Native} (hloc : PrimitiveLocalization f a b s) (L : ActualSignedPhysicalData.NativeLabel f.active) (x : ActualSignedPhysicalData.LiftPoint) (hx : 0 < x.1.1) (hm : (f.primary L).mask L.val.1 (ActualSignedPhysicalData.cylinderZero x) ≠ 0) (hT : (f.primary L).target L.val.1 (ActualSignedPhysicalData.cylinderZero x) ≠ 0) : PhysicalClassBounds.cylindricalMap x ∈ s.domain

noncomputable def NavierStokes.PositiveTimeSignedData.potentialCopies {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : ActualSignedPhysicalData.SignedFamily U) (i : Fin 3) : PhysicalCopyBounds.CopyFamily 1 ActualSignedPhysicalData.Frequency

Only the positive-time representative changes; the native potential source and every carrier are the original ones.

Equations

• NavierStokes.PositiveTimeSignedData.potentialCopies sys hh f i = NavierStokes.PositiveTimeCopyFamily.gate (NavierStokes.ActualSignedPhysicalData.potentialFamily sys hh f i)

noncomputable def NavierStokes.PositiveTimeSignedData.pressureCopies {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : ActualSignedPhysicalData.SignedFamily U) : PhysicalCopyBounds.CopyFamily 1 ActualSignedPhysicalData.Frequency

Pressure copies, given by PositiveTimeCopyFamily.gate (ActualSignedPhysicalData.pressureFamily sys hh f).

Equations

• NavierStokes.PositiveTimeSignedData.pressureCopies sys hh f = NavierStokes.PositiveTimeCopyFamily.gate (NavierStokes.ActualSignedPhysicalData.pressureFamily sys hh f)

noncomputable def NavierStokes.PositiveTimeSignedData.potentialCells {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : ActualSignedPhysicalData.SignedFamily U) (i : Fin 3) : PhysicalCopyBounds.SupportCells (potentialCopies sys hh f i)

Potential cells, given by PositiveTimeCopyFamily.gateCells (localizedPotentialCells sys hh f i).

Equations

• NavierStokes.PositiveTimeSignedData.potentialCells sys hh f i = NavierStokes.PositiveTimeCopyFamily.gateCells (NavierStokes.ActualSignedPhysicalData.localizedPotentialCells sys hh f i)

noncomputable def NavierStokes.PositiveTimeSignedData.pressureCells {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : ActualSignedPhysicalData.SignedFamily U) : PhysicalCopyBounds.SupportCells (pressureCopies sys hh f)

Pressure cells, given by PositiveTimeCopyFamily.gateCells (localizedPressureCells sys hh f).

Equations

• NavierStokes.PositiveTimeSignedData.pressureCells sys hh f = NavierStokes.PositiveTimeCopyFamily.gateCells (NavierStokes.ActualSignedPhysicalData.localizedPressureCells sys hh f)

theorem NavierStokes.PositiveTimeSignedData.potential_support {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : ActualSignedPhysicalData.SignedFamily U) {a b : ℝ} {s : WeightedClasses.StripData ActualSignedPhysicalData.Native} (hloc : PrimitiveLocalization f a b s) (G : ActualSignedPhysicalData.ReferenceGeometry sys f) (hh0 : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hb : 0 < b) (i : Fin 3) : LocalPhysicalCopyBounds.SupportData (potentialCopies sys hh f i) (a / 4) (2 * b) h sys.radius 2 0

The globally quantified support record is valid for the explicit positive-time amplitude representative.

theorem NavierStokes.PositiveTimeSignedData.pressure_support {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : ActualSignedPhysicalData.SignedFamily U) {a b : ℝ} {s : WeightedClasses.StripData ActualSignedPhysicalData.Native} (hloc : PrimitiveLocalization f a b s) (G : ActualSignedPhysicalData.ReferenceGeometry sys f) (hh0 : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hb : 0 < b) : LocalPhysicalCopyBounds.SupportData (pressureCopies sys hh f) (a / 4) (2 * b) h sys.radius 2 0

noncomputable def NavierStokes.PositiveTimeSignedData.potentialCarrier {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : ActualSignedPhysicalData.SignedFamily U) {a b : ℝ} (ha : 0 < a) (hp : ActualSignedPhysicalData.NativeProfiles f) (i : Fin 3) : PhysicalCopyBounds.CarrierBounds (potentialCopies sys hh f i) (potentialCells sys hh f i) (a / 4) (2 * b) h sys.radius

Potential carrier, constructed using PositiveTimeCopyFamily.gateCarrier.

Equations

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

noncomputable def NavierStokes.PositiveTimeSignedData.pressureCarrier {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : ActualSignedPhysicalData.SignedFamily U) {a b : ℝ} (ha : 0 < a) (hp : ActualSignedPhysicalData.NativeProfiles f) : PhysicalCopyBounds.CarrierBounds (pressureCopies sys hh f) (pressureCells sys hh f) (a / 4) (2 * b) h sys.radius

Pressure carrier, given by PositiveTimeCopyFamily.gateCarrier (localizedPressureCells sys hh f) (ActualSignedPhysicalData.pressureCarrier sys hh f ha hp).

Equations

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

theorem NavierStokes.PositiveTimeSignedData.potential_amplitude_smooth {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : ActualSignedPhysicalData.SignedFamily U) {a b : ℝ} (ha : 0 < a) (hn : ActualSignedPhysicalData.NativeRegular sys hh f) (i : Fin 3) (k : ActualSignedPhysicalData.Frequency) (I : PhysicalWaveSum.WaveIndex 1) : ContDiffOn ℝ (↑⊤) ((potentialCopies sys hh f i).amplitude k I) (ActualSignedPhysicalData.liftedNativePast a b)

theorem NavierStokes.PositiveTimeSignedData.pressure_amplitude_smooth {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : ActualSignedPhysicalData.SignedFamily U) {a b : ℝ} (ha : 0 < a) (hn : ActualSignedPhysicalData.NativeRegular sys hh f) (k : ActualSignedPhysicalData.Frequency) (I : PhysicalWaveSum.WaveIndex 1) : ContDiffOn ℝ (↑⊤) ((pressureCopies sys hh f).amplitude k I) (ActualSignedPhysicalData.liftedNativePast a b)

theorem NavierStokes.PositiveTimeSignedData.potentialSmooth {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : ActualSignedPhysicalData.SignedFamily U) {a b : ℝ} {s : WeightedClasses.StripData ActualSignedPhysicalData.Native} (hloc : PrimitiveLocalization f a b s) (G : ActualSignedPhysicalData.ReferenceGeometry sys f) (hh0 : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hb : 0 < b) (hp : ActualSignedPhysicalData.NativeProfiles f) (hn : ActualSignedPhysicalData.NativeRegular sys hh f) (i : Fin 3) : LocalPhysicalCopyBounds.SmoothData (potentialCopies sys hh f i) (a / 4) h sys.radius

theorem NavierStokes.PositiveTimeSignedData.pressureSmooth {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : ActualSignedPhysicalData.SignedFamily U) {a b : ℝ} {s : WeightedClasses.StripData ActualSignedPhysicalData.Native} (hloc : PrimitiveLocalization f a b s) (G : ActualSignedPhysicalData.ReferenceGeometry sys f) (hh0 : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hb : 0 < b) (hp : ActualSignedPhysicalData.NativeProfiles f) (hn : ActualSignedPhysicalData.NativeRegular sys hh f) : LocalPhysicalCopyBounds.SmoothData (pressureCopies sys hh f) (a / 4) h sys.radius

Source charts confined to positive time

noncomputable def NavierStokes.PositiveTimeSignedData.identitySourceChart {N : ℕ} {K I : Type} (f : PhysicalCopyBounds.CopyFamily N K) (cells : PhysicalCopyBounds.SupportCells f) {a b h r Z σ : ℝ} {gap : ℕ} (ha : 0 < a) (hs : LocalPhysicalCopyBounds.SupportData (PositiveTimeCopyFamily.gate f) a b h r Z gap) (s : WeightedClasses.StripData ActualSignedPhysicalData.LiftPoint) (source : I → ℕ → ActualSignedPhysicalData.LiftPoint → ℂ) (idx : K → PhysicalWaveSum.WaveIndex N → I) (he : ∀ (k : K) (J : PhysicalWaveSum.WaveIndex N) (x : PhysicalWaveSum.LiftPoint), f.amplitude k J x = ChartScales.Q (↑J.1).1 ^ σ • source (idx k J) (↑J.1).1 x) (hd : ∀ (k : K) (J : PhysicalWaveSum.WaveIndex N), ∀ x ∈ PositiveTimeCopyFamily.liftPast, f.amplitude k J x ≠ 0 → x ∈ s.domain) : LocalPhysicalCopyBounds.CommonChart (PositiveTimeCopyFamily.gate f) (PositiveTimeCopyFamily.gateCells cells) a b h r σ source

The chart equality is asserted only on its actual open domain. The source remains the original source, including its unchanged totalization.

Equations

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

theorem NavierStokes.PositiveTimeSignedData.potential_source_domain {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : ActualSignedPhysicalData.SignedFamily U) {a b : ℝ} {s : WeightedClasses.StripData ActualSignedPhysicalData.Native} (hloc : PrimitiveLocalization f a b s) (hh0 : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hb : 0 < b) (i : Fin 3) (k : ActualSignedPhysicalData.Frequency) (I : PhysicalWaveSum.WaveIndex 1) (x : ActualSignedPhysicalData.LiftPoint) (hx : x ∈ PositiveTimeCopyFamily.liftPast) (hne : (ActualSignedPhysicalData.potentialFamily sys hh f i).amplitude k I x ≠ 0) : x ∈ (CartesianCopySource.pullStrip s (a / 4) (2 * b) ⋯).domain

theorem NavierStokes.PositiveTimeSignedData.pressure_source_domain {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : ActualSignedPhysicalData.SignedFamily U) {a b : ℝ} {s : WeightedClasses.StripData ActualSignedPhysicalData.Native} (hloc : PrimitiveLocalization f a b s) (hh0 : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hb : 0 < b) (k : ActualSignedPhysicalData.Frequency) (I : PhysicalWaveSum.WaveIndex 1) (x : ActualSignedPhysicalData.LiftPoint) (hx : x ∈ PositiveTimeCopyFamily.liftPast) (hne : (ActualSignedPhysicalData.pressureFamily sys hh f).amplitude k I x ≠ 0) : x ∈ (CartesianCopySource.pullStrip s (a / 4) (2 * b) ⋯).domain

noncomputable def NavierStokes.PositiveTimeSignedData.potentialWaveData {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : ActualSignedPhysicalData.SignedFamily U) {a b : ℝ} {s : WeightedClasses.StripData ActualSignedPhysicalData.Native} (hloc : PrimitiveLocalization f a b s) (G : ActualSignedPhysicalData.ReferenceGeometry sys f) (hh0 : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hb : 0 < b) (hp : ActualSignedPhysicalData.NativeProfiles f) (hn : ActualSignedPhysicalData.NativeRegular sys hh f) {P : ℝ} (hP : 1 ≤ P) (hf : ∀ (L : ActualSignedPhysicalData.NativeLabel f.active), |((f.primary L).pulse (f.column L)).phase.p L.val.1| ≤ P ∧ |((f.primary L).pulse (f.column L)).phase.pz L.val.1| ≤ P ∧ |((f.primary L).pulse (f.column L)).phase.x0 L.val.1| ≤ P) {α : ℝ} {w : ActualSignedPhysicalData.SourceIndex → ℕ → ActualSignedPhysicalData.Native → ℝ} (hs : LocalPhysicalCopyBounds.LocalSourceBounds s h α w (ActualSignedPhysicalData.nativePotentialSource sys hh f)) : PhysicalStageBounds.WaveData h ActualSignedPhysicalData.LiftPoint (Fin 3 × ActualSignedPhysicalData.SourceIndex) ActualSignedPhysicalData.Frequency (Fin 3)

A physical potential datum using the original source bounds and the proved positive-time support. No off-past localization is required.

Equations

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

noncomputable def NavierStokes.PositiveTimeSignedData.pressureWaveData {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : ActualSignedPhysicalData.SignedFamily U) {a b : ℝ} {s : WeightedClasses.StripData ActualSignedPhysicalData.Native} (hloc : PrimitiveLocalization f a b s) (G : ActualSignedPhysicalData.ReferenceGeometry sys f) (hh0 : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hb : 0 < b) (hp : ActualSignedPhysicalData.NativeProfiles f) (hn : ActualSignedPhysicalData.NativeRegular sys hh f) {P : ℝ} (hP : 1 ≤ P) (hf : ∀ (L : ActualSignedPhysicalData.NativeLabel f.active), |((f.primary L).pulse (f.column L)).phase.p L.val.1| ≤ P ∧ |((f.primary L).pulse (f.column L)).phase.pz L.val.1| ≤ P ∧ |((f.primary L).pulse (f.column L)).phase.x0 L.val.1| ≤ P) {α : ℝ} {w : ActualSignedPhysicalData.SourceIndex → ℕ → ActualSignedPhysicalData.Native → ℝ} (hs : LocalPhysicalCopyBounds.LocalSourceBounds s h α w (ActualSignedPhysicalData.nativePressureSource sys hh f)) : PhysicalStageBounds.WaveData h ActualSignedPhysicalData.LiftPoint ActualSignedPhysicalData.SourceIndex ActualSignedPhysicalData.Frequency Unit

Pressure wave data, bundling lowerRadius, upperRadius, nativeWidth, slowBound and the required compatibility proofs.

Equations

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

theorem NavierStokes.PositiveTimeSignedData.potentialWaveData_vector_germ {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : ActualSignedPhysicalData.SignedFamily U) {a b : ℝ} {s : WeightedClasses.StripData ActualSignedPhysicalData.Native} (hloc : PrimitiveLocalization f a b s) (G : ActualSignedPhysicalData.ReferenceGeometry sys f) (hh0 : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hb : 0 < b) (hp : ActualSignedPhysicalData.NativeProfiles f) (hn : ActualSignedPhysicalData.NativeRegular sys hh f) {P : ℝ} (hP : 1 ≤ P) (hf : ∀ (L : ActualSignedPhysicalData.NativeLabel f.active), |((f.primary L).pulse (f.column L)).phase.p L.val.1| ≤ P ∧ |((f.primary L).pulse (f.column L)).phase.pz L.val.1| ≤ P ∧ |((f.primary L).pulse (f.column L)).phase.x0 L.val.1| ≤ P) {α : ℝ} {w : ActualSignedPhysicalData.SourceIndex → ℕ → ActualSignedPhysicalData.Native → ℝ} (hpotential : LocalPhysicalCopyBounds.LocalSourceBounds s h α w (ActualSignedPhysicalData.nativePotentialSource sys hh f)) {x : ProblemStatement.SpaceTime} (hx : x ∈ PhysicalWaveSum.preterminal) : (potentialWaveData sys hh f hloc G hh0 hh1 ha hb hp hn hP hf hpotential).vector =ᶠ[nhds x] PhysicalCopyBounds.vectorSum (ActualSignedPhysicalData.potentialFamily sys hh f) (a / 4) h sys.radius

Every preterminal potential germ is the germ of the original physical copy sum, including all spatial and time derivatives.

theorem NavierStokes.PositiveTimeSignedData.pressureWaveData_pressure_germ {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : ActualSignedPhysicalData.SignedFamily U) {a b : ℝ} {s : WeightedClasses.StripData ActualSignedPhysicalData.Native} (hloc : PrimitiveLocalization f a b s) (G : ActualSignedPhysicalData.ReferenceGeometry sys f) (hh0 : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hb : 0 < b) (hp : ActualSignedPhysicalData.NativeProfiles f) (hn : ActualSignedPhysicalData.NativeRegular sys hh f) {P : ℝ} (hP : 1 ≤ P) (hf : ∀ (L : ActualSignedPhysicalData.NativeLabel f.active), |((f.primary L).pulse (f.column L)).phase.p L.val.1| ≤ P ∧ |((f.primary L).pulse (f.column L)).phase.pz L.val.1| ≤ P ∧ |((f.primary L).pulse (f.column L)).phase.x0 L.val.1| ≤ P) {α : ℝ} {w : ActualSignedPhysicalData.SourceIndex → ℕ → ActualSignedPhysicalData.Native → ℝ} (hpressure : LocalPhysicalCopyBounds.LocalSourceBounds s h α w (ActualSignedPhysicalData.nativePressureSource sys hh f)) {x : ProblemStatement.SpaceTime} (hx : x ∈ PhysicalWaveSum.preterminal) : (pressureWaveData sys hh f hloc G hh0 hh1 ha hb hp hn hP hf hpressure).pressure =ᶠ[nhds x] fun (y : ProblemStatement.SpaceTime) => ((ActualSignedPhysicalData.pressureFamily sys hh f).sum (a / 4) h sys.radius y).re

theorem NavierStokes.PositiveTimeSignedData.potential_physical_bound {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : ActualSignedPhysicalData.SignedFamily U) {a b : ℝ} {s : WeightedClasses.StripData ActualSignedPhysicalData.Native} (hloc : PrimitiveLocalization f a b s) (G : ActualSignedPhysicalData.ReferenceGeometry sys f) (hh0 : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hb : 0 < b) (hp : ActualSignedPhysicalData.NativeProfiles f) (hn : ActualSignedPhysicalData.NativeRegular sys hh f) {P : ℝ} (hP : 1 ≤ P) (hf : ∀ (L : ActualSignedPhysicalData.NativeLabel f.active), |((f.primary L).pulse (f.column L)).phase.p L.val.1| ≤ P ∧ |((f.primary L).pulse (f.column L)).phase.pz L.val.1| ≤ P ∧ |((f.primary L).pulse (f.column L)).phase.x0 L.val.1| ≤ P) {α : ℝ} {w : ActualSignedPhysicalData.SourceIndex → ℕ → ActualSignedPhysicalData.Native → ℝ} (hpotential : LocalPhysicalCopyBounds.LocalSourceBounds s h α w (ActualSignedPhysicalData.nativePotentialSource sys hh f)) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ x ∈ PhysicalWaveSum.preterminal, PhysicalWaveSum.physicalQ h x ≤ 1 → ‖iteratedFDeriv ℝ m (PhysicalCopyBounds.vectorSum (ActualSignedPhysicalData.potentialFamily sys hh f) (a / 4) h sys.radius) x‖ ≤ C * PhysicalWaveSum.physicalQ h x ^ (h * α - PhysicalClassBounds.physicalLoss h (-h) m)

The physical estimate applies to the original preterminal potential, not just to its chosen positive-time representative.

theorem NavierStokes.PositiveTimeSignedData.pressure_physical_bound {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (f : ActualSignedPhysicalData.SignedFamily U) {a b : ℝ} {s : WeightedClasses.StripData ActualSignedPhysicalData.Native} (hloc : PrimitiveLocalization f a b s) (G : ActualSignedPhysicalData.ReferenceGeometry sys f) (hh0 : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hb : 0 < b) (hp : ActualSignedPhysicalData.NativeProfiles f) (hn : ActualSignedPhysicalData.NativeRegular sys hh f) {P : ℝ} (hP : 1 ≤ P) (hf : ∀ (L : ActualSignedPhysicalData.NativeLabel f.active), |((f.primary L).pulse (f.column L)).phase.p L.val.1| ≤ P ∧ |((f.primary L).pulse (f.column L)).phase.pz L.val.1| ≤ P ∧ |((f.primary L).pulse (f.column L)).phase.x0 L.val.1| ≤ P) {α : ℝ} {w : ActualSignedPhysicalData.SourceIndex → ℕ → ActualSignedPhysicalData.Native → ℝ} (hpressure : LocalPhysicalCopyBounds.LocalSourceBounds s h α w (ActualSignedPhysicalData.nativePressureSource sys hh f)) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ x ∈ PhysicalWaveSum.preterminal, PhysicalWaveSum.physicalQ h x ≤ 1 → ‖iteratedFDeriv ℝ m (fun (y : ProblemStatement.SpaceTime) => ((ActualSignedPhysicalData.pressureFamily sys hh f).sum (a / 4) h sys.radius y).re) x‖ ≤ C * PhysicalWaveSum.physicalQ h x ^ (h * α - PhysicalClassBounds.physicalLoss h (-(2 * CoordinateAlgebra.A h)) m)

The actual dependent signed family

theorem NavierStokes.PositiveTimeSignedData.singletonLocalization {B N0 : ℕ} (s : (l : ActualSignedPhysicalBinding.Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (L : ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.family s).active) : PrimitiveLocalization ((ActualSignedExterior.family s).singleton L) (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal) ActualPrimaryBounds.strip

Every actual singleton supplies the positive-time primitive data. Neither its current request nor any output support property is assumed.

The actual signed carrier profiles on their Prepared regions

The family keeps each label's genuine Prepared phase domain. The closed one-mesh mask support lies strictly inside the open two-mesh domain at positive time. This proves the physical closure-coverage condition without extending the profile functions across a native domain boundary.

@[reducible, inline]

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

Label: an abbreviation for ActualSignedPhysicalBinding.Label.

Equations

• NavierStokes.ActualSignedNativeProfiles.Label = NavierStokes.ActualSignedPhysicalBinding.Label

@[reducible, inline]

abbrev NavierStokes.ActualSignedNativeProfiles.NativeLabel (B N0 : ℕ) : Type

Native label: an abbreviation for ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.labels B N0).

Equations

• NavierStokes.ActualSignedNativeProfiles.NativeLabel B N0 = NavierStokes.ActualSignedPhysicalData.NativeLabel (NavierStokes.ActualSignedExterior.labels B N0)

@[reducible, inline]

abbrev NavierStokes.ActualSignedNativeProfiles.Slow : Type

Slow: an abbreviation for PhaseCalculus.Slow.

Equations

• NavierStokes.ActualSignedNativeProfiles.Slow = NavierStokes.PhaseCalculus.Slow

@[reducible, inline]

abbrev NavierStokes.ActualSignedNativeProfiles.Frequency : Type

Frequency: an abbreviation for TorusInverse.Frequency.

Equations

• NavierStokes.ActualSignedNativeProfiles.Frequency = NavierStokes.TorusInverse.Frequency

@[reducible, inline]

abbrev NavierStokes.ActualSignedNativeProfiles.LiftPoint : Type

Lift point: an abbreviation for PhysicalGraphBounds.LiftPoint.

Equations

• NavierStokes.ActualSignedNativeProfiles.LiftPoint = NavierStokes.PhysicalGraphBounds.LiftPoint

noncomputable def NavierStokes.ActualSignedNativeProfiles.region (B N0 : ℕ) (L : PhysicalWaveSum.BandLabel) : Set Slow

No Prepared data is chosen for omitted physical labels.

Equations

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

theorem NavierStokes.ActualSignedNativeProfiles.region_open (B N0 : ℕ) (L : PhysicalWaveSum.BandLabel) : IsOpen (region B N0 L)

theorem NavierStokes.ActualSignedNativeProfiles.region_active {B N0 : ℕ} (L : NativeLabel B N0) : region B N0 ⟨L.val, ⋯⟩ = (ActualSignedPhysicalBinding.domain (ActualSignedExterior.actualLabel L)).carrier 0

noncomputable def NavierStokes.ActualSignedNativeProfiles.profilePair (B n : ℕ) (p : Slow) : ℝ × ℝ

Profile pair as an element of ℝ × ℝ.

Equations

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

noncomputable def NavierStokes.ActualSignedNativeProfiles.profileDomain (B N0 : ℕ) : PhaseJetBounds.Domain (Frequency × PhysicalWaveSum.BandLabel) Slow

Profile domain, given by PhysicalCopyBounds.copyBandDomain (fun (_ : Frequency) L => region B N0 L) (fun _ L => region_open B N0 L).

Equations

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

theorem NavierStokes.ActualSignedNativeProfiles.profile_jets {B N0 : ℕ} : PhaseJetBounds.PolynomialJets (profileDomain B N0) fun (I : Frequency × PhysicalWaveSum.BandLabel) (p : Slow) => profilePair B (↑I.2).1 p

The constants come from the original joint Prepared family before selecting a physical label or a lattice copy.

noncomputable def NavierStokes.ActualSignedNativeProfiles.liftedSlow (x : LiftPoint) : Slow

Lifted slow, given by (PolarCharts.radius (PhysicalGraphBounds.liftXY x), PhysicalGraphBounds.liftZT x).

Equations

• NavierStokes.ActualSignedNativeProfiles.liftedSlow x = (NavierStokes.PolarCharts.radius (NavierStokes.PhysicalGraphBounds.liftXY x), NavierStokes.PhysicalGraphBounds.liftZT x)

theorem NavierStokes.ActualSignedNativeProfiles.liftedSlow_continuous : Continuous liftedSlow

theorem NavierStokes.ActualSignedNativeProfiles.liftedSlow_physical (n : ℕ) (w : ProblemStatement.SpaceTime) : liftedSlow (PhysicalGraphBounds.physicalLift CorrectionInitialization.ActualPrimary.h n w) = ActualSignedPhysicalData.nativeSlow (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n 0 w)

theorem NavierStokes.ActualSignedNativeProfiles.singleton_profiles {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (L : NativeLabel B N0) (K : PhysicalWaveSum.BandLabel) (k : Frequency) (p : Slow) : ((ActualSignedPhysicalData.extendedCarrier ((ActualSignedExterior.family s).singleton L) K k).F p, (ActualSignedPhysicalData.extendedCarrier ((ActualSignedExterior.family s).singleton L) K k).G p) = if K = ⟨L.val, ⋯⟩ then profilePair B (↑K).1 p else 0

theorem NavierStokes.ActualSignedNativeProfiles.singleton_jets {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (L : NativeLabel B N0) : PhaseJetBounds.PolynomialJets (profileDomain B N0) fun (I : Frequency × PhysicalWaveSum.BandLabel) (p : Slow) => ((ActualSignedPhysicalData.extendedCarrier ((ActualSignedExterior.family s).singleton L) I.2 I.1).F p, (ActualSignedPhysicalData.extendedCarrier ((ActualSignedExterior.family s).singleton L) I.2 I.1).G p)

A single active branch uses the common joint constants; omitted branches have identically zero carrier profiles.

theorem NavierStokes.ActualSignedNativeProfiles.core_empty {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (L : NativeLabel B N0) {K : PhysicalWaveSum.BandLabel} (hne : K ≠ ⟨L.val, ⋯⟩) : ActualSignedPhysicalData.primitiveCore ((ActualSignedExterior.family s).singleton L) K = ∅

theorem NavierStokes.ActualSignedNativeProfiles.core_in_mask_support {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (L : NativeLabel B N0) : ActualSignedPhysicalData.primitiveCore ((ActualSignedExterior.family s).singleton L) ⟨L.val, ⋯⟩ ⊆ liftedSlow ⁻¹' tsupport (PrimaryRepresentatives.nativeMask (BaseChartJets.cellBand (ActualSignedExterior.actualLabel L).1) (PrimaryGeometryAssembly.label CorrectionInitialization.ActualPrimary.nominal (ActualSignedExterior.actualLabel L).1).2)

theorem NavierStokes.ActualSignedNativeProfiles.closure_covers {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (L : NativeLabel B N0) (K : PhysicalWaveSum.BandLabel) (w : ProblemStatement.SpaceTime) (hw : w ∈ PhysicalWaveSum.preterminal) (hc : PhysicalGraphBounds.physicalLift CorrectionInitialization.ActualPrimary.h (↑K).1 w ∈ closure (ActualSignedPhysicalData.primitiveCore ((ActualSignedExterior.family s).singleton L) K)) : ActualSignedPhysicalData.nativeSlow (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h (↑K).1 0 w) ∈ region B N0 K

noncomputable def NavierStokes.ActualSignedNativeProfiles.nativeProfiles {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (L : NativeLabel B N0) : ActualSignedPhysicalData.NativeProfiles ((ActualSignedExterior.family s).singleton L)

The actual homogeneous singleton interface needed by the physical factory, with no extension or output-bound assumptions.

Equations

• NavierStokes.ActualSignedNativeProfiles.nativeProfiles s L = { region := NavierStokes.ActualSignedNativeProfiles.region B N0, region_open := ⋯, jets := ⋯, covers := ⋯ }

theorem NavierStokes.ActualSignedNativeProfiles.potential_profiles_jets {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (i : Fin 3) : PhaseJetBounds.PolynomialJets (profileDomain B N0) fun (I : Frequency × PhysicalWaveSum.BandLabel) (p : Slow) => ((((ActualSignedExterior.family s).potentialCopies CorrectionInitialization.ActualPrimary.slots ⋯ i).carrier I.1 I.2).F p, (((ActualSignedExterior.family s).potentialCopies CorrectionInitialization.ActualPrimary.slots ⋯ i).carrier I.1 I.2).G p)

The actual assembled potential carrier retains the joint Prepared bound, including the copy index and every physical label.

theorem NavierStokes.ActualSignedNativeProfiles.pressure_profiles_jets {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) : PhaseJetBounds.PolynomialJets (profileDomain B N0) fun (I : Frequency × PhysicalWaveSum.BandLabel) (p : Slow) => ((((ActualSignedExterior.family s).pressureCopies CorrectionInitialization.ActualPrimary.slots ⋯).carrier I.1 I.2).F p, (((ActualSignedExterior.family s).pressureCopies CorrectionInitialization.ActualPrimary.slots ⋯).carrier I.1 I.2).G p)

Support and local smoothness of the actual signed copy family

The aggregate retains the original singleton at each active label and is zero at omitted labels. Positive lift-time gating commutes with this assembly. The source-domain statements concern the original, ungated amplitudes on positive lift time.

@[reducible, inline]

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

Label: an abbreviation for ActualSignedPhysicalBinding.Label.

Equations

• NavierStokes.ActualSignedFamilySupport.Label = NavierStokes.ActualSignedPhysicalBinding.Label

noncomputable def NavierStokes.ActualSignedFamilySupport.potentialCopies {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (i : Fin 3) : PhysicalCopyBounds.CopyFamily 1 TorusInverse.Frequency

The actual aggregate potential copies, with the sole positive-time gate.

Equations

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

noncomputable def NavierStokes.ActualSignedFamilySupport.pressureCopies {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) : PhysicalCopyBounds.CopyFamily 1 TorusInverse.Frequency

The actual aggregate pressure copies, with the same gate.

Equations

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

theorem NavierStokes.ActualSignedFamilySupport.potential_support {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (hgeo : (L : ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.family s).active) → ActualSignedPhysicalData.ReferenceGeometry CorrectionInitialization.ActualPrimary.slots ((ActualSignedExterior.family s).singleton L)) (i : Fin 3) : LocalPhysicalCopyBounds.SupportData (potentialCopies s i) ActualPolarCoverage.inner ActualPolarCoverage.outer CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius 2 0

Global support of the aggregate follows from the primitive masks and targets of its selected singletons.

theorem NavierStokes.ActualSignedFamilySupport.pressure_support {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (hgeo : (L : ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.family s).active) → ActualSignedPhysicalData.ReferenceGeometry CorrectionInitialization.ActualPrimary.slots ((ActualSignedExterior.family s).singleton L)) : LocalPhysicalCopyBounds.SupportData (pressureCopies s) ActualPolarCoverage.inner ActualPolarCoverage.outer CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius 2 0

theorem NavierStokes.ActualSignedFamilySupport.potential_smooth {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (hgeo : (L : ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.family s).active) → ActualSignedPhysicalData.ReferenceGeometry CorrectionInitialization.ActualPrimary.slots ((ActualSignedExterior.family s).singleton L)) (hn : ∀ (L : ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.family s).active), ActualSignedPhysicalData.NativeRegular CorrectionInitialization.ActualPrimary.slots ⋯ ((ActualSignedExterior.family s).singleton L)) (i : Fin 3) : LocalPhysicalCopyBounds.SmoothData (potentialCopies s i) ActualPolarCoverage.inner CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius

Only the native regularity near actual copy support is used.

theorem NavierStokes.ActualSignedFamilySupport.pressure_smooth {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (hgeo : (L : ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.family s).active) → ActualSignedPhysicalData.ReferenceGeometry CorrectionInitialization.ActualPrimary.slots ((ActualSignedExterior.family s).singleton L)) (hn : ∀ (L : ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.family s).active), ActualSignedPhysicalData.NativeRegular CorrectionInitialization.ActualPrimary.slots ⋯ ((ActualSignedExterior.family s).singleton L)) : LocalPhysicalCopyBounds.SmoothData (pressureCopies s) ActualPolarCoverage.inner CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius

theorem NavierStokes.ActualSignedFamilySupport.potential_source_domain {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (i : Fin 3) (k : TorusInverse.Frequency) (I : PhysicalWaveSum.WaveIndex 1) (x : PhysicalGraphBounds.LiftPoint) (hx : x ∈ PositiveTimeCopyFamily.liftPast) (hne : ((ActualSignedExterior.family s).potentialCopies CorrectionInitialization.ActualPrimary.slots ⋯ i).amplitude k I x ≠ 0) : x ∈ (CartesianCopySource.pullStrip ActualPrimaryBounds.strip ActualPolarCoverage.inner ActualPolarCoverage.outer ActualPolarCoverage.inner_pos).domain

A nonzero original potential amplitude at positive lift time lies in the actual source strip. No geometry or output estimate is assumed.

theorem NavierStokes.ActualSignedFamilySupport.pressure_source_domain {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (k : TorusInverse.Frequency) (I : PhysicalWaveSum.WaveIndex 1) (x : PhysicalGraphBounds.LiftPoint) (hx : x ∈ PositiveTimeCopyFamily.liftPast) (hne : ((ActualSignedExterior.family s).pressureCopies CorrectionInitialization.ActualPrimary.slots ⋯).amplitude k I x ≠ 0) : x ∈ (CartesianCopySource.pullStrip ActualPrimaryBounds.strip ActualPolarCoverage.inner ActualPolarCoverage.outer ActualPolarCoverage.inner_pos).domain

@[reducible, inline]

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

Label: an abbreviation for ActualSignedPhysicalBinding.Label.

Equations

• NavierStokes.ActualSignedWaveData.Label = NavierStokes.ActualSignedPhysicalBinding.Label

@[reducible, inline]

abbrev NavierStokes.ActualSignedWaveData.Native : Type

Native: an abbreviation for ActualSignedPhysicalData.Native.

Equations

• NavierStokes.ActualSignedWaveData.Native = NavierStokes.ActualSignedPhysicalData.Native

@[reducible, inline]

abbrev NavierStokes.ActualSignedWaveData.SourceIndex : Type

Source index: an abbreviation for Σ (_ : BandLabel), ActualSignedPhysicalData.SourceIndex.

Equations

• NavierStokes.ActualSignedWaveData.SourceIndex = ((_ : NavierStokes.PhysicalWaveSum.BandLabel) × NavierStokes.ActualSignedPhysicalData.SourceIndex)

noncomputable def NavierStokes.ActualSignedWaveData.nativeStates {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State LocalSignedRequest.Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (l : Label B N0) : (ActualSignedPhysicalBinding.nativeViews l).StateData

Native states, given by ActualSignedPhysicalBinding.nativeStateData l P u H hp.

Equations

• NavierStokes.ActualSignedWaveData.nativeStates P u H hp l = NavierStokes.ActualSignedPhysicalBinding.nativeStateData l P u H hp

noncomputable def NavierStokes.ActualSignedWaveData.family {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State LocalSignedRequest.Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) : DependentSignedPhysicalFamily.Family

Family, given by ActualSignedExterior.family (nativeStates (N0 := N0) P u H hp).

Equations

• NavierStokes.ActualSignedWaveData.family P u H hp = NavierStokes.ActualSignedExterior.family (NavierStokes.ActualSignedWaveData.nativeStates P u H hp)

noncomputable def NavierStokes.ActualSignedWaveData.singletonGeometry {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State LocalSignedRequest.Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (L : ActualSignedPhysicalData.NativeLabel (family P u H hp).active) : ActualSignedPhysicalData.ReferenceGeometry CorrectionInitialization.ActualPrimary.slots ((family P u H hp).singleton L)

The physical geometry is derived from the same actual primary, views, and current-state request; no representation assertion is assumed.

Equations

• NavierStokes.ActualSignedWaveData.singletonGeometry P u H hp L = NavierStokes.ActualSignedReferenceGeometry.singletonGeometry P u H hp L

theorem NavierStokes.ActualSignedWaveData.singleton_frequencies {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State LocalSignedRequest.Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion P.a P.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion P.a P.b u.pressure) (L : ActualSignedPhysicalData.NativeLabel (family P u H hp).active) (K : ActualSignedPhysicalData.NativeLabel ((family P u H hp).singleton L).active) : |((((family P u H hp).singleton L).primary K).pulse (((family P u H hp).singleton L).column K)).phase.p K.val.1| ≤ ActualPhaseJetBounds.phaseSize B N0 ∧ |((((family P u H hp).singleton L).primary K).pulse (((family P u H hp).singleton L).column K)).phase.pz K.val.1| ≤ ActualPhaseJetBounds.phaseSize B N0 ∧ |((((family P u H hp).singleton L).primary K).pulse (((family P u H hp).singleton L).column K)).phase.x0 K.val.1| ≤ ActualPhaseJetBounds.phaseSize B N0

One actual bound works for every native label and both signs.

noncomputable def NavierStokes.ActualSignedWaveData.originalPotentialCells {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (i : Fin 3) : PhysicalCopyBounds.SupportCells ((ActualSignedExterior.family s).potentialCopies CorrectionInitialization.ActualPrimary.slots ⋯ i)

Original potential cells, constructed using DependentSignedPhysicalFamily.diagonalCells.

Equations

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

noncomputable def NavierStokes.ActualSignedWaveData.originalPressureCells {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) : PhysicalCopyBounds.SupportCells ((ActualSignedExterior.family s).pressureCopies CorrectionInitialization.ActualPrimary.slots ⋯)

Original pressure cells, constructed using DependentSignedPhysicalFamily.diagonalCells.

Equations

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

theorem NavierStokes.ActualSignedWaveData.potentialCells_active {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (i : Fin 3) (L : ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.labels B N0)) : (originalPotentialCells s i).cells ⟨L.val, ⋯⟩ = (ActualSignedPhysicalData.localizedPotentialCells CorrectionInitialization.ActualPrimary.slots ⋯ ((ActualSignedExterior.family s).singleton L) i).cells ⟨L.val, ⋯⟩

theorem NavierStokes.ActualSignedWaveData.pressureCells_active {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (L : ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.labels B N0)) : (originalPressureCells s).cells ⟨L.val, ⋯⟩ = (ActualSignedPhysicalData.localizedPressureCells CorrectionInitialization.ActualPrimary.slots ⋯ ((ActualSignedExterior.family s).singleton L)).cells ⟨L.val, ⋯⟩

theorem NavierStokes.ActualSignedWaveData.potentialCells_inactive {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (i : Fin 3) {L : PhysicalWaveSum.BandLabel} (hL : L ∉ ActualSignedExterior.labels B N0) : (originalPotentialCells s i).cells L = DependentSignedPhysicalFamily.zeroCells.cells L

theorem NavierStokes.ActualSignedWaveData.pressureCells_inactive {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) {L : PhysicalWaveSum.BandLabel} (hL : L ∉ ActualSignedExterior.labels B N0) : (originalPressureCells s).cells L = DependentSignedPhysicalFamily.zeroCells.cells L

noncomputable def NavierStokes.ActualSignedWaveData.originalPotentialCarrier {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (i : Fin 3) : PhysicalCopyBounds.CarrierBounds ((ActualSignedExterior.family s).potentialCopies CorrectionInitialization.ActualPrimary.slots ⋯ i) (originalPotentialCells s i) ActualPolarCoverage.inner ActualPolarCoverage.outer CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius

Original potential carrier, bundling region, open_region, jets, contains and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.ActualSignedWaveData.originalPressureCarrier {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) : PhysicalCopyBounds.CarrierBounds ((ActualSignedExterior.family s).pressureCopies CorrectionInitialization.ActualPrimary.slots ⋯) (originalPressureCells s) ActualPolarCoverage.inner ActualPolarCoverage.outer CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius

Original pressure carrier, bundling region, open_region, jets, contains and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.ActualSignedWaveData.potentialCopies {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (i : Fin 3) : PhysicalCopyBounds.CopyFamily 1 TorusInverse.Frequency

The actual assembled copies, extended by zero outside positive lift time. Their fields agree with the original signed fields before t=1.

Equations

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

noncomputable def NavierStokes.ActualSignedWaveData.pressureCopies {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) : PhysicalCopyBounds.CopyFamily 1 TorusInverse.Frequency

Pressure copies, given by PositiveTimeCopyFamily.gate ((ActualSignedExterior.family s).pressureCopies slots outgoing.data.h_pos.le).

Equations

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

noncomputable def NavierStokes.ActualSignedWaveData.potentialCells {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (i : Fin 3) : PhysicalCopyBounds.SupportCells (potentialCopies s i)

Potential cells, given by PositiveTimeCopyFamily.gateCells (originalPotentialCells s i).

Equations

• NavierStokes.ActualSignedWaveData.potentialCells s i = NavierStokes.PositiveTimeCopyFamily.gateCells (NavierStokes.ActualSignedWaveData.originalPotentialCells s i)

noncomputable def NavierStokes.ActualSignedWaveData.pressureCells {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) : PhysicalCopyBounds.SupportCells (pressureCopies s)

Pressure cells, given by PositiveTimeCopyFamily.gateCells (originalPressureCells s).

Equations

• NavierStokes.ActualSignedWaveData.pressureCells s = NavierStokes.PositiveTimeCopyFamily.gateCells (NavierStokes.ActualSignedWaveData.originalPressureCells s)

noncomputable def NavierStokes.ActualSignedWaveData.potentialCarrier {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (i : Fin 3) : PhysicalCopyBounds.CarrierBounds (potentialCopies s i) (potentialCells s i) ActualPolarCoverage.inner ActualPolarCoverage.outer CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius

Potential carrier, given by PositiveTimeCopyFamily.gateCarrier (originalPotentialCells s i) (originalPotentialCarrier s i).

Equations

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

noncomputable def NavierStokes.ActualSignedWaveData.pressureCarrier {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) : PhysicalCopyBounds.CarrierBounds (pressureCopies s) (pressureCells s) ActualPolarCoverage.inner ActualPolarCoverage.outer CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius

Pressure carrier, given by PositiveTimeCopyFamily.gateCarrier (originalPressureCells s) (originalPressureCarrier s).

Equations

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

theorem NavierStokes.ActualSignedWaveData.potential_field_eq {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : PhysicalCopyBounds.vectorSum (potentialCopies s) ActualPolarCoverage.inner CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius w = ActualSignedExterior.potential s w

theorem NavierStokes.ActualSignedWaveData.pressure_field_eq {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : ((pressureCopies s).sum ActualPolarCoverage.inner CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius w).re = ActualSignedExterior.pressure s w

theorem NavierStokes.ActualSignedWaveData.potential_field_germ {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : PhysicalCopyBounds.vectorSum (potentialCopies s) ActualPolarCoverage.inner CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius =ᶠ[nhds w] ActualSignedExterior.potential s

theorem NavierStokes.ActualSignedWaveData.pressure_field_germ {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : (fun (w : ProblemStatement.SpaceTime) => ((pressureCopies s).sum ActualPolarCoverage.inner CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius w).re) =ᶠ[nhds w] ActualSignedExterior.pressure s

theorem NavierStokes.ActualSignedWaveData.singleton_frequencies_of_states {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (L : ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.family s).active) (K : ActualSignedPhysicalData.NativeLabel ((ActualSignedExterior.family s).singleton L).active) : |((((ActualSignedExterior.family s).singleton L).primary K).pulse (((ActualSignedExterior.family s).singleton L).column K)).phase.p K.val.1| ≤ ActualPhaseJetBounds.phaseSize B N0 ∧ |((((ActualSignedExterior.family s).singleton L).primary K).pulse (((ActualSignedExterior.family s).singleton L).column K)).phase.pz K.val.1| ≤ ActualPhaseJetBounds.phaseSize B N0 ∧ |((((ActualSignedExterior.family s).singleton L).primary K).pulse (((ActualSignedExterior.family s).singleton L).column K)).phase.x0 K.val.1| ≤ ActualPhaseJetBounds.phaseSize B N0

The carrier coefficients remain jointly bounded after label selection and the positive-time extension.

theorem NavierStokes.ActualSignedWaveData.potential_frequencies {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (i : Fin 3) (k : TorusInverse.Frequency) (L : PhysicalWaveSum.BandLabel) : |((potentialCopies s i).carrier k L).angular| ≤ ActualPhaseJetBounds.phaseSize B N0 ∧ |((potentialCopies s i).carrier k L).axial| ≤ ActualPhaseJetBounds.phaseSize B N0 ∧ |((potentialCopies s i).carrier k L).radial| ≤ ActualPhaseJetBounds.phaseSize B N0

theorem NavierStokes.ActualSignedWaveData.pressure_frequencies {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (k : TorusInverse.Frequency) (L : PhysicalWaveSum.BandLabel) : |((pressureCopies s).carrier k L).angular| ≤ ActualPhaseJetBounds.phaseSize B N0 ∧ |((pressureCopies s).carrier k L).axial| ≤ ActualPhaseJetBounds.phaseSize B N0 ∧ |((pressureCopies s).carrier k L).radial| ≤ ActualPhaseJetBounds.phaseSize B N0

The jointly indexed Cartesian sources

noncomputable def NavierStokes.ActualSignedWaveData.sourceStrip : WeightedClasses.StripData PhysicalGraphBounds.LiftPoint

Source strip, constructed using CartesianCopySource.pullStrip.

Equations

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

noncomputable def NavierStokes.ActualSignedWaveData.potentialSource {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) : Fin 3 × SourceIndex → ℕ → PhysicalGraphBounds.LiftPoint → ℂ

Potential source as an element of (Fin 3 × SourceIndex) → ℕ → PhysicalGraphBounds.LiftPoint → ℂ.

Equations

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

noncomputable def NavierStokes.ActualSignedWaveData.pressureSource {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) : SourceIndex → ℕ → PhysicalGraphBounds.LiftPoint → ℂ

Pressure source as an element of SourceIndex → ℕ → PhysicalGraphBounds.LiftPoint → ℂ.

Equations

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

noncomputable def NavierStokes.ActualSignedWaveData.sourceWeight : SourceIndex → ℕ → (x : PhysicalGraphBounds.LiftPoint) → ℝ

Source weight, given by Real.sqrt (ActualPrimaryBounds.strip.zeta (PhysicalClassBounds.cylindricalMap x)).

Equations

• NavierStokes.ActualSignedWaveData.sourceWeight x✝¹ x✝ x = √(NavierStokes.ActualPrimaryBounds.strip.zeta (NavierStokes.PhysicalClassBounds.cylindricalMap x))

noncomputable def NavierStokes.ActualSignedWaveData.potentialWeight (I : Fin 3 × SourceIndex) (n : ℕ) (x : PhysicalGraphBounds.LiftPoint) : ℝ

Potential weight, given by sourceWeight I.2 n x.

Equations

• NavierStokes.ActualSignedWaveData.potentialWeight I n x = NavierStokes.ActualSignedWaveData.sourceWeight I.2 n x

theorem NavierStokes.ActualSignedWaveData.potential_amplitude_eq_source {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (i : Fin 3) (k : TorusInverse.Frequency) (I : PhysicalWaveSum.WaveIndex 1) (x : PhysicalGraphBounds.LiftPoint) : ((ActualSignedExterior.family s).potentialCopies CorrectionInitialization.ActualPrimary.slots ⋯ i).amplitude k I x = ChartScales.Q (↑I.1).1 ^ (-CorrectionInitialization.ActualPrimary.h) • potentialSource s (i, ⟨I.1, (I, k)⟩) (↑I.1).1 x

theorem NavierStokes.ActualSignedWaveData.pressure_amplitude_eq_source {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (k : TorusInverse.Frequency) (I : PhysicalWaveSum.WaveIndex 1) (x : PhysicalGraphBounds.LiftPoint) : ((ActualSignedExterior.family s).pressureCopies CorrectionInitialization.ActualPrimary.slots ⋯).amplitude k I x = ChartScales.Q (↑I.1).1 ^ (-(2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h)) • pressureSource s ⟨I.1, (I, k)⟩ (↑I.1).1 x

theorem NavierStokes.ActualSignedWaveData.potential_source_bounds {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) {α : ℝ} (hs : LocalPhysicalCopyBounds.LocalSourceBounds ActualPrimaryBounds.strip CorrectionInitialization.ActualPrimary.h α (fun (x : SourceIndex) (x_1 : ℕ) (y : ActualPrimaryBounds.Point) => √(ActualPrimaryBounds.strip.zeta y)) (DependentSignedPhysicalFamily.jointSource ((ActualSignedExterior.family s).potentialSource CorrectionInitialization.ActualPrimary.slots ⋯))) : LocalPhysicalCopyBounds.LocalSourceBounds sourceStrip CorrectionInitialization.ActualPrimary.h α potentialWeight (potentialSource s)

theorem NavierStokes.ActualSignedWaveData.pressure_source_bounds {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) {α : ℝ} (hs : LocalPhysicalCopyBounds.LocalSourceBounds ActualPrimaryBounds.strip CorrectionInitialization.ActualPrimary.h α (fun (x : SourceIndex) (x_1 : ℕ) (y : ActualPrimaryBounds.Point) => √(ActualPrimaryBounds.strip.zeta y)) (DependentSignedPhysicalFamily.jointSource ((ActualSignedExterior.family s).pressureSource CorrectionInitialization.ActualPrimary.slots ⋯))) : LocalPhysicalCopyBounds.LocalSourceBounds sourceStrip CorrectionInitialization.ActualPrimary.h α sourceWeight (pressureSource s)

noncomputable def NavierStokes.ActualSignedWaveData.potentialOfNative {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (hgeo : (L : ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.family s).active) → ActualSignedPhysicalData.ReferenceGeometry CorrectionInitialization.ActualPrimary.slots ((ActualSignedExterior.family s).singleton L)) (hn : ∀ (L : ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.family s).active), ActualSignedPhysicalData.NativeRegular CorrectionInitialization.ActualPrimary.slots ⋯ ((ActualSignedExterior.family s).singleton L)) {α : ℝ} (hs : LocalPhysicalCopyBounds.LocalSourceBounds ActualPrimaryBounds.strip CorrectionInitialization.ActualPrimary.h α (fun (x : SourceIndex) (x_1 : ℕ) (y : ActualPrimaryBounds.Point) => √(ActualPrimaryBounds.strip.zeta y)) (DependentSignedPhysicalFamily.jointSource ((ActualSignedExterior.family s).potentialSource CorrectionInitialization.ActualPrimary.slots ⋯))) : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h PhysicalGraphBounds.LiftPoint (Fin 3 × SourceIndex) TorusInverse.Frequency (Fin 3)

The physical potential datum is assembled once over all source labels. The source estimate and profile constants are chosen before those labels.

Equations

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

noncomputable def NavierStokes.ActualSignedWaveData.pressureOfNative {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (hgeo : (L : ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.family s).active) → ActualSignedPhysicalData.ReferenceGeometry CorrectionInitialization.ActualPrimary.slots ((ActualSignedExterior.family s).singleton L)) (hn : ∀ (L : ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.family s).active), ActualSignedPhysicalData.NativeRegular CorrectionInitialization.ActualPrimary.slots ⋯ ((ActualSignedExterior.family s).singleton L)) {α : ℝ} (hs : LocalPhysicalCopyBounds.LocalSourceBounds ActualPrimaryBounds.strip CorrectionInitialization.ActualPrimary.h α (fun (x : SourceIndex) (x_1 : ℕ) (y : ActualPrimaryBounds.Point) => √(ActualPrimaryBounds.strip.zeta y)) (DependentSignedPhysicalFamily.jointSource ((ActualSignedExterior.family s).pressureSource CorrectionInitialization.ActualPrimary.slots ⋯))) : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h PhysicalGraphBounds.LiftPoint SourceIndex TorusInverse.Frequency Unit

Pressure of native, bundling lowerRadius, upperRadius, nativeWidth, slowBound and the required compatibility proofs.

Equations

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

@[simp]

theorem NavierStokes.ActualSignedWaveData.potentialOfNative_alpha {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (hgeo : (L : ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.family s).active) → ActualSignedPhysicalData.ReferenceGeometry CorrectionInitialization.ActualPrimary.slots ((ActualSignedExterior.family s).singleton L)) (hn : ∀ (L : ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.family s).active), ActualSignedPhysicalData.NativeRegular CorrectionInitialization.ActualPrimary.slots ⋯ ((ActualSignedExterior.family s).singleton L)) {α : ℝ} (hpotential : LocalPhysicalCopyBounds.LocalSourceBounds ActualPrimaryBounds.strip CorrectionInitialization.ActualPrimary.h α (fun (x : SourceIndex) (x_1 : ℕ) (y : ActualPrimaryBounds.Point) => √(ActualPrimaryBounds.strip.zeta y)) (DependentSignedPhysicalFamily.jointSource ((ActualSignedExterior.family s).potentialSource CorrectionInitialization.ActualPrimary.slots ⋯))) : (potentialOfNative s hgeo hn hpotential).alpha = α

@[simp]

theorem NavierStokes.ActualSignedWaveData.pressureOfNative_alpha {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (hgeo : (L : ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.family s).active) → ActualSignedPhysicalData.ReferenceGeometry CorrectionInitialization.ActualPrimary.slots ((ActualSignedExterior.family s).singleton L)) (hn : ∀ (L : ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.family s).active), ActualSignedPhysicalData.NativeRegular CorrectionInitialization.ActualPrimary.slots ⋯ ((ActualSignedExterior.family s).singleton L)) {α : ℝ} (hpressure : LocalPhysicalCopyBounds.LocalSourceBounds ActualPrimaryBounds.strip CorrectionInitialization.ActualPrimary.h α (fun (x : SourceIndex) (x_1 : ℕ) (y : ActualPrimaryBounds.Point) => √(ActualPrimaryBounds.strip.zeta y)) (DependentSignedPhysicalFamily.jointSource ((ActualSignedExterior.family s).pressureSource CorrectionInitialization.ActualPrimary.slots ⋯))) : (pressureOfNative s hgeo hn hpressure).alpha = α

@[simp]

theorem NavierStokes.ActualSignedWaveData.potentialOfNative_shift {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (hgeo : (L : ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.family s).active) → ActualSignedPhysicalData.ReferenceGeometry CorrectionInitialization.ActualPrimary.slots ((ActualSignedExterior.family s).singleton L)) (hn : ∀ (L : ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.family s).active), ActualSignedPhysicalData.NativeRegular CorrectionInitialization.ActualPrimary.slots ⋯ ((ActualSignedExterior.family s).singleton L)) {α : ℝ} (hpotential : LocalPhysicalCopyBounds.LocalSourceBounds ActualPrimaryBounds.strip CorrectionInitialization.ActualPrimary.h α (fun (x : SourceIndex) (x_1 : ℕ) (y : ActualPrimaryBounds.Point) => √(ActualPrimaryBounds.strip.zeta y)) (DependentSignedPhysicalFamily.jointSource ((ActualSignedExterior.family s).potentialSource CorrectionInitialization.ActualPrimary.slots ⋯))) : (potentialOfNative s hgeo hn hpotential).shift = -CorrectionInitialization.ActualPrimary.h

@[simp]

theorem NavierStokes.ActualSignedWaveData.pressureOfNative_shift {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (hgeo : (L : ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.family s).active) → ActualSignedPhysicalData.ReferenceGeometry CorrectionInitialization.ActualPrimary.slots ((ActualSignedExterior.family s).singleton L)) (hn : ∀ (L : ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.family s).active), ActualSignedPhysicalData.NativeRegular CorrectionInitialization.ActualPrimary.slots ⋯ ((ActualSignedExterior.family s).singleton L)) {α : ℝ} (hpressure : LocalPhysicalCopyBounds.LocalSourceBounds ActualPrimaryBounds.strip CorrectionInitialization.ActualPrimary.h α (fun (x : SourceIndex) (x_1 : ℕ) (y : ActualPrimaryBounds.Point) => √(ActualPrimaryBounds.strip.zeta y)) (DependentSignedPhysicalFamily.jointSource ((ActualSignedExterior.family s).pressureSource CorrectionInitialization.ActualPrimary.slots ⋯))) : (pressureOfNative s hgeo hn hpressure).shift = -(2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h)

theorem NavierStokes.ActualSignedWaveData.potentialOfNative_vector_eq {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (hgeo : (L : ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.family s).active) → ActualSignedPhysicalData.ReferenceGeometry CorrectionInitialization.ActualPrimary.slots ((ActualSignedExterior.family s).singleton L)) (hn : ∀ (L : ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.family s).active), ActualSignedPhysicalData.NativeRegular CorrectionInitialization.ActualPrimary.slots ⋯ ((ActualSignedExterior.family s).singleton L)) {α : ℝ} (hpotential : LocalPhysicalCopyBounds.LocalSourceBounds ActualPrimaryBounds.strip CorrectionInitialization.ActualPrimary.h α (fun (x : SourceIndex) (x_1 : ℕ) (y : ActualPrimaryBounds.Point) => √(ActualPrimaryBounds.strip.zeta y)) (DependentSignedPhysicalFamily.jointSource ((ActualSignedExterior.family s).potentialSource CorrectionInitialization.ActualPrimary.slots ⋯))) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : (potentialOfNative s hgeo hn hpotential).vector w = ActualSignedExterior.potential s w

theorem NavierStokes.ActualSignedWaveData.pressureOfNative_pressure_eq {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (hgeo : (L : ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.family s).active) → ActualSignedPhysicalData.ReferenceGeometry CorrectionInitialization.ActualPrimary.slots ((ActualSignedExterior.family s).singleton L)) (hn : ∀ (L : ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.family s).active), ActualSignedPhysicalData.NativeRegular CorrectionInitialization.ActualPrimary.slots ⋯ ((ActualSignedExterior.family s).singleton L)) {α : ℝ} (hpressure : LocalPhysicalCopyBounds.LocalSourceBounds ActualPrimaryBounds.strip CorrectionInitialization.ActualPrimary.h α (fun (x : SourceIndex) (x_1 : ℕ) (y : ActualPrimaryBounds.Point) => √(ActualPrimaryBounds.strip.zeta y)) (DependentSignedPhysicalFamily.jointSource ((ActualSignedExterior.family s).pressureSource CorrectionInitialization.ActualPrimary.slots ⋯))) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : (pressureOfNative s hgeo hn hpressure).pressure w = ActualSignedExterior.pressure s w

theorem NavierStokes.ActualSignedWaveData.potentialOfNative_vector_germ {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (hgeo : (L : ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.family s).active) → ActualSignedPhysicalData.ReferenceGeometry CorrectionInitialization.ActualPrimary.slots ((ActualSignedExterior.family s).singleton L)) (hn : ∀ (L : ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.family s).active), ActualSignedPhysicalData.NativeRegular CorrectionInitialization.ActualPrimary.slots ⋯ ((ActualSignedExterior.family s).singleton L)) {α : ℝ} (hpotential : LocalPhysicalCopyBounds.LocalSourceBounds ActualPrimaryBounds.strip CorrectionInitialization.ActualPrimary.h α (fun (x : SourceIndex) (x_1 : ℕ) (y : ActualPrimaryBounds.Point) => √(ActualPrimaryBounds.strip.zeta y)) (DependentSignedPhysicalFamily.jointSource ((ActualSignedExterior.family s).potentialSource CorrectionInitialization.ActualPrimary.slots ⋯))) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : (potentialOfNative s hgeo hn hpotential).vector =ᶠ[nhds w] ActualSignedExterior.potential s

theorem NavierStokes.ActualSignedWaveData.pressureOfNative_pressure_germ {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (hgeo : (L : ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.family s).active) → ActualSignedPhysicalData.ReferenceGeometry CorrectionInitialization.ActualPrimary.slots ((ActualSignedExterior.family s).singleton L)) (hn : ∀ (L : ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.family s).active), ActualSignedPhysicalData.NativeRegular CorrectionInitialization.ActualPrimary.slots ⋯ ((ActualSignedExterior.family s).singleton L)) {α : ℝ} (hpressure : LocalPhysicalCopyBounds.LocalSourceBounds ActualPrimaryBounds.strip CorrectionInitialization.ActualPrimary.h α (fun (x : SourceIndex) (x_1 : ℕ) (y : ActualPrimaryBounds.Point) => √(ActualPrimaryBounds.strip.zeta y)) (DependentSignedPhysicalFamily.jointSource ((ActualSignedExterior.family s).pressureSource CorrectionInitialization.ActualPrimary.slots ⋯))) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : (pressureOfNative s hgeo hn hpressure).pressure =ᶠ[nhds w] ActualSignedExterior.pressure s

noncomputable def NavierStokes.ActualSignedWaveData.potentialFromResiduals {B N0 : ℕ} (u : CorrectionState.State LocalSignedRequest.Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b u.pressure) (α : ℝ) (hfixed : VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u = u) (hθ : WeightedClasses.MeanClass ActualInitialization.geometry.strip α (u.thetaResidual (CorrectionInitialization.ActualPrimary.commonContext B))) (hz : WeightedClasses.MeanClass ActualInitialization.geometry.strip α (u.axialResidual (CorrectionInitialization.ActualPrimary.commonContext B))) : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h PhysicalGraphBounds.LiftPoint (Fin 3 × SourceIndex) TorusInverse.Frequency (Fin 3)

Genuine primitive and measured residual data produce the entire potential record. Native regularity and native output bounds are derived.

Equations

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

noncomputable def NavierStokes.ActualSignedWaveData.pressureFromResiduals {B N0 : ℕ} (u : CorrectionState.State LocalSignedRequest.Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b u.pressure) (α : ℝ) (hfixed : VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u = u) (hθ : WeightedClasses.MeanClass ActualInitialization.geometry.strip α (u.thetaResidual (CorrectionInitialization.ActualPrimary.commonContext B))) (hz : WeightedClasses.MeanClass ActualInitialization.geometry.strip α (u.axialResidual (CorrectionInitialization.ActualPrimary.commonContext B))) : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h PhysicalGraphBounds.LiftPoint SourceIndex TorusInverse.Frequency Unit

Pressure from residuals, constructed using pressureOfNative.

Equations

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

@[simp]

theorem NavierStokes.ActualSignedWaveData.potentialFromResiduals_alpha {B N0 : ℕ} (u : CorrectionState.State LocalSignedRequest.Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b u.pressure) (α : ℝ) (hfixed : VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u = u) (hθ : WeightedClasses.MeanClass ActualInitialization.geometry.strip α (u.thetaResidual (CorrectionInitialization.ActualPrimary.commonContext B))) (hz : WeightedClasses.MeanClass ActualInitialization.geometry.strip α (u.axialResidual (CorrectionInitialization.ActualPrimary.commonContext B))) : (potentialFromResiduals u H hp α hfixed hθ hz).alpha = α

@[simp]

theorem NavierStokes.ActualSignedWaveData.pressureFromResiduals_alpha {B N0 : ℕ} (u : CorrectionState.State LocalSignedRequest.Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b u.pressure) (α : ℝ) (hfixed : VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u = u) (hθ : WeightedClasses.MeanClass ActualInitialization.geometry.strip α (u.thetaResidual (CorrectionInitialization.ActualPrimary.commonContext B))) (hz : WeightedClasses.MeanClass ActualInitialization.geometry.strip α (u.axialResidual (CorrectionInitialization.ActualPrimary.commonContext B))) : (pressureFromResiduals u H hp α hfixed hθ hz).alpha = α

@[simp]

theorem NavierStokes.ActualSignedWaveData.potentialFromResiduals_shift {B N0 : ℕ} (u : CorrectionState.State LocalSignedRequest.Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b u.pressure) (α : ℝ) (hfixed : VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u = u) (hθ : WeightedClasses.MeanClass ActualInitialization.geometry.strip α (u.thetaResidual (CorrectionInitialization.ActualPrimary.commonContext B))) (hz : WeightedClasses.MeanClass ActualInitialization.geometry.strip α (u.axialResidual (CorrectionInitialization.ActualPrimary.commonContext B))) : (potentialFromResiduals u H hp α hfixed hθ hz).shift = -CorrectionInitialization.ActualPrimary.h

@[simp]

theorem NavierStokes.ActualSignedWaveData.pressureFromResiduals_shift {B N0 : ℕ} (u : CorrectionState.State LocalSignedRequest.Point) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b u.pressure) (α : ℝ) (hfixed : VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u = u) (hθ : WeightedClasses.MeanClass ActualInitialization.geometry.strip α (u.thetaResidual (CorrectionInitialization.ActualPrimary.commonContext B))) (hz : WeightedClasses.MeanClass ActualInitialization.geometry.strip α (u.axialResidual (CorrectionInitialization.ActualPrimary.commonContext B))) : (pressureFromResiduals u H hp α hfixed hθ hz).shift = -(2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h)

noncomputable def NavierStokes.ActualSignedWaveData.cyclePotentialData {B N0 : ℕ} {σ : ℝ} (x : CorrectionStep.CycleState (Label B N0)) (R : ActualParticularMeanGain.Result x σ) : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h PhysicalGraphBounds.LiftPoint (Fin 3 × SourceIndex) TorusInverse.Frequency (Fin 3)

The post-particular theorem supplies every analytic hypothesis; the physical copies use its same reconstructed state and pressure primitive.

Equations

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

noncomputable def NavierStokes.ActualSignedWaveData.cyclePressureData {B N0 : ℕ} {σ : ℝ} (x : CorrectionStep.CycleState (Label B N0)) (R : ActualParticularMeanGain.Result x σ) : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h PhysicalGraphBounds.LiftPoint SourceIndex TorusInverse.Frequency Unit

Cycle pressure data, constructed using pressureFromResiduals.

Equations

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

@[simp]

theorem NavierStokes.ActualSignedWaveData.cyclePotentialData_alpha {B N0 : ℕ} {σ : ℝ} (x : CorrectionStep.CycleState (Label B N0)) (R : ActualParticularMeanGain.Result x σ) : (cyclePotentialData x R).alpha = 1 + σ - ChartScales.kappa

@[simp]

theorem NavierStokes.ActualSignedWaveData.cyclePressureData_alpha {B N0 : ℕ} {σ : ℝ} (x : CorrectionStep.CycleState (Label B N0)) (R : ActualParticularMeanGain.Result x σ) : (cyclePressureData x R).alpha = 1 + σ - ChartScales.kappa

@[simp]

theorem NavierStokes.ActualSignedWaveData.cyclePotentialData_shift {B N0 : ℕ} {σ : ℝ} (x : CorrectionStep.CycleState (Label B N0)) (R : ActualParticularMeanGain.Result x σ) : (cyclePotentialData x R).shift = -CorrectionInitialization.ActualPrimary.h

@[simp]

theorem NavierStokes.ActualSignedWaveData.cyclePressureData_shift {B N0 : ℕ} {σ : ℝ} (x : CorrectionStep.CycleState (Label B N0)) (R : ActualParticularMeanGain.Result x σ) : (cyclePressureData x R).shift = -(2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h)

theorem NavierStokes.ActualSignedWaveData.cyclePotentialData_eq {B N0 : ℕ} {σ : ℝ} (x : CorrectionStep.CycleState (Label B N0)) (R : ActualParticularMeanGain.Result x σ) : Set.EqOn (cyclePotentialData x R).vector (ActualSignedExterior.cyclePotential x ⋯ ⋯) PhysicalWaveSum.preterminal

theorem NavierStokes.ActualSignedWaveData.cyclePressureData_eq {B N0 : ℕ} {σ : ℝ} (x : CorrectionStep.CycleState (Label B N0)) (R : ActualParticularMeanGain.Result x σ) : Set.EqOn (cyclePressureData x R).pressure (ActualSignedExterior.cyclePressure x ⋯ ⋯) PhysicalWaveSum.preterminal

theorem NavierStokes.ActualSignedWaveData.cyclePotentialData_germ {B N0 : ℕ} {σ : ℝ} (x : CorrectionStep.CycleState (Label B N0)) (R : ActualParticularMeanGain.Result x σ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : (cyclePotentialData x R).vector =ᶠ[nhds w] ActualSignedExterior.cyclePotential x ⋯ ⋯

theorem NavierStokes.ActualSignedWaveData.cyclePressureData_germ {B N0 : ℕ} {σ : ℝ} (x : CorrectionStep.CycleState (Label B N0)) (R : ActualParticularMeanGain.Result x σ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : (cyclePressureData x R).pressure =ᶠ[nhds w] ActualSignedExterior.cyclePressure x ⋯ ⋯

theorem NavierStokes.ActualSignedWaveData.cyclePotential_bound {B N0 : ℕ} {σ : ℝ} (x : CorrectionStep.CycleState (Label B N0)) (R : ActualParticularMeanGain.Result x σ) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ PhysicalWaveSum.preterminal, PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ 1 → ‖iteratedFDeriv ℝ m (ActualSignedExterior.cyclePotential x ⋯ ⋯) w‖ ≤ C * PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ^ (CorrectionInitialization.ActualPrimary.h * (1 + σ - ChartScales.kappa) - PhysicalClassBounds.physicalLoss CorrectionInitialization.ActualPrimary.h (-CorrectionInitialization.ActualPrimary.h) m)

A consequence for the original signed potential, including every ambient time and spatial derivative.

theorem NavierStokes.ActualSignedWaveData.cyclePressure_bound {B N0 : ℕ} {σ : ℝ} (x : CorrectionStep.CycleState (Label B N0)) (R : ActualParticularMeanGain.Result x σ) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ PhysicalWaveSum.preterminal, PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ 1 → ‖iteratedFDeriv ℝ m (ActualSignedExterior.cyclePressure x ⋯ ⋯) w‖ ≤ C * PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ^ (CorrectionInitialization.ActualPrimary.h * (1 + σ - ChartScales.kappa) - PhysicalClassBounds.physicalLoss CorrectionInitialization.ActualPrimary.h (-(2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h)) m)

The actual infinite stage sequence

theorem NavierStokes.ActualSignedWaveData.stageResult (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) : ActualParticularMeanGain.Result (ActualCyclePreservation.state B N0 j) (ActualIterationLedger.sigma j)

noncomputable def NavierStokes.ActualSignedWaveData.signedInputs (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) : GluedStageEstimates.SignedInputs PhysicalGraphBounds.LiftPoint SourceIndex TorusInverse.Frequency

The actual signed part of the schedule. There is no input WaveData, physical bound or native output-regularity hypothesis.

Equations

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

theorem NavierStokes.ActualSignedWaveData.signedInputs_potential_eq (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) : Set.EqOn ((signedInputs B N0 hN).potential j).vector (ActualSignedExterior.cyclePotential (ActualCyclePreservation.state B N0 j) ⋯ ⋯) PhysicalWaveSum.preterminal

theorem NavierStokes.ActualSignedWaveData.signedInputs_pressure_eq (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) : Set.EqOn ((signedInputs B N0 hN).pressure j).pressure (ActualSignedExterior.cyclePressure (ActualCyclePreservation.state B N0 j) ⋯ ⋯) PhysicalWaveSum.preterminal