Actual primary covariance and the flat target

The two columns use the two signs of the same representative and the actual Volterra primary. Target smallness at the attachment points is retained as a scalar factor throughout the finite matrix solve.

Primary phase geometry for the constructed slow base

The representatives are chosen in the actual positive-time mask support. The phase carrier is an open two-mesh cell; the larger three-mesh cell is used for the local base estimates. Compact constants use the genuine stable inverse branch, including its regular zero-time boundary.

@[reducible, inline]

abbrev NavierStokes.PrimaryGeometryAssembly.Slow : Type

Slow: an abbreviation for PhaseCalculus.Slow.

Equations

• NavierStokes.PrimaryGeometryAssembly.Slow = NavierStokes.PhaseCalculus.Slow

@[reducible, inline]

abbrev NavierStokes.PrimaryGeometryAssembly.Plane : Type

Plane: an abbreviation for MovingFrameODE.Plane /-! ## The actual positive support cells -/.

Equations

• NavierStokes.PrimaryGeometryAssembly.Plane = NavierStokes.MovingFrameODE.Plane

The actual positive support cells

noncomputable def NavierStokes.PrimaryGeometryAssembly.openCell (n : ℕ) (k : SlotColoring.Grid) : Set Slow

Two meshes leave an open neighborhood of the closed one-mesh mask support. They also give the precise 3/S³ representative distance used by the phase comparison theorem.

Equations

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

theorem NavierStokes.PrimaryGeometryAssembly.openCell_open (n : ℕ) (k : SlotColoring.Grid) : IsOpen (openCell n k)

theorem NavierStokes.PrimaryGeometryAssembly.openCell_convex (n : ℕ) (k : SlotColoring.Grid) : Convex ℝ (openCell n k)

theorem NavierStokes.PrimaryGeometryAssembly.openCell_subset_box (n : ℕ) (k : SlotColoring.Grid) : openCell n k ⊆ PrimaryRepresentatives.gridBox n k 2

theorem NavierStokes.PrimaryGeometryAssembly.openCell_subset_larger {n : ℕ} (hn : 1 ≤ n) (k : SlotColoring.Grid) : openCell n k ⊆ PositiveRepresentatives.positiveCell n k

theorem NavierStokes.PrimaryGeometryAssembly.support_subset_openCell {n : ℕ} (hn : 1 ≤ n) (k : SlotColoring.Grid) : tsupport (PrimaryRepresentatives.nativeMask n k) ∩ PositiveRepresentatives.positiveTime ⊆ openCell n k

theorem NavierStokes.PrimaryGeometryAssembly.representative_mem_openCell (K : Set Slow) (L : PositiveRepresentatives.ActiveLabel K) : PositiveRepresentatives.representative K L ∈ openCell (↑L).1 (↑L).2

theorem NavierStokes.PrimaryGeometryAssembly.openCell_representative_distance (K : Set Slow) (L : PositiveRepresentatives.ActiveLabel K) {p : Slow} (hp : p ∈ openCell (↑L).1 (↑L).2) : ‖p - PositiveRepresentatives.representative K L‖ ≤ 3 / ChartScales.S (↑L).1 ^ 3

noncomputable def NavierStokes.PrimaryGeometryAssembly.cellDomain (h lo hi : ℝ) (N : ℕ) : PhaseJetBounds.Domain (BaseChartJets.CellIndex h lo hi N) Slow

Cell domain, bundling scale, carrier, isOpen, one_le_scale.

Equations

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

theorem NavierStokes.PrimaryGeometryAssembly.cellDomain_subset_larger {h lo hi : ℝ} {N : ℕ} (L : BaseChartJets.CellIndex h lo hi N) : (cellDomain h lo hi N).carrier L ⊆ (BaseChartJets.positiveCellDomain h lo hi N).carrier L

theorem NavierStokes.PrimaryGeometryAssembly.cellDomain_support {h lo hi : ℝ} {N : ℕ} (L : BaseChartJets.CellIndex h lo hi N) : tsupport (PrimaryRepresentatives.nativeMask (↑↑L).1 (↑↑L).2) ∩ PositiveRepresentatives.positiveTime ⊆ (cellDomain h lo hi N).carrier L

theorem NavierStokes.PrimaryGeometryAssembly.cellDomain_representative {h lo hi : ℝ} {N : ℕ} (L : BaseChartJets.CellIndex h lo hi N) : PositiveRepresentatives.representative (PrimaryRepresentatives.referenceCompact h lo hi) ↑L ∈ (cellDomain h lo hi N).carrier L

noncomputable def NavierStokes.PrimaryGeometryAssembly.earlierIndex {h lo hi : ℝ} {N M : ℕ} (hNM : N ≤ M) (L : BaseChartJets.CellIndex h lo hi M) : BaseChartJets.CellIndex h lo hi N

Restrict labels after the constants have been chosen. The actual label and its chosen positive representative are unchanged.

Equations

• NavierStokes.PrimaryGeometryAssembly.earlierIndex hNM L = ⟨↑L, ⋯⟩

@[simp]

theorem NavierStokes.PrimaryGeometryAssembly.earlierIndex_band {h lo hi : ℝ} {N M : ℕ} (hNM : N ≤ M) (L : BaseChartJets.CellIndex h lo hi M) : BaseChartJets.cellBand (earlierIndex hNM L) = BaseChartJets.cellBand L

theorem NavierStokes.PrimaryGeometryAssembly.polynomial_restrict_reindex {ι : Type u_1} {κ : Type u_2} {E : Type u_3} {V : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {D : PhaseJetBounds.Domain ι E} {D' : PhaseJetBounds.Domain κ E} {f : ι → E → V} (hf : PhaseJetBounds.PolynomialJets D f) (e : κ → ι) (hscale : ∀ (i : κ), D'.scale i = D.scale (e i)) (hinside : ∀ (i : κ), D'.carrier i ⊆ D.carrier (e i)) : PhaseJetBounds.PolynomialJets D' fun (i : κ) => f (e i)

The fixed profile, schedule, and joint label family

noncomputable def NavierStokes.PrimaryGeometryAssembly.referenceSet {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : Set Slow

Reference set, given by PrimaryRepresentatives.referenceCompact F.data.h (NominalConeAssembly.activeLeft W) (NominalConeAssembly.activeRight W).

Equations

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

@[reducible, inline]

abbrev NavierStokes.PrimaryGeometryAssembly.Index {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (N : ℕ) : Type

Index: an abbreviation for BaseChartJets.CellIndex F.data.h (NominalConeAssembly.activeLeft W) (NominalConeAssembly.activeRight W) N.

Equations

• NavierStokes.PrimaryGeometryAssembly.Index W N = NavierStokes.BaseChartJets.CellIndex F.data.h (NavierStokes.NominalConeAssembly.activeLeft W) (NavierStokes.NominalConeAssembly.activeRight W) N

instance NavierStokes.PrimaryGeometryAssembly.indexCountable {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (N : ℕ) : Countable (Index W N)

noncomputable def NavierStokes.PrimaryGeometryAssembly.label {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {N : ℕ} (L : Index W N) : PartitionedCovariance.UnsignedLabel

Label, given by L.val.val.

Equations

• NavierStokes.PrimaryGeometryAssembly.label W L = ↑↑L

theorem NavierStokes.PrimaryGeometryAssembly.label_injective {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {N : ℕ} : Function.Injective (label W)

noncomputable def NavierStokes.PrimaryGeometryAssembly.domain {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (N : ℕ) : PhaseJetBounds.Domain (Index W N) Slow

Domain, given by cellDomain F.data.h (NominalConeAssembly.activeLeft W) (NominalConeAssembly.activeRight W) N.

Equations

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

noncomputable def NavierStokes.PrimaryGeometryAssembly.representative {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {N : ℕ} (L : Index W N) : Slow

Representative, given by PositiveRepresentatives.representative (referenceSet W) L.val.

Equations

• NavierStokes.PrimaryGeometryAssembly.representative W L = NavierStokes.PositiveRepresentatives.representative (NavierStokes.PrimaryGeometryAssembly.referenceSet W) ↑L

noncomputable def NavierStokes.PrimaryGeometryAssembly.baseDomain {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {N : ℕ} (L : Index W N) : Set Slow

Base domain, given by PositiveRepresentatives.positiveCell L.val.val.1 L.val.val.2.

Equations

• NavierStokes.PrimaryGeometryAssembly.baseDomain W L = NavierStokes.PositiveRepresentatives.positiveCell (↑↑L).1 (↑↑L).2

theorem NavierStokes.PrimaryGeometryAssembly.representative_positive {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {N : ℕ} (L : Index W N) : 0 < (representative W L).2.2

theorem NavierStokes.PrimaryGeometryAssembly.representative_in_reference {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {N : ℕ} (L : Index W N) : representative W L ∈ referenceSet W

theorem NavierStokes.PrimaryGeometryAssembly.representative_in_carrier {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {N : ℕ} (L : Index W N) : representative W L ∈ (domain W N).carrier L

theorem NavierStokes.PrimaryGeometryAssembly.representative_in_baseDomain {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {N : ℕ} (L : Index W N) : representative W L ∈ baseDomain W L

theorem NavierStokes.PrimaryGeometryAssembly.carrier_in_baseDomain {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {N : ℕ} (L : Index W N) : (domain W N).carrier L ⊆ baseDomain W L

theorem NavierStokes.PrimaryGeometryAssembly.representative_distance {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {N : ℕ} (L : Index W N) {p : Slow} (hp : p ∈ (domain W N).carrier L) : ‖p - representative W L‖ ≤ 3 / (domain W N).scale L ^ 3

theorem NavierStokes.PrimaryGeometryAssembly.native_support_in_carrier {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {N : ℕ} (L : Index W N) : tsupport (PrimaryRepresentatives.nativeMask (↑↑L).1 (↑↑L).2) ∩ PositiveRepresentatives.positiveTime ⊆ (domain W N).carrier L

theorem NavierStokes.PrimaryGeometryAssembly.native_jet_support_in_carrier {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {N : ℕ} (L : Index W N) (m : ℕ) : tsupport (iteratedFDeriv ℝ m (PrimaryRepresentatives.nativeMask (↑↑L).1 (↑↑L).2)) ∩ PositiveRepresentatives.positiveTime ⊆ (domain W N).carrier L

theorem NavierStokes.PrimaryGeometryAssembly.physicalMask_has_index {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {N : ℕ} (L : PartitionedCovariance.UnsignedLabel) (hL : 1 ≤ L.1) (hN : N ≤ L.1) {q : ℝ} {x : SlotColoring.Position} (hq : 0 < q) (hR : 0 ≤ x 0) (hT : 0 < x 2) (he : SimilarityCoordinates.forwardScalar (2 * F.data.h) (x 1) q = x 2) (hX : x 0 ^ 2 / (2 * q) ∈ Set.Icc (NominalConeAssembly.activeLeft W) (NominalConeAssembly.activeRight W)) (hm : PartitionedCovariance.mask (CoordinateAlgebra.D F.data.h) L q x ≠ 0) : ∃ (i : Index W N), label W i = L

Every genuinely nonzero physical mask has one of the joint positive labels used here. The implicit inverse is never evaluated at zero time.

noncomputable def NavierStokes.PrimaryGeometryAssembly.fromTimeAxial (R : ℝ) (tz : ℝ × ℝ) : Slow

Mean-flow charts use (T,Z), while the phase chart uses (R,(Z,T)). This explicit map prevents their equal product types hiding a swap.

Equations

• NavierStokes.PrimaryGeometryAssembly.fromTimeAxial R tz = (R, tz.2, tz.1)

@[simp]

theorem NavierStokes.PrimaryGeometryAssembly.fromTimeAxial_time (R : ℝ) (tz : ℝ × ℝ) : (fromTimeAxial R tz).2.2 = tz.1

@[simp]

theorem NavierStokes.PrimaryGeometryAssembly.fromTimeAxial_axial (R : ℝ) (tz : ℝ × ℝ) : (fromTimeAxial R tz).2.1 = tz.2

noncomputable def NavierStokes.PrimaryGeometryAssembly.frequency {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B n : ℕ) : Slow → ℝ

The chart field of the very same FinalSlowBase schedule.

Equations

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

noncomputable def NavierStokes.PrimaryGeometryAssembly.axial {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B n : ℕ) : Slow → ℝ

Axial, given by BaseChartJets.axial (FinalSlowBase.scales H v upper B) F.data.h (FinalSlowBase.coefficients H v) (ChartScales.Q n).

Equations

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

noncomputable def NavierStokes.PrimaryGeometryAssembly.leadingFrequency {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) : Slow → ℝ

Leading frequency, given by BaseChartJets.leadingFrequency F.data.h W.axis.normalization (FinalSlowBase.coefficients H v).

Equations

• NavierStokes.PrimaryGeometryAssembly.leadingFrequency H v = NavierStokes.BaseChartJets.leadingFrequency F.data.h W.axis.normalization (NavierStokes.FinalSlowBase.coefficients H v)

noncomputable def NavierStokes.PrimaryGeometryAssembly.leadingAxial {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) : Slow → ℝ

Leading axial, given by BaseChartJets.leadingAxial F.data.h (FinalSlowBase.coefficients H v).

Equations

• NavierStokes.PrimaryGeometryAssembly.leadingAxial H v = NavierStokes.BaseChartJets.leadingAxial F.data.h (NavierStokes.FinalSlowBase.coefficients H v)

noncomputable def NavierStokes.PrimaryGeometryAssembly.shear {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) : Slow → Plane

Shear, given by PhaseEstimates.shearVector (leadingFrequency H v) (leadingAxial H v).

Equations

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

structure NavierStokes.PrimaryGeometryAssembly.Prepared {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (r0 : ℝ) (N0 : ℕ) : Type

This record is an output of the concrete construction below. None of its analytic bounds are assumptions of the exported constructor.

• N : ℕ

  Truncation order of Prepared, of type ℕ.

• threshold : N0 ≤ self.N
• M : ℝ

  M of Prepared, of type ℝ.

• u : ℝ

  U of Prepared, of type ℝ.

• eta : ℝ

  Eta of Prepared, of type ℝ.

• target : Slow → Plane

  Target of Prepared, of type Slow → Plane.

• one_le_M : 1 ≤ self.M
• u_pos : 0 < self.u
• eta_pos : 0 < self.eta
• u_le : self.u ≤ self.M
• length_bound : 1 / (2 * r0) ≤ self.M
• slot_bound : 4 * r0 * ChartScales.Tg ≤ self.M
• base (L : Index W self.N) : PhaseEstimates.LocalBaseBounds (frequency H v upper B (BaseChartJets.cellBand L)) (axial H v upper B (BaseChartJets.cellBand L)) (leadingFrequency H v) (leadingAxial H v) (baseDomain W L) self.M (ChartScales.epsilon F.data.h (BaseChartJets.cellBand L))
• frequency_jets : PhaseJetBounds.PolynomialJets (domain W self.N) fun (L : Index W self.N) => frequency H v upper B (BaseChartJets.cellBand L)
• axial_jets : PhaseJetBounds.PolynomialJets (domain W self.N) fun (L : Index W self.N) => axial H v upper B (BaseChartJets.cellBand L)
• radius_pos (L : Index W self.N) (p : Slow) : p ∈ (domain W self.N).carrier L → 0 < p.1
• radius (L : Index W self.N) (p : Slow) : p ∈ (domain W self.N).carrier L → 1 / self.M ≤ |p.1| ∧ |p.1| ≤ self.M
• parameters (L : Index W self.N) : PrimaryRepresentatives.ParameterBounds self.M (representative W L).1 (leadingFrequency H v (representative W L)) (shear H v (representative W L))
• cone (L : Index W self.N) : PrimaryRepresentatives.ReferenceCone (leadingFrequency H v (representative W L)) (shear H v (representative W L))
• target_continuous : ContinuousOn self.target (referenceSet W)
• target_unit (p : Slow) : p ∈ referenceSet W → ‖self.target p‖ = 1
• target_actual (p : Slow) : p ∈ referenceSet W → (PositiveRepresentatives.stableInner F.data.h p).1 ∈ Set.Ioo (NominalConeAssembly.activeLeft W) (NominalConeAssembly.activeRight W) → self.target p = PrimaryRepresentatives.normalDirection (ProfileSpectralCone.stressVector v.profiles F.data.h (PositiveRepresentatives.stableInner F.data.h p))
• target_margin (L : Index W self.N) (p : Slow) : p ∈ PositiveRepresentatives.positivePart (referenceSet W) → p ∈ (domain W self.N).carrier L → inner ℝ (self.target p) (PrimaryRepresentatives.normalDirection (shear H v (representative W L))) ≤ -self.eta ∧ |PrimaryRepresentatives.c0 (leadingFrequency H v (representative W L)) (shear H v (representative W L)) * inner ℝ (self.target p) (PrimaryRepresentatives.transverseDirection (shear H v (representative W L))) / inner ℝ (self.target p) (PrimaryRepresentatives.normalDirection (shear H v (representative W L)))| + self.eta ≤ PrimaryRepresentatives.slopeRatio self.u
• large (n : ℕ) : self.N ≤ n → BasePhaseGeometry.LargeBand F.data.h self.M self.u n

noncomputable def NavierStokes.PrimaryGeometryAssembly.phaseSign (c : Fin 2) : ℝ

Phase sign, with branches according to c = 0.

Equations

• NavierStokes.PrimaryGeometryAssembly.phaseSign c = if c = 0 then 1 else -1

theorem NavierStokes.PrimaryGeometryAssembly.phaseSign_abs (c : Fin 2) : |phaseSign c| = 1

noncomputable def NavierStokes.PrimaryGeometryAssembly.family {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : Prepared H v upper B r0 N0) (c : Fin 2) : BasePhaseGeometry.FamilyData (domain W a.N) F.data.h r0 a.u a.M

The actual positive representatives instantiate every entry of the phase data, including the unstable eigenpair and the nonzero rounding.

Equations

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

noncomputable def NavierStokes.PrimaryGeometryAssembly.construction {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : Prepared H v upper B r0 N0) (hr0 : 0 < r0) (c : Fin 2) : PrimaryPulseBounds.PhaseConstruction (domain W a.N)

Both signs have one joint domain and the same constants, which were fixed before its band threshold. All phase comparison outputs are proved by FamilyData.construction.

Equations

• NavierStokes.PrimaryGeometryAssembly.construction H v a hr0 c = (NavierStokes.PrimaryGeometryAssembly.family H v a c).construction ⋯ hr0 ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem NavierStokes.PrimaryGeometryAssembly.exists_majorant (M0 b u r0 lo hi : ℝ) : ∃ (M : ℝ), 1 ≤ M ∧ M0 ≤ M ∧ b ≤ M ∧ u ≤ M ∧ 1 / (2 * r0) ≤ M ∧ 4 * r0 * ChartScales.Tg ≤ M ∧ PositiveRepresentatives.cellBound hi ≤ M ∧ 2 / √lo ≤ M

Every fixed chart, radial, and slot constant is enlarged before any phase band is selected.

theorem NavierStokes.PrimaryGeometryAssembly.active_order {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} : NominalConeAssembly.activeLeft W < NominalConeAssembly.activeRight W

theorem NavierStokes.PrimaryGeometryAssembly.radius_lower_of_majorant {lo M : ℝ} (hlo : 0 < lo) (hM : 1 ≤ M) (hbound : 2 / √lo ≤ M) : 1 / M ≤ √lo / 2

theorem NavierStokes.PrimaryGeometryAssembly.exists_prepared {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (hcone : LeadingStressWeights.FullTrueCone v) (upper : ℝ) (B : ℕ) (r0 : ℝ) (hbox : 2 * NominalConeAssembly.activeRight W ≤ FinalSlowBase.boxRadius W upper) (N0 : ℕ) : Nonempty (Prepared H v upper B r0 N0)

The smooth summed base, its positive mask representatives, and the actual strict cone supply every datum used by the phase theorem. The last threshold is chosen only after u, the target margin, and M. The same threshold applies to every active label and to both signs.

noncomputable def NavierStokes.PrimaryGeometryAssembly.prepared {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (hcone : LeadingStressWeights.FullTrueCone v) (upper : ℝ) (B : ℕ) (r0 : ℝ) (hbox : 2 * NominalConeAssembly.activeRight W ≤ FinalSlowBase.boxRadius W upper) (N0 : ℕ) : Prepared H v upper B r0 N0

A selected, fully constructed datum. The caller supplies no local base bound, eigenpair estimate, or phase comparison.

Equations

• NavierStokes.PrimaryGeometryAssembly.prepared H v hcone upper B r0 hbox N0 = Classical.choice ⋯

noncomputable def NavierStokes.PrimaryGeometryAssembly.phases {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (hcone : LeadingStressWeights.FullTrueCone v) (upper : ℝ) (B : ℕ) (r0 : ℝ) (hr0 : 0 < r0) (hbox : 2 * NominalConeAssembly.activeRight W ≤ FinalSlowBase.boxRadius W upper) (N0 : ℕ) : Fin 2 → PrimaryPulseBounds.PhaseConstruction (domain W (prepared H v hcone upper B r0 hbox N0).N)

Phases, given by construction H v (prepared H v hcone upper B r0 hbox N0) hr0.

Equations

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

noncomputable def NavierStokes.PrimaryGeometryAssembly.canonicalPrepared {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (hcone : LeadingStressWeights.FullTrueCone v) (B : ℕ) (r0 : ℝ) (N0 : ℕ) : Prepared H v (2 * NominalConeAssembly.activeRight W) B r0 N0

A canonical box large enough for every enlarged chart of the active annulus. This uses exactly FinalSlowBase.scales H v (2*activeRight) B.

Equations

• NavierStokes.PrimaryGeometryAssembly.canonicalPrepared H v hcone B r0 N0 = NavierStokes.PrimaryGeometryAssembly.prepared H v hcone (2 * NavierStokes.NominalConeAssembly.activeRight W) B r0 ⋯ N0

noncomputable def NavierStokes.PrimaryGeometryAssembly.canonicalPhases {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (hcone : LeadingStressWeights.FullTrueCone v) (B : ℕ) (r0 : ℝ) (hr0 : 0 < r0) (N0 : ℕ) : Fin 2 → PrimaryPulseBounds.PhaseConstruction (domain W (canonicalPrepared H v hcone B r0 N0).N)

Canonical phases, given by construction H v (canonicalPrepared H v hcone B r0 N0) hr0.

Equations

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

theorem NavierStokes.PrimaryGeometryAssembly.prepared_threshold {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (hcone : LeadingStressWeights.FullTrueCone v) (upper : ℝ) (B : ℕ) (r0 : ℝ) (hbox : 2 * NominalConeAssembly.activeRight W ≤ FinalSlowBase.boxRadius W upper) (N0 : ℕ) : N0 ≤ (prepared H v hcone upper B r0 hbox N0).N

theorem NavierStokes.PrimaryGeometryAssembly.four_le_threshold {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : Prepared H v upper B r0 N0) : 4 ≤ a.N

theorem NavierStokes.PrimaryGeometryAssembly.construction_frequency {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : Prepared H v upper B r0 N0) (hr0 : 0 < r0) (c : Fin 2) (L : Index W a.N) : (construction H v a hr0 c).phase.F L = frequency H v upper B (BaseChartJets.cellBand L)

theorem NavierStokes.PrimaryGeometryAssembly.construction_axial {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : Prepared H v upper B r0 N0) (hr0 : 0 < r0) (c : Fin 2) (L : Index W a.N) : (construction H v a hr0 c).phase.G L = axial H v upper B (BaseChartJets.cellBand L)

theorem NavierStokes.PrimaryGeometryAssembly.construction_epsilon {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : Prepared H v upper B r0 N0) (hr0 : 0 < r0) (c : Fin 2) (L : Index W a.N) : (construction H v a hr0 c).phase.epsilon L = ChartScales.epsilon F.data.h (BaseChartJets.cellBand L)

theorem NavierStokes.PrimaryGeometryAssembly.construction_viscosity {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : Prepared H v upper B r0 N0) (hr0 : 0 < r0) (c : Fin 2) (L : Index W a.N) : (construction H v a hr0 c).viscosity L = ChartScales.epsilon F.data.h (BaseChartJets.cellBand L) * ↑(ChartScales.carrier F.data.h (BaseChartJets.cellBand L)) ^ 2

theorem NavierStokes.PrimaryGeometryAssembly.construction_length {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : Prepared H v upper B r0 N0) (hr0 : 0 < r0) (c : Fin 2) (L : Index W a.N) : (construction H v a hr0 c).L L = ChartScales.slotLength r0 F.data.h (BaseChartJets.cellBand L)

theorem NavierStokes.PrimaryGeometryAssembly.construction_slot {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : Prepared H v upper B r0 N0) (hr0 : 0 < r0) (c : Fin 2) (L : Index W a.N) : (construction H v a hr0 c).V L = Set.Ioo (-ChartScales.slotLength r0 F.data.h (BaseChartJets.cellBand L)) (2 * ChartScales.slotLength r0 F.data.h (BaseChartJets.cellBand L))

theorem NavierStokes.PrimaryGeometryAssembly.construction_lambda {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : Prepared H v upper B r0 N0) (hr0 : 0 < r0) (c : Fin 2) (L : Index W a.N) : (construction H v a hr0 c).lam L = PrimaryRepresentatives.lambda0 (leadingFrequency H v (representative W L)) (shear H v (representative W L))

theorem NavierStokes.PrimaryGeometryAssembly.construction_ratio {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : Prepared H v upper B r0 N0) (hr0 : 0 < r0) (c : Fin 2) (L : Index W a.N) : (construction H v a hr0 c).c0 L = PrimaryRepresentatives.c0 (leadingFrequency H v (representative W L)) (shear H v (representative W L))

theorem NavierStokes.PrimaryGeometryAssembly.construction_transverse {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : Prepared H v upper B r0 N0) (hr0 : 0 < r0) (c : Fin 2) (L : Index W a.N) : (construction H v a hr0 c).K L = PrimaryRepresentatives.transverseDirection (shear H v (representative W L))

theorem NavierStokes.PrimaryGeometryAssembly.construction_u {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : Prepared H v upper B r0 N0) (hr0 : 0 < r0) (c : Fin 2) (L : Index W a.N) : (construction H v a hr0 c).u L = a.u

noncomputable def NavierStokes.PrimaryGeometryAssembly.angularMode {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : Prepared H v upper B r0 N0) (c : Fin 2) (L : Index W a.N) : ℤ

The actual integer angular mode is retained; zero-floor rounding is not replaced by an unproved assertion that a real frequency is integral.

Equations

• NavierStokes.PrimaryGeometryAssembly.angularMode H v a c L = (NavierStokes.PrimaryGeometryAssembly.family H v a c).angularMode L

theorem NavierStokes.PrimaryGeometryAssembly.angularMode_ne_zero {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : Prepared H v upper B r0 N0) (c : Fin 2) (L : Index W a.N) : angularMode H v a c L ≠ 0

theorem NavierStokes.PrimaryGeometryAssembly.carrier_mul_phase_p {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : Prepared H v upper B r0 N0) (hr0 : 0 < r0) (c : Fin 2) (L : Index W a.N) : ↑(ChartScales.carrier F.data.h (BaseChartJets.cellBand L)) * (construction H v a hr0 c).phase.p L = ↑(angularMode H v a c L)

theorem NavierStokes.PrimaryGeometryAssembly.angular_rounding_error {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : Prepared H v upper B r0 N0) (hr0 : 0 < r0) (c : Fin 2) (L : Index W a.N) : |(construction H v a hr0 c).phase.p L - (family H v a c).target L| ≤ 1 / ↑(ChartScales.carrier F.data.h (BaseChartJets.cellBand L))

theorem NavierStokes.PrimaryGeometryAssembly.phase_signs {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : Prepared H v upper B r0 N0) (L : Index W a.N) : (family H v a 0).sigma L = 1 ∧ (family H v a 1).sigma L = -1

theorem NavierStokes.PrimaryGeometryAssembly.common_bounds {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : Prepared H v upper B r0 N0) (hr0 : 0 < r0) (c d : Fin 2) : (construction H v a hr0 c).r = (construction H v a hr0 d).r ∧ (construction H v a hr0 c).b = (construction H v a hr0 d).b ∧ (construction H v a hr0 c).M = (construction H v a hr0 d).M ∧ (construction H v a hr0 c).C = (construction H v a hr0 d).C ∧ (construction H v a hr0 c).E = (construction H v a hr0 d).E

theorem NavierStokes.PrimaryGeometryAssembly.carrier_time_positive {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : Prepared H v upper B r0 N0) {L : Index W a.N} {p : Slow} (hp : p ∈ (domain W a.N).carrier L) : 0 < p.2.2

theorem NavierStokes.PrimaryGeometryAssembly.target_eq_normalized_stress {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : Prepared H v upper B r0 N0) {p : Slow} (hp : p ∈ referenceSet W) (hT : 0 < p.2.2) (hX : (BaseChartJets.normalizedCoordinates F.data.h p).2.1 ∈ Set.Ioo (NominalConeAssembly.activeLeft W) (NominalConeAssembly.activeRight W)) : a.target p = PrimaryRepresentatives.normalDirection (ProfileSpectralCone.stressVector v.profiles F.data.h (BaseChartJets.normalizedCoordinates F.data.h p).2)

theorem NavierStokes.PrimaryGeometryAssembly.frequency_eq_physical {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {p : Slow} (hT : 0 < p.2.2) (hR : 0 < p.1) (n : ℕ) : frequency H v upper B n p = ChartScales.Q n ^ CoordinateAlgebra.A F.data.h * (FinalSlowBase.velocity H v upper B (BaseChartJets.bandPoint F.data.h (ChartScales.Q n) p)).ofLp 1 / p.1

theorem NavierStokes.PrimaryGeometryAssembly.axial_eq_physical {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {p : Slow} (hT : 0 < p.2.2) (n : ℕ) : axial H v upper B n p = ChartScales.Q n ^ CoordinateAlgebra.A F.data.h * (FinalSlowBase.velocity H v upper B (BaseChartJets.bandPoint F.data.h (ChartScales.Q n) p)).ofLp 2

A later common cutoff preserves the already selected geometry

noncomputable def NavierStokes.PrimaryGeometryAssembly.Prepared.restrict {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {H : NominalConeAssembly.Certificate W} {ld : ModulatedProfileAssembly.LoopData W} {v : ModulatedProfileAssembly.Witness ld} {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : Prepared H v upper B r0 N0) (N : ℕ) (hN : a.N ≤ N) : Prepared H v upper B r0 N0

Restriction changes only the set of admissible labels. It does not reselect a target direction, parameter constant, representative, or Fourier mode. A final consumer can therefore take the maximum of its covariance cutoff and this geometry cutoff.

Equations

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

@[simp]

theorem NavierStokes.PrimaryGeometryAssembly.Prepared.restrict_N {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {H : NominalConeAssembly.Certificate W} {ld : ModulatedProfileAssembly.LoopData W} {v : ModulatedProfileAssembly.Witness ld} {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : Prepared H v upper B r0 N0) (N : ℕ) (hN : a.N ≤ N) : (a.restrict N hN).N = N

@[simp]

theorem NavierStokes.PrimaryGeometryAssembly.Prepared.restrict_parameters {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {H : NominalConeAssembly.Certificate W} {ld : ModulatedProfileAssembly.LoopData W} {v : ModulatedProfileAssembly.Witness ld} {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : Prepared H v upper B r0 N0) (N : ℕ) (hN : a.N ≤ N) : (a.restrict N hN).M = a.M ∧ (a.restrict N hN).u = a.u ∧ (a.restrict N hN).eta = a.eta ∧ (a.restrict N hN).target = a.target

theorem NavierStokes.PrimaryGeometryAssembly.Prepared.restrict_frame {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {H : NominalConeAssembly.Certificate W} {ld : ModulatedProfileAssembly.LoopData W} {v : ModulatedProfileAssembly.Witness ld} {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : Prepared H v upper B r0 N0) (hr0 : 0 < r0) (N : ℕ) (hN : a.N ≤ N) (c : Fin 2) (L : Index W N) : (construction H v (a.restrict N hN) hr0 c).frame L = (construction H v a hr0 c).frame (earlierIndex hN L)

theorem NavierStokes.PrimaryGeometryAssembly.Prepared.restrict_angularMode {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {H : NominalConeAssembly.Certificate W} {ld : ModulatedProfileAssembly.LoopData W} {v : ModulatedProfileAssembly.Witness ld} {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : Prepared H v upper B r0 N0) (N : ℕ) (hN : a.N ≤ N) (c : Fin 2) (L : Index W N) : angularMode H v (a.restrict N hN) c L = angularMode H v a c (earlierIndex hN L)

theorem NavierStokes.PrimaryGeometryAssembly.Prepared.restrict_phase_p {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {H : NominalConeAssembly.Certificate W} {ld : ModulatedProfileAssembly.LoopData W} {v : ModulatedProfileAssembly.Witness ld} {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : Prepared H v upper B r0 N0) (hr0 : 0 < r0) (N : ℕ) (hN : a.N ≤ N) (c : Fin 2) (L : Index W N) : (construction H v (a.restrict N hN) hr0 c).phase.p L = (construction H v a hr0 c).phase.p (earlierIndex hN L)

@[reducible, inline]

abbrev NavierStokes.PrimaryTargetBounds.Plane : Type

Plane: an abbreviation for MovingFrameODE.Plane.

Equations

• NavierStokes.PrimaryTargetBounds.Plane = NavierStokes.MovingFrameODE.Plane

@[reducible, inline]

abbrev NavierStokes.PrimaryTargetBounds.Slow : Type

Slow: an abbreviation for PhaseCalculus.Slow.

Equations

• NavierStokes.PrimaryTargetBounds.Slow = NavierStokes.PhaseCalculus.Slow

@[reducible, inline]

abbrev NavierStokes.PrimaryTargetBounds.Mat2 : Type

Mat2: an abbreviation for SmoothCovariance.Mat2.

Equations

• NavierStokes.PrimaryTargetBounds.Mat2 = NavierStokes.SmoothCovariance.Mat2

@[reducible, inline]

abbrev NavierStokes.PrimaryTargetBounds.Vec2 : Type

Vec2: an abbreviation for SmoothCovariance.Vec2.

Equations

• NavierStokes.PrimaryTargetBounds.Vec2 = NavierStokes.SmoothCovariance.Vec2

noncomputable def NavierStokes.PrimaryTargetBounds.phaseSign (j : Fin 2) : ℝ

Phase sign, with branches according to j = 0.

Equations

• NavierStokes.PrimaryTargetBounds.phaseSign j = if j = 0 then 1 else -1

theorem NavierStokes.PrimaryTargetBounds.phaseSign_abs (j : Fin 2) : |phaseSign j| = 1

noncomputable def NavierStokes.PrimaryTargetBounds.basisMatrix (K : Plane) : Mat2

The normal and transverse columns in the fixed physical tangent plane.

Equations

• NavierStokes.PrimaryTargetBounds.basisMatrix K i j = if j = 0 then (NavierStokes.MovingFrameODE.quarterTurn K).ofLp i else K.ofLp i

noncomputable def NavierStokes.PrimaryTargetBounds.modelMatrix (c u : ℝ) (K : Plane) : Mat2

Model matrix, given by basisMatrix K * PulseCovariance.signedModel c u.

Equations

• NavierStokes.PrimaryTargetBounds.modelMatrix c u K = NavierStokes.PrimaryTargetBounds.basisMatrix K * NavierStokes.PulseCovariance.signedModel c u

noncomputable def NavierStokes.PrimaryTargetBounds.modelNormal (K T : Plane) : ℝ

Model normal, given by -⟪T, MovingFrameODE.quarterTurn K⟫_ℝ.

Equations

• NavierStokes.PrimaryTargetBounds.modelNormal K T = -inner ℝ T (NavierStokes.MovingFrameODE.quarterTurn K)

noncomputable def NavierStokes.PrimaryTargetBounds.modelTransverse (K T : Plane) : ℝ

Model transverse, given by ⟪T, K⟫_ℝ.

Equations

• NavierStokes.PrimaryTargetBounds.modelTransverse K T = inner ℝ T K

theorem NavierStokes.PrimaryTargetBounds.basisMatrix_det (K : Plane) (hK : ‖K‖ = 1) : Matrix.det (basisMatrix K) = -1

theorem NavierStokes.PrimaryTargetBounds.modelMatrix_column (c u : ℝ) (K : Plane) (i j : Fin 2) : modelMatrix c u K i j = c * √(1 + u ^ 2) * (MovingFrameODE.quarterTurn K).ofLp i - phaseSign j * u * K.ofLp i

theorem NavierStokes.PrimaryTargetBounds.basisMatrix_target (K T : Plane) (hK : ‖K‖ = 1) : Matrix.mulVec (basisMatrix K) (Covariance.target (modelNormal K T) (modelTransverse K T)) = fun (i : Fin 2) => T.ofLp i

theorem NavierStokes.PrimaryTargetBounds.weights_unique {H : Mat2} {T z : Vec2} (hd : Matrix.det H ≠ 0) (he : Matrix.mulVec H z = T) : SmoothCovariance.weights H T = z

theorem NavierStokes.PrimaryTargetBounds.strictCone_mul_left {B H : Mat2} {T : Vec2} (hB : Matrix.det B ≠ 0) (hH : SmoothCovariance.StrictCone H T) : SmoothCovariance.StrictCone (B * H) (Matrix.mulVec B T)

theorem NavierStokes.PrimaryTargetBounds.modelMatrix_strictCone {c u eta : ℝ} {K T : Plane} (hc : c < 0) (hu : 0 < u) (heta : 0 < eta) (hK : ‖K‖ = 1) (hm : eta ≤ modelNormal K T) (hr : |c * modelTransverse K T| ≤ (PrimaryRepresentatives.slopeRatio u - eta) * modelNormal K T) : SmoothCovariance.StrictCone (modelMatrix c u K) fun (i : Fin 2) => T.ofLp i

@[reducible, inline]

abbrev NavierStokes.PrimaryTargetBounds.ModelPoint : Type

Model point: an abbreviation for ℝ × (Plane × Plane).

Equations

• NavierStokes.PrimaryTargetBounds.ModelPoint = (ℝ × NavierStokes.PrimaryTargetBounds.Plane × NavierStokes.PrimaryTargetBounds.Plane)

noncomputable def NavierStokes.PrimaryTargetBounds.modelSet (M u eta : ℝ) : Set ModelPoint

Model set as an element of Set ModelPoint.

Equations

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

theorem NavierStokes.PrimaryTargetBounds.modelNormal_continuous : Continuous fun (p : ModelPoint) => modelNormal p.2.1 p.2.2

theorem NavierStokes.PrimaryTargetBounds.modelTransverse_continuous : Continuous fun (p : ModelPoint) => modelTransverse p.2.1 p.2.2

theorem NavierStokes.PrimaryTargetBounds.modelSet_compact (M u eta : ℝ) : IsCompact (modelSet M u eta)

theorem NavierStokes.PrimaryTargetBounds.modelMatrix_continuous (u : ℝ) (i j : Fin 2) : Continuous fun (p : ModelPoint) => modelMatrix p.1 u p.2.1 i j

theorem NavierStokes.PrimaryTargetBounds.compact_model_data {M u eta : ℝ} (hM : 1 ≤ M) (hu : 0 < u) (heta : 0 < eta) : (∀ (i j : Fin 2), ContinuousOn (fun (p : ModelPoint) => modelMatrix p.1 u p.2.1 i j) (modelSet M u eta)) ∧ (∀ (i : Fin 2), ContinuousOn (fun (p : ModelPoint) => p.2.2.ofLp i) (modelSet M u eta)) ∧ ∀ p ∈ modelSet M u eta, SmoothCovariance.StrictCone (modelMatrix p.1 u p.2.1) fun (i : Fin 2) => p.2.2.ofLp i

noncomputable def NavierStokes.PrimaryTargetBounds.modelVector (c s : ℝ) (K : Plane) : Plane

Model vector, given by (-s) • K + (c * Real.sqrt (1 + s ^ 2)) • MovingFrameODE.quarterTurn K.

Equations

• NavierStokes.PrimaryTargetBounds.modelVector c s K = -s • K + (c * √(1 + s ^ 2)) • NavierStokes.MovingFrameODE.quarterTurn K

theorem NavierStokes.PrimaryTargetBounds.modelVector_column (c u : ℝ) (K : Plane) (j i : Fin 2) : (modelVector c (phaseSign j * u) K).ofLp i = modelMatrix c u K i j

theorem NavierStokes.PrimaryTargetBounds.modelVector_lipschitz (c s t : ℝ) (K : Plane) (hK : ‖K‖ = 1) : ‖modelVector c s K - modelVector c t K‖ ≤ (|c| + 1) * |s - t|

theorem NavierStokes.PrimaryTargetBounds.frame_combination_error (k K : Plane) (hk : ‖k‖ = 1) (a b a0 b0 : ℝ) : ‖a • k + b • MovingFrameODE.quarterTurn k - (a0 • K + b0 • MovingFrameODE.quarterTurn K)‖ ≤ |a - a0| + |b - b0| + (|a0| + |b0|) * ‖k - K‖

theorem NavierStokes.PrimaryTargetBounds.tangent_ratio_error {n : MovingFrameODE.Space} {K : Plane} {B s delta r h : ℝ} (hB : 0 < B) (hK : ‖K‖ = 1) (hd : delta ≤ B / 2) (hn : ‖n - MovingFrameODE.pack (B * s) (B • K)‖ ≤ delta) : ‖-MovingFrameODE.radialSlope n • MovingFrameODE.normalDirection n + r • MovingFrameODE.quarterTurn (MovingFrameODE.normalDirection n) - (-s • K + h • MovingFrameODE.quarterTurn K)‖ ≤ (2 * (1 + |s|) + 4 * (|s| + |h|)) * delta / B + |r - h|

noncomputable def NavierStokes.PrimaryTargetBounds.pulseRatio (d : PrimaryODE.FrameData Slow) (lam u L : ℝ) (p : Slow) (v : ℝ) : Plane

Pulse ratio as an element of Plane.

Equations

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

theorem NavierStokes.PrimaryTargetBounds.pulseRatio_eq (d : PrimaryODE.FrameData Slow) (lam u : ℝ) {L : ℝ} (hL : 0 < L) {U : Set Slow} (hA : ContinuousOn (d.coefficient 1) (U ×ˢ Set.Icc 0 L)) {p : Slow} (hp : p ∈ U) {v : ℝ} (hv : v ∈ Set.Icc 0 L) (hx : PrimaryODE.radialPrimary ⋯ d (fun (z : Slow × ℝ) => PrimaryPulseBounds.referenceP lam u L z.2) p v ≠ 0) : pulseRatio d lam u L p v = -d.rho (p, v) • (d.frame (p, v)) 0 + (PrimaryODE.transversePrimary ⋯ d (fun (z : Slow × ℝ) => PrimaryPulseBounds.referenceP lam u L z.2) p v / PrimaryODE.radialPrimary ⋯ d (fun (z : Slow × ℝ) => PrimaryPulseBounds.referenceP lam u L z.2) p v) • (d.frame (p, v)) 1

noncomputable def NavierStokes.PrimaryTargetBounds.geometricRatioConstant (M u : ℝ) : ℝ

Geometric ratio constant as an element of ℝ.

Equations

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

noncomputable def NavierStokes.PrimaryTargetBounds.ratioConstant (M u gap : ℝ) : ℝ

Ratio constant, constructed using geometricRatioConstant.

Equations

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

theorem NavierStokes.PrimaryTargetBounds.geometricRatioConstant_nonneg {M u : ℝ} (hM : 1 ≤ M) : 0 ≤ geometricRatioConstant M u

theorem NavierStokes.PrimaryTargetBounds.ratioConstant_nonneg {M u gap : ℝ} (hM : 1 ≤ M) (hgap : 0 < gap) : 0 ≤ ratioConstant M u gap

theorem NavierStokes.PrimaryTargetBounds.signedSlot_center {u L : ℝ} (hu : 0 ≤ u) (hL : 0 < L) (j : Fin 2) (v : ℝ) : |PhaseEstimates.signedSlot (phaseSign j) u L v - phaseSign j * u| = u * |v - L / 2| / L

theorem NavierStokes.PrimaryTargetBounds.coefficient_continuous {ι : Type u_1} {D : PhaseJetBounds.Domain ι Slow} {h r0 u M : ℝ} (a : BasePhaseGeometry.FamilyData D h r0 u M) (hh : 0 ≤ h) (hr : 0 < r0) (hM : 1 ≤ M) (hu : 0 < u) (huM : u ≤ M) (hL : 1 / (2 * r0) ≤ M) (hslot : 4 * r0 * ChartScales.Tg ≤ M) (hlarge : ∀ (i : ι), BasePhaseGeometry.LargeBand h M u (a.band i)) (i : ι) : ContinuousOn ((a.frame i).coefficient 1) (D.carrier i ×ˢ Set.Icc 0 (a.length i))

theorem NavierStokes.PrimaryTargetBounds.primary_ratio_error {ι : Type u_1} {D : PhaseJetBounds.Domain ι Slow} {h r0 u M : ℝ} (a : BasePhaseGeometry.FamilyData D h r0 u M) (hh : 0 ≤ h) (hr : 0 < r0) (hM : 1 ≤ M) (hu : 0 < u) (huM : u ≤ M) (hL : 1 / (2 * r0) ≤ M) (hslot : 4 * r0 * ChartScales.Tg ≤ M) (hlarge : ∀ (i : ι), BasePhaseGeometry.LargeBand h M u (a.band i)) (i : ι) {p : Slow} (hp : p ∈ D.carrier i) {gap : ℝ} (hgap : 0 < gap) (hg : ∀ v ∈ Set.Icc 0 (a.length i), gap ≤ ViscousPropagator.referenceEigenvalue (a.lam i) u (a.length i) v) (hcone : 2 * GrowingMode.coneConstant gap (BasePhaseGeometry.modalConstant M u) ≤ D.scale i) {v : ℝ} (hv : v ∈ Set.Icc 0 (a.length i)) : ‖pulseRatio (a.frame i) (a.lam i) u (a.length i) p v - modelVector (a.c0 i) (a.slope i (p, v)) (a.K i)‖ ≤ ratioConstant M u gap / D.scale i

theorem NavierStokes.PrimaryTargetBounds.primary_center_error {ι : Type u_1} {D : PhaseJetBounds.Domain ι Slow} {h r0 u M : ℝ} (a : BasePhaseGeometry.FamilyData D h r0 u M) (hh : 0 ≤ h) (hr : 0 < r0) (hM : 1 ≤ M) (hu : 0 < u) (huM : u ≤ M) (hL : 1 / (2 * r0) ≤ M) (hslot : 4 * r0 * ChartScales.Tg ≤ M) (hlarge : ∀ (i : ι), BasePhaseGeometry.LargeBand h M u (a.band i)) (i : ι) (j : Fin 2) (hsign : a.sigma i = phaseSign j) {p : Slow} (hp : p ∈ D.carrier i) {gap : ℝ} (hgap : 0 < gap) (hg : ∀ v ∈ Set.Icc 0 (a.length i), gap ≤ ViscousPropagator.referenceEigenvalue (a.lam i) u (a.length i) v) (hcone : 2 * GrowingMode.coneConstant gap (BasePhaseGeometry.modalConstant M u) ≤ D.scale i) {v : ℝ} (hv : v ∈ Set.Icc 0 (a.length i)) (k : Fin 2) : |(PrimaryPulseBounds.normalizedPulse (a.frame i) (a.lam i) u (a.length i) (p, v / a.length i)).ofLp k.succ / (PrimaryPulseBounds.normalizedPulse (a.frame i) (a.lam i) u (a.length i) (p, v / a.length i)).ofLp 0 - modelMatrix (a.c0 i) u (a.K i) k j| ≤ 2 * r0 * ChartScales.Tg * ratioConstant M u gap / a.length i + (M + 1) * u * |v - a.length i / 2| / a.length i

The actual uncut primary is compared with the central signed model. The two errors have the concentration-compatible orders 1/L and |v-L/2|/L; no covariance convergence is a hypothesis.

structure NavierStokes.PrimaryTargetBounds.CompatiblePair {ι : Type u_1} {D : PhaseJetBounds.Domain ι Slow} {h r0 u M : ℝ} (a : Fin 2 → BasePhaseGeometry.FamilyData D h r0 u M) : Prop

The two signs share the same actual representative.

• band (j : Fin 2) (i : ι) : (a j).band i = (a 0).band i
• ratio (j : Fin 2) (i : ι) : (a j).c0 i = (a 0).c0 i
• transverse (j : Fin 2) (i : ι) : (a j).K i = (a 0).K i
• sign (j : Fin 2) (i : ι) : (a j).sigma i = phaseSign j

noncomputable def NavierStokes.PrimaryTargetBounds.familyCovariance {ι : Type u_1} {D : PhaseJetBounds.Domain ι Slow} {h r0 u M : ℝ} (vr vt : TorusInverse.Plane) (a : Fin 2 → BasePhaseGeometry.FamilyData D h r0 u M) (i : ι) (p : Slow) : Mat2

The native finite covariance with the original joint label.

Equations

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

theorem NavierStokes.PrimaryTargetBounds.familyCovariance_eq_native {ι : Type u_1} {D : PhaseJetBounds.Domain ι Slow} {h r0 u M : ℝ} (vr vt : TorusInverse.Plane) (a : Fin 2 → BasePhaseGeometry.FamilyData D h r0 u M) (hc : CompatiblePair a) (i : ι) (p : Slow) : familyCovariance vr vt a i p = PrimaryCovarianceBounds.nativePrimaryCovariance vr vt r0 h (fun (j : Fin 2) (x : ℕ) => (a j).frame i) (fun (j : Fin 2) (x : ℕ) => (a j).lam i) (fun (x : Fin 2) (x_1 : ℕ) => u) ((a 0).band i) p

theorem NavierStokes.PrimaryTargetBounds.exists_family_bounds {h r0 u M : ℝ} (vr vt : TorusInverse.Plane) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (hh : 0 ≤ h) (hr : 0 < r0) (hM : 1 ≤ M) (hu : 0 < u) (huM : u ≤ M) (hL : 1 / (2 * r0) ≤ M) (hslot : 4 * r0 * ChartScales.Tg ≤ M) {eta : ℝ} (heta : 0 < eta) : ∃ (N : ℕ), 4 ≤ N ∧ ∃ (detGap : ℝ) (entryBound : ℝ) (inverseLower : ℝ), 0 < detGap ∧ 1 ≤ entryBound ∧ 0 < inverseLower ∧ ∀ (ι : Type u_2) (D : PhaseJetBounds.Domain ι Slow) (a : Fin 2 → BasePhaseGeometry.FamilyData D h r0 u M), CompatiblePair a → (∀ (j : Fin 2) (i : ι), BasePhaseGeometry.LargeBand h M u ((a j).band i)) → ∀ (i : ι), N ≤ (a 0).band i → ∀ p ∈ D.carrier i, ∀ (T : Plane), ((a 0).c0 i, (a 0).K i, T) ∈ modelSet M u eta → ∀ (zeta : ℝ), 0 ≤ zeta → PrimaryCovarianceBounds.ZeroOrderBounds (√(ChartScales.S ((a 0).band i))) detGap entryBound inverseLower zeta (familyCovariance vr vt a i p) (FlatCovariance.scaledTarget zeta fun (k : Fin 2) => T.ofLp k)

Uniform finite-matrix bounds follow from the actual constructed phases and their ODEs. The model point only records the common representative and a unit target direction.

theorem NavierStokes.PrimaryTargetBounds.prepared_pair {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) : CompatiblePair (PrimaryGeometryAssembly.family H v a)

theorem NavierStokes.PrimaryTargetBounds.prepared_model_mem {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (L : PrimaryGeometryAssembly.Index W a.N) {p : Slow} (hp : p ∈ PositiveRepresentatives.positivePart (PrimaryGeometryAssembly.referenceSet W)) (hpL : p ∈ (PrimaryGeometryAssembly.domain W a.N).carrier L) : ((PrimaryGeometryAssembly.family H v a 0).c0 L, (PrimaryGeometryAssembly.family H v a 0).K L, a.target p) ∈ modelSet a.M a.u a.eta

The mixed target margin is supplied by the actual closed profile direction and its actual positive representative.

noncomputable def NavierStokes.PrimaryTargetBounds.preparedCovariance {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (vr vt : TorusInverse.Plane) : PrimaryGeometryAssembly.Index W a.N → Slow → Mat2

Prepared covariance, given by familyCovariance vr vt (family H v a).

Equations

• NavierStokes.PrimaryTargetBounds.preparedCovariance H v a vr vt = NavierStokes.PrimaryTargetBounds.familyCovariance vr vt (NavierStokes.PrimaryGeometryAssembly.family H v a)

theorem NavierStokes.PrimaryTargetBounds.preparedCovariance_eq_construction {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (vr vt : TorusInverse.Plane) (hr0 : 0 < r0) : preparedCovariance H v a vr vt = PrimaryPulseBounds.primaryCovariance (fun (x : Fin 2) (L : BaseChartJets.CellIndex F.data.h (NominalConeAssembly.activeLeft W) (NominalConeAssembly.activeRight W) a.N) => PartitionedCovariance.nativePrefactor vr vt r0 * ChartScales.timeCoefficient F.data.h (BaseChartJets.cellBand L) * ChartScales.slotLength r0 F.data.h (BaseChartJets.cellBand L)) (fun (j : Fin 2) => (PrimaryGeometryAssembly.construction H v a hr0 j).frame) (fun (j : Fin 2) => (PrimaryGeometryAssembly.construction H v a hr0 j).lam) (fun (j : Fin 2) => (PrimaryGeometryAssembly.construction H v a hr0 j).u) fun (j : Fin 2) => (PrimaryGeometryAssembly.construction H v a hr0 j).L

theorem NavierStokes.PrimaryTargetBounds.exists_prepared_bounds {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (vr vt : TorusInverse.Plane) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (hr0 : 0 < r0) : ∃ (N : ℕ), a.N ≤ N ∧ ∃ (detGap : ℝ) (entryBound : ℝ) (inverseLower : ℝ), 0 < detGap ∧ 1 ≤ entryBound ∧ 0 < inverseLower ∧ ∀ (L : PrimaryGeometryAssembly.Index W a.N), N ≤ BaseChartJets.cellBand L → ∀ p ∈ PositiveRepresentatives.positivePart (PrimaryGeometryAssembly.referenceSet W), p ∈ (PrimaryGeometryAssembly.domain W a.N).carrier L → ∀ (zeta : ℝ), 0 ≤ zeta → PrimaryCovarianceBounds.ZeroOrderBounds (√(ChartScales.S (BaseChartJets.cellBand L))) detGap entryBound inverseLower zeta (preparedCovariance H v a vr vt L p) (FlatCovariance.scaledTarget zeta fun (k : Fin 2) => (a.target p).ofLp k)

One later cutoff, with all representatives, targets and phases kept fixed, supplies the actual normalized determinant and inverse bounds.

noncomputable def NavierStokes.PrimaryTargetBounds.leftRadius {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : ℝ

Left radius, given by Real.sqrt (2 * NominalConeAssembly.activeLeft W).

Equations

• NavierStokes.PrimaryTargetBounds.leftRadius W = √(2 * NavierStokes.NominalConeAssembly.activeLeft W)

noncomputable def NavierStokes.PrimaryTargetBounds.rightRadius {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : ℝ

Right radius, given by Real.sqrt (2 * NominalConeAssembly.activeRight W).

Equations

• NavierStokes.PrimaryTargetBounds.rightRadius W = √(2 * NavierStokes.NominalConeAssembly.activeRight W)

theorem NavierStokes.PrimaryTargetBounds.leftRadius_pos {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : 0 < leftRadius W

theorem NavierStokes.PrimaryTargetBounds.rightRadius_pos {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : 0 < rightRadius W

theorem NavierStokes.PrimaryTargetBounds.radii_ordered {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : leftRadius W < rightRadius W

noncomputable def NavierStokes.PrimaryTargetBounds.stripWeight {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (r : ℝ) : ℝ

These are the radial-log coefficients of the very same product weight, not a replacement weight with a faster decay.

Equations

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

theorem NavierStokes.PrimaryTargetBounds.stripWeight_nonneg {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (r : ℝ) : 0 ≤ stripWeight W r

theorem NavierStokes.PrimaryTargetBounds.edge_double (c x : ℝ) : FlatCutoff.edge c (2 * x) = FlatCutoff.edge (c / 4) x

theorem NavierStokes.PrimaryTargetBounds.log_square_half {r : ℝ} (hr : 0 < r) : Real.log (r ^ 2 / 2) = 2 * Real.log r - Real.log 2

theorem NavierStokes.PrimaryTargetBounds.stripWeight_eq {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (r eta : ℝ) (hr : 0 < r) : stripWeight W r = FinalSlowBase.weight W (r ^ 2 / 2, eta)

noncomputable def NavierStokes.PrimaryTargetBounds.profileRadius (h : ℝ) (p : Slow) : ℝ

Profile radius, given by p.1 / Real.sqrt (BaseChartJets.normalizedCoordinates h p).1.

Equations

• NavierStokes.PrimaryTargetBounds.profileRadius h p = p.1 / √(NavierStokes.BaseChartJets.normalizedCoordinates h p).1

noncomputable def NavierStokes.PrimaryTargetBounds.movingWeight {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (p : Slow) : ℝ

Moving weight, given by stripWeight W (profileRadius F.data.h p).

Equations

• NavierStokes.PrimaryTargetBounds.movingWeight W p = NavierStokes.PrimaryTargetBounds.stripWeight W (NavierStokes.PrimaryTargetBounds.profileRadius F.data.h p)

theorem NavierStokes.PrimaryTargetBounds.movingWeight_nonneg {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (p : Slow) : 0 ≤ movingWeight W p

theorem NavierStokes.PrimaryTargetBounds.profileRadius_pos {F : OutgoingProfile.Profile} {p : Slow} (hT : 0 < p.2.2) (hR : 0 < p.1) : 0 < profileRadius F.data.h p

theorem NavierStokes.PrimaryTargetBounds.profileRadius_sq {F : OutgoingProfile.Profile} {p : Slow} (hT : 0 < p.2.2) : profileRadius F.data.h p ^ 2 / 2 = (BaseChartJets.normalizedCoordinates F.data.h p).2.1

theorem NavierStokes.PrimaryTargetBounds.movingWeight_eq {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : Slow} (hT : 0 < p.2.2) (hR : 0 < p.1) : movingWeight W p = FinalSlowBase.weight W (BaseChartJets.normalizedCoordinates F.data.h p).2

noncomputable def NavierStokes.PrimaryTargetBounds.meanPoint (x : LocalSignedRequest.Point) : Slow

The mean-variable ordering (R,((T,Z),Y)) uses exactly the same normalized point (R,(Z,T)).

Equations

• NavierStokes.PrimaryTargetBounds.meanPoint x = (x.1, x.2.1.2, x.2.1.1)

theorem NavierStokes.PrimaryTargetBounds.meanPoint_scalar {F : OutgoingProfile.Profile} (x : LocalSignedRequest.Point) : (BaseChartJets.normalizedCoordinates F.data.h (meanPoint x)).1 = MeanRankUpdate.chartQ (2 * F.data.h) x

theorem NavierStokes.PrimaryTargetBounds.movingStripData_zeta {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) (epsilon S : ℕ → ℝ) (hepsilon : ∀ (n : ℕ), 0 < epsilon n) (hepsilon_one : ∀ (n : ℕ), epsilon n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) (x : LocalSignedRequest.Point) : (LocalSignedRequest.movingStripData U (leftRadius W) (rightRadius W) (FinalSlowBase.edgeExponent W / 4) 1 ⋯ ⋯ movingStripData_zeta._proof_2 epsilon S hepsilon hepsilon_one hS).zeta x = movingWeight W (meanPoint x)

Exact equality with the strip used for the signed correction.

theorem NavierStokes.PrimaryTargetBounds.weight_zero_of_not_active {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {w : ℝ × ℝ} (hx : w.1 ∉ Set.Ioo (NominalConeAssembly.activeLeft W) (NominalConeAssembly.activeRight W)) : FinalSlowBase.weight W w = 0

noncomputable def NavierStokes.PrimaryTargetBounds.actualTarget {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (p : Slow) : Plane

The literal leading covariance target in its own normalized band.

Equations

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

noncomputable def NavierStokes.PrimaryTargetBounds.targetAmplitude {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (p : Slow) : ℝ

Target amplitude as an element of ℝ.

Equations

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

theorem NavierStokes.PrimaryTargetBounds.targetAmplitude_nonneg {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {p : Slow} (hT : 0 < p.2.2) : 0 ≤ targetAmplitude v p

theorem NavierStokes.PrimaryTargetBounds.stress_norm_le_plane {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (w : ℝ × ℝ) : ‖FinalSlowBase.leadingStress v w‖ ≤ ‖ProfileSpectralCone.stressVector v.profiles F.data.h w‖

theorem NavierStokes.PrimaryTargetBounds.targetAmplitude_lower {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (hcone : LeadingStressWeights.FullTrueCone v) : ∃ (c : ℝ), 0 < c ∧ ∀ p ∈ PositiveRepresentatives.positivePart (PrimaryGeometryAssembly.referenceSet W), (BaseChartJets.normalizedCoordinates F.data.h p).2.1 ∈ Set.Ioo (NominalConeAssembly.activeLeft W) (NominalConeAssembly.activeRight W) → c * movingWeight W p ≤ targetAmplitude v p

theorem NavierStokes.PrimaryTargetBounds.actualTarget_eq_direction {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) {p : Slow} (hp : p ∈ PositiveRepresentatives.positivePart (PrimaryGeometryAssembly.referenceSet W)) (hx : (BaseChartJets.normalizedCoordinates F.data.h p).2.1 ∈ Set.Ioo (NominalConeAssembly.activeLeft W) (NominalConeAssembly.activeRight W)) : actualTarget v p = targetAmplitude v p • a.target p

theorem NavierStokes.PrimaryTargetBounds.stress_zero_of_not_active {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {w : ℝ × ℝ} (hw : 0 < w.1) (heta : w.2 ∈ Set.Icc (-1) 1) (hx : w.1 ∉ Set.Ioo (NominalConeAssembly.activeLeft W) (NominalConeAssembly.activeRight W)) : ProfileSpectralCone.stressVector v.profiles F.data.h w = 0

theorem NavierStokes.PrimaryTargetBounds.actualTarget_eq_direction_all {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) {p : Slow} (hp : p ∈ PositiveRepresentatives.positivePart (PrimaryGeometryAssembly.referenceSet W)) : actualTarget v p = targetAmplitude v p • a.target p

theorem NavierStokes.PrimaryTargetBounds.targetAmplitude_lower_all {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (hcone : LeadingStressWeights.FullTrueCone v) : ∃ (c : ℝ), 0 < c ∧ ∀ p ∈ PositiveRepresentatives.positivePart (PrimaryGeometryAssembly.referenceSet W), c * movingWeight W p ≤ targetAmplitude v p

theorem NavierStokes.PrimaryTargetBounds.covarianceTarget_eq_actual {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {p : Slow} (hT : 0 < p.2.2) (hR : 0 < p.1) (N : ℕ) (U : PartitionedCovariance.UnsignedLabel) : FinalSlowBase.covarianceTarget H v (ChartScales.Q (U.1 + N) * (BaseChartJets.normalizedCoordinates F.data.h p).1) N U p = actualTarget v p

The chart target at its own band is exactly the actual leading stress times the residual scalar coordinate.

theorem NavierStokes.PrimaryTargetBounds.exists_actual_bounds {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hcone : LeadingStressWeights.FullTrueCone v) (vr vt : TorusInverse.Plane) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (hr0 : 0 < r0) : ∃ (N : ℕ), a.N ≤ N ∧ ∃ (detGap : ℝ) (entryBound : ℝ) (inverseLower : ℝ), 0 < detGap ∧ 1 ≤ entryBound ∧ 0 < inverseLower ∧ ∀ (L : PrimaryGeometryAssembly.Index W a.N), N ≤ BaseChartJets.cellBand L → ∀ p ∈ PositiveRepresentatives.positivePart (PrimaryGeometryAssembly.referenceSet W), p ∈ (PrimaryGeometryAssembly.domain W a.N).carrier L → PrimaryCovarianceBounds.ZeroOrderBounds (√(ChartScales.S (BaseChartJets.cellBand L))) detGap entryBound inverseLower (movingWeight W p) (preparedCovariance H v a vr vt L p) fun (k : Fin 2) => (actualTarget v p).ofLp k

The actual primary covariance and the actual leading target satisfy all order-zero hypotheses used for positive square-root weights, with the same moving flat weight through both closed attachment edges.

theorem NavierStokes.PrimaryTargetBounds.restricted_covariance {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (vr vt : TorusInverse.Plane) (N : ℕ) (hN : a.N ≤ N) (L : PrimaryGeometryAssembly.Index W N) (p : Slow) : preparedCovariance H v (a.restrict N hN) vr vt L p = preparedCovariance H v a vr vt (PrimaryGeometryAssembly.earlierIndex hN L) p

theorem NavierStokes.PrimaryTargetBounds.exists_restricted_actual_bounds {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hcone : LeadingStressWeights.FullTrueCone v) (vr vt : TorusInverse.Plane) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) (hr0 : 0 < r0) : ∃ (N : ℕ) (hN : a.N ≤ N) (detGap : ℝ) (entryBound : ℝ) (inverseLower : ℝ), 0 < detGap ∧ 1 ≤ entryBound ∧ 0 < inverseLower ∧ ∀ (L : PrimaryGeometryAssembly.Index W N), ∀ p ∈ PositiveRepresentatives.positivePart (PrimaryGeometryAssembly.referenceSet W), p ∈ (PrimaryGeometryAssembly.domain W N).carrier L → PrimaryCovarianceBounds.ZeroOrderBounds (√(ChartScales.S (BaseChartJets.cellBand L))) detGap entryBound inverseLower (movingWeight W p) (preparedCovariance H v (a.restrict N hN) vr vt L p) fun (k : Fin 2) => (actualTarget v p).ofLp k

A single final band threshold suffices. Restriction retains the original representative, carrier and phase on each surviving label.

theorem NavierStokes.PrimaryTargetBounds.exists_constructed_bounds {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (hcone : LeadingStressWeights.FullTrueCone v) (upper : ℝ) (B : ℕ) (r0 : ℝ) (hr0 : 0 < r0) (hbox : 2 * NominalConeAssembly.activeRight W ≤ FinalSlowBase.boxRadius W upper) (N0 : ℕ) (vr vt : TorusInverse.Plane) (hdet : vr.1 * vt.2 - vr.2 * vt.1 ≠ 0) : ∃ (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (detGap : ℝ) (entryBound : ℝ) (inverseLower : ℝ), 0 < detGap ∧ 1 ≤ entryBound ∧ 0 < inverseLower ∧ ∀ (L : PrimaryGeometryAssembly.Index W a.N), ∀ p ∈ PositiveRepresentatives.positivePart (PrimaryGeometryAssembly.referenceSet W), p ∈ (PrimaryGeometryAssembly.domain W a.N).carrier L → PrimaryCovarianceBounds.ZeroOrderBounds (√(ChartScales.S (BaseChartJets.cellBand L))) detGap entryBound inverseLower (movingWeight W p) (preparedCovariance H v a vr vt L p) fun (k : Fin 2) => (actualTarget v p).ofLp k

The source profile supplies the whole geometry. There is no extra target orientation, determinant, inverse-weight or ODE-error input.