L4.2 assembly with automatic scalar Plemelj convergence

Radial regularization on bounded smooth Jordan carriers supplies the full frontier convergence previously threaded through the scalar-companion assembly as an analytic hypothesis. This file removes that hypothesis from the one-domain companion package and from the smooth-thickening L4.2 capstone.

The remaining inputs are the genuinely sharp phase contraction, polynomial approximation, and reproduction of the polynomial auxiliary contour.

theorem exists_continuous_scalarCompanion_approximation_of_boundaryPhaseTransform_radial {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (hkernel : ∀ z ∈ Omega.carrier, crouzeixScalarCauchyKernel Omega z = 1) (hphase : ∀ xi ∈ frontier Omega.carrier, ‖star (Polynomial.eval xi p) + crouzeixPolynomialBoundaryPhaseTransform Omega xi (p /ₘ (Polynomial.X - Polynomial.C xi))‖ ≤ polynomialSupNorm p (frontier Omega.carrier)) (r : ℕ → Polynomial ℂ) (happrox : ∀ (j : ℕ), ∀ z ∈ closure Omega.carrier, ‖Polynomial.eval z (r j) - crouzeixPolynomialScalarCompanionClosedExtension Omega p z‖ ≤ 1 / (↑j + 1)) (hPlemelj : crouzeixAuxiliaryOperator A Omega (crouzeixPolynomialScalarCompanionClosedExtension Omega p) = crouzeixPolynomialAuxiliaryOperator A Omega p) : ∃ (g : ℂ → ℂ) (q : ℕ → Polynomial ℂ), ContinuousOn g (Omega.boundaryParam '' Set.Icc 0 (2 * Real.pi)) ∧ (∀ z ∈ closure Omega.carrier, ‖g z‖ ≤ polynomialSupNorm p (closure Omega.carrier)) ∧ (∀ (j : ℕ), ∀ z ∈ closure Omega.carrier, ‖Polynomial.eval z (q j) - g z‖ ≤ 1 / (↑j + 1)) ∧ crouzeixAuxiliaryOperator A Omega g = crouzeixPolynomialAuxiliaryOperator A Omega p

On a winding-normalized smooth domain, exterior decay and radial geometry automatically supply boundedness and the convergence needed by the canonical phase-controlled scalar companion.

theorem crouzeixAuxiliaryOperator_congr_boundaryParam {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (f g : ℂ → ℂ) (hfg : ∀ t ∈ Set.Icc 0 (2 * Real.pi), f (Omega.boundaryParam t) = g (Omega.boundaryParam t)) : crouzeixAuxiliaryOperator A Omega f = crouzeixAuxiliaryOperator A Omega g

Auxiliary contours depend only on the scalar datum along the chosen boundary parametrization.

theorem crouzeixAuxiliaryOperator_congr_frontier {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (f g : ℂ → ℂ) (hfg : Set.EqOn f g (frontier Omega.carrier)) : crouzeixAuxiliaryOperator A Omega f = crouzeixAuxiliaryOperator A Omega g

In particular, equality on the geometric frontier determines the auxiliary contour.

theorem crouzeixAuxiliaryOperator_congr_closure {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (f g : ℂ → ℂ) (hfg : Set.EqOn f g (closure Omega.carrier)) : crouzeixAuxiliaryOperator A Omega f = crouzeixAuxiliaryOperator A Omega g

Equality on the carrier closure is therefore also sufficient.

theorem crouzeixAuxiliaryOperator_scalarCompanionClosedExtension_smul_of_cauchyKernel_eq_one {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (a : ℂ) (p : Polynomial ℂ) (hkernel : ∀ z ∈ Omega.carrier, crouzeixScalarCauchyKernel Omega z = 1) : crouzeixAuxiliaryOperator A Omega (crouzeixPolynomialScalarCompanionClosedExtension Omega (a • p)) = star a • crouzeixAuxiliaryOperator A Omega (crouzeixPolynomialScalarCompanionClosedExtension Omega p)

Scaling a polynomial conjugate-scales the auxiliary contour of its canonical closed companion.

theorem crouzeixAuxiliaryOperator_scalarCompanionClosedExtension_smul_eq_iff {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) {a : ℂ} (ha : a ≠ 0) (p : Polynomial ℂ) (hkernel : ∀ z ∈ Omega.carrier, crouzeixScalarCauchyKernel Omega z = 1) : crouzeixAuxiliaryOperator A Omega (crouzeixPolynomialScalarCompanionClosedExtension Omega (a • p)) = crouzeixPolynomialAuxiliaryOperator A Omega (a • p) ↔ crouzeixAuxiliaryOperator A Omega (crouzeixPolynomialScalarCompanionClosedExtension Omega p) = crouzeixPolynomialAuxiliaryOperator A Omega p

For a nonzero scalar, companion-contour reproduction is preserved and reflected by polynomial scaling.

theorem crouzeixAuxiliaryOperator_scalarCompanionClosedExtension_add_C_of_cauchyKernel_eq_one {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (a : ℂ) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) (hkernel : ∀ z ∈ Omega.carrier, crouzeixScalarCauchyKernel Omega z = 1) : crouzeixAuxiliaryOperator A Omega (crouzeixPolynomialScalarCompanionClosedExtension Omega (p + Polynomial.C a)) = crouzeixAuxiliaryOperator A Omega (crouzeixPolynomialScalarCompanionClosedExtension Omega p) + crouzeixPolynomialAuxiliaryOperator A Omega (Polynomial.C a)

Adding a constant polynomial shifts the canonical companion contour by exactly the constant-polynomial auxiliary operator.

theorem crouzeixAuxiliaryOperator_scalarCompanionClosedExtension_add_C_eq_iff {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (a : ℂ) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) (hkernel : ∀ z ∈ Omega.carrier, crouzeixScalarCauchyKernel Omega z = 1) : crouzeixAuxiliaryOperator A Omega (crouzeixPolynomialScalarCompanionClosedExtension Omega (p + Polynomial.C a)) = crouzeixPolynomialAuxiliaryOperator A Omega (p + Polynomial.C a) ↔ crouzeixAuxiliaryOperator A Omega (crouzeixPolynomialScalarCompanionClosedExtension Omega p) = crouzeixPolynomialAuxiliaryOperator A Omega p

The companion-contour reproduction identity is invariant under adding a constant polynomial. It may therefore be checked after any convenient constant normalization of p.

theorem crouzeixAuxiliaryOperator_scalarCompanionClosedExtension_affine_of_cauchyKernel_eq_one {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (a b : ℂ) (p : Polynomial ℂ) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) (hkernel : ∀ z ∈ Omega.carrier, crouzeixScalarCauchyKernel Omega z = 1) : crouzeixAuxiliaryOperator A Omega (crouzeixPolynomialScalarCompanionClosedExtension Omega (a • p + Polynomial.C b)) = star a • crouzeixAuxiliaryOperator A Omega (crouzeixPolynomialScalarCompanionClosedExtension Omega p) + crouzeixPolynomialAuxiliaryOperator A Omega (Polynomial.C b)

The auxiliary contour of the canonical companion satisfies the full conjugate-affine law.

theorem crouzeixAuxiliaryOperator_scalarCompanionClosedExtension_affine_eq_iff {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) {a : ℂ} (ha : a ≠ 0) (b : ℂ) (p : Polynomial ℂ) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) (hkernel : ∀ z ∈ Omega.carrier, crouzeixScalarCauchyKernel Omega z = 1) : crouzeixAuxiliaryOperator A Omega (crouzeixPolynomialScalarCompanionClosedExtension Omega (a • p + Polynomial.C b)) = crouzeixPolynomialAuxiliaryOperator A Omega (a • p + Polynomial.C b) ↔ crouzeixAuxiliaryOperator A Omega (crouzeixPolynomialScalarCompanionClosedExtension Omega p) = crouzeixPolynomialAuxiliaryOperator A Omega p

Reproduction is invariant under the full nondegenerate affine action on the source polynomial.

theorem crouzeixAuxiliaryOperator_scalarCompanionClosedExtension_eq_iff_sub_C_eval_zero {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) (hkernel : ∀ z ∈ Omega.carrier, crouzeixScalarCauchyKernel Omega z = 1) : crouzeixAuxiliaryOperator A Omega (crouzeixPolynomialScalarCompanionClosedExtension Omega p) = crouzeixPolynomialAuxiliaryOperator A Omega p ↔ crouzeixAuxiliaryOperator A Omega (crouzeixPolynomialScalarCompanionClosedExtension Omega (p - Polynomial.C (Polynomial.eval 0 p))) = crouzeixPolynomialAuxiliaryOperator A Omega (p - Polynomial.C (Polynomial.eval 0 p))

In particular, contour reproduction for p is equivalent to contour reproduction after normalizing its value at zero to vanish.

theorem crouzeixAuxiliaryOperator_scalarCompanionClosedExtension_of_normalized_vanishingAtZero {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) (hkernel : ∀ z ∈ Omega.carrier, crouzeixScalarCauchyKernel Omega z = 1) (hnormalized : ∀ (p : Polynomial ℂ), 0 < p.natDegree → Polynomial.eval 0 p = 0 → polynomialSupNorm p (frontier Omega.carrier) = 1 → crouzeixAuxiliaryOperator A Omega (crouzeixPolynomialScalarCompanionClosedExtension Omega p) = crouzeixPolynomialAuxiliaryOperator A Omega p) (p : Polynomial ℂ) : crouzeixAuxiliaryOperator A Omega (crouzeixPolynomialScalarCompanionClosedExtension Omega p) = crouzeixPolynomialAuxiliaryOperator A Omega p

Constant shifts, nonzero scaling, and the automatic constant case reduce companion-contour reproduction to positive-degree polynomials that vanish at zero and have frontier sup norm one.

theorem crouzeix_palencia_of_convexThickening_cauchy_support_boundaryPhase_radial_approximation {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : ℕ → SmoothJordanDomain) (hcarrier : ∀ (n : ℕ), (Omega n).carrier = convexThickeningApprox (closure (numericalRange A)) n) (hCauchyP : ∀ (p : Polynomial ℂ) (n : ℕ), (Polynomial.aeval A) p = (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => Polynomial.eval z p • resolvent A z) (Omega n).boundaryParam) (hsupport : ∀ (n : ℕ), ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ∀ w ∈ numericalRange A, ((starRingEnd ℂ) (-Complex.I * deriv (Omega n).boundaryParam t) * (w - (Omega n).boundaryParam t)).re ≤ 0) (hkernel : ∀ (n : ℕ), ∀ z ∈ (Omega n).carrier, crouzeixScalarCauchyKernel (Omega n) z = 1) (hphase : ∀ (p : Polynomial ℂ) (n : ℕ), ∀ xi ∈ frontier (Omega n).carrier, ‖star (Polynomial.eval xi p) + crouzeixPolynomialBoundaryPhaseTransform (Omega n) xi (p /ₘ (Polynomial.X - Polynomial.C xi))‖ ≤ polynomialSupNorm p (frontier (Omega n).carrier)) (happrox : ∀ (p : Polynomial ℂ) (n : ℕ), ∃ (r : ℕ → Polynomial ℂ), ∀ (j : ℕ), ∀ z ∈ compactThickeningApprox (closure (numericalRange A)) n, ‖Polynomial.eval z (r j) - crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p z‖ ≤ 1 / (↑j + 1)) (hPlemelj : ∀ (p : Polynomial ℂ) (n : ℕ), crouzeixAuxiliaryOperator A (Omega n) (crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p) = crouzeixPolynomialAuxiliaryOperator A (Omega n) p) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

The smooth-thickening scalar-companion capstone no longer assumes regularized frontier convergence: boundedness of each compact stage and the radial Plemelj theorem prove it internally.

theorem crouzeix_palencia_of_convexThickening_cauchy_support_boundaryPhase_radial_positiveDegree {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : ℕ → SmoothJordanDomain) (hcarrier : ∀ (n : ℕ), (Omega n).carrier = convexThickeningApprox (closure (numericalRange A)) n) (hCauchyP : ∀ (p : Polynomial ℂ) (n : ℕ), (Polynomial.aeval A) p = (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => Polynomial.eval z p • resolvent A z) (Omega n).boundaryParam) (hsupport : ∀ (n : ℕ), ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ∀ w ∈ numericalRange A, ((starRingEnd ℂ) (-Complex.I * deriv (Omega n).boundaryParam t) * (w - (Omega n).boundaryParam t)).re ≤ 0) (hkernel : ∀ (n : ℕ), ∀ z ∈ (Omega n).carrier, crouzeixScalarCauchyKernel (Omega n) z = 1) (hphase : ∀ (p : Polynomial ℂ) (n : ℕ), ∀ xi ∈ frontier (Omega n).carrier, ‖star (Polynomial.eval xi p) + crouzeixPolynomialBoundaryPhaseTransform (Omega n) xi (p /ₘ (Polynomial.X - Polynomial.C xi))‖ ≤ polynomialSupNorm p (frontier (Omega n).carrier)) (happrox : ∀ (p : Polynomial ℂ) (n : ℕ), 0 < p.natDegree → ∃ (r : ℕ → Polynomial ℂ), ∀ (j : ℕ), ∀ z ∈ compactThickeningApprox (closure (numericalRange A)) n, ‖Polynomial.eval z (r j) - crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p z‖ ≤ 1 / (↑j + 1)) (hPlemelj : ∀ (p : Polynomial ℂ) (n : ℕ), 0 < p.natDegree → crouzeixAuxiliaryOperator A (Omega n) (crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p) = crouzeixPolynomialAuxiliaryOperator A (Omega n) p) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

Constant companions and their auxiliary contours are automatic, so the approximation and contour-reproduction inputs need only be supplied for positive-degree polynomials.

theorem crouzeix_palencia_of_convexThickening_cauchy_support_boundaryPhase_induction_radial {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : ℕ → SmoothJordanDomain) (hcarrier : ∀ (n : ℕ), (Omega n).carrier = convexThickeningApprox (closure (numericalRange A)) n) (hCauchyP : ∀ (p : Polynomial ℂ) (n : ℕ), (Polynomial.aeval A) p = (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => Polynomial.eval z p • resolvent A z) (Omega n).boundaryParam) (hsupport : ∀ (n : ℕ), ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ∀ w ∈ numericalRange A, ((starRingEnd ℂ) (-Complex.I * deriv (Omega n).boundaryParam t) * (w - (Omega n).boundaryParam t)).re ≤ 0) (hkernel : ∀ (n : ℕ), ∀ z ∈ (Omega n).carrier, crouzeixScalarCauchyKernel (Omega n) z = 1) (hphaseStep : ∀ (n : ℕ) (p : Polynomial ℂ), 0 < p.natDegree → (∀ xi ∈ frontier (Omega n).carrier, CrouzeixBoundaryPhaseContractive (Omega n) (p /ₘ (Polynomial.X - Polynomial.C xi))) → CrouzeixBoundaryPhaseContractive (Omega n) p) (happrox : ∀ (p : Polynomial ℂ) (n : ℕ), ∃ (r : ℕ → Polynomial ℂ), ∀ (j : ℕ), ∀ z ∈ compactThickeningApprox (closure (numericalRange A)) n, ‖Polynomial.eval z (r j) - crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p z‖ ≤ 1 / (↑j + 1)) (hPlemelj : ∀ (p : Polynomial ℂ) (n : ℕ), crouzeixAuxiliaryOperator A (Omega n) (crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p) = crouzeixPolynomialAuxiliaryOperator A (Omega n) p) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

Automatic radial Plemelj convergence leaves only the strict-degree divided-difference induction step for the sharp boundary-phase invariant.

theorem crouzeixPalencia_of_thickening_cauchy_support_boundaryPhase_induction_radial_positiveDegree {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : ℕ → SmoothJordanDomain) (hcarrier : ∀ (n : ℕ), (Omega n).carrier = convexThickeningApprox (closure (numericalRange A)) n) (hCauchyP : ∀ (p : Polynomial ℂ) (n : ℕ), (Polynomial.aeval A) p = (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => Polynomial.eval z p • resolvent A z) (Omega n).boundaryParam) (hsupport : ∀ (n : ℕ), ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ∀ w ∈ numericalRange A, ((starRingEnd ℂ) (-Complex.I * deriv (Omega n).boundaryParam t) * (w - (Omega n).boundaryParam t)).re ≤ 0) (hkernel : ∀ (n : ℕ), ∀ z ∈ (Omega n).carrier, crouzeixScalarCauchyKernel (Omega n) z = 1) (hphaseStep : ∀ (n : ℕ) (p : Polynomial ℂ), 0 < p.natDegree → (∀ xi ∈ frontier (Omega n).carrier, CrouzeixBoundaryPhaseContractive (Omega n) (p /ₘ (Polynomial.X - Polynomial.C xi))) → CrouzeixBoundaryPhaseContractive (Omega n) p) (happrox : ∀ (p : Polynomial ℂ) (n : ℕ), 0 < p.natDegree → ∃ (r : ℕ → Polynomial ℂ), ∀ (j : ℕ), ∀ z ∈ compactThickeningApprox (closure (numericalRange A)) n, ‖Polynomial.eval z (r j) - crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p z‖ ≤ 1 / (↑j + 1)) (hPlemelj : ∀ (p : Polynomial ℂ) (n : ℕ), 0 < p.natDegree → crouzeixAuxiliaryOperator A (Omega n) (crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p) = crouzeixPolynomialAuxiliaryOperator A (Omega n) p) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

Combining radial Plemelj convergence, the automatic constant case, and strict degree descent reduces every remaining companion input to positive degree.

theorem crouzeixPalencia_of_thickening_cauchy_support_normalized_boundaryPhase_radial_positiveDegree {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : ℕ → SmoothJordanDomain) (hcarrier : ∀ (n : ℕ), (Omega n).carrier = convexThickeningApprox (closure (numericalRange A)) n) (hCauchyP : ∀ (p : Polynomial ℂ) (n : ℕ), (Polynomial.aeval A) p = (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => Polynomial.eval z p • resolvent A z) (Omega n).boundaryParam) (hsupport : ∀ (n : ℕ), ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ∀ w ∈ numericalRange A, ((starRingEnd ℂ) (-Complex.I * deriv (Omega n).boundaryParam t) * (w - (Omega n).boundaryParam t)).re ≤ 0) (hkernel : ∀ (n : ℕ), ∀ z ∈ (Omega n).carrier, crouzeixScalarCauchyKernel (Omega n) z = 1) (hphaseNormalized : ∀ (n : ℕ) (p : Polynomial ℂ), 0 < p.natDegree → polynomialSupNorm p (frontier (Omega n).carrier) = 1 → CrouzeixBoundaryPhaseContractive (Omega n) p) (happrox : ∀ (p : Polynomial ℂ) (n : ℕ), 0 < p.natDegree → ∃ (r : ℕ → Polynomial ℂ), ∀ (j : ℕ), ∀ z ∈ compactThickeningApprox (closure (numericalRange A)) n, ‖Polynomial.eval z (r j) - crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p z‖ ≤ 1 / (↑j + 1)) (hPlemelj : ∀ (p : Polynomial ℂ) (n : ℕ), 0 < p.natDegree → crouzeixAuxiliaryOperator A (Omega n) (crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p) = crouzeixPolynomialAuxiliaryOperator A (Omega n) p) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

After automatic radial convergence and the constant case, every remaining phase, approximation, and contour-reproduction input is restricted to positive-degree polynomials; the phase input may moreover be normalized to frontier sup norm one.

theorem crouzeixPalencia_of_thickening_cauchy_support_normalized_boundaryPhase_radialZero {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : ℕ → SmoothJordanDomain) (hcarrier : ∀ (n : ℕ), (Omega n).carrier = convexThickeningApprox (closure (numericalRange A)) n) (hCauchyP : ∀ (p : Polynomial ℂ) (n : ℕ), (Polynomial.aeval A) p = (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => Polynomial.eval z p • resolvent A z) (Omega n).boundaryParam) (hsupport : ∀ (n : ℕ), ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ∀ w ∈ numericalRange A, ((starRingEnd ℂ) (-Complex.I * deriv (Omega n).boundaryParam t) * (w - (Omega n).boundaryParam t)).re ≤ 0) (hkernel : ∀ (n : ℕ), ∀ z ∈ (Omega n).carrier, crouzeixScalarCauchyKernel (Omega n) z = 1) (hphaseNormalized : ∀ (n : ℕ) (p : Polynomial ℂ), 0 < p.natDegree → polynomialSupNorm p (frontier (Omega n).carrier) = 1 → CrouzeixBoundaryPhaseContractive (Omega n) p) (happrox : ∀ (p : Polynomial ℂ) (n : ℕ), 0 < p.natDegree → Polynomial.eval 0 p = 0 → ∃ (r : ℕ → Polynomial ℂ), ∀ (j : ℕ), ∀ z ∈ compactThickeningApprox (closure (numericalRange A)) n, ‖Polynomial.eval z (r j) - crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p z‖ ≤ 1 / (↑j + 1)) (hPlemelj : ∀ (p : Polynomial ℂ) (n : ℕ), 0 < p.natDegree → Polynomial.eval 0 p = 0 → polynomialSupNorm p (frontier (Omega n).carrier) = 1 → crouzeixAuxiliaryOperator A (Omega n) (crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p) = crouzeixPolynomialAuxiliaryOperator A (Omega n) p) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

Constant-shift invariance reduces approximation to positive-degree polynomials vanishing at zero. Scaling invariance further restricts contour reproduction to that subclass at frontier sup norm one; the sharp phase input is likewise normalized to frontier sup norm one.

theorem crouzeix_palencia_of_convexThickening_cauchy_support_normalized_boundaryPhase_radial {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : ℕ → SmoothJordanDomain) (hcarrier : ∀ (n : ℕ), (Omega n).carrier = convexThickeningApprox (closure (numericalRange A)) n) (hCauchyP : ∀ (p : Polynomial ℂ) (n : ℕ), (Polynomial.aeval A) p = (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => Polynomial.eval z p • resolvent A z) (Omega n).boundaryParam) (hsupport : ∀ (n : ℕ), ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ∀ w ∈ numericalRange A, ((starRingEnd ℂ) (-Complex.I * deriv (Omega n).boundaryParam t) * (w - (Omega n).boundaryParam t)).re ≤ 0) (hkernel : ∀ (n : ℕ), ∀ z ∈ (Omega n).carrier, crouzeixScalarCauchyKernel (Omega n) z = 1) (hphaseNormalized : ∀ (n : ℕ) (p : Polynomial ℂ), 0 < p.natDegree → polynomialSupNorm p (frontier (Omega n).carrier) = 1 → CrouzeixBoundaryPhaseContractive (Omega n) p) (happrox : ∀ (p : Polynomial ℂ) (n : ℕ), ∃ (r : ℕ → Polynomial ℂ), ∀ (j : ℕ), ∀ z ∈ compactThickeningApprox (closure (numericalRange A)) n, ‖Polynomial.eval z (r j) - crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p z‖ ≤ 1 / (↑j + 1)) (hPlemelj : ∀ (p : Polynomial ℂ) (n : ℕ), crouzeixAuxiliaryOperator A (Omega n) (crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p) = crouzeixPolynomialAuxiliaryOperator A (Omega n) p) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

After automatic radial Plemelj convergence and scalar normalization, the L4.2 route needs the sharp phase theorem only for positive-degree frontier-sup-norm-one polynomials.