The first stress coefficient on the terminal collar

The first coefficient is the canonical primitive of the actual repaired residual. The order-zero moment retained below is essential: exterior agreement of velocities alone does not fix the constant of integration.

Stress confinement for the coherent repaired slow sequence

The five rows constructed by GlobalSlowProfiles imply the two actual conservative residual integrals vanish. Their negative radial primitives therefore vanish past the same outer radius, uniformly over positive orders n ≥ 2. The preceding angular coefficient then has an ordinary repaired moment; no renormalized order-zero moment is used in this module.

noncomputable def NavierStokes.GlobalStressSupport.axialHistory {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (n : ℕ) : GlobalSlowProfiles.Field

The actual axial coefficients pulled back from X to signed radius.

Equations

• NavierStokes.GlobalStressSupport.axialHistory s n = NavierStokes.SlowResidualMatching.toRadius ((NavierStokes.GlobalSlowProfiles.asSlowProfiles s).axial n)

noncomputable def NavierStokes.GlobalStressSupport.angularHistory {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (n : ℕ) : GlobalSlowProfiles.Field

The actual angular velocity coefficients in signed radius.

Equations

• NavierStokes.GlobalStressSupport.angularHistory s n = NavierStokes.SlowResidualMatching.swirlRadius C ((NavierStokes.GlobalSlowProfiles.asSlowProfiles s).phi n)

noncomputable def NavierStokes.GlobalStressSupport.fluxHistory {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (n : ℕ) : GlobalSlowProfiles.Field

The divergence variable is V = X β = R² β/2.

Equations

• NavierStokes.GlobalStressSupport.fluxHistory s n = NavierStokes.SlowResidualMatching.toRadius ((NavierStokes.GlobalSlowProfiles.asSlowProfiles s).flux n)

noncomputable def NavierStokes.GlobalStressSupport.pressureField {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (n : ℕ) : GlobalSlowProfiles.Field

Pressure field, given by SlowResidualMatching.toRadius ((asSlowProfiles s).pressure n).

Equations

• NavierStokes.GlobalStressSupport.pressureField s n = NavierStokes.SlowResidualMatching.toRadius ((NavierStokes.GlobalSlowProfiles.asSlowProfiles s).pressure n)

noncomputable def NavierStokes.GlobalStressSupport.previousOmega {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (n : ℕ) (w : ℝ × ℝ) : ℝ

The full preceding radial residual, including both viscous terms.

Equations

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

theorem NavierStokes.GlobalStressSupport.toRadius_xProfile {S : Set ℝ} (f : GlobalSlowProfiles.EvenProfile S) {w : ℝ × ℝ} (hw : w.2 ∈ S) : SlowResidualMatching.toRadius (GlobalSlowProfiles.xProfile f) w = ↑f w

theorem NavierStokes.GlobalStressSupport.axialHistory_eq {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (n : ℕ) {w : ℝ × ℝ} (hw : w.2 ∈ S) : axialHistory s n w = ↑(GlobalSlowProfiles.profiles s n).axial w

theorem NavierStokes.GlobalStressSupport.angularHistory_eq {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (n : ℕ) {w : ℝ × ℝ} (hw : w.2 ∈ S) : angularHistory s n w = GlobalSlowProfiles.angularField C (GlobalSlowProfiles.profiles s n).phi w

theorem NavierStokes.GlobalStressSupport.fluxHistory_eq {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (n : ℕ) {w : ℝ × ℝ} (hw : w.2 ∈ S) : fluxHistory s n w = w.1 ^ 2 / 2 * ↑(GlobalSlowProfiles.profiles s n).beta w

theorem NavierStokes.GlobalStressSupport.pressureField_eq {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (n : ℕ) {w : ℝ × ℝ} (hw : w.2 ∈ S) : pressureField s n w = ↑(GlobalSlowProfiles.profiles s n).pressure w

theorem NavierStokes.GlobalStressSupport.axialHistory_smooth {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (n : ℕ) : GlobalSlowProfiles.Smooth S (axialHistory s n)

theorem NavierStokes.GlobalStressSupport.angularHistory_smooth {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (n : ℕ) : GlobalSlowProfiles.Smooth S (angularHistory s n)

theorem NavierStokes.GlobalStressSupport.fluxHistory_smooth {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (n : ℕ) : GlobalSlowProfiles.Smooth S (fluxHistory s n)

theorem NavierStokes.GlobalStressSupport.pressureField_smooth {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (n : ℕ) : GlobalSlowProfiles.Smooth S (pressureField s n)

theorem NavierStokes.GlobalStressSupport.axialHistory_exterior {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (n : ℕ) : SlowStressSupport.exterior s.B S (axialHistory s n)

theorem NavierStokes.GlobalStressSupport.angularHistory_exterior {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) {n : ℕ} (hn : 0 < n) : SlowStressSupport.exterior s.B S (angularHistory s n)

theorem NavierStokes.GlobalStressSupport.fluxHistory_exterior {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (n : ℕ) : SlowStressSupport.exterior s.B S (fluxHistory s n)

theorem NavierStokes.GlobalStressSupport.pressureField_exterior {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) {n : ℕ} (hn : 0 < n) : SlowStressSupport.exterior s.B S (pressureField s n)

theorem NavierStokes.GlobalStressSupport.previousOmega_exterior {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (n : ℕ) : SlowStressSupport.exterior s.B S (previousOmega s n)

theorem NavierStokes.GlobalStressSupport.pressureGradient_eq {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (n : ℕ) {w : ℝ × ℝ} (hw : w.2 ∈ S) : PositiveOrderMoments.jointPressureGradient n (angularHistory s) (previousOmega s n) w = PositiveOrderMoments.jointPressureGradient n (fun (j : ℕ) => GlobalSlowProfiles.angularField C (GlobalSlowProfiles.profiles s j).phi) (previousOmega s n) w

theorem NavierStokes.GlobalStressSupport.pressureGradient_smooth {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (n : ℕ) : GlobalSlowProfiles.Smooth S (PositiveOrderMoments.jointPressureGradient n (angularHistory s) (previousOmega s n))

theorem NavierStokes.GlobalStressSupport.pressureField_eq_primitive {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) {n : ℕ} (hn : 0 < n) {w : ℝ × ℝ} (hw : w.2 ∈ S) : pressureField s n w = PositiveOrderMoments.pressureHistory n (angularHistory s) (previousOmega s n) w

theorem NavierStokes.GlobalStressSupport.moments_zero {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) {n : ℕ} (hn : 0 < n) {eta : ℝ} (heta : eta ∈ S) : (PositiveOrderMoments.moments n (PositiveOrderMoments.slice (axialHistory s) eta) (PositiveOrderMoments.slice (angularHistory s) eta) fun (R : ℝ) => previousOmega s n (R, eta)) = 0

These are the five rows of the constructed sequence, with its actual preceding radial residual.

theorem NavierStokes.GlobalStressSupport.rowDensity_exterior {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) {n : ℕ} (hn : 0 < n) {eta : ℝ} (heta : eta ∈ S) {R : ℝ} (hR : s.B ≤ R) : PositiveOrderMoments.jointRowDensity n (axialHistory s) (angularHistory s) (previousOmega s n) (R, eta) = 0

theorem NavierStokes.GlobalStressSupport.conservative_moments_zero {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) {n : ℕ} (hn : 0 < n) {eta : ℝ} (heta : eta ∈ S) : SlowStressSupport.moment s.B 1 (axialHistory s n) eta = 0 ∧ SlowStressSupport.moment s.B 2 (angularHistory s n) eta = 0 ∧ SlowStressSupport.moment s.B 2 (SlowStressSupport.conv n (axialHistory s) (angularHistory s)) eta = 0 ∧ SlowStressSupport.moment s.B 1 (fun (w : ℝ × ℝ) => SlowStressSupport.conv n (axialHistory s) (axialHistory s) w + pressureField s n w) eta = 0

In particular, pressure integration by parts converts the fifth repaired row into the actual axial pressure/transport flux moment.

theorem NavierStokes.GlobalStressSupport.fluxHistory_axis {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (n : ℕ) {eta : ℝ} (heta : eta ∈ S) : fluxHistory s n (0, eta) = 0

theorem NavierStokes.GlobalStressSupport.angularDensity_moment_zero {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) {n : ℕ} (hn : 2 ≤ n) {eta : ℝ} (heta : eta ∈ S) : SlowStressSupport.moment s.B 0 (SlowStressSupport.angularDensity h n (fluxHistory s) (axialHistory s) (angularHistory s)) eta = 0

The angular conservative residual has zero actual radial integral. Differentiation of the zero moments and radial integration by parts are performed by the imported balance theorem.

theorem NavierStokes.GlobalStressSupport.axialDensity_moment_zero {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) {n : ℕ} (hn : 2 ≤ n) {eta : ℝ} (heta : eta ∈ S) : SlowStressSupport.moment s.B 0 (SlowStressSupport.axialDensity h n (fluxHistory s) (axialHistory s) (pressureField s n)) eta = 0

theorem NavierStokes.GlobalStressSupport.angularDensity_exterior {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) {n : ℕ} (hn : 2 ≤ n) : SlowStressSupport.exterior s.B S (SlowStressSupport.angularDensity h n (fluxHistory s) (axialHistory s) (angularHistory s))

theorem NavierStokes.GlobalStressSupport.axialDensity_exterior {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) {n : ℕ} (hn : 2 ≤ n) : SlowStressSupport.exterior s.B S (SlowStressSupport.axialDensity h n (fluxHistory s) (axialHistory s) (pressureField s n))

theorem NavierStokes.GlobalStressSupport.radial_divergence {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hbase : s.base.beta = GlobalSlowProfiles.betaFromU ⋯ 0 s.base.axial) (n : ℕ) {w : ℝ × ℝ} (hw : w.2 ∈ S) : SlowStressSupport.dr (fluxHistory s n) w = -w.1 * SlowStressSupport.axialOp h (SlowStressSupport.orderExponent h n) (axialHistory s n) w

At order zero the same divergence reconstruction is the only additional generic input. At every positive order it is part of the proved recursion.

theorem NavierStokes.GlobalStressSupport.thetaDensity_eq {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hbase : s.base.beta = GlobalSlowProfiles.betaFromU ⋯ 0 s.base.axial) {n : ℕ} (hn : 0 < n) : Set.EqOn (SlowResidualMatching.thetaDensity h C (GlobalSlowProfiles.asSlowProfiles s) n) (SlowStressSupport.angularDensity h n (fluxHistory s) (axialHistory s) (angularHistory s)) (GlobalSlowProfiles.region S)

theorem NavierStokes.GlobalStressSupport.zDensity_eq {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hbase : s.base.beta = GlobalSlowProfiles.betaFromU ⋯ 0 s.base.axial) {n : ℕ} (hn : 0 < n) : Set.EqOn (SlowResidualMatching.zDensity h (GlobalSlowProfiles.asSlowProfiles s) n) (SlowStressSupport.axialDensity h n (fluxHistory s) (axialHistory s) (pressureField s n)) (GlobalSlowProfiles.region S)

theorem NavierStokes.GlobalStressSupport.thetaDensity_smooth {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hbase : s.base.beta = GlobalSlowProfiles.betaFromU ⋯ 0 s.base.axial) {n : ℕ} (hn : 0 < n) : GlobalSlowProfiles.Smooth S (SlowResidualMatching.thetaDensity h C (GlobalSlowProfiles.asSlowProfiles s) n)

theorem NavierStokes.GlobalStressSupport.zDensity_smooth {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hbase : s.base.beta = GlobalSlowProfiles.betaFromU ⋯ 0 s.base.axial) {n : ℕ} (hn : 0 < n) : GlobalSlowProfiles.Smooth S (SlowResidualMatching.zDensity h (GlobalSlowProfiles.asSlowProfiles s) n)

theorem NavierStokes.GlobalStressSupport.thetaDensity_moment_zero {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hbase : s.base.beta = GlobalSlowProfiles.betaFromU ⋯ 0 s.base.axial) {n : ℕ} (hn : 2 ≤ n) {eta : ℝ} (heta : eta ∈ S) : SlowStressSupport.moment s.B 0 (SlowResidualMatching.thetaDensity h C (GlobalSlowProfiles.asSlowProfiles s) n) eta = 0

Cancellation of the actual coefficient density, not an assumed moment of an abstract source.

theorem NavierStokes.GlobalStressSupport.zDensity_moment_zero {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hbase : s.base.beta = GlobalSlowProfiles.betaFromU ⋯ 0 s.base.axial) {n : ℕ} (hn : 2 ≤ n) {eta : ℝ} (heta : eta ∈ S) : SlowStressSupport.moment s.B 0 (SlowResidualMatching.zDensity h (GlobalSlowProfiles.asSlowProfiles s) n) eta = 0

theorem NavierStokes.GlobalStressSupport.thetaDensity_exterior {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hbase : s.base.beta = GlobalSlowProfiles.betaFromU ⋯ 0 s.base.axial) {n : ℕ} (hn : 2 ≤ n) : SlowStressSupport.exterior s.B S (SlowResidualMatching.thetaDensity h C (GlobalSlowProfiles.asSlowProfiles s) n)

theorem NavierStokes.GlobalStressSupport.zDensity_exterior {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hbase : s.base.beta = GlobalSlowProfiles.betaFromU ⋯ 0 s.base.axial) {n : ℕ} (hn : 2 ≤ n) : SlowStressSupport.exterior s.B S (SlowResidualMatching.zDensity h (GlobalSlowProfiles.asSlowProfiles s) n)

theorem NavierStokes.GlobalStressSupport.thetaDensity_integrableOn {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hbase : s.base.beta = GlobalSlowProfiles.betaFromU ⋯ 0 s.base.axial) {n : ℕ} (hn : 2 ≤ n) {eta : ℝ} (heta : eta ∈ S) : MeasureTheory.IntegrableOn (fun (R : ℝ) => SlowResidualMatching.thetaDensity h C (GlobalSlowProfiles.asSlowProfiles s) n (R, eta)) (Set.Ioi 0) MeasureTheory.volume

theorem NavierStokes.GlobalStressSupport.zDensity_integrableOn {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hbase : s.base.beta = GlobalSlowProfiles.betaFromU ⋯ 0 s.base.axial) {n : ℕ} (hn : 2 ≤ n) {eta : ℝ} (heta : eta ∈ S) : MeasureTheory.IntegrableOn (fun (R : ℝ) => SlowResidualMatching.zDensity h (GlobalSlowProfiles.asSlowProfiles s) n (R, eta)) (Set.Ioi 0) MeasureTheory.volume

theorem NavierStokes.GlobalStressSupport.thetaDensity_positive_integral_zero {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hbase : s.base.beta = GlobalSlowProfiles.betaFromU ⋯ 0 s.base.axial) {n : ℕ} (hn : 2 ≤ n) {eta : ℝ} (heta : eta ∈ S) : ∫ (R : ℝ) in Set.Ioi 0, SlowResidualMatching.thetaDensity h C (GlobalSlowProfiles.asSlowProfiles s) n (R, eta) = 0

theorem NavierStokes.GlobalStressSupport.zDensity_positive_integral_zero {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hbase : s.base.beta = GlobalSlowProfiles.betaFromU ⋯ 0 s.base.axial) {n : ℕ} (hn : 2 ≤ n) {eta : ℝ} (heta : eta ∈ S) : ∫ (R : ℝ) in Set.Ioi 0, SlowResidualMatching.zDensity h (GlobalSlowProfiles.asSlowProfiles s) n (R, eta) = 0

theorem NavierStokes.GlobalStressSupport.raw_stresses_exterior {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hbase : s.base.beta = GlobalSlowProfiles.betaFromU ⋯ 0 s.base.axial) {n : ℕ} (hn : 2 ≤ n) : GlobalSlowProfiles.Exterior s.B S (SlowStressSupport.stress 2 (SlowResidualMatching.thetaDensity h C (GlobalSlowProfiles.asSlowProfiles s) n)) ∧ GlobalSlowProfiles.Exterior s.B S (SlowStressSupport.stress 1 (SlowResidualMatching.zDensity h (GlobalSlowProfiles.asSlowProfiles s) n))

Both canonical negative radial primitives have the same exterior radius for all n ≥ 2. There is no output-support hypothesis.

theorem NavierStokes.GlobalStressSupport.nominal_base_beta {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : (AssembledSlowBase.nominalScheme W).base.beta = GlobalSlowProfiles.betaFromU ⋯ 0 (AssembledSlowBase.nominalScheme W).base.axial

The nominal scheme uses the actual mass reconstruction already at order zero, so the generic extra input is discharged definitionally.

theorem NavierStokes.GlobalStressSupport.nominal_stresses_exterior {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {n : ℕ} (hn : 2 ≤ n) : GlobalSlowProfiles.Exterior (AssembledSlowBase.nominalOuterRadius W) (AssembledSlowBase.nominalParameters W) (SlowStressSupport.stress 2 (SlowResidualMatching.thetaDensity F.data.h W.axis.normalization (GlobalSlowProfiles.asSlowProfiles (AssembledSlowBase.nominalScheme W)) n)) ∧ GlobalSlowProfiles.Exterior (AssembledSlowBase.nominalOuterRadius W) (AssembledSlowBase.nominalParameters W) (SlowStressSupport.stress 1 (SlowResidualMatching.zDensity F.data.h (GlobalSlowProfiles.asSlowProfiles (AssembledSlowBase.nominalScheme W)) n))

theorem NavierStokes.GlobalStressSupport.nominal_density_integrals_zero {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {n : ℕ} (hn : 2 ≤ n) {eta : ℝ} (heta : eta ∈ AssembledSlowBase.nominalParameters W) : ∫ (R : ℝ) in Set.Ioi 0, SlowResidualMatching.thetaDensity F.data.h W.axis.normalization (GlobalSlowProfiles.asSlowProfiles (AssembledSlowBase.nominalScheme W)) n (R, eta) = 0 ∧ ∫ (R : ℝ) in Set.Ioi 0, SlowResidualMatching.zDensity F.data.h (GlobalSlowProfiles.asSlowProfiles (AssembledSlowBase.nominalScheme W)) n (R, eta) = 0

theorem NavierStokes.GlobalStressSupport.nominalCoefficients_stress_zero_right {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {n : ℕ} (hn : 2 ≤ n) {p : ℝ × ℝ} (hX : AssembledSlowBase.nominalOuterX W ≤ p.1) : (AssembledSlowBase.nominalCoefficients W).stressTheta n p = 0 ∧ (AssembledSlowBase.nominalCoefficients W).stressAxial n p = 0

The actual globally smooth coefficients vanish outside the fixed outer radius for every parameter, including outside the physical parameter strip.

theorem NavierStokes.GlobalStressSupport.nominalCoefficients_stress_support {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {n : ℕ} (hn : 2 ≤ n) : (tsupport fun (p : SlowBorelBase.Inner) => ((AssembledSlowBase.nominalCoefficients W).stressTheta n p, (AssembledSlowBase.nominalCoefficients W).stressAxial n p)) ⊆ Set.Icc (AssembledSlowBase.nominalInner W / 8) (AssembledSlowBase.nominalOuterX W) ×ˢ Set.Icc (-(AssembledSlowBase.commonWindow (AssembledSlowBase.nominalScheme W) ⋯).outer) (AssembledSlowBase.commonWindow (AssembledSlowBase.nominalScheme W) ⋯).outer

One compact rectangle contains both stress supports for the entire higher-order family. Its radial lower edge is strictly positive.

theorem NavierStokes.GlobalStressSupport.nominalCoefficients_stress_compactSupport {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {n : ℕ} (hn : 2 ≤ n) : HasCompactSupport fun (p : SlowBorelBase.Inner) => ((AssembledSlowBase.nominalCoefficients W).stressTheta n p, (AssembledSlowBase.nominalCoefficients W).stressAxial n p)

theorem NavierStokes.FirstOrderBaseEdge.exterior_mono {S : Set ℝ} {f : SlowStressSupport.Field} {a b : ℝ} (hf : SlowStressSupport.exterior a S f) (hab : a ≤ b) : SlowStressSupport.exterior b S f

theorem NavierStokes.FirstOrderBaseEdge.moment_eq_of_exterior {S : Set ℝ} {f : SlowStressSupport.Field} {a b eta : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (hf : SlowStressSupport.exterior a S f) (heta : eta ∈ S) (m : ℕ) : SlowStressSupport.moment b m f eta = SlowStressSupport.moment a m f eta

theorem NavierStokes.FirstOrderBaseEdge.conservative_moments_at {S : Set ℝ} {h C R : ℝ} (s : GlobalSlowProfiles.Scheme S h C) {n : ℕ} (hn : 0 < n) (hR : s.B ≤ R) {eta : ℝ} (heta : eta ∈ S) : SlowStressSupport.moment R 1 (GlobalStressSupport.axialHistory s n) eta = 0 ∧ SlowStressSupport.moment R 2 (GlobalStressSupport.angularHistory s n) eta = 0 ∧ SlowStressSupport.moment R 2 (SlowStressSupport.conv n (GlobalStressSupport.axialHistory s) (GlobalStressSupport.angularHistory s)) eta = 0 ∧ SlowStressSupport.moment R 1 (fun (w : ℝ × ℝ) => SlowStressSupport.conv n (GlobalStressSupport.axialHistory s) (GlobalStressSupport.axialHistory s) w + GlobalStressSupport.pressureField s n w) eta = 0

The four conservative moments at every radius beyond the actual repair patch follow from the five constructed rows.

theorem NavierStokes.FirstOrderBaseEdge.first_angular_balance {S : Set ℝ} {h C R : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hbase : s.base.beta = GlobalSlowProfiles.betaFromU ⋯ 0 s.base.axial) (hR : s.B ≤ R) {eta : ℝ} (heta : eta ∈ S) : SlowStressSupport.stress 2 (SlowResidualMatching.thetaDensity h C (GlobalSlowProfiles.asSlowProfiles s) 1) (R, eta) = SlowStressSupport.moment R 2 (SlowStressSupport.axialOp2 h (SlowStressSupport.orderExponent h 0) (GlobalStressSupport.angularHistory s 0)) eta / R ^ 2

The exact first angular primitive, with its order-zero viscosity moment still displayed. This is derived from the repaired rows, not prescribed as a stress boundary condition.

theorem NavierStokes.FirstOrderBaseEdge.first_axial_exterior {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hbase : s.base.beta = GlobalSlowProfiles.betaFromU ⋯ 0 s.base.axial) (hmass : ∀ eta ∈ S, SlowStressSupport.moment s.B 1 (GlobalStressSupport.axialHistory s 0) eta = 0) : SlowStressSupport.exterior s.B S (SlowStressSupport.stress 1 (SlowResidualMatching.zDensity h (GlobalSlowProfiles.asSlowProfiles s) 1))

At order one the axial primitive vanishes outside the repair patch as soon as the actual base mass is zero there.

The literal physical viscosity and its zero total moment

theorem NavierStokes.FirstOrderBaseEdge.physical_angular_germ (F : OutgoingProfile.Profile) {XR cost L : ℝ} (w : HeatedOutgoing.CompensationWitness F XR cost) {E : ℝ × ℝ → ℝ} (hmatch : ∀ eta ∈ Set.Ioo (-1) 1, ∀ (X : ℝ), L ≤ X → E (X, eta) = HeatedOutgoing.E F XR w.coefficients (X, eta)) {p : SimilarityProfile.PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) (hL : L < SimilarityProfile.X F.data.h p) (hfull : 1 / 2 < Real.log (SimilarityProfile.X F.data.h p / OutgoingDilation.switchRadius F XR) + 1 / 5) : SimilarityProfile.pullback F.data.h (-CoordinateAlgebra.A F.data.h) E =ᶠ[nhds p] SlowFirstOrderEdge.physicalAngular (TerminalHistoryBridge.normalization F XR) F.data (TerminalHistoryBridge.shift F XR)

theorem NavierStokes.FirstOrderBaseEdge.actual_viscosity_eq_terminal (F : OutgoingProfile.Profile) {XR cost L : ℝ} (w : HeatedOutgoing.CompensationWitness F XR cost) {E G : ℝ × ℝ → ℝ} (hG : SlowStressSupport.Smooth (Set.Ioo (-1) 1) G) (hGE : ∀ (R : ℝ), 0 < R → ∀ eta ∈ Set.Ioo (-1) 1, G (R, eta) = E (R ^ 2 / 2, eta)) (hmatch : ∀ eta ∈ Set.Ioo (-1) 1, ∀ (X : ℝ), L ≤ X → E (X, eta) = HeatedOutgoing.E F XR w.coefficients (X, eta)) {R eta : ℝ} (hR : 0 < R) (heta : eta ∈ Set.Ioo (-1) 1) (hL : L < R ^ 2 / 2) (hfull : 1 / 2 < Real.log (R ^ 2 / 2 / OutgoingDilation.switchRadius F XR) + 1 / 5) : SlowStressSupport.axialOp2 F.data.h (SlowStressSupport.orderExponent F.data.h 0) G (R, eta) = -SlowFirstOrderEdge.radialSource (TerminalHistoryBridge.normalization F XR) F.data (TerminalHistoryBridge.shift F XR) eta R

On the switched tail the actual second axial derivative is the source used in the independently constructed flat terminal primitive.

theorem NavierStokes.FirstOrderBaseEdge.actual_viscosity_total_zero (F : OutgoingProfile.Profile) {XR cost L : ℝ} (w : HeatedOutgoing.CompensationWitness F XR cost) {E G : ℝ × ℝ → ℝ} (hG : SlowStressSupport.Smooth (Set.Ioo (-1) 1) G) (hGE : ∀ (R : ℝ), 0 < R → ∀ eta ∈ Set.Ioo (-1) 1, G (R, eta) = E (R ^ 2 / 2, eta)) (hmatch : ∀ eta ∈ Set.Ioo (-1) 1, ∀ (X : ℝ), L ≤ X → E (X, eta) = HeatedOutgoing.E F XR w.coefficients (X, eta)) (hreset : ∀ eta ∈ Set.Ioo (-1) 1, ∫ (X : ℝ) in Set.Ioi 0, √(2 * X) * E (X, eta) - OutgoingDilation.powerH F XR X = ∫ (X : ℝ) in Set.Ioi 0, HeatedOutgoing.H F XR w.coefficients (X, eta) - OutgoingDilation.powerH F XR X) {eta : ℝ} (heta : eta ∈ Set.Ioo (-1) 1) : MeasureTheory.IntegrableOn (fun (R : ℝ) => R ^ 2 * SlowStressSupport.axialOp2 F.data.h (SlowStressSupport.orderExponent F.data.h 0) G (R, eta)) (Set.Ioi 0) MeasureTheory.volume ∧ ∫ (R : ℝ) in Set.Ioi 0, R ^ 2 * SlowStressSupport.axialOp2 F.data.h (SlowStressSupport.orderExponent F.data.h 0) G (R, eta) = 0

theorem NavierStokes.FirstOrderBaseEdge.full_switch_monotone (F : OutgoingProfile.Profile) {XR R r : ℝ} (hXR : 0 < XR) (hR : 0 < R) (hr : R ≤ r) (hf : 1 / 2 < Real.log (R ^ 2 / 2 / OutgoingDilation.switchRadius F XR) + 1 / 5) : 1 / 2 < Real.log (r ^ 2 / 2 / OutgoingDilation.switchRadius F XR) + 1 / 5

theorem NavierStokes.FirstOrderBaseEdge.first_angular_eq_backward (F : OutgoingProfile.Profile) {XR cost L C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR cost) {S : Set ℝ} (s : GlobalSlowProfiles.Scheme S F.data.h C) (hS : Set.Ioo (-1) 1 ⊆ S) (hbase : s.base.beta = GlobalSlowProfiles.betaFromU ⋯ 0 s.base.axial) {E : ℝ × ℝ → ℝ} (hGE : ∀ (R : ℝ), 0 < R → ∀ eta ∈ Set.Ioo (-1) 1, GlobalStressSupport.angularHistory s 0 (R, eta) = E (R ^ 2 / 2, eta)) (hmatch : ∀ eta ∈ Set.Ioo (-1) 1, ∀ (X : ℝ), L ≤ X → E (X, eta) = HeatedOutgoing.E F XR w.coefficients (X, eta)) (hreset : ∀ eta ∈ Set.Ioo (-1) 1, ∫ (X : ℝ) in Set.Ioi 0, √(2 * X) * E (X, eta) - OutgoingDilation.powerH F XR X = ∫ (X : ℝ) in Set.Ioi 0, HeatedOutgoing.H F XR w.coefficients (X, eta) - OutgoingDilation.powerH F XR X) {R eta : ℝ} (hR : s.B ≤ R) (heta : eta ∈ Set.Ioo (-1) 1) (hL : L < R ^ 2 / 2) (hfull : 1 / 2 < Real.log (R ^ 2 / 2 / OutgoingDilation.switchRadius F XR) + 1 / 5) : SlowStressSupport.stress 2 (SlowResidualMatching.thetaDensity F.data.h C (GlobalSlowProfiles.asSlowProfiles s) 1) (R, eta) = SlowFirstOrderEdge.radialStress (TerminalHistoryBridge.normalization F XR) F.data (TerminalHistoryBridge.shift F XR) eta R

The forward first-order primitive equals the backward terminal one. The total viscosity moment is derived from the same original reset row.

Identifying the common extension with its actual radial primitive

theorem NavierStokes.FirstOrderBaseEdge.coefficients_stress_eq_window {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : GlobalSlowProfiles.Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : GlobalSlowProfiles.Localization s A inner) (B0 : GlobalSlowProfiles.BaseAgreement s A inner) (Z0 : AssembledSlowBase.ZeroOrderSolved s inner) (hI : Set.Icc (-1) 1 ⊆ S) (n : ℕ) {p : ℝ × ℝ} (hX : 0 ≤ p.1) (heta : |p.2| ≤ (AssembledSlowBase.commonWindow s hI).inner) : (AssembledSlowBase.coefficients L B0 Z0 hI).stressTheta n p = SlowResidualMatching.thetaStress h C (GlobalSlowProfiles.asSlowProfiles s) n p ∧ (AssembledSlowBase.coefficients L B0 Z0 hI).stressAxial n p = SlowResidualMatching.zStress h (GlobalSlowProfiles.asSlowProfiles s) n p

theorem NavierStokes.FirstOrderBaseEdge.coefficients_stress_germ {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : GlobalSlowProfiles.Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : GlobalSlowProfiles.Localization s A inner) (B0 : GlobalSlowProfiles.BaseAgreement s A inner) (Z0 : AssembledSlowBase.ZeroOrderSolved s inner) (hI : Set.Icc (-1) 1 ⊆ S) (n : ℕ) {p : ℝ × ℝ} (hX : 0 < p.1) (heta : |p.2| ≤ 1) : (fun (q : ℝ × ℝ) => ((AssembledSlowBase.coefficients L B0 Z0 hI).stressTheta n q, (AssembledSlowBase.coefficients L B0 Z0 hI).stressAxial n q)) =ᶠ[nhds p] fun (q : ℝ × ℝ) => (SlowResidualMatching.thetaStress h C (GlobalSlowProfiles.asSlowProfiles s) n q, SlowResidualMatching.zStress h (GlobalSlowProfiles.asSlowProfiles s) n q)

theorem NavierStokes.FirstOrderBaseEdge.nominal_angular_zero_eq {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {R eta : ℝ} (hR : 0 < R) (heta : eta ∈ AssembledSlowBase.nominalParameters W) : GlobalStressSupport.angularHistory (AssembledSlowBase.nominalScheme W) 0 (R, eta) = W.E (R ^ 2 / 2, eta)

theorem NavierStokes.FirstOrderBaseEdge.nominal_axial_mass_zero {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {eta : ℝ} (heta : eta ∈ AssembledSlowBase.nominalParameters W) : SlowStressSupport.moment (AssembledSlowBase.nominalScheme W).B 1 (GlobalStressSupport.axialHistory (AssembledSlowBase.nominalScheme W) 0) eta = 0

theorem NavierStokes.FirstOrderBaseEdge.nominal_first_axial_zero {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : ℝ × ℝ} (hX : AssembledSlowBase.nominalOuterX W ≤ p.1) : (AssembledSlowBase.nominalCoefficients W).stressAxial 1 p = 0

theorem NavierStokes.FirstOrderBaseEdge.nominal_first_angular_eq {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : ℝ × ℝ} (hX : AssembledSlowBase.nominalOuterX W < p.1) (heta : p.2 ∈ Set.Ioo (-1) 1) (hfull : 1 / 2 < Real.log (p.1 / OutgoingDilation.switchRadius F W.controls.radius) + 1 / 5) : (AssembledSlowBase.nominalCoefficients W).stressTheta 1 p = SlowFirstOrderEdge.stressX (TerminalHistoryBridge.normalization F W.controls.radius) F.data (TerminalHistoryBridge.shift F W.controls.radius) p

Closed-parameter derivative tensors and the weighted collar estimate

theorem NavierStokes.FirstOrderBaseEdge.iteratedFDeriv_eq_closed_parameter {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f g : ℝ × ℝ → V} {cut : ℝ} (hcut : 0 ≤ cut) (hf : ∀ (p : ℝ × ℝ), 0 < p.1 → ContDiffAt ℝ (↑⊤) f p) (hg : ∀ (p : ℝ × ℝ), 0 < p.1 → ContDiffAt ℝ (↑⊤) g p) (he : Set.EqOn f g (Set.Ioi cut ×ˢ Set.Ioo (-1) 1)) (m : ℕ) {p : ℝ × ℝ} (hp : cut < p.1) (heta : p.2 ∈ Set.Icc (-1) 1) : iteratedFDeriv ℝ m f p = iteratedFDeriv ℝ m g p

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

Terminal amplitude, given by TerminalHistoryBridge.normalization F W.controls.radius.

Equations

• NavierStokes.FirstOrderBaseEdge.terminalAmplitude W = NavierStokes.TerminalHistoryBridge.normalization F W.controls.radius

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

Terminal shift, given by TerminalHistoryBridge.shift F W.controls.radius.

Equations

• NavierStokes.FirstOrderBaseEdge.terminalShift W = NavierStokes.TerminalHistoryBridge.shift F W.controls.radius

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

Terminal inner, given by Real.exp (terminalShift W + 1).

Equations

• NavierStokes.FirstOrderBaseEdge.terminalInner W = Real.exp (NavierStokes.FirstOrderBaseEdge.terminalShift W + 1)

theorem NavierStokes.FirstOrderBaseEdge.terminalInner_pos {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : 0 < terminalInner W

theorem NavierStokes.FirstOrderBaseEdge.switch_lt_terminalInner {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : OutgoingDilation.switchRadius F W.controls.radius < terminalInner W

theorem NavierStokes.FirstOrderBaseEdge.terminalInner_full {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {X : ℝ} (hX : terminalInner W < X) : AssembledSlowBase.nominalOuterX W < X ∧ 1 / 2 < Real.log (X / OutgoingDilation.switchRadius F W.controls.radius) + 1 / 5

theorem NavierStokes.FirstOrderBaseEdge.nominal_first_pair_eq {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : Set.EqOn (BaseResidual.stressPair (AssembledSlowBase.nominalCoefficients W) 1) (fun (p : SlowBorelBase.Inner) => (SlowFirstOrderEdge.stressX (terminalAmplitude W) F.data (terminalShift W) p, 0)) (Set.Ioi (terminalInner W) ×ˢ Set.Ioo (-1) 1)

theorem NavierStokes.FirstOrderBaseEdge.edgeJets_of_interior_equality {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {f : ℝ × ℝ → ℝ × ℝ} (hf : ContDiff ℝ (↑⊤) f) (he : Set.EqOn f (fun (p : ℝ × ℝ) => (SlowFirstOrderEdge.stressX (terminalAmplitude W) F.data (terminalShift W) p, 0)) (Set.Ioi (terminalInner W) ×ˢ Set.Ioo (-1) 1)) {c left : ℝ} (hc : 0 < c) (hl : left < terminalShift W + 2) : BaseResidual.PolynomialEdgeJets (BaseResidual.outerWindow (Real.exp (terminalShift W + 3 - 1)) (terminalShift W + 3)) (BaseResidual.activeZeta c left (terminalShift W + 3)) (BaseResidual.activeDelta left (terminalShift W + 3)) f

The scalar terminal factor has the same entire derivative tensor as the actual stress through both physical parameter endpoints. The proof uses continuity of each tensor, without identifying different outside extensions.

theorem NavierStokes.FirstOrderBaseEdge.nominal_first_edgeJets {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {c left : ℝ} (hc : 0 < c) (hl : left < terminalShift W + 2) : BaseResidual.PolynomialEdgeJets (BaseResidual.outerWindow (Real.exp (terminalShift W + 3 - 1)) (terminalShift W + 3)) (BaseResidual.activeZeta c left (terminalShift W + 3)) (BaseResidual.activeDelta left (terminalShift W + 3)) (BaseResidual.stressPair (AssembledSlowBase.nominalCoefficients W) 1)

Transfer through a finite modification with the restored angular row

theorem NavierStokes.FirstOrderBaseEdge.moment_axialOp_congr {S : Set ℝ} (hS : IsOpen S) {f g : SlowStressSupport.Field} (hf : SlowStressSupport.Smooth S f) (hg : SlowStressSupport.Smooth S g) (h b R : ℝ) (m : ℕ) (hm : ∀ eta ∈ S, SlowStressSupport.moment R m f eta = SlowStressSupport.moment R m g eta) (hb : ∀ eta ∈ S, f (R, eta) = g (R, eta)) {eta : ℝ} (heta : eta ∈ S) : SlowStressSupport.moment R m (SlowStressSupport.axialOp h b f) eta = SlowStressSupport.moment R m (SlowStressSupport.axialOp h b g) eta

theorem NavierStokes.FirstOrderBaseEdge.moment_axialOp2_congr {S : Set ℝ} (hS : IsOpen S) {f g : SlowStressSupport.Field} (hf : SlowStressSupport.Smooth S f) (hg : SlowStressSupport.Smooth S g) (h b R : ℝ) (m : ℕ) (hL : ∀ eta ∈ S, PositiveAxisSystem.ell h eta ≠ 0) (hm : ∀ eta ∈ S, SlowStressSupport.moment R m f eta = SlowStressSupport.moment R m g eta) (hfg : ∀ eta ∈ S, f =ᶠ[nhds (R, eta)] g) {eta : ℝ} (heta : eta ∈ S) : SlowStressSupport.moment R m (SlowStressSupport.axialOp2 h b f) eta = SlowStressSupport.moment R m (SlowStressSupport.axialOp2 h b g) eta

theorem NavierStokes.FirstOrderBaseEdge.angular_moment_of_baseFields {S : Set ℝ} {h C : ℝ} {D : ProfileHistories.RadialDomain} (d : GlobalSlowProfiles.Domain S h) (P : ProfileHistories.Profiles D) (hD : ∀ (X : ℝ), 0 ≤ X → ∀ eta ∈ S, (X, eta) ∈ D.carrier) (hC : C ≠ 0) {R eta : ℝ} (hR : 0 ≤ R) (heta : eta ∈ S) : SlowStressSupport.moment R 2 (GlobalSlowProfiles.angularField C (AssembledSlowBase.baseFields d C P hD).phi) eta = P.I (R ^ 2 / 2, eta)

theorem NavierStokes.FirstOrderBaseEdge.scheme_angular_moment_zero {S : Set ℝ} {h C R eta : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (heta : eta ∈ S) : SlowStressSupport.moment R 2 (GlobalStressSupport.angularHistory s 0) eta = SlowStressSupport.moment R 2 (GlobalSlowProfiles.angularField C s.base.phi) eta

theorem NavierStokes.FirstOrderBaseEdge.history_equal_after {D D' : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles D') {R X eta : ℝ} (hR : 0 ≤ R) (hX : R ≤ X) (hP : ∀ x ∈ Set.Icc 0 X, (x, eta) ∈ D.carrier) (hQ : ∀ x ∈ Set.Icc 0 X, (x, eta) ∈ D'.carrier) (hI : P.I (R, eta) = Q.I (R, eta)) (he : ∀ x ∈ Set.Icc R X, P.f (x, eta) = Q.f (x, eta)) : P.I (X, eta) = Q.I (X, eta)

theorem NavierStokes.FirstOrderBaseEdge.modified_angular_history {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) (hI : ∀ eta ∈ S, Q.I (AssembledSlowBase.nominalOuterX W, eta) = W.profiles.I (AssembledSlowBase.nominalOuterX W, eta)) {X eta : ℝ} (hX : AssembledSlowBase.nominalOuterX W ≤ X) (heta : eta ∈ S) : Q.I (X, eta) = W.profiles.I (X, eta)

theorem NavierStokes.FirstOrderBaseEdge.modified_angular_moment_eq {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) (hI : ∀ eta ∈ S, Q.I (AssembledSlowBase.nominalOuterX W, eta) = W.profiles.I (AssembledSlowBase.nominalOuterX W, eta)) {R eta : ℝ} (hR : AssembledSlowBase.nominalOuterRadius W ≤ R) (heta : eta ∈ S) : SlowStressSupport.moment R 2 (GlobalStressSupport.angularHistory (AssembledSlowBase.modifiedScheme W Q M) 0) eta = SlowStressSupport.moment R 2 (GlobalStressSupport.angularHistory (AssembledSlowBase.nominalScheme W) 0) eta

theorem NavierStokes.FirstOrderBaseEdge.modified_angular_zero_eq {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) {R eta : ℝ} (hR : 0 ≤ R) (heta : eta ∈ S) : GlobalStressSupport.angularHistory (AssembledSlowBase.modifiedScheme W Q M) 0 (R, eta) = Q.E (R ^ 2 / 2, eta)

theorem NavierStokes.FirstOrderBaseEdge.modified_angular_zero_germ {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) {R eta : ℝ} (hR : AssembledSlowBase.nominalOuterRadius W < R) (heta : eta ∈ S) : GlobalStressSupport.angularHistory (AssembledSlowBase.modifiedScheme W Q M) 0 =ᶠ[nhds (R, eta)] GlobalStressSupport.angularHistory (AssembledSlowBase.nominalScheme W) 0

theorem NavierStokes.FirstOrderBaseEdge.modified_viscosity_moment_eq {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) (hI : ∀ eta ∈ S, Q.I (AssembledSlowBase.nominalOuterX W, eta) = W.profiles.I (AssembledSlowBase.nominalOuterX W, eta)) {R eta : ℝ} (hR : AssembledSlowBase.nominalOuterRadius W < R) (heta : eta ∈ S) : SlowStressSupport.moment R 2 (SlowStressSupport.axialOp2 F.data.h (SlowStressSupport.orderExponent F.data.h 0) (GlobalStressSupport.angularHistory (AssembledSlowBase.modifiedScheme W Q M) 0)) eta = SlowStressSupport.moment R 2 (SlowStressSupport.axialOp2 F.data.h (SlowStressSupport.orderExponent F.data.h 0) (GlobalStressSupport.angularHistory (AssembledSlowBase.nominalScheme W) 0)) eta

theorem NavierStokes.FirstOrderBaseEdge.outerRadius_lt_sqrt {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {X : ℝ} (hX : AssembledSlowBase.nominalOuterX W < X) : AssembledSlowBase.nominalOuterRadius W < √(2 * X)

theorem NavierStokes.FirstOrderBaseEdge.modified_first_theta_eq_nominal {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) (hI : ∀ eta ∈ S, Q.I (AssembledSlowBase.nominalOuterX W, eta) = W.profiles.I (AssembledSlowBase.nominalOuterX W, eta)) {p : ℝ × ℝ} (hX : AssembledSlowBase.nominalOuterX W < p.1) (heta : |p.2| ≤ 1) : (AssembledSlowBase.modifiedCoefficients W Q M).stressTheta 1 p = (AssembledSlowBase.nominalCoefficients W).stressTheta 1 p

theorem NavierStokes.FirstOrderBaseEdge.modified_axial_mass_zero {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) {eta : ℝ} (heta : eta ∈ S) : SlowStressSupport.moment (AssembledSlowBase.modifiedScheme W Q M).B 1 (GlobalStressSupport.axialHistory (AssembledSlowBase.modifiedScheme W Q M) 0) eta = 0

theorem NavierStokes.FirstOrderBaseEdge.modified_first_axial_zero {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) {p : ℝ × ℝ} (hX : AssembledSlowBase.nominalOuterX W ≤ p.1) : (AssembledSlowBase.modifiedCoefficients W Q M).stressAxial 1 p = 0

theorem NavierStokes.FirstOrderBaseEdge.modified_first_pair_eq {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) (hI : ∀ eta ∈ S, Q.I (AssembledSlowBase.nominalOuterX W, eta) = W.profiles.I (AssembledSlowBase.nominalOuterX W, eta)) : Set.EqOn (BaseResidual.stressPair (AssembledSlowBase.modifiedCoefficients W Q M) 1) (fun (p : SlowBorelBase.Inner) => (SlowFirstOrderEdge.stressX (terminalAmplitude W) F.data (terminalShift W) p, 0)) (Set.Ioi (terminalInner W) ×ˢ Set.Ioo (-1) 1)

theorem NavierStokes.FirstOrderBaseEdge.modified_first_edgeJets {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) (hI : ∀ eta ∈ S, Q.I (AssembledSlowBase.nominalOuterX W, eta) = W.profiles.I (AssembledSlowBase.nominalOuterX W, eta)) {c left : ℝ} (hc : 0 < c) (hl : left < terminalShift W + 2) : BaseResidual.PolynomialEdgeJets (BaseResidual.outerWindow (Real.exp (terminalShift W + 3 - 1)) (terminalShift W + 3)) (BaseResidual.activeZeta c left (terminalShift W + 3)) (BaseResidual.activeDelta left (terminalShift W + 3)) (BaseResidual.stressPair (AssembledSlowBase.modifiedCoefficients W Q M) 1)

Changing the hierarchy cutoff while retaining the same leading fields

theorem NavierStokes.FirstOrderBaseEdge.first_axial_balance {S : Set ℝ} {h C R : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hbase : s.base.beta = GlobalSlowProfiles.betaFromU ⋯ 0 s.base.axial) (hR : s.B ≤ R) {eta : ℝ} (heta : eta ∈ S) : SlowStressSupport.stress 1 (SlowResidualMatching.zDensity h (GlobalSlowProfiles.asSlowProfiles s) 1) (R, eta) = SlowStressSupport.moment R 1 (SlowStressSupport.axialOp2 h (SlowStressSupport.orderExponent h 0) (GlobalStressSupport.axialHistory s 0)) eta / R

theorem NavierStokes.FirstOrderBaseEdge.moment_axialOp2_eq_of_eqOn {S : Set ℝ} (hS : IsOpen S) {f g : SlowStressSupport.Field} (hf : SlowStressSupport.Smooth S f) (hg : SlowStressSupport.Smooth S g) (he : Set.EqOn f g (Set.univ ×ˢ S)) (h b R : ℝ) (m : ℕ) (hL : ∀ eta ∈ S, PositiveAxisSystem.ell h eta ≠ 0) {eta : ℝ} (heta : eta ∈ S) : SlowStressSupport.moment R m (SlowStressSupport.axialOp2 h b f) eta = SlowStressSupport.moment R m (SlowStressSupport.axialOp2 h b g) eta

theorem NavierStokes.FirstOrderBaseEdge.first_stresses_eq_of_leading {S : Set ℝ} {h C C' R eta : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (t : GlobalSlowProfiles.Scheme S h C') (hs : s.base.beta = GlobalSlowProfiles.betaFromU ⋯ 0 s.base.axial) (ht : t.base.beta = GlobalSlowProfiles.betaFromU ⋯ 0 t.base.axial) (he : Set.EqOn (GlobalStressSupport.angularHistory s 0) (GlobalStressSupport.angularHistory t 0) (Set.univ ×ˢ S)) (hu : Set.EqOn (GlobalStressSupport.axialHistory s 0) (GlobalStressSupport.axialHistory t 0) (Set.univ ×ˢ S)) (hRs : s.B ≤ R) (hRt : t.B ≤ R) (heta : eta ∈ S) : SlowStressSupport.stress 2 (SlowResidualMatching.thetaDensity h C (GlobalSlowProfiles.asSlowProfiles s) 1) (R, eta) = SlowStressSupport.stress 2 (SlowResidualMatching.thetaDensity h C' (GlobalSlowProfiles.asSlowProfiles t) 1) (R, eta) ∧ SlowStressSupport.stress 1 (SlowResidualMatching.zDensity h (GlobalSlowProfiles.asSlowProfiles s) 1) (R, eta) = SlowStressSupport.stress 1 (SlowResidualMatching.zDensity h (GlobalSlowProfiles.asSlowProfiles t) 1) (R, eta)

The first stress outside both repair regions depends only on the actual order-zero angular and axial fields. It is unchanged by moving the common hierarchy cutoff or by rebuilding the positive-order repair.

theorem NavierStokes.FirstOrderBaseEdge.coefficients_first_pair_eq_modified {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) {C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : GlobalSlowProfiles.Scheme S F.data.h C} {A : SlowRecursion.LocalHierarchy rho U F.data.h C base} (L : GlobalSlowProfiles.Localization s A inner) (B0 : GlobalSlowProfiles.BaseAgreement s A inner) (Z0 : AssembledSlowBase.ZeroOrderSolved s inner) (hI : Set.Icc (-1) 1 ⊆ S) (hbase : s.base.beta = GlobalSlowProfiles.betaFromU ⋯ 0 s.base.axial) (hB : s.B ≤ AssembledSlowBase.nominalOuterRadius W) (he : Set.EqOn (GlobalStressSupport.angularHistory s 0) (GlobalStressSupport.angularHistory (AssembledSlowBase.modifiedScheme W Q M) 0) (Set.univ ×ˢ S)) (hu : Set.EqOn (GlobalStressSupport.axialHistory s 0) (GlobalStressSupport.axialHistory (AssembledSlowBase.modifiedScheme W Q M) 0) (Set.univ ×ˢ S)) {p : ℝ × ℝ} (hp : AssembledSlowBase.nominalOuterX W < p.1) (heta : |p.2| ≤ 1) : BaseResidual.stressPair (AssembledSlowBase.coefficients L B0 Z0 hI) 1 p = BaseResidual.stressPair (AssembledSlowBase.modifiedCoefficients W Q M) 1 p

theorem NavierStokes.FirstOrderBaseEdge.coefficients_first_edgeJets {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) {C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : GlobalSlowProfiles.Scheme S F.data.h C} {A : SlowRecursion.LocalHierarchy rho U F.data.h C base} (L : GlobalSlowProfiles.Localization s A inner) (B0 : GlobalSlowProfiles.BaseAgreement s A inner) (Z0 : AssembledSlowBase.ZeroOrderSolved s inner) (hI : Set.Icc (-1) 1 ⊆ S) (hbase : s.base.beta = GlobalSlowProfiles.betaFromU ⋯ 0 s.base.axial) (hB : s.B ≤ AssembledSlowBase.nominalOuterRadius W) (he : Set.EqOn (GlobalStressSupport.angularHistory s 0) (GlobalStressSupport.angularHistory (AssembledSlowBase.modifiedScheme W Q M) 0) (Set.univ ×ˢ S)) (hu : Set.EqOn (GlobalStressSupport.axialHistory s 0) (GlobalStressSupport.axialHistory (AssembledSlowBase.modifiedScheme W Q M) 0) (Set.univ ×ˢ S)) (hrow : ∀ eta ∈ S, Q.I (AssembledSlowBase.nominalOuterX W, eta) = W.profiles.I (AssembledSlowBase.nominalOuterX W, eta)) {c left : ℝ} (hc : 0 < c) (hl : left < terminalShift W + 2) : BaseResidual.PolynomialEdgeJets (BaseResidual.outerWindow (Real.exp (terminalShift W + 3 - 1)) (terminalShift W + 3)) (BaseResidual.activeZeta c left (terminalShift W + 3)) (BaseResidual.activeDelta left (terminalShift W + 3)) (BaseResidual.stressPair (AssembledSlowBase.coefficients L B0 Z0 hI) 1)

theorem NavierStokes.FirstOrderBaseEdge.first_pair_jets_of_interior_equality {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {f : ℝ × ℝ → ℝ × ℝ} (hf : ContDiff ℝ (↑⊤) f) (he : Set.EqOn f (fun (p : ℝ × ℝ) => (SlowFirstOrderEdge.stressX (terminalAmplitude W) F.data (terminalShift W) p, 0)) (Set.Ioi (terminalInner W) ×ˢ Set.Ioo (-1) 1)) (m : ℕ) {p : ℝ × ℝ} (hp : terminalInner W < p.1) (heta : p.2 ∈ Set.Icc (-1) 1) : iteratedFDeriv ℝ m f p = iteratedFDeriv ℝ m (fun (q : ℝ × ℝ) => (SlowFirstOrderEdge.stressX (terminalAmplitude W) F.data (terminalShift W) q, 0)) p

Every ambient derivative tensor of the actual pair agrees with the terminal factor on the closed physical parameter interval.

theorem NavierStokes.FirstOrderBaseEdge.first_pair_zero_right {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {f : ℝ × ℝ → ℝ × ℝ} (hf : ContDiff ℝ (↑⊤) f) (he : Set.EqOn f (fun (p : ℝ × ℝ) => (SlowFirstOrderEdge.stressX (terminalAmplitude W) F.data (terminalShift W) p, 0)) (Set.Ioi (terminalInner W) ×ˢ Set.Ioo (-1) 1)) {p : ℝ × ℝ} (hp : Real.exp (terminalShift W + 3) ≤ p.1) (heta : p.2 ∈ Set.Icc (-1) 1) : f p = 0

theorem NavierStokes.FirstOrderBaseEdge.physical_first_pair {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {f : ℝ × ℝ → ℝ × ℝ} (he : Set.EqOn f (fun (p : ℝ × ℝ) => (SlowFirstOrderEdge.stressX (terminalAmplitude W) F.data (terminalShift W) p, 0)) (Set.Ioi (terminalInner W) ×ˢ Set.Ioo (-1) 1)) {t r z : ℝ} (ht : t < 1) (hr : 0 < r) (hX : terminalInner W < SimilarityProfile.X F.data.h (TerminalStress.radiusPoint t r z)) : SimilarityProfile.q F.data.h (TerminalStress.radiusPoint t r z) ^ (-CoordinateAlgebra.A F.data.h - 1 / 2 + 2 * F.data.h) • f (SimilarityProfile.inner F.data.h (TerminalStress.radiusPoint t r z)) = (SlowFirstOrderEdge.physicalStress (terminalAmplitude W) F.data (terminalShift W) t z r, 0)

The tensor scale is the exact first slow-order scale q^(-A-1/2+2h), and the angular term is the actual physical backward primitive of minus the second axial derivative.

theorem NavierStokes.FirstOrderBaseEdge.nominal_first_jets {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (m : ℕ) {p : ℝ × ℝ} (hp : terminalInner W < p.1) (heta : p.2 ∈ Set.Icc (-1) 1) : iteratedFDeriv ℝ m (BaseResidual.stressPair (AssembledSlowBase.nominalCoefficients W) 1) p = iteratedFDeriv ℝ m (fun (q : ℝ × ℝ) => (SlowFirstOrderEdge.stressX (terminalAmplitude W) F.data (terminalShift W) q, 0)) p

theorem NavierStokes.FirstOrderBaseEdge.modulated_first_edgeJets {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) {c left : ℝ} (hc : 0 < c) (hl : left < terminalShift W + 2) : BaseResidual.PolynomialEdgeJets (BaseResidual.outerWindow (Real.exp (terminalShift W + 3 - 1)) (terminalShift W + 3)) (BaseResidual.activeZeta c left (terminalShift W + 3)) (BaseResidual.activeDelta left (terminalShift W + 3)) (BaseResidual.stressPair (AssembledSlowBase.modifiedCoefficients W v.profiles ⋯) 1)

The actual constructed modulation witness supplies the additional angular anchor, using the same profile and the same finite modification.