Documentation

LeanPool.NavierStokesAndEuler.NavierStokes.ActualPhysicalPrefixFields

Physical residual fields from the literal mixed prefixes #

Local per-stage polar identities are converted to cylindrical germs. The angle-branch conversion uses the actual harmonic periodicity of the stored correction state. Exterior statements use pointwise identities on an open past sublevel, not global topological support.

Exterior identities for the actual finite physical prefixes #

The assumptions concern the primitive potential, direct velocity, and pressure stages on the genuine past exterior sublevel. Openness turns their pointwise identities into the germs needed by the spatial curl. No global support condition or final velocity identity is assumed.

noncomputable def NavierStokes.ActualExteriorPrefix.exteriorDomain (Nr : ℕ) :

Set ProblemStatement.SpaceTime

The open physical exterior on which the raw stages are constructed.

Equations

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

Instances For

theorem NavierStokes.ActualExteriorPrefix.mem_exteriorDomain {Nr : ℕ} {w : ProblemStatement.SpaceTime} :

w ∈ exteriorDomain Nr ↔ w ∈ PhysicalWaveSum.preterminal ∧ PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w < ChartScales.Q Nr ∧ w ∉ ActualPolarCoverage.active

theorem NavierStokes.ActualExteriorPrefix.exteriorDomain_open (Nr : ℕ) :

IsOpen (exteriorDomain Nr)

theorem NavierStokes.ActualExteriorPrefix.eqOn_exterior_germ {V : Type u_1} {Nr : ℕ} {f g : ProblemStatement.SpaceTime → V} (h : Set.EqOn f g (exteriorDomain Nr)) {w : ProblemStatement.SpaceTime} (hw : w ∈ exteriorDomain Nr) :

f =ᶠ[nhds w] g

Local primitive equality gives an ambient germ at every exterior point.

structure NavierStokes.ActualExteriorPrefix.ExteriorStages (B Nr : ℕ) (A D : ℕ → ProblemStatement.VelocityField) (P : ℕ → ProblemStatement.PressureField) :

Primitive stage data on the valid exterior. The direct angular field vanishes also at stage zero; the potential and pressure retain their actual slow-base stage zero.

potential_zero : Set.EqOn (A 0) (TailGaugePotential.finalPotential CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B) (exteriorDomain Nr)
potential_succ (k : ℕ) : Set.EqOn (A (k + 1)) 0 (exteriorDomain Nr)
direct_zero (k : ℕ) : Set.EqOn (D k) 0 (exteriorDomain Nr)
pressure_zero : Set.EqOn (P 0) (FinalSlowBase.pressure CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B) (exteriorDomain Nr)
pressure_succ (k : ℕ) : Set.EqOn (P (k + 1)) 0 (exteriorDomain Nr)

Instances For

theorem NavierStokes.ActualExteriorPrefix.uncutPrefix_eqOn_first {V : Type u_1} [NormedAddCommGroup V] {A : ℕ → ProblemStatement.SpaceTime → V} {f : ProblemStatement.SpaceTime → V} {U : Set ProblemStatement.SpaceTime} (h0 : Set.EqOn (A 0) f U) (h : ∀ (k : ℕ), Set.EqOn (A (k + 1)) 0 U) (J : ℕ) :

Set.EqOn (DiagonalJetBounds.uncutPrefix A (J + 1)) f U

theorem NavierStokes.ActualExteriorPrefix.uncutPrefix_eqOn_zero {V : Type u_1} [NormedAddCommGroup V] {A : ℕ → ProblemStatement.SpaceTime → V} {U : Set ProblemStatement.SpaceTime} (h : ∀ (k : ℕ), Set.EqOn (A k) 0 U) (N : ℕ) :

Set.EqOn (DiagonalJetBounds.uncutPrefix A N) 0 U

theorem NavierStokes.ActualExteriorPrefix.ExteriorStages.potential_prefix_eqOn {B Nr : ℕ} {A D : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} (H : ExteriorStages B Nr A D P) (J : ℕ) :

Set.EqOn (DiagonalJetBounds.uncutPrefix A (J + 1)) (TailGaugePotential.finalPotential CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B) (exteriorDomain Nr)

theorem NavierStokes.ActualExteriorPrefix.ExteriorStages.direct_prefix_eqOn {B Nr : ℕ} {A D : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} (H : ExteriorStages B Nr A D P) (N : ℕ) :

Set.EqOn (DiagonalJetBounds.uncutPrefix D N) 0 (exteriorDomain Nr)

theorem NavierStokes.ActualExteriorPrefix.ExteriorStages.pressure_prefix_eqOn {B Nr : ℕ} {A D : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} (H : ExteriorStages B Nr A D P) (J : ℕ) :

Set.EqOn (DiagonalJetBounds.uncutPrefix P (J + 1)) (FinalSlowBase.pressure CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B) (exteriorDomain Nr)

theorem NavierStokes.ActualExteriorPrefix.ExteriorStages.potential_prefix_germ {B Nr : ℕ} {A D : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} (H : ExteriorStages B Nr A D P) (J : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ exteriorDomain Nr) :

DiagonalJetBounds.uncutPrefix A (J + 1) =ᶠ[nhds w] TailGaugePotential.finalPotential CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B

theorem NavierStokes.ActualExteriorPrefix.ExteriorStages.velocity_prefix_eqOn {B Nr : ℕ} {A D : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} (H : ExteriorStages B Nr A D P) (J : ℕ) :

Set.EqOn (MixedDiagonalResidual.uncutVelocity A D J) (FinalSlowBase.velocity CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B) (exteriorDomain Nr)

The spatial curl sees the actual potential germ, so the finite velocity prefix agrees with the slow base without any differentiability premise on the totalized raw stages.

theorem NavierStokes.ActualExteriorPrefix.ExteriorStages.prefix_exterior {B Nr : ℕ} {A D : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} (H : ExteriorStages B Nr A D P) (J : ℕ) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w < ChartScales.Q Nr) (hout : w ∉ ActualPolarCoverage.active) :

MixedDiagonalResidual.uncutVelocity A D J w = FinalSlowBase.velocity CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B w ∧ DiagonalJetBounds.uncutPrefix P (J + 1) w = FinalSlowBase.pressure CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B w

The exterior part of the physical realization required for each finite cycle follows solely from the primitive stage identities.

@[reducible, inline]

abbrev NavierStokes.ActualPhysicalPrefixFields.Point :

Point: an abbreviation for PhysicalMeanJetBounds.Point.

Equations

NavierStokes.ActualPhysicalPrefixFields.Point = NavierStokes.PhysicalMeanJetBounds.Point

Instances For

@[reducible, inline]

abbrev NavierStokes.ActualPhysicalPrefixFields.Cylinder :

Cylinder: an abbreviation for PhysicalResidualBridge.Cylinder.

Equations

NavierStokes.ActualPhysicalPrefixFields.Cylinder = NavierStokes.PhysicalResidualBridge.Cylinder

Instances For

@[reducible, inline]

abbrev NavierStokes.ActualPhysicalPrefixFields.ScaledGraph :

Scaled graph: an abbreviation for PhysicalResidualBridge.ScaledGraph.

Equations

NavierStokes.ActualPhysicalPrefixFields.ScaledGraph = NavierStokes.PhysicalResidualBridge.ScaledGraph

Instances For

noncomputable def NavierStokes.ActualPhysicalPrefixFields.forward (z : ProblemStatement.SpaceTime) :

ProblemStatement.SpaceTime

Forward, given by (z.1, CylindricalResidual.chart z.2).

Equations

NavierStokes.ActualPhysicalPrefixFields.forward z = (z.1, NavierStokes.CylindricalResidual.chart z.2)

Instances For

theorem NavierStokes.ActualPhysicalPrefixFields.forward_smooth :

ContDiff ℝ (↑⊤) forward

noncomputable def NavierStokes.ActualPhysicalPrefixFields.replaceAngle (z : ProblemStatement.SpaceTime) (theta : ℝ) :

ProblemStatement.SpaceTime

Replace angle, given by (z.1, AxisymmetricResidual.pack (z.2 0) theta (z.2 2)).

Equations

NavierStokes.ActualPhysicalPrefixFields.replaceAngle z theta = (z.1, NavierStokes.AxisymmetricResidual.pack (z.2.ofLp 0) theta (z.2.ofLp 2))

Instances For

@[simp]

theorem NavierStokes.ActualPhysicalPrefixFields.replaceAngle_self (z : ProblemStatement.SpaceTime) :

replaceAngle z (z.2.ofLp 1) = z

def NavierStokes.ActualPhysicalPrefixFields.AngularPeriodic {E : Type u_1} (f : ProblemStatement.SpaceTime → E) :

Angular periodic, given by ∀ z, Function.Periodic (fun theta => f (replaceAngle z theta)) (2 * Real.pi).

Equations

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

Instances For

theorem NavierStokes.ActualPhysicalPrefixFields.periodic_eq_of_cos_sin {E : Type u_1} {f : ℝ → E} (hf : Function.Periodic f (2 * Real.pi)) {alpha beta : ℝ} (hc : Real.cos alpha = Real.cos beta) (hs : Real.sin alpha = Real.sin beta) :

f alpha = f beta

theorem NavierStokes.ActualPhysicalPrefixFields.polarCoordinates_shape {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {z : ProblemStatement.SpaceTime} (hr : 0 < z.2.ofLp 0) (hc : forward z ∈ ActualMeanPotentialRealization.cartesianDomain a i) :

PhysicalCurlCovariance.polarCoordinates a i (forward z) = replaceAngle z (PhysicalCurlCovariance.polarInput a i (forward z)).2

theorem NavierStokes.ActualPhysicalPrefixFields.polarInput_cos_sin {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {z : ProblemStatement.SpaceTime} (hr : 0 < z.2.ofLp 0) (hc : forward z ∈ ActualMeanPotentialRealization.cartesianDomain a i) :

Real.cos (PhysicalCurlCovariance.polarInput a i (forward z)).2 = Real.cos (z.2.ofLp 1) ∧ Real.sin (PhysicalCurlCovariance.polarInput a i (forward z)).2 = Real.sin (z.2.ofLp 1)

theorem NavierStokes.ActualPhysicalPrefixFields.polarPressure_forward {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {f : ProblemStatement.PressureField} (hf : AngularPeriodic f) {z : ProblemStatement.SpaceTime} (hr : 0 < z.2.ofLp 0) (hc : forward z ∈ ActualMeanPotentialRealization.cartesianDomain a i) :

(CyclePhysicalPrefixes.polarPressureMap a i) f (forward z) = f z

theorem NavierStokes.ActualPhysicalPrefixFields.polarVelocity_forward {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {f : ProblemStatement.VelocityField} (hf : AngularPeriodic f) {z : ProblemStatement.SpaceTime} (hr : 0 < z.2.ofLp 0) (hc : forward z ∈ ActualMeanPotentialRealization.cartesianDomain a i) :

(CyclePhysicalPrefixes.polarVelocityMap a i) f (forward z) = (CylindricalResidual.frame (z.2.ofLp 1)) (f z)

theorem NavierStokes.ActualPhysicalPrefixFields.velocity_pullback_germ {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {u f : ProblemStatement.VelocityField} (hf : AngularPeriodic f) {V : Set ProblemStatement.SpaceTime} (hV : IsOpen V) (hu : Set.EqOn u ((CyclePhysicalPrefixes.polarVelocityMap a i) f) V) {z : ProblemStatement.SpaceTime} (hr : 0 < z.2.ofLp 0) (hz : forward z ∈ V) (hc : forward z ∈ ActualMeanPotentialRealization.cartesianDomain a i) :

u ∘ forward =ᶠ[nhds z] fun (y : ProblemStatement.SpaceTime) => (CylindricalResidual.frame (y.2.ofLp 1)) (f y)

theorem NavierStokes.ActualPhysicalPrefixFields.pressure_pullback_germ {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {P f : ProblemStatement.PressureField} (hf : AngularPeriodic f) {V : Set ProblemStatement.SpaceTime} (hV : IsOpen V) (hP : Set.EqOn P ((CyclePhysicalPrefixes.polarPressureMap a i) f) V) {z : ProblemStatement.SpaceTime} (hr : 0 < z.2.ofLp 0) (hz : forward z ∈ V) (hc : forward z ∈ ActualMeanPotentialRealization.cartesianDomain a i) :

CylindricalResidual.pressurePullback P =ᶠ[nhds z] f

Periodicity comes from the stored harmonic representation #

theorem NavierStokes.ActualPhysicalPrefixFields.represented_oscillation_periodic {ι : Type} {v : CorrectionStep.CycleCoefficients ι} {s : CorrectionState.State Point} {axis : CorrectionStep.AxisymmetricAlias} (H : CorrectionStep.CycleRepresentation v s axis) (n : ℕ) (x : Point) (j : Fin 3) :

Function.Periodic (fun (theta : ℝ) => s.oscillation n (x, theta) j) (2 * Real.pi)

theorem NavierStokes.ActualPhysicalPrefixFields.represented_pressure_periodic {ι : Type} {v : CorrectionStep.CycleCoefficients ι} {s : CorrectionState.State Point} {axis : CorrectionStep.AxisymmetricAlias} (H : CorrectionStep.CycleRepresentation v s axis) (n : ℕ) (x : Point) :

Function.Periodic (fun (theta : ℝ) => s.oscillatoryPressure n (x, theta)) (2 * Real.pi)

theorem NavierStokes.ActualPhysicalPrefixFields.represented_components_periodic {ι : Type} {v : CorrectionStep.CycleCoefficients ι} {s : CorrectionState.State Point} {axis : CorrectionStep.AxisymmetricAlias} (H : CorrectionStep.CycleRepresentation v s axis) (c : CorrectionState.Context Point) (n : ℕ) (x : Point) :

Function.Periodic (fun (theta : ℝ) => (PhysicalResidualBridge.baseComponents c n + PhysicalResidualBridge.incrementComponents s n) (x, theta)) (2 * Real.pi)

theorem NavierStokes.ActualPhysicalPrefixFields.represented_totalPressure_periodic {ι : Type} {v : CorrectionStep.CycleCoefficients ι} {s : CorrectionState.State Point} {axis : CorrectionStep.AxisymmetricAlias} (H : CorrectionStep.CycleRepresentation v s axis) (n : ℕ) (x : Point) :

Function.Periodic (fun (theta : ℝ) => s.totalPressureIncrement n (x, theta)) (2 * Real.pi)

theorem NavierStokes.ActualPhysicalPrefixFields.graphMapTZ_replaceAngle (G : ScaledGraph) (z : ProblemStatement.SpaceTime) (theta : ℝ) :

PhysicalResidualTZ.graphMapTZ G (replaceAngle z theta) = ((PhysicalResidualTZ.graphMapTZ G z).1, theta)

theorem NavierStokes.ActualPhysicalPrefixFields.velocityTZ_periodic (G : ScaledGraph) (a : Cylinder → Fin 3 → ℝ) (ha : ∀ (x : Point), Function.Periodic (fun (theta : ℝ) => a (x, theta)) (2 * Real.pi)) :

AngularPeriodic (PhysicalResidualTZ.velocityTZ G a)

theorem NavierStokes.ActualPhysicalPrefixFields.pressureTZ_periodic (G : ScaledGraph) (a : Cylinder → ℝ) (ha : ∀ (x : Point), Function.Periodic (fun (theta : ℝ) => a (x, theta)) (2 * Real.pi)) :

AngularPeriodic (PhysicalResidualTZ.pressureTZ G a)

Actual finite prefixes retain local stage agreement #

theorem NavierStokes.ActualPhysicalPrefixFields.uncutPrefix_eqOn {E : Type u_1} [NormedAddCommGroup E] {V : Set ProblemStatement.SpaceTime} {f g : ℕ → ProblemStatement.SpaceTime → E} (hf : ∀ (k : ℕ), Set.EqOn (f k) (g k) V) (J : ℕ) :

Set.EqOn (DiagonalJetBounds.uncutPrefix f J) (DiagonalJetBounds.uncutPrefix g J) V

theorem NavierStokes.ActualPhysicalPrefixFields.mixedVelocity_eqOn {ι : Type} (p : ℕ → CorrectionStep.CycleParameters ι) (c : CorrectionState.Context Point) (seed : CorrectionStep.CycleState ι) (a : ℝ) (i : PolarCharts.Index) (G : ScaledGraph) (n : ℕ) {V : Set ProblemStatement.SpaceTime} (hV : IsOpen V) (A D : ℕ → ProblemStatement.VelocityField) (hA : ∀ (k : ℕ), DifferentiableOn ℝ (A k) V) (hc : ∀ (k : ℕ), Set.EqOn (SpatialCurl.spatialCurl (A k)) (CyclePhysicalPrefixes.potentialParts p c seed a i G n k) V) (hD : ∀ (k : ℕ), Set.EqOn (D k) (CyclePhysicalPrefixes.directStages p c seed a i G n k) V) (J : ℕ) :

Set.EqOn (MixedDiagonalResidual.uncutVelocity A D J) (CyclePhysicalPrefixes.velocity a i G n c (CorrectionStep.CycleState.iterate p c seed J).state) V

theorem NavierStokes.ActualPhysicalPrefixFields.pressurePrefix_eqOn {ι : Type} (p : ℕ → CorrectionStep.CycleParameters ι) (c : CorrectionState.Context Point) (seed : CorrectionStep.CycleState ι) (a : ℝ) (i : PolarCharts.Index) (G : ScaledGraph) (n : ℕ) (p0 : Cylinder → ℝ) {V : Set ProblemStatement.SpaceTime} (P : ℕ → ProblemStatement.PressureField) (hP : ∀ (k : ℕ), Set.EqOn (P k) (CyclePhysicalPrefixes.pressureStages p c seed a i G n p0 k) V) (J : ℕ) :

Set.EqOn (DiagonalJetBounds.uncutPrefix P (J + 1)) (CyclePhysicalPrefixes.pressure a i G n p0 (CorrectionStep.CycleState.iterate p c seed J).state) V

Open valid charts and the honest residual floor #

theorem NavierStokes.ActualPhysicalPrefixFields.graphSource_open (G : ScaledGraph) (hl : 0 < G.radialScale) {U : Set Cylinder} (hU : IsOpen U) :

IsOpen (PhysicalResidualTZ.graphSourceTZ G U)

theorem NavierStokes.ActualPhysicalPrefixFields.exists_cartesianChart {z : ProblemStatement.SpaceTime} (hr : 0 < z.2.ofLp 0) :

∃ (a : ℝ), 0 < a ∧ ∃ (i : PolarCharts.Index), forward z ∈ ActualMeanPotentialRealization.cartesianDomain a i

noncomputable def NavierStokes.ActualPhysicalPrefixFields.source (n : ℕ) :

Set ProblemStatement.SpaceTime

Source, given by PhysicalResidualTZ.graphSourceTZ (ActualCycleResidualBounds.actualBandGraph n) ActualPolarCoverage.nativeDomain.

Equations

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

Instances For

noncomputable def NavierStokes.ActualPhysicalPrefixFields.cartesianChartDomain (qbig : ℝ) (n : ℕ) (a : ℝ) (i : PolarCharts.Index) :

Set ProblemStatement.SpaceTime

Cartesian chart domain, constructed using CutStageEstimates.physicalSublevel.

Equations

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

Instances For

theorem NavierStokes.ActualPhysicalPrefixFields.source_open (n : ℕ) :

IsOpen (source n)

theorem NavierStokes.ActualPhysicalPrefixFields.cartesianChartDomain_open (qbig : ℝ) (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) :

IsOpen (cartesianChartDomain qbig n a i)

theorem NavierStokes.ActualPhysicalPrefixFields.source_q_lt (n : ℕ) {z : ProblemStatement.SpaceTime} (ht : z ∈ PhysicalWaveSum.preterminal) (hz : z ∈ source n) :

PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h (forward z) < 2 * ChartScales.Q n

theorem NavierStokes.ActualPhysicalPrefixFields.source_sublevel {Nr : ℕ} {qbig : ℝ} (hfloor : 2 * ChartScales.Q Nr ≤ qbig) {n : ℕ} (hn : Nr ≤ n) {z : ProblemStatement.SpaceTime} (ht : z ∈ PhysicalWaveSum.preterminal) (hz : z ∈ source n) :

forward z ∈ CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig

theorem NavierStokes.ActualPhysicalPrefixFields.source_polarCoordinates {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) (n : ℕ) {z : ProblemStatement.SpaceTime} (hz : z ∈ source n) (hc : forward z ∈ ActualMeanPotentialRealization.cartesianDomain a i) :

PhysicalCurlCovariance.polarCoordinates a i (forward z) ∈ source n

theorem NavierStokes.ActualPhysicalPrefixFields.exists_validChart {Nr : ℕ} {qbig : ℝ} (hfloor : 2 * ChartScales.Q Nr ≤ qbig) {n : ℕ} (hn : Nr ≤ n) {z : ProblemStatement.SpaceTime} (ht : z ∈ PhysicalWaveSum.preterminal) (hz : z ∈ source n) :

∃ (a : ℝ), 0 < a ∧ ∃ (i : PolarCharts.Index), forward z ∈ cartesianChartDomain qbig n a i

theorem NavierStokes.ActualPhysicalPrefixFields.actual_pressure_periodic {ι : Type} {v : CorrectionStep.CycleCoefficients ι} {s : CorrectionState.State Point} {axis : CorrectionStep.AxisymmetricAlias} (H : CorrectionStep.CycleRepresentation v s axis) (B n : ℕ) (x : Point) :

Function.Periodic (fun (theta : ℝ) => (ActualCycleResidualBounds.actualBasePressure B n + s.totalPressureIncrement n) (x, theta)) (2 * Real.pi)

structure NavierStokes.ActualPhysicalPrefixFields.StageRealizations (B N0 Nr : ℕ) (p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)) (qbig : ℝ) (A D : ℕ → ProblemStatement.VelocityField) (P : ℕ → ProblemStatement.PressureField) :

Every input is an individual stage agreement on its concrete valid polar chart. No finite-prefix or germ equality is a field of this record.

potential (n : ℕ) : Nr ≤ n → ∀ (a : ℝ), 0 < a → ∀ (i : PolarCharts.Index) (k : ℕ), Set.EqOn (SpatialCurl.spatialCurl (A k)) (CyclePhysicalPrefixes.potentialParts p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) a i (ActualCycleResidualBounds.actualBandGraph n) n k) (cartesianChartDomain qbig n a i)
direct (n : ℕ) : Nr ≤ n → ∀ (a : ℝ), 0 < a → ∀ (i : PolarCharts.Index) (k : ℕ), Set.EqOn (D k) (CyclePhysicalPrefixes.directStages p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) a i (ActualCycleResidualBounds.actualBandGraph n) n k) (cartesianChartDomain qbig n a i)
pressure (n : ℕ) : Nr ≤ n → ∀ (a : ℝ), 0 < a → ∀ (i : PolarCharts.Index) (k : ℕ), Set.EqOn (P k) (CyclePhysicalPrefixes.pressureStages p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) a i (ActualCycleResidualBounds.actualBandGraph n) n (ActualCycleResidualBounds.actualBasePressure B n) k) (cartesianChartDomain qbig n a i)

Instances For

theorem NavierStokes.ActualPhysicalPrefixFields.StageRealizations.velocity_prefix {B N0 Nr : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} {qbig : ℝ} {A D : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} (H : StageRealizations B N0 Nr p qbig A D P) (hA : ∀ (k : ℕ), ContDiffOn ℝ (↑⊤) (A k) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)) (n : ℕ) (hn : Nr ≤ n) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) (J : ℕ) :

Set.EqOn (MixedDiagonalResidual.uncutVelocity A D J) (CyclePhysicalPrefixes.velocity a i (ActualCycleResidualBounds.actualBandGraph n) n (CorrectionInitialization.ActualPrimary.commonContext B) (CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) J).state) (cartesianChartDomain qbig n a i)

theorem NavierStokes.ActualPhysicalPrefixFields.StageRealizations.pressure_prefix {B N0 Nr : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} {qbig : ℝ} {A D : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} (H : StageRealizations B N0 Nr p qbig A D P) (n : ℕ) (hn : Nr ≤ n) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) (J : ℕ) :

Set.EqOn (DiagonalJetBounds.uncutPrefix P (J + 1)) (CyclePhysicalPrefixes.pressure a i (ActualCycleResidualBounds.actualBandGraph n) n (ActualCycleResidualBounds.actualBasePressure B n) (CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) J).state) (cartesianChartDomain qbig n a i)

theorem NavierStokes.ActualPhysicalPrefixFields.StageRealizations.velocity_germ {B N0 Nr : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} {qbig : ℝ} {A D : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} (H : StageRealizations B N0 Nr p qbig A D P) (hfloor : 2 * ChartScales.Q Nr ≤ qbig) (hA : ∀ (k : ℕ), ContDiffOn ℝ (↑⊤) (A k) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)) (J : ℕ) (Hrep : CorrectionStep.CycleRepresentation (CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) J).coefficients (CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) J).state (CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) J).axisymmetricAlias) (n : ℕ) (hn : Nr ≤ n) {z : ProblemStatement.SpaceTime} (ht : z ∈ PhysicalWaveSum.preterminal) (hz : z ∈ source n) :

(fun (y : ProblemStatement.SpaceTime) => MixedDiagonalResidual.uncutVelocity A D J (y.1, CylindricalResidual.chart y.2)) =ᶠ[nhds z] fun (y : ProblemStatement.SpaceTime) => (CylindricalResidual.frame (y.2.ofLp 1)) (PhysicalResidualTZ.velocityTZ (ActualCycleResidualBounds.actualBandGraph n) (fun (v : PhysicalResidualTZ.Cylinder) (i : Fin 3) => PhysicalResidualBridge.baseComponents (CorrectionInitialization.ActualPrimary.commonContext B) n v i + PhysicalResidualBridge.incrementComponents (CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) J).state n v i) y)

theorem NavierStokes.ActualPhysicalPrefixFields.StageRealizations.pressure_germ {B N0 Nr : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} {qbig : ℝ} {A D : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} (H : StageRealizations B N0 Nr p qbig A D P) (hfloor : 2 * ChartScales.Q Nr ≤ qbig) (J : ℕ) (Hrep : CorrectionStep.CycleRepresentation (CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) J).coefficients (CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) J).state (CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) J).axisymmetricAlias) (n : ℕ) (hn : Nr ≤ n) {z : ProblemStatement.SpaceTime} (ht : z ∈ PhysicalWaveSum.preterminal) (hz : z ∈ source n) :

CylindricalResidual.pressurePullback (DiagonalJetBounds.uncutPrefix P (J + 1)) =ᶠ[nhds z] PhysicalResidualTZ.pressureTZ (ActualCycleResidualBounds.actualBandGraph n) fun (v : PhysicalResidualTZ.Cylinder) => ActualCycleResidualBounds.actualBasePressure B n v + (CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) J).state.totalPressureIncrement n v

All five physical-field obligations for the same literal prefix #

theorem NavierStokes.ActualPhysicalPrefixFields.physicalFields_of_stages {B N0 Nr : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} {qbig : ℝ} {A D : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} (H : StageRealizations B N0 Nr p qbig A D P) (HE : ActualExteriorPrefix.ExteriorStages B Nr A D P) (hfloor : 2 * ChartScales.Q Nr ≤ qbig) (hA : ∀ (k : ℕ), ContDiffOn ℝ (↑⊤) (A k) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)) (hD : ∀ (k : ℕ), ContDiffOn ℝ (↑⊤) (D k) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)) (hP : ∀ (k : ℕ), ContDiffOn ℝ (↑⊤) (P k) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)) (J : ℕ) (Hrep : CorrectionStep.CycleRepresentation (CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) J).coefficients (CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) J).state (CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) J).axisymmetricAlias) :

ActualCycleResidualBounds.PhysicalData B Nr (CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) J).state (MixedDiagonalResidual.uncutVelocity A D J) (DiagonalJetBounds.uncutPrefix P (J + 1))

theorem NavierStokes.ActualPhysicalPrefixFields.physicalFields_all {B N0 Nr : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} {qbig : ℝ} {A D : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} (H : StageRealizations B N0 Nr p qbig A D P) (HE : ActualExteriorPrefix.ExteriorStages B Nr A D P) (hfloor : 2 * ChartScales.Q Nr ≤ qbig) (hA : ∀ (k : ℕ), ContDiffOn ℝ (↑⊤) (A k) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)) (hD : ∀ (k : ℕ), ContDiffOn ℝ (↑⊤) (D k) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)) (hP : ∀ (k : ℕ), ContDiffOn ℝ (↑⊤) (P k) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)) (Hrep : ∀ (J : ℕ), CorrectionStep.CycleRepresentation (CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) J).coefficients (CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) J).state (CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) J).axisymmetricAlias) (J : ℕ) :

ActualCycleResidualBounds.PhysicalData B Nr (CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) J).state (MixedDiagonalResidual.uncutVelocity A D J) (DiagonalJetBounds.uncutPrefix P (J + 1))

The actual residual-rate consumer can use this family without reprovisioning any cylindrical germs or exterior prefix identities.