The actual slow base on a coarsest common integer cover

The physical base, virtual stress, dyadic band and small parameter stay fixed. Only the integer cover used in the graph operators changes. The forward real-lift map is the genuine integer covering matrix, with its actual norm.

@[reducible, inline]

abbrev NavierStokes.CommonBaseContext.Plane : Type

Plane: an abbreviation for BaseContextAssembly.Plane.

Equations

• NavierStokes.CommonBaseContext.Plane = NavierStokes.BaseContextAssembly.Plane

@[reducible, inline]

abbrev NavierStokes.CommonBaseContext.Point : Type

Point: an abbreviation for BaseContextAssembly.Point.

Equations

• NavierStokes.CommonBaseContext.Point = NavierStokes.BaseContextAssembly.Point

@[reducible, inline]

abbrev NavierStokes.CommonBaseContext.Slow : Type

Slow: an abbreviation for BaseContextAssembly.Slow.

Equations

• NavierStokes.CommonBaseContext.Slow = NavierStokes.BaseContextAssembly.Slow

structure NavierStokes.CommonBaseContext.IndexBounds (h : ℝ) (index : ℕ → ℕ) (K : ℕ) : Prop

Scalar hypotheses on the chosen common index, including every low band.

• le_native (n : ℕ) : index n ≤ ChartScales.nativeIndex h n
• gap_le (n : ℕ) : ChartScales.nativeIndex h n - index n ≤ K

theorem NavierStokes.CommonBaseContext.IndexBounds.native_le_add {h : ℝ} {index : ℕ → ℕ} {K : ℕ} (H : IndexBounds h index K) (n : ℕ) : ChartScales.nativeIndex h n ≤ index n + K

theorem NavierStokes.CommonBaseContext.IndexBounds.add_gap {h : ℝ} {index : ℕ → ℕ} {K : ℕ} (H : IndexBounds h index K) (n : ℕ) : index n + (ChartScales.nativeIndex h n - index n) = ChartScales.nativeIndex h n

theorem NavierStokes.CommonBaseContext.IndexBounds.commonRatio {h : ℝ} {index : ℕ → ℕ} {K : ℕ} (H : IndexBounds h index K) (n : ℕ) : 0 < MeanChartCompatibility.commonRatio h n (index n) ∧ MeanChartCompatibility.commonRatio h n (index n) ≤ ChartScales.Tg ^ K

noncomputable def NavierStokes.CommonBaseContext.radialFrequency (h : ℝ) (index : ℕ → ℕ) (n : ℕ) : ℝ

Radial frequency, given by ChartScales.Lambda ^ index n * ChartScales.Q n ^ (ChartScales.radialExponent h / 2).

Equations

• NavierStokes.CommonBaseContext.radialFrequency h index n = NavierStokes.ChartScales.Lambda ^ index n * NavierStokes.ChartScales.Q n ^ (NavierStokes.ChartScales.radialExponent h / 2)

noncomputable def NavierStokes.CommonBaseContext.fastCoefficient (h : ℝ) (index : ℕ → ℕ) (n : ℕ) : ℝ

Fast coefficient, given by ChartScales.Tg ^ index n * ChartScales.Q n ^ (1 + h).

Equations

• NavierStokes.CommonBaseContext.fastCoefficient h index n = NavierStokes.ChartScales.Tg ^ index n * NavierStokes.ChartScales.Q n ^ (1 + h)

theorem NavierStokes.CommonBaseContext.radialFrequency_pos (h : ℝ) (index : ℕ → ℕ) (n : ℕ) : 0 < radialFrequency h index n

theorem NavierStokes.CommonBaseContext.fastCoefficient_pos (h : ℝ) (index : ℕ → ℕ) (n : ℕ) : 0 < fastCoefficient h index n

theorem NavierStokes.CommonBaseContext.radialFrequency_mono (h : ℝ) {i j : ℕ → ℕ} {n : ℕ} (hij : i n ≤ j n) : radialFrequency h i n ≤ radialFrequency h j n

theorem NavierStokes.CommonBaseContext.fastCoefficient_mono (h : ℝ) {i j : ℕ → ℕ} {n : ℕ} (hij : i n ≤ j n) : fastCoefficient h i n ≤ fastCoefficient h j n

theorem NavierStokes.CommonBaseContext.radialFrequency_add (h : ℝ) (i k : ℕ → ℕ) (n : ℕ) : radialFrequency h (fun (m : ℕ) => i m + k m) n = ChartScales.Lambda ^ k n * radialFrequency h i n

theorem NavierStokes.CommonBaseContext.fastCoefficient_add (h : ℝ) (i k : ℕ → ℕ) (n : ℕ) : fastCoefficient h (fun (m : ℕ) => i m + k m) n = ChartScales.Tg ^ k n * fastCoefficient h i n

theorem NavierStokes.CommonBaseContext.radialFrequency_bounds {h : ℝ} {index : ℕ → ℕ} {K : ℕ} (H : IndexBounds h index K) (n : ℕ) : ChartScales.radialCoefficient h n / ChartScales.Lambda ^ K ≤ radialFrequency h index n ∧ radialFrequency h index n ≤ ChartScales.radialCoefficient h n

theorem NavierStokes.CommonBaseContext.fastCoefficient_bounds {h : ℝ} {index : ℕ → ℕ} {K : ℕ} (H : IndexBounds h index K) (n : ℕ) : ChartScales.timeCoefficient h n / ChartScales.Tg ^ K ≤ fastCoefficient h index n ∧ fastCoefficient h index n ≤ ChartScales.timeCoefficient h n

theorem NavierStokes.CommonBaseContext.fastCoefficient_inverse_bound {h : ℝ} {index : ℕ → ℕ} {K : ℕ} (H : IndexBounds h index K) (hh : 0 ≤ h) {n : ℕ} (hn : 4 ≤ n) : (fastCoefficient h index n)⁻¹ ≤ ChartScales.Tg ^ (K + 1) * ChartScales.S n

noncomputable def NavierStokes.CommonBaseContext.reconstruction (h : ℝ) (index : ℕ → ℕ) (a b : ℝ) (hab : a < b) : CorrectionState.ReconstructionData

Reconstruction, bundling exponent, inner, outer, inner_lt_outer and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.CommonBaseContext.operators (h : ℝ) (index : ℕ → ℕ) (a b : ℝ) (hab : a < b) : MeanIncrementBounds.Operators Point

Operators, constructed using CorrectionState.graphOperators.

Equations

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

theorem NavierStokes.CommonBaseContext.operators_native (h a b : ℝ) (hab : a < b) : operators h (ChartScales.nativeIndex h) a b hab = BaseContextAssembly.operators h a b hab

theorem NavierStokes.CommonBaseContext.operators_match_physical (h : ℝ) (index : ℕ → ℕ) (a b : ℝ) (hab : a < b) (n : ℕ) : PhysicalResidualTZ.MatchesAtTZ (operators h index a b hab) (PhysicalResidualBridge.commonGraph (ChartScales.Q n) h (index n)) n

theorem NavierStokes.CommonBaseContext.operator_bounds {h : ℝ} (hh : 0 ≤ h) (U : LocalSignedRequest.SlowRegion (2 * h)) {index : ℕ → ℕ} (hi : ∀ (n : ℕ), index n ≤ ChartScales.nativeIndex h n) {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) : MeanIncrementBounds.OperatorBounds (BaseContextAssembly.movingStrip hh U a b cL cR ha hcL hcR) (operators h index a b hab) ChartScales.kappa

noncomputable def NavierStokes.CommonBaseContext.coverLift (k : ℕ) : Point ≃L[ℝ] Point

The forward integer covering on the full free auxiliary lift.

Equations

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

@[simp]

theorem NavierStokes.CommonBaseContext.coverLift_apply (k : ℕ) (x : Point) : (coverLift k) x = (x.1, x.2.1, (CommonCoverSolve.coverPower k) x.2.2)

@[simp]

theorem NavierStokes.CommonBaseContext.coverLift_slow (k : ℕ) (x : Point) : BaseContextAssembly.slowCoordinates ((coverLift k) x) = BaseContextAssembly.slowCoordinates x

theorem NavierStokes.CommonBaseContext.coverLift_eR (k : ℕ) : (coverLift k) (1, 0, 0) = (1, 0, 0)

theorem NavierStokes.CommonBaseContext.coverLift_eZ (k : ℕ) : (coverLift k) (0, (0, 1), 0) = (0, (0, 1), 0)

theorem NavierStokes.CommonBaseContext.coverLift_eT (k : ℕ) : (coverLift k) (0, (1, 0), 0) = (0, (1, 0), 0)

theorem NavierStokes.CommonBaseContext.coverPower_radial (k : ℕ) : (CommonCoverSolve.coverPower k) (TorusInverse.vector TorusInverse.Direction.radial) = ChartScales.Lambda ^ k • TorusInverse.vector TorusInverse.Direction.radial

theorem NavierStokes.CommonBaseContext.coverPower_temporal (k : ℕ) : (CommonCoverSolve.coverPower k) (TorusInverse.vector TorusInverse.Direction.temporal) = ChartScales.Tg ^ k • TorusInverse.vector TorusInverse.Direction.temporal

theorem NavierStokes.CommonBaseContext.coverLift_vR (k : ℕ) : (coverLift k) (0, 0, TorusInverse.vector TorusInverse.Direction.radial) = ChartScales.Lambda ^ k • (0, 0, TorusInverse.vector TorusInverse.Direction.radial)

theorem NavierStokes.CommonBaseContext.coverLift_vT (k : ℕ) : (coverLift k) (0, 0, TorusInverse.vector TorusInverse.Direction.temporal) = ChartScales.Tg ^ k • (0, 0, TorusInverse.vector TorusInverse.Direction.temporal)

theorem NavierStokes.CommonBaseContext.coverPower_comp (i k : ℕ) (Y : Plane) : (CommonCoverSolve.coverPower k) ((CommonCoverSolve.coverPower i) Y) = (CommonCoverSolve.coverPower (i + k)) Y

theorem NavierStokes.CommonBaseContext.coverLift_physicalToChart (h : ℝ) (n i k : ℕ) (x : Point) : (coverLift k) ((PhysicalResidualTZ.physicalToChartTZ h n i) x) = (PhysicalResidualTZ.physicalToChartTZ h n (i + k)) x

theorem NavierStokes.CommonBaseContext.IndexBounds.physicalToChart {h : ℝ} {index : ℕ → ℕ} {K : ℕ} (H : IndexBounds h index K) (n : ℕ) (x : Point) : (coverLift (ChartScales.nativeIndex h n - index n)) ((PhysicalResidualTZ.physicalToChartTZ h n (index n)) x) = (PhysicalResidualTZ.physicalToChartTZ h n (ChartScales.nativeIndex h n)) x

noncomputable def NavierStokes.CommonBaseContext.pull {E : Type u_1} (gap : ℕ → ℕ) (f : ℕ → Point → E) (n : ℕ) (x : Point) : E

Pull, given by f n (coverLift (gap n) x).

Equations

• NavierStokes.CommonBaseContext.pull gap f n x = f n ((NavierStokes.CommonBaseContext.coverLift (gap n)) x)

theorem NavierStokes.CommonBaseContext.pull_fderiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (gap : ℕ → ℕ) (f : ℕ → Point → E) (n : ℕ) (x v : Point) : (fderiv ℝ (pull gap f n) x) v = (fderiv ℝ (f n) ((coverLift (gap n)) x)) ((coverLift (gap n)) v)

theorem NavierStokes.CommonBaseContext.pull_dr (h a b : ℝ) (hab : a < b) (index gap : ℕ → ℕ) (f : ℕ → Point → ℝ) : (operators h index a b hab).dr (pull gap f) = pull gap ((operators h (fun (n : ℕ) => index n + gap n) a b hab).dr f)

theorem NavierStokes.CommonBaseContext.pull_dz (h a b : ℝ) (hab : a < b) (index gap : ℕ → ℕ) (f : ℕ → Point → ℝ) : (operators h index a b hab).dz (pull gap f) = pull gap ((operators h (fun (n : ℕ) => index n + gap n) a b hab).dz f)

theorem NavierStokes.CommonBaseContext.pull_slowTime (h a b : ℝ) (hab : a < b) (index gap : ℕ → ℕ) (f : ℕ → Point → ℝ) : (operators h index a b hab).slowTime (pull gap f) = pull gap ((operators h (fun (n : ℕ) => index n + gap n) a b hab).slowTime f)

theorem NavierStokes.CommonBaseContext.pull_fastTime (h a b : ℝ) (hab : a < b) (index gap : ℕ → ℕ) (f : ℕ → Point → ℝ) : (operators h index a b hab).fastTime (pull gap f) = pull gap ((operators h (fun (n : ℕ) => index n + gap n) a b hab).fastTime f)

theorem NavierStokes.CommonBaseContext.pull_time (h a b : ℝ) (hab : a < b) (index gap : ℕ → ℕ) (f : ℕ → Point → ℝ) : (operators h index a b hab).time (pull gap f) = pull gap ((operators h (fun (n : ℕ) => index n + gap n) a b hab).time f)

theorem NavierStokes.CommonBaseContext.pull_native_derivatives (h a b : ℝ) (hab : a < b) {index : ℕ → ℕ} (hi : ∀ (n : ℕ), index n ≤ ChartScales.nativeIndex h n) (f : ℕ → Point → ℝ) : have gap := fun (n : ℕ) => ChartScales.nativeIndex h n - index n; (operators h index a b hab).dr (pull gap f) = pull gap ((BaseContextAssembly.operators h a b hab).dr f) ∧ (operators h index a b hab).dz (pull gap f) = pull gap ((BaseContextAssembly.operators h a b hab).dz f) ∧ (operators h index a b hab).slowTime (pull gap f) = pull gap ((BaseContextAssembly.operators h a b hab).slowTime f) ∧ (operators h index a b hab).fastTime (pull gap f) = pull gap ((BaseContextAssembly.operators h a b hab).fastTime f) ∧ (operators h index a b hab).time (pull gap f) = pull gap ((BaseContextAssembly.operators h a b hab).time f)

theorem NavierStokes.CommonBaseContext.coverLift_radialField (h a b : ℝ) (hab : a < b) (index gap : ℕ → ℕ) (n : ℕ) (x : Point) : (coverLift (gap n)) ((operators h index a b hab).eR + ((operators h index a b hab).radialFrequency n * (operators h index a b hab).radialProfile x) • (operators h index a b hab).vR) = (operators h (fun (m : ℕ) => index m + gap m) a b hab).eR + ((operators h (fun (m : ℕ) => index m + gap m) a b hab).radialFrequency n * (operators h (fun (m : ℕ) => index m + gap m) a b hab).radialProfile ((coverLift (gap n)) x)) • (operators h (fun (m : ℕ) => index m + gap m) a b hab).vR

theorem NavierStokes.CommonBaseContext.coverLift_axialField (h a b : ℝ) (hab : a < b) (index gap : ℕ → ℕ) (n : ℕ) : (coverLift (gap n)) ((operators h index a b hab).epsilon n • (operators h index a b hab).eZ) = (operators h (fun (m : ℕ) => index m + gap m) a b hab).epsilon n • (operators h (fun (m : ℕ) => index m + gap m) a b hab).eZ

theorem NavierStokes.CommonBaseContext.coverLift_timeField (h a b : ℝ) (hab : a < b) (index gap : ℕ → ℕ) (n : ℕ) : (coverLift (gap n)) ((operators h index a b hab).fastCoefficient n • (operators h index a b hab).vT - (operators h index a b hab).epsilon n • (operators h index a b hab).eT) = (operators h (fun (m : ℕ) => index m + gap m) a b hab).fastCoefficient n • (operators h (fun (m : ℕ) => index m + gap m) a b hab).vT - (operators h (fun (m : ℕ) => index m + gap m) a b hab).epsilon n • (operators h (fun (m : ℕ) => index m + gap m) a b hab).eT

theorem NavierStokes.CommonBaseContext.pull_eq_coverPull (k : ℕ) (f : Point → ℝ) : (fun (x : Point) => f ((coverLift k) x)) = MeanChartCompatibility.coverPull 1 (ContinuousLinearMap.id ℝ Plane) k 1 f

theorem NavierStokes.CommonBaseContext.pull_periodic (k : ℕ) {f : Point → ℝ} (hf : PressureStream.TorusPeriodicLift f) : PressureStream.TorusPeriodicLift fun (x : PressureStream.Lift BaseContextAssembly.Plane) => f ((coverLift k) x)

theorem NavierStokes.CommonBaseContext.pull_periodicOn (k : ℕ) {U : Set Plane} {f : Point → ℝ} (hf : PhysicalMeanDomain.PeriodicOn U f) : PhysicalMeanDomain.PeriodicOn U fun (x : PressureStream.Lift Plane) => f ((coverLift k) x)

theorem NavierStokes.CommonBaseContext.coverLift_norm_le {k K : ℕ} (hk : k ≤ K) : ‖↑(coverLift k)‖ ≤ 1 + CommonCoverSolve.coveringBound K

theorem NavierStokes.CommonBaseContext.coverLift_mem {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) (k : ℕ) (x : Point) : (coverLift k) x ∈ (BaseContextAssembly.nativeStrip W U).domain ↔ x ∈ (BaseContextAssembly.nativeStrip W U).domain

theorem NavierStokes.CommonBaseContext.coverLift_delta {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) (k : ℕ) (x : Point) : (BaseContextAssembly.nativeStrip W U).delta ((coverLift k) x) = (BaseContextAssembly.nativeStrip W U).delta x

theorem NavierStokes.CommonBaseContext.coverLift_zeta {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) (k : ℕ) (x : Point) : (BaseContextAssembly.nativeStrip W U).zeta ((coverLift k) x) = (BaseContextAssembly.nativeStrip W U).zeta x

theorem NavierStokes.CommonBaseContext.coverLift_growth {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) (k n : ℕ) (x : Point) : (BaseContextAssembly.nativeStrip W U).growth n ((coverLift k) x) = (BaseContextAssembly.nativeStrip W U).growth n x

theorem NavierStokes.CommonBaseContext.class_pull {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {gap : ℕ → ℕ} {K : ℕ} (hgap : ∀ (n : ℕ), gap n ≤ K) {w : ℕ → Point → ℝ} {alpha : ℝ} {f : ℕ → Point → E} (hf : WeightedClasses.MemClass (BaseContextAssembly.nativeStrip W U) w alpha f) (hw : ∀ (n : ℕ), ∀ x ∈ (BaseContextAssembly.nativeStrip W U).domain, w n ((coverLift (gap n)) x) = w n x) : WeightedClasses.MemClass (BaseContextAssembly.nativeStrip W U) w alpha (pull gap f)

True covering norms produce one finite-jet constant before the band is chosen. No isometry property is assumed of the cover.

theorem NavierStokes.CommonBaseContext.unweighted_pull {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {gap : ℕ → ℕ} {K : ℕ} (hgap : ∀ (n : ℕ), gap n ≤ K) {alpha : ℝ} {f : ℕ → Point → E} (hf : WeightedClasses.UnweightedClass (BaseContextAssembly.nativeStrip W U) alpha f) : WeightedClasses.UnweightedClass (BaseContextAssembly.nativeStrip W U) alpha (pull gap f)

theorem NavierStokes.CommonBaseContext.mean_pull {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {gap : ℕ → ℕ} {K : ℕ} (hgap : ∀ (n : ℕ), gap n ≤ K) {alpha : ℝ} {f : ℕ → Point → E} (hf : WeightedClasses.MeanClass (BaseContextAssembly.nativeStrip W U) alpha f) : WeightedClasses.MeanClass (BaseContextAssembly.nativeStrip W U) alpha (pull gap f)

theorem NavierStokes.CommonBaseContext.temporalAtIndex_class {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) {index : ℕ → ℕ} {K : ℕ} (hi : IndexBounds F.data.h index K) {alpha : ℝ} {f : ℕ → Point → ℝ} (hf : WeightedClasses.MeanClass (BaseContextAssembly.nativeStrip W U) alpha fun (n : ℕ) => TemporalMeanUpdate.desiredIncrement F.data.h n (f n)) : WeightedClasses.MeanClass (BaseContextAssembly.nativeStrip W U) alpha fun (n : ℕ) => MeanChartCompatibility.temporalAtIndex F.data.h n (index n) (f n)

noncomputable def NavierStokes.CommonBaseContext.context {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (index : ℕ → ℕ) : CorrectionState.Context Point

Same actual base and stress; only the graph's integer index changes.

Equations

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

@[simp]

theorem NavierStokes.CommonBaseContext.context_base {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (index : ℕ → ℕ) : (context H v upper B index).base = (BaseContextAssembly.nativeContext H v upper B).base

@[simp]

theorem NavierStokes.CommonBaseContext.context_virtualTheta {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (index : ℕ → ℕ) : (context H v upper B index).virtualTheta = (BaseContextAssembly.nativeContext H v upper B).virtualTheta

@[simp]

theorem NavierStokes.CommonBaseContext.context_virtualAxial {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (index : ℕ → ℕ) : (context H v upper B index).virtualAxial = (BaseContextAssembly.nativeContext H v upper B).virtualAxial

theorem NavierStokes.CommonBaseContext.context_native {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : context H v upper B (ChartScales.nativeIndex F.data.h) = BaseContextAssembly.nativeContext H v upper B

theorem NavierStokes.CommonBaseContext.context_operator_bounds {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) {index : ℕ → ℕ} (hi : ∀ (n : ℕ), index n ≤ ChartScales.nativeIndex F.data.h n) : MeanIncrementBounds.OperatorBounds (BaseContextAssembly.nativeStrip W U) (context H v upper B index).operators ChartScales.kappa

theorem NavierStokes.CommonBaseContext.context_base_bounds {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) (index : ℕ → ℕ) : MeanIncrementBounds.BaseBounds (BaseContextAssembly.nativeStrip W U) (context H v upper B index).base

theorem NavierStokes.CommonBaseContext.context_base_smooth {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) (index : ℕ → ℕ) : MeanIncrementBounds.SmoothTriple (LocalRankDefect.positiveDomain U.carrier) (context H v upper B index).base

theorem NavierStokes.CommonBaseContext.context_operators_local {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (U : Set Plane) (index : ℕ → ℕ) : LocalRankDefect.LocalOperators U (context H v upper B index).operators

theorem NavierStokes.CommonBaseContext.context_isSlow {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (U : Set Plane) (index : ℕ → ℕ) : LocalRankDefect.IsSlowOn U (context H v upper B index).base.radial ∧ LocalRankDefect.IsSlowOn U (context H v upper B index).base.angular ∧ LocalRankDefect.IsSlowOn U (context H v upper B index).base.axial

theorem NavierStokes.CommonBaseContext.context_matches_physical {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (index : ℕ → ℕ) (n : ℕ) : PhysicalResidualTZ.MatchesAtTZ (context H v upper B index).operators (PhysicalResidualBridge.commonGraph (ChartScales.Q n) F.data.h (index n)) n

theorem NavierStokes.CommonBaseContext.context_radial_physical {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (index : ℕ → ℕ) (n : ℕ) (x : Point) : (context H v upper B index).base.radial n x = ChartScales.Q n ^ CoordinateAlgebra.A F.data.h * (FinalSlowBase.velocity H v upper B (BaseContextAssembly.physicalPoint F.data.h n x)).ofLp 0

theorem NavierStokes.CommonBaseContext.context_angular_physical {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (index : ℕ → ℕ) (n : ℕ) {x : Point} (hT : 0 < x.2.1.1) (hR : 0 < x.1) : (context H v upper B index).base.angular n x = ChartScales.Q n ^ CoordinateAlgebra.A F.data.h * (FinalSlowBase.velocity H v upper B (BaseContextAssembly.physicalPoint F.data.h n x)).ofLp 1

theorem NavierStokes.CommonBaseContext.context_axial_physical {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (index : ℕ → ℕ) (n : ℕ) {x : Point} (hT : 0 < x.2.1.1) : (context H v upper B index).base.axial n x = ChartScales.Q n ^ CoordinateAlgebra.A F.data.h * (FinalSlowBase.velocity H v upper B (BaseContextAssembly.physicalPoint F.data.h n x)).ofLp 2

theorem NavierStokes.CommonBaseContext.context_stress_properties {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) (index : ℕ → ℕ) (n : ℕ) : ContDiffOn ℝ (↑⊤) (fun (x : Point) => ((context H v upper B index).virtualTheta n x, (context H v upper B index).virtualAxial n x)) (PhysicalMeanDomain.slowDomain U.carrier) ∧ PhysicalMeanDomain.PeriodicOn U.carrier ((context H v upper B index).virtualTheta n) ∧ PhysicalMeanDomain.PeriodicOn U.carrier ((context H v upper B index).virtualAxial n) ∧ LocalSignedRequest.MovingSupport (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W) (2 * F.data.h) U.carrier ((context H v upper B index).virtualTheta n) ∧ LocalSignedRequest.MovingSupport (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W) (2 * F.data.h) U.carrier ((context H v upper B index).virtualAxial n)

theorem NavierStokes.CommonBaseContext.context_base_cover {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (index : ℕ → ℕ) (k n : ℕ) (x : Point) : HarmonicResidual.contextBase (context H v upper B index) n ((coverLift k) x) = HarmonicResidual.contextBase (context H v upper B index) n x

theorem NavierStokes.CommonBaseContext.context_virtualTheta_cover {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (index : ℕ → ℕ) (k n : ℕ) (x : Point) : (context H v upper B index).virtualTheta n ((coverLift k) x) = (context H v upper B index).virtualTheta n x

theorem NavierStokes.CommonBaseContext.context_virtualAxial_cover {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (index : ℕ → ℕ) (k n : ℕ) (x : Point) : (context H v upper B index).virtualAxial n ((coverLift k) x) = (context H v upper B index).virtualAxial n x

theorem NavierStokes.CommonBaseContext.contextOn_add {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (index gap : ℕ → ℕ) (U : Set Point) (n : ℕ) : PhysicalResidualNaturality.ContextOn U (coverLift (gap n)) 1 1 (context H v upper B index) (context H v upper B fun (m : ℕ) => index m + gap m) n n

Context coherence is proved on every free auxiliary lift point.

theorem NavierStokes.CommonBaseContext.contextOn_native {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {index : ℕ → ℕ} (hi : ∀ (n : ℕ), index n ≤ ChartScales.nativeIndex F.data.h n) (U : Set Point) (n : ℕ) : PhysicalResidualNaturality.ContextOn U (coverLift (ChartScales.nativeIndex F.data.h n - index n)) 1 1 (context H v upper B index) (BaseContextAssembly.nativeContext H v upper B) n n

theorem NavierStokes.CommonBaseContext.context_stress_classes {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (hcone : LeadingStressWeights.FullTrueCone v) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) (index : ℕ → ℕ) : WeightedClasses.MeanClass (BaseContextAssembly.nativeStrip W U) 1 (context H v upper B index).virtualTheta ∧ WeightedClasses.MeanClass (BaseContextAssembly.nativeStrip W U) 1 (context H v upper B index).virtualAxial

theorem NavierStokes.CommonBaseContext.context_higher_stress_classes {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) (index : ℕ → ℕ) : (WeightedClasses.MeanClass (BaseContextAssembly.nativeStrip W U) 2 fun (n : ℕ) (x : BaseContextAssembly.Point) => (context H v upper B index).virtualTheta n x - (BaseContextAssembly.leadingVirtualStress H v n x).1) ∧ WeightedClasses.MeanClass (BaseContextAssembly.nativeStrip W U) 2 fun (n : ℕ) (x : BaseContextAssembly.Point) => (context H v upper B index).virtualAxial n x - (BaseContextAssembly.leadingVirtualStress H v n x).2

theorem NavierStokes.CommonBaseContext.context_primaryCoefficients_match {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) (index : ℕ → ℕ) {D : PhaseJetBounds.Domain ℕ Slow} (P : PrimaryPulseBounds.PhaseConstruction D) (hF : P.phase.F = BaseContextAssembly.frequencySlow H v upper B) (hG : P.phase.G = BaseContextAssembly.axialSlow H v upper B) (chi : ℕ → Point × ℝ → PhaseCalculus.Slot) (hchi : ∀ (n : ℕ) (x : Point × ℝ), (chi n x).1 = BaseContextAssembly.slowCoordinates x.1) (amplitude : ℕ → Point × ℝ → HarmonicCalculus.ComplexVector) (pressure : ℕ → Point × ℝ → ℂ) (frequency : ℕ → ℝ) : PrimaryResidualClass.Matches (BaseContextAssembly.nativeStrip W U) (context H v upper B index) (PrimaryMaterialDefect.coefficients P (BaseContextAssembly.radialSlow H v upper B) chi amplitude pressure frequency)