Actual signed outputs from native support estimates

The background is the same chosen primary background. Its local controls are restricted to the signed phase cells before applying the native-copy localization and periodization estimates.

noncomputable def NavierStokes.ActualSignedOutputBounds.copies {B N0 : ℕ} (request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2) (l : ActualSignedStageControls.SignedLabel B N0) : PeriodizedWaveBounds.CopyData ActualSignedStageControls.FullPoint ActualSignedStageControls.Frequency

Copies, given by (parameters l).copyData ActualPrimaryBounds.strip request.

Equations

• NavierStokes.ActualSignedOutputBounds.copies request l = (NavierStokes.ActualSignedStageControls.parameters l).copyData NavierStokes.ActualPrimaryBounds.strip request

noncomputable def NavierStokes.ActualSignedOutputBounds.jointCell {B N0 : ℕ} (n : ℕ) (i : ActualSignedStageControls.SignedLabel B N0 × ActualSignedStageControls.Frequency) : Set ActualSignedStageControls.FullPoint

Joint cell, given by phaseCell i.1 n i.2.

Equations

• NavierStokes.ActualSignedOutputBounds.jointCell n i = NavierStokes.ActualSignedStageControls.phaseCell i.1 n i.2

noncomputable def NavierStokes.ActualSignedOutputBounds.primaryIndex {B N0 : ℕ} (i : ActualSignedStageControls.SignedLabel B N0 × ActualSignedStageControls.Frequency) : ActualPrimaryBounds.CopyIndex B N0

Primary index, given by ((i.1.2, i.1.1), i.2).

Equations

• NavierStokes.ActualSignedOutputBounds.primaryIndex i = ((i.1.2, i.1.1), i.2)

theorem NavierStokes.ActualSignedOutputBounds.primary_local {B N0 : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {w : ℕ → ActualPrimaryBounds.CopyIndex B N0 → ActualSignedStageControls.FullPoint → ℝ} {α : ℝ} {f : ℕ → ActualPrimaryBounds.CopyIndex B N0 → ActualSignedStageControls.FullPoint → E} (hf : LocalizedWaveBounds.LocalClass ActualSignedStageControls.fullStrip ActualPrimaryBounds.controlCell w α f) : LocalizedWaveBounds.LocalClass ActualSignedStageControls.fullStrip jointCell (fun (n : ℕ) (i : ActualSignedStageControls.SignedLabel B N0 × ActualSignedStageControls.Frequency) => w n (primaryIndex i)) α fun (n : ℕ) (i : ActualSignedStageControls.SignedLabel B N0 × ActualSignedStageControls.Frequency) => f n (primaryIndex i)

Uniform primary estimates restrict to the actual signed phase cells. The constants are chosen before both the label and the lattice copy.

theorem NavierStokes.ActualSignedOutputBounds.envelope_nonneg {B N0 : ℕ} (l : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (x : ActualSignedStageControls.FullPoint) : 0 ≤ ActualSignedStageControls.envelope l n x

theorem NavierStokes.ActualSignedOutputBounds.background_normal_eq {B N0 : ℕ} (request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2) : (CorrectionStep.jointRawBackground (copies request)).normal ActualSignedStageControls.fullStrip (ActualSignedStageControls.directions B) = fun (n : ℕ) (i : ActualSignedStageControls.SignedLabel B N0 × ActualSignedStageControls.Frequency) => ActualPrimaryBounds.actualFamily.normal ActualSignedStageControls.fullStrip (ActualSignedStageControls.directions B) n (primaryIndex i)

theorem NavierStokes.ActualSignedOutputBounds.background_defect_eq {B N0 : ℕ} (request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2) : (CorrectionStep.jointRawBackground (copies request)).defect ActualSignedStageControls.fullStrip (ActualSignedStageControls.directions B) = fun (n : ℕ) (i : ActualSignedStageControls.SignedLabel B N0 × ActualSignedStageControls.Frequency) => ActualPrimaryBounds.actualFamily.defect ActualSignedStageControls.fullStrip (ActualSignedStageControls.directions B) n (primaryIndex i)

theorem NavierStokes.ActualSignedOutputBounds.background_inputs {B N0 : ℕ} (request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2) : LocalizedWaveBounds.InputBounds ActualSignedStageControls.fullStrip jointCell (fun (n : ℕ) (i : ActualSignedStageControls.SignedLabel B N0 × ActualSignedStageControls.Frequency) (x : ActualSignedStageControls.FullPoint) => ActualSignedStageControls.envelope i.1 n x) 0 ChartScales.kappa (ActualSignedStageControls.directions B) (CorrectionStep.jointRawBackground (copies request))

This background certificate has zero amplitude and pressure. Every nonzero field in it is an actual primary background or phase expression.

theorem NavierStokes.ActualSignedOutputBounds.normal_range {B N0 : ℕ} (request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2) (l : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (k : ActualSignedStageControls.Frequency) {x : ActualSignedStageControls.FullPoint} (hx : x ∈ ActualSignedStageControls.fullStrip.domain) (hc : x ∈ ActualSignedStageControls.phaseCell l n k) : ActualPrimaryBounds.normalFloor B N0 ≤ ‖(copies request l).background.normal ActualSignedStageControls.fullStrip (ActualSignedStageControls.directions B) n x‖ ∧ ‖(copies request l).background.normal ActualSignedStageControls.fullStrip (ActualSignedStageControls.directions B) n x‖ ≤ ActualPrimaryBounds.normalCeiling B N0

theorem NavierStokes.ActualSignedOutputBounds.inverse_frequency {B N0 : ℕ} (request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2) : LocalizedWaveBounds.LocalUnweighted ActualSignedStageControls.fullStrip jointCell (1 / 2) fun (n : ℕ) (i : ActualSignedStageControls.SignedLabel B N0 × ActualSignedStageControls.Frequency) (x : ActualSignedStageControls.FullPoint) => 1 / (copies request i.1).background.frequency n

theorem NavierStokes.ActualSignedOutputBounds.localized_zero_of_cutoff {B N0 : ℕ} (request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2) (l : ActualSignedStageControls.SignedLabel B N0) {n : ℕ} {k : ActualSignedStageControls.Frequency} {x : ActualSignedStageControls.FullPoint} (hzero : ActualSignedStageControls.cutoff l k n =ᶠ[nhds x] fun (x : ActualSignedStageControls.FullPoint) => 0) : (((copies request l).localized k).amplitude n =ᶠ[nhds x] fun (x : ActualSignedStageControls.FullPoint) => 0) ∧ ((copies request l).localized k).pressure n =ᶠ[nhds x] fun (x : ActualSignedStageControls.FullPoint) => 0

A genuine cutoff zero germ kills both localized input fields.

theorem NavierStokes.ActualSignedOutputBounds.localized_zero_of_mask {B N0 : ℕ} (request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2) (l : ActualSignedStageControls.SignedLabel B N0) {n : ℕ} {k : ActualSignedStageControls.Frequency} {x : ActualSignedStageControls.FullPoint} (hzero : ActualSignedStageControls.mask l k n =ᶠ[nhds x] fun (x : ActualSignedStageControls.FullPoint) => 0) : (((copies request l).localized k).amplitude n =ᶠ[nhds x] fun (x : ActualSignedStageControls.FullPoint) => 0) ∧ ((copies request l).localized k).pressure n =ᶠ[nhds x] fun (x : ActualSignedStageControls.FullPoint) => 0

theorem NavierStokes.ActualSignedOutputBounds.phaseCell_or_localized_zero {B N0 : ℕ} (request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2) (l : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (k : ActualSignedStageControls.Frequency) {x : ActualSignedStageControls.FullPoint} (hx : x ∈ ActualSignedStageControls.fullStrip.domain) : x ∈ ActualSignedStageControls.phaseCell l n k ∨ (((copies request l).localized k).amplitude n =ᶠ[nhds x] fun (x : ActualSignedStageControls.FullPoint) => 0) ∧ ((copies request l).localized k).pressure n =ᶠ[nhds x] fun (x : ActualSignedStageControls.FullPoint) => 0

Every point in a copy cell either has the actual phase estimates or has a neighborhood on which both localized input fields vanish.

structure NavierStokes.ActualSignedOutputBounds.OutputBounds {B N0 : ℕ} (request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2) (α : ℝ) : Prop

These are the literal five outputs of one actual signed copy family.

• amplitude : LabelSumBounds.UniformWaveClass ActualSignedStageControls.fullStrip ActualSignedStageControls.envelope α fun (l : ActualSignedStageControls.SignedLabel B N0) => (copies request l).common.amplitude
• corrected : LabelSumBounds.UniformWaveClass ActualSignedStageControls.fullStrip ActualSignedStageControls.envelope α fun (l : ActualSignedStageControls.SignedLabel B N0) => ((copies request l).commonCorrected ActualSignedStageControls.fullStrip (ActualSignedStageControls.directions B)).amplitude
• pressure : LabelSumBounds.UniformWaveClass ActualSignedStageControls.fullStrip ActualSignedStageControls.envelope (α + 1 / 2) fun (l : ActualSignedStageControls.SignedLabel B N0) => (copies request l).common.pressure
• curl : LabelSumBounds.UniformWaveClass ActualSignedStageControls.fullStrip ActualSignedStageControls.envelope (α + 1 / 2 - ChartScales.kappa) fun (l : ActualSignedStageControls.SignedLabel B N0) => (copies request l).common.curlCorrection ActualSignedStageControls.fullStrip (ActualSignedStageControls.directions B)
• good : LabelSumBounds.UniformWaveClass ActualSignedStageControls.fullStrip ActualSignedStageControls.envelope (α + 1 / 2 - 3 * ChartScales.kappa) fun (l : ActualSignedStageControls.SignedLabel B N0) => (copies request l).globalGood ActualSignedStageControls.fullStrip (ActualSignedStageControls.directions B)

theorem NavierStokes.ActualSignedOutputBounds.native_inputs {B N0 : ℕ} {β : ℝ} {request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2} (hR : ∀ (q : Fin 2), PeriodizedWaveBounds.UniformLocalJets ActualSignedStageControls.fullStrip (fun (x : ActualSignedStageControls.SignedLabel B N0) (x_1 : ℕ) (x_2 : ActualSignedStageControls.FullPoint) => ActualSignedStageControls.fullStrip.zeta x_2) β ActualSignedStageControls.phaseCell fun (x : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (x_1 : ActualSignedStageControls.Frequency) (x_2 : ActualSignedStageControls.FullPoint) => request n x_2 q) : LocalizedWaveBounds.InputBounds ActualSignedStageControls.fullStrip jointCell (fun (n : ℕ) (i : ActualSignedStageControls.SignedLabel B N0 × ActualSignedStageControls.Frequency) (x : ActualSignedStageControls.FullPoint) => ActualSignedStageControls.envelope i.1 n x) (β + 1 / 2) ChartScales.kappa (ActualSignedStageControls.directions B) (LocalizedWaveBounds.jointNativeFamily (copies request))

Native input bounds are proved from the actual signed quotient and projected pressure, followed by the actual single cutoff.

theorem NavierStokes.ActualSignedOutputBounds.common_bounds {B N0 : ℕ} {β : ℝ} {request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2} (hR : ∀ (q : Fin 2), PeriodizedWaveBounds.UniformLocalJets ActualSignedStageControls.fullStrip (fun (x : ActualSignedStageControls.SignedLabel B N0) (x_1 : ℕ) (x_2 : ActualSignedStageControls.FullPoint) => ActualSignedStageControls.fullStrip.zeta x_2) β ActualSignedStageControls.phaseCell fun (x : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (x_1 : ActualSignedStageControls.Frequency) (x_2 : ActualSignedStageControls.FullPoint) => request n x_2 q) : OutputBounds request (β + 1 / 2)

All common outputs follow from native input estimates and actual support. No common, corrected, or good output bound is a premise.

theorem NavierStokes.ActualSignedOutputBounds.actual_common_bounds {B N0 : ℕ} (G : SignedMeanGain.Geometry) (hs : G.strip = ActualPrimaryBounds.strip) (c : CorrectionState.Context ActualSignedStageControls.Point) (u : CorrectionState.State ActualSignedStageControls.Point) (α : ℝ) (H : MeanStateRegularity.PrimitiveData G.region G.patch.a G.patch.b c u) (hfixed : VariableGaugeMean.reconstructState G.gauge c u = u) (hθ : WeightedClasses.MeanClass G.strip α (u.thetaResidual c)) (hz : WeightedClasses.MeanClass G.strip α (u.axialResidual c)) : OutputBounds (LocalSignedRequest.fullRequest G.strip G.patch G.coord c u) (α - 1 / 2)

The actual request is estimated from the current measured residuals. Only primitive incoming state data and its ordinary mean classes are used.

noncomputable def NavierStokes.ActualSignedOutputBounds.meanEnvelope {B N0 : ℕ} (l : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (x : ActualSignedStageControls.Point) : ℝ

Mean envelope, given by envelope l n (x, 0).

Equations

• NavierStokes.ActualSignedOutputBounds.meanEnvelope l n x = NavierStokes.ActualSignedStageControls.envelope l n (x, 0)

theorem NavierStokes.ActualSignedOutputBounds.block_bounds {B N0 : ℕ} {β : ℝ} {request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2} (hR : ∀ (q : Fin 2), PeriodizedWaveBounds.UniformLocalJets ActualSignedStageControls.fullStrip (fun (x : ActualSignedStageControls.SignedLabel B N0) (x_1 : ℕ) (x_2 : ActualSignedStageControls.FullPoint) => ActualSignedStageControls.fullStrip.zeta x_2) β ActualSignedStageControls.phaseCell fun (x : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (x_1 : ActualSignedStageControls.Frequency) (x_2 : ActualSignedStageControls.FullPoint) => request n x_2 q) : (∀ (i : Fin 3) (j : ℤ), LabelSumBounds.UniformWaveClass ActualPrimaryBounds.strip meanEnvelope (β + 1 / 2) fun (l : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (x : ActualPrimaryBounds.Point) => (((ActualSignedStageControls.parameters l).tangentBlock ActualPrimaryBounds.strip request).velocity n i).coeff j x) ∧ (∀ (i : Fin 3) (j : ℤ), LabelSumBounds.UniformWaveClass ActualPrimaryBounds.strip meanEnvelope (β + 1 / 2) fun (l : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (x : ActualPrimaryBounds.Point) => (((ActualSignedStageControls.parameters l).exactBlock ActualPrimaryBounds.strip request).velocity n i).coeff j x) ∧ (∀ (j : ℤ), LabelSumBounds.UniformWaveClass ActualPrimaryBounds.strip meanEnvelope (β + 1) fun (l : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (x : ActualPrimaryBounds.Point) => (((ActualSignedStageControls.parameters l).exactBlock ActualPrimaryBounds.strip request).pressure n).coeff j x) ∧ (∀ (i : Fin 3) (j : ℤ), LabelSumBounds.UniformWaveClass ActualPrimaryBounds.strip meanEnvelope (β + 1 - ChartScales.kappa) fun (l : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (x : ActualPrimaryBounds.Point) => (((ActualSignedStageControls.parameters l).curlBlock ActualPrimaryBounds.strip request).velocity n i).coeff j x) ∧ ∀ (i : Fin 3) (j : ℤ), LabelSumBounds.UniformWaveClass ActualPrimaryBounds.strip meanEnvelope (β + 1 - 3 * ChartScales.kappa) fun (l : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (x : ActualPrimaryBounds.Point) => (((ActualSignedStageControls.parameters l).goodBlock ActualPrimaryBounds.strip request).velocity n i).coeff j x

The same bounds apply to the actual stored tangent, exact, pressure, curl-difference, and good harmonic blocks.

theorem NavierStokes.ActualSignedOutputBounds.actual_block_bounds {B N0 : ℕ} (G : SignedMeanGain.Geometry) (hs : G.strip = ActualPrimaryBounds.strip) (c : CorrectionState.Context ActualSignedStageControls.Point) (u : CorrectionState.State ActualSignedStageControls.Point) (α : ℝ) (H : MeanStateRegularity.PrimitiveData G.region G.patch.a G.patch.b c u) (hfixed : VariableGaugeMean.reconstructState G.gauge c u = u) (hθ : WeightedClasses.MeanClass G.strip α (u.thetaResidual c)) (hz : WeightedClasses.MeanClass G.strip α (u.axialResidual c)) : have request := LocalSignedRequest.fullRequest G.strip G.patch G.coord c u; (∀ (i : Fin 3) (j : ℤ), LabelSumBounds.UniformWaveClass ActualPrimaryBounds.strip meanEnvelope (α - 1 / 2) fun (l : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (x : ActualPrimaryBounds.Point) => (((ActualSignedStageControls.parameters l).tangentBlock ActualPrimaryBounds.strip request).velocity n i).coeff j x) ∧ (∀ (i : Fin 3) (j : ℤ), LabelSumBounds.UniformWaveClass ActualPrimaryBounds.strip meanEnvelope (α - 1 / 2) fun (l : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (x : ActualPrimaryBounds.Point) => (((ActualSignedStageControls.parameters l).exactBlock ActualPrimaryBounds.strip request).velocity n i).coeff j x) ∧ (∀ (j : ℤ), LabelSumBounds.UniformWaveClass ActualPrimaryBounds.strip meanEnvelope α fun (l : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (x : ActualPrimaryBounds.Point) => (((ActualSignedStageControls.parameters l).exactBlock ActualPrimaryBounds.strip request).pressure n).coeff j x) ∧ (∀ (i : Fin 3) (j : ℤ), LabelSumBounds.UniformWaveClass ActualPrimaryBounds.strip meanEnvelope (α - ChartScales.kappa) fun (l : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (x : ActualPrimaryBounds.Point) => (((ActualSignedStageControls.parameters l).curlBlock ActualPrimaryBounds.strip request).velocity n i).coeff j x) ∧ ∀ (i : Fin 3) (j : ℤ), LabelSumBounds.UniformWaveClass ActualPrimaryBounds.strip meanEnvelope (α - 3 * ChartScales.kappa) fun (l : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (x : ActualPrimaryBounds.Point) => (((ActualSignedStageControls.parameters l).goodBlock ActualPrimaryBounds.strip request).velocity n i).coeff j x

The stored signed blocks are bounded directly from the measured incoming residuals. There is no signed-output estimate among the inputs.

noncomputable def NavierStokes.ActualSignedOutputBounds.localPotential {B N0 : ℕ} (request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2) (l : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (k : ActualSignedStageControls.Frequency) (x : ActualSignedStageControls.FullPoint) : HarmonicCalculus.ComplexVector

The cut native vector-potential coefficient before restoring the carrier or applying the physical coordinate prefactor.

Equations

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

theorem NavierStokes.ActualSignedOutputBounds.localPotential_jets {B N0 : ℕ} {β : ℝ} {request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2} (hR : ∀ (q : Fin 2), PeriodizedWaveBounds.UniformLocalJets ActualSignedStageControls.fullStrip (fun (x : ActualSignedStageControls.SignedLabel B N0) (x_1 : ℕ) (x_2 : ActualSignedStageControls.FullPoint) => ActualSignedStageControls.fullStrip.zeta x_2) β ActualSignedStageControls.phaseCell fun (x : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (x_1 : ActualSignedStageControls.Frequency) (x_2 : ActualSignedStageControls.FullPoint) => request n x_2 q) : PeriodizedWaveBounds.UniformLocalJets ActualSignedStageControls.fullStrip (fun (l : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (x : ActualSignedStageControls.FullPoint) => √(ActualSignedStageControls.fullStrip.zeta x) * ActualSignedStageControls.envelope l n x) (β + 1) ActualSignedStageControls.phaseCell (localPotential request)

The inverse carrier supplies the extra half-power in the actual localized vector potential. Physical scaling factors stay outside it.

theorem NavierStokes.ActualSignedOutputBounds.localized_pressure_jets {B N0 : ℕ} {β : ℝ} {request : ℕ → ActualSignedStageControls.FullPoint → SignedWaveUpdate.Vec2} (hR : ∀ (q : Fin 2), PeriodizedWaveBounds.UniformLocalJets ActualSignedStageControls.fullStrip (fun (x : ActualSignedStageControls.SignedLabel B N0) (x_1 : ℕ) (x_2 : ActualSignedStageControls.FullPoint) => ActualSignedStageControls.fullStrip.zeta x_2) β ActualSignedStageControls.phaseCell fun (x : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (x_1 : ActualSignedStageControls.Frequency) (x_2 : ActualSignedStageControls.FullPoint) => request n x_2 q) : PeriodizedWaveBounds.UniformLocalJets ActualSignedStageControls.fullStrip (fun (l : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (x : ActualSignedStageControls.FullPoint) => √(ActualSignedStageControls.fullStrip.zeta x) * ActualSignedStageControls.envelope l n x) (β + 1) ActualSignedStageControls.phaseCell fun (l : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (k : ActualSignedStageControls.Frequency) => ((copies request l).localized k).pressure n

theorem NavierStokes.ActualSignedOutputBounds.actual_native_potential_pressure_jets {B N0 : ℕ} (G : SignedMeanGain.Geometry) (hs : G.strip = ActualPrimaryBounds.strip) (c : CorrectionState.Context ActualSignedStageControls.Point) (u : CorrectionState.State ActualSignedStageControls.Point) (α : ℝ) (H : MeanStateRegularity.PrimitiveData G.region G.patch.a G.patch.b c u) (hfixed : VariableGaugeMean.reconstructState G.gauge c u = u) (hθ : WeightedClasses.MeanClass G.strip α (u.thetaResidual c)) (hz : WeightedClasses.MeanClass G.strip α (u.axialResidual c)) : have request := LocalSignedRequest.fullRequest G.strip G.patch G.coord c u; PeriodizedWaveBounds.UniformLocalJets ActualSignedStageControls.fullStrip (fun (l : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (x : ActualSignedStageControls.FullPoint) => √(ActualSignedStageControls.fullStrip.zeta x) * ActualSignedStageControls.envelope l n x) α ActualSignedStageControls.phaseCell (localPotential request) ∧ PeriodizedWaveBounds.UniformLocalJets ActualSignedStageControls.fullStrip (fun (l : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (x : ActualSignedStageControls.FullPoint) => √(ActualSignedStageControls.fullStrip.zeta x) * ActualSignedStageControls.envelope l n x) α ActualSignedStageControls.phaseCell fun (l : ActualSignedStageControls.SignedLabel B N0) (n : ℕ) (k : ActualSignedStageControls.Frequency) => ((copies request l).localized k).pressure n

Native potential and pressure bounds directly from the actual incoming residual classes, before their distinct physical prefactors.