Exact exterior support of the actual signed physical fields

The original spatial mask and leading target force every signed copy to vanish outside the fixed nominal active annulus. The argument retains the normalized radial coordinate exactly and is independent of the request.

Signed physical families with label-dependent phase domains

Each active primary label retains its own phase domain, primary data, views, and state. Homogeneous singleton views permit reuse of the existing per-label constructors. Physical copies are then assembled before the locally finite sum is estimated; no maximum over infinitely many per-label constants occurs.

@[reducible, inline]

abbrev NavierStokes.DependentSignedPhysicalFamily.NativeLabel (active : Set PhysicalWaveSum.BandLabel) : Type

Native label: an abbreviation for ActualSignedPhysicalData.NativeLabel.

Equations

• NavierStokes.DependentSignedPhysicalFamily.NativeLabel = NavierStokes.ActualSignedPhysicalData.NativeLabel

structure NavierStokes.DependentSignedPhysicalFamily.Family : Type

Only active labels carry primary data, and their phase domains may differ.

• active : Set PhysicalWaveSum.BandLabel

  Active of Family, of type Set BandLabel.

• domain : NativeLabel self.active → PhaseJetBounds.Domain ℕ PhaseCalculus.Slow

  Domain of Family, of type NativeLabel active → PhaseJetBounds.Domain ℕ PhaseCalculus.Slow.

• primary (L : NativeLabel self.active) : PhysicalSignedWave.PrimaryData (self.domain L)

  Primary of Family, of type (L : NativeLabel active) → PhysicalSignedWave.PrimaryData (domain L).

• view (L : NativeLabel self.active) : (self.primary L).Views L.val.1

  View of Family, of type (L : NativeLabel active) → (primary L).Views L.val.1.

• state (L : NativeLabel self.active) : (self.view L).StateData

  State of Family, of type (L : NativeLabel active) → (view L).StateData.

• column : NativeLabel self.active → Fin 2

  Column of Family, of type NativeLabel active → Fin 2.

noncomputable def NavierStokes.DependentSignedPhysicalFamily.Family.singletonLabel (f : Family) (L : NativeLabel f.active) : NativeLabel {⟨L.val, ⋯⟩}

Singleton label, given by ⟨L.val, L.property, Set.mem_singleton _⟩.

Equations

• f.singletonLabel L = { val := L.val, property := ⋯, mem := ⋯ }

theorem NavierStokes.DependentSignedPhysicalFamily.Family.singleton_label_val (f : Family) (L : NativeLabel f.active) (K : NativeLabel {⟨L.val, ⋯⟩}) : K.val = L.val

noncomputable def NavierStokes.DependentSignedPhysicalFamily.Family.singletonPayload (f : Family) (L : NativeLabel f.active) (K : NativeLabel {⟨L.val, ⋯⟩}) : (V : (f.primary L).Views K.val.1) × V.StateData

Singleton payload as an element of (f.primary L).Views K.val.1, V.StateData.

Equations

• f.singletonPayload L K = ⋯.mpr ⟨f.view L, f.state L⟩

noncomputable def NavierStokes.DependentSignedPhysicalFamily.Family.singleton (f : Family) (L : NativeLabel f.active) : ActualSignedPhysicalData.SignedFamily (f.domain L)

Reuse the old homogeneous interface for exactly one actual label. There is no choice of data for an omitted label.

Equations

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

@[simp]

theorem NavierStokes.DependentSignedPhysicalFamily.Family.singleton_active (f : Family) (L : NativeLabel f.active) : (f.singleton L).active = {⟨L.val, ⋯⟩}

@[simp]

theorem NavierStokes.DependentSignedPhysicalFamily.Family.singleton_primary (f : Family) (L : NativeLabel f.active) (K : NativeLabel (f.singleton L).active) : (f.singleton L).primary K = f.primary L

@[simp]

theorem NavierStokes.DependentSignedPhysicalFamily.Family.singleton_view (f : Family) (L : NativeLabel f.active) : (f.singleton L).view (f.singletonLabel L) = f.view L

@[simp]

theorem NavierStokes.DependentSignedPhysicalFamily.Family.singleton_state (f : Family) (L : NativeLabel f.active) : (f.singleton L).state (f.singletonLabel L) = f.state L

@[simp]

theorem NavierStokes.DependentSignedPhysicalFamily.Family.singleton_column (f : Family) (L : NativeLabel f.active) (K : NativeLabel (f.singleton L).active) : (f.singleton L).column K = f.column L

theorem NavierStokes.DependentSignedPhysicalFamily.Family.singleton_referenceRequest (f : Family) (L : NativeLabel f.active) : ((f.singleton L).state (f.singletonLabel L)).referenceRequest = (f.state L).referenceRequest

theorem NavierStokes.DependentSignedPhysicalFamily.Family.singleton_request (f : Family) (L : NativeLabel f.active) : ((f.singleton L).state (f.singletonLabel L)).request = (f.state L).request

noncomputable def NavierStokes.DependentSignedPhysicalFamily.Family.valueAt (f : Family) {V : Type u_1} [Zero V] (value : NativeLabel f.active → V) (L : PhysicalWaveSum.BandLabel) : V

Extend actual values by zero without extending their primary data.

Equations

• f.valueAt value L = if hL : L ∈ f.active then value { val := ↑L, property := ⋯, mem := hL } else 0

@[simp]

theorem NavierStokes.DependentSignedPhysicalFamily.Family.valueAt_active (f : Family) {V : Type u_1} [Zero V] (value : NativeLabel f.active → V) (L : NativeLabel f.active) : f.valueAt value ⟨L.val, ⋯⟩ = value L

theorem NavierStokes.DependentSignedPhysicalFamily.Family.valueAt_inactive (f : Family) {V : Type u_1} [Zero V] (value : NativeLabel f.active → V) {L : PhysicalWaveSum.BandLabel} (hL : L ∉ f.active) : f.valueAt value L = 0

One physical copy family, selected label by label

noncomputable def NavierStokes.DependentSignedPhysicalFamily.zeroCopies {H : ℕ} {K : Type u_1} : PhysicalCopyBounds.CopyFamily H K

Zero copies, bundling gap, carrier, amplitude.

Equations

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

@[simp]

theorem NavierStokes.DependentSignedPhysicalFamily.zeroCopies_term {H : ℕ} {K : Type u_1} (a h r0 : ℝ) (I : PhysicalWaveSum.WaveIndex H) (k : K) : zeroCopies.term a h r0 I k = 0

noncomputable def NavierStokes.DependentSignedPhysicalFamily.zeroCells {H : ℕ} {K : Type u_1} : PhysicalCopyBounds.SupportCells zeroCopies

Zero cells, bundling cells, carrier, closed, locallyFinite and the required compatibility proofs.

Equations

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

theorem NavierStokes.DependentSignedPhysicalFamily.zeroSupport {H : ℕ} {K : Type u_1} {a b h r0 Z : ℝ} {Δ : ℕ} : LocalPhysicalCopyBounds.SupportData zeroCopies a b h r0 Z Δ

theorem NavierStokes.DependentSignedPhysicalFamily.zeroSmooth {H : ℕ} {K : Type u_1} {a h r0 : ℝ} : LocalPhysicalCopyBounds.SmoothData zeroCopies a h r0

noncomputable def NavierStokes.DependentSignedPhysicalFamily.diagonal {H : ℕ} {K : Type u_1} (f : PhysicalWaveSum.BandLabel → PhysicalCopyBounds.CopyFamily H K) : PhysicalCopyBounds.CopyFamily H K

Diagonal, bundling gap, carrier, amplitude.

Equations

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

@[simp]

theorem NavierStokes.DependentSignedPhysicalFamily.diagonal_gap {H : ℕ} {K : Type u_1} (f : PhysicalWaveSum.BandLabel → PhysicalCopyBounds.CopyFamily H K) (L : PhysicalWaveSum.BandLabel) : (diagonal f).gap L = (f L).gap L

@[simp]

theorem NavierStokes.DependentSignedPhysicalFamily.diagonal_carrier {H : ℕ} {K : Type u_1} (f : PhysicalWaveSum.BandLabel → PhysicalCopyBounds.CopyFamily H K) (k : K) (L : PhysicalWaveSum.BandLabel) : (diagonal f).carrier k L = (f L).carrier k L

@[simp]

theorem NavierStokes.DependentSignedPhysicalFamily.diagonal_amplitude {H : ℕ} {K : Type u_1} (f : PhysicalWaveSum.BandLabel → PhysicalCopyBounds.CopyFamily H K) (k : K) (I : PhysicalWaveSum.WaveIndex H) : (diagonal f).amplitude k I = (f I.1).amplitude k I

@[simp]

theorem NavierStokes.DependentSignedPhysicalFamily.diagonal_term {H : ℕ} {K : Type u_1} (f : PhysicalWaveSum.BandLabel → PhysicalCopyBounds.CopyFamily H K) (a h r0 : ℝ) (I : PhysicalWaveSum.WaveIndex H) (k : K) : (diagonal f).term a h r0 I k = (f I.1).term a h r0 I k

@[simp]

theorem NavierStokes.DependentSignedPhysicalFamily.diagonal_periodized {H : ℕ} {K : Type u_1} (f : PhysicalWaveSum.BandLabel → PhysicalCopyBounds.CopyFamily H K) (a h r0 : ℝ) (I : PhysicalWaveSum.WaveIndex H) : (diagonal f).periodized a h r0 I = (f I.1).periodized a h r0 I

theorem NavierStokes.DependentSignedPhysicalFamily.diagonal_sum {H : ℕ} {K : Type u_1} (f : PhysicalWaveSum.BandLabel → PhysicalCopyBounds.CopyFamily H K) (a h r0 : ℝ) (w : ProblemStatement.SpaceTime) : (diagonal f).sum a h r0 w = ∑ᶠ (I : PhysicalWaveSum.WaveIndex H), (f I.1).periodized a h r0 I w

noncomputable def NavierStokes.DependentSignedPhysicalFamily.diagonalCells {H : ℕ} {K : Type u_1} (f : PhysicalWaveSum.BandLabel → PhysicalCopyBounds.CopyFamily H K) (c : (L : PhysicalWaveSum.BandLabel) → PhysicalCopyBounds.SupportCells (f L)) : PhysicalCopyBounds.SupportCells (diagonal f)

Diagonal cells, bundling cells, support.

Equations

• NavierStokes.DependentSignedPhysicalFamily.diagonalCells f c = { cells := fun (L : NavierStokes.PhysicalWaveSum.BandLabel) => (c L).cells L, support := ⋯ }

@[simp]

theorem NavierStokes.DependentSignedPhysicalFamily.diagonalCells_cells {H : ℕ} {K : Type u_1} (f : PhysicalWaveSum.BandLabel → PhysicalCopyBounds.CopyFamily H K) (c : (L : PhysicalWaveSum.BandLabel) → PhysicalCopyBounds.SupportCells (f L)) (L : PhysicalWaveSum.BandLabel) : (diagonalCells f c).cells L = (c L).cells L

theorem NavierStokes.DependentSignedPhysicalFamily.diagonalSupport {H : ℕ} {K : Type u_1} (f : PhysicalWaveSum.BandLabel → PhysicalCopyBounds.CopyFamily H K) {a b h r0 Z : ℝ} {Δ : ℕ} (s : ∀ (L : PhysicalWaveSum.BandLabel), LocalPhysicalCopyBounds.SupportData (f L) a b h r0 Z Δ) : LocalPhysicalCopyBounds.SupportData (diagonal f) a b h r0 Z Δ

theorem NavierStokes.DependentSignedPhysicalFamily.diagonalSmooth {H : ℕ} {K : Type u_1} (f : PhysicalWaveSum.BandLabel → PhysicalCopyBounds.CopyFamily H K) {a h r0 : ℝ} (s : ∀ (L : PhysicalWaveSum.BandLabel), LocalPhysicalCopyBounds.SmoothData (f L) a h r0) : LocalPhysicalCopyBounds.SmoothData (diagonal f) a h r0

theorem NavierStokes.DependentSignedPhysicalFamily.diagonal_sum_locally_finite {H : ℕ} {K : Type u_1} (f : PhysicalWaveSum.BandLabel → PhysicalCopyBounds.CopyFamily H K) {a b h r0 Z : ℝ} {Δ : ℕ} (s : ∀ (L : PhysicalWaveSum.BandLabel), LocalPhysicalCopyBounds.SupportData (f L) a b h r0 Z Δ) (hh : 0 < h) (hh1 : h < 1 / 2) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : ∃ (t : Finset (PhysicalWaveSum.WaveIndex H)), t.card ≤ 2250 * (2 * H + 1) ∧ (diagonal f).sum a h r0 =ᶠ[nhds w] fun (y : ProblemStatement.SpaceTime) => ∑ I ∈ t, (f I.1).periodized a h r0 I y

The assembled infinite family retains the original uniform overlap bound and has a genuine local finite-sum identity.

theorem NavierStokes.DependentSignedPhysicalFamily.diagonal_sum_smooth {H : ℕ} {K : Type u_1} (f : PhysicalWaveSum.BandLabel → PhysicalCopyBounds.CopyFamily H K) {a b h r0 Z : ℝ} {Δ : ℕ} (c : (L : PhysicalWaveSum.BandLabel) → PhysicalCopyBounds.SupportCells (f L)) (s : ∀ (L : PhysicalWaveSum.BandLabel), LocalPhysicalCopyBounds.SupportData (f L) a b h r0 Z Δ) (sm : ∀ (L : PhysicalWaveSum.BandLabel), LocalPhysicalCopyBounds.SmoothData (f L) a h r0) (ha : 0 < a) (hh : 0 < h) (hh1 : h < 1 / 2) : ContDiffOn ℝ (↑⊤) ((diagonal f).sum a h r0) PhysicalWaveSum.preterminal

noncomputable def NavierStokes.DependentSignedPhysicalFamily.Family.copyAt {H : ℕ} {K : Type u_1} (f : Family) (copies : NativeLabel f.active → PhysicalCopyBounds.CopyFamily H K) (L : PhysicalWaveSum.BandLabel) : PhysicalCopyBounds.CopyFamily H K

The missing labels receive zero copies, never invented primary data.

Equations

• f.copyAt copies L = if hL : L ∈ f.active then copies { val := ↑L, property := ⋯, mem := hL } else NavierStokes.DependentSignedPhysicalFamily.zeroCopies

@[simp]

theorem NavierStokes.DependentSignedPhysicalFamily.Family.copyAt_active {H : ℕ} {K : Type u_1} (f : Family) (copies : NativeLabel f.active → PhysicalCopyBounds.CopyFamily H K) (L : NativeLabel f.active) : f.copyAt copies ⟨L.val, ⋯⟩ = copies L

theorem NavierStokes.DependentSignedPhysicalFamily.Family.copyAt_inactive {H : ℕ} {K : Type u_1} (f : Family) (copies : NativeLabel f.active → PhysicalCopyBounds.CopyFamily H K) {L : PhysicalWaveSum.BandLabel} (hL : L ∉ f.active) : f.copyAt copies L = zeroCopies

noncomputable def NavierStokes.DependentSignedPhysicalFamily.Family.assembled {H : ℕ} {K : Type u_1} (f : Family) (copies : NativeLabel f.active → PhysicalCopyBounds.CopyFamily H K) : PhysicalCopyBounds.CopyFamily H K

Assembled, given by diagonal (f.copyAt copies).

Equations

• f.assembled copies = NavierStokes.DependentSignedPhysicalFamily.diagonal (f.copyAt copies)

theorem NavierStokes.DependentSignedPhysicalFamily.Family.assembled_term_active {H : ℕ} {K : Type u_1} (f : Family) (copies : NativeLabel f.active → PhysicalCopyBounds.CopyFamily H K) (L : NativeLabel f.active) (j : PhysicalWaveSum.Harmonic H) (a h r0 : ℝ) (k : K) : (f.assembled copies).term a h r0 (⟨L.val, ⋯⟩, j) k = (copies L).term a h r0 (⟨L.val, ⋯⟩, j) k

theorem NavierStokes.DependentSignedPhysicalFamily.Family.assembled_term_inactive {H : ℕ} {K : Type u_1} (f : Family) (copies : NativeLabel f.active → PhysicalCopyBounds.CopyFamily H K) (I : PhysicalWaveSum.WaveIndex H) (hI : I.1 ∉ f.active) (a h r0 : ℝ) (k : K) : (f.assembled copies).term a h r0 I k = 0

noncomputable def NavierStokes.DependentSignedPhysicalFamily.Family.branchCells {H : ℕ} {K : Type u_1} (f : Family) (copies : NativeLabel f.active → PhysicalCopyBounds.CopyFamily H K) (c : (L : NativeLabel f.active) → PhysicalCopyBounds.SupportCells (copies L)) (L : PhysicalWaveSum.BandLabel) : PhysicalCopyBounds.SupportCells (f.copyAt copies L)

Branch cells as an element of SupportCells (f.copyAt copies L).

Equations

• f.branchCells copies c L = if hL : L ∈ f.active then ⋯.mpr (c { val := ↑L, property := ⋯, mem := hL }) else ⋯.mpr NavierStokes.DependentSignedPhysicalFamily.zeroCells

theorem NavierStokes.DependentSignedPhysicalFamily.Family.branchSupport {H : ℕ} {K : Type u_1} (f : Family) (copies : NativeLabel f.active → PhysicalCopyBounds.CopyFamily H K) {a b h r0 Z : ℝ} {Δ : ℕ} (s : ∀ (L : NativeLabel f.active), LocalPhysicalCopyBounds.SupportData (copies L) a b h r0 Z Δ) (L : PhysicalWaveSum.BandLabel) : LocalPhysicalCopyBounds.SupportData (f.copyAt copies L) a b h r0 Z Δ

theorem NavierStokes.DependentSignedPhysicalFamily.Family.branchSmooth {H : ℕ} {K : Type u_1} (f : Family) (copies : NativeLabel f.active → PhysicalCopyBounds.CopyFamily H K) {a h r0 : ℝ} (s : ∀ (L : NativeLabel f.active), LocalPhysicalCopyBounds.SmoothData (copies L) a h r0) (L : PhysicalWaveSum.BandLabel) : LocalPhysicalCopyBounds.SmoothData (f.copyAt copies L) a h r0

noncomputable def NavierStokes.DependentSignedPhysicalFamily.Family.potentialSource (f : Family) {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) (L : PhysicalWaveSum.BandLabel) : ActualSignedPhysicalData.SourceIndex → ℕ → ActualSignedPhysicalData.Native → HarmonicCalculus.ComplexVector

The exact native source belonging to a primary label. Uniform bounds must hold jointly over this label and the native source index.

Equations

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

noncomputable def NavierStokes.DependentSignedPhysicalFamily.Family.pressureSource (f : Family) {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) (L : PhysicalWaveSum.BandLabel) : ActualSignedPhysicalData.SourceIndex → ℕ → ActualSignedPhysicalData.Native → ℂ

Pressure source, given by f.valueAt (fun L => ActualSignedPhysicalData.nativePressureSource sys hh (f.singleton L)) L.

Equations

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

@[simp]

theorem NavierStokes.DependentSignedPhysicalFamily.Family.potentialSource_active (f : Family) {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) (L : NativeLabel f.active) : f.potentialSource sys hh ⟨L.val, ⋯⟩ = ActualSignedPhysicalData.nativePotentialSource sys hh (f.singleton L)

@[simp]

theorem NavierStokes.DependentSignedPhysicalFamily.Family.pressureSource_active (f : Family) {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) (L : NativeLabel f.active) : f.pressureSource sys hh ⟨L.val, ⋯⟩ = ActualSignedPhysicalData.nativePressureSource sys hh (f.singleton L)

noncomputable def NavierStokes.DependentSignedPhysicalFamily.Family.potentialCopies (f : Family) {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) (i : Fin 3) : PhysicalCopyBounds.CopyFamily 1 TorusInverse.Frequency

Potential copies, given by f.assembled (fun L => ActualSignedPhysicalData.potentialFamily sys hh (f.singleton L) i).

Equations

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

noncomputable def NavierStokes.DependentSignedPhysicalFamily.Family.pressureCopies (f : Family) {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) : PhysicalCopyBounds.CopyFamily 1 TorusInverse.Frequency

Pressure copies, given by f.assembled (fun L => ActualSignedPhysicalData.pressureFamily sys hh (f.singleton L)).

Equations

• f.pressureCopies sys hh = f.assembled fun (L : NavierStokes.DependentSignedPhysicalFamily.NativeLabel f.active) => NavierStokes.ActualSignedPhysicalData.pressureFamily sys hh (f.singleton L)

theorem NavierStokes.DependentSignedPhysicalFamily.Family.potential_amplitude_eq_source (f : Family) {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) (i : Fin 3) (k : TorusInverse.Frequency) (I : PhysicalWaveSum.WaveIndex 1) (x : PhysicalGraphBounds.LiftPoint) : (f.potentialCopies sys hh i).amplitude k I x = ChartScales.Q (↑I.1).1 ^ (-h) • CartesianCopySource.rotatedSource (f.potentialSource sys hh I.1) (I, k) (↑I.1).1 x i

Native Cartesian rotation and the physical factor are retained exactly by the dependent assembly.

theorem NavierStokes.DependentSignedPhysicalFamily.Family.pressure_amplitude_eq_source (f : Family) {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) (k : TorusInverse.Frequency) (I : PhysicalWaveSum.WaveIndex 1) (x : PhysicalGraphBounds.LiftPoint) : (f.pressureCopies sys hh).amplitude k I x = ChartScales.Q (↑I.1).1 ^ (-(2 * CoordinateAlgebra.A h)) • f.pressureSource sys hh I.1 (I, k) (↑I.1).1 (PhysicalClassBounds.cylindricalMap x)

theorem NavierStokes.DependentSignedPhysicalFamily.Family.potential_periodized_active (f : Family) {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) (L : NativeLabel f.active) (i : Fin 3) (a r0 : ℝ) : (f.potentialCopies sys hh i).periodized a h r0 (ActualSignedPhysicalData.positiveIndex ⟨L.val, ⋯⟩) = (ActualSignedPhysicalData.potentialFamily sys hh (f.singleton L) i).periodized a h r0 (ActualSignedPhysicalData.positiveIndex ⟨L.val, ⋯⟩)

theorem NavierStokes.DependentSignedPhysicalFamily.Family.pressure_periodized_active (f : Family) {D h : ℝ} (sys : PartitionedCovariance.SlotSystem D h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) (L : NativeLabel f.active) (a r0 : ℝ) : (f.pressureCopies sys hh).periodized a h r0 (ActualSignedPhysicalData.positiveIndex ⟨L.val, ⋯⟩) = (ActualSignedPhysicalData.pressureFamily sys hh (f.singleton L)).periodized a h r0 (ActualSignedPhysicalData.positiveIndex ⟨L.val, ⋯⟩)

Sources retain their label in a dependent index

noncomputable def NavierStokes.DependentSignedPhysicalFamily.jointSource {E : Type} {ι : PhysicalWaveSum.BandLabel → Type u_2} {V : Type u_3} (source : (L : PhysicalWaveSum.BandLabel) → ι L → ℕ → E → V) : (L : PhysicalWaveSum.BandLabel) × ι L → ℕ → E → V

Joint source, defined pointwise by source I.1 I.2.

Equations

• NavierStokes.DependentSignedPhysicalFamily.jointSource source I = source I.fst I.snd

theorem NavierStokes.DependentSignedPhysicalFamily.localSourceBounds_slice {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : PhysicalWaveSum.BandLabel → Type u_2} {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {s : WeightedClasses.StripData E} {h α : ℝ} {w : (L : PhysicalWaveSum.BandLabel) → ι L → ℕ → E → ℝ} {source : (L : PhysicalWaveSum.BandLabel) → ι L → ℕ → E → V} (hs : LocalPhysicalCopyBounds.LocalSourceBounds s h α (jointSource w) (jointSource source)) (L : PhysicalWaveSum.BandLabel) : LocalPhysicalCopyBounds.LocalSourceBounds s h α (w L) (source L)

Native chart and carrier bounds are uniform before label selection

noncomputable def NavierStokes.DependentSignedPhysicalFamily.diagonalChart {H : ℕ} {K : Type u_1} {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : PhysicalWaveSum.BandLabel → Type u_2} (f : PhysicalWaveSum.BandLabel → PhysicalCopyBounds.CopyFamily H K) (c : (L : PhysicalWaveSum.BandLabel) → PhysicalCopyBounds.SupportCells (f L)) {a b h r0 σ : ℝ} (source : (L : PhysicalWaveSum.BandLabel) → ι L → ℕ → E → ℂ) (ch : (L : PhysicalWaveSum.BandLabel) → LocalPhysicalCopyBounds.CommonChart (f L) (c L) a b h r0 σ (source L)) (hj : ∀ (m : ℕ), ∃ (B : ℝ), 1 ≤ B ∧ ∃ (q : ℕ), ∀ (k : K) (I : PhysicalWaveSum.WaveIndex H), ∀ x ∈ (ch I.1).domain k I, ∀ (j : ℕ), 1 ≤ j → j ≤ m → ‖iteratedFDeriv ℝ j ((ch I.1).map k I) x‖ ≤ B * ChartScales.S (↑I.1).1 ^ q) : LocalPhysicalCopyBounds.CommonChart (diagonal f) (diagonalCells f c) a b h r0 σ (jointSource source)

Diagonal chart, bundling sourceIndex, map, domain, open_domain and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.DependentSignedPhysicalFamily.diagonalCarrier {H : ℕ} {K : Type u_1} (f : PhysicalWaveSum.BandLabel → PhysicalCopyBounds.CopyFamily H K) (c : (L : PhysicalWaveSum.BandLabel) → PhysicalCopyBounds.SupportCells (f L)) {a b h r0 : ℝ} (bc : (L : PhysicalWaveSum.BandLabel) → PhysicalCopyBounds.CarrierBounds (f L) (c L) a b h r0) (hj : PhaseJetBounds.PolynomialJets (PhysicalCopyBounds.copyBandDomain (fun (k : K) (L : PhysicalWaveSum.BandLabel) => (bc L).region k L) ⋯) fun (I : K × PhysicalWaveSum.BandLabel) (x : PhysicalGraphBounds.Slow) => (((f I.2).carrier I.1 I.2).F x, ((f I.2).carrier I.1 I.2).G x)) : PhysicalCopyBounds.CarrierBounds (diagonal f) (diagonalCells f c) a b h r0

Diagonal carrier, bundling region, open_region, jets, contains.

Equations

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

noncomputable def NavierStokes.DependentSignedPhysicalFamily.zeroCarrier {H : ℕ} {K : Type u_1} {a b h r0 : ℝ} : PhysicalCopyBounds.CarrierBounds zeroCopies zeroCells a b h r0

No native region is required for an omitted label whose amplitude vanishes identically.

Equations

• NavierStokes.DependentSignedPhysicalFamily.zeroCarrier = { region := fun (x : K) (x_1 : NavierStokes.PhysicalWaveSum.BandLabel) => ∅, open_region := ⋯, jets := ⋯, contains := ⋯ }

noncomputable def NavierStokes.DependentSignedPhysicalFamily.zeroChart {H : ℕ} {K : Type u_1} {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {ν : Type u_3} {a b h r0 σ : ℝ} (source : ν → ℕ → E → ℂ) (index : K → PhysicalWaveSum.WaveIndex H → ν) : LocalPhysicalCopyBounds.CommonChart zeroCopies zeroCells a b h r0 σ source

Zero chart, bundling sourceIndex, map, domain, open_domain and the required compatibility proofs.

Equations

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

theorem NavierStokes.DependentSignedPhysicalFamily.identity_chart_jets {H : ℕ} {K : Type u_1} {ι : PhysicalWaveSum.BandLabel → Type u_2} (f : PhysicalWaveSum.BandLabel → PhysicalCopyBounds.CopyFamily H K) (c : (L : PhysicalWaveSum.BandLabel) → PhysicalCopyBounds.SupportCells (f L)) {a b h r0 σ : ℝ} (source : (L : PhysicalWaveSum.BandLabel) → ι L → ℕ → PhysicalGraphBounds.LiftPoint → ℂ) (ch : (L : PhysicalWaveSum.BandLabel) → LocalPhysicalCopyBounds.CommonChart (f L) (c L) a b h r0 σ (source L)) (hid : ∀ (k : K) (I : PhysicalWaveSum.WaveIndex H), (ch I.1).map k I = fun (x : PhysicalWaveSum.LiftPoint) => x) (m : ℕ) : ∃ (B : ℝ), 1 ≤ B ∧ ∃ (q : ℕ), ∀ (k : K) (I : PhysicalWaveSum.WaveIndex H), ∀ x ∈ (ch I.1).domain k I, ∀ (j : ℕ), 1 ≤ j → j ≤ m → ‖iteratedFDeriv ℝ j ((ch I.1).map k I) x‖ ≤ B * ChartScales.S (↑I.1).1 ^ q

In the actual Cartesian source adapter every local map is the identity. Its common positive-jet bound is exactly one, with polynomial degree zero.

theorem NavierStokes.DependentSignedPhysicalFamily.identity_or_empty_chart_jets {H : ℕ} {K : Type u_1} {ι : PhysicalWaveSum.BandLabel → Type u_2} (f : PhysicalWaveSum.BandLabel → PhysicalCopyBounds.CopyFamily H K) (c : (L : PhysicalWaveSum.BandLabel) → PhysicalCopyBounds.SupportCells (f L)) {a b h r0 σ : ℝ} (source : (L : PhysicalWaveSum.BandLabel) → ι L → ℕ → PhysicalGraphBounds.LiftPoint → ℂ) (ch : (L : PhysicalWaveSum.BandLabel) → LocalPhysicalCopyBounds.CommonChart (f L) (c L) a b h r0 σ (source L)) (hid : ∀ (k : K) (I : PhysicalWaveSum.WaveIndex H), (ch I.1).domain k I = ∅ ∨ (ch I.1).map k I = fun (x : PhysicalWaveSum.LiftPoint) => x) (m : ℕ) : ∃ (B : ℝ), 1 ≤ B ∧ ∃ (q : ℕ), ∀ (k : K) (I : PhysicalWaveSum.WaveIndex H), ∀ x ∈ (ch I.1).domain k I, ∀ (j : ℕ), 1 ≤ j → j ≤ m → ‖iteratedFDeriv ℝ j ((ch I.1).map k I) x‖ ≤ B * ChartScales.S (↑I.1).1 ^ q

Empty inactive charts do not alter the common bound for identity charts of active labels.

One application of the physical-family estimate

noncomputable def NavierStokes.DependentSignedPhysicalFamily.waveData {H : ℕ} {K : Type u_1} {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : PhysicalWaveSum.BandLabel → Type u_2} {J : Type u_3} {a b h r0 Z P0 α σ : ℝ} {Δ : ℕ} (s : WeightedClasses.StripData E) (f : J → PhysicalWaveSum.BandLabel → PhysicalCopyBounds.CopyFamily H K) (c : (i : J) → (L : PhysicalWaveSum.BandLabel) → PhysicalCopyBounds.SupportCells (f i L)) (source : (L : PhysicalWaveSum.BandLabel) → ι L → ℕ → E → ℂ) (weight : (L : PhysicalWaveSum.BandLabel) → ι L → ℕ → E → ℝ) (hsource : LocalPhysicalCopyBounds.LocalSourceBounds s h α (jointSource weight) (jointSource source)) (ch : (i : J) → (L : PhysicalWaveSum.BandLabel) → LocalPhysicalCopyBounds.CommonChart (f i L) (c i L) a b h r0 σ (source L)) (hchart : ∀ (i : J) (m : ℕ), ∃ (B : ℝ), 1 ≤ B ∧ ∃ (q : ℕ), ∀ (k : K) (I : PhysicalWaveSum.WaveIndex H), ∀ x ∈ (ch i I.1).domain k I, ∀ (j : ℕ), 1 ≤ j → j ≤ m → ‖iteratedFDeriv ℝ j ((ch i I.1).map k I) x‖ ≤ B * ChartScales.S (↑I.1).1 ^ q) (hmap : ∀ (i : J) (k : K) (I : PhysicalWaveSum.WaveIndex H), Set.MapsTo ((ch i I.1).map k I) ((ch i I.1).domain k I) s.domain) (bc : (i : J) → (L : PhysicalWaveSum.BandLabel) → PhysicalCopyBounds.CarrierBounds (f i L) (c i L) a b h r0) (hphase : ∀ (i : J), PhaseJetBounds.PolynomialJets (PhysicalCopyBounds.copyBandDomain (fun (k : K) (L : PhysicalWaveSum.BandLabel) => (bc i L).region k L) ⋯) fun (I : K × PhysicalWaveSum.BandLabel) (x : PhysicalGraphBounds.Slow) => (((f i I.2).carrier I.1 I.2).F x, ((f i I.2).carrier I.1 I.2).G x)) (hsupport : ∀ (i : J) (L : PhysicalWaveSum.BandLabel), LocalPhysicalCopyBounds.SupportData (f i L) a b h r0 Z Δ) (hsmooth : ∀ (i : J) (L : PhysicalWaveSum.BandLabel), LocalPhysicalCopyBounds.SmoothData (f i L) a h r0) (ha : 0 < a) (hr0 : 0 ≤ r0) (hZ : 0 ≤ Z) (hP : 1 ≤ P0) (hfrequency : ∀ (i : J) (k : K) (L : PhysicalWaveSum.BandLabel), |((f i L).carrier k L).angular| ≤ P0 ∧ |((f i L).carrier k L).axial| ≤ P0 ∧ |((f i L).carrier k L).radial| ≤ P0) : PhysicalStageBounds.WaveData h E ((L : PhysicalWaveSum.BandLabel) × ι L) K J

The physical factory is applied once to all labels. Its source and phase bounds are jointly quantified; individual physical bounds are not inputs to this constructor.

Equations

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

theorem NavierStokes.DependentSignedPhysicalFamily.waveData_copies {H : ℕ} {K : Type u_1} {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : PhysicalWaveSum.BandLabel → Type u_2} {J : Type u_3} {a b h r0 Z P0 α σ : ℝ} {Δ : ℕ} (s : WeightedClasses.StripData E) (f : J → PhysicalWaveSum.BandLabel → PhysicalCopyBounds.CopyFamily H K) (c : (i : J) → (L : PhysicalWaveSum.BandLabel) → PhysicalCopyBounds.SupportCells (f i L)) (source : (L : PhysicalWaveSum.BandLabel) → ι L → ℕ → E → ℂ) (weight : (L : PhysicalWaveSum.BandLabel) → ι L → ℕ → E → ℝ) (hsource : LocalPhysicalCopyBounds.LocalSourceBounds s h α (jointSource weight) (jointSource source)) (ch : (i : J) → (L : PhysicalWaveSum.BandLabel) → LocalPhysicalCopyBounds.CommonChart (f i L) (c i L) a b h r0 σ (source L)) (hchart : ∀ (i : J) (m : ℕ), ∃ (B : ℝ), 1 ≤ B ∧ ∃ (q : ℕ), ∀ (k : K) (I : PhysicalWaveSum.WaveIndex H), ∀ x ∈ (ch i I.1).domain k I, ∀ (j : ℕ), 1 ≤ j → j ≤ m → ‖iteratedFDeriv ℝ j ((ch i I.1).map k I) x‖ ≤ B * ChartScales.S (↑I.1).1 ^ q) (hmap : ∀ (i : J) (k : K) (I : PhysicalWaveSum.WaveIndex H), Set.MapsTo ((ch i I.1).map k I) ((ch i I.1).domain k I) s.domain) (bc : (i : J) → (L : PhysicalWaveSum.BandLabel) → PhysicalCopyBounds.CarrierBounds (f i L) (c i L) a b h r0) (hphase : ∀ (i : J), PhaseJetBounds.PolynomialJets (PhysicalCopyBounds.copyBandDomain (fun (k : K) (L : PhysicalWaveSum.BandLabel) => (bc i L).region k L) ⋯) fun (I : K × PhysicalWaveSum.BandLabel) (x : PhysicalGraphBounds.Slow) => (((f i I.2).carrier I.1 I.2).F x, ((f i I.2).carrier I.1 I.2).G x)) (hsupport : ∀ (i : J) (L : PhysicalWaveSum.BandLabel), LocalPhysicalCopyBounds.SupportData (f i L) a b h r0 Z Δ) (hsmooth : ∀ (i : J) (L : PhysicalWaveSum.BandLabel), LocalPhysicalCopyBounds.SmoothData (f i L) a h r0) (ha : 0 < a) (hr0 : 0 ≤ r0) (hZ : 0 ≤ Z) (hP : 1 ≤ P0) (hfrequency : ∀ (i : J) (k : K) (L : PhysicalWaveSum.BandLabel), |((f i L).carrier k L).angular| ≤ P0 ∧ |((f i L).carrier k L).axial| ≤ P0 ∧ |((f i L).carrier k L).radial| ≤ P0) (i : J) : (waveData s f c source weight hsource ch hchart hmap bc hphase hsupport hsmooth ha hr0 hZ hP hfrequency).copies i = diagonal (f i)

theorem NavierStokes.DependentSignedPhysicalFamily.waveData_scalar {H : ℕ} {K : Type u_1} {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : PhysicalWaveSum.BandLabel → Type u_2} {J : Type u_3} {a b h r0 Z P0 α σ : ℝ} {Δ : ℕ} (s : WeightedClasses.StripData E) (f : J → PhysicalWaveSum.BandLabel → PhysicalCopyBounds.CopyFamily H K) (c : (i : J) → (L : PhysicalWaveSum.BandLabel) → PhysicalCopyBounds.SupportCells (f i L)) (source : (L : PhysicalWaveSum.BandLabel) → ι L → ℕ → E → ℂ) (weight : (L : PhysicalWaveSum.BandLabel) → ι L → ℕ → E → ℝ) (hsource : LocalPhysicalCopyBounds.LocalSourceBounds s h α (jointSource weight) (jointSource source)) (ch : (i : J) → (L : PhysicalWaveSum.BandLabel) → LocalPhysicalCopyBounds.CommonChart (f i L) (c i L) a b h r0 σ (source L)) (hchart : ∀ (i : J) (m : ℕ), ∃ (B : ℝ), 1 ≤ B ∧ ∃ (q : ℕ), ∀ (k : K) (I : PhysicalWaveSum.WaveIndex H), ∀ x ∈ (ch i I.1).domain k I, ∀ (j : ℕ), 1 ≤ j → j ≤ m → ‖iteratedFDeriv ℝ j ((ch i I.1).map k I) x‖ ≤ B * ChartScales.S (↑I.1).1 ^ q) (hmap : ∀ (i : J) (k : K) (I : PhysicalWaveSum.WaveIndex H), Set.MapsTo ((ch i I.1).map k I) ((ch i I.1).domain k I) s.domain) (bc : (i : J) → (L : PhysicalWaveSum.BandLabel) → PhysicalCopyBounds.CarrierBounds (f i L) (c i L) a b h r0) (hphase : ∀ (i : J), PhaseJetBounds.PolynomialJets (PhysicalCopyBounds.copyBandDomain (fun (k : K) (L : PhysicalWaveSum.BandLabel) => (bc i L).region k L) ⋯) fun (I : K × PhysicalWaveSum.BandLabel) (x : PhysicalGraphBounds.Slow) => (((f i I.2).carrier I.1 I.2).F x, ((f i I.2).carrier I.1 I.2).G x)) (hsupport : ∀ (i : J) (L : PhysicalWaveSum.BandLabel), LocalPhysicalCopyBounds.SupportData (f i L) a b h r0 Z Δ) (hsmooth : ∀ (i : J) (L : PhysicalWaveSum.BandLabel), LocalPhysicalCopyBounds.SmoothData (f i L) a h r0) (ha : 0 < a) (hr0 : 0 ≤ r0) (hZ : 0 ≤ Z) (hP : 1 ≤ P0) (hfrequency : ∀ (i : J) (k : K) (L : PhysicalWaveSum.BandLabel), |((f i L).carrier k L).angular| ≤ P0 ∧ |((f i L).carrier k L).axial| ≤ P0 ∧ |((f i L).carrier k L).radial| ≤ P0) (i : J) : (waveData s f c source weight hsource ch hchart hmap bc hphase hsupport hsmooth ha hr0 hZ hP hfrequency).scalar i = (diagonal (f i)).sum a h r0

theorem NavierStokes.DependentSignedPhysicalFamily.physical_scalar_bound {H : ℕ} {K : Type u_1} {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : PhysicalWaveSum.BandLabel → Type u_2} {J : Type u_3} {a b h r0 Z P0 α σ : ℝ} {Δ : ℕ} (s : WeightedClasses.StripData E) (f : J → PhysicalWaveSum.BandLabel → PhysicalCopyBounds.CopyFamily H K) (c : (i : J) → (L : PhysicalWaveSum.BandLabel) → PhysicalCopyBounds.SupportCells (f i L)) (source : (L : PhysicalWaveSum.BandLabel) → ι L → ℕ → E → ℂ) (weight : (L : PhysicalWaveSum.BandLabel) → ι L → ℕ → E → ℝ) (hsource : LocalPhysicalCopyBounds.LocalSourceBounds s h α (jointSource weight) (jointSource source)) (ch : (i : J) → (L : PhysicalWaveSum.BandLabel) → LocalPhysicalCopyBounds.CommonChart (f i L) (c i L) a b h r0 σ (source L)) (hchart : ∀ (i : J) (m : ℕ), ∃ (B : ℝ), 1 ≤ B ∧ ∃ (q : ℕ), ∀ (k : K) (I : PhysicalWaveSum.WaveIndex H), ∀ x ∈ (ch i I.1).domain k I, ∀ (j : ℕ), 1 ≤ j → j ≤ m → ‖iteratedFDeriv ℝ j ((ch i I.1).map k I) x‖ ≤ B * ChartScales.S (↑I.1).1 ^ q) (hmap : ∀ (i : J) (k : K) (I : PhysicalWaveSum.WaveIndex H), Set.MapsTo ((ch i I.1).map k I) ((ch i I.1).domain k I) s.domain) (bc : (i : J) → (L : PhysicalWaveSum.BandLabel) → PhysicalCopyBounds.CarrierBounds (f i L) (c i L) a b h r0) (hphase : ∀ (i : J), PhaseJetBounds.PolynomialJets (PhysicalCopyBounds.copyBandDomain (fun (k : K) (L : PhysicalWaveSum.BandLabel) => (bc i L).region k L) ⋯) fun (I : K × PhysicalWaveSum.BandLabel) (x : PhysicalGraphBounds.Slow) => (((f i I.2).carrier I.1 I.2).F x, ((f i I.2).carrier I.1 I.2).G x)) (hsupport : ∀ (i : J) (L : PhysicalWaveSum.BandLabel), LocalPhysicalCopyBounds.SupportData (f i L) a b h r0 Z Δ) (hsmooth : ∀ (i : J) (L : PhysicalWaveSum.BandLabel), LocalPhysicalCopyBounds.SmoothData (f i L) a h r0) (ha : 0 < a) (hr0 : 0 ≤ r0) (hZ : 0 ≤ Z) (hP : 1 ≤ P0) (hfrequency : ∀ (i : J) (k : K) (L : PhysicalWaveSum.BandLabel), |((f i L).carrier k L).angular| ≤ P0 ∧ |((f i L).carrier k L).axial| ≤ P0 ∧ |((f i L).carrier k L).radial| ≤ P0) (hh : 0 < h) (hh1 : h < 1 / 2) (i : J) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ PhysicalWaveSum.preterminal, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m ((diagonal (f i)).sum a h r0) w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (h * α - PhysicalClassBounds.physicalLoss h σ m)

@[reducible, inline]

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

Label: an abbreviation for ActualSignedPhysicalBinding.Label.

Equations

• NavierStokes.ActualSignedExterior.Label = NavierStokes.ActualSignedPhysicalBinding.Label

noncomputable def NavierStokes.ActualSignedExterior.active : Set ProblemStatement.SpaceTime

Active, given by ActualPolarCoverage.active /-! ## The normalized radial coordinate does not depend on the band -/.

Equations

• NavierStokes.ActualSignedExterior.active = NavierStokes.ActualPolarCoverage.active

The normalized radial coordinate does not depend on the band

theorem NavierStokes.ActualSignedExterior.normalizedX_graph (n d : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : (BaseChartJets.normalizedCoordinates CorrectionInitialization.ActualPrimary.h (ActualSignedPhysicalData.nativeSlow (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n d w))).2.1 = (SlowBorelBase.cartesianChart CorrectionInitialization.ActualPrimary.h w).2.1

theorem NavierStokes.ActualSignedExterior.physicalLift_slow (n : ℕ) (w : ProblemStatement.SpaceTime) : ((ActualSignedPhysicalData.cylinderZero (PhysicalGraphBounds.physicalLift CorrectionInitialization.ActualPrimary.h n w)).1.1, (ActualSignedPhysicalData.cylinderZero (PhysicalGraphBounds.physicalLift CorrectionInitialization.ActualPrimary.h n w)).1.2.1) = ActualSignedPhysicalData.nativeSlow (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n 0 w)

theorem NavierStokes.ActualSignedExterior.primary_mask_or_target_zero {B N0 : ℕ} (l : Label B N0) (n m : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hout : w ∉ active) : (ActualSignedPhysicalBinding.primary l).mask n (ActualSignedPhysicalData.cylinderZero (PhysicalGraphBounds.physicalLift CorrectionInitialization.ActualPrimary.h m w)) = 0 ∨ (ActualSignedPhysicalBinding.primary l).target n (ActualSignedPhysicalData.cylinderZero (PhysicalGraphBounds.physicalLift CorrectionInitialization.ActualPrimary.h m w)) = 0

This is a statement about the literal primary mask and target. No property of the signed output or of the current request is assumed.

All actual labels, with their original dependent data

noncomputable def NavierStokes.ActualSignedExterior.bandLabel {B N0 : ℕ} (l : Label B N0) : PhysicalWaveSum.BandLabel

Band label, given by ⟨ActualSignedPhysicalBinding.spatialLabel l, ActualPrimaryBounds.label_large (l.2, l.1)⟩.

Equations

• NavierStokes.ActualSignedExterior.bandLabel l = ⟨NavierStokes.ActualSignedPhysicalBinding.spatialLabel l, ⋯⟩

theorem NavierStokes.ActualSignedExterior.bandLabel_injective {B N0 : ℕ} : Function.Injective bandLabel

noncomputable def NavierStokes.ActualSignedExterior.labels (B N0 : ℕ) : Set PhysicalWaveSum.BandLabel

Labels, given by range (bandLabel (B := B) (N0 := N0)).

Equations

• NavierStokes.ActualSignedExterior.labels B N0 = Set.range NavierStokes.ActualSignedExterior.bandLabel

noncomputable def NavierStokes.ActualSignedExterior.nativeLabel {B N0 : ℕ} (l : Label B N0) : ActualSignedPhysicalData.NativeLabel (labels B N0)

Native label, given by ⟨ActualSignedPhysicalBinding.spatialLabel l, ActualPrimaryBounds.label_large (l.2, l.1), Set.mem_range_self l⟩.

Equations

• NavierStokes.ActualSignedExterior.nativeLabel l = { val := NavierStokes.ActualSignedPhysicalBinding.spatialLabel l, property := ⋯, mem := ⋯ }

noncomputable def NavierStokes.ActualSignedExterior.actualLabel {B N0 : ℕ} (L : ActualSignedPhysicalData.NativeLabel (labels B N0)) : Label B N0

Actual label, given by Classical.choose L.mem.

Equations

• NavierStokes.ActualSignedExterior.actualLabel L = Classical.choose ⋯

theorem NavierStokes.ActualSignedExterior.bandLabel_actualLabel {B N0 : ℕ} (L : ActualSignedPhysicalData.NativeLabel (labels B N0)) : bandLabel (actualLabel L) = ⟨L.val, ⋯⟩

@[simp]

theorem NavierStokes.ActualSignedExterior.actualLabel_nativeLabel {B N0 : ℕ} (l : Label B N0) : actualLabel (nativeLabel l) = l

theorem NavierStokes.ActualSignedExterior.nativeLabel_ext {S : Set PhysicalWaveSum.BandLabel} {L M : ActualSignedPhysicalData.NativeLabel S} (he : L.val = M.val) : L = M

@[simp]

theorem NavierStokes.ActualSignedExterior.nativeLabel_actualLabel {B N0 : ℕ} (L : ActualSignedPhysicalData.NativeLabel (labels B N0)) : nativeLabel (actualLabel L) = L

noncomputable def NavierStokes.ActualSignedExterior.labelEquiv {B N0 : ℕ} : Label B N0 ≃ ActualSignedPhysicalData.NativeLabel (labels B N0)

Label equiv, bundling toFun, invFun, left_inv, right_inv.

Equations

• NavierStokes.ActualSignedExterior.labelEquiv = { toFun := NavierStokes.ActualSignedExterior.nativeLabel, invFun := NavierStokes.ActualSignedExterior.actualLabel, left_inv := ⋯, right_inv := ⋯ }

theorem NavierStokes.ActualSignedExterior.actualLabel_reference {B N0 : ℕ} (L : ActualSignedPhysicalData.NativeLabel (labels B N0)) : ActualSignedPhysicalBinding.reference (actualLabel L) = L.val.1

noncomputable def NavierStokes.ActualSignedExterior.rebandPayload {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {P : PhysicalSignedWave.PrimaryData U} {n m : ℕ} (he : n = m) (V : P.Views n) (s : V.StateData) : (W : P.Views m) × W.StateData

Reband payload, given by he ▸ ⟨V, s⟩.

Equations

• NavierStokes.ActualSignedExterior.rebandPayload he V s = he ▸ ⟨V, s⟩

theorem NavierStokes.ActualSignedExterior.rebandPayload_referenceRequest {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {P : PhysicalSignedWave.PrimaryData U} {n m : ℕ} (he : n = m) (V : P.Views n) (s : V.StateData) : (rebandPayload he V s).snd.referenceRequest = s.referenceRequest

noncomputable def NavierStokes.ActualSignedExterior.payload {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (L : ActualSignedPhysicalData.NativeLabel (labels B N0)) : (V : (ActualSignedPhysicalBinding.primary (actualLabel L)).Views L.val.1) × V.StateData

Payload, given by rebandPayload (actualLabel_reference L) (ActualSignedPhysicalBinding.nativeViews (actualLabel L)) (s (actualLabel L)).

Equations

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

noncomputable def NavierStokes.ActualSignedExterior.family {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) : DependentSignedPhysicalFamily.Family

Both signs and every actual primary label are retained. Only proof transport of the reference index is used in the view/state fields.

Equations

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

@[simp]

theorem NavierStokes.ActualSignedExterior.family_referenceRequest {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (L : ActualSignedPhysicalData.NativeLabel (labels B N0)) : ((family s).state L).referenceRequest = (s (actualLabel L)).referenceRequest

theorem NavierStokes.ActualSignedExterior.family_referenceRequest_nativeLabel {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (l : Label B N0) : ((family s).state (nativeLabel l)).referenceRequest = (s l).referenceRequest

Every physical copy vanishes on the exact exterior

theorem NavierStokes.ActualSignedExterior.potential_gap {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (i : Fin 3) (L : PhysicalWaveSum.BandLabel) : ((family s).potentialCopies CorrectionInitialization.ActualPrimary.slots ⋯ i).gap L = 0

theorem NavierStokes.ActualSignedExterior.pressure_gap {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (L : PhysicalWaveSum.BandLabel) : ((family s).pressureCopies CorrectionInitialization.ActualPrimary.slots ⋯).gap L = 0

theorem NavierStokes.ActualSignedExterior.potential_amplitude_zero {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (i : Fin 3) (I : PhysicalWaveSum.WaveIndex 1) (k : TorusInverse.Frequency) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hout : w ∉ active) : ((family s).potentialCopies CorrectionInitialization.ActualPrimary.slots ⋯ i).amplitude k I (PhysicalGraphBounds.physicalLift CorrectionInitialization.ActualPrimary.h (↑I.1).1 w) = 0

theorem NavierStokes.ActualSignedExterior.pressure_amplitude_zero {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (I : PhysicalWaveSum.WaveIndex 1) (k : TorusInverse.Frequency) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hout : w ∉ active) : ((family s).pressureCopies CorrectionInitialization.ActualPrimary.slots ⋯).amplitude k I (PhysicalGraphBounds.physicalLift CorrectionInitialization.ActualPrimary.h (↑I.1).1 w) = 0

theorem NavierStokes.ActualSignedExterior.potential_term_zero {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (i : Fin 3) (I : PhysicalWaveSum.WaveIndex 1) (k : TorusInverse.Frequency) (a r0 : ℝ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hout : w ∉ active) : ((family s).potentialCopies CorrectionInitialization.ActualPrimary.slots ⋯ i).term a CorrectionInitialization.ActualPrimary.h r0 I k w = 0

theorem NavierStokes.ActualSignedExterior.pressure_term_zero {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (I : PhysicalWaveSum.WaveIndex 1) (k : TorusInverse.Frequency) (a r0 : ℝ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hout : w ∉ active) : ((family s).pressureCopies CorrectionInitialization.ActualPrimary.slots ⋯).term a CorrectionInitialization.ActualPrimary.h r0 I k w = 0

theorem NavierStokes.ActualSignedExterior.potential_sum_zero {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (i : Fin 3) (a r0 : ℝ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hout : w ∉ active) : ((family s).potentialCopies CorrectionInitialization.ActualPrimary.slots ⋯ i).sum a CorrectionInitialization.ActualPrimary.h r0 w = 0

theorem NavierStokes.ActualSignedExterior.pressure_sum_zero {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (a r0 : ℝ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hout : w ∉ active) : ((family s).pressureCopies CorrectionInitialization.ActualPrimary.slots ⋯).sum a CorrectionInitialization.ActualPrimary.h r0 w = 0

noncomputable def NavierStokes.ActualSignedExterior.potential {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) : ProblemStatement.VelocityField

The literal dependent-family potential, at the fixed physical chart radius.

Equations

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

noncomputable def NavierStokes.ActualSignedExterior.pressure {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) : ProblemStatement.PressureField

Pressure, defined pointwise by (((family s).pressureCopies slots outgoing.data.h_pos.le).sum ActualPolarCoverage.inner h slots.radius w).re.

Equations

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

theorem NavierStokes.ActualSignedExterior.potential_zero {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hout : w ∉ active) : potential s w = 0

theorem NavierStokes.ActualSignedExterior.pressure_zero {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hout : w ∉ active) : pressure s w = 0

theorem NavierStokes.ActualSignedExterior.exterior_open : IsOpen {w : ProblemStatement.SpaceTime | w ∈ PhysicalWaveSum.preterminal ∧ w ∉ active}

theorem NavierStokes.ActualSignedExterior.potential_zero_germ {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hout : w ∉ active) : potential s =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.ActualSignedExterior.pressure_zero_germ {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hout : w ∉ active) : pressure s =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.ActualSignedExterior.velocity_zero {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hout : w ∉ active) : SpatialCurl.spatialCurl (potential s) w = 0

theorem NavierStokes.ActualSignedExterior.exterior_below {B N0 : ℕ} (s : (l : Label B N0) → (ActualSignedPhysicalBinding.nativeViews l).StateData) (Nres : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (_hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w < ChartScales.Q Nres) (hout : w ∉ active) : potential s w = 0 ∧ pressure s w = 0

Any fixed residual floor is allowed, since the stronger exterior identity above holds on the whole preterminal set.

The same state and request as the actual correction cycle

noncomputable def NavierStokes.ActualSignedExterior.cycleNativeStates {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) : (ActualSignedPhysicalBinding.nativeViews l).StateData

Cycle native states, constructed using ActualSignedPhysicalBinding.nativeStateData.

Equations

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

noncomputable def NavierStokes.ActualSignedExterior.cycleFamily {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) : DependentSignedPhysicalFamily.Family

Cycle family, given by family (cycleNativeStates x H hp).

Equations

• NavierStokes.ActualSignedExterior.cycleFamily x H hp = NavierStokes.ActualSignedExterior.family (NavierStokes.ActualSignedExterior.cycleNativeStates x H hp)

noncomputable def NavierStokes.ActualSignedExterior.cyclePotential {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) : ProblemStatement.VelocityField

Cycle potential, given by potential (cycleNativeStates x H hp).

Equations

• NavierStokes.ActualSignedExterior.cyclePotential x H hp = NavierStokes.ActualSignedExterior.potential (NavierStokes.ActualSignedExterior.cycleNativeStates x H hp)

noncomputable def NavierStokes.ActualSignedExterior.cyclePressure {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) : ProblemStatement.PressureField

Cycle pressure, given by pressure (cycleNativeStates x H hp).

Equations

• NavierStokes.ActualSignedExterior.cyclePressure x H hp = NavierStokes.ActualSignedExterior.pressure (NavierStokes.ActualSignedExterior.cycleNativeStates x H hp)

theorem NavierStokes.ActualSignedExterior.cycle_referenceRequest {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) (z : ActualSignedPhysicalBinding.Cylinder) : ((cycleFamily x H hp).state (nativeLabel l)).referenceRequest (ActualSignedPhysicalBinding.reference l) z = (ActualCycleParameters.fixedParameters B N0).signedRequest x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state (ActualSignedPhysicalBinding.reference l) ((ActualSignedPhysicalBinding.toCommonCylinder l) z)

The exterior statement concerns the signed request of the literal cycle after its particular update, without replacing the incoming state.

theorem NavierStokes.ActualSignedExterior.cycle_potential_zero {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) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hout : w ∉ active) : cyclePotential x H hp w = 0

theorem NavierStokes.ActualSignedExterior.cycle_pressure_zero {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) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hout : w ∉ active) : cyclePressure x H hp w = 0

theorem NavierStokes.ActualSignedExterior.cycle_zero_germs {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) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hout : w ∉ active) : (cyclePotential x H hp =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0) ∧ cyclePressure x H hp =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.ActualSignedExterior.cycle_velocity_zero {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) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hout : w ∉ active) : SpatialCurl.spatialCurl (cyclePotential x H hp) w = 0

theorem NavierStokes.ActualSignedExterior.cycle_exterior {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) (Nres : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w < ChartScales.Q Nres) (hout : w ∉ active) : cyclePotential x H hp w = 0 ∧ cyclePressure x H hp w = 0