Covariance of the fixed physical primary family

The selected primary phases, native matrices, masks, and physical labels are those of CorrectionInitialization.ActualPrimary. The finite family is assembled before averaging. The fixed starting threshold is retained.

@[reducible, inline]

abbrev NavierStokes.ActualPrimaryCovariance.Point : Type

Point: an abbreviation for LocalSignedRequest.Point.

Equations

• NavierStokes.ActualPrimaryCovariance.Point = NavierStokes.LocalSignedRequest.Point

@[reducible, inline]

abbrev NavierStokes.ActualPrimaryCovariance.Slow : Type

Slow: an abbreviation for PhaseCalculus.Slow.

Equations

• NavierStokes.ActualPrimaryCovariance.Slow = NavierStokes.PhaseCalculus.Slow

@[reducible, inline]

abbrev NavierStokes.ActualPrimaryCovariance.Plane : Type

Plane: an abbreviation for TorusInverse.Plane /-! ## Changing the common auxiliary cover does not change a diagonal average -/.

Equations

• NavierStokes.ActualPrimaryCovariance.Plane = NavierStokes.TorusInverse.Plane

Changing the common auxiliary cover does not change a diagonal average

theorem NavierStokes.ActualPrimaryCovariance.covered_common {m k : ℕ} (hk : k ≤ m) (f : Plane → ℝ) (Y : Plane) : PartitionedCovariance.covered m f ((CommonCoverSolve.coverPower k).symm Y) = PartitionedCovariance.covered (m - k) f Y

theorem NavierStokes.ActualPrimaryCovariance.wave_common {m k : ℕ} (hk : k ≤ m) (a : ℝ) (f : Plane → ℝ) (j : ℤ) (phase : Plane → ℝ) (Y : Plane) (theta : ℝ) : PartitionedCovariance.wave a m f j phase ((CommonCoverSolve.coverPower k).symm Y) theta = PartitionedCovariance.wave a (m - k) f j (fun (Z : PartitionedCovariance.Plane) => phase ((CommonCoverSolve.coverPower k).symm Z)) Y theta

theorem NavierStokes.ActualPrimaryCovariance.pair_diagonal_at_cover {D h : ℝ} {vr vt : Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {U : PartitionedCovariance.UnsignedLabel} (P : PartitionedCovariance.PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (a : ℝ) (n : ℕ) (phase : Plane → ℝ) (j i : Fin 2) : (PartitionedCovariance.doubleAverage fun (Y : PartitionedCovariance.Plane) (theta : ℝ) => PartitionedCovariance.wave a n (P.rawRadial hdet j) (P.modes j) phase Y theta * PartitionedCovariance.wave a n (P.rawTangent hdet j i) (P.modes j) phase Y theta) = a ^ 2 * P.matrix i j

theorem NavierStokes.ActualPrimaryCovariance.pair_diagonal_common {D h : ℝ} {vr vt : Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {U : PartitionedCovariance.UnsignedLabel} (P : PartitionedCovariance.PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) {k : ℕ} (hk : k ≤ SlotColoring.nativeIndex h U.1) (outer epsilon : ℝ) (T : PartitionedCovariance.Vec2) (q : ℝ) (x : SlotColoring.Position) (j i : Fin 2) : (PartitionedCovariance.doubleAverage fun (Y : PartitionedCovariance.Plane) (theta : ℝ) => PrimaryFieldAssembly.slotVelocity P hdet outer epsilon T q x j ((CommonCoverSolve.coverPower k).symm Y) theta 0 * PrimaryFieldAssembly.slotVelocity P hdet outer epsilon T q x j ((CommonCoverSolve.coverPower k).symm Y) theta i.succ) = (outer * PartitionedCovariance.amplitude epsilon (PartitionedCovariance.mask D U q x) P.matrix T j) ^ 2 * P.matrix i j

theorem NavierStokes.ActualPrimaryCovariance.pair_diagonal_common_continuous {D h : ℝ} {vr vt : Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {U : PartitionedCovariance.UnsignedLabel} (P : PartitionedCovariance.PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) {k : ℕ} (hk : k ≤ SlotColoring.nativeIndex h U.1) (outer epsilon : ℝ) (T : PartitionedCovariance.Vec2) (q : ℝ) (x : SlotColoring.Position) (j i : Fin 2) : (∀ (Y : TorusInverse.Plane), Continuous fun (theta : ℝ) => PrimaryFieldAssembly.slotVelocity P hdet outer epsilon T q x j ((CommonCoverSolve.coverPower k).symm Y) theta 0 * PrimaryFieldAssembly.slotVelocity P hdet outer epsilon T q x j ((CommonCoverSolve.coverPower k).symm Y) theta i.succ) ∧ Continuous fun (Y : TorusInverse.Plane) => SmoothLoop.angularMean fun (theta : ℝ) => PrimaryFieldAssembly.slotVelocity P hdet outer epsilon T q x j ((CommonCoverSolve.coverPower k).symm Y) theta 0 * PrimaryFieldAssembly.slotVelocity P hdet outer epsilon T q x j ((CommonCoverSolve.coverPower k).symm Y) theta i.succ

Zero masks really remove the selected native fields

theorem NavierStokes.ActualPrimaryCovariance.rawVelocity_zero_of_mask {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (p : Slow) (hm : CorrectionInitialization.ActualPrimary.spatialMask L p = 0) (Y : Plane) : CorrectionInitialization.ActualPrimary.rawVelocity j L (p, Y) = 0

theorem NavierStokes.ActualPrimaryCovariance.commonAmplitude_zero_of_mask {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (p : Slow) (hm : CorrectionInitialization.ActualPrimary.spatialMask L p = 0) (Y : Plane) : CorrectionInitialization.ActualPrimary.commonAmplitude j L p Y = 0

theorem NavierStokes.ActualPrimaryCovariance.tangentMode_zero_of_mask {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (p : Slow) (hm : CorrectionInitialization.ActualPrimary.spatialMask L p = 0) (Y : Plane) (theta : ℝ) : CorrectionInitialization.ActualPrimary.tangentMode j L p Y theta = 0

theorem NavierStokes.ActualPrimaryCovariance.physicalTangentMode_zero_of_mask {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (p : Slow) (hm : CorrectionInitialization.ActualPrimary.spatialMask L p = 0) (Y : Plane) (theta : ℝ) : CorrectionInitialization.ActualPrimary.physicalTangentMode j L p Y theta = 0

theorem NavierStokes.ActualPrimaryCovariance.physicalTangentMode_eq_slot {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (p : Slow) (hp : p ∈ (PrimaryGeometryAssembly.domain CorrectionInitialization.ActualPrimary.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N).carrier L) (Y : Plane) (theta : ℝ) : CorrectionInitialization.ActualPrimary.physicalTangentMode j L p Y theta = PrimaryFieldAssembly.slotVelocity (CorrectionInitialization.ActualPrimary.sourcePair L p hp).pairData CorrectionInitialization.ActualPrimary.vectors_det (ChartScales.Q (BaseChartJets.cellBand L) ^ (-CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h)) (ChartScales.epsilon CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)) (fun (i : Fin 2) => (PrimaryTargetBounds.actualTarget CorrectionInitialization.ActualPrimary.modulation p).ofLp i) (CorrectionInitialization.ActualPrimary.similarityScale L p) (CorrectionInitialization.ActualPrimary.position L p) j Y theta

The same physical point in each fixed label's native coordinates

noncomputable def NavierStokes.ActualPrimaryCovariance.nativePoint {B N0 : ℕ} (n : ℕ) (x : Point) (L : CorrectionInitialization.ActualPrimary.Label B N0) : Slow

Native point, given by nativeSlow L (toAbsolute n x).

Equations

• NavierStokes.ActualPrimaryCovariance.nativePoint n x L = NavierStokes.CorrectionInitialization.ActualPrimary.nativeSlow L (NavierStokes.CorrectionInitialization.ActualPrimary.toAbsolute n x)

theorem NavierStokes.ActualPrimaryCovariance.nativePoint_auxiliary {B N0 : ℕ} (n : ℕ) (x : Point) (L : CorrectionInitialization.ActualPrimary.Label B N0) (Y : Plane) : nativePoint n (x.1, x.2.1, Y) L = nativePoint n x L

theorem NavierStokes.ActualPrimaryCovariance.nativePoint_time {B N0 : ℕ} (n : ℕ) {x : Point} (hT : 0 < x.2.1.1) (L : CorrectionInitialization.ActualPrimary.Label B N0) : 0 < (nativePoint n x L).2.2

theorem NavierStokes.ActualPrimaryCovariance.nativePoint_radius {B N0 : ℕ} (n : ℕ) {x : Point} (hR : 0 < x.1) (L : CorrectionInitialization.ActualPrimary.Label B N0) : 0 < (nativePoint n x L).1

theorem NavierStokes.ActualPrimaryCovariance.nativePoint_inner {B N0 : ℕ} (n : ℕ) {x : Point} (hT : 0 < x.2.1.1) (L : CorrectionInitialization.ActualPrimary.Label B N0) : (BaseChartJets.normalizedCoordinates CorrectionInitialization.ActualPrimary.h (nativePoint n x L)).2 = (BaseChartJets.normalizedCoordinates CorrectionInitialization.ActualPrimary.h (BaseContextAssembly.slowCoordinates x)).2

theorem NavierStokes.ActualPrimaryCovariance.nativePoint_profileRadius {B N0 : ℕ} (n : ℕ) {x : Point} (hT : 0 < x.2.1.1) (hR : 0 < x.1) (L : CorrectionInitialization.ActualPrimary.Label B N0) : PrimaryTargetBounds.profileRadius CorrectionInitialization.ActualPrimary.h (nativePoint n x L) = PrimaryTargetBounds.profileRadius CorrectionInitialization.ActualPrimary.h (BaseContextAssembly.slowCoordinates x)

theorem NavierStokes.ActualPrimaryCovariance.nativePoint_position {B N0 : ℕ} (n : ℕ) (x : Point) (L : CorrectionInitialization.ActualPrimary.Label B N0) : CorrectionInitialization.ActualPrimary.position L (nativePoint n x L) = CorrectionInitialization.ActualPrimary.physicalPosition n x

theorem NavierStokes.ActualPrimaryCovariance.nativePoint_scale {B N0 : ℕ} (n : ℕ) {x : Point} (hT : 0 < x.2.1.1) (L : CorrectionInitialization.ActualPrimary.Label B N0) : CorrectionInitialization.ActualPrimary.similarityScale L (nativePoint n x L) = CorrectionInitialization.ActualPrimary.physicalScale n x

theorem NavierStokes.ActualPrimaryCovariance.nativePoint_mask {B N0 : ℕ} (n : ℕ) {x : Point} (hT : 0 < x.2.1.1) (L : CorrectionInitialization.ActualPrimary.Label B N0) : CorrectionInitialization.ActualPrimary.spatialMask L (nativePoint n x L) = PartitionedCovariance.mask (CoordinateAlgebra.D CorrectionInitialization.ActualPrimary.h) (PrimaryGeometryAssembly.label CorrectionInitialization.ActualPrimary.nominal L) (CorrectionInitialization.ActualPrimary.physicalScale n x) (CorrectionInitialization.ActualPrimary.physicalPosition n x)

theorem NavierStokes.ActualPrimaryCovariance.nativePoint_weight_pos {B N0 : ℕ} (n : ℕ) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) (L : CorrectionInitialization.ActualPrimary.Label B N0) : 0 < PrimaryTargetBounds.movingWeight CorrectionInitialization.ActualPrimary.nominal (nativePoint n x L)

theorem NavierStokes.ActualPrimaryCovariance.nativePoint_reference {B N0 : ℕ} (n : ℕ) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) (L : CorrectionInitialization.ActualPrimary.Label B N0) (hm : CorrectionInitialization.ActualPrimary.spatialMask L (nativePoint n x L) ≠ 0) : nativePoint n x L ∈ PositiveRepresentatives.positivePart (PrimaryGeometryAssembly.referenceSet CorrectionInitialization.ActualPrimary.nominal)

noncomputable def NavierStokes.ActualPrimaryCovariance.unsignedLabels (B N0 n : ℕ) : Finset (CorrectionInitialization.ActualPrimary.Label B N0)

Unsigned labels as an element of Finset (Label B N0).

Equations

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

theorem NavierStokes.ActualPrimaryCovariance.activeLabels_product (B N0 n : ℕ) : CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n = (unsignedLabels B N0 n).product Finset.univ

theorem NavierStokes.ActualPrimaryCovariance.mem_unsignedLabels {B N0 : ℕ} (n : ℕ) (L : CorrectionInitialization.ActualPrimary.Label B N0) : L ∈ unsignedLabels B N0 n ↔ (L, 0) ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n

theorem NavierStokes.ActualPrimaryCovariance.active_cover_le {B N0 : ℕ} (n : ℕ) {L : CorrectionInitialization.ActualPrimary.Label B N0} (hL : L ∈ unsignedLabels B N0 n) : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)

noncomputable def NavierStokes.ActualPrimaryCovariance.signedLabelOf {B N0 : ℕ} (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) : SlotColoring.Label

Signed label of, given by signedLabel (PrimaryGeometryAssembly.label nominal l.1) l.2.

Equations

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

theorem NavierStokes.ActualPrimaryCovariance.signedLabelOf_injective {B N0 : ℕ} : Function.Injective signedLabelOf

noncomputable def NavierStokes.ActualPrimaryCovariance.viewTangent {B N0 : ℕ} (n : ℕ) (x : Point) (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) (Y : Plane) (theta : ℝ) : Fin 3 → ℝ

View tangent, constructed using physicalTangentMode.

Equations

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

theorem NavierStokes.ActualPrimaryCovariance.viewTangent_cross_zero {B N0 : ℕ} (n : ℕ) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) {l m : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2} (hlm : l ≠ m) (Y : Plane) (theta : ℝ) (i : Fin 2) : viewTangent n x l Y theta 0 * viewTangent n x m Y theta i.succ = 0

theorem NavierStokes.ActualPrimaryCovariance.viewTangent_diagonal_continuous {B N0 : ℕ} (n : ℕ) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) (hl : l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n) (i : Fin 2) : (∀ (Y : Plane), Continuous fun (theta : ℝ) => viewTangent n x l Y theta 0 * viewTangent n x l Y theta i.succ) ∧ Continuous fun (Y : Plane) => SmoothLoop.angularMean fun (theta : ℝ) => viewTangent n x l Y theta 0 * viewTangent n x l Y theta i.succ

theorem NavierStokes.ActualPrimaryCovariance.viewTangent_pair_covariance {B N0 : ℕ} (n : ℕ) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) (L : CorrectionInitialization.ActualPrimary.Label B N0) (hL : L ∈ unsignedLabels B N0 n) (i : Fin 2) : (∑ j : Fin 2, PartitionedCovariance.doubleAverage fun (Y : PartitionedCovariance.Plane) (theta : ℝ) => viewTangent n x (L, j) Y theta 0 * viewTangent n x (L, j) Y theta i.succ) = (ChartScales.Q (BaseChartJets.cellBand L) ^ (-CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h)) ^ 2 * ChartScales.epsilon CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L) * CorrectionInitialization.ActualPrimary.spatialMask L (nativePoint n x L) ^ 2 * (PrimaryTargetBounds.actualTarget CorrectionInitialization.ActualPrimary.modulation (nativePoint n x L)).ofLp i

noncomputable def NavierStokes.ActualPrimaryCovariance.viewSum (B N0 n : ℕ) (x : Point) (Y : Plane) (theta : ℝ) : Fin 3 → ℝ

View sum, defined pointwise by ∑ l ∈ activeLabels standardRegion B N0 n, viewTangent n x l Y theta i.

Equations

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

theorem NavierStokes.ActualPrimaryCovariance.viewSum_covariance (B N0 n : ℕ) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) (i : Fin 2) : (PartitionedCovariance.doubleAverage fun (Y : PartitionedCovariance.Plane) (theta : ℝ) => viewSum B N0 n x Y theta 0 * viewSum B N0 n x Y theta i.succ) = ∑ L ∈ unsignedLabels B N0 n, (ChartScales.Q (BaseChartJets.cellBand L) ^ (-CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h)) ^ 2 * ChartScales.epsilon CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L) * CorrectionInitialization.ActualPrimary.spatialMask L (nativePoint n x L) ^ 2 * (PrimaryTargetBounds.actualTarget CorrectionInitialization.ActualPrimary.modulation (nativePoint n x L)).ofLp i

noncomputable def NavierStokes.ActualPrimaryCovariance.physicalLeading (n : ℕ) (x : Point) (i : Fin 2) : ℝ

Physical leading, constructed using physicalScale.

Equations

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

noncomputable def NavierStokes.ActualPrimaryCovariance.partitionFactor (B N0 n : ℕ) (x : Point) : ℝ

Partition factor, given by ∑ L ∈ unsignedLabels B N0 n, spatialMask L (nativePoint n x L) ^ 2.

Equations

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

theorem NavierStokes.ActualPrimaryCovariance.viewSum_covariance_factor (B N0 n : ℕ) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) (i : Fin 2) : (PartitionedCovariance.doubleAverage fun (Y : PartitionedCovariance.Plane) (theta : ℝ) => viewSum B N0 n x Y theta 0 * viewSum B N0 n x Y theta i.succ) = partitionFactor B N0 n x * physicalLeading n x i

Coverage by the fixed chosen labels

theorem NavierStokes.ActualPrimaryCovariance.chosen_threshold_four (B N0 : ℕ) : 4 ≤ (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N

theorem NavierStokes.ActualPrimaryCovariance.physicalScale_pos (n : ℕ) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) : 0 < CorrectionInitialization.ActualPrimary.physicalScale n x

theorem NavierStokes.ActualPrimaryCovariance.physicalScale_le_two (n : ℕ) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) : CorrectionInitialization.ActualPrimary.physicalScale n x ≤ 2

theorem NavierStokes.ActualPrimaryCovariance.physicalScale_forward (n : ℕ) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) : SimilarityCoordinates.forwardScalar (2 * CorrectionInitialization.ActualPrimary.h) (CorrectionInitialization.ActualPrimary.physicalPosition n x 1) (CorrectionInitialization.ActualPrimary.physicalScale n x) = CorrectionInitialization.ActualPrimary.physicalPosition n x 2

theorem NavierStokes.ActualPrimaryCovariance.physicalPosition_normalized (n : ℕ) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) : CorrectionInitialization.ActualPrimary.physicalPosition n x 0 ^ 2 / (2 * CorrectionInitialization.ActualPrimary.physicalScale n x) = (BaseChartJets.normalizedCoordinates CorrectionInitialization.ActualPrimary.h (BaseContextAssembly.slowCoordinates x)).2.1

noncomputable def NavierStokes.ActualPrimaryCovariance.relativeLabel (B N0 : ℕ) (L : CorrectionInitialization.ActualPrimary.Label B N0) : PartitionedCovariance.UnsignedLabel

Relative label, given by ((PrimaryGeometryAssembly.label nominal L).1 - (choice B N0).prepared.N, (PrimaryGeometryAssembly.label nominal L).2).

Equations

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

theorem NavierStokes.ActualPrimaryCovariance.relativeLabel_tail (B N0 : ℕ) (L : CorrectionInitialization.ActualPrimary.Label B N0) : PartitionedCovariance.tailLabel (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N (relativeLabel B N0 L) = PrimaryGeometryAssembly.label CorrectionInitialization.ActualPrimary.nominal L

theorem NavierStokes.ActualPrimaryCovariance.relativeLabel_injective (B N0 : ℕ) : Function.Injective (relativeLabel B N0)

theorem NavierStokes.ActualPrimaryCovariance.partitionFactor_eq_tail (B N0 n : ℕ) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) : partitionFactor B N0 n x = ∑ᶠ (U : PartitionedCovariance.UnsignedLabel), PartitionedCovariance.mask (CoordinateAlgebra.D CorrectionInitialization.ActualPrimary.h) (PartitionedCovariance.tailLabel (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N U) (CorrectionInitialization.ActualPrimary.physicalScale n x) (CorrectionInitialization.ActualPrimary.physicalPosition n x) ^ 2

theorem NavierStokes.ActualPrimaryCovariance.partitionFactor_eq_one (B N0 n : ℕ) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) (hq : CorrectionInitialization.ActualPrimary.physicalScale n x ≤ ChartScales.Q (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N) : partitionFactor B N0 n x = 1

theorem NavierStokes.ActualPrimaryCovariance.Q_antitone : Antitone ChartScales.Q

theorem NavierStokes.ActualPrimaryCovariance.Q_succ (n : ℕ) : ChartScales.Q (n + 1) = ChartScales.Q n / 2

theorem NavierStokes.ActualPrimaryCovariance.physicalScale_tail (B N0 : ℕ) {n : ℕ} (hn : (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N + 1 ≤ n) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) : CorrectionInitialization.ActualPrimary.physicalScale n x ≤ ChartScales.Q (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N

Covariance of the literal initialized tangent pieces

noncomputable def NavierStokes.ActualPrimaryCovariance.tangentSum (B N0 : ℕ) : CorrectionState.Oscillation Point

Tangent sum, defined pointwise by ∑ l ∈ activeLabels standardRegion B N0 n, (piece standardRegion l.2 l.1).tangentVelocity n z i.

Equations

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

noncomputable def NavierStokes.ActualPrimaryCovariance.tangentCovariance (B N0 : ℕ) (i j : Fin 3) : CorrectionState.ScalarField Point

Tangent covariance, given by CorrectionState.bilinearCovariance (tangentSum B N0) (tangentSum B N0) i j.

Equations

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

noncomputable def NavierStokes.ActualPrimaryCovariance.leadingStress (i : Fin 2) (n : ℕ) (x : Point) : ℝ

Leading stress, with branches according to i = 0.

Equations

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

theorem NavierStokes.ActualPrimaryCovariance.tangentSum_eq_viewSum (B N0 n : ℕ) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) (Y : Plane) (theta : ℝ) (i : Fin 3) : tangentSum B N0 n ((x.1, x.2.1, Y), theta) i = ChartScales.Q n ^ CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h * viewSum B N0 n x Y theta i

theorem NavierStokes.ActualPrimaryCovariance.chart_physical_leading (n : ℕ) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) (i : Fin 2) : (ChartScales.Q n ^ CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) ^ 2 * physicalLeading n x i = leadingStress i n x

theorem NavierStokes.ActualPrimaryCovariance.mean_tangentCovariance_factor (B N0 n : ℕ) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) (i : Fin 2) : StateMomentBalances.meanBar (tangentCovariance B N0 0 i.succ) n x = partitionFactor B N0 n x * leadingStress i n x

theorem NavierStokes.ActualPrimaryCovariance.mean_tangentCovariance_eq_leading (B N0 : ℕ) {n : ℕ} (hn : (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N + 1 ≤ n) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) (i : Fin 2) : StateMomentBalances.meanBar (tangentCovariance B N0 0 i.succ) n x = leadingStress i n x

theorem NavierStokes.ActualPrimaryCovariance.mean_tangentCovariance_jets (B N0 : ℕ) {n : ℕ} (hn : (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N + 1 ≤ n) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) (i : Fin 2) (m : ℕ) : iteratedFDeriv ℝ m (StateMomentBalances.meanBar (tangentCovariance B N0 0 i.succ) n) x = iteratedFDeriv ℝ m (leadingStress i n) x

The exact finite low-band defect

noncomputable def NavierStokes.ActualPrimaryCovariance.dyadicTail (N : ℕ) (q : ℝ) : ℝ

Dyadic tail, given by ∑ᶠ n : ℕ, SquaredPartition.dyadicMask ((n + N : ℕ) : ℤ) q ^ 2.

Equations

• NavierStokes.ActualPrimaryCovariance.dyadicTail N q = ∑ᶠ (n : ℕ), NavierStokes.SquaredPartition.dyadicMask (↑(n + N)) q ^ 2

theorem NavierStokes.ActualPrimaryCovariance.mask_tail_eq_dyadicTail (D : ℝ) (N : ℕ) {q : ℝ} (hq : 0 < q) (x : SlotColoring.Position) : ∑ᶠ (U : PartitionedCovariance.UnsignedLabel), PartitionedCovariance.mask D (PartitionedCovariance.tailLabel N U) q x ^ 2 = dyadicTail N q

noncomputable def NavierStokes.ActualPrimaryCovariance.missingWeight (N : ℕ) (q : ℝ) : ℝ

Missing weight, given by ∑ m ∈ Finset.Icc (-1 : ℤ) ((N : ℤ) - 1), SquaredPartition.dyadicMask m q ^ 2.

Equations

• NavierStokes.ActualPrimaryCovariance.missingWeight N q = ∑ m ∈ Finset.Icc (-1) (↑N - 1), NavierStokes.SquaredPartition.dyadicMask m q ^ 2

theorem NavierStokes.ActualPrimaryCovariance.missingWeight_smooth (N : ℕ) : ContDiff ℝ (↑⊤) (missingWeight N)

theorem NavierStokes.ActualPrimaryCovariance.missingWeight_compact (N : ℕ) : HasCompactSupport (missingWeight N)

theorem NavierStokes.ActualPrimaryCovariance.dyadicMask_zero_below_minus_one {q : ℝ} (hq : q ≤ 2) {m : ℤ} (hm : m < -1) : SquaredPartition.dyadicMask m q = 0

theorem NavierStokes.ActualPrimaryCovariance.missingWeight_add_tail (N : ℕ) {q : ℝ} (hq : 0 < q) (hq2 : q ≤ 2) : missingWeight N q + dyadicTail N q = 1

theorem NavierStokes.ActualPrimaryCovariance.partitionFactor_eq_one_sub_missing (B N0 n : ℕ) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) : partitionFactor B N0 n x = 1 - missingWeight (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N (CorrectionInitialization.ActualPrimary.physicalScale n x)

noncomputable def NavierStokes.ActualPrimaryCovariance.averagedDefect (B N0 : ℕ) (i : Fin 2) : CorrectionState.ScalarField Point

Averaged defect, given by StateMomentBalances.meanBar (tangentCovariance B N0 0 i.succ) - leadingStress i.

Equations

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

theorem NavierStokes.ActualPrimaryCovariance.averagedDefect_eq (B N0 n : ℕ) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) (i : Fin 2) : averagedDefect B N0 i n x = -missingWeight (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N (CorrectionInitialization.ActualPrimary.physicalScale n x) * leadingStress i n x

theorem NavierStokes.ActualPrimaryCovariance.averagedDefect_zero_tail (B N0 : ℕ) {n : ℕ} (hn : (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N + 1 ≤ n) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) (i : Fin 2) : averagedDefect B N0 i n x = 0

All-order bounds for the retained finite prefix

theorem NavierStokes.ActualPrimaryCovariance.memClass_of_finite_bands {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {alpha beta : ℝ} {f : ℕ → D → E} (hf : WeightedClasses.MemClass s w alpha f) (N : ℕ) (hz : ∀ (n : ℕ), N ≤ n → ∀ x ∈ s.domain, f n x = 0) : WeightedClasses.MemClass s w beta f

An actual class whose fields vanish after a fixed band has every exponent. The new constant is one finite sum of powers of the original positive band scales, chosen before the band and spatial point.

theorem NavierStokes.ActualPrimaryCovariance.physicalScale_unweighted : WeightedClasses.UnweightedClass (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion) 0 CorrectionInitialization.ActualPrimary.physicalScale

theorem NavierStokes.ActualPrimaryCovariance.missingWeight_unweighted (N : ℕ) : WeightedClasses.UnweightedClass (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion) 0 fun (n : ℕ) (x : BaseContextAssembly.Point) => missingWeight N (CorrectionInitialization.ActualPrimary.physicalScale n x)

theorem NavierStokes.ActualPrimaryCovariance.leadingStress_meanClass (i : Fin 2) : WeightedClasses.MeanClass (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion) 1 (leadingStress i)

theorem NavierStokes.ActualPrimaryCovariance.averagedDefect_meanClass_one (B N0 : ℕ) (i : Fin 2) : WeightedClasses.MeanClass (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion) 1 (averagedDefect B N0 i)

theorem NavierStokes.ActualPrimaryCovariance.averagedDefect_meanClass (B N0 : ℕ) (i : Fin 2) (beta : ℝ) : WeightedClasses.MeanClass (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion) beta (averagedDefect B N0 i)

The finite omitted primary prefix is an actual error in every mean class, with no new threshold or primary choice and no assumption on the assembled covariance.

theorem NavierStokes.ActualPrimaryCovariance.averagedDefect_derivative_meanClass (B N0 : ℕ) (i : Fin 2) (beta : ℝ) : WeightedClasses.MeanClass (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion) beta fun (n : ℕ) => fderiv ℝ (averagedDefect B N0 i n)

Every actual spatial derivative of the averaged covariance error has the same arbitrary exponent; the finite-prefix constants may depend on the chosen exponent and derivative order.

theorem NavierStokes.ActualPrimaryCovariance.averagedDefect_radialDiv_meanClass (B N0 : ℕ) (i : Fin 2) (beta weight : ℝ) : WeightedClasses.MeanClass (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion) beta ((CorrectionInitialization.ActualPrimary.commonContext B).operators.radialDiv weight (averagedDefect B N0 i))

Direct interfaces for the initial mean balance

theorem NavierStokes.ActualPrimaryCovariance.meanBar_of_fiber_constant (f : CorrectionState.ScalarField Point) (hf : ∀ (n : ℕ) (x : Point) (Y : PressureStream.Plane), f n (x.1, x.2.1, Y) = f n x) : StateMomentBalances.meanBar f = f

theorem NavierStokes.ActualPrimaryCovariance.meanBar_leadingStress (i : Fin 2) : StateMomentBalances.meanBar (leadingStress i) = leadingStress i

theorem NavierStokes.ActualPrimaryCovariance.meanBar_virtualTheta (B : ℕ) : StateMomentBalances.meanBar (CorrectionInitialization.ActualPrimary.commonContext B).virtualTheta = (CorrectionInitialization.ActualPrimary.commonContext B).virtualTheta

theorem NavierStokes.ActualPrimaryCovariance.meanBar_virtualAxial (B : ℕ) : StateMomentBalances.meanBar (CorrectionInitialization.ActualPrimary.commonContext B).virtualAxial = (CorrectionInitialization.ActualPrimary.commonContext B).virtualAxial

theorem NavierStokes.ActualPrimaryCovariance.tangent_virtual_bar_meanClass (B N0 : ℕ) : WeightedClasses.MeanClass (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion) 2 (StateMomentBalances.meanBar (tangentCovariance B N0 0 1) - StateMomentBalances.meanBar (CorrectionInitialization.ActualPrimary.commonContext B).virtualTheta) ∧ WeightedClasses.MeanClass (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion) 2 (StateMomentBalances.meanBar (tangentCovariance B N0 0 2) - StateMomentBalances.meanBar (CorrectionInitialization.ActualPrimary.commonContext B).virtualAxial)

The measured tangent covariance matches the same full virtual stress up to its actual order-two Borel remainder and the explicitly retained finite primary prefix. This supplies both initial averaged radial fluxes.

Actual closed support and separation on the common chart

The support statements use the literal cut amplitude. Compactness of the padded native rectangle gives closed lifted support on the torus, so passing from nonzero values to topological support requires no false zero-germ claim at an edge. The common-chart disjointness statements retain the intersection with the genuine open domain.

theorem NavierStokes.ActualPrimaryCovariance.quotientPoint_eq_of_torusEq {x y : Plane} (hxy : SlotGeometry.torusEq x y) : TorusAverages.quotientPoint x = TorusAverages.quotientPoint y

theorem NavierStokes.ActualPrimaryCovariance.quotientPoint_continuous : Continuous TorusAverages.quotientPoint

theorem NavierStokes.ActualPrimaryCovariance.orientedRectangle_isCompact (c a b : Plane) (r : ℝ) : IsCompact (SlotGeometry.orientedRectangle c a b r)

theorem NavierStokes.ActualPrimaryCovariance.liftedSupport_isClosed (n : ℕ) {S : Set Plane} (hS : IsCompact S) : IsClosed (SlotGeometry.liftedSupport n S)

theorem NavierStokes.ActualPrimaryCovariance.slotAmplitude_supported {D h : ℝ} {vr vt : Plane} {sys : PartitionedCovariance.SlotSystem D h vr vt} {U : PartitionedCovariance.UnsignedLabel} (P : PartitionedCovariance.PairData sys U) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (outer epsilon : ℝ) (T : PartitionedCovariance.Vec2) (q : ℝ) (x : SlotColoring.Position) (j : Fin 2) {Y : Plane} (hY : PrimaryFieldAssembly.slotAmplitude P hdet outer epsilon T q x j Y ≠ 0) : Y ∈ SlotGeometry.liftedSupport (SlotColoring.nativeIndex h U.1) (PartitionedCovariance.slotSet h sys.radius vr vt (PartitionedCovariance.signedLabel U j))

noncomputable def NavierStokes.ActualPrimaryCovariance.absoluteAuxiliary (n : ℕ) (x : Point) : Plane

Absolute auxiliary, given by (CommonCoverSolve.coverPower (CorrectionInitialization.CommonWindow.index h n)).symm x.2.2.

Equations

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

theorem NavierStokes.ActualPrimaryCovariance.absoluteAuxiliary_continuous (n : ℕ) : Continuous (absoluteAuxiliary n)

noncomputable def NavierStokes.ActualPrimaryCovariance.physicalWindow (n : ℕ) (x : Point) : LabelSumBounds.WindowPoint

Physical window, given by (SquaredPartition.logCoordinate (physicalScale n x), physicalPosition n x).

Equations

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

theorem NavierStokes.ActualPrimaryCovariance.physicalPosition_continuous (n : ℕ) : Continuous (CorrectionInitialization.ActualPrimary.physicalPosition n)

theorem NavierStokes.ActualPrimaryCovariance.physicalScale_continuousAt (n : ℕ) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) : ContinuousAt (CorrectionInitialization.ActualPrimary.physicalScale n) x

theorem NavierStokes.ActualPrimaryCovariance.physicalWindow_continuousOn (n : ℕ) : ContinuousOn (physicalWindow n) (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain

noncomputable def NavierStokes.ActualPrimaryCovariance.cutAmplitude {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : CorrectionInitialization.ActualPrimary.FullPoint → HarmonicCalculus.ComplexVector

Cut amplitude, given by ((chartCoefficients j L).withCutoff (chartCutoff j L)).amplitude n.

Equations

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

theorem NavierStokes.ActualPrimaryCovariance.cutAmplitude_eq_common {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) (theta : ℝ) : cutAmplitude j L n (x, theta) = (ChartScales.Q n ^ CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h * ChartScales.Q (BaseChartJets.cellBand L) ^ (-CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h)) • CorrectionInitialization.ActualPrimary.commonAmplitude j L (nativePoint n x L) (absoluteAuxiliary n x)

theorem NavierStokes.ActualPrimaryCovariance.cutAmplitude_support {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) (theta : ℝ) (hn : cutAmplitude j L n (x, theta) ≠ 0) : (CorrectionInitialization.ActualPrimary.physicalScale n x, CorrectionInitialization.ActualPrimary.physicalPosition n x) ∈ PhysicalWaveSum.labelRegion (CoordinateAlgebra.D CorrectionInitialization.ActualPrimary.h) (signedLabelOf (L, j)) ∧ absoluteAuxiliary n x ∈ SlotGeometry.liftedSupport (SlotColoring.nativeIndex CorrectionInitialization.ActualPrimary.h (signedLabelOf (L, j)).1) (PartitionedCovariance.slotSet CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius CorrectionInitialization.ActualPrimary.radialVector CorrectionInitialization.ActualPrimary.temporalVector (signedLabelOf (L, j)))

theorem NavierStokes.ActualPrimaryCovariance.cutAmplitude_tsupport_physical {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) (theta : ℝ) (ht : (x, theta) ∈ tsupport (cutAmplitude j L n)) : (CorrectionInitialization.ActualPrimary.physicalScale n x, CorrectionInitialization.ActualPrimary.physicalPosition n x) ∈ PhysicalWaveSum.labelRegion (CoordinateAlgebra.D CorrectionInitialization.ActualPrimary.h) (signedLabelOf (L, j)) ∧ absoluteAuxiliary n x ∈ SlotGeometry.liftedSupport (SlotColoring.nativeIndex CorrectionInitialization.ActualPrimary.h (signedLabelOf (L, j)).1) (PartitionedCovariance.slotSet CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius CorrectionInitialization.ActualPrimary.radialVector CorrectionInitialization.ActualPrimary.temporalVector (signedLabelOf (L, j)))

theorem NavierStokes.ActualPrimaryCovariance.cutAmplitude_tsupport {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) (theta : ℝ) (ht : (x, theta) ∈ tsupport (cutAmplitude j L n)) : physicalWindow n x ∈ LabelSumBounds.closedWindow (CoordinateAlgebra.D CorrectionInitialization.ActualPrimary.h) (signedLabelOf (L, j)) ∧ absoluteAuxiliary n x ∈ SlotGeometry.liftedSupport (SlotColoring.nativeIndex CorrectionInitialization.ActualPrimary.h (signedLabelOf (L, j)).1) (PartitionedCovariance.slotSet CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius CorrectionInitialization.ActualPrimary.radialVector CorrectionInitialization.ActualPrimary.temporalVector (signedLabelOf (L, j)))

theorem NavierStokes.ActualPrimaryCovariance.piece_support {B N0 : ℕ} (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) (n : ℕ) (x : Point) (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) (theta : ℝ) (ht : (x, theta) ∈ tsupport (((CorrectionInitialization.ActualPrimary.piece CorrectionInitialization.ActualPrimary.standardRegion l.2 l.1).coefficients.withCutoff (CorrectionInitialization.ActualPrimary.piece CorrectionInitialization.ActualPrimary.standardRegion l.2 l.1).cutoff).amplitude n)) : physicalWindow n x ∈ LabelSumBounds.closedWindow (CoordinateAlgebra.D CorrectionInitialization.ActualPrimary.h) (signedLabelOf l) ∧ absoluteAuxiliary n x ∈ SlotGeometry.liftedSupport (SlotColoring.nativeIndex CorrectionInitialization.ActualPrimary.h (signedLabelOf l).1) (PartitionedCovariance.slotSet CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.slots.radius CorrectionInitialization.ActualPrimary.radialVector CorrectionInitialization.ActualPrimary.temporalVector (signedLabelOf l))

theorem NavierStokes.ActualPrimaryCovariance.cutAmplitude_tsupport_active {B N0 : ℕ} (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) (n : ℕ) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) (theta : ℝ) (ht : (x, theta) ∈ tsupport (cutAmplitude l.2 l.1 n)) : l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n

theorem NavierStokes.ActualPrimaryCovariance.cutAmplitude_inactive_germ {B N0 : ℕ} (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) (n : ℕ) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) (theta : ℝ) (hl : l ∉ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n) : cutAmplitude l.2 l.1 n =ᶠ[nhds (x, theta)] fun (x : Point × ℝ) => 0

theorem NavierStokes.ActualPrimaryCovariance.velocity_inactive_germ {B N0 : ℕ} (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) (n : ℕ) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) (theta : ℝ) (hl : l ∉ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n) : (CorrectionInitialization.ActualPrimary.piece CorrectionInitialization.ActualPrimary.standardRegion l.2 l.1).velocity n =ᶠ[nhds (x, theta)] fun (x : Point × ℝ) => 0

theorem NavierStokes.ActualPrimaryCovariance.cutAmplitude_tsupport_disjoint {B N0 : ℕ} (n : ℕ) {l m : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2} (hlm : l ≠ m) : Disjoint (Prod.fst ⁻¹' (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain ∩ tsupport (cutAmplitude l.2 l.1 n)) (Prod.fst ⁻¹' (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain ∩ tsupport (cutAmplitude m.2 m.1 n))

theorem NavierStokes.ActualPrimaryCovariance.exactAmplitude_tsupport_disjoint {B N0 : ℕ} (n : ℕ) {l m : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2} (hlm : l ≠ m) : Disjoint (Prod.fst ⁻¹' (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain ∩ tsupport ((CorrectionInitialization.ActualPrimary.piece CorrectionInitialization.ActualPrimary.standardRegion l.2 l.1).exactCoefficients.amplitude n)) (Prod.fst ⁻¹' (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain ∩ tsupport ((CorrectionInitialization.ActualPrimary.piece CorrectionInitialization.ActualPrimary.standardRegion m.2 m.1).exactCoefficients.amplitude n))

theorem NavierStokes.ActualPrimaryCovariance.velocity_tsupport_disjoint {B N0 : ℕ} (n : ℕ) {l m : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2} (hlm : l ≠ m) : Disjoint (Prod.fst ⁻¹' (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain ∩ tsupport ((CorrectionInitialization.ActualPrimary.piece CorrectionInitialization.ActualPrimary.standardRegion l.2 l.1).velocity n)) (Prod.fst ⁻¹' (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain ∩ tsupport ((CorrectionInitialization.ActualPrimary.piece CorrectionInitialization.ActualPrimary.standardRegion m.2 m.1).velocity n))

Inactive physical labels vanish on entire slow fibers

The radial coordinate is unrestricted here. A nonzero literal attached coefficient forces radial interior support and a nonzero actual mask, which imply membership in the fixed active-label set. On an inactive label the entire raw coefficient is therefore zero in an open slow neighborhood; this also removes its actual curl and Gaussian term.

theorem NavierStokes.ActualPrimaryCovariance.attachedRawPressure_zero_of_attachedVelocity_zero {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (x : ActualSignedGeometry.Native) (hv : CorrectionInitialization.ActualPrimary.attachedRawVelocity j L x = 0) : CorrectionInitialization.ActualPrimary.attachedRawPressure j L x = 0

theorem NavierStokes.ActualPrimaryCovariance.active_of_native_nonzero {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) {x : Point} (hs : x.2.1 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier) (hr : PrimaryTargetBounds.profileRadius CorrectionInitialization.ActualPrimary.h (nativePoint n x L) ∈ Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)) (hm : CorrectionInitialization.ActualPrimary.spatialMask L (nativePoint n x L) ≠ 0) : (L, j) ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n

theorem NavierStokes.ActualPrimaryCovariance.attachedRawVelocity_zero_inactive {B N0 : ℕ} (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) (n : ℕ) {x : Point} (hs : x.2.1 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier) (hl : l ∉ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n) (Y : Plane) : CorrectionInitialization.ActualPrimary.attachedRawVelocity l.2 l.1 (nativePoint n x l.1, Y) = 0

theorem NavierStokes.ActualPrimaryCovariance.nativeCoefficients_inactive {B N0 : ℕ} (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) (n : ℕ) {x : Point} (hs : x.2.1 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier) (theta : ℝ) (hl : l ∉ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n) : (CorrectionInitialization.ActualPrimary.chartCoefficients l.2 l.1).amplitude n (x, theta) = 0 ∧ (CorrectionInitialization.ActualPrimary.chartCoefficients l.2 l.1).pressure n (x, theta) = 0

theorem NavierStokes.ActualPrimaryCovariance.cutAmplitude_inactive_fullFiber_germ {B N0 : ℕ} (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) (n : ℕ) {x : Point} (hs : x.2.1 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier) (theta : ℝ) (hl : l ∉ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n) : cutAmplitude l.2 l.1 n =ᶠ[nhds (x, theta)] fun (x : Point × ℝ) => 0

theorem NavierStokes.ActualPrimaryCovariance.piece_velocity_inactive_germ {B N0 : ℕ} (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) (n : ℕ) {x : Point} (hs : x.2.1 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier) (theta : ℝ) (hl : l ∉ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n) : (CorrectionInitialization.ActualPrimary.piece CorrectionInitialization.ActualPrimary.standardRegion l.2 l.1).velocity n =ᶠ[nhds (x, theta)] fun (x : Point × ℝ) => 0

theorem NavierStokes.ActualPrimaryCovariance.piece_velocity_inactive {B N0 : ℕ} (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) (n : ℕ) {x : Point} (hs : x.2.1 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier) (theta : ℝ) (hl : l ∉ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n) : (CorrectionInitialization.ActualPrimary.piece CorrectionInitialization.ActualPrimary.standardRegion l.2 l.1).velocity n (x, theta) = 0

theorem NavierStokes.ActualPrimaryCovariance.piece_pressure_inactive {B N0 : ℕ} (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) (n : ℕ) {x : Point} (hs : x.2.1 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier) (theta : ℝ) (hl : l ∉ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n) : (CorrectionInitialization.ActualPrimary.piece CorrectionInitialization.ActualPrimary.standardRegion l.2 l.1).pressure n (x, theta) = 0

theorem NavierStokes.ActualPrimaryCovariance.piece_excluded_inactive {B N0 : ℕ} (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) (n : ℕ) {x : Point} (hs : x.2.1 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier) (theta : ℝ) (hl : l ∉ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n) : (CorrectionInitialization.ActualPrimary.piece CorrectionInitialization.ActualPrimary.standardRegion l.2 l.1).excluded n (x, theta) = 0