Literal physical data for the actual candidate

The initial fields use the same primary choice and the same initialized mean state as ActualCandidateConstruction. Their support, smoothness, and axis germs are derived from those constructors.

The same initialized correction sequence and its physical prefixes

Every state below comes from the actual initialized primary choice and the fixed actual cycle parameters. The finite labels, phase carriers, base error, and current pressure alias are retained through the literal recurrence.

@[reducible, inline]

abbrev NavierStokes.ActualCandidateConstruction.Index (B N0 : ℕ) : Type

Index: an abbreviation for ActualInitialization.Index.

Equations

• NavierStokes.ActualCandidateConstruction.Index = NavierStokes.ActualInitialization.Index

@[reducible, inline]

abbrev NavierStokes.ActualCandidateConstruction.Point : Type

Point: an abbreviation for CorrectionStep.CyclePoint.

Equations

• NavierStokes.ActualCandidateConstruction.Point = NavierStokes.CorrectionStep.CyclePoint

@[reducible, inline]

abbrev NavierStokes.ActualCandidateConstruction.Full : Type

Full: an abbreviation for Point × ℝ.

Equations

• NavierStokes.ActualCandidateConstruction.Full = (NavierStokes.ActualCandidateConstruction.Point × ℝ)

noncomputable def NavierStokes.ActualCandidateConstruction.parameters (B N0 : ℕ) : CorrectionStep.CycleParameters (Index B N0)

Parameters, given by ActualCycleParameters.fixedParameters B N0.

Equations

• NavierStokes.ActualCandidateConstruction.parameters B N0 = NavierStokes.ActualCycleParameters.fixedParameters B N0

noncomputable def NavierStokes.ActualCandidateConstruction.parameterSequence (B N0 a✝ : ℕ) : CorrectionStep.CycleParameters (Index B N0)

Parameter sequence, defined pointwise by parameters B N0.

Equations

• NavierStokes.ActualCandidateConstruction.parameterSequence B N0 x✝ = NavierStokes.ActualCandidateConstruction.parameters B N0

noncomputable def NavierStokes.ActualCandidateConstruction.cycle (B N0 a✝ : ℕ) : CorrectionStep.CycleState (Index B N0)

Cycle, given by CycleState.iterate (parameterSequence B N0) (commonContext B) (ActualInitialization.initialCycleState B N0).

Equations

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

@[simp]

theorem NavierStokes.ActualCandidateConstruction.cycle_zero (B N0 : ℕ) : cycle B N0 0 = ActualInitialization.initialCycleState B N0

theorem NavierStokes.ActualCandidateConstruction.cycle_succ (B N0 j : ℕ) : cycle B N0 (j + 1) = CorrectionStep.CycleState.step (parameters B N0) (CorrectionInitialization.ActualPrimary.commonContext B) (cycle B N0 j)

theorem NavierStokes.ActualCandidateConstruction.cycle_labels (B N0 j : ℕ) : (cycle B N0 j).coefficients.labels = CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0

theorem NavierStokes.ActualCandidateConstruction.cycle_aliasCoefficients (B N0 j : ℕ) : (cycle B N0 j).coefficients.aliasCoefficients = fun (x : Index B N0) => 0

theorem NavierStokes.ActualCandidateConstruction.cycle_carrier (B N0 j : ℕ) (l : Index B N0) : CorrectionStep.SameCarrier ((cycle B N0 j).coefficients.blocks l) (ActualInitialization.tangentBlock l)

theorem NavierStokes.ActualCandidateConstruction.current_parameters (B N0 j : ℕ) : ActualCycleParameters.parameters (cycle B N0 j) = parameters B N0

Recomputing the actual constructor at this state selects precisely the fixed parameters used by the recurrence.

theorem NavierStokes.ActualCandidateConstruction.cycle_signed_carrier (B N0 j : ℕ) (l : Index B N0) : CorrectionStep.SameCarrier ((cycle B N0 j).coefficients.blocks l) ((parameters B N0).signedBlock (cycle B N0 j).coefficients (CorrectionInitialization.ActualPrimary.commonContext B) (cycle B N0 j).state l)

theorem NavierStokes.ActualCandidateConstruction.cycle_representation (B N0 j : ℕ) : CorrectionStep.CycleRepresentation (cycle B N0 j).coefficients (cycle B N0 j).state (cycle B N0 j).axisymmetricAlias

theorem NavierStokes.ActualCandidateConstruction.cycle_coefficientBands (B N0 j : ℕ) : CorrectionStep.CoefficientBands (cycle B N0 j).coefficients

theorem NavierStokes.ActualCandidateConstruction.cycle_residualBand (B N0 j : ℕ) : (cycle B N0 j).coefficients.residualBand = 2 ^ (j + 1)

theorem NavierStokes.ActualCandidateConstruction.cycle_base_error (B N0 j : ℕ) : (cycle B N0 j).state.errors.base = ActualInitialization.baseError B

theorem NavierStokes.ActualCandidateConstruction.cycle_reconstructed (B N0 j : ℕ) : (VariableGaugeMean.reconstructState CorrectionInitialization.ActualPrimary.commonGauge (CorrectionInitialization.ActualPrimary.commonContext B) (cycle B N0 j).state).pressure = (cycle B N0 j).state.pressure

noncomputable def NavierStokes.ActualCandidateConstruction.initialTemporalAlias (B N0 : ℕ) : CorrectionState.Oscillation Point

Initial temporal alias, constructed using VariableGaugeMean.temporalAliasState.

Equations

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

noncomputable def NavierStokes.ActualCandidateConstruction.temporalAlias (B N0 j : ℕ) : CorrectionState.Oscillation Point

Temporal alias, given by CycleStateCoherence.temporalAliasAt (parameterSequence B N0) (commonContext B) (ActualInitialization.initialCycleState B N0) j.

Equations

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

theorem NavierStokes.ActualCandidateConstruction.cycle_alias_error (B N0 J : ℕ) : (cycle B N0 J).state.errors.aliasError = initialTemporalAlias B N0 + ∑ j ∈ Finset.range J, temporalAlias B N0 j + VariableGaugeMean.pressureAliasState CorrectionInitialization.ActualPrimary.commonGauge (CorrectionInitialization.ActualPrimary.commonContext B) (cycle B N0 J).state

Every earlier temporal alias and exactly the current pressure alias remain present, with the signs inherited from the actual state updates.

noncomputable def NavierStokes.ActualCandidateConstruction.firstBand (B N0 : ℕ) : ℕ

One positive band floor is retained for every physical stage.

Equations

• NavierStokes.ActualCandidateConstruction.firstBand B N0 = max 4 (NavierStokes.ActualCycleParameters.bandFloor B N0)

theorem NavierStokes.ActualCandidateConstruction.firstBand_four (B N0 : ℕ) : 4 ≤ firstBand B N0

theorem NavierStokes.ActualCandidateConstruction.firstBand_pos (B N0 : ℕ) : 1 ≤ firstBand B N0

theorem NavierStokes.ActualCandidateConstruction.firstBand_ge_choice (B N0 : ℕ) : ActualCycleParameters.bandFloor B N0 ≤ firstBand B N0

theorem NavierStokes.ActualCandidateConstruction.firstBand_ge (B N0 : ℕ) : N0 ≤ firstBand B N0

noncomputable def NavierStokes.ActualCandidateConstruction.qbig (B N0 : ℕ) : ℝ

Qbig, given by ChartScales.Q (firstBand B N0).

Equations

• NavierStokes.ActualCandidateConstruction.qbig B N0 = NavierStokes.ChartScales.Q (NavierStokes.ActualCandidateConstruction.firstBand B N0)

theorem NavierStokes.ActualCandidateConstruction.qbig_pos (B N0 : ℕ) : 0 < qbig B N0

theorem NavierStokes.ActualCandidateConstruction.qbig_le_choice (B N0 : ℕ) : qbig B N0 ≤ ChartScales.Q (ActualCycleParameters.bandFloor B N0)

noncomputable def NavierStokes.ActualCandidateConstruction.residualBand (B N0 : ℕ) : ℕ

One extra comparison band keeps every native point with q/Q < 2 inside the original raw field's validity domain.

Equations

• NavierStokes.ActualCandidateConstruction.residualBand B N0 = NavierStokes.ActualCandidateConstruction.firstBand B N0 + 1

theorem NavierStokes.ActualCandidateConstruction.residualBand_four (B N0 : ℕ) : 4 ≤ residualBand B N0

theorem NavierStokes.ActualCandidateConstruction.firstBand_le_residualBand (B N0 : ℕ) : firstBand B N0 ≤ residualBand B N0

theorem NavierStokes.ActualCandidateConstruction.twice_residual_scale (B N0 : ℕ) : 2 * ChartScales.Q (residualBand B N0) = qbig B N0

theorem NavierStokes.ActualCandidateConstruction.nativeScale_lt_qbig (B N0 n : ℕ) (hn : residualBand B N0 ≤ n) {r : ℝ} (hr : r < 2) : ChartScales.Q n * r < qbig B N0

noncomputable def NavierStokes.ActualCandidateConstruction.physicalDomain (B N0 : ℕ) : Set ProblemStatement.SpaceTime

Physical domain, given by CutStageEstimates.physicalSublevel h (qbig B N0).

Equations

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

theorem NavierStokes.ActualCandidateConstruction.physicalDomain_open (B N0 : ℕ) : IsOpen (physicalDomain B N0)

theorem NavierStokes.ActualCandidateConstruction.initial_invariant (B N0 : ℕ) : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope ActualInitialization.labelCarrier (ActualIterationLedger.sigma 0) (cycle B N0 0)

One selected initialization

noncomputable def NavierStokes.ActualCandidateConstruction.selectedBudget : ℕ

Selected budget, given by 0.

Equations

• NavierStokes.ActualCandidateConstruction.selectedBudget = 0

noncomputable def NavierStokes.ActualCandidateConstruction.selectedThreshold : ℕ

Selected threshold, given by ActualCarrierGeometry.startingThreshold 0.

Equations

• NavierStokes.ActualCandidateConstruction.selectedThreshold = NavierStokes.ActualCarrierGeometry.startingThreshold 0

theorem NavierStokes.ActualCandidateConstruction.selectedThreshold_geometry : ActualCarrierGeometry.geometricThreshold ≤ selectedThreshold

noncomputable def NavierStokes.ActualCandidateConstruction.selectedCycle : ℕ → CorrectionStep.CycleState (Index selectedBudget selectedThreshold)

Selected cycle, given by cycle selectedBudget selectedThreshold.

Equations

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

noncomputable def NavierStokes.ActualCandidateConstruction.selectedQbig : ℝ

Selected qbig, given by qbig selectedBudget selectedThreshold.

Equations

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

theorem NavierStokes.ActualCandidateConstruction.selectedQbig_pos : 0 < selectedQbig

theorem NavierStokes.ActualCandidateConstruction.selected_initial_invariant : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext selectedBudget) ActualInitialization.tangentBlock ActualInitialization.envelope ActualInitialization.labelCarrier (ActualIterationLedger.sigma 0) (selectedCycle 0)

theorem NavierStokes.ActualCandidateConstruction.selected_initial_meanHypotheses : LiftedMeanResidual.MeanHypotheses ActualInitialMeanEquation.strip.domain (CorrectionInitialization.ActualPrimary.commonContext selectedBudget) (selectedCycle 0).state

Exact finite physical prefixes in any valid polar chart

noncomputable def NavierStokes.ActualCandidateConstruction.graph (n : ℕ) : PhysicalResidualBridge.ScaledGraph

Graph, given by PhysicalResidualBridge.commonGraph (ChartScales.Q n) h (CorrectionInitialization.CommonWindow.index h n).

Equations

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

noncomputable def NavierStokes.ActualCandidateConstruction.basePressure (B n : ℕ) : Full → ℝ

Base pressure, given by ActualBaseResidual.basePressure certificate modulation upper B n.

Equations

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

noncomputable def NavierStokes.ActualCandidateConstruction.chartVelocity (B N0 : ℕ) (a : ℝ) (i : PolarCharts.Index) (n j : ℕ) : ProblemStatement.VelocityField

Chart velocity, given by CyclePhysicalPrefixes.velocity a i (graph n) n (commonContext B) (cycle B N0 j).state.

Equations

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

noncomputable def NavierStokes.ActualCandidateConstruction.chartPressure (B N0 : ℕ) (a : ℝ) (i : PolarCharts.Index) (n j : ℕ) : ProblemStatement.PressureField

Chart pressure, given by CyclePhysicalPrefixes.pressure a i (graph n) n (basePressure B n) (cycle B N0 j).state.

Equations

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

noncomputable def NavierStokes.ActualCandidateConstruction.chartVelocityStages (B N0 : ℕ) (a : ℝ) (i : PolarCharts.Index) (n : ℕ) : ℕ → ProblemStatement.VelocityField

Chart velocity stages, constructed using CyclePhysicalPrefixes.velocityStages.

Equations

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

noncomputable def NavierStokes.ActualCandidateConstruction.chartPressureStages (B N0 : ℕ) (a : ℝ) (i : PolarCharts.Index) (n : ℕ) : ℕ → ProblemStatement.PressureField

Chart pressure stages, constructed using CyclePhysicalPrefixes.pressureStages.

Equations

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

noncomputable def NavierStokes.ActualCandidateConstruction.chartPotentialParts (B N0 : ℕ) (a : ℝ) (i : PolarCharts.Index) (n : ℕ) : ℕ → ProblemStatement.VelocityField

Chart potential parts, constructed using CyclePhysicalPrefixes.potentialParts.

Equations

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

noncomputable def NavierStokes.ActualCandidateConstruction.chartDirectStages (B N0 : ℕ) (a : ℝ) (i : PolarCharts.Index) (n : ℕ) : ℕ → ProblemStatement.VelocityField

Chart direct stages, constructed using CyclePhysicalPrefixes.directStages.

Equations

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

theorem NavierStokes.ActualCandidateConstruction.chart_velocity_prefix (B N0 : ℕ) (a : ℝ) (i : PolarCharts.Index) (n J : ℕ) : DiagonalJetBounds.uncutPrefix (chartVelocityStages B N0 a i n) (J + 1) = chartVelocity B N0 a i n J

theorem NavierStokes.ActualCandidateConstruction.chart_pressure_prefix (B N0 : ℕ) (a : ℝ) (i : PolarCharts.Index) (n J : ℕ) : DiagonalJetBounds.uncutPrefix (chartPressureStages B N0 a i n) (J + 1) = chartPressure B N0 a i n J

theorem NavierStokes.ActualCandidateConstruction.chart_velocity_split (B N0 : ℕ) (a : ℝ) (i : PolarCharts.Index) (n j : ℕ) : chartVelocityStages B N0 a i n j = chartPotentialParts B N0 a i n j + chartDirectStages B N0 a i n j

The global physical representatives need only agree with an individual chart on its open validity set. Finite summation and the genuine residual preserve precisely this local agreement.

theorem NavierStokes.ActualCandidateConstruction.uncutPrefix_eqOn {V : Type u_1} [NormedAddCommGroup V] {U : Set ProblemStatement.SpaceTime} {f g : ℕ → ProblemStatement.SpaceTime → V} (hf : ∀ (j : ℕ), Set.EqOn (f j) (g j) U) (N : ℕ) : Set.EqOn (DiagonalJetBounds.uncutPrefix f N) (DiagonalJetBounds.uncutPrefix g N) U

theorem NavierStokes.ActualCandidateConstruction.chart_velocity_of_stage_realizations (B N0 : ℕ) (a : ℝ) (i : PolarCharts.Index) (n : ℕ) {U : Set ProblemStatement.SpaceTime} (hU : IsOpen U) (AP BP : ℕ → ProblemStatement.VelocityField) (hA : ∀ (k : ℕ), DifferentiableOn ℝ (AP k) U) (hcurl : ∀ (k : ℕ), Set.EqOn (SpatialCurl.spatialCurl (AP k)) (chartPotentialParts B N0 a i n k) U) (hB : ∀ (k : ℕ), Set.EqOn (BP k) (chartDirectStages B N0 a i n k) U) (J : ℕ) : Set.EqOn (MixedDiagonalResidual.uncutVelocity AP BP J) (chartVelocity B N0 a i n J) U

theorem NavierStokes.ActualCandidateConstruction.chart_pressure_of_stage_realizations (B N0 : ℕ) (a : ℝ) (i : PolarCharts.Index) (n : ℕ) {U : Set ProblemStatement.SpaceTime} (PP : ℕ → ProblemStatement.PressureField) (hP : ∀ (k : ℕ), Set.EqOn (PP k) (chartPressureStages B N0 a i n k) U) (J : ℕ) : Set.EqOn (DiagonalJetBounds.uncutPrefix PP (J + 1)) (chartPressure B N0 a i n J) U

theorem NavierStokes.ActualCandidateConstruction.chart_residual_of_stage_realizations (B N0 : ℕ) (a : ℝ) (i : PolarCharts.Index) (n : ℕ) {U : Set ProblemStatement.SpaceTime} (hU : IsOpen U) (AP BP : ℕ → ProblemStatement.VelocityField) (PP : ℕ → ProblemStatement.PressureField) (hA : ∀ (k : ℕ), DifferentiableOn ℝ (AP k) U) (hcurl : ∀ (k : ℕ), Set.EqOn (SpatialCurl.spatialCurl (AP k)) (chartPotentialParts B N0 a i n k) U) (hB : ∀ (k : ℕ), Set.EqOn (BP k) (chartDirectStages B N0 a i n k) U) (hP : ∀ (k : ℕ), Set.EqOn (PP k) (chartPressureStages B N0 a i n k) U) (J : ℕ) : Set.EqOn (fun (z : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual (MixedDiagonalResidual.uncutVelocity AP BP J) (DiagonalJetBounds.uncutPrefix PP (J + 1)) z.1 z.2) (fun (z : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual (chartVelocity B N0 a i n J) (chartPressure B N0 a i n J) z.1 z.2) U

theorem NavierStokes.ActualCandidateConstruction.chart_residual_jets_of_stage_realizations (B N0 : ℕ) (a : ℝ) (i : PolarCharts.Index) (n : ℕ) {U : Set ProblemStatement.SpaceTime} (hU : IsOpen U) (AP BP : ℕ → ProblemStatement.VelocityField) (PP : ℕ → ProblemStatement.PressureField) (hA : ∀ (k : ℕ), DifferentiableOn ℝ (AP k) U) (hcurl : ∀ (k : ℕ), Set.EqOn (SpatialCurl.spatialCurl (AP k)) (chartPotentialParts B N0 a i n k) U) (hB : ∀ (k : ℕ), Set.EqOn (BP k) (chartDirectStages B N0 a i n k) U) (hP : ∀ (k : ℕ), Set.EqOn (PP k) (chartPressureStages B N0 a i n k) U) (J m : ℕ) : Set.EqOn (iteratedFDeriv ℝ m fun (z : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual (MixedDiagonalResidual.uncutVelocity AP BP J) (DiagonalJetBounds.uncutPrefix PP (J + 1)) z.1 z.2) (iteratedFDeriv ℝ m fun (z : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual (chartVelocity B N0 a i n J) (chartPressure B N0 a i n J) z.1 z.2) U

The actual mean fields, with one common physical representative

The selector defining this atlas depends on the physical point and the fixed validity strip. It is independent of the scalar being represented. Consequently sums and differences retain the original absolute mean and pressure; no new integration constant or choice enters a later stage.

noncomputable def NavierStokes.ActualCandidateConstruction.meanAtlas (B N0 : ℕ) : ActualMeanPhysicalData.Atlas CorrectionInitialization.ActualPrimary.h (firstBand B N0) (CorrectionInitialization.CommonWindow.gap CorrectionInitialization.ActualPrimary.h)

Mean atlas, given by ActualMeanPhysicalData.initialAtlas (firstBand B N0).

Equations

• NavierStokes.ActualCandidateConstruction.meanAtlas B N0 = NavierStokes.ActualMeanPhysicalData.initialAtlas (NavierStokes.ActualCandidateConstruction.firstBand B N0)

noncomputable def NavierStokes.ActualCandidateConstruction.meanField (B N0 : ℕ) (degree : ℝ) (f : ActualMeanPhysicalData.Scalar) : ProblemStatement.PressureField

Mean field, given by (meanAtlas B N0).physical standardRegion.carrier degree f ∘ PhysicalMeanJetBounds.physicalPoint h.

Equations

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

noncomputable def NavierStokes.ActualCandidateConstruction.meanAngularField (B N0 : ℕ) (degree : ℝ) (f : ActualMeanPhysicalData.Scalar) : ProblemStatement.VelocityField

Mean angular field, defined pointwise by meanField B N0 degree f w • PhysicalMeanJetBounds.angularVector (PhysicalGraphBounds.radialProjection w).

Equations

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

theorem NavierStokes.ActualCandidateConstruction.meanField_add (B N0 : ℕ) (degree : ℝ) (f g : ActualMeanPhysicalData.Scalar) : meanField B N0 degree (f + g) = meanField B N0 degree f + meanField B N0 degree g

theorem NavierStokes.ActualCandidateConstruction.meanField_sub (B N0 : ℕ) (degree : ℝ) (f g : ActualMeanPhysicalData.Scalar) : meanField B N0 degree (f - g) = meanField B N0 degree f - meanField B N0 degree g

theorem NavierStokes.ActualCandidateConstruction.meanAngularField_add (B N0 : ℕ) (degree : ℝ) (f g : ActualMeanPhysicalData.Scalar) : meanAngularField B N0 degree (f + g) = meanAngularField B N0 degree f + meanAngularField B N0 degree g

theorem NavierStokes.ActualCandidateConstruction.meanAngularField_sub (B N0 : ℕ) (degree : ℝ) (f g : ActualMeanPhysicalData.Scalar) : meanAngularField B N0 degree (f - g) = meanAngularField B N0 degree f - meanAngularField B N0 degree g

noncomputable def NavierStokes.ActualCandidateConstruction.angularNativeStages (B N0 : ℕ) : ℕ → ActualMeanPhysicalData.Scalar

Angular native stages as an element of ℕ → ActualMeanPhysicalData.Scalar.

Equations

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

noncomputable def NavierStokes.ActualCandidateConstruction.pressureNativeStages (B N0 : ℕ) : ℕ → ActualMeanPhysicalData.Scalar

Pressure native stages, defined pointwise by Nat.casesOn k (cycle B N0 0).state.pressure (fun j => (cycle B N0 (j + 1)).state.pressure - (cycle B N0 j).state.pressure).

Equations

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

noncomputable def NavierStokes.ActualCandidateConstruction.angularMeanStages (B N0 : ℕ) : ℕ → ProblemStatement.VelocityField

Angular mean stages, defined pointwise by meanAngularField B N0 (CoordinateAlgebra.A h) (angularNativeStages B N0 j).

Equations

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

noncomputable def NavierStokes.ActualCandidateConstruction.pressureMeanStages (B N0 : ℕ) : ℕ → ProblemStatement.PressureField

Pressure mean stages, defined pointwise by meanField B N0 (2 * CoordinateAlgebra.A h) (pressureNativeStages B N0 j).

Equations

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

theorem NavierStokes.ActualCandidateConstruction.angularNativeStages_succ (B N0 j : ℕ) : angularNativeStages B N0 (j + 1) = ((parameters B N0).temporalIncrement (cycle B N0 j).coefficients (CorrectionInitialization.ActualPrimary.commonContext B) (cycle B N0 j).state).angular + ((parameters B N0).rankIncrement (cycle B N0 j).coefficients (CorrectionInitialization.ActualPrimary.commonContext B) (cycle B N0 j).state).angular

theorem NavierStokes.ActualCandidateConstruction.uncutPrefix_succ {V : Type u_1} [NormedAddCommGroup V] (f : ℕ → ProblemStatement.SpaceTime → V) (N : ℕ) : DiagonalJetBounds.uncutPrefix f (N + 1) = DiagonalJetBounds.uncutPrefix f N + f N

theorem NavierStokes.ActualCandidateConstruction.angularMeanStages_prefix (B N0 J : ℕ) : DiagonalJetBounds.uncutPrefix (angularMeanStages B N0) (J + 1) = meanAngularField B N0 (CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) (cycle B N0 J).state.mean.angular

theorem NavierStokes.ActualCandidateConstruction.pressureMeanStages_prefix (B N0 J : ℕ) : DiagonalJetBounds.uncutPrefix (pressureMeanStages B N0) (J + 1) = meanField B N0 (2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) (cycle B N0 J).state.pressure

noncomputable def NavierStokes.ActualCandidateConstruction.temporalNative (B N0 j : ℕ) : ActualMeanPhysicalData.Scalar

Temporal native, constructed using VariableGaugeMean.temporalPotential.

Equations

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

noncomputable def NavierStokes.ActualCandidateConstruction.rankNative (B N0 j : ℕ) : ActualMeanPhysicalData.Scalar

Rank native, constructed using VariableGaugeMean.rankPotential.

Equations

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

noncomputable def NavierStokes.ActualCandidateConstruction.streamNativeStages (B N0 : ℕ) : ℕ → ActualMeanPhysicalData.Scalar

Stream native stages as an element of ℕ → ActualMeanPhysicalData.Scalar.

Equations

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

noncomputable def NavierStokes.ActualCandidateConstruction.streamMeanStages (B N0 : ℕ) : ℕ → ProblemStatement.VelocityField

Stream mean stages, defined pointwise by meanAngularField B N0 (CoordinateAlgebra.A h - 1 / 2) (streamNativeStages B N0 j).

Equations

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

theorem NavierStokes.ActualCandidateConstruction.streamMeanStages_zero (B N0 : ℕ) : streamMeanStages B N0 0 = (ActualMeanPhysicalData.initialStreamFamily B N0 (firstBand B N0)).angularField

theorem NavierStokes.ActualCandidateConstruction.angularMeanStages_zero (B N0 : ℕ) : angularMeanStages B N0 0 = (ActualMeanPhysicalData.initialAngularFamily B N0 (firstBand B N0)).angularField

theorem NavierStokes.ActualCandidateConstruction.pressureMeanStages_zero (B N0 : ℕ) : pressureMeanStages B N0 0 = (ActualMeanPhysicalData.initialPressureFamily B N0 (firstBand B N0)).field

@[reducible, inline]

abbrev NavierStokes.ActualCandidateConstruction.MeanCycleInput (B N0 : ℕ) : Prop

Mean cycle input: an abbreviation for ActualMeanPhysicalData.InitialCycleInput B N0 (firstBand B N0) (parameterSequence B N0).

Equations

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

theorem NavierStokes.ActualCandidateConstruction.parameters_realizes (B N0 j : ℕ) : CycleStateCoherence.Realizes ActualMeanPhysicalData.initialGeometry (parameterSequence B N0 j) (CorrectionInitialization.ActualPrimary.commonContext B)

theorem NavierStokes.ActualCandidateConstruction.streamMeanStages_succ {B N0 : ℕ} (H : MeanCycleInput B N0) (j : ℕ) : streamMeanStages B N0 (j + 1) = ((ActualMeanPhysicalData.initialCycleData H).streamFamily j).angularField

theorem NavierStokes.ActualCandidateConstruction.angularMeanStages_succ {B N0 : ℕ} (H : MeanCycleInput B N0) (j : ℕ) : angularMeanStages B N0 (j + 1) = ((ActualMeanPhysicalData.initialCycleData H).angularIncrementFamily j).angularField

theorem NavierStokes.ActualCandidateConstruction.pressureMeanStages_succ {B N0 : ℕ} (H : MeanCycleInput B N0) (j : ℕ) : pressureMeanStages B N0 (j + 1) = ((ActualMeanPhysicalData.initialCycleData H).pressureIncrementFamily j).field

noncomputable def NavierStokes.ActualCandidateConstruction.chartMeanPressureParts (B N0 : ℕ) (a : ℝ) (i : PolarCharts.Index) (n j : ℕ) : ProblemStatement.PressureField

Chart mean pressure parts, constructed using CyclePhysicalPrefixes.polarPressureMap.

Equations

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

noncomputable def NavierStokes.ActualCandidateConstruction.chartStreamParts (B N0 : ℕ) (a : ℝ) (i : PolarCharts.Index) (n : ℕ) : ℕ → ProblemStatement.VelocityField

Chart stream parts as an element of ℕ → VelocityField.

Equations

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

theorem NavierStokes.ActualCandidateConstruction.angularNativeStages_overlap {B N0 : ℕ} (H : MeanCycleInput B N0) (j : ℕ) : (meanAtlas B N0).OverlapLaw CorrectionInitialization.ActualPrimary.standardRegion.carrier (CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) (angularNativeStages B N0 j)

theorem NavierStokes.ActualCandidateConstruction.pressureNativeStages_overlap {B N0 : ℕ} (H : MeanCycleInput B N0) (j : ℕ) : (meanAtlas B N0).OverlapLaw CorrectionInitialization.ActualPrimary.standardRegion.carrier (2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) (pressureNativeStages B N0 j)

theorem NavierStokes.ActualCandidateConstruction.angularNativeStages_chart (B N0 : ℕ) (a : ℝ) (i : PolarCharts.Index) (n j : ℕ) : (CyclePhysicalPrefixes.polarVelocityMap a i) ((CyclePhysicalPrefixes.velocityMap (graph n)) fun (x : CyclePhysicalPrefixes.Cylinder) => ![0, angularNativeStages B N0 j n x.1, 0]) = chartDirectStages B N0 a i n j

theorem NavierStokes.ActualCandidateConstruction.angularMeanStages_on_chart {B N0 : ℕ} (H : MeanCycleInput B N0) (j : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) (n : ℕ) (hn : firstBand B N0 ≤ n) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (hu : (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n ((meanAtlas B N0).gap n) w).2.1 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier) (hw : w ∈ ActualMeanPotentialRealization.cartesianDomain a i) : angularMeanStages B N0 j w = chartDirectStages B N0 a i n j w

theorem NavierStokes.ActualCandidateConstruction.pressureMeanStages_on_chart {B N0 : ℕ} (H : MeanCycleInput B N0) (j : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) (n : ℕ) (hn : firstBand B N0 ≤ n) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (hu : (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n ((meanAtlas B N0).gap n) w).2.1 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier) (hw : w ∈ ActualMeanPotentialRealization.cartesianDomain a i) : pressureMeanStages B N0 j w = chartMeanPressureParts B N0 a i n j w

theorem NavierStokes.ActualCandidateConstruction.streamMeanStages_curl_on_chart {B N0 : ℕ} (H : MeanCycleInput B N0) (j : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) (n : ℕ) (hn : firstBand B N0 ≤ n) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (hu : (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n ((meanAtlas B N0).gap n) w).2.1 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier) (hw : w ∈ ActualMeanPotentialRealization.cartesianDomain a i) : SpatialCurl.spatialCurl (streamMeanStages B N0 j) w = chartStreamParts B N0 a i n j w

noncomputable def NavierStokes.ActualCandidateConstruction.chartBaseVelocity (B : ℕ) (a : ℝ) (i : PolarCharts.Index) (n : ℕ) : ProblemStatement.VelocityField

Chart base velocity, constructed using CyclePhysicalPrefixes.polarVelocityMap.

Equations

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

noncomputable def NavierStokes.ActualCandidateConstruction.chartBasePressure (B : ℕ) (a : ℝ) (i : PolarCharts.Index) (n : ℕ) : ProblemStatement.PressureField

Chart base pressure, given by CyclePhysicalPrefixes.polarPressureMap a i (CyclePhysicalPrefixes.pressureMap (graph n) (basePressure B n)).

Equations

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

noncomputable def NavierStokes.ActualCandidateConstruction.chartWaveParts (B N0 : ℕ) (a : ℝ) (i : PolarCharts.Index) (n : ℕ) : ℕ → ProblemStatement.VelocityField

Chart wave parts as an element of ℕ → VelocityField.

Equations

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

noncomputable def NavierStokes.ActualCandidateConstruction.chartWavePressureParts (B N0 : ℕ) (a : ℝ) (i : PolarCharts.Index) (n : ℕ) : ℕ → ProblemStatement.PressureField

Chart wave pressure parts as an element of ℕ → PressureField.

Equations

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

theorem NavierStokes.ActualCandidateConstruction.chartPotentialParts_zero (B N0 : ℕ) (a : ℝ) (i : PolarCharts.Index) (n : ℕ) : chartPotentialParts B N0 a i n 0 = chartBaseVelocity B a i n + chartWaveParts B N0 a i n 0 + chartStreamParts B N0 a i n 0

theorem NavierStokes.ActualCandidateConstruction.chartPotentialParts_succ (B N0 j : ℕ) (a : ℝ) (i : PolarCharts.Index) (n : ℕ) : chartPotentialParts B N0 a i n (j + 1) = chartWaveParts B N0 a i n (j + 1) + chartStreamParts B N0 a i n (j + 1)

theorem NavierStokes.ActualCandidateConstruction.chartPressureParts_zero (B N0 : ℕ) (a : ℝ) (i : PolarCharts.Index) (n : ℕ) : chartPressureStages B N0 a i n 0 = chartBasePressure B a i n + chartWavePressureParts B N0 a i n 0 + chartMeanPressureParts B N0 a i n 0

theorem NavierStokes.ActualCandidateConstruction.chartPressureParts_succ (B N0 j : ℕ) (a : ℝ) (i : PolarCharts.Index) (n : ℕ) : chartPressureStages B N0 a i n (j + 1) = chartWavePressureParts B N0 a i n (j + 1) + chartMeanPressureParts B N0 a i n (j + 1)

The fixed physical base in the same chart

Both normalizations below are computed from the actual graph map. In particular the pressure factor is the square of the velocity factor.

theorem NavierStokes.ActualCandidateConstruction.graph_cylinderPoint (n : ℕ) (z : ProblemStatement.SpaceTime) : ActualBaseResidual.cylinderPoint CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (PhysicalResidualTZ.graphMapTZ (graph n) z) = z

theorem NavierStokes.ActualCandidateConstruction.graph_physicalPoint (n : ℕ) (z : ProblemStatement.SpaceTime) : ActualBaseResidual.physicalPoint CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (PhysicalResidualTZ.graphMapTZ (graph n) z) = (z.1, CylindricalResidual.chart z.2)

theorem NavierStokes.ActualCandidateConstruction.graph_mem_baseDomain (n : ℕ) {z : ProblemStatement.SpaceTime} (ht : z.1 < 1) (hr : 0 < z.2.ofLp 0) : PhysicalResidualTZ.graphMapTZ (graph n) z ∈ ActualBaseResidual.domain

theorem NavierStokes.ActualCandidateConstruction.base_velocity_on_cylinder (B n : ℕ) {z : ProblemStatement.SpaceTime} (ht : z.1 < 1) (hr : 0 < z.2.ofLp 0) : (CyclePhysicalPrefixes.velocityMap (graph n)) (PhysicalResidualBridge.baseComponents (CorrectionInitialization.ActualPrimary.commonContext B) n) z = (CylindricalResidual.frame (-z.2.ofLp 1)) (FinalSlowBase.velocity CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B (z.1, CylindricalResidual.chart z.2))

theorem NavierStokes.ActualCandidateConstruction.base_pressure_on_cylinder (B n : ℕ) (z : ProblemStatement.SpaceTime) : (CyclePhysicalPrefixes.pressureMap (graph n)) (basePressure B n) z = FinalSlowBase.pressure CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B (z.1, CylindricalResidual.chart z.2)

theorem NavierStokes.ActualCandidateConstruction.chartBaseVelocity_eq (B : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) (n : ℕ) {w : ProblemStatement.SpaceTime} (ht : w.1 < 1) (hw : w ∈ ActualMeanPotentialRealization.cartesianDomain a i) : chartBaseVelocity B a i n w = FinalSlowBase.velocity CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B w

theorem NavierStokes.ActualCandidateConstruction.chartBasePressure_eq (B : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) (n : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ ActualMeanPotentialRealization.cartesianDomain a i) : chartBasePressure B a i n w = FinalSlowBase.pressure CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B w

theorem NavierStokes.ActualCandidateConstruction.basePotential_curl_on_chart (B : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) (n : ℕ) {w : ProblemStatement.SpaceTime} (ht : w.1 < 1) (hw : w ∈ ActualMeanPotentialRealization.cartesianDomain a i) : SpatialCurl.spatialCurl (TailGaugePotential.finalPotential CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B) w = chartBaseVelocity B a i n w

Constructed direct angular and mean-stream stage data

noncomputable def NavierStokes.ActualCandidateConstruction.directData {B N0 : ℕ} (H : MeanCycleInput B N0) : ℕ → DirectAngularDiagonal.AngularData (LocalAngularDiagonal.localSlowDomain CorrectionInitialization.ActualPrimary.h (qbig B N0))

Direct data as an element of ℕ → DirectAngularDiagonal.AngularData (LocalAngularDiagonal.localSlowDomain h (qbig B N0)).

Equations

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

noncomputable def NavierStokes.ActualCandidateConstruction.streamData {B N0 : ℕ} (H : MeanCycleInput B N0) : ℕ → DirectAngularDiagonal.AngularData (LocalAngularDiagonal.localSlowDomain CorrectionInitialization.ActualPrimary.h (qbig B N0))

Stream data as an element of ℕ → DirectAngularDiagonal.AngularData (LocalAngularDiagonal.localSlowDomain h (qbig B N0)).

Equations

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

noncomputable def NavierStokes.ActualCandidateConstruction.meanStreamSupport {B N0 : ℕ} (H : MeanCycleInput B N0) (j : ℕ) : MixedAxisPreservation.AngularSupport (MixedAxisPreservation.localDomain CorrectionInitialization.ActualPrimary.h (qbig B N0))

Mean stream support, given by MixedAxisPreservation.AngularSupport.ofAngularData (streamData H j) (fun _ hw => hw).

Equations

• NavierStokes.ActualCandidateConstruction.meanStreamSupport H j = NavierStokes.MixedAxisPreservation.AngularSupport.ofAngularData (NavierStokes.ActualCandidateConstruction.streamData H j) ⋯

theorem NavierStokes.ActualCandidateConstruction.directData_field {B N0 : ℕ} (H : MeanCycleInput B N0) (j : ℕ) : LocalAngularDiagonal.rawSeries (directData H) j = angularMeanStages B N0 j

theorem NavierStokes.ActualCandidateConstruction.streamData_field {B N0 : ℕ} (H : MeanCycleInput B N0) (j : ℕ) : DirectAngularDiagonal.angularField (streamData H j).scalar = streamMeanStages B N0 j

theorem NavierStokes.ActualCandidateConstruction.meanStreamSupport_field {B N0 : ℕ} (H : MeanCycleInput B N0) (j : ℕ) : (meanStreamSupport H j).field = streamMeanStages B N0 j

theorem NavierStokes.ActualCandidateConstruction.angularMeanStages_smooth {B N0 : ℕ} (H : MeanCycleInput B N0) (j : ℕ) : ContDiffOn ℝ (↑⊤) (angularMeanStages B N0 j) (physicalDomain B N0)

theorem NavierStokes.ActualCandidateConstruction.streamMeanStages_smooth {B N0 : ℕ} (H : MeanCycleInput B N0) (j : ℕ) : ContDiffOn ℝ (↑⊤) (streamMeanStages B N0 j) (physicalDomain B N0)

theorem NavierStokes.ActualCandidateConstruction.angularMeanStages_shrinkingSupport {B N0 : ℕ} (H : MeanCycleInput B N0) (j : ℕ) : MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h PhysicalStageSupport.actualOuterConstant (qbig B N0) (angularMeanStages B N0 j)

theorem NavierStokes.ActualCandidateConstruction.streamMeanStages_shrinkingSupport {B N0 : ℕ} (H : MeanCycleInput B N0) (j : ℕ) : MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h PhysicalStageSupport.actualOuterConstant (qbig B N0) (streamMeanStages B N0 j)

theorem NavierStokes.ActualCandidateConstruction.pressureMeanStages_shrinkingSupport {B N0 : ℕ} (H : MeanCycleInput B N0) (j : ℕ) : MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h PhysicalStageSupport.actualOuterConstant (qbig B N0) (pressureMeanStages B N0 j)

The stage constructors retain the actual copy data. The wave producers supply these records; the mean field is fixed by the same cycle above.

noncomputable def NavierStokes.ActualCandidateConstruction.initialPotentialStage (B N0 : ℕ) (wave : MixedAxisPreservation.CopyPotential CorrectionInitialization.ActualPrimary.h) : MixedAxisPreservation.PotentialStage CorrectionInitialization.ActualPrimary.h (MixedAxisPreservation.localDomain CorrectionInitialization.ActualPrimary.h (qbig B N0))

Initial potential stage, bundling waveCount, waves, streamCount, streams.

Equations

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

noncomputable def NavierStokes.ActualCandidateConstruction.positivePotentialStage {B N0 : ℕ} (H : MeanCycleInput B N0) (j : ℕ) (particular signed : MixedAxisPreservation.CopyPotential CorrectionInitialization.ActualPrimary.h) : MixedAxisPreservation.PotentialStage CorrectionInitialization.ActualPrimary.h (MixedAxisPreservation.localDomain CorrectionInitialization.ActualPrimary.h (qbig B N0))

Positive potential stage, bundling waveCount, waves, streamCount, streams.

Equations

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

theorem NavierStokes.ActualCandidateConstruction.initialPotentialStage_field (B N0 : ℕ) (wave : MixedAxisPreservation.CopyPotential CorrectionInitialization.ActualPrimary.h) : (initialPotentialStage B N0 wave).field = wave.field + streamMeanStages B N0 0

theorem NavierStokes.ActualCandidateConstruction.positivePotentialStage_field {B N0 : ℕ} (H : MeanCycleInput B N0) (j : ℕ) (particular signed : MixedAxisPreservation.CopyPotential CorrectionInitialization.ActualPrimary.h) : (positivePotentialStage H j particular signed).field = particular.field + signed.field + streamMeanStages B N0 (j + 1)

Endpoint inputs for the actual raw candidate stages

Positive stages use their already proved raw estimates. Stage zero uses the actual initial mean families and the existing extensions of the same base potential and pressure. No output extension is an input below.

structure NavierStokes.ActualEndpointInputs.EndpointInputs (h qbig : ℝ) (A V : ℕ → ProblemStatement.VelocityField) (P : ℕ → ProblemStatement.PressureField) : Prop

The three off-plane endpoint obligations of candidate_of_finite_stages. This is an output package; the construction below does not assume its fields.

• potential (x : ProblemStatement.Space) : x.ofLp 2 ≠ 0 → EndpointCoordinates.endpointRoot (2 * h) (x.ofLp 2) < qbig → ∀ (j : ℕ), Nonempty (JointResidualLimits.OneSidedExtension (A j) x)
• direct (x : ProblemStatement.Space) : x.ofLp 2 ≠ 0 → EndpointCoordinates.endpointRoot (2 * h) (x.ofLp 2) < qbig → ∀ (j : ℕ), Nonempty (JointResidualLimits.OneSidedExtension (V j) x)
• pressure (x : ProblemStatement.Space) : x.ofLp 2 ≠ 0 → EndpointCoordinates.endpointRoot (2 * h) (x.ofLp 2) < qbig → ∀ (j : ℕ), Nonempty (JointResidualLimits.OneSidedExtension (P j) x)

noncomputable def NavierStokes.ActualEndpointInputs.initialPotentialModel {DA : Type} [NormedAddCommGroup DA] [NormedSpace ℝ DA] {IA : Type u_1} {KA : Type u_2} (B N0 N : ℕ) (hN : 4 ≤ N) (WA : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DA IA KA (Fin 3)) : ProblemStatement.VelocityField

The exact base and bounded finite initial potential correction.

Equations

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

noncomputable def NavierStokes.ActualEndpointInputs.initialDirectModel (B N0 N : ℕ) : ProblemStatement.VelocityField

Initial direct model, given by (ActualMeanPhysicalData.initialAngularFamily B N0 N).angularField.

Equations

• NavierStokes.ActualEndpointInputs.initialDirectModel B N0 N = (NavierStokes.ActualMeanPhysicalData.initialAngularFamily B N0 N).angularField

noncomputable def NavierStokes.ActualEndpointInputs.initialPressureModel {DP : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] {IP : Type u_3} {KP : Type u_4} (B N0 N : ℕ) (hN : 4 ≤ N) (WP : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DP IP KP Unit) : ProblemStatement.PressureField

The pressure of the same summed base and the actual finite initial wave and mean-pressure correction.

Equations

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

theorem NavierStokes.ActualEndpointInputs.initialPotentialModel_eq {DA : Type} [NormedAddCommGroup DA] [NormedSpace ℝ DA] {IA : Type u_1} {KA : Type u_2} (B N0 N : ℕ) (hN : 4 ≤ N) (WA : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DA IA KA (Fin 3)) (w : ProblemStatement.SpaceTime) : initialPotentialModel B N0 N hN WA w = TailGaugePotential.finalPotential CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B w + (WA.vector w + (ActualMeanPhysicalData.initialStreamFamily B N0 N).angularField w)

theorem NavierStokes.ActualEndpointInputs.initialPressureModel_eq {DP : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] {IP : Type u_3} {KP : Type u_4} (B N0 N : ℕ) (hN : 4 ≤ N) (WP : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DP IP KP Unit) (w : ProblemStatement.SpaceTime) : initialPressureModel B N0 N hN WP w = FinalSlowBase.pressure CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B w + (WP.pressure w + (ActualMeanPhysicalData.initialPressureFamily B N0 N).field w)

theorem NavierStokes.ActualEndpointInputs.initialPotentialModel_extension {DA : Type} [NormedAddCommGroup DA] [NormedSpace ℝ DA] {IA : Type u_1} {KA : Type u_2} (B N0 N : ℕ) (hN : 4 ≤ N) (WA : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DA IA KA (Fin 3)) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) {x : ProblemStatement.Space} (hx : x.ofLp 2 ≠ 0) (hqx : EndpointCoordinates.endpointRoot (2 * CorrectionInitialization.ActualPrimary.h) (x.ofLp 2) < qbig) : Nonempty (JointResidualLimits.OneSidedExtension (initialPotentialModel B N0 N hN WA) x)

theorem NavierStokes.ActualEndpointInputs.initialDirectModel_extension (B N0 N : ℕ) (hN : 4 ≤ N) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) {x : ProblemStatement.Space} (hx : x.ofLp 2 ≠ 0) (hqx : EndpointCoordinates.endpointRoot (2 * CorrectionInitialization.ActualPrimary.h) (x.ofLp 2) < qbig) : Nonempty (JointResidualLimits.OneSidedExtension (initialDirectModel B N0 N) x)

theorem NavierStokes.ActualEndpointInputs.initialPressureModel_extension {DP : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] {IP : Type u_3} {KP : Type u_4} (B N0 N : ℕ) (hN : 4 ≤ N) (WP : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DP IP KP Unit) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) {x : ProblemStatement.Space} (hx : x.ofLp 2 ≠ 0) (hqx : EndpointCoordinates.endpointRoot (2 * CorrectionInitialization.ActualPrimary.h) (x.ofLp 2) < qbig) : Nonempty (JointResidualLimits.OneSidedExtension (initialPressureModel B N0 N hN WP) x)

theorem NavierStokes.ActualEndpointInputs.endpointInputs_of_representations {DA DP : Type} [NormedAddCommGroup DA] [NormedSpace ℝ DA] [NormedAddCommGroup DP] [NormedSpace ℝ DP] {IA : Type u_1} {KA : Type u_2} {IP : Type u_3} {KP : Type u_4} (B N0 N : ℕ) (hN : 4 ≤ N) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) (WA : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DA IA KA (Fin 3)) (WP : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DP IP KP Unit) {A V : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} (E : MixedCandidateAssembly.StageEstimates CorrectionInitialization.ActualPrimary.h qbig A V P) (hA : Set.EqOn (A 0) (initialPotentialModel B N0 N hN WA) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)) (hV : Set.EqOn (V 0) (initialDirectModel B N0 N) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)) (hP : Set.EqOn (P 0) (initialPressureModel B N0 N hN WP) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)) : EndpointInputs CorrectionInitialization.ActualPrimary.h qbig A V P

The physical bounds and exact initial representations supply all three endpoint inputs, including index zero. No extension or endpoint limit is assumed for any raw stage.

theorem NavierStokes.ActualEndpointInputs.actual_stage_endpoints {DA DP : Type} [NormedAddCommGroup DA] [NormedSpace ℝ DA] [NormedAddCommGroup DP] [NormedSpace ℝ DP] {IA : Type u_1} {KA : Type u_2} {IP : Type u_3} {KP : Type u_4} (B N0 N : ℕ) (hN : 4 ≤ N) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) (WA : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DA IA KA (Fin 3)) (WP : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DP IP KP Unit) (initial : MixedAxisPreservation.PotentialStage CorrectionInitialization.ActualPrimary.h (MixedAxisPreservation.localDomain CorrectionInitialization.ActualPrimary.h qbig)) (stages : ℕ → MixedAxisPreservation.PotentialStage CorrectionInitialization.ActualPrimary.h (MixedAxisPreservation.localDomain CorrectionInitialization.ActualPrimary.h qbig)) (direct : ℕ → DirectAngularDiagonal.AngularData (LocalAngularDiagonal.localSlowDomain CorrectionInitialization.ActualPrimary.h qbig)) (pInitial : ProblemStatement.PressureField) (pStages : ℕ → ProblemStatement.PressureField) (E : MixedCandidateAssembly.StageEstimates CorrectionInitialization.ActualPrimary.h qbig (MixedCandidateAssembly.potentialStages CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B initial stages) (LocalAngularDiagonal.rawSeries direct) (MixedCandidateAssembly.pressureStages CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B pInitial pStages)) (hInitial : Set.EqOn initial.field (fun (w : ProblemStatement.SpaceTime) => WA.vector w + (ActualMeanPhysicalData.initialStreamFamily B N0 N).angularField w) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)) (hDirect : Set.EqOn (LocalAngularDiagonal.rawSeries direct 0) (initialDirectModel B N0 N) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)) (hPressure : Set.EqOn pInitial (fun (w : ProblemStatement.SpaceTime) => WP.pressure w + (ActualMeanPhysicalData.initialPressureFamily B N0 N).field w) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)) : EndpointInputs CorrectionInitialization.ActualPrimary.h qbig (MixedCandidateAssembly.potentialStages CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B initial stages) (LocalAngularDiagonal.rawSeries direct) (MixedCandidateAssembly.pressureStages CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B pInitial pStages)

Application to the literal raw families expected by MixedCandidateAssembly.candidate_of_finite_stages. The remaining equalities identify the produced physical fields, not their endpoint jets.

theorem NavierStokes.ActualEndpointInputs.direct_initial_representation (B N0 N : ℕ) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) (direct : ℕ → DirectAngularDiagonal.AngularData (LocalAngularDiagonal.localSlowDomain CorrectionInitialization.ActualPrimary.h qbig)) (hDirect : direct 0 = ActualMeanStageData.initialAngularData B N0 N qbig hq) : LocalAngularDiagonal.rawSeries direct 0 = initialDirectModel B N0 N

The chosen direct angular constructor supplies its stage-zero representation by its proved global field identity.

theorem NavierStokes.ActualEndpointInputs.endpointInputs_of_run {B N0 N : ℕ} {DP DS DA0 DP0 : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] [NormedAddCommGroup DA0] [NormedSpace ℝ DA0] [NormedAddCommGroup DP0] [NormedSpace ℝ DP0] {IP : Type u_1} {KP : Type u_2} {IS : Type u_3} {KS : Type u_4} {IA0 : Type u_5} {KA0 : Type u_6} {IP0 : Type u_7} {KP0 : Type u_8} (R : ActualStageEstimates.RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : ActualStageEstimates.WaveInputs DP IP KP DS IS KS) (WA : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DA0 IA0 KA0 (Fin 3)) (WP : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DP0 IP0 KP0 Unit) {qbig : ℝ} {A V : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} (e : ActualStageEstimates.Representations R M hN W qbig WA WP A V P) (hq : qbig ≤ ChartScales.Q N) : EndpointInputs CorrectionInitialization.ActualPrimary.h qbig A V P

Direct application to the fixed actual run. Native wave and mean data and their exact physical representations already imply the endpoint inputs; no finite-residual estimate or completed StageEstimates record is required for this conclusion.

Endpoint inputs for physical fields assembled by germs

The potential increments may be literal glued physical fields. Only their interior smoothness and actual derivative estimates enter the extension argument; a representation by a fixed-reference copy family is unnecessary. The zeroth potential and pressure retain the separately extended slow base.

structure NavierStokes.GermEndpointInputs.PhysicalJets (h qbig : ℝ) {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : ProblemStatement.SpaceTime → V) : Prop

Interior data for one actual physical field. The exponent and logarithmic loss may depend on the derivative order and on the field. In particular this record neither assumes an endpoint limit nor compares different stages.

• smooth : ContDiffOn ℝ (↑⊤) f (CutStageEstimates.physicalSublevel h qbig)
• bound (m : ℕ) : ∃ (C : ℝ) (p : ℝ) (e : ℝ), ∀ w ∈ CutStageEstimates.physicalSublevel h qbig, |w.1| ≤ 1 → PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m f w‖ ≤ C * (1 + |Real.log (PhysicalWaveSum.physicalQ h w)|) ^ p * PhysicalWaveSum.physicalQ h w ^ e

theorem NavierStokes.GermEndpointInputs.PhysicalJets.of_power {h qbig : ℝ} {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ProblemStatement.SpaceTime → V} (hf : ContDiffOn ℝ (↑⊤) f (CutStageEstimates.physicalSublevel h qbig)) (hb : ∀ (m : ℕ), ∃ (C : ℝ) (e : ℝ), ∀ w ∈ CutStageEstimates.physicalSublevel h qbig, |w.1| ≤ 1 → PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m f w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ e) : PhysicalJets h qbig f

Adapter for the power bounds of the current-band physical construction. The time restriction is kept, as in the physical wave estimate.

theorem NavierStokes.GermEndpointInputs.PhysicalJets.of_rawStage {h qbig : ℝ} {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {A : ℕ → ProblemStatement.SpaceTime → V} {g L : ℕ → ℝ} {C p : ℕ → ℕ → ℝ} (hb : CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ h) A g L C p (PhysicalWaveSum.preterminal ∩ CutStageEstimates.physicalSublevel h qbig)) {j : ℕ} (hj : 1 ≤ j) (hf : ContDiffOn ℝ (↑⊤) (A j) (CutStageEstimates.physicalSublevel h qbig)) : PhysicalJets h qbig (A j)

The positive-index restriction in RawStageBounds is preserved.

theorem NavierStokes.GermEndpointInputs.PhysicalJets.mono {h qbig : ℝ} {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ProblemStatement.SpaceTime → V} {qsmall : ℝ} (J : PhysicalJets h qbig f) (hq : qsmall ≤ qbig) : PhysicalJets h qsmall f

A smaller scale cap preserves the same constants.

theorem NavierStokes.GermEndpointInputs.PhysicalJets.congr {h qbig : ℝ} {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ProblemStatement.SpaceTime → V} (J : PhysicalJets h qbig f) {g : ProblemStatement.SpaceTime → V} (hh : 0 < h) (hh1 : h < 1 / 2) (he : Set.EqOn g f (CutStageEstimates.physicalSublevel h qbig)) : PhysicalJets h qbig g

Physical identities on the open validity region identify every actual ordinary jet. Values at a chart face or beyond the region are irrelevant.

theorem NavierStokes.GermEndpointInputs.PhysicalJets.add {h qbig : ℝ} {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ProblemStatement.SpaceTime → V} (J : PhysicalJets h qbig f) {g : ProblemStatement.SpaceTime → V} (K : PhysicalJets h qbig g) (hh : 0 < h) (hh1 : h < 1 / 2) : PhysicalJets h qbig fun (w : ProblemStatement.SpaceTime) => f w + g w

Finite sums retain derivative bounds without identifying a summand with any copy-family construction.

theorem NavierStokes.GermEndpointInputs.PhysicalJets.extension {h qbig : ℝ} {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ProblemStatement.SpaceTime → V} [CompleteSpace V] (J : PhysicalJets h qbig f) (hh : 0 < h) (hh1 : h < 1 / 2) (hqbig : qbig ≤ 1) {x : ProblemStatement.Space} (hx : x.ofLp 2 ≠ 0) (hqx : EndpointCoordinates.endpointRoot (2 * h) (x.ofLp 2) < qbig) : Nonempty (JointResidualLimits.OneSidedExtension f x)

This is an application of the existing local bounded-jet extension theorem. No new boundary regularity hypothesis is introduced.

theorem NavierStokes.GermEndpointInputs.mean_field_jets {h degree qbig : ℝ} (M : ActualPhysicalStageBounds.MeanInput h degree) (hh : 0 < h) (hh1 : h < 1 / 2) (hq : qbig ≤ ChartScales.Q M.firstBand) : PhysicalJets h qbig M.family.field

The actual mean-pressure native bounds supply the single-field input.

theorem NavierStokes.GermEndpointInputs.mean_angular_jets {h degree qbig : ℝ} (M : ActualPhysicalStageBounds.MeanInput h degree) (hh : 0 < h) (hh1 : h < 1 / 2) (hq : qbig ≤ ChartScales.Q M.firstBand) : PhysicalJets h qbig M.family.angularField

This applies to both actual mean-stream potentials and the direct angular increments, with their own physical degree and their original first band.

theorem NavierStokes.GermEndpointInputs.wave_vector_jets {h qbig : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (W : PhysicalStageBounds.WaveData h D I K (Fin 3)) (hh : 0 < h) (hh1 : h < 1 / 2) : PhysicalJets h qbig W.vector

Existing initial or signed wave data can be used for those summands. No such data are requested for the glued particular summand.

theorem NavierStokes.GermEndpointInputs.wave_pressure_jets {h qbig : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (W : PhysicalStageBounds.WaveData h D I K Unit) (hh : 0 < h) (hh1 : h < 1 / 2) : PhysicalJets h qbig W.pressure

theorem NavierStokes.GermEndpointInputs.initial_potential_jets {DA : Type} [NormedAddCommGroup DA] [NormedSpace ℝ DA] {IA : Type u_1} {KA : Type u_2} (B N0 N : ℕ) (hN : 4 ≤ N) (WA : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DA IA KA (Fin 3)) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) : PhysicalJets CorrectionInitialization.ActualPrimary.h qbig fun (w : ProblemStatement.SpaceTime) => WA.vector w + (ActualMeanPhysicalData.initialStreamFamily B N0 N).angularField w

The finite potential correction at index zero uses the actual initial wave, temporal mean, and rank mean. The slow-base gauge is excluded here.

theorem NavierStokes.GermEndpointInputs.initial_direct_jets (B N0 N : ℕ) (hN : 4 ≤ N) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) : PhysicalJets CorrectionInitialization.ActualPrimary.h qbig (ActualMeanPhysicalData.initialAngularFamily B N0 N).angularField

theorem NavierStokes.GermEndpointInputs.initial_pressure_jets {DP : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] {IP : Type u_3} {KP : Type u_4} (B N0 N : ℕ) (hN : 4 ≤ N) (WP : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DP IP KP Unit) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) : PhysicalJets CorrectionInitialization.ActualPrimary.h qbig fun (w : ProblemStatement.SpaceTime) => WP.pressure w + (ActualMeanPhysicalData.initialPressureFamily B N0 N).field w

The finite initial pressure correction retains the actual initial wave pressure and the pressure mean.

theorem NavierStokes.GermEndpointInputs.extension_of_sum3 {h qbig : ℝ} {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {f f₁ f₂ f₃ : ProblemStatement.SpaceTime → V} (J₁ : PhysicalJets h qbig f₁) (J₂ : PhysicalJets h qbig f₂) (J₃ : PhysicalJets h qbig f₃) (he : Set.EqOn f (fun (w : ProblemStatement.SpaceTime) => f₁ w + f₂ w + f₃ w) (CutStageEstimates.physicalSublevel h qbig)) (hh : 0 < h) (hh1 : h < 1 / 2) (hqbig : qbig ≤ 1) {x : ProblemStatement.Space} (hx : x.ofLp 2 ≠ 0) (hqx : EndpointCoordinates.endpointRoot (2 * h) (x.ofLp 2) < qbig) : Nonempty (JointResidualLimits.OneSidedExtension f x)

A finite physical sum can be extended directly from estimates of its actual summands. Equality is required only on the physical validity region.

theorem NavierStokes.GermEndpointInputs.endpoints_of_bounds {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (bandFloor : ℕ) {qbig : ℝ} (hqbig : qbig ≤ 1) {A V : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} {initial : ProblemStatement.VelocityField} {pInitial : ProblemStatement.PressureField} (hA0 : Set.EqOn (A 0) (fun (w : ProblemStatement.SpaceTime) => TailGaugePotential.finalPotential H v upper bandFloor w + initial w) (CutStageEstimates.physicalSublevel F.data.h qbig)) (hP0 : Set.EqOn (P 0) (fun (w : ProblemStatement.SpaceTime) => FinalSlowBase.pressure H v upper bandFloor w + pInitial w) (CutStageEstimates.physicalSublevel F.data.h qbig)) (Jinitial : PhysicalJets F.data.h qbig initial) (JpInitial : PhysicalJets F.data.h qbig pInitial) (JA : ∀ (j : ℕ), 1 ≤ j → PhysicalJets F.data.h qbig (A j)) (JV : ∀ (j : ℕ), PhysicalJets F.data.h qbig (V j)) (JP : ∀ (j : ℕ), 1 ≤ j → PhysicalJets F.data.h qbig (P j)) : ActualEndpointInputs.EndpointInputs F.data.h qbig A V P

Bounds for literal raw fields imply all three candidate endpoint inputs. The base gauge is never subjected to a growth assumption, and the positive stage estimate is never applied to index zero.

theorem NavierStokes.GermEndpointInputs.germ_stage_endpoints {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (bandFloor : ℕ) {qbig : ℝ} (hqbig : qbig ≤ 1) (initial : ProblemStatement.VelocityField) (stages : ℕ → ProblemStatement.VelocityField) (D : ℕ → DirectAngularDiagonal.AngularData (LocalAngularDiagonal.localSlowDomain F.data.h qbig)) (pInitial : ProblemStatement.PressureField) (pStages : ℕ → ProblemStatement.PressureField) (Jinitial : PhysicalJets F.data.h qbig initial) (Jstages : ∀ (j : ℕ), PhysicalJets F.data.h qbig (stages j)) (JD : ∀ (j : ℕ), PhysicalJets F.data.h qbig (LocalAngularDiagonal.rawSeries D j)) (JpInitial : PhysicalJets F.data.h qbig pInitial) (JpStages : ∀ (j : ℕ), PhysicalJets F.data.h qbig (pStages j)) : ActualEndpointInputs.EndpointInputs F.data.h qbig (GermCandidateAssembly.potentialStages H v upper bandFloor initial stages) (LocalAngularDiagonal.rawSeries D) (MixedCandidateAssembly.pressureStages H v upper bandFloor pInitial pStages)

Literal fields accepted by GermCandidateAssembly. In particular stages j may be a glued current-particular field plus signed and mean corrections; there is no copy-family or potential-stage argument.

theorem NavierStokes.GermEndpointInputs.germ_stage_endpoints_of_estimates {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (bandFloor : ℕ) {qbig : ℝ} (hqbig : qbig ≤ 1) (initial : ProblemStatement.VelocityField) (stages : ℕ → ProblemStatement.VelocityField) (D : ℕ → DirectAngularDiagonal.AngularData (LocalAngularDiagonal.localSlowDomain F.data.h qbig)) (pInitial : ProblemStatement.PressureField) (pStages : ℕ → ProblemStatement.PressureField) (E : MixedCandidateAssembly.StageEstimates F.data.h qbig (GermCandidateAssembly.potentialStages H v upper bandFloor initial stages) (LocalAngularDiagonal.rawSeries D) (MixedCandidateAssembly.pressureStages H v upper bandFloor pInitial pStages)) (Jinitial : PhysicalJets F.data.h qbig initial) (Jdirect : PhysicalJets F.data.h qbig (LocalAngularDiagonal.rawSeries D 0)) (JpInitial : PhysicalJets F.data.h qbig pInitial) : ActualEndpointInputs.EndpointInputs F.data.h qbig (GermCandidateAssembly.potentialStages H v upper bandFloor initial stages) (LocalAngularDiagonal.rawSeries D) (MixedCandidateAssembly.pressureStages H v upper bandFloor pInitial pStages)

Once the finite-stage estimates have been derived, only the bounded finite initial pieces remain to be supplied. This wrapper does not inspect or impose a representation of any positive physical stage.

theorem NavierStokes.GermEndpointInputs.actual_initial_potential_jets (B N0 N : ℕ) (hN : 4 ≤ N) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) : PhysicalJets CorrectionInitialization.ActualPrimary.h qbig fun (w : ProblemStatement.SpaceTime) => InitialPhysicalData.potential B N0 w + (ActualMeanPhysicalData.initialStreamFamily B N0 N).angularField w

The chosen initial potential supplies its own native wave data. The consumer does not have to provide or postulate such a witness.

theorem NavierStokes.GermEndpointInputs.actual_initial_pressure_jets (B N0 N : ℕ) (hN : 4 ≤ N) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) : PhysicalJets CorrectionInitialization.ActualPrimary.h qbig fun (w : ProblemStatement.SpaceTime) => InitialPhysicalData.pressure B N0 w + (ActualMeanPhysicalData.initialPressureFamily B N0 N).field w

theorem NavierStokes.GermEndpointInputs.actual_germ_stage_endpoints (B N0 N : ℕ) (hN : 4 ≤ N) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) (initial : ProblemStatement.VelocityField) (stages : ℕ → ProblemStatement.VelocityField) (D : ℕ → DirectAngularDiagonal.AngularData (LocalAngularDiagonal.localSlowDomain CorrectionInitialization.ActualPrimary.h qbig)) (pInitial : ProblemStatement.PressureField) (pStages : ℕ → ProblemStatement.PressureField) (hInitial : Set.EqOn initial (fun (w : ProblemStatement.SpaceTime) => InitialPhysicalData.potential B N0 w + (ActualMeanPhysicalData.initialStreamFamily B N0 N).angularField w) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)) (hDirect : Set.EqOn (LocalAngularDiagonal.rawSeries D 0) (ActualMeanPhysicalData.initialAngularFamily B N0 N).angularField (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)) (hPressure : Set.EqOn pInitial (fun (w : ProblemStatement.SpaceTime) => InitialPhysicalData.pressure B N0 w + (ActualMeanPhysicalData.initialPressureFamily B N0 N).field w) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)) (Jstages : ∀ (j : ℕ), PhysicalJets CorrectionInitialization.ActualPrimary.h qbig (stages j)) (Jdirect : ∀ (j : ℕ), 1 ≤ j → PhysicalJets CorrectionInitialization.ActualPrimary.h qbig (LocalAngularDiagonal.rawSeries D j)) (JpStages : ∀ (j : ℕ), PhysicalJets CorrectionInitialization.ActualPrimary.h qbig (pStages j)) : ActualEndpointInputs.EndpointInputs CorrectionInitialization.ActualPrimary.h qbig (GermCandidateAssembly.potentialStages CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B initial stages) (LocalAngularDiagonal.rawSeries D) (MixedCandidateAssembly.pressureStages CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B pInitial pStages)

The same-choice mixed raw sequence has all endpoint inputs. Positive fields are arbitrary physical fields, including the genuine glued particular fields. Only their derived interior jet estimates are used. Initialization is bound to the actual initial wave and actual mean families by local field identities, with no supplied wave-data or endpoint-extension witness.

theorem NavierStokes.GermEndpointInputs.actual_germ_stage_endpoints_of_estimates (B N0 N : ℕ) (hN : 4 ≤ N) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) (initial : ProblemStatement.VelocityField) (stages : ℕ → ProblemStatement.VelocityField) (D : ℕ → DirectAngularDiagonal.AngularData (LocalAngularDiagonal.localSlowDomain CorrectionInitialization.ActualPrimary.h qbig)) (pInitial : ProblemStatement.PressureField) (pStages : ℕ → ProblemStatement.PressureField) (E : MixedCandidateAssembly.StageEstimates CorrectionInitialization.ActualPrimary.h qbig (GermCandidateAssembly.potentialStages CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B initial stages) (LocalAngularDiagonal.rawSeries D) (MixedCandidateAssembly.pressureStages CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B pInitial pStages)) (hInitial : Set.EqOn initial (fun (w : ProblemStatement.SpaceTime) => InitialPhysicalData.potential B N0 w + (ActualMeanPhysicalData.initialStreamFamily B N0 N).angularField w) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)) (hDirect : Set.EqOn (LocalAngularDiagonal.rawSeries D 0) (ActualMeanPhysicalData.initialAngularFamily B N0 N).angularField (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)) (hPressure : Set.EqOn pInitial (fun (w : ProblemStatement.SpaceTime) => InitialPhysicalData.pressure B N0 w + (ActualMeanPhysicalData.initialPressureFamily B N0 N).field w) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)) : ActualEndpointInputs.EndpointInputs CorrectionInitialization.ActualPrimary.h qbig (GermCandidateAssembly.potentialStages CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B initial stages) (LocalAngularDiagonal.rawSeries D) (MixedCandidateAssembly.pressureStages CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B pInitial pStages)

A derived StageEstimates record is an alternative source of the positive-stage estimates. No quantitative conclusion or representation of the glued particular field is added as a hypothesis here.

The Cartesian curl of the actual finite particular-wave sum

The potential and pressure are the literal current-band sums constructed in ActualCurrentParticularPhysical. Their modes are identified with the same canonical solver used by the correction cycle. On a valid current polar chart, the curl is therefore the actual particular velocity increment, with its physical scale and moving frame. No output representation is an input to these identities.

theorem NavierStokes.ActualCurrentParticularAssembly.space_sum_apply {ι : Type u_1} (s : Finset ι) (v : ι → ProblemStatement.Space) (k : Fin 3) : (∑ b ∈ s, v b).ofLp k = ∑ b ∈ s, (v b).ofLp k

theorem NavierStokes.ActualCurrentParticularAssembly.localPotential_eq_sum {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualInitialization.Index B N0)) (n : ℕ) : ActualCurrentParticularPhysical.localPotential (ActualCycleParameters.particularState x) n = fun (w : ProblemStatement.SpaceTime) => ∑ l ∈ x.coefficients.labels n, ∑ j ∈ ParticularWaveAssembly.modes x.coefficients.residualBand, ActualCurrentParticularPhysical.localPotentialMode (ActualCycleParameters.particularState x) (l.2, l.1) j n w

theorem NavierStokes.ActualCurrentParticularAssembly.localPressure_eq_sum {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualInitialization.Index B N0)) (n : ℕ) : ActualCurrentParticularPhysical.localPressure (ActualCycleParameters.particularState x) n = fun (w : ProblemStatement.SpaceTime) => ∑ l ∈ x.coefficients.labels n, ∑ j ∈ ParticularWaveAssembly.modes x.coefficients.residualBand, ActualCurrentParticularPhysical.localPressureMode (ActualCycleParameters.particularState x) (l.2, l.1) j n w

theorem NavierStokes.ActualCurrentParticularAssembly.nativeMode_eq {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualInitialization.Index B N0)) (l : ActualInitialization.Index B N0) (j : ℤ) (n : ℕ) (z : PhysicalResidualBridge.Cylinder) (k : Fin 3) : ActualParticularCycleData.nativeMode x l j n z k = (ActualCurrentParticularPhysical.nativeVelocity (ActualCycleParameters.particularState x) (l.2, l.1) j n (ActualWaveRegularity.particularChart z) k).re

theorem NavierStokes.ActualCurrentParticularAssembly.particularVelocity_eq_sum {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {σ : ℝ} (H : ActualParticularCycleData.Invariant σ x) (n : ℕ) (z : PhysicalResidualBridge.Cylinder) (k : Fin 3) : (ActualCycleParameters.fixedParameters B N0).particularVelocity x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state n z k = ∑ l ∈ x.coefficients.labels n, ∑ j ∈ ParticularWaveAssembly.modes x.coefficients.residualBand, (ActualCurrentParticularPhysical.nativeVelocity (ActualCycleParameters.particularState x) (l.2, l.1) j n (ActualWaveRegularity.particularChart z) k).re

theorem NavierStokes.ActualCurrentParticularAssembly.particularPressure_eq_sum {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {σ : ℝ} (H : ActualParticularCycleData.Invariant σ x) (n : ℕ) (z : PhysicalResidualBridge.Cylinder) : (ActualCycleParameters.fixedParameters B N0).particularPressure x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state n z = ∑ l ∈ x.coefficients.labels n, ∑ j ∈ ParticularWaveAssembly.modes x.coefficients.residualBand, (ActualCurrentParticularPhysical.nativePressure (ActualCycleParameters.particularState x) (l.2, l.1) j n (ActualWaveRegularity.particularChart z)).re

theorem NavierStokes.ActualCurrentParticularAssembly.nativeMap_eq_graph (n : ℕ) (z : ProblemStatement.SpaceTime) : PhysicalParticularWave.nativeMap CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n) z = ActualWaveRegularity.particularChart (PhysicalResidualTZ.graphMapTZ (ActualCycleResidualBounds.actualBandGraph n) z)

theorem NavierStokes.ActualCurrentParticularAssembly.velocityMap_apply (n : ℕ) (v : PhysicalResidualBridge.Cylinder → Fin 3 → ℝ) (z : ProblemStatement.SpaceTime) (k : Fin 3) : ((CyclePhysicalPrefixes.velocityMap (ActualCycleResidualBounds.actualBandGraph n)) v z).ofLp k = ChartScales.Q n ^ (-CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) * v (PhysicalResidualTZ.graphMapTZ (ActualCycleResidualBounds.actualBandGraph n) z) k

theorem NavierStokes.ActualCurrentParticularAssembly.pressureMap_apply (n : ℕ) (p : PhysicalResidualBridge.Cylinder → ℝ) (z : ProblemStatement.SpaceTime) : (CyclePhysicalPrefixes.pressureMap (ActualCycleResidualBounds.actualBandGraph n)) p z = ChartScales.Q n ^ (-2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) * p (PhysicalResidualTZ.graphMapTZ (ActualCycleResidualBounds.actualBandGraph n) z)

theorem NavierStokes.ActualCurrentParticularAssembly.localPotential_curl_eq_sum {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {σ : ℝ} (H : ActualParticularCycleData.Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hw : w ∈ ActualMeanPotentialRealization.cartesianDomain a i) (hm : ActualCurrentParticularPhysical.nativePoint n w ∈ ActualCurrentParticularPhysical.nativeDomain) : SpatialCurl.spatialCurl (ActualCurrentParticularPhysical.localPotential (ActualCycleParameters.particularState x) n) w = ∑ l ∈ x.coefficients.labels n, ∑ j ∈ ParticularWaveAssembly.modes x.coefficients.residualBand, SpatialCurl.spatialCurl (ActualCurrentParticularPhysical.localPotentialMode (ActualCycleParameters.particularState x) (l.2, l.1) j n) w

theorem NavierStokes.ActualCurrentParticularAssembly.localPotential_curl_components {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {σ : ℝ} (H : ActualParticularCycleData.Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {z : ProblemStatement.SpaceTime} (hz : z ∈ PhysicalCurlCovariance.validCylindrical a i) (hm : PhysicalParticularWave.nativeMap CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n) z ∈ ActualCurrentParticularPhysical.nativeDomain) (k : Fin 3) : ((CylindricalResidual.frame (-z.2.ofLp 1)) (SpatialCurl.spatialCurl (ActualCurrentParticularPhysical.localPotential (ActualCycleParameters.particularState x) n) (z.1, CylindricalResidual.chart z.2))).ofLp k = ChartScales.Q n ^ (-CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) * (ActualCycleParameters.fixedParameters B N0).particularVelocity x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state n (PhysicalResidualTZ.graphMapTZ (ActualCycleResidualBounds.actualBandGraph n) z) k

theorem NavierStokes.ActualCurrentParticularAssembly.localPotential_curl_forward {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {σ : ℝ} (H : ActualParticularCycleData.Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {z : ProblemStatement.SpaceTime} (hz : z ∈ PhysicalCurlCovariance.validCylindrical a i) (hm : PhysicalParticularWave.nativeMap CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n) z ∈ ActualCurrentParticularPhysical.nativeDomain) : SpatialCurl.spatialCurl (ActualCurrentParticularPhysical.localPotential (ActualCycleParameters.particularState x) n) (z.1, CylindricalResidual.chart z.2) = (CyclePhysicalPrefixes.polarVelocityMap a i) ((CyclePhysicalPrefixes.velocityMap (ActualCycleResidualBounds.actualBandGraph n)) ((ActualCycleParameters.fixedParameters B N0).particularVelocity x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state n)) (z.1, CylindricalResidual.chart z.2)

theorem NavierStokes.ActualCurrentParticularAssembly.localPotential_curl {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {σ : ℝ} (H : ActualParticularCycleData.Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hw : w ∈ ActualMeanPotentialRealization.cartesianDomain a i) (hm : ActualCurrentParticularPhysical.nativePoint n w ∈ ActualCurrentParticularPhysical.nativeDomain) : SpatialCurl.spatialCurl (ActualCurrentParticularPhysical.localPotential (ActualCycleParameters.particularState x) n) w = (CyclePhysicalPrefixes.polarVelocityMap a i) ((CyclePhysicalPrefixes.velocityMap (ActualCycleResidualBounds.actualBandGraph n)) ((ActualCycleParameters.fixedParameters B N0).particularVelocity x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state n)) w

theorem NavierStokes.ActualCurrentParticularAssembly.localPressure_eq {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {σ : ℝ} (H : ActualParticularCycleData.Invariant σ x) (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hw : w ∈ ActualMeanPotentialRealization.cartesianDomain a i) : ActualCurrentParticularPhysical.localPressure (ActualCycleParameters.particularState x) n w = (CyclePhysicalPrefixes.polarPressureMap a i) ((CyclePhysicalPrefixes.pressureMap (ActualCycleResidualBounds.actualBandGraph n)) ((ActualCycleParameters.fixedParameters B N0).particularPressure x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state n)) w

theorem NavierStokes.ActualCurrentParticularAssembly.nativePoint_mem_of_chartDomain {qbig : ℝ} {n : ℕ} {a : ℝ} {i : PolarCharts.Index} {w : ProblemStatement.SpaceTime} (hw : w ∈ ActualPhysicalPrefixFields.cartesianChartDomain qbig n a i) : ActualCurrentParticularPhysical.nativePoint n w ∈ ActualCurrentParticularPhysical.nativeDomain

theorem NavierStokes.ActualCurrentParticularAssembly.localPotential_curl_eqOn {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {σ : ℝ} (H : ActualParticularCycleData.Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (qbig : ℝ) (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) : Set.EqOn (SpatialCurl.spatialCurl (ActualCurrentParticularPhysical.localPotential (ActualCycleParameters.particularState x) n)) ((CyclePhysicalPrefixes.polarVelocityMap a i) ((CyclePhysicalPrefixes.velocityMap (ActualCycleResidualBounds.actualBandGraph n)) ((ActualCycleParameters.fixedParameters B N0).particularVelocity x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state n))) (ActualPhysicalPrefixFields.cartesianChartDomain qbig n a i)

The literal finite potential has exactly the physical curl required by the particular stage of the correction cycle, throughout each valid current chart.

theorem NavierStokes.ActualCurrentParticularAssembly.localPressure_eqOn {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {σ : ℝ} (H : ActualParticularCycleData.Invariant σ x) (qbig : ℝ) (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) : Set.EqOn (ActualCurrentParticularPhysical.localPressure (ActualCycleParameters.particularState x) n) ((CyclePhysicalPrefixes.polarPressureMap a i) ((CyclePhysicalPrefixes.pressureMap (ActualCycleResidualBounds.actualBandGraph n)) ((ActualCycleParameters.fixedParameters B N0).particularPressure x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state n))) (ActualPhysicalPrefixFields.cartesianChartDomain qbig n a i)

The pressure uses the same finite harmonic and label sums and the square of the physical velocity scale.

Exact exterior vanishing of the actual mean fields

The native moving support is the nominal profile interval itself. Squaring the exact normalized-radius identity places the physical support in the closed nominal active annulus, without enlarging either edge. This applies to the literal initialized fields and to every mean stage of the same coherent cycle.

theorem NavierStokes.ActualMeanExterior.active_of_mem_tsupport {degree : ℝ} {N Δ : ℕ} (D : PhysicalMeanJetBounds.CoherentFamily CorrectionInitialization.ActualPrimary.h degree N Δ CorrectionInitialization.ActualPrimary.standardRegion.carrier ℝ) (Hm : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion CorrectionInitialization.ActualPrimary.commonGauge.radial.inner CorrectionInitialization.ActualPrimary.commonGauge.radial.outer D.native) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ ChartScales.Q N) (hs : w ∈ tsupport D.field) : w ∈ ActualPolarCoverage.active

The actual moving radial support gives the closed nominal active annulus at every physical support point with a comparable band.

theorem NavierStokes.ActualMeanExterior.not_mem_tsupport_of_exterior {degree : ℝ} {N Δ : ℕ} (D : PhysicalMeanJetBounds.CoherentFamily CorrectionInitialization.ActualPrimary.h degree N Δ CorrectionInitialization.ActualPrimary.standardRegion.carrier ℝ) (Hm : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion CorrectionInitialization.ActualPrimary.commonGauge.radial.inner CorrectionInitialization.ActualPrimary.commonGauge.radial.outer D.native) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ ChartScales.Q N) (he : w ∉ ActualPolarCoverage.active) : w ∉ tsupport D.field

theorem NavierStokes.ActualMeanExterior.exterior_zero_germs {degree : ℝ} {N Δ : ℕ} (D : PhysicalMeanJetBounds.CoherentFamily CorrectionInitialization.ActualPrimary.h degree N Δ CorrectionInitialization.ActualPrimary.standardRegion.carrier ℝ) (Hm : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion CorrectionInitialization.ActualPrimary.commonGauge.radial.inner CorrectionInitialization.ActualPrimary.commonGauge.radial.outer D.native) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ ChartScales.Q N) (he : w ∉ ActualPolarCoverage.active) : (D.field =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0) ∧ D.angularField =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

Scalar coefficients and their Cartesian angular realization vanish as germs on the exterior of the closed nominal active annulus.

theorem NavierStokes.ActualMeanExterior.exterior_zero {degree : ℝ} {N Δ : ℕ} (D : PhysicalMeanJetBounds.CoherentFamily CorrectionInitialization.ActualPrimary.h degree N Δ CorrectionInitialization.ActualPrimary.standardRegion.carrier ℝ) (Hm : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion CorrectionInitialization.ActualPrimary.commonGauge.radial.inner CorrectionInitialization.ActualPrimary.commonGauge.radial.outer D.native) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ ChartScales.Q N) (he : w ∉ ActualPolarCoverage.active) : D.field w = 0 ∧ D.angularField w = 0

theorem NavierStokes.ActualMeanExterior.actualAngularData_exterior {degree : ℝ} {N Δ : ℕ} (D : PhysicalMeanJetBounds.CoherentFamily CorrectionInitialization.ActualPrimary.h degree N Δ CorrectionInitialization.ActualPrimary.standardRegion.carrier ℝ) (Hm : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion CorrectionInitialization.ActualPrimary.commonGauge.radial.inner CorrectionInitialization.ActualPrimary.commonGauge.radial.outer D.native) (qbig : ℝ) (hbound : qbig ≤ ChartScales.Q N) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w < qbig) (he : w ∉ ActualPolarCoverage.active) : DirectAngularDiagonal.angularField (ActualMeanStageData.actualAngularData D Hm qbig hbound).scalar w = 0

The direct angular-field constructor used for both angular velocity and stream potentials retains the same exact exterior zero.

The same initialized fields

theorem NavierStokes.ActualMeanExterior.initialAngular_exterior (B N0 N : ℕ) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ ChartScales.Q N) (he : w ∉ ActualPolarCoverage.active) : (ActualMeanPhysicalData.initialAngularFamily B N0 N).field w = 0 ∧ (ActualMeanPhysicalData.initialAngularFamily B N0 N).angularField w = 0

theorem NavierStokes.ActualMeanExterior.initialPressure_exterior (B N0 N : ℕ) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ ChartScales.Q N) (he : w ∉ ActualPolarCoverage.active) : (ActualMeanPhysicalData.initialPressureFamily B N0 N).field w = 0 ∧ (ActualMeanPhysicalData.initialPressureFamily B N0 N).angularField w = 0

theorem NavierStokes.ActualMeanExterior.initialTemporal_exterior (B N0 N : ℕ) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ ChartScales.Q N) (he : w ∉ ActualPolarCoverage.active) : (ActualMeanPhysicalData.initialTemporalFamily B N0 N).field w = 0 ∧ (ActualMeanPhysicalData.initialTemporalFamily B N0 N).angularField w = 0

theorem NavierStokes.ActualMeanExterior.initialRank_exterior (B N0 N : ℕ) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ ChartScales.Q N) (he : w ∉ ActualPolarCoverage.active) : (ActualMeanPhysicalData.initialRankFamily B N0 N).field w = 0 ∧ (ActualMeanPhysicalData.initialRankFamily B N0 N).angularField w = 0

theorem NavierStokes.ActualMeanExterior.initialStream_exterior (B N0 N : ℕ) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ ChartScales.Q N) (he : w ∉ ActualPolarCoverage.active) : (ActualMeanPhysicalData.initialStreamFamily B N0 N).field w = 0 ∧ (ActualMeanPhysicalData.initialStreamFamily B N0 N).angularField w = 0

The full initialized stream is the literal temporal-plus-rank stream.

Every stage of the same coherent cycle

theorem NavierStokes.ActualMeanExterior.cycleAngular_exterior {B N0 N : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} (H : ActualMeanPhysicalData.InitialCycleInput B N0 N p) (j : ℕ) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ ChartScales.Q N) (he : w ∉ ActualPolarCoverage.active) : ((ActualMeanPhysicalData.initialCycleData H).angularFamily j).field w = 0 ∧ ((ActualMeanPhysicalData.initialCycleData H).angularFamily j).angularField w = 0

theorem NavierStokes.ActualMeanExterior.cyclePressure_exterior {B N0 N : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} (H : ActualMeanPhysicalData.InitialCycleInput B N0 N p) (j : ℕ) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ ChartScales.Q N) (he : w ∉ ActualPolarCoverage.active) : ((ActualMeanPhysicalData.initialCycleData H).pressureFamily j).field w = 0 ∧ ((ActualMeanPhysicalData.initialCycleData H).pressureFamily j).angularField w = 0

theorem NavierStokes.ActualMeanExterior.cycleAngularIncrement_exterior {B N0 N : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} (H : ActualMeanPhysicalData.InitialCycleInput B N0 N p) (j : ℕ) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ ChartScales.Q N) (he : w ∉ ActualPolarCoverage.active) : ((ActualMeanPhysicalData.initialCycleData H).angularIncrementFamily j).field w = 0 ∧ ((ActualMeanPhysicalData.initialCycleData H).angularIncrementFamily j).angularField w = 0

theorem NavierStokes.ActualMeanExterior.cyclePressureIncrement_exterior {B N0 N : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} (H : ActualMeanPhysicalData.InitialCycleInput B N0 N p) (j : ℕ) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ ChartScales.Q N) (he : w ∉ ActualPolarCoverage.active) : ((ActualMeanPhysicalData.initialCycleData H).pressureIncrementFamily j).field w = 0 ∧ ((ActualMeanPhysicalData.initialCycleData H).pressureIncrementFamily j).angularField w = 0

theorem NavierStokes.ActualMeanExterior.cycleTemporal_exterior {B N0 N : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} (H : ActualMeanPhysicalData.InitialCycleInput B N0 N p) (j : ℕ) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ ChartScales.Q N) (he : w ∉ ActualPolarCoverage.active) : ((ActualMeanPhysicalData.initialCycleData H).temporalFamily j).field w = 0 ∧ ((ActualMeanPhysicalData.initialCycleData H).temporalFamily j).angularField w = 0

theorem NavierStokes.ActualMeanExterior.cycleRank_exterior {B N0 N : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} (H : ActualMeanPhysicalData.InitialCycleInput B N0 N p) (j : ℕ) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ ChartScales.Q N) (he : w ∉ ActualPolarCoverage.active) : ((ActualMeanPhysicalData.initialCycleData H).rankFamily j).field w = 0 ∧ ((ActualMeanPhysicalData.initialCycleData H).rankFamily j).angularField w = 0

theorem NavierStokes.ActualMeanExterior.cycleStream_exterior {B N0 N : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} (H : ActualMeanPhysicalData.InitialCycleInput B N0 N p) (j : ℕ) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ ChartScales.Q N) (he : w ∉ ActualPolarCoverage.active) : ((ActualMeanPhysicalData.initialCycleData H).streamFamily j).field w = 0 ∧ ((ActualMeanPhysicalData.initialCycleData H).streamFamily j).angularField w = 0

Exterior germs for physical stages

One certificate supplies support and axis-germ bounds. The existing exterior lemmas on closed sublevels remain available; they imply this local certificate.

theorem NavierStokes.ActualCandidateAssembly.axis_not_active {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (ha : PhysicalGraphBounds.radialProjection w = 0) : w ∉ ActualPolarCoverage.active

theorem NavierStokes.ActualCandidateAssembly.eventually_not_active {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (he : w ∉ ActualPolarCoverage.active) : ∀ᶠ (y : ProblemStatement.SpaceTime) in nhds w, y ∉ ActualPolarCoverage.active

The exterior of the active annulus is open within the preterminal region: the profile radius is continuous there and the annulus is its preimage of a closed interval.

structure NavierStokes.ActualCandidateAssembly.PhysicalStage (B N0 : ℕ) {V : Type u_1} [Zero V] (f : ProblemStatement.SpaceTime → V) : Prop

A stage field of the actual candidate: zero near every point of the physical domain outside the active annulus.

• exterior (w : ProblemStatement.SpaceTime) : w ∈ ActualCandidateConstruction.physicalDomain B N0 → w ∉ ActualPolarCoverage.active → f =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

  The field vanishes in a neighborhood of each exterior point.

theorem NavierStokes.ActualCandidateAssembly.PhysicalStage.of_eq_zero {B N0 : ℕ} {V : Type u_1} [Zero V] {f : ProblemStatement.SpaceTime → V} (hz : ∀ w ∈ ActualCandidateConstruction.physicalDomain B N0, w ∉ ActualPolarCoverage.active → f w = 0) : PhysicalStage B N0 f

A pointwise exterior identity suffices, since the exterior is open in the domain.

theorem NavierStokes.ActualCandidateAssembly.PhysicalStage.zero {B N0 : ℕ} {V : Type u_1} [Zero V] : PhysicalStage B N0 fun (x : ProblemStatement.SpaceTime) => 0

The zero field is a physical stage.

theorem NavierStokes.ActualCandidateAssembly.PhysicalStage.eq_zero {B N0 : ℕ} {V : Type u_1} [Zero V] {f : ProblemStatement.SpaceTime → V} (hf : PhysicalStage B N0 f) {w : ProblemStatement.SpaceTime} (hw : w ∈ ActualCandidateConstruction.physicalDomain B N0) (he : w ∉ ActualPolarCoverage.active) : f w = 0

theorem NavierStokes.ActualCandidateAssembly.PhysicalStage.support {B N0 : ℕ} {V : Type u_2} [NormedAddCommGroup V] {f : ProblemStatement.SpaceTime → V} (hf : PhysicalStage B N0 f) : MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h PhysicalStageSupport.actualOuterConstant (ActualCandidateConstruction.qbig B N0) f

Shrinking support: a support point lies in the active annulus, whose outer edge is below the outer constant.

theorem NavierStokes.ActualCandidateAssembly.PhysicalStage.axisZeroOn {B N0 : ℕ} {f : ProblemStatement.VelocityField} (hf : PhysicalStage B N0 f) : GermCandidateAssembly.AxisZeroOn (MixedAxisPreservation.localDomain CorrectionInitialization.ActualPrimary.h (ActualCandidateConstruction.qbig B N0)) f

The axis of the local domain lies outside the active annulus, so the hub's axis zero germ is a projection.

theorem NavierStokes.ActualCandidateAssembly.PhysicalStage.add {B N0 : ℕ} {V : Type u_2} [AddZeroClass V] {f g : ProblemStatement.SpaceTime → V} (hf : PhysicalStage B N0 f) (hg : PhysicalStage B N0 g) : PhysicalStage B N0 (f + g)

Exterior zero germs are preserved by addition.

The finite initialization, without the base fields

noncomputable def NavierStokes.ActualCandidateAssembly.initialPotential (B N0 : ℕ) : ProblemStatement.VelocityField

Initial potential, given by InitialPhysicalData.potential B N0 + ActualCandidateConstruction.streamMeanStages B N0 0.

Equations

• NavierStokes.ActualCandidateAssembly.initialPotential B N0 = NavierStokes.InitialPhysicalData.potential B N0 + NavierStokes.ActualCandidateConstruction.streamMeanStages B N0 0

noncomputable def NavierStokes.ActualCandidateAssembly.initialPressure (B N0 : ℕ) : ProblemStatement.PressureField

Initial pressure, given by InitialPhysicalData.pressure B N0 + ActualCandidateConstruction.pressureMeanStages B N0 0.

Equations

• NavierStokes.ActualCandidateAssembly.initialPressure B N0 = NavierStokes.InitialPhysicalData.pressure B N0 + NavierStokes.ActualCandidateConstruction.pressureMeanStages B N0 0

noncomputable def NavierStokes.ActualCandidateAssembly.initialDirect (B N0 : ℕ) : ProblemStatement.VelocityField

Initial direct, given by ActualCandidateConstruction.angularMeanStages B N0 0.

Equations

• NavierStokes.ActualCandidateAssembly.initialDirect B N0 = NavierStokes.ActualCandidateConstruction.angularMeanStages B N0 0

noncomputable def NavierStokes.ActualCandidateAssembly.initialDirectData (B N0 : ℕ) : DirectAngularDiagonal.AngularData (LocalAngularDiagonal.localSlowDomain CorrectionInitialization.ActualPrimary.h (ActualCandidateConstruction.qbig B N0))

Initial direct data, constructed using ActualMeanStageData.initialAngularData.

Equations

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

theorem NavierStokes.ActualCandidateAssembly.initialDirectData_field (B N0 : ℕ) : DirectAngularDiagonal.angularField (initialDirectData B N0).scalar = initialDirect B N0

theorem NavierStokes.ActualCandidateAssembly.initialPotential_eq_stage (B N0 : ℕ) : initialPotential B N0 = (ActualCandidateConstruction.initialPotentialStage B N0 (InitialPhysicalData.copyPotential B N0)).field

theorem NavierStokes.ActualCandidateAssembly.initialPotential_eq_increment (B N0 : ℕ) : initialPotential B N0 = ActualPhysicalStageBounds.initialIncrement (InitialPhysicalData.potentialWaveData B N0) (ActualPhysicalStageBounds.actualInitialTemporalInput B N0 (ActualCandidateConstruction.firstBand B N0) ⋯) (ActualPhysicalStageBounds.actualInitialRankInput B N0 (ActualCandidateConstruction.firstBand B N0) ⋯)

theorem NavierStokes.ActualCandidateAssembly.initialPressure_eq_increment (B N0 : ℕ) : initialPressure B N0 = ActualPhysicalStageBounds.initialPressureIncrement (InitialPhysicalData.pressureWaveData B N0) (ActualPhysicalStageBounds.actualInitialPressureInput B N0 (ActualCandidateConstruction.firstBand B N0) ⋯)

theorem NavierStokes.ActualCandidateAssembly.initialPotential_smooth (B N0 : ℕ) : ContDiffOn ℝ (↑⊤) (initialPotential B N0) (ActualCandidateConstruction.physicalDomain B N0)

theorem NavierStokes.ActualCandidateAssembly.initialPressure_smooth (B N0 : ℕ) : ContDiffOn ℝ (↑⊤) (initialPressure B N0) (ActualCandidateConstruction.physicalDomain B N0)

theorem NavierStokes.ActualCandidateAssembly.initialDirect_smooth (B N0 : ℕ) : ContDiffOn ℝ (↑⊤) (initialDirect B N0) (ActualCandidateConstruction.physicalDomain B N0)

Exact exterior coordinates

theorem NavierStokes.ActualCandidateAssembly.physicalRadiusX_eq (w : ProblemStatement.SpaceTime) : PhysicalWaveSum.physicalPosition w 0 ^ 2 / (2 * PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w) = (SlowBorelBase.cartesianChart CorrectionInitialization.ActualPrimary.h w).2.1

theorem NavierStokes.ActualCandidateAssembly.initialDirect_exterior (B N0 : ℕ) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ ActualCandidateConstruction.qbig B N0) (he : w ∉ ActualPolarCoverage.active) : initialDirect B N0 w = 0

theorem NavierStokes.ActualCandidateAssembly.initialPotential_exterior (B N0 : ℕ) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ ActualCandidateConstruction.qbig B N0) (he : w ∉ ActualPolarCoverage.active) : initialPotential B N0 w = 0

theorem NavierStokes.ActualCandidateAssembly.initialPressure_exterior (B N0 : ℕ) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ ActualCandidateConstruction.qbig B N0) (he : w ∉ ActualPolarCoverage.active) : initialPressure B N0 w = 0

theorem NavierStokes.ActualCandidateAssembly.initialPotential_stage (B N0 : ℕ) : PhysicalStage B N0 (initialPotential B N0)

The initial potential has an exterior zero germ on its physical domain.

theorem NavierStokes.ActualCandidateAssembly.initialPressure_stage (B N0 : ℕ) : PhysicalStage B N0 (initialPressure B N0)

The initial pressure has an exterior zero germ on its physical domain.

theorem NavierStokes.ActualCandidateAssembly.initialDirect_stage (B N0 : ℕ) : PhysicalStage B N0 (initialDirect B N0)

The initial direct field has an exterior zero germ on its physical domain.

theorem NavierStokes.ActualCandidateAssembly.initialPotential_support (B N0 : ℕ) : MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h PhysicalStageSupport.actualOuterConstant (ActualCandidateConstruction.qbig B N0) (initialPotential B N0)

theorem NavierStokes.ActualCandidateAssembly.initialPressure_support (B N0 : ℕ) : MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h PhysicalStageSupport.actualOuterConstant (ActualCandidateConstruction.qbig B N0) (initialPressure B N0)

theorem NavierStokes.ActualCandidateAssembly.initialDirect_support (B N0 : ℕ) : MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h PhysicalStageSupport.actualOuterConstant (ActualCandidateConstruction.qbig B N0) (initialDirect B N0)

theorem NavierStokes.ActualCandidateAssembly.initialPotential_axisZeroOn (B N0 : ℕ) : GermCandidateAssembly.AxisZeroOn (MixedAxisPreservation.localDomain CorrectionInitialization.ActualPrimary.h (ActualCandidateConstruction.qbig B N0)) (initialPotential B N0)

The literal zeroth potential and pressure retain the base

noncomputable def NavierStokes.ActualCandidateAssembly.zerothPotential (B N0 : ℕ) : ProblemStatement.VelocityField

Zeroth potential, given by `TailGaugePotential.finalPotential certificate modulation upper B

• initialPotential B N0`.

Equations

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

noncomputable def NavierStokes.ActualCandidateAssembly.zerothPressure (B N0 : ℕ) : ProblemStatement.PressureField

Zeroth pressure, given by FinalSlowBase.pressure certificate modulation upper B + initialPressure B N0.

Equations

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

theorem NavierStokes.ActualCandidateAssembly.zerothPotential_eq_initialPotential (B N0 : ℕ) : zerothPotential B N0 = ActualPhysicalStageBounds.initialPotential CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B (InitialPhysicalData.potentialWaveData B N0) (ActualPhysicalStageBounds.actualInitialTemporalInput B N0 (ActualCandidateConstruction.firstBand B N0) ⋯) (ActualPhysicalStageBounds.actualInitialRankInput B N0 (ActualCandidateConstruction.firstBand B N0) ⋯)

theorem NavierStokes.ActualCandidateAssembly.zerothPotential_smooth (B N0 : ℕ) : ContDiffOn ℝ (↑⊤) (zerothPotential B N0) (ActualCandidateConstruction.physicalDomain B N0)

theorem NavierStokes.ActualCandidateAssembly.zerothPressure_smooth (B N0 : ℕ) : ContDiffOn ℝ (↑⊤) (zerothPressure B N0) (ActualCandidateConstruction.physicalDomain B N0)

The particular fields come from the same current state

The valid-band representative uses the common physical floor. Its local formulas are the actual current solves, with the initializer's label order converted by ActualCycleParameters.particularState inside the producer.

noncomputable def NavierStokes.ActualCandidateAssembly.particularPotential (B N0 j : ℕ) : ProblemStatement.VelocityField

Particular potential, given by ActualValidBandWaves.potential (ActualCandidateConstruction.cycle B N0 j) (ActualCandidateConstruction.firstBand B N0).

Equations

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

noncomputable def NavierStokes.ActualCandidateAssembly.particularPressure (B N0 j : ℕ) : ProblemStatement.PressureField

Particular pressure, constructed using ActualValidBandWaves.pressure.

Equations

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

Mean fields on the exact residual-comparison charts

theorem NavierStokes.ActualCandidateAssembly.meanChart_mem (B N0 n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hw : w ∈ ActualPhysicalPrefixFields.cartesianChartDomain (ActualCandidateConstruction.qbig B N0) n a i) : (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n ((ActualCandidateConstruction.meanAtlas B N0).gap n) w).2.1 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier

theorem NavierStokes.ActualCandidateAssembly.initial_oscillation (B N0 n : ℕ) (x : PhysicalResidualBridge.Cylinder) (i : Fin 3) : (ActualCandidateConstruction.cycle B N0 0).state.oscillation n x i = ∑ l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n, (CorrectionInitialization.ActualPrimary.piece CorrectionInitialization.ActualPrimary.standardRegion l.2 l.1).velocity n x i

theorem NavierStokes.ActualCandidateAssembly.initial_oscillatoryPressure (B N0 n : ℕ) (x : PhysicalResidualBridge.Cylinder) : (ActualCandidateConstruction.cycle B N0 0).state.oscillatoryPressure n x = ∑ l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n, (CorrectionInitialization.ActualPrimary.piece CorrectionInitialization.ActualPrimary.standardRegion l.2 l.1).pressure n x

theorem NavierStokes.ActualCandidateAssembly.initialVelocity_on_cylinder (B N0 n d : ℕ) {z : ProblemStatement.SpaceTime} (ht : z.1 < 1) (hr : 0 < z.2.ofLp 0) (hs : (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n d (z.1, CylindricalResidual.chart z.2)).2.1 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier) : (CyclePhysicalPrefixes.velocityMap (ActualCandidateConstruction.graph n)) ((ActualCandidateConstruction.cycle B N0 0).state.oscillation n) z = (CylindricalResidual.frame (-z.2.ofLp 1)) (SpatialCurl.spatialCurl (InitialPhysicalData.potential B N0) (z.1, CylindricalResidual.chart z.2))

theorem NavierStokes.ActualCandidateAssembly.initialPressure_on_cylinder (B N0 n d : ℕ) {z : ProblemStatement.SpaceTime} (ht : z.1 < 1) (hr : 0 < z.2.ofLp 0) (hs : (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n d (z.1, CylindricalResidual.chart z.2)).2.1 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier) : (CyclePhysicalPrefixes.pressureMap (ActualCandidateConstruction.graph n)) ((ActualCandidateConstruction.cycle B N0 0).state.oscillatoryPressure n) z = InitialPhysicalData.pressure B N0 (z.1, CylindricalResidual.chart z.2)

theorem NavierStokes.ActualCandidateAssembly.initialWavePotential_on_chart (B N0 n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) : Set.EqOn (SpatialCurl.spatialCurl (InitialPhysicalData.potential B N0)) (ActualCandidateConstruction.chartWaveParts B N0 a i n 0) (ActualPhysicalPrefixFields.cartesianChartDomain (ActualCandidateConstruction.qbig B N0) n a i)

theorem NavierStokes.ActualCandidateAssembly.initialWavePressure_on_chart (B N0 n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) : Set.EqOn (InitialPhysicalData.pressure B N0) (ActualCandidateConstruction.chartWavePressureParts B N0 a i n 0) (ActualPhysicalPrefixFields.cartesianChartDomain (ActualCandidateConstruction.qbig B N0) n a i)

theorem NavierStokes.ActualCandidateAssembly.chartDomain_band (B N0 n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hw : w ∈ ActualPhysicalPrefixFields.cartesianChartDomain (ActualCandidateConstruction.qbig B N0) n a i) : w ∈ ValidDyadicBandCover.band CorrectionInitialization.ActualPrimary.h n

theorem NavierStokes.ActualCandidateAssembly.direct_on_chart {B N0 : ℕ} (M : ActualCandidateConstruction.MeanCycleInput B N0) (j n : ℕ) (hn : ActualCandidateConstruction.firstBand B N0 ≤ n) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) : Set.EqOn (LocalAngularDiagonal.rawSeries (ActualCandidateConstruction.directData M) j) (ActualCandidateConstruction.chartDirectStages B N0 a i n j) (ActualPhysicalPrefixFields.cartesianChartDomain (ActualCandidateConstruction.qbig B N0) n a i)

theorem NavierStokes.ActualCandidateAssembly.stream_on_chart {B N0 : ℕ} (M : ActualCandidateConstruction.MeanCycleInput B N0) (j n : ℕ) (hn : ActualCandidateConstruction.firstBand B N0 ≤ n) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) : Set.EqOn (SpatialCurl.spatialCurl (ActualCandidateConstruction.streamMeanStages B N0 j)) (ActualCandidateConstruction.chartStreamParts B N0 a i n j) (ActualPhysicalPrefixFields.cartesianChartDomain (ActualCandidateConstruction.qbig B N0) n a i)

theorem NavierStokes.ActualCandidateAssembly.meanPressure_on_chart {B N0 : ℕ} (M : ActualCandidateConstruction.MeanCycleInput B N0) (j n : ℕ) (hn : ActualCandidateConstruction.firstBand B N0 ≤ n) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) : Set.EqOn (ActualCandidateConstruction.pressureMeanStages B N0 j) (ActualCandidateConstruction.chartMeanPressureParts B N0 a i n j) (ActualPhysicalPrefixFields.cartesianChartDomain (ActualCandidateConstruction.qbig B N0) n a i)

theorem NavierStokes.ActualCandidateAssembly.stream_exterior {B N0 : ℕ} (M : ActualCandidateConstruction.MeanCycleInput B N0) (j : ℕ) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ ActualCandidateConstruction.qbig B N0) (he : w ∉ ActualPolarCoverage.active) : ActualCandidateConstruction.streamMeanStages B N0 j w = 0

theorem NavierStokes.ActualCandidateAssembly.direct_exterior {B N0 : ℕ} (M : ActualCandidateConstruction.MeanCycleInput B N0) (j : ℕ) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ ActualCandidateConstruction.qbig B N0) (he : w ∉ ActualPolarCoverage.active) : LocalAngularDiagonal.rawSeries (ActualCandidateConstruction.directData M) j w = 0

theorem NavierStokes.ActualCandidateAssembly.meanPressure_exterior {B N0 : ℕ} (M : ActualCandidateConstruction.MeanCycleInput B N0) (j : ℕ) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ ActualCandidateConstruction.qbig B N0) (he : w ∉ ActualPolarCoverage.active) : ActualCandidateConstruction.pressureMeanStages B N0 j w = 0

theorem NavierStokes.ActualCandidateAssembly.stream_axisZeroOn {B N0 : ℕ} (M : ActualCandidateConstruction.MeanCycleInput B N0) (j : ℕ) : GermCandidateAssembly.AxisZeroOn (MixedAxisPreservation.localDomain CorrectionInitialization.ActualPrimary.h (ActualCandidateConstruction.qbig B N0)) (ActualCandidateConstruction.streamMeanStages B N0 j)

The actual native run supplies every mean and signed request

noncomputable def NavierStokes.ActualCandidateAssembly.runData (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) : ActualStageEstimates.RunData B N0

Run data, bundling invariant, step, particular.

Equations

• NavierStokes.ActualCandidateAssembly.runData B N0 hN = { invariant := ⋯, step := NavierStokes.ActualCyclePreservation.stateStepData B N0 hN, particular := ⋯ }

theorem NavierStokes.ActualCandidateAssembly.meanCycleInput (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) : ActualCandidateConstruction.MeanCycleInput B N0

theorem NavierStokes.ActualCandidateAssembly.postParticularResult (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) : ActualParticularMeanGain.Result (ActualCandidateConstruction.cycle B N0 j) (ActualIterationLedger.sigma j)

noncomputable def NavierStokes.ActualCandidateAssembly.signedPotential (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) : ProblemStatement.VelocityField

Signed potential, constructed using ActualSignedExterior.cyclePotential.

Equations

• NavierStokes.ActualCandidateAssembly.signedPotential B N0 hN j = NavierStokes.ActualSignedExterior.cyclePotential (NavierStokes.ActualCandidateConstruction.cycle B N0 j) ⋯ ⋯

noncomputable def NavierStokes.ActualCandidateAssembly.signedPressure (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) : ProblemStatement.PressureField

Signed pressure, constructed using ActualSignedExterior.cyclePressure.

Equations

• NavierStokes.ActualCandidateAssembly.signedPressure B N0 hN j = NavierStokes.ActualSignedExterior.cyclePressure (NavierStokes.ActualCandidateConstruction.cycle B N0 j) ⋯ ⋯

noncomputable def NavierStokes.ActualCandidateAssembly.positivePotential (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) : ProblemStatement.VelocityField

Positive potential, given by particularPotential B N0 j + signedPotential B N0 hN j + ActualCandidateConstruction.streamMeanStages B N0 (j + 1).

Equations

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

noncomputable def NavierStokes.ActualCandidateAssembly.positivePressure (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) : ProblemStatement.PressureField

Positive pressure, given by particularPressure B N0 j + signedPressure B N0 hN j + ActualCandidateConstruction.pressureMeanStages B N0 (j + 1).

Equations

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

noncomputable def NavierStokes.ActualCandidateAssembly.directData (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) : ℕ → DirectAngularDiagonal.AngularData (LocalAngularDiagonal.localSlowDomain CorrectionInitialization.ActualPrimary.h (ActualCandidateConstruction.qbig B N0))

Direct data, given by ActualCandidateConstruction.directData (meanCycleInput B N0 hN).

Equations

• NavierStokes.ActualCandidateAssembly.directData B N0 hN = NavierStokes.ActualCandidateConstruction.directData ⋯

noncomputable def NavierStokes.ActualCandidateAssembly.potentialStages (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) : ℕ → ProblemStatement.VelocityField

Potential stages, given by GermCandidateAssembly.potentialStages certificate modulation upper B (initialPotential B N0) (positivePotential B N0 hN).

Equations

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

noncomputable def NavierStokes.ActualCandidateAssembly.directStages (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) : ℕ → ProblemStatement.VelocityField

Direct stages, given by LocalAngularDiagonal.rawSeries (directData B N0 hN).

Equations

• NavierStokes.ActualCandidateAssembly.directStages B N0 hN = NavierStokes.LocalAngularDiagonal.rawSeries (NavierStokes.ActualCandidateAssembly.directData B N0 hN)

noncomputable def NavierStokes.ActualCandidateAssembly.pressureStages (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) : ℕ → ProblemStatement.PressureField

Pressure stages, given by MixedCandidateAssembly.pressureStages certificate modulation upper B (initialPressure B N0) (positivePressure B N0 hN).

Equations

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

theorem NavierStokes.ActualCandidateAssembly.potentialStages_zero (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) : potentialStages B N0 hN 0 = zerothPotential B N0

theorem NavierStokes.ActualCandidateAssembly.potentialStages_succ (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) : potentialStages B N0 hN (j + 1) = positivePotential B N0 hN j

theorem NavierStokes.ActualCandidateAssembly.directStages_eq (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) : directStages B N0 hN j = ActualCandidateConstruction.angularMeanStages B N0 j

theorem NavierStokes.ActualCandidateAssembly.directStages_zero (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) : directStages B N0 hN 0 = initialDirect B N0

theorem NavierStokes.ActualCandidateAssembly.pressureStages_zero (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) : pressureStages B N0 hN 0 = zerothPressure B N0

theorem NavierStokes.ActualCandidateAssembly.pressureStages_succ (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) : pressureStages B N0 hN (j + 1) = positivePressure B N0 hN j

Geometric inputs are consequences of the same constructed fields

theorem NavierStokes.ActualCandidateAssembly.particular_smooth (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) : ContDiffOn ℝ (↑⊤) (particularPotential B N0 j) (ActualCandidateConstruction.physicalDomain B N0) ∧ ContDiffOn ℝ (↑⊤) (particularPressure B N0 j) (ActualCandidateConstruction.physicalDomain B N0)

theorem NavierStokes.ActualCandidateAssembly.particular_zero_germs (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ ActualCandidateConstruction.physicalDomain B N0) (he : w ∉ ActualPolarCoverage.active) : (particularPotential B N0 j =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0) ∧ particularPressure B N0 j =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.ActualCandidateAssembly.signed_zero_germs (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (he : w ∉ ActualPolarCoverage.active) : (signedPotential B N0 hN j =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0) ∧ signedPressure B N0 hN j =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.ActualCandidateAssembly.stream_stage {B N0 : ℕ} (M : ActualCandidateConstruction.MeanCycleInput B N0) (j : ℕ) : PhysicalStage B N0 (ActualCandidateConstruction.streamMeanStages B N0 j)

The stream correction inherits its zero germs from its exterior identity.

theorem NavierStokes.ActualCandidateAssembly.meanPressure_stage {B N0 : ℕ} (M : ActualCandidateConstruction.MeanCycleInput B N0) (j : ℕ) : PhysicalStage B N0 (ActualCandidateConstruction.pressureMeanStages B N0 j)

The mean pressure inherits its zero germs from its exterior identity.

theorem NavierStokes.ActualCandidateAssembly.particular_stage (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) : PhysicalStage B N0 (particularPotential B N0 j) ∧ PhysicalStage B N0 (particularPressure B N0 j)

theorem NavierStokes.ActualCandidateAssembly.signed_stage (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) : PhysicalStage B N0 (signedPotential B N0 hN j) ∧ PhysicalStage B N0 (signedPressure B N0 hN j)

theorem NavierStokes.ActualCandidateAssembly.positive_stage (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) : PhysicalStage B N0 (positivePotential B N0 hN j) ∧ PhysicalStage B N0 (positivePressure B N0 hN j)

The positive stages are sums of three physical stages.

theorem NavierStokes.ActualCandidateAssembly.particular_support (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) : MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h PhysicalStageSupport.actualOuterConstant (ActualCandidateConstruction.qbig B N0) (particularPotential B N0 j) ∧ MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h PhysicalStageSupport.actualOuterConstant (ActualCandidateConstruction.qbig B N0) (particularPressure B N0 j)

theorem NavierStokes.ActualCandidateAssembly.particular_axisZeroOn (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) : GermCandidateAssembly.AxisZeroOn (MixedAxisPreservation.localDomain CorrectionInitialization.ActualPrimary.h (ActualCandidateConstruction.qbig B N0)) (particularPotential B N0 j)

theorem NavierStokes.ActualCandidateAssembly.support_of_exterior_zero {V : Type u_1} [NormedAddCommGroup V] {f : ProblemStatement.SpaceTime → V} {qbig : ℝ} (hz : ∀ w ∈ PhysicalWaveSum.preterminal, w ∉ ActualPolarCoverage.active → f w = 0) : MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h PhysicalStageSupport.actualOuterConstant qbig f

theorem NavierStokes.ActualCandidateAssembly.signed_support (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) : MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h PhysicalStageSupport.actualOuterConstant (ActualCandidateConstruction.qbig B N0) (signedPotential B N0 hN j) ∧ MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h PhysicalStageSupport.actualOuterConstant (ActualCandidateConstruction.qbig B N0) (signedPressure B N0 hN j)

theorem NavierStokes.ActualCandidateAssembly.signed_axisZeroOn (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) : GermCandidateAssembly.AxisZeroOn (MixedAxisPreservation.localDomain CorrectionInitialization.ActualPrimary.h (ActualCandidateConstruction.qbig B N0)) (signedPotential B N0 hN j)

theorem NavierStokes.ActualCandidateAssembly.positivePotential_support (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) : MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h PhysicalStageSupport.actualOuterConstant (ActualCandidateConstruction.qbig B N0) (positivePotential B N0 hN j)

theorem NavierStokes.ActualCandidateAssembly.positivePressure_support (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) : MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h PhysicalStageSupport.actualOuterConstant (ActualCandidateConstruction.qbig B N0) (positivePressure B N0 hN j)

theorem NavierStokes.ActualCandidateAssembly.directStages_support (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) : MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h PhysicalStageSupport.actualOuterConstant (ActualCandidateConstruction.qbig B N0) (directStages B N0 hN j)

theorem NavierStokes.ActualCandidateAssembly.positivePotential_axisZeroOn (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) : GermCandidateAssembly.AxisZeroOn (MixedAxisPreservation.localDomain CorrectionInitialization.ActualPrimary.h (ActualCandidateConstruction.qbig B N0)) (positivePotential B N0 hN j)

theorem NavierStokes.ActualCandidateAssembly.positive_exterior (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ ActualCandidateConstruction.physicalDomain B N0) (he : w ∉ ActualPolarCoverage.active) : positivePotential B N0 hN j w = 0 ∧ positivePressure B N0 hN j w = 0

theorem NavierStokes.ActualCandidateAssembly.exteriorStages (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) : ActualExteriorPrefix.ExteriorStages B (ActualCandidateConstruction.residualBand B N0) (potentialStages B N0 hN) (directStages B N0 hN) (pressureStages B N0 hN)

theorem NavierStokes.ActualCandidateAssembly.particularPotential_on_chart (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j n : ℕ) (hn : ActualCandidateConstruction.firstBand B N0 ≤ n) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) : Set.EqOn (SpatialCurl.spatialCurl (particularPotential B N0 j)) ((CyclePhysicalPrefixes.polarVelocityMap a i) ((CyclePhysicalPrefixes.velocityMap (ActualCandidateConstruction.graph n)) ((ActualCandidateConstruction.parameters B N0).particularVelocity (ActualCandidateConstruction.cycle B N0 j).coefficients (CorrectionInitialization.ActualPrimary.commonContext B) (ActualCandidateConstruction.cycle B N0 j).state n))) (ActualPhysicalPrefixFields.cartesianChartDomain (ActualCandidateConstruction.qbig B N0) n a i)

theorem NavierStokes.ActualCandidateAssembly.particularPressure_on_chart (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j n : ℕ) (hn : ActualCandidateConstruction.firstBand B N0 ≤ n) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) : Set.EqOn (particularPressure B N0 j) ((CyclePhysicalPrefixes.polarPressureMap a i) ((CyclePhysicalPrefixes.pressureMap (ActualCandidateConstruction.graph n)) ((ActualCandidateConstruction.parameters B N0).particularPressure (ActualCandidateConstruction.cycle B N0 j).coefficients (CorrectionInitialization.ActualPrimary.commonContext B) (ActualCandidateConstruction.cycle B N0 j).state n))) (ActualPhysicalPrefixFields.cartesianChartDomain (ActualCandidateConstruction.qbig B N0) n a i)

The quantitative component record uses these exact sequences

theorem NavierStokes.ActualCandidateAssembly.representations_of_signed_eqOn (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (W : GluedStageEstimates.SignedInputs D I K) (hA : ∀ (j : ℕ), Set.EqOn (W.potential j).vector (signedPotential B N0 hN j) (ActualCandidateConstruction.physicalDomain B N0)) (hP : ∀ (j : ℕ), Set.EqOn (W.pressure j).pressure (signedPressure B N0 hN j) (ActualCandidateConstruction.physicalDomain B N0)) : GluedStageEstimates.ActualRepresentations (runData B N0 hN) ⋯ ⋯ W (ActualCandidateConstruction.qbig B N0) (potentialStages B N0 hN) (directStages B N0 hN) (pressureStages B N0 hN)

theorem NavierStokes.ActualCandidateAssembly.stages_smooth_of_signed_eqOn (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (W : GluedStageEstimates.SignedInputs D I K) (hA : ∀ (j : ℕ), Set.EqOn (W.potential j).vector (signedPotential B N0 hN j) (ActualCandidateConstruction.physicalDomain B N0)) (hP : ∀ (j : ℕ), Set.EqOn (W.pressure j).pressure (signedPressure B N0 hN j) (ActualCandidateConstruction.physicalDomain B N0)) : (∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (potentialStages B N0 hN j) (ActualCandidateConstruction.physicalDomain B N0)) ∧ (∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (directStages B N0 hN j) (ActualCandidateConstruction.physicalDomain B N0)) ∧ ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (pressureStages B N0 hN j) (ActualCandidateConstruction.physicalDomain B N0)

theorem NavierStokes.ActualCandidateAssembly.signedPotential_eq_native (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) : Set.EqOn ((ActualSignedWaveData.signedInputs B N0 hN).potential j).vector (signedPotential B N0 hN j) PhysicalWaveSum.preterminal

theorem NavierStokes.ActualCandidateAssembly.signedPressure_eq_native (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) : Set.EqOn ((ActualSignedWaveData.signedInputs B N0 hN).pressure j).pressure (signedPressure B N0 hN j) PhysicalWaveSum.preterminal

theorem NavierStokes.ActualCandidateAssembly.signedPotential_smooth (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) : ContDiffOn ℝ (↑⊤) (signedPotential B N0 hN j) PhysicalWaveSum.preterminal

theorem NavierStokes.ActualCandidateAssembly.signedPressure_smooth (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) : ContDiffOn ℝ (↑⊤) (signedPressure B N0 hN j) PhysicalWaveSum.preterminal

theorem NavierStokes.ActualCandidateAssembly.representations (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) : GluedStageEstimates.ActualRepresentations (runData B N0 hN) ⋯ ⋯ (ActualSignedWaveData.signedInputs B N0 hN) (ActualCandidateConstruction.qbig B N0) (potentialStages B N0 hN) (directStages B N0 hN) (pressureStages B N0 hN)

theorem NavierStokes.ActualCandidateAssembly.stages_smooth (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) : (∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (potentialStages B N0 hN j) (ActualCandidateConstruction.physicalDomain B N0)) ∧ (∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (directStages B N0 hN j) (ActualCandidateConstruction.physicalDomain B N0)) ∧ ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (pressureStages B N0 hN j) (ActualCandidateConstruction.physicalDomain B N0)

theorem NavierStokes.ActualCandidateAssembly.postParticular_coherent (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) : ActualCycleCoherence.StateCoherent (ActualParticularMeanGain.postParticular (ActualCandidateConstruction.cycle B N0 j))

theorem NavierStokes.ActualCandidateAssembly.signed_amplitude_bound (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) (l : ActualInitialization.Index B N0) : CurrentSignedCurl.AmplitudeBound l (ActualParticularMeanGain.postParticular (ActualCandidateConstruction.cycle B N0 j)) (1 + ActualIterationLedger.sigma j - ChartScales.kappa - 1 / 2)

theorem NavierStokes.ActualCandidateAssembly.zerothPotential_on_chart (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (n : ℕ) (hn : ActualCandidateConstruction.firstBand B N0 ≤ n) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) : Set.EqOn (SpatialCurl.spatialCurl (zerothPotential B N0)) (ActualCandidateConstruction.chartPotentialParts B N0 a i n 0) (ActualPhysicalPrefixFields.cartesianChartDomain (ActualCandidateConstruction.qbig B N0) n a i)

theorem NavierStokes.ActualCandidateAssembly.zerothPressure_on_chart (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (n : ℕ) (hn : ActualCandidateConstruction.firstBand B N0 ≤ n) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) : Set.EqOn (zerothPressure B N0) (ActualCandidateConstruction.chartPressureStages B N0 a i n 0) (ActualPhysicalPrefixFields.cartesianChartDomain (ActualCandidateConstruction.qbig B N0) n a i)

theorem NavierStokes.ActualCandidateAssembly.signedPotential_on_chart (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) : Set.EqOn (SpatialCurl.spatialCurl (signedPotential B N0 hN j)) ((CyclePhysicalPrefixes.polarVelocityMap a i) ((CyclePhysicalPrefixes.velocityMap (ActualCandidateConstruction.graph n)) ((ActualCandidateConstruction.parameters B N0).signedVelocity (ActualCandidateConstruction.cycle B N0 j).coefficients (CorrectionInitialization.ActualPrimary.commonContext B) (ActualCandidateConstruction.cycle B N0 j).state n))) (ActualPhysicalPrefixFields.cartesianChartDomain (ActualCandidateConstruction.qbig B N0) n a i)

theorem NavierStokes.ActualCandidateAssembly.signedPressure_on_chart (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) : Set.EqOn (signedPressure B N0 hN j) ((CyclePhysicalPrefixes.polarPressureMap a i) ((CyclePhysicalPrefixes.pressureMap (ActualCandidateConstruction.graph n)) ((ActualCandidateConstruction.parameters B N0).signedPressure (ActualCandidateConstruction.cycle B N0 j).coefficients (CorrectionInitialization.ActualPrimary.commonContext B) (ActualCandidateConstruction.cycle B N0 j).state n))) (ActualPhysicalPrefixFields.cartesianChartDomain (ActualCandidateConstruction.qbig B N0) n a i)

theorem NavierStokes.ActualCandidateAssembly.positivePotential_curl (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℕ) : Set.EqOn (SpatialCurl.spatialCurl (positivePotential B N0 hN j)) (fun (w : ProblemStatement.SpaceTime) => SpatialCurl.spatialCurl (particularPotential B N0 j) w + SpatialCurl.spatialCurl (signedPotential B N0 hN j) w + SpatialCurl.spatialCurl (ActualCandidateConstruction.streamMeanStages B N0 (j + 1)) w) (ActualCandidateConstruction.physicalDomain B N0)

theorem NavierStokes.ActualCandidateAssembly.positivePotential_on_chart (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j n : ℕ) (hn : ActualCandidateConstruction.firstBand B N0 ≤ n) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) : Set.EqOn (SpatialCurl.spatialCurl (positivePotential B N0 hN j)) (ActualCandidateConstruction.chartPotentialParts B N0 a i n (j + 1)) (ActualPhysicalPrefixFields.cartesianChartDomain (ActualCandidateConstruction.qbig B N0) n a i)

theorem NavierStokes.ActualCandidateAssembly.positivePressure_on_chart (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j n : ℕ) (hn : ActualCandidateConstruction.firstBand B N0 ≤ n) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) : Set.EqOn (positivePressure B N0 hN j) (ActualCandidateConstruction.chartPressureStages B N0 a i n (j + 1)) (ActualPhysicalPrefixFields.cartesianChartDomain (ActualCandidateConstruction.qbig B N0) n a i)

theorem NavierStokes.ActualCandidateAssembly.stageRealizations (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) : ActualPhysicalPrefixFields.StageRealizations B N0 (ActualCandidateConstruction.residualBand B N0) (ActualCandidateConstruction.parameterSequence B N0) (ActualCandidateConstruction.qbig B N0) (potentialStages B N0 hN) (directStages B N0 hN) (pressureStages B N0 hN)

theorem NavierStokes.ActualCandidateAssembly.physicalData (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (J : ℕ) : ActualCycleResidualBounds.PhysicalData B (ActualCandidateConstruction.residualBand B N0) (ActualCandidateConstruction.cycle B N0 J).state (MixedDiagonalResidual.uncutVelocity (potentialStages B N0 hN) (directStages B N0 hN) J) (DiagonalJetBounds.uncutPrefix (pressureStages B N0 hN) (J + 1))

noncomputable def NavierStokes.ActualCandidateAssembly.estimates (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) : MixedCandidateAssembly.StageEstimates CorrectionInitialization.ActualPrimary.h (ActualCandidateConstruction.qbig B N0) (potentialStages B N0 hN) (directStages B N0 hN) (pressureStages B N0 hN)

Estimates, constructed using GluedStageEstimates.actualStageEstimates.

Equations

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

theorem NavierStokes.ActualCandidateAssembly.endpoints (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) : ActualEndpointInputs.EndpointInputs CorrectionInitialization.ActualPrimary.h (ActualCandidateConstruction.qbig B N0) (potentialStages B N0 hN) (directStages B N0 hN) (pressureStages B N0 hN)

The common schedule and its actual fields

def NavierStokes.ActualCandidateAssembly.Witness (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) : Prop

The output retains the actual three sums, the smooth force, and the strong consequences for this same velocity and pressure.

Equations

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

theorem NavierStokes.ActualCandidateAssembly.witness (B N0 : ℕ) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) : Witness B N0 hN

One closed choice fixes all three raw sequences together.

noncomputable def NavierStokes.ActualCandidateAssembly.selectedPotentialStages : ℕ → ProblemStatement.VelocityField

Selected potential stages, constructed using potentialStages.

Equations

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

noncomputable def NavierStokes.ActualCandidateAssembly.selectedDirectStages : ℕ → ProblemStatement.VelocityField

Selected direct stages, constructed using directStages.

Equations

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

noncomputable def NavierStokes.ActualCandidateAssembly.selectedPressureStages : ℕ → ProblemStatement.PressureField

Selected pressure stages, constructed using pressureStages.

Equations

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

theorem NavierStokes.ActualCandidateAssembly.selected_witness : Witness ActualCandidateConstruction.selectedBudget ActualCandidateConstruction.selectedThreshold ActualCandidateConstruction.selectedThreshold_geometry

theorem NavierStokes.ActualCandidateAssembly.selected_candidate : ProblemStatement.candidateStatement