The natural core solves the actual order-zero residual equations

The natural solution is the one retained by NaturalEntrance.CoefficientProfile. Its scalar swirl is normalized as phi = C*f, its pressure is unchanged, and its radial flux is X*beta. The two residual equations below are derived from the constructed natural equations, not assumed as slow-order hypotheses.

theorem NavierStokes.NaturalCoefficientBridge.nat_le_infty (n : ℕ) : ↑n ≤ ↑⊤

theorem NavierStokes.NaturalCoefficientBridge.partialX_eq_slice {f : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hf : DifferentiableAt ℝ f w) : SimilarityProfile.partialX f w = deriv (fun (x : ℝ) => f (x, w.2)) w.1

theorem NavierStokes.NaturalCoefficientBridge.partialEta_eq_slice {f : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hf : DifferentiableAt ℝ f w) : SimilarityProfile.partialEta f w = deriv (fun (η : ℝ) => f (w.1, η)) w.2

theorem NavierStokes.NaturalCoefficientBridge.secondX_eq_slice {f : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hf : ContDiffAt ℝ (↑⊤) f w) : SimilarityProfile.partialX (SimilarityProfile.partialX f) w = iteratedDeriv 2 (fun (x : ℝ) => f (x, w.2)) w.1

theorem NavierStokes.NaturalCoefficientBridge.radialDifferential_eq {f : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hf : ContDiffAt ℝ (↑⊤) f w) (m : ℕ) : NaturalAxisBridge.radialDifferential m f w = w.1 * SimilarityProfile.partialX (SimilarityProfile.partialX f) w + ↑m * SimilarityProfile.partialX f w

theorem NavierStokes.NaturalCoefficientBridge.partialX_const_mul (C : ℝ) {f : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hf : DifferentiableAt ℝ f w) : SimilarityProfile.partialX (fun (p : SimilarityProfile.InnerPoint) => C * f p) w = C * SimilarityProfile.partialX f w

theorem NavierStokes.NaturalCoefficientBridge.partialEta_const_mul (C : ℝ) {f : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hf : DifferentiableAt ℝ f w) : SimilarityProfile.partialEta (fun (p : SimilarityProfile.InnerPoint) => C * f p) w = C * SimilarityProfile.partialEta f w

theorem NavierStokes.NaturalCoefficientBridge.secondX_const_mul (C : ℝ) {f : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hf : ContDiffAt ℝ (↑⊤) f w) : SimilarityProfile.partialX (SimilarityProfile.partialX fun (p : SimilarityProfile.InnerPoint) => C * f p) w = C * SimilarityProfile.partialX (SimilarityProfile.partialX f) w

noncomputable def NavierStokes.NaturalCoefficientBridge.naturalFlux (h : ℝ) (U V : SimilarityProfile.InnerProfile) (w : SimilarityProfile.InnerPoint) : ℝ

Flux reconstructed from the actual natural radial average.

Equations

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

noncomputable def NavierStokes.NaturalCoefficientBridge.zeroSequence (f : SimilarityProfile.InnerProfile) (n : ℕ) : SimilarityProfile.InnerProfile

Zero sequence, with branches according to n = 0.

Equations

• NavierStokes.NaturalCoefficientBridge.zeroSequence f n = if n = 0 then f else fun (x : NavierStokes.SimilarityProfile.InnerPoint) => 0

noncomputable def NavierStokes.NaturalCoefficientBridge.naturalProfiles (h C : ℝ) (f U V P : SimilarityProfile.InnerProfile) : SlowExpansionResidual.SlowProfiles

Natural profiles, bundling phi, axial, flux, pressure.

Equations

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

theorem NavierStokes.NaturalCoefficientBridge.angular_zero_formula (h : ℝ) (f : SlowExpansionResidual.SlowProfiles) (w : SimilarityProfile.InnerPoint) : SlowExpansionResidual.angularCoefficient h f 0 w = SimilarityProfile.T h (SlowExpansionResidual.angularExponent h) (f.phi 0) w - 2 * (w.1 * SimilarityProfile.partialX (SimilarityProfile.partialX (f.phi 0)) w + 2 * SimilarityProfile.partialX (f.phi 0) w) + (f.flux 0 w * (SimilarityProfile.partialX (f.phi 0) w + f.phi 0 w / w.1) + f.axial 0 w * SimilarityProfile.Z h (SlowExpansionResidual.angularExponent h) (f.phi 0) w)

theorem NavierStokes.NaturalCoefficientBridge.axial_zero_formula (h : ℝ) (f : SlowExpansionResidual.SlowProfiles) (w : SimilarityProfile.InnerPoint) : SlowExpansionResidual.axialCoefficient h f 0 w = SimilarityProfile.T h (SlowExpansionResidual.axialExponent h) (f.axial 0) w - 2 * (w.1 * SimilarityProfile.partialX (SimilarityProfile.partialX (f.axial 0)) w + SimilarityProfile.partialX (f.axial 0) w) + SimilarityProfile.Z h (SlowExpansionResidual.pressureExponent h) (f.pressure 0) w + (f.flux 0 w * SimilarityProfile.partialX (f.axial 0) w + f.axial 0 w * SimilarityProfile.Z h (SlowExpansionResidual.axialExponent h) (f.axial 0) w)

theorem NavierStokes.NaturalCoefficientBridge.natural_angular_zero {h j Λ : ℝ} {P0 a0 : ℝ → ℝ} {f U V P : SimilarityProfile.InnerProfile} (hs : NaturalProfile.IsNaturalSolution h j Λ P0 a0 f U V P) (C : ℝ) {w : SimilarityProfile.InnerPoint} (hw : w ∈ NaturalProfile.domain Λ) (hX : w.1 ≠ 0) (hL : CoordinateAlgebra.L h w.2 ≠ 0) : SlowExpansionResidual.angularCoefficient h (naturalProfiles h C f U V P) 0 w = 0

theorem NavierStokes.NaturalCoefficientBridge.natural_axial_zero {h j Λ : ℝ} {P0 a0 : ℝ → ℝ} {f U V P : SimilarityProfile.InnerProfile} (hs : NaturalProfile.IsNaturalSolution h j Λ P0 a0 f U V P) (C : ℝ) {w : SimilarityProfile.InnerPoint} (hw : w ∈ NaturalProfile.domain Λ) (hL : CoordinateAlgebra.L h w.2 ≠ 0) : SlowExpansionResidual.axialCoefficient h (naturalProfiles h C f U V P) 0 w = 0

theorem NavierStokes.NaturalCoefficientBridge.natural_average_eq {h j Λ : ℝ} {P0 a0 : ℝ → ℝ} {f U V P : SimilarityProfile.InnerProfile} (hs : NaturalProfile.IsNaturalSolution h j Λ P0 a0 f U V P) {w : SimilarityProfile.InnerPoint} (hw : w ∈ NaturalProfile.domain Λ) : V w = ProfileHistories.average U w

The natural average is the genuine radial average, including the axis.

theorem NavierStokes.NaturalCoefficientBridge.naturalFlux_eq_radialFlux {h j Λ : ℝ} {P0 a0 : ℝ → ℝ} {f U V P : SimilarityProfile.InnerProfile} (hs : NaturalProfile.IsNaturalSolution h j Λ P0 a0 f U V P) {w : SimilarityProfile.InnerPoint} (hw : w ∈ NaturalProfile.domain Λ) : naturalFlux h U V w = SlowDivergence.radialFlux h 0 U w

The flux in the natural equations is precisely the canonical divergence primitive used by the slow recursion.

theorem NavierStokes.NaturalCoefficientBridge.natural_pressure_zero {h j Λ C : ℝ} {P0 a0 : ℝ → ℝ} {f U V P : SimilarityProfile.InnerProfile} (hs : NaturalProfile.IsNaturalSolution h j Λ P0 a0 f U V P) (hC : C ≠ 0) {w : SimilarityProfile.InnerPoint} (hw : w ∈ NaturalProfile.domain Λ) : SlowExpansionResidual.pressureCoefficient h C (naturalProfiles h C f U V P) 0 w = 0

The same unscaled pressure solves the normalized slow pressure equation; the C⁻² in that equation cancels the square of C*f.

theorem NavierStokes.NaturalCoefficientBridge.zero_of_natural_germs {h j Λ C : ℝ} {P0 a0 : ℝ → ℝ} {f U V P : SimilarityProfile.InnerProfile} (hs : NaturalProfile.IsNaturalSolution h j Λ P0 a0 f U V P) {g : SlowExpansionResidual.SlowProfiles} {w : SimilarityProfile.InnerPoint} (hw : w ∈ NaturalProfile.domain Λ) (hX : w.1 ≠ 0) (hL : CoordinateAlgebra.L h w.2 ≠ 0) (hphi : g.phi 0 =ᶠ[nhds w] fun (p : SimilarityProfile.InnerPoint) => C * f p) (hu : g.axial 0 =ᶠ[nhds w] U) (hv : g.flux 0 =ᶠ[nhds w] naturalFlux h U V) (hp : g.pressure 0 =ᶠ[nhds w] P) : SlowExpansionResidual.angularCoefficient h g 0 w = 0 ∧ SlowExpansionResidual.axialCoefficient h g 0 w = 0

Germ transfer to any actual slow sequence. Higher coefficients are irrelevant at order zero. No order-zero residual equation is a hypothesis.

theorem NavierStokes.NaturalCoefficientBridge.zero_of_radialFlux_germs {h j Λ C : ℝ} {P0 a0 : ℝ → ℝ} {f U V P : SimilarityProfile.InnerProfile} (hs : NaturalProfile.IsNaturalSolution h j Λ P0 a0 f U V P) {g : SlowExpansionResidual.SlowProfiles} {w : SimilarityProfile.InnerPoint} (hw : w ∈ NaturalProfile.domain Λ) (hX : w.1 ≠ 0) (hL : CoordinateAlgebra.L h w.2 ≠ 0) (hphi : g.phi 0 =ᶠ[nhds w] fun (p : SimilarityProfile.InnerPoint) => C * f p) (hu : g.axial 0 =ᶠ[nhds w] U) (hv : g.flux 0 =ᶠ[nhds w] SlowDivergence.radialFlux h 0 U) (hp : g.pressure 0 =ᶠ[nhds w] P) : SlowExpansionResidual.angularCoefficient h g 0 w = 0 ∧ SlowExpansionResidual.axialCoefficient h g 0 w = 0

noncomputable def NavierStokes.NaturalCoefficientBridge.initialBand (Λ : ℝ) : Set SimilarityProfile.InnerPoint

The closed initial segment on which ACT and the stock continuation retain the natural fields. Its parameter interval is open and contains [-1,1].

Equations

• NavierStokes.NaturalCoefficientBridge.initialBand Λ = Set.Icc 0 (4 / Λ) ×ˢ NavierStokes.ReferencePath.parameterInterval

noncomputable def NavierStokes.NaturalCoefficientBridge.initialCore (Λ : ℝ) : Set SimilarityProfile.InnerPoint

Initial core, given by Ioo (0 : ℝ) (4 / Λ) ×ˢ ReferencePath.parameterInterval.

Equations

• NavierStokes.NaturalCoefficientBridge.initialCore Λ = Set.Ioo 0 (4 / Λ) ×ˢ NavierStokes.ReferencePath.parameterInterval

theorem NavierStokes.NaturalCoefficientBridge.initialCore_open (Λ : ℝ) : IsOpen (initialCore Λ)

theorem NavierStokes.NaturalCoefficientBridge.initialCore_subset_band (Λ : ℝ) : initialCore Λ ⊆ initialBand Λ

theorem NavierStokes.NaturalCoefficientBridge.initialBand_mem_domain {Λ : ℝ} (hΛ : 0 < Λ) {w : SimilarityProfile.InnerPoint} (hw : w ∈ initialBand Λ) : w ∈ NaturalProfile.domain Λ

theorem NavierStokes.NaturalCoefficientBridge.radialFlux_congr_germ (h lam : ℝ) {U V : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hu : U =ᶠ[nhds w] V) (ha : ProfileHistories.average U =ᶠ[nhds w] ProfileHistories.average V) : SlowDivergence.radialFlux h lam U =ᶠ[nhds w] SlowDivergence.radialFlux h lam V

theorem NavierStokes.NaturalCoefficientBridge.initial_histories {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hP0 : ContDiff ℝ (↑⊤) P0) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) (hq0 : Q.pressure0 = P0) (hf : Set.EqOn Q.f F.f (initialBand Λ)) (hu : Set.EqOn Q.U F.U (initialBand Λ)) {w : SimilarityProfile.InnerPoint} (hw : w ∈ initialBand Λ) : Q.Ubar w = F.Ubar w ∧ Q.pressure w = F.Pi w

Initial field agreement determines the actual integral histories; no pressure or average matching is postulated separately.

theorem NavierStokes.NaturalCoefficientBridge.initial_germs {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hP0 : ContDiff ℝ (↑⊤) P0) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) (hq0 : Q.pressure0 = P0) (hf : Set.EqOn Q.f F.f (initialBand Λ)) (hu : Set.EqOn Q.U F.U (initialBand Λ)) {w : SimilarityProfile.InnerPoint} (hw : w ∈ initialCore Λ) : Q.f =ᶠ[nhds w] F.f ∧ Q.U =ᶠ[nhds w] F.U ∧ Q.Ubar =ᶠ[nhds w] F.Ubar ∧ Q.pressure =ᶠ[nhds w] F.Pi ∧ SlowDivergence.radialFlux h 0 Q.U =ᶠ[nhds w] SlowDivergence.radialFlux h 0 F.U

theorem NavierStokes.NaturalCoefficientBridge.zero_of_initial_profiles {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hP0 : ContDiff ℝ (↑⊤) P0) (hsmall : NaturalAxisData.SmallParameters h j) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) (hq0 : Q.pressure0 = P0) (hf : Set.EqOn Q.f F.f (initialBand Λ)) (hu : Set.EqOn Q.U F.U (initialBand Λ)) {g : SlowExpansionResidual.SlowProfiles} {w : SimilarityProfile.InnerPoint} (hw : w ∈ initialCore Λ) (hphi : g.phi 0 =ᶠ[nhds w] fun (p : SimilarityProfile.InnerPoint) => C * Q.f p) (haxial : g.axial 0 =ᶠ[nhds w] Q.U) (hflux : g.flux 0 =ᶠ[nhds w] SlowDivergence.radialFlux h 0 Q.U) (hpressure : g.pressure 0 =ᶠ[nhds w] Q.pressure) : SlowExpansionResidual.angularCoefficient h g 0 w = 0 ∧ SlowExpansionResidual.axialCoefficient h g 0 w = 0

The generic assembly interface: the natural equations are derived for any slow sequence whose order-zero fields are the same initial construction.

noncomputable def NavierStokes.NaturalCoefficientBridge.historiesProfiles {D : ProfileHistories.RadialDomain} (h C : ℝ) (Q : ProfileHistories.Profiles D) : SlowExpansionResidual.SlowProfiles

The order-zero profile sequence formed from genuine histories. The stored radial component is beta; ofBeta inserts its required factor X.

Equations

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

theorem NavierStokes.NaturalCoefficientBridge.historiesProfiles_flux {D : ProfileHistories.RadialDomain} (h C : ℝ) (Q : ProfileHistories.Profiles D) : (historiesProfiles h C Q).flux 0 = SlowDivergence.radialFlux h 0 Q.U

theorem NavierStokes.NaturalCoefficientBridge.transition_initial_fields {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) {T δ κ w₁ w₂ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) (hT : 0 < T) (hb : δ ≤ (TransitionRamp.ofNatural F hΛ hsmall hδ hδT hP0).bigTime) (hw₁ : 0 < w₁) (hw₂ : 0 < w₂) : have Q := TransitionRamp.physicalProfiles F hΛ hsmall hδ hδT hP0 hT hb hw₁ hw₂; Set.EqOn Q.f F.f (initialBand Λ) ∧ Set.EqOn Q.U F.U (initialBand Λ)

Concrete matching for the exact stock continuation later used by the nominal profile.

theorem NavierStokes.NaturalCoefficientBridge.transition_coefficients_zero {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) {T δ κ w₁ w₂ : ℝ} (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (hP0 : ContDiff ℝ (↑⊤) P0) (hT : 0 < T) (hb : δ ≤ (TransitionRamp.ofNatural F hΛ hsmall hδ hδT hP0).bigTime) (hw₁ : 0 < w₁) (hw₂ : 0 < w₂) {p : SimilarityProfile.InnerPoint} (hp : p ∈ initialCore Λ) : have Q := TransitionRamp.physicalProfiles F hΛ hsmall hδ hδT hP0 hT hb hw₁ hw₂; SlowExpansionResidual.angularCoefficient h (historiesProfiles h C Q) 0 p = 0 ∧ SlowExpansionResidual.axialCoefficient h (historiesProfiles h C Q) 0 p = 0

theorem NavierStokes.NaturalCoefficientBridge.hierarchy_flux_zero {N : ReferencePath.Input} {h R : ℝ} {P0 : ℝ → ℝ} {Ω : Set ℂ} (E : ActivationHolomorphic.InitialTube N h P0 R Ω) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) (C : ℝ) {X η : ℝ} (hX : X ∈ Set.Ioo 0 (ActualSlowAxis.axisRadius N δ ^ 2)) (hη : ↑η ∈ ActualSlowAxis.parameterDomain Ω) : have A := ActualSlowAxis.hierarchy E hT hδ hδT κ hP0 C; have Q := StressActivation.FromReference.histories N hT hδ hδT κ P0 hP0; (SlowResidualMatching.hierarchyProfiles A).flux 0 (X, η) = SlowDivergence.radialFlux h 0 Q.U (X, η)

At zero slow order the actual recursion's stored beta reconstructs the canonical flux of its own axial field, with no missing X factor.

theorem NavierStokes.NaturalCoefficientBridge.radial_densities_zero {h C r a : ℝ} {f : SlowExpansionResidual.SlowProfiles} {S : Set ℝ} (ha : a ^ 2 / 2 < r) (hzero : ∀ p ∈ Set.Ioo 0 r ×ˢ S, SlowExpansionResidual.angularCoefficient h f 0 p = 0 ∧ SlowExpansionResidual.axialCoefficient h f 0 p = 0) {R η : ℝ} (hR : R ∈ Set.Icc 0 a) (hη : η ∈ S) : SlowResidualMatching.thetaDensity h C f 0 (R, η) = 0 ∧ SlowResidualMatching.zDensity h f 0 (R, η) = 0

theorem NavierStokes.NaturalCoefficientBridge.radial_primitives_zero {h C r a : ℝ} {f : SlowExpansionResidual.SlowProfiles} {S : Set ℝ} (ha : a ^ 2 / 2 < r) (hzero : ∀ p ∈ Set.Ioo 0 r ×ˢ S, SlowExpansionResidual.angularCoefficient h f 0 p = 0 ∧ SlowExpansionResidual.axialCoefficient h f 0 p = 0) {R η : ℝ} (hR : R ∈ Set.Icc 0 a) (hη : η ∈ S) : ProfileHistories.primitive (SlowResidualMatching.thetaDensity h C f 0) (R, η) = 0 ∧ ProfileHistories.primitive (SlowResidualMatching.zDensity h f 0) (R, η) = 0

Both defining radial integrals vanish. This proves the integration constants are zero, rather than only proving a derivative equation.

theorem NavierStokes.NaturalCoefficientBridge.radial_stresses_zero {h C r a : ℝ} {f : SlowExpansionResidual.SlowProfiles} {S : Set ℝ} (ha : a ^ 2 / 2 < r) (hzero : ∀ p ∈ Set.Ioo 0 r ×ˢ S, SlowExpansionResidual.angularCoefficient h f 0 p = 0 ∧ SlowExpansionResidual.axialCoefficient h f 0 p = 0) {R η : ℝ} (hR : R ≤ a) (hη : η ∈ S) : SlowStressSupport.stress 2 (SlowResidualMatching.thetaDensity h C f 0) (R, η) = 0 ∧ SlowStressSupport.stress 1 (SlowResidualMatching.zDensity h f 0) (R, η) = 0

The canonical negative stress primitives are zero on the entire inner half-line, including their defined zero extension across the axis.

theorem NavierStokes.NaturalCoefficientBridge.activation_initial_fields {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalProfile.ProfileFamily d Λ C) (hΛ : 0 < Λ) (hP0 : ContDiff ℝ (↑⊤) P0) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) : have Q := StressActivation.FromReference.histories (ReferencePath.Input.ofNatural hΛ F) hT hδ hδT κ P0 hP0; Set.EqOn Q.f F.f (initialBand Λ) ∧ Set.EqOn Q.U F.U (initialBand Λ)

theorem NavierStokes.NaturalCoefficientBridge.fromNatural_coefficients_zero {h j σ Λ C : ℝ} {g a : ℝ → ℝ} {cap : ℝ} {P0 : ℝ → ℝ} (hp : PressureDatum.Admissible g a cap) (hP0 : P0 = PressureDatum.pressure g a) {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) {p : SimilarityProfile.InnerPoint} (hp0 : p ∈ initialCore Λ) (hpη : ↑p.2 ∈ ActualSlowAxis.parameterDomain (AxisHolomorphic.parameterTube ActivationHolomorphic.parameterWindow (ActualSlowAxis.tubeWidth hp hP0 F hΛ hsmall hσ))) : have A := ActualSlowAxis.fromNatural hp hP0 F hΛ hsmall hσ hT hδ hδT κ; SlowExpansionResidual.angularCoefficient h (SlowResidualMatching.hierarchyProfiles A) 0 p = 0 ∧ SlowExpansionResidual.axialCoefficient h (SlowResidualMatching.hierarchyProfiles A) 0 p = 0

The actual ActualSlowAxis.fromNatural hierarchy solves both order-zero equations on its natural core. This uses its constructed beta and recomputed pressure, not additional equations supplied to the hierarchy.

theorem NavierStokes.NaturalCoefficientBridge.fromNatural_primitives_and_stresses_zero {h j σ Λ C : ℝ} {g a : ℝ → ℝ} {cap : ℝ} {P0 : ℝ → ℝ} (hp : PressureDatum.Admissible g a cap) (hP0 : P0 = PressureDatum.pressure g a) {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : NaturalEntrance.CoefficientProfile d Λ C) (hΛ : 0 < Λ) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) {T δ : ℝ} (hT : 0 < T) (hδ : 0 < δ) (hδT : 2 * δ < ReferencePath.rampLimit) (κ : ℝ) {R η : ℝ} (hR : R ∈ Set.Icc 0 √(4 / Λ)) (hη : ↑η ∈ ActualSlowAxis.parameterDomain (AxisHolomorphic.parameterTube ActivationHolomorphic.parameterWindow (ActualSlowAxis.tubeWidth hp hP0 F hΛ hsmall hσ))) : have A := ActualSlowAxis.fromNatural hp hP0 F hΛ hsmall hσ hT hδ hδT κ; have f := SlowResidualMatching.hierarchyProfiles A; ProfileHistories.primitive (SlowResidualMatching.thetaDensity h C f 0) (R, η) = 0 ∧ ProfileHistories.primitive (SlowResidualMatching.zDensity h f 0) (R, η) = 0 ∧ SlowStressSupport.stress 2 (SlowResidualMatching.thetaDensity h C f 0) (R, η) = 0 ∧ SlowStressSupport.stress 1 (SlowResidualMatching.zDensity h f 0) (R, η) = 0

For the same constructed natural/ACT hierarchy, the defining integrals and both canonical stresses vanish on a fixed positive neighborhood of the axis. The radius here is strictly inside the natural coefficient core.