Related estimates used together by the same construction modules.

Reference geometry of the actual signed family

Every singleton retains the original primary label, phase, native view, and current-state request. Reindexing its dependent payload changes only the proof of the reference-band equality. The seven reference-geometry fields below come from these primitive identities; no equality of output physical fields or native regularity is assumed.

@[reducible, inline]

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

Label: an abbreviation for ActualSignedPhysicalBinding.Label.

Equations

• NavierStokes.ActualSignedReferenceGeometry.Label = NavierStokes.ActualSignedPhysicalBinding.Label

theorem NavierStokes.ActualSignedReferenceGeometry.singleton_index_eq (f : DependentSignedPhysicalFamily.Family) (L : ActualSignedPhysicalData.NativeLabel f.active) (K : ActualSignedPhysicalData.NativeLabel (f.singleton L).active) : K = f.singletonLabel L

theorem NavierStokes.ActualSignedReferenceGeometry.reband_exponent {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {P : PhysicalSignedWave.PrimaryData U} {n m : ℕ} (he : n = m) (V : P.Views n) (s : V.StateData) : (ActualSignedExterior.rebandPayload he V s).fst.exponent = V.exponent

theorem NavierStokes.ActualSignedReferenceGeometry.reband_scale {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {P : PhysicalSignedWave.PrimaryData U} {n m : ℕ} (he : n = m) (V : P.Views n) (s : V.StateData) : (ActualSignedExterior.rebandPayload he V s).fst.referenceScale = V.referenceScale

theorem NavierStokes.ActualSignedReferenceGeometry.reband_cover {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {P : PhysicalSignedWave.PrimaryData U} {n m : ℕ} (he : n = m) (V : P.Views n) (s : V.StateData) : (ActualSignedExterior.rebandPayload he V s).fst.referenceCover = V.referenceCover

noncomputable def NavierStokes.ActualSignedReferenceGeometry.singletonGeometryOfAngular {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (ha : (l : ActualSignedPhysicalBinding.Label B N0) → (ActualSignedPhysicalBinding.primary l).Angular (s l).referenceRequest (ActualSignedPhysicalBinding.reference l)) (L : ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.family s).active) : ActualSignedPhysicalData.ReferenceGeometry CorrectionInitialization.ActualPrimary.slots ((ActualSignedExterior.family s).singleton L)

The geometric part is uniform over native state families. The sole state-dependent primitive here is angular invariance of the request. singletonGeometry below constructs it for the actual measured request.

Equations

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

noncomputable def NavierStokes.ActualSignedReferenceGeometry.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 (ActualSignedExterior.family fun (l : Label B N0) => ActualSignedPhysicalBinding.nativeStateData l P u H hp).active) : ActualSignedPhysicalData.ReferenceGeometry CorrectionInitialization.ActualPrimary.slots ((ActualSignedExterior.family fun (l : Label B N0) => ActualSignedPhysicalBinding.nativeStateData l P u H hp).singleton L)

All seven fields for the canonical measured-request family, retaining the actual current state and the same prepared primary choice.

Equations

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

noncomputable def NavierStokes.ActualSignedReferenceGeometry.nativeSingletonGeometry {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) : ActualSignedPhysicalData.ReferenceGeometry CorrectionInitialization.ActualPrimary.slots ((ActualSignedExterior.family fun (k : Label B N0) => ActualSignedPhysicalBinding.nativeStateData k P u H hp).singleton (ActualSignedExterior.nativeLabel l))

Original-label form, suitable for the per-label current-chart coherence theorems.

Equations

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

noncomputable def NavierStokes.ActualSignedReferenceGeometry.cycleSingletonGeometry {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) ((ActualCycleParameters.fixedParameters B N0).afterParticular x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state)) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b ((ActualCycleParameters.fixedParameters B N0).afterParticular x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state).pressure) (L : ActualSignedPhysicalData.NativeLabel (ActualSignedExterior.cycleFamily x H hp).active) : ActualSignedPhysicalData.ReferenceGeometry CorrectionInitialization.ActualPrimary.slots ((ActualSignedExterior.cycleFamily x H hp).singleton L)

The actual post-particular cycle family is definitionally the same family used above, including its state and request.

Equations

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

noncomputable def NavierStokes.ActualSignedReferenceGeometry.cycleNativeGeometry {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) ((ActualCycleParameters.fixedParameters B N0).afterParticular x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state)) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b ((ActualCycleParameters.fixedParameters B N0).afterParticular x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state).pressure) (l : Label B N0) : ActualSignedPhysicalData.ReferenceGeometry CorrectionInitialization.ActualPrimary.slots ((ActualSignedExterior.cycleFamily x H hp).singleton (ActualSignedExterior.nativeLabel l))

Cycle native geometry, given by cycleSingletonGeometry x H hp (ActualSignedExterior.nativeLabel l).

Equations

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

Native regularity of the actual signed cut sources

The dyadic factor is retained literally. The estimates below first turn the actual radial flat-weight classes into bounded jets, including at the radial edges; no smooth continuation of the unmasked request at a dyadic face is assumed.

Exact native-source factorization for the actual signed family

The primitive state, primary choice, request, and lattice copy are unchanged. The identities retain the one Gaussian already present in the native cutoff. They hold on the whole native coordinate space, before any smoothness claim or own-band/harmonic gate is applied.

@[reducible, inline]

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

Label: an abbreviation for ActualSignedPhysicalBinding.Label.

Equations

• NavierStokes.ActualSignedUnmaskedBinding.Label = NavierStokes.ActualSignedPhysicalBinding.Label

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

abbrev NavierStokes.ActualSignedUnmaskedBinding.Point : Type

Point: an abbreviation for LocalSignedRequest.Point.

Equations

• NavierStokes.ActualSignedUnmaskedBinding.Point = NavierStokes.LocalSignedRequest.Point

@[reducible, inline]

abbrev NavierStokes.ActualSignedUnmaskedBinding.Cylinder : Type

Cylinder: an abbreviation for ActualSignedPhysicalBinding.Cylinder.

Equations

• NavierStokes.ActualSignedUnmaskedBinding.Cylinder = NavierStokes.ActualSignedPhysicalBinding.Cylinder

@[reducible, inline]

abbrev NavierStokes.ActualSignedUnmaskedBinding.Native : Type

Native: an abbreviation for ActualSignedPhysicalData.Native.

Equations

• NavierStokes.ActualSignedUnmaskedBinding.Native = NavierStokes.ActualSignedPhysicalData.Native

@[reducible, inline]

abbrev NavierStokes.ActualSignedUnmaskedBinding.Copy : Type

Copy: an abbreviation for TorusInverse.Frequency.

Equations

• NavierStokes.ActualSignedUnmaskedBinding.Copy = NavierStokes.TorusInverse.Frequency

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

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

Equations

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

noncomputable def NavierStokes.ActualSignedUnmaskedBinding.states {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State 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

States, given by ActualSignedPhysicalBinding.nativeStateData l P u H hp.

Equations

• NavierStokes.ActualSignedUnmaskedBinding.states P u H hp l = NavierStokes.ActualSignedPhysicalBinding.nativeStateData l P u H hp

noncomputable def NavierStokes.ActualSignedUnmaskedBinding.branch {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State 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 : NativeLabel B N0) : ActualSignedPhysicalData.SignedFamily ((ActualSignedExterior.family (states P u H hp)).domain L)

Branch, given by (ActualSignedExterior.family (states P u H hp)).singleton L.

Equations

• NavierStokes.ActualSignedUnmaskedBinding.branch P u H hp L = (NavierStokes.ActualSignedExterior.family (NavierStokes.ActualSignedUnmaskedBinding.states P u H hp)).singleton L

noncomputable def NavierStokes.ActualSignedUnmaskedBinding.branchLabel {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State 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 : NativeLabel B N0) : ActualSignedPhysicalData.NativeLabel (branch P u H hp L).active

Branch label, given by (ActualSignedExterior.family (states P u H hp)).singletonLabel L.

Equations

• NavierStokes.ActualSignedUnmaskedBinding.branchLabel P u H hp L = (NavierStokes.ActualSignedExterior.family (NavierStokes.ActualSignedUnmaskedBinding.states P u H hp)).singletonLabel L

theorem NavierStokes.ActualSignedUnmaskedBinding.branch_request {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State 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 : NativeLabel B N0) : ((branch P u H hp L).state (branchLabel P u H hp L)).referenceRequest = (ActualSignedPhysicalBinding.nativeStateData (ActualSignedExterior.actualLabel L) P u H hp).referenceRequest

theorem NavierStokes.ActualSignedUnmaskedBinding.layout_eq {B N0 : ℕ} (L : NativeLabel B N0) : ActualSignedPhysicalData.layout CorrectionInitialization.ActualPrimary.slots ⋯ L.val ⋯ 0 = ActualSignedPhysicalBinding.layout (ActualSignedExterior.actualLabel L)

theorem NavierStokes.ActualSignedUnmaskedBinding.unit_reference {B N0 : ℕ} (l : Label B N0) (k : Copy) (x : Cylinder) : ActualPeriodizedSignedRealization.nativeUnit (ActualSignedPhysicalBinding.primary l) (ActualSignedPhysicalBinding.layout l) (ActualSignedPhysicalBinding.nativeViews l) l.2 k (ActualSignedPhysicalBinding.reference l) x = ActualPeriodizedSignedRealization.referenceNativeUnit (ActualSignedPhysicalBinding.primary l) (ActualSignedPhysicalBinding.layout l) l.2 (ActualSignedPhysicalBinding.reference l) k x

theorem NavierStokes.ActualSignedUnmaskedBinding.reference_amplitude_formula {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State 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) (x : Cylinder) : (ActualSignedPhysicalBinding.referenceCopies l P u H hp).amplitude (ActualSignedPhysicalBinding.reference l) k x = ActualPeriodizedSignedRealization.referenceScalar (ActualSignedPhysicalBinding.primary l) (ActualSignedPhysicalBinding.nativeStateData l P u H hp).referenceRequest l.2 (ActualSignedPhysicalBinding.reference l) x • CurlClassBounds.complexify (ActualPeriodizedSignedRealization.referenceNativeUnit (ActualSignedPhysicalBinding.primary l) (ActualSignedPhysicalBinding.layout l) l.2 (ActualSignedPhysicalBinding.reference l) k x)

theorem NavierStokes.ActualSignedUnmaskedBinding.reference_pressure_formula {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State 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) (x : Cylinder) : (ActualSignedPhysicalBinding.referenceCopies l P u H hp).pressure (ActualSignedPhysicalBinding.reference l) k x = ActualPeriodizedSignedRealization.referenceScalar (ActualSignedPhysicalBinding.primary l) (ActualSignedPhysicalBinding.nativeStateData l P u H hp).referenceRequest l.2 (ActualSignedPhysicalBinding.reference l) x • 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) x) ((ActualSignedPhysicalBinding.primary l).normalMotion (ActualSignedPhysicalBinding.reference l) x) ((ActualSignedPhysicalBinding.primary l).action (ActualSignedPhysicalBinding.reference l) x) (ActualPeriodizedSignedRealization.referenceNativeUnit (ActualSignedPhysicalBinding.primary l) (ActualSignedPhysicalBinding.layout l) l.2 (ActualSignedPhysicalBinding.reference l) k x)

theorem NavierStokes.ActualSignedUnmaskedBinding.branch_amplitude_reference {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State 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 : NativeLabel B N0) (k : Copy) (x : Cylinder) : ActualSignedPhysicalData.rawSignedAmplitude CorrectionInitialization.ActualPrimary.slots ⋯ (branch P u H hp L) (branchLabel P u H hp L) k x = (ActualSignedPhysicalBinding.referenceCopies (ActualSignedExterior.actualLabel L) P u H hp).amplitude (ActualSignedPhysicalBinding.reference (ActualSignedExterior.actualLabel L)) k x

theorem NavierStokes.ActualSignedUnmaskedBinding.branch_pressure_reference {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State 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 : NativeLabel B N0) (k : Copy) (x : Cylinder) : ActualSignedPhysicalData.rawPressure CorrectionInitialization.ActualPrimary.slots ⋯ (branch P u H hp L) (branchLabel P u H hp L) k x = (ActualSignedPhysicalBinding.referenceCopies (ActualSignedExterior.actualLabel L) P u H hp).pressure (ActualSignedPhysicalBinding.reference (ActualSignedExterior.actualLabel L)) k x

theorem NavierStokes.ActualSignedUnmaskedBinding.branch_potential_reference {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State 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 : NativeLabel B N0) (k : Copy) (x : Cylinder) : ActualSignedPhysicalData.rawPotential CorrectionInitialization.ActualPrimary.slots ⋯ (branch P u H hp L) (branchLabel P u H hp L) k x = (ActualSignedPhysicalData.potentialMap ((ActualSignedPhysicalBinding.primary (ActualSignedExterior.actualLabel L)).base.frequency (ActualSignedPhysicalBinding.reference (ActualSignedExterior.actualLabel L))) ((ActualSignedPhysicalBinding.primary (ActualSignedExterior.actualLabel L)).base.normal (ActualSignedPhysicalBinding.primary (ActualSignedExterior.actualLabel L)).strip (ActualSignedPhysicalBinding.primary (ActualSignedExterior.actualLabel L)).directions (ActualSignedPhysicalBinding.reference (ActualSignedExterior.actualLabel L)) x)) ((ActualSignedPhysicalBinding.referenceCopies (ActualSignedExterior.actualLabel L) P u H hp).amplitude (ActualSignedPhysicalBinding.reference (ActualSignedExterior.actualLabel L)) k x)

theorem NavierStokes.ActualSignedUnmaskedBinding.waveMask_reference {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State 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 : NativeLabel B N0) (k : Copy) (x : Cylinder) : ActualSignedPhysicalData.waveMask CorrectionInitialization.ActualPrimary.slots L.val ((ActualSignedPhysicalData.geometry CorrectionInitialization.ActualPrimary.slots L.val 0).coordinates k x.1.2.2) = (ActualSignedPhysicalBinding.referenceCopies (ActualSignedExterior.actualLabel L) P u H hp).cutoff (ActualSignedPhysicalBinding.reference (ActualSignedExterior.actualLabel L)) k x

theorem NavierStokes.ActualSignedUnmaskedBinding.cylinder_potential_factor {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State 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 : NativeLabel B N0) (k : Copy) (x : Cylinder) : ActualSignedPhysicalData.waveMask CorrectionInitialization.ActualPrimary.slots L.val ((ActualSignedPhysicalData.geometry CorrectionInitialization.ActualPrimary.slots L.val 0).coordinates k x.1.2.2) • ActualSignedPhysicalData.rawPotential CorrectionInitialization.ActualPrimary.slots ⋯ (branch P u H hp L) (branchLabel P u H hp L) k x = ActualSignedUnmaskedBounds.dyadicFactor (ActualSignedExterior.actualLabel L) k (ActualSignedUnmaskedBounds.reference (ActualSignedExterior.actualLabel L)) ((ActualSignedPhysicalBinding.toCommonCylinder (ActualSignedExterior.actualLabel L)) x) • ActualSignedUnmaskedBounds.potential (request P u) (ActualSignedExterior.actualLabel L) k (ActualSignedUnmaskedBounds.reference (ActualSignedExterior.actualLabel L)) ((ActualSignedPhysicalBinding.toCommonCylinder (ActualSignedExterior.actualLabel L)) x)

The scalar factor is removed after the one existing native Gaussian has been applied. No additional cutoff is introduced.

theorem NavierStokes.ActualSignedUnmaskedBinding.cylinder_pressure_factor {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State 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 : NativeLabel B N0) (k : Copy) (x : Cylinder) : ActualSignedPhysicalData.waveMask CorrectionInitialization.ActualPrimary.slots L.val ((ActualSignedPhysicalData.geometry CorrectionInitialization.ActualPrimary.slots L.val 0).coordinates k x.1.2.2) • ActualSignedPhysicalData.rawPressure CorrectionInitialization.ActualPrimary.slots ⋯ (branch P u H hp L) (branchLabel P u H hp L) k x = ActualSignedUnmaskedBounds.dyadicFactor (ActualSignedExterior.actualLabel L) k (ActualSignedUnmaskedBounds.reference (ActualSignedExterior.actualLabel L)) ((ActualSignedPhysicalBinding.toCommonCylinder (ActualSignedExterior.actualLabel L)) x) • ActualSignedUnmaskedBounds.pressure (request P u) (ActualSignedExterior.actualLabel L) k (ActualSignedUnmaskedBounds.reference (ActualSignedExterior.actualLabel L)) ((ActualSignedPhysicalBinding.toCommonCylinder (ActualSignedExterior.actualLabel L)) x)

theorem NavierStokes.ActualSignedUnmaskedBinding.native_potential_factor {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State 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 : NativeLabel B N0) (k : Copy) (y : Native) : ActualSignedPhysicalData.waveMask CorrectionInitialization.ActualPrimary.slots L.val ((ActualSignedPhysicalData.geometry CorrectionInitialization.ActualPrimary.slots L.val 0).coordinates k y.2.2) • ActualSignedPhysicalData.rawPotential CorrectionInitialization.ActualPrimary.slots ⋯ (branch P u H hp L) (branchLabel P u H hp L) k (ActualSignedPhysicalData.nativeCylinder y) = SquaredPartition.dyadicProfile (SimilarityCoordinates.coordinateQ (2 * CorrectionInitialization.ActualPrimary.h) y.2.1) • ActualSignedUnmaskedBounds.potential (request P u) (ActualSignedExterior.actualLabel L) k (ActualSignedUnmaskedBounds.reference (ActualSignedExterior.actualLabel L)) ((ActualSignedPhysicalBinding.toCommonCylinder (ActualSignedExterior.actualLabel L)) (ActualSignedPhysicalData.nativeCylinder y))

theorem NavierStokes.ActualSignedUnmaskedBinding.native_pressure_factor {B N0 : ℕ} (P : SignedStressPrimitive.Patch) (u : CorrectionState.State 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 : NativeLabel B N0) (k : Copy) (y : Native) : ActualSignedPhysicalData.waveMask CorrectionInitialization.ActualPrimary.slots L.val ((ActualSignedPhysicalData.geometry CorrectionInitialization.ActualPrimary.slots L.val 0).coordinates k y.2.2) • ActualSignedPhysicalData.rawPressure CorrectionInitialization.ActualPrimary.slots ⋯ (branch P u H hp L) (branchLabel P u H hp L) k (ActualSignedPhysicalData.nativeCylinder y) = SquaredPartition.dyadicProfile (SimilarityCoordinates.coordinateQ (2 * CorrectionInitialization.ActualPrimary.h) y.2.1) • ActualSignedUnmaskedBounds.pressure (request P u) (ActualSignedExterior.actualLabel L) k (ActualSignedUnmaskedBounds.reference (ActualSignedExterior.actualLabel L)) ((ActualSignedPhysicalBinding.toCommonCylinder (ActualSignedExterior.actualLabel L)) (ActualSignedPhysicalData.nativeCylinder y))

Literal flat dyadic products from locally bounded interior jets

The unmasked factor is smooth only in the open dyadic band. Its actual interior jets are locally bounded at each face. Flatness of the fixed cutoff then proves smoothness and vanishing of all jets of the literal product, without assigning new values to the unmasked factor outside the band.

def NavierStokes.FlatDyadicExtension.LocalJetBounds {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (Ω : Set D) (q : D → ℝ) (g : D → E) : Prop

The constant and neighborhood may depend on the face point and finite jet order. Values and derivatives of g outside the open band are unused.

Equations

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

theorem NavierStokes.FlatDyadicExtension.tensor_hasFDerivAt {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {f : D → E} {x : D} (hf : ContDiffAt ℝ (↑⊤) f x) (n : ℕ) : HasFDerivAt (iteratedFDeriv ℝ n f) (iteratedFDeriv ℝ (n + 1) f x).curryLeft x

theorem NavierStokes.FlatDyadicExtension.flat_jet_isLittleO {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {f : D → E} {x : D} (hf : ContDiffAt ℝ (↑⊤) f x) (hz : ∀ (n : ℕ), iteratedFDeriv ℝ n f x = 0) (n : ℕ) : iteratedFDeriv ℝ n f =o[nhds x] fun (y : D) => y - x

One extra zero tensor makes each flat jet little-o of ambient distance.

theorem NavierStokes.FlatDyadicExtension.product_jet_extension_isLittleO {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : Set D} (hΩ : IsOpen Ω) {q φ : D → ℝ} (hq : ContinuousOn q Ω) (hφ : ContDiffOn ℝ (↑⊤) φ Ω) {a b : ℝ} {g : D → E} (hg : ContDiffOn ℝ (↑⊤) g (WaveEdgeExtension.windowDomain Ω q a b)) {x : D} (hx : x ∈ Ω) (hflat : ∀ (n : ℕ), iteratedFDeriv ℝ n φ x = 0) (m : ℕ) (hB : ∃ (C : ℝ), 0 ≤ C ∧ ∀ᶠ (y : D) in nhds x, y ∈ WaveEdgeExtension.windowDomain Ω q a b → ∀ j ≤ m, ‖iteratedFDeriv ℝ j g y‖ ≤ C) : WaveEdgeExtension.extension q a b (iteratedFDeriv ℝ m fun (y : D) => φ y • g y) =o[nhds x] fun (y : D) => y - x

A flat smooth scalar times a factor with locally bounded interior jets has little-o interior product jets. Zero extension needs no source values or source regularity on the other side of the boundary.

A Taylor family for the literal window extension

def NavierStokes.FlatDyadicExtension.SmallOJets {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (Ω : Set D) (q : D → ℝ) (a b : ℝ) (f : D → E) : Prop

Small O jets, given by ∀ n : ℕ, ∀ x ∈ Ω, q x = a ∨ q x = b → extension q a b (iteratedFDeriv ℝ n f) =o[𝓝 x] (fun y => y - x).

Equations

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

theorem NavierStokes.FlatDyadicExtension.hasFDerivAt_extension_zero {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {q : D → ℝ} {a b : ℝ} {f : D → E} {x : D} (hx : x ∉ WaveEdgeExtension.window q a b) (hf : WaveEdgeExtension.extension q a b f =o[nhds x] fun (y : D) => y - x) : HasFDerivAt (WaveEdgeExtension.extension q a b f) 0 x

theorem NavierStokes.FlatDyadicExtension.extendedJets_hasFDerivAt {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : Set D} (hΩ : IsOpen Ω) {q : D → ℝ} (hq : ContinuousOn q Ω) {a b : ℝ} {f : D → E} (hf : ContDiffOn ℝ (↑⊤) f (WaveEdgeExtension.windowDomain Ω q a b)) (hB : SmallOJets Ω q a b f) (n : ℕ) {x : D} (hx : x ∈ Ω) : HasFDerivAt (fun (y : D) => WaveEdgeExtension.extendedJets q a b f y n) (WaveEdgeExtension.extendedJets q a b f x (n + 1)).curryLeft x

theorem NavierStokes.FlatDyadicExtension.hasFTaylorSeriesUpToOn_extension {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : Set D} (hΩ : IsOpen Ω) {q : D → ℝ} (hq : ContinuousOn q Ω) {a b : ℝ} {f : D → E} (hf : ContDiffOn ℝ (↑⊤) f (WaveEdgeExtension.windowDomain Ω q a b)) (hB : SmallOJets Ω q a b f) : HasFTaylorSeriesUpToOn (↑⊤) (WaveEdgeExtension.extension q a b f) (WaveEdgeExtension.extendedJets q a b f) Ω

theorem NavierStokes.FlatDyadicExtension.iteratedFDeriv_extension {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : Set D} (hΩ : IsOpen Ω) {q : D → ℝ} (hq : ContinuousOn q Ω) {a b : ℝ} {f : D → E} (hf : ContDiffOn ℝ (↑⊤) f (WaveEdgeExtension.windowDomain Ω q a b)) (hB : SmallOJets Ω q a b f) (n : ℕ) {x : D} (hx : x ∈ Ω) : iteratedFDeriv ℝ n (WaveEdgeExtension.extension q a b f) x = WaveEdgeExtension.extension q a b (iteratedFDeriv ℝ n f) x

The fixed dyadic cutoff

theorem NavierStokes.FlatDyadicExtension.dyadicProduct_eq_extension {D : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (q : D → ℝ) (g : D → E) : (fun (x : D) => SquaredPartition.dyadicProfile (q x) • g x) = WaveEdgeExtension.extension q (1 / 2) 2 fun (x : D) => SquaredPartition.dyadicProfile (q x) • g x

theorem NavierStokes.FlatDyadicExtension.dyadic_product_smooth_and_flat {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : Set D} (hΩ : IsOpen Ω) {q : D → ℝ} (hq : ContDiffOn ℝ (↑⊤) q Ω) {g : D → E} (hg : ContDiffOn ℝ (↑⊤) g (WaveEdgeExtension.windowDomain Ω q (1 / 2) 2)) (hB : LocalJetBounds Ω q g) : ContDiffOn ℝ (↑⊤) (fun (x : D) => SquaredPartition.dyadicProfile (q x) • g x) Ω ∧ ∀ x ∈ Ω, q x = 1 / 2 ∨ q x = 2 → ∀ (n : ℕ), iteratedFDeriv ℝ n (fun (y : D) => SquaredPartition.dyadicProfile (q y) • g y) x = 0

Main endpoint: the literal product is smooth on the ambient open domain and every actual tensor vanishes at either dyadic face.

theorem NavierStokes.FlatDyadicExtension.dyadic_product_contDiffOn {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : Set D} (hΩ : IsOpen Ω) {q : D → ℝ} (hq : ContDiffOn ℝ (↑⊤) q Ω) {g : D → E} (hg : ContDiffOn ℝ (↑⊤) g (WaveEdgeExtension.windowDomain Ω q (1 / 2) 2)) (hB : LocalJetBounds Ω q g) : ContDiffOn ℝ (↑⊤) (fun (x : D) => SquaredPartition.dyadicProfile (q x) • g x) Ω

theorem NavierStokes.FlatDyadicExtension.dyadic_product_face {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : Set D} (hΩ : IsOpen Ω) {q : D → ℝ} (hq : ContDiffOn ℝ (↑⊤) q Ω) {g : D → E} (hg : ContDiffOn ℝ (↑⊤) g (WaveEdgeExtension.windowDomain Ω q (1 / 2) 2)) (hB : LocalJetBounds Ω q g) {x : D} (hx : x ∈ Ω) (he : q x = 1 / 2 ∨ q x = 2) : ContDiffAt ℝ (↑⊤) (fun (y : D) => SquaredPartition.dyadicProfile (q y) • g y) x ∧ ∀ (n : ℕ), iteratedFDeriv ℝ n (fun (y : D) => SquaredPartition.dyadicProfile (q y) • g y) x = 0

@[reducible, inline]

abbrev NavierStokes.ActualSignedNativeRegularity.FullPoint : Type

Full point: an abbreviation for ActualWaveRegularityData.FullPoint.

Equations

• NavierStokes.ActualSignedNativeRegularity.FullPoint = NavierStokes.ActualWaveRegularityData.FullPoint

theorem NavierStokes.ActualSignedNativeRegularity.half_weight_bounded {cL cR L : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ t ∈ Set.Ioo 0 L, max 1 (WeightedRadialPrimitive.delta L t)⁻¹ ^ m * √(WeightedRadialPrimitive.zeta cL cR L t) ≤ C

theorem NavierStokes.ActualSignedNativeRegularity.radial_weight_bounded (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : FullPoint), ActualWaveRegularityData.radius x ∈ Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal) → WaveEdgeExtension.edgeGrowth ActualWaveRegularityData.radius (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal) x ^ m * √(ActualSignedStageControls.fullStrip.zeta x) ≤ C

theorem NavierStokes.ActualSignedNativeRegularity.radial_jets_zero_outside {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℕ → FullPoint → E} {α : ℝ} (hf : WeightedClasses.MemClass ActualSignedStageControls.fullStrip (fun (x : ℕ) (x_1 : ActualSignedStageControls.FullPoint) => √(ActualSignedStageControls.fullStrip.zeta x_1)) α f) (hz : ∀ (n : ℕ), ∀ x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion, ActualWaveRegularityData.radius x ∉ Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal) → f n x = 0) (n m : ℕ) {x : FullPoint} (hx : x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion) (ho : ActualWaveRegularityData.radius x ∉ Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)) : iteratedFDeriv ℝ m (f n) x = 0

theorem NavierStokes.ActualSignedNativeRegularity.radial_class_bounded_jets {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℕ → FullPoint → E} {α : ℝ} (hf : WeightedClasses.MemClass ActualSignedStageControls.fullStrip (fun (x : ℕ) (x_1 : ActualSignedStageControls.FullPoint) => √(ActualSignedStageControls.fullStrip.zeta x_1)) α f) (hz : ∀ (n : ℕ), ∀ x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion, ActualWaveRegularityData.radius x ∉ Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal) → f n x = 0) (n m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion, ∀ j ≤ m, ‖iteratedFDeriv ℝ j (f n) x‖ ≤ C

theorem NavierStokes.ActualSignedNativeRegularity.norm_iteratedFDeriv_linear_pull {D F V : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup V] [NormedSpace ℝ V] (e : D →L[ℝ] F) {Ω : Set F} (hΩ : IsOpen Ω) {g : F → V} (hg : ContDiffOn ℝ (↑⊤) g Ω) (m : ℕ) {x : D} (hx : e x ∈ Ω) : ‖iteratedFDeriv ℝ m (g ∘ ⇑e) x‖ ≤ ‖iteratedFDeriv ℝ m g (e x)‖ * ‖e‖ ^ m

theorem NavierStokes.ActualSignedNativeRegularity.radial_class_pull_local_bounds {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {f : ℕ → FullPoint → E} {α : ℝ} (hf : WeightedClasses.MemClass ActualSignedStageControls.fullStrip (fun (x : ℕ) (x_1 : ActualSignedStageControls.FullPoint) => √(ActualSignedStageControls.fullStrip.zeta x_1)) α f) (hz : ∀ (n : ℕ), ∀ x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion, ActualWaveRegularityData.radius x ∉ Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal) → f n x = 0) (e : D →L[ℝ] FullPoint) (Ω : Set D) (q : D → ℝ) (hmap : Set.MapsTo (⇑e) (WaveEdgeExtension.windowDomain Ω q (1 / 2) 2) (ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion)) (n : ℕ) : FlatDyadicExtension.LocalJetBounds Ω q (f n ∘ ⇑e)

theorem NavierStokes.ActualSignedNativeRegularity.radial_class_dyadic_pull_smooth {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {f : ℕ → FullPoint → E} {α : ℝ} (hf : WeightedClasses.MemClass ActualSignedStageControls.fullStrip (fun (x : ℕ) (x_1 : ActualSignedStageControls.FullPoint) => √(ActualSignedStageControls.fullStrip.zeta x_1)) α f) (hz : ∀ (n : ℕ), ∀ x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion, ActualWaveRegularityData.radius x ∉ Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal) → f n x = 0) (e : D →L[ℝ] FullPoint) {Ω : Set D} (hΩ : IsOpen Ω) {q : D → ℝ} (hq : ContDiffOn ℝ (↑⊤) q Ω) (hmap : Set.MapsTo (⇑e) (WaveEdgeExtension.windowDomain Ω q (1 / 2) 2) (ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion)) (n : ℕ) : ContDiffOn ℝ (↑⊤) (fun (y : D) => SquaredPartition.dyadicProfile (q y) • f n (e y)) Ω ∧ ∀ x ∈ Ω, q x = 1 / 2 ∨ q x = 2 → ∀ (m : ℕ), iteratedFDeriv ℝ m (fun (y : D) => SquaredPartition.dyadicProfile (q y) • f n (e y)) x = 0

@[reducible, inline]

abbrev NavierStokes.ActualSignedNativeRegularity.Native : Type

Native: an abbreviation for ActualSignedPhysicalData.Native.

Equations

• NavierStokes.ActualSignedNativeRegularity.Native = NavierStokes.ActualSignedPhysicalData.Native

@[reducible, inline]

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

Label: an abbreviation for ActualSignedPhysicalBinding.Label B N0.

Equations

• NavierStokes.ActualSignedNativeRegularity.Label B N0 = NavierStokes.ActualSignedPhysicalBinding.Label B N0

noncomputable def NavierStokes.ActualSignedNativeRegularity.nativeCylinderMap : Native →L[ℝ] PhysicalSignedWave.Cylinder

Native cylinder map as an element of Native →L[ℝ] PhysicalSignedWave.Cylinder.

Equations

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

theorem NavierStokes.ActualSignedNativeRegularity.nativeCylinderMap_apply (y : Native) : nativeCylinderMap y = ActualSignedPhysicalData.nativeCylinder y

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

Native to common, given by (ActualSignedPhysicalBinding.toCommonCylinder l).toContinuousLinearMap.comp nativeCylinderMap.

Equations

• NavierStokes.ActualSignedNativeRegularity.nativeToCommon l = ↑(NavierStokes.ActualSignedPhysicalBinding.toCommonCylinder l) ∘SL NavierStokes.ActualSignedNativeRegularity.nativeCylinderMap

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

noncomputable def NavierStokes.ActualSignedNativeRegularity.nativeQ (y : Native) : ℝ

Native Q, given by SimilarityCoordinates.coordinateQ (2 * ActualPrimary.h) y.2.1.

Equations

• NavierStokes.ActualSignedNativeRegularity.nativeQ y = NavierStokes.SimilarityCoordinates.coordinateQ (2 * NavierStokes.CorrectionInitialization.ActualPrimary.h) y.2.1

theorem NavierStokes.ActualSignedNativeRegularity.nativeQ_smooth : ContDiffOn ℝ (↑⊤) nativeQ ActualSignedPhysicalData.nativePast

theorem NavierStokes.ActualSignedNativeRegularity.nativeToCommon_maps {B N0 : ℕ} (l : Label B N0) : Set.MapsTo (⇑(nativeToCommon l)) (WaveEdgeExtension.windowDomain ActualSignedPhysicalData.nativePast nativeQ (1 / 2) 2) (ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion)

theorem NavierStokes.ActualSignedNativeRegularity.radial_class_native_smooth {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {B N0 : ℕ} (l : Label B N0) {f : ℕ → FullPoint → E} {α : ℝ} (hf : WeightedClasses.MemClass ActualSignedStageControls.fullStrip (fun (x : ℕ) (x_1 : ActualSignedStageControls.FullPoint) => √(ActualSignedStageControls.fullStrip.zeta x_1)) α f) (hz : ∀ (n : ℕ), ∀ x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion, ActualWaveRegularityData.radius x ∉ Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal) → f n x = 0) (n : ℕ) : ContDiffOn ℝ (↑⊤) (fun (y : Native) => SquaredPartition.dyadicProfile (nativeQ y) • f n ((nativeToCommon l) y)) ActualSignedPhysicalData.nativePast ∧ ∀ y ∈ ActualSignedPhysicalData.nativePast, nativeQ y = 1 / 2 ∨ nativeQ y = 2 → ∀ (m : ℕ), iteratedFDeriv ℝ m (fun (z : Native) => SquaredPartition.dyadicProfile (nativeQ z) • f n ((nativeToCommon l) z)) y = 0

theorem NavierStokes.ActualSignedNativeRegularity.primary_mask_zero_outside {B N0 : ℕ} (l : Label B N0) (n : ℕ) (x : PhysicalSignedWave.Cylinder) (ho : SimilarityCoordinates.coordinateQ (2 * CorrectionInitialization.ActualPrimary.h) (x.1.2.1.2, x.1.2.1.1) ∉ Set.Ioo (1 / 2) 2) : (ActualSignedPhysicalBinding.primary l).mask n x = 0

theorem NavierStokes.ActualSignedNativeRegularity.referenceScalar_zero_outside {B N0 : ℕ} (l : Label B N0) (request : ℕ → PhysicalSignedWave.Cylinder → SignedWaveUpdate.Vec2) (j : Fin 2) (n : ℕ) (x : PhysicalSignedWave.Cylinder) (ho : SimilarityCoordinates.coordinateQ (2 * CorrectionInitialization.ActualPrimary.h) (x.1.2.1.2, x.1.2.1.1) ∉ Set.Ioo (1 / 2) 2) : ActualPeriodizedSignedRealization.referenceScalar (ActualSignedPhysicalBinding.primary l) request j n x = 0

theorem NavierStokes.ActualSignedNativeRegularity.own_native_smooth {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {B N0 : ℕ} {f : Label B N0 → TorusInverse.Frequency → ℕ → FullPoint → E} {α : ℝ} (hf : LabelSumBounds.UniformClass ActualSignedStageControls.fullStrip (fun (i : Label B N0 × TorusInverse.Frequency) (n : ℕ) (x : ActualSignedStageControls.FullPoint) => √(ActualSignedStageControls.fullStrip.zeta x) * ActualSignedStageControls.envelope i.1 n x) α (ActualSignedUnmaskedBounds.ownField f)) (hz : ∀ (l : Label B N0) (k : TorusInverse.Frequency), ∀ x ∈ ActualWaveRegularity.fullDomain CorrectionInitialization.ActualPrimary.standardRegion, ActualWaveRegularityData.radius x ∉ Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal) → f l k (ActualSignedUnmaskedBounds.reference l) x = 0) (l : Label B N0) (k : TorusInverse.Frequency) : ContDiffOn ℝ (↑⊤) (fun (y : Native) => SquaredPartition.dyadicProfile (nativeQ y) • f l k (ActualSignedUnmaskedBounds.reference l) ((nativeToCommon l) y)) ActualSignedPhysicalData.nativePast ∧ ∀ y ∈ ActualSignedPhysicalData.nativePast, nativeQ y = 1 / 2 ∨ nativeQ y = 2 → ∀ (m : ℕ), iteratedFDeriv ℝ m (fun (z : Native) => SquaredPartition.dyadicProfile (nativeQ z) • f l k (ActualSignedUnmaskedBounds.reference l) ((nativeToCommon l) z)) y = 0

theorem NavierStokes.ActualSignedNativeRegularity.potential_smooth_and_flat {B N0 : ℕ} {request : ℕ → FullPoint → SignedWaveUpdate.Vec2} {β : ℝ} (hR : ∀ (q : Fin 2), PeriodizedWaveBounds.UniformLocalJets ActualSignedStageControls.fullStrip (fun (x : Label B N0) (x_1 : ℕ) (x_2 : ActualSignedStageControls.FullPoint) => ActualSignedStageControls.fullStrip.zeta x_2) β ActualSignedStageControls.phaseCell fun (x : Label B N0) (n : ℕ) (x_1 : ActualSignedStageControls.Frequency) (x_2 : ActualSignedStageControls.FullPoint) => request n x_2 q) (l : Label B N0) (k : TorusInverse.Frequency) : ContDiffOn ℝ (↑⊤) (fun (y : Native) => SquaredPartition.dyadicProfile (nativeQ y) • ActualSignedUnmaskedBounds.potential request l k (ActualSignedUnmaskedBounds.reference l) ((nativeToCommon l) y)) ActualSignedPhysicalData.nativePast ∧ ∀ y ∈ ActualSignedPhysicalData.nativePast, nativeQ y = 1 / 2 ∨ nativeQ y = 2 → ∀ (m : ℕ), iteratedFDeriv ℝ m (fun (z : Native) => SquaredPartition.dyadicProfile (nativeQ z) • ActualSignedUnmaskedBounds.potential request l k (ActualSignedUnmaskedBounds.reference l) ((nativeToCommon l) z)) y = 0

theorem NavierStokes.ActualSignedNativeRegularity.pressure_smooth_and_flat {B N0 : ℕ} {request : ℕ → FullPoint → SignedWaveUpdate.Vec2} {β : ℝ} (hR : ∀ (q : Fin 2), PeriodizedWaveBounds.UniformLocalJets ActualSignedStageControls.fullStrip (fun (x : Label B N0) (x_1 : ℕ) (x_2 : ActualSignedStageControls.FullPoint) => ActualSignedStageControls.fullStrip.zeta x_2) β ActualSignedStageControls.phaseCell fun (x : Label B N0) (n : ℕ) (x_1 : ActualSignedStageControls.Frequency) (x_2 : ActualSignedStageControls.FullPoint) => request n x_2 q) (l : Label B N0) (k : TorusInverse.Frequency) : ContDiffOn ℝ (↑⊤) (fun (y : Native) => SquaredPartition.dyadicProfile (nativeQ y) • ActualSignedUnmaskedBounds.pressure request l k (ActualSignedUnmaskedBounds.reference l) ((nativeToCommon l) y)) ActualSignedPhysicalData.nativePast ∧ ∀ y ∈ ActualSignedPhysicalData.nativePast, nativeQ y = 1 / 2 ∨ nativeQ y = 2 → ∀ (m : ℕ), iteratedFDeriv ℝ m (fun (z : Native) => SquaredPartition.dyadicProfile (nativeQ z) • ActualSignedUnmaskedBounds.pressure request l k (ActualSignedUnmaskedBounds.reference l) ((nativeToCommon l) z)) y = 0

theorem NavierStokes.ActualSignedNativeRegularity.native_potential_source_factor {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 : ActualSignedUnmaskedBinding.NativeLabel B N0) (I : ActualSignedPhysicalData.SourceIndex) (n : ℕ) : ActualSignedPhysicalData.nativePotentialSource CorrectionInitialization.ActualPrimary.slots ⋯ (ActualSignedUnmaskedBinding.branch P u H hp L) I n = if I.1.1 = ⟨L.val, ⋯⟩ ∧ ↑I.1.2 = 1 ∧ n = L.val.1 then fun (y : Native) => SquaredPartition.dyadicProfile (nativeQ y) • ActualSignedUnmaskedBounds.potential (ActualSignedUnmaskedBinding.request P u) (ActualSignedExterior.actualLabel L) I.2 (ActualSignedUnmaskedBounds.reference (ActualSignedExterior.actualLabel L)) ((nativeToCommon (ActualSignedExterior.actualLabel L)) y) else fun (x : Native) => 0

The only gates are the original discrete label, harmonic, and band gates.

theorem NavierStokes.ActualSignedNativeRegularity.native_pressure_source_factor {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 : ActualSignedUnmaskedBinding.NativeLabel B N0) (I : ActualSignedPhysicalData.SourceIndex) (n : ℕ) : ActualSignedPhysicalData.nativePressureSource CorrectionInitialization.ActualPrimary.slots ⋯ (ActualSignedUnmaskedBinding.branch P u H hp L) I n = if I.1.1 = ⟨L.val, ⋯⟩ ∧ ↑I.1.2 = 1 ∧ n = L.val.1 then fun (y : Native) => SquaredPartition.dyadicProfile (nativeQ y) • ActualSignedUnmaskedBounds.pressure (ActualSignedUnmaskedBinding.request P u) (ActualSignedExterior.actualLabel L) I.2 (ActualSignedUnmaskedBounds.reference (ActualSignedExterior.actualLabel L)) ((nativeToCommon (ActualSignedExterior.actualLabel L)) y) else fun (x : Native) => 0

theorem NavierStokes.ActualSignedNativeRegularity.zero_native_smooth_and_flat {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] : ContDiffOn ℝ (↑⊤) (fun (x : Native) => 0) ActualSignedPhysicalData.nativePast ∧ ∀ y ∈ ActualSignedPhysicalData.nativePast, nativeQ y = 1 / 2 ∨ nativeQ y = 2 → ∀ (m : ℕ), iteratedFDeriv ℝ m (fun (x : Native) => 0) y = 0

theorem NavierStokes.ActualSignedNativeRegularity.native_potential_smooth_and_flat {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 : Label B N0) (x_1 : ℕ) (x_2 : ActualSignedStageControls.FullPoint) => ActualSignedStageControls.fullStrip.zeta x_2) β ActualSignedStageControls.phaseCell fun (x : Label B N0) (n : ℕ) (x_1 : ActualSignedStageControls.Frequency) (x_2 : ActualSignedStageControls.FullPoint) => ActualSignedUnmaskedBinding.request P u n x_2 q) (L : ActualSignedUnmaskedBinding.NativeLabel B N0) (I : ActualSignedPhysicalData.SourceIndex) (n : ℕ) : ContDiffOn ℝ (↑⊤) (ActualSignedPhysicalData.nativePotentialSource CorrectionInitialization.ActualPrimary.slots ⋯ (ActualSignedUnmaskedBinding.branch P u H hp L) I n) ActualSignedPhysicalData.nativePast ∧ ∀ y ∈ ActualSignedPhysicalData.nativePast, nativeQ y = 1 / 2 ∨ nativeQ y = 2 → ∀ (m : ℕ), iteratedFDeriv ℝ m (ActualSignedPhysicalData.nativePotentialSource CorrectionInitialization.ActualPrimary.slots ⋯ (ActualSignedUnmaskedBinding.branch P u H hp L) I n) y = 0

theorem NavierStokes.ActualSignedNativeRegularity.native_pressure_smooth_and_flat {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 : Label B N0) (x_1 : ℕ) (x_2 : ActualSignedStageControls.FullPoint) => ActualSignedStageControls.fullStrip.zeta x_2) β ActualSignedStageControls.phaseCell fun (x : Label B N0) (n : ℕ) (x_1 : ActualSignedStageControls.Frequency) (x_2 : ActualSignedStageControls.FullPoint) => ActualSignedUnmaskedBinding.request P u n x_2 q) (L : ActualSignedUnmaskedBinding.NativeLabel B N0) (I : ActualSignedPhysicalData.SourceIndex) (n : ℕ) : ContDiffOn ℝ (↑⊤) (ActualSignedPhysicalData.nativePressureSource CorrectionInitialization.ActualPrimary.slots ⋯ (ActualSignedUnmaskedBinding.branch P u H hp L) I n) ActualSignedPhysicalData.nativePast ∧ ∀ y ∈ ActualSignedPhysicalData.nativePast, nativeQ y = 1 / 2 ∨ nativeQ y = 2 → ∀ (m : ℕ), iteratedFDeriv ℝ m (ActualSignedPhysicalData.nativePressureSource CorrectionInitialization.ActualPrimary.slots ⋯ (ActualSignedUnmaskedBinding.branch P u H hp L) I n) y = 0

theorem NavierStokes.ActualSignedNativeRegularity.nativeRegular {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 : Label B N0) (x_1 : ℕ) (x_2 : ActualSignedStageControls.FullPoint) => ActualSignedStageControls.fullStrip.zeta x_2) β ActualSignedStageControls.phaseCell fun (x : Label B N0) (n : ℕ) (x_1 : ActualSignedStageControls.Frequency) (x_2 : ActualSignedStageControls.FullPoint) => ActualSignedUnmaskedBinding.request P u n x_2 q) (L : ActualSignedUnmaskedBinding.NativeLabel B N0) : ActualSignedPhysicalData.NativeRegular CorrectionInitialization.ActualPrimary.slots ⋯ (ActualSignedUnmaskedBinding.branch P u H hp L)

Full positive-time native regularity of the same actual signed family. Only the actual request jets are used; no native output smoothness is assumed.

theorem NavierStokes.ActualSignedNativeRegularity.request_jets_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) (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))) (q : Fin 2) : PeriodizedWaveBounds.UniformLocalJets ActualSignedStageControls.fullStrip (fun (x : Label B N0) (x_1 : ℕ) (x_2 : ActualSignedStageControls.FullPoint) => ActualSignedStageControls.fullStrip.zeta x_2) (α - 1) ActualSignedStageControls.phaseCell fun (x : Label B N0) (n : ℕ) (x_1 : ActualSignedStageControls.Frequency) (x_2 : ActualSignedStageControls.FullPoint) => ActualSignedUnmaskedBinding.request ActualInitialization.patch u n x_2 q

The request estimate is derived from the two measured mean residuals of the same reconstructed state.

theorem NavierStokes.ActualSignedNativeRegularity.nativeRegular_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))) (L : ActualSignedUnmaskedBinding.NativeLabel B N0) : ActualSignedPhysicalData.NativeRegular CorrectionInitialization.ActualPrimary.slots ⋯ (ActualSignedUnmaskedBinding.branch ActualInitialization.patch u H hp L)

No regularity hypothesis on a native output or unmasked quotient is needed: the actual mean residual classes provide all required input jets.

theorem NavierStokes.ActualSignedNativeRegularity.cycleNativeRegular {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (H : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) ((ActualCycleParameters.fixedParameters B N0).afterParticular x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state)) (hp : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b ((ActualCycleParameters.fixedParameters B N0).afterParticular x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state).pressure) (α : ℝ) (hfixed : VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) ((ActualCycleParameters.fixedParameters B N0).afterParticular x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state) = (ActualCycleParameters.fixedParameters B N0).afterParticular x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state) (hθ : WeightedClasses.MeanClass ActualInitialization.geometry.strip α (((ActualCycleParameters.fixedParameters B N0).afterParticular x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state).thetaResidual (CorrectionInitialization.ActualPrimary.commonContext B))) (hz : WeightedClasses.MeanClass ActualInitialization.geometry.strip α (((ActualCycleParameters.fixedParameters B N0).afterParticular x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state).axialResidual (CorrectionInitialization.ActualPrimary.commonContext B))) (L : ActualSignedUnmaskedBinding.NativeLabel B N0) : ActualSignedPhysicalData.NativeRegular CorrectionInitialization.ActualPrimary.slots ⋯ ((ActualSignedExterior.cycleFamily x H hp).singleton L)

This is the literal post-particular state used to construct the canonical signed physical family, with its initialization and gauge intact.