The material defect of the actual primary chart phase

The same selected phase is pulled through the actual physical band change. The base coefficients are identified through their common physical field before the native material cancellation is used.

@[reducible, inline]

abbrev NavierStokes.ActualPhaseDefect.Slow : Type

Slow: an abbreviation for PhaseCalculus.Slow.

Equations

• NavierStokes.ActualPhaseDefect.Slow = NavierStokes.PhaseCalculus.Slow

@[reducible, inline]

abbrev NavierStokes.ActualPhaseDefect.Plane : Type

Plane: an abbreviation for TorusInverse.Plane.

Equations

• NavierStokes.ActualPhaseDefect.Plane = NavierStokes.TorusInverse.Plane

@[reducible, inline]

abbrev NavierStokes.ActualPhaseDefect.Cylinder : Type

Cylinder: an abbreviation for PhysicalResidualBridge.Cylinder.

Equations

• NavierStokes.ActualPhaseDefect.Cylinder = NavierStokes.PhysicalResidualBridge.Cylinder

theorem NavierStokes.ActualPhaseDefect.ratioPower_mul_power {Q Qr : ℝ} (_hQ : 0 < Q) (hQr : 0 < Qr) (a : ℝ) : PhysicalParticularWave.ratioPower Q Qr a * Qr ^ a = Q ^ a

theorem NavierStokes.ActualPhaseDefect.bandPoint_change {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (h : ℝ) (p : Slow) : BaseChartJets.bandPoint h Qr ((ActualSignedGeometry.slowChange h Q Qr) p) = BaseChartJets.bandPoint h Q p

theorem NavierStokes.ActualPhaseDefect.clock_eq_velocity_radial {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (h : ℝ) : PhysicalParticularWave.clockWeight h Q Qr = PhysicalParticularWave.velocityWeight h Q Qr * PhysicalParticularWave.ratioPower Q Qr (1 / 2)

theorem NavierStokes.ActualPhaseDefect.material_chartChange {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (h : ℝ) (i gap : ℕ) (scale : ℝ) (b F G br Fr Gr Phi : Cylinder → ℝ) {x : Cylinder} (hx : 0 < x.1.1) (hPhi : DifferentiableAt ℝ Phi ((PhysicalParticularWave.cylinderChange h Q Qr gap) x)) (hb : b x = PhysicalParticularWave.velocityWeight h Q Qr * br ((PhysicalParticularWave.cylinderChange h Q Qr gap) x)) (hF : F x = PhysicalParticularWave.clockWeight h Q Qr * Fr ((PhysicalParticularWave.cylinderChange h Q Qr gap) x)) (hG : G x = PhysicalParticularWave.velocityWeight h Q Qr * Gr ((PhysicalParticularWave.cylinderChange h Q Qr gap) x)) : LinearWaveResidual.materialPhaseDefect PhysicalResidualBridge.ScaledGraph.radius b F G (PhysicalResidualBridge.commonGraph Q h i).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph Q h i).axial (PhysicalResidualBridge.commonGraph Q h i).temporal (fun (y : PhysicalResidualBridge.Cylinder) => scale * Phi ((PhysicalParticularWave.cylinderChange h Q Qr gap) y)) x = scale * PhysicalParticularWave.clockWeight h Q Qr * LinearWaveResidual.materialPhaseDefect PhysicalResidualBridge.ScaledGraph.radius br Fr Gr (PhysicalResidualBridge.commonGraph Qr h (i + gap)).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph Qr h (i + gap)).axial (PhysicalResidualBridge.commonGraph Qr h (i + gap)).temporal Phi ((PhysicalParticularWave.cylinderChange h Q Qr gap) x)

Only primitive base values and the actual chart differential enter this identity. It does not assume a phase-defect identity.

theorem NavierStokes.ActualPhaseDefect.slot_coordinate_temporal {dimension h : ℝ} (sys : PartitionedCovariance.SlotSystem dimension h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (l : SlotColoring.Label) : (ActualSignedGeometry.slotGeometry sys ActualSignedGeometry.vectors_det l 0).coordinateLinear ActualSignedGeometry.temporalVector = (0, (ChartScales.timeCoefficient h l.1)⁻¹)

theorem NavierStokes.ActualPhaseDefect.slot_coordinates_temporal {dimension h : ℝ} (sys : PartitionedCovariance.SlotSystem dimension h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (l : SlotColoring.Label) (x : Cylinder) : (ActualSignedGeometry.slotLinear (ActualSignedGeometry.slotGeometry sys ActualSignedGeometry.vectors_det l 0)) ((PhysicalResidualBridge.commonGraph (ChartScales.Q l.1) h (ChartScales.nativeIndex h l.1)).temporal x) = PhaseCalculus.eV - ChartScales.epsilon h l.1 • PhaseCalculus.eT

theorem NavierStokes.ActualPhaseDefect.slot_material {dimension h : ℝ} (sys : PartitionedCovariance.SlotSystem dimension h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (l : SlotColoring.Label) (p pz x0 : ℝ) (b F G : Slow → ℝ) (k : TorusInverse.Frequency) {x : Cylinder} (hx : 0 < x.1.1) (hF : DifferentiableAt ℝ F (x.1.1, x.1.2.1)) (hG : DifferentiableAt ℝ G (x.1.1, x.1.2.1)) : LinearWaveResidual.materialPhaseDefect PhysicalResidualBridge.ScaledGraph.radius (fun (y : PhysicalResidualBridge.Cylinder) => b (y.1.1, y.1.2.1)) (fun (y : PhysicalResidualBridge.Cylinder) => F (y.1.1, y.1.2.1)) (fun (y : PhysicalResidualBridge.Cylinder) => G (y.1.1, y.1.2.1)) (PhysicalResidualBridge.commonGraph (ChartScales.Q l.1) h (ChartScales.nativeIndex h l.1)).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph (ChartScales.Q l.1) h (ChartScales.nativeIndex h l.1)).axial (PhysicalResidualBridge.commonGraph (ChartScales.Q l.1) h (ChartScales.nativeIndex h l.1)).temporal (PhaseCalculus.phase (ChartScales.epsilon h l.1) p pz x0 F G ∘ ActualSignedGeometry.slotCoordinates (ActualSignedGeometry.slotGeometry sys ActualSignedGeometry.vectors_det l 0) k) x = PrimaryMaterialDefect.expression (ChartScales.epsilon h l.1) p pz x0 ((ActualSignedGeometry.slotGeometry sys ActualSignedGeometry.vectors_det l 0).coordinates k x.1.2.2).2 (b (x.1.1, x.1.2.1)) (G (x.1.1, x.1.2.1)) (PhaseCalculus.slowR F (x.1.1, x.1.2.1)) (PhaseCalculus.slowR G (x.1.1, x.1.2.1)) (PhaseCalculus.slowT F (x.1.1, x.1.2.1)) (PhaseCalculus.slowT G (x.1.1, x.1.2.1)) (PhaseCalculus.slowZ F (x.1.1, x.1.2.1)) (PhaseCalculus.slowZ G (x.1.1, x.1.2.1))

theorem NavierStokes.ActualPhaseDefect.radialSlow_change {out : OutgoingProfile.Profile} {W : NominalProfile.Witness out} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B n m : ℕ) (p : Slow) : BaseContextAssembly.radialSlow H v upper B n p = PhysicalParticularWave.velocityWeight out.data.h (ChartScales.Q n) (ChartScales.Q m) * BaseContextAssembly.radialSlow H v upper B m ((ActualSignedGeometry.slowChange out.data.h (ChartScales.Q n) (ChartScales.Q m)) p)

theorem NavierStokes.ActualPhaseDefect.axialSlow_change {out : OutgoingProfile.Profile} {W : NominalProfile.Witness out} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B n m : ℕ) {p : Slow} (hT : 0 < p.2.2) : BaseContextAssembly.axialSlow H v upper B n p = PhysicalParticularWave.velocityWeight out.data.h (ChartScales.Q n) (ChartScales.Q m) * BaseContextAssembly.axialSlow H v upper B m ((ActualSignedGeometry.slowChange out.data.h (ChartScales.Q n) (ChartScales.Q m)) p)

theorem NavierStokes.ActualPhaseDefect.frequencySlow_change {out : OutgoingProfile.Profile} {W : NominalProfile.Witness out} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B n m : ℕ) {p : Slow} (hT : 0 < p.2.2) (hR : 0 < p.1) : BaseContextAssembly.frequencySlow H v upper B n p = PhysicalParticularWave.clockWeight out.data.h (ChartScales.Q n) (ChartScales.Q m) * BaseContextAssembly.frequencySlow H v upper B m ((ActualSignedGeometry.slowChange out.data.h (ChartScales.Q n) (ChartScales.Q m)) p)

theorem NavierStokes.ActualPhaseDefect.material_congr_germ {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (R b F G : E → ℝ) (Vr Vtheta Vz Vt : E → E) {Phi Psi : E → ℝ} {x : E} (he : Phi =ᶠ[nhds x] Psi) : LinearWaveResidual.materialPhaseDefect R b F G Vr Vtheta Vz Vt Phi =ᶠ[nhds x] LinearWaveResidual.materialPhaseDefect R b F G Vr Vtheta Vz Vt Psi

theorem NavierStokes.ActualPhaseDefect.periodic_material_germ {dimension h : ℝ} (sys : PartitionedCovariance.SlotSystem dimension h ActualSignedGeometry.radialVector ActualSignedGeometry.temporalVector) (hh : 0 ≤ h) {l : SlotColoring.Label} (hl : 4 ≤ l.1) (p pz x0 : ℝ) (b F G : Slow → ℝ) {S : Set Slow} (hS : IsOpen S) (hF : ContDiffOn ℝ (↑⊤) F S) (hG : ContDiffOn ℝ (↑⊤) G S) (k : TorusInverse.Frequency) {x : Cylinder} (hR : 0 < x.1.1) (hx : (x.1.1, x.1.2.1) ∈ S) (hc : (ActualSignedGeometry.slotGeometry sys ActualSignedGeometry.vectors_det l 0).coordinates k x.1.2.2 ∈ (ActualSignedGeometry.clockWindow sys l.1).core) : (fun (y : Cylinder) => LinearWaveResidual.materialPhaseDefect PhysicalResidualBridge.ScaledGraph.radius (fun (z : PhysicalResidualBridge.Cylinder) => b (z.1.1, z.1.2.1)) (fun (z : PhysicalResidualBridge.Cylinder) => F (z.1.1, z.1.2.1)) (fun (z : PhysicalResidualBridge.Cylinder) => G (z.1.1, z.1.2.1)) (PhysicalResidualBridge.commonGraph (ChartScales.Q l.1) h (ChartScales.nativeIndex h l.1)).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph (ChartScales.Q l.1) h (ChartScales.nativeIndex h l.1)).axial (PhysicalResidualBridge.commonGraph (ChartScales.Q l.1) h (ChartScales.nativeIndex h l.1)).temporal (ActualSignedGeometry.periodicPhase sys l 0 (ChartScales.epsilon h l.1) p pz x0 F G) y) =ᶠ[nhds x] fun (y : Cylinder) => PrimaryMaterialDefect.expression (ChartScales.epsilon h l.1) p pz x0 ((ActualSignedGeometry.slotGeometry sys ActualSignedGeometry.vectors_det l 0).coordinates k y.1.2.2).2 (b (y.1.1, y.1.2.1)) (G (y.1.1, y.1.2.1)) (PhaseCalculus.slowR F (y.1.1, y.1.2.1)) (PhaseCalculus.slowR G (y.1.1, y.1.2.1)) (PhaseCalculus.slowT F (y.1.1, y.1.2.1)) (PhaseCalculus.slowT G (y.1.1, y.1.2.1)) (PhaseCalculus.slowZ F (y.1.1, y.1.2.1)) (PhaseCalculus.slowZ G (y.1.1, y.1.2.1))

theorem NavierStokes.ActualPhaseDefect.context_material_swap (c : CorrectionState.Context LocalSignedRequest.Point) (s : WeightedClasses.StripData LocalSignedRequest.Point) (a : LinearWaveBounds.WaveCoefficients (LocalSignedRequest.Point × ℝ)) (n : ℕ) (G : PhysicalResidualBridge.ScaledGraph) (hG : PhysicalResidualTZ.MatchesAtTZ c.operators G n) (hepsilon : s.epsilon n = c.operators.epsilon n) (Phi : Cylinder → ℝ) (hphase : a.phase n = fun (y : PhysicalResidualTZ.Cylinder) => Phi (PhysicalResidualTZ.swapCylinder y)) (x : LocalSignedRequest.Point × ℝ) : a.defect (HarmonicWaveInteraction.productStrip s) (PrimaryResidualClass.directions c) n x = LinearWaveResidual.materialPhaseDefect PhysicalResidualBridge.ScaledGraph.radius (fun (y : PhysicalResidualBridge.Cylinder) => a.radialBase n (PhysicalResidualTZ.swapCylinder y)) (fun (y : PhysicalResidualBridge.Cylinder) => a.frequencyBase n (PhysicalResidualTZ.swapCylinder y)) (fun (y : PhysicalResidualBridge.Cylinder) => a.axialBase n (PhysicalResidualTZ.swapCylinder y)) G.radial PhysicalResidualBridge.ScaledGraph.angular G.axial G.temporal Phi (PhysicalResidualTZ.swapCylinder x)

noncomputable def NavierStokes.ActualPhaseDefect.nativeCopy {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) (x : CorrectionInitialization.ActualPrimary.FullPoint) : Slow × Plane

Native copy, constructed using ActualSignedGeometry.copyPoint.

Equations

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

noncomputable def NavierStokes.ActualPhaseDefect.viewMap {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : CorrectionInitialization.ActualPrimary.FullPoint →L[ℝ] Cylinder

View map as an element of FullPoint →L[ℝ] Cylinder.

Equations

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

theorem NavierStokes.ActualPhaseDefect.nativeCopy_view {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) (x : CorrectionInitialization.ActualPrimary.FullPoint) : nativeCopy j L n k x = ParticularWaveBounds.nativePoint (ActualSignedGeometry.slotGeometry CorrectionInitialization.ActualPrimary.slots CorrectionInitialization.ActualPrimary.vectors_det (PartitionedCovariance.signedLabel (PrimaryGeometryAssembly.label CorrectionInitialization.ActualPrimary.nominal L) j) 0) k (ActualSignedGeometry.cylinderNative ((viewMap L n) x))

theorem NavierStokes.ActualPhaseDefect.view_slot {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) (x : CorrectionInitialization.ActualPrimary.FullPoint) : ActualSignedGeometry.slotCoordinates (ActualSignedGeometry.slotGeometry CorrectionInitialization.ActualPrimary.slots CorrectionInitialization.ActualPrimary.vectors_det (PartitionedCovariance.signedLabel (PrimaryGeometryAssembly.label CorrectionInitialization.ActualPrimary.nominal L) j) 0) k ((viewMap L n) x) = ((nativeCopy j L n k x).1, x.2, (nativeCopy j L n k x).2.2)

theorem NavierStokes.ActualPhaseDefect.chart_phase_germ {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)) (k : TorusInverse.Frequency) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hc : (nativeCopy j L n k x).2 ∈ (ActualSignedGeometry.clockWindow CorrectionInitialization.ActualPrimary.slots (BaseChartJets.cellBand L)).core) : (CorrectionInitialization.ActualPrimary.chartCoefficients j L).phase n =ᶠ[nhds x] fun (y : CorrectionInitialization.ActualPrimary.FullPoint) => ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)) / ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n) * PhaseCalculus.phase (ChartScales.epsilon CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)) ((CorrectionInitialization.ActualPrimary.phases B N0 j).phase.p L) ((CorrectionInitialization.ActualPrimary.phases B N0 j).phase.pz L) ((CorrectionInitialization.ActualPrimary.phases B N0 j).phase.x0 L) ((CorrectionInitialization.ActualPrimary.phases B N0 j).phase.F L) ((CorrectionInitialization.ActualPrimary.phases B N0 j).phase.G L) ((nativeCopy j L n k y).1, y.2, (nativeCopy j L n k y).2.2)

The phase germ itself is valid on the closed native core, with the angle and both fast coordinates free. No open-q restriction is needed.

noncomputable def NavierStokes.ActualPhaseDefect.defect {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : CorrectionInitialization.ActualPrimary.FullPoint → ℝ

Defect as an element of FullPoint → ℝ.

Equations

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

noncomputable def NavierStokes.ActualPhaseDefect.referenceMaterial {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : Cylinder → ℝ

Reference material, constructed using LinearWaveResidual.materialPhaseDefect.

Equations

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

noncomputable def NavierStokes.ActualPhaseDefect.nativeExpression {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) (x : CorrectionInitialization.ActualPrimary.FullPoint) : ℝ

Native expression as an element of ℝ.

Equations

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

theorem NavierStokes.ActualPhaseDefect.chart_material_view {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hT : 0 < x.1.2.1.1) (hR : 0 < x.1.1) (hp : (((viewMap L n) x).1.1, ((viewMap L n) x).1.2.1) ∈ (PrimaryGeometryAssembly.domain CorrectionInitialization.ActualPrimary.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N).carrier L) : defect j L n x = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)) / ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n) * PhysicalParticularWave.clockWeight CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand L)) * referenceMaterial j L ((viewMap L n) x)

theorem NavierStokes.ActualPhaseDefect.chart_defect_germ {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)) (k : TorusInverse.Frequency) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hT : 0 < x.1.2.1.1) (hR : 0 < x.1.1) (hp : (nativeCopy j L n k x).1 ∈ (PrimaryGeometryAssembly.domain CorrectionInitialization.ActualPrimary.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N).carrier L) (hc : (nativeCopy j L n k x).2 ∈ (ActualSignedGeometry.clockWindow CorrectionInitialization.ActualPrimary.slots (BaseChartJets.cellBand L)).core) : defect j L n =ᶠ[nhds x] fun (y : CorrectionInitialization.ActualPrimary.FullPoint) => ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)) / ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n) * PhysicalParticularWave.clockWeight CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand L)) * nativeExpression j L n k y

The literal initializer defect agrees as an ambient germ with the native material expression. The closed core condition includes both endpoints of the native slow partition and leaves all fast variables free.

noncomputable def NavierStokes.ActualPhaseDefect.reducedExpression {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) (x : CorrectionInitialization.ActualPrimary.FullPoint) : ℝ

Reduced expression as an element of ℝ.

Equations

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

theorem NavierStokes.ActualPhaseDefect.nativeExpression_reduced {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hT : 0 < x.1.2.1.1) : nativeExpression j L n k x = ChartScales.epsilon CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L) * reducedExpression j L n k x

noncomputable def NavierStokes.ActualPhaseDefect.materialWeight {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : ℝ

Material weight as an element of ℝ.

Equations

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

theorem NavierStokes.ActualPhaseDefect.chart_defect_reduced_germ {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)) (k : TorusInverse.Frequency) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hT : 0 < x.1.2.1.1) (hR : 0 < x.1.1) (hp : (nativeCopy j L n k x).1 ∈ (PrimaryGeometryAssembly.domain CorrectionInitialization.ActualPrimary.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N).carrier L) (hc : (nativeCopy j L n k x).2 ∈ (ActualSignedGeometry.clockWindow CorrectionInitialization.ActualPrimary.slots (BaseChartJets.cellBand L)).core) : defect j L n =ᶠ[nhds x] fun (y : CorrectionInitialization.ActualPrimary.FullPoint) => ChartScales.epsilon CorrectionInitialization.ActualPrimary.h n * materialWeight L n * reducedExpression j L n k y

The exact small factor is the target-band viscosity.

theorem NavierStokes.ActualPhaseDefect.materialWeight_normal {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : materialWeight L n = PhysicalParticularWave.normalWeight (ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand L)) ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n) ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)) * PhysicalParticularWave.ratioPower (ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand L)) (CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h - CorrectionInitialization.ActualPrimary.h)

noncomputable def NavierStokes.ActualPhaseDefect.materialWeightBound : ℝ

Material weight bound, given by 2*ActualSignedGeometry.powerBound (h/2+1/2) * ActualSignedGeometry.powerBound (CoordinateAlgebra.A h-h).

Equations

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

theorem NavierStokes.ActualPhaseDefect.materialWeight_pos {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : 0 < materialWeight L n

theorem NavierStokes.ActualPhaseDefect.materialWeight_bound {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (hnm : n ≤ BaseChartJets.cellBand L + 4) (hmn : BaseChartJets.cellBand L ≤ n + 4) : materialWeight L n ≤ materialWeightBound

theorem NavierStokes.ActualPhaseDefect.native_core_of_interval {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hu : |(nativeCopy j L n k x).2.1| ≤ CorrectionInitialization.ActualPrimary.slots.radius) (hv : (nativeCopy j L n k x).2.2 ∈ Set.Ioo 0 ((CorrectionInitialization.ActualPrimary.phases B N0 j).L L)) : (nativeCopy j L n k x).2 ∈ (ActualSignedGeometry.clockWindow CorrectionInitialization.ActualPrimary.slots (BaseChartJets.cellBand L)).core

theorem NavierStokes.ActualPhaseDefect.active_copy_defect_germ {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (hactive : BaseChartJets.cellBand L ∈ CorrectionInitialization.CommonWindow.levels n) (k : TorusInverse.Frequency) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hx : x ∈ (HarmonicWaveInteraction.productStrip (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion)).domain) (hp : (nativeCopy j L n k x).1 ∈ (PrimaryGeometryAssembly.domain CorrectionInitialization.ActualPrimary.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N).carrier L) (hc : (nativeCopy j L n k x).2 ∈ (ActualSignedGeometry.clockWindow CorrectionInitialization.ActualPrimary.slots (BaseChartJets.cellBand L)).core) : defect j L n =ᶠ[nhds x] fun (y : CorrectionInitialization.ActualPrimary.FullPoint) => ChartScales.epsilon CorrectionInitialization.ActualPrimary.h n * materialWeight L n * reducedExpression j L n k y

theorem NavierStokes.ActualPhaseDefect.active_copy_defect_jets {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (hactive : BaseChartJets.cellBand L ∈ CorrectionInitialization.CommonWindow.levels n) (k : TorusInverse.Frequency) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hx : x ∈ (HarmonicWaveInteraction.productStrip (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion)).domain) (hp : (nativeCopy j L n k x).1 ∈ (PrimaryGeometryAssembly.domain CorrectionInitialization.ActualPrimary.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N).carrier L) (hc : (nativeCopy j L n k x).2 ∈ (ActualSignedGeometry.clockWindow CorrectionInitialization.ActualPrimary.slots (BaseChartJets.cellBand L)).core) (m : ℕ) : iteratedFDeriv ℝ m (defect j L n) x = iteratedFDeriv ℝ m (fun (y : CorrectionInitialization.ActualPrimary.FullPoint) => ChartScales.epsilon CorrectionInitialization.ActualPrimary.h n * materialWeight L n * reducedExpression j L n k y) x

theorem NavierStokes.ActualPhaseDefect.active_materialWeight_bound {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (hactive : BaseChartJets.cellBand L ∈ CorrectionInitialization.CommonWindow.levels n) : 0 < materialWeight L n ∧ materialWeight L n ≤ materialWeightBound

Actual native jets before the copy-coordinate pullback

noncomputable def NavierStokes.ActualPhaseDefect.paddedRegion : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)

Padded region, bundling carrier, isOpen, have, coord_pos and the required compatibility proofs.

Equations

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

theorem NavierStokes.ActualPhaseDefect.padded_slow_mem {p : Slow} (hT : 0 < p.2.2) (hq : SimilarityHomogeneity.chartQ CorrectionInitialization.ActualPrimary.h p ∈ Set.Icc (1 / 2) 2) (hr : PrimaryTargetBounds.profileRadius CorrectionInitialization.ActualPrimary.h p ∈ Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)) : p ∈ BaseContextAssembly.slowCarrier CorrectionInitialization.ActualPrimary.nominal paddedRegion

noncomputable def NavierStokes.ActualPhaseDefect.reducedSlowDomain {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) : PhaseJetBounds.Domain (Fin 2 × CorrectionInitialization.ActualPrimary.Label B N0) Slow

Reduced slow domain, bundling scale, carrier, isOpen, one_le_scale.

Equations

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

noncomputable def NavierStokes.ActualPhaseDefect.reducedJetDomain {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) : PhaseJetBounds.Domain (Fin 2 × CorrectionInitialization.ActualPrimary.Label B N0) (Slow × ℝ)

Reduced jet domain, given by (reducedSlowDomain U).slot (fun i => (phases B N0 i.1).V i.2) (fun i => (phases B N0 i.1).openV i.2).

Equations

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

noncomputable def NavierStokes.ActualPhaseDefect.nativeReduced {B N0 : ℕ} (i : Fin 2 × CorrectionInitialization.ActualPrimary.Label B N0) (z : Slow × ℝ) : ℝ

Native reduced, constructed using PrimaryMaterialDefect.expression.

Equations

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

theorem NavierStokes.ActualPhaseDefect.reducedExpression_eq_native {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) (x : CorrectionInitialization.ActualPrimary.FullPoint) : reducedExpression j L n k x = nativeReduced (j, L) ((nativeCopy j L n k x).1, (nativeCopy j L n k x).2.2)

theorem NavierStokes.ActualPhaseDefect.native_reduced_polynomial {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) : PhaseJetBounds.PolynomialJets (reducedJetDomain U) nativeReduced

theorem NavierStokes.ActualPhaseDefect.native_reduced_finite_jets {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (N : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∃ (m : ℕ), ∀ (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0), JetBounds.FiniteJetBound N (nativeReduced (j, L)) ((reducedJetDomain U).carrier (j, L)) (C * ChartScales.S (BaseChartJets.cellBand L) ^ m)

theorem NavierStokes.ActualPhaseDefect.native_reduced_domain_mem {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) {p : Slow} {t : ℝ} (hp : p ∈ (PrimaryGeometryAssembly.domain CorrectionInitialization.ActualPrimary.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N).carrier L) (hs : p ∈ BaseContextAssembly.slowCarrier CorrectionInitialization.ActualPrimary.nominal U) (ht : t ∈ Set.Icc 0 ((CorrectionInitialization.ActualPrimary.phases B N0 j).L L)) : (p, t) ∈ (reducedJetDomain U).carrier (j, L)