Prove the Jensen-pencil bidiagonal PF preserver backend

[PerAlexandersson]

Corrected target

Prove a sound Jensen-pencil criterion implying that bidiagonalOperator preserves PF polynomials, or correct the current jensenPencilBidiagonalPreserverStatement if its normalization is insufficient.

The proof must use the genuine affine Borcea--Branden algebraic symbol. It cannot pass through the old homogeneous FiniteSymbolPF.finiteSymbol implication: that implication has a checked d = 1 counterexample recorded in #239.

Required outline

1. Compute or invoke the exact affine symbol via finiteAlgebraicSymbol_bidiagonalLinearMap.
2. State the exact Jensen certificate, including binomial factors, signs, and truncation.
3. Prove that this certificate implies stability of the genuine affine symbol, or produce a counterexample and correct the certificate.
4. Invoke only a checked affine finite-symbol sufficiency theorem from Prove the finite-symbol and homogenization stability backends #239.
5. Derive PF/real-rootedness preservation formally from those results.

Acceptance criteria

• Add a checked theorem, not a def ...Statement : Prop, sorry, hidden axiom, or assumption of the desired preserver conclusion.
• Preserve the explicit jensen_backend in tactic/OEIS entry points until all normalization and finite-symbol dependencies above are checked.
• Remove that backend only when the proved theorem applies directly; retain an explicit experimental override only if useful.
• If a genuinely combinatorial model interpretation is supplied as an application hypothesis, place a nearby comment explaining why it is intentionally left unformalized. The stability and real-rootedness deductions must still be formal.
• Run focused and aggregate Lake builds and report the proof witness by name.

Depends on #239. Parent: #238.

[PerAlexandersson]

Tactic follow-up once this theorem lands: the Jensen PF tactics currently require callers to pass jensen_backend := .... A proof of jensenPencilBidiagonalPreserverStatement should become the internal default certificate, eliminating that strategy argument while retaining an explicit override only if useful for experimentation. I am not editing the tactic file now because another worker has an active refactor there.

[PerAlexandersson]

Aristotle task 197fbcc3-b110-43fc-a780-7261abda70d1 reached status COMPLETE, but its downloaded project snapshot leaves RealRooted/Tactic/PFBidiagonal.lean byte-identical to current main: jensenPencilBidiagonalPreserverStatement is still a def ... : Prop. The task event endpoint remains unavailable with HTTP 403, so this should be recorded as an unsuccessful/no-change proof attempt, not a solved theorem. Tactic frontends should continue requiring jensen_backend until a checked theorem lands.

[PerAlexandersson]

Paper-based proof outline (Borcea-Bränden, arXiv:0809.0401, Theorem 1.1): the relevant route is the forward finite-symbol implication, not a declaration-shape refactor. First compute the exact algebraic symbol T[(z+w)^κ] for bidiagonalOperator; then match the Jensen-pencil certificate to that symbol, including binomial coefficients, signs, and degree truncation; then prove symbol stability and invoke the finite-symbol sufficiency theorem. Until that normalization identity and the finite-symbol theorem are checked, jensen_backend must remain explicit. A theorem proved by sorry cannot become the tactic default.

[PerAlexandersson]

The general algebraic-symbol API and exact univariate compatibility bridge are now on main through 3aaf723. This gives a non-ad-hoc route for the Jensen backend normalization:

1. restrict bidiagonalOperator to degreeOfLE (Fin 1) ℝ d;
2. compute its MvPolynomial.algebraicSymbol;
3. use the checked univariate rename bridge to identify the ordinary finite symbol;
4. identify the tactic's homogenized finiteSymbol alpha beta d and its existing dehomogenization/Jensen pencil;
5. invoke finite-symbol sufficiency.

Steps 1-4 are algebraic; step 5 remains the deep input. Therefore jensen_backend should not yet be removed from tactics.

[PerAlexandersson]

The finite-symbol dependency has a concrete counterexample in its current tactic-symbol form.

For d=1, alpha=[1,0], beta=[2,1], the homogeneous tactic symbol is (X+Y)^2, but the operator sends the PF polynomial 1+2X to non-real-rooted 1+2X+2X^2 (discriminant -4). Therefore jensenPencilBidiagonalPreserverStatement cannot be discharged by composing the current finiteSymbolBBStatement; that statement is false.

The Jensen route must first establish a stronger certificate that implies stability of the genuine affine symbol w+2zw+z^2 in this example-sensitive normalization. Keep the Jensen backend explicit until that additional implication is proved.

[PerAlexandersson]

Counterexample audit for the current Jensen certificate: the checked d = 1 counterexample to the homogeneous tactic-symbol implication does not refute jensenPencilBidiagonalPreserverStatement.

For

alpha(0)=1, alpha(1)=0
beta(0)=2, beta(1)=1

we have

J_alpha,1 = 1
X * J_beta,1 = 2X + X^2
J_alpha,1 + lambda * X * J_beta,1 = 1 + 2 lambda X + lambda X^2.

The pencil discriminant is 4 lambda (lambda - 1), so the required BidiagonalJensenPencilCertificate fails for every 0 < lambda < 1. At lambda = 1/2, scaling by 2 gives 2 + 2X + X^2; polytool checked discriminant -4 and real_rooted=false exactly.

Consequences:

• The existing finite-symbol counterexample remains decisive against finiteSymbolBBStatement and any homogeneous-symbol proof of Prove the Jensen-pencil bidiagonal PF preserver backend #240.
• It is not a counterexample to the Jensen-pencil backend itself.
• The current Jensen statement therefore remains plausible, but its proof must use the proper-position/Schur--Szego route described in the source comment or prove a direct implication to the genuine affine algebraic symbol. jensen_backend must remain explicit until that transfer is checked.

This narrows the validity audit only; it does not prove #240.

[PerAlexandersson]

Primary-source audit for the direct Jensen route: paper-cache now has Garloff--Wagner, Hadamard Products of Stable Polynomials Are Stable (1996), paper id 88, DOI 10.1006/jmaa.1996.0348.

The relevant result is Theorem 12 on p. 805, not the headline Hurwitz theorem. For standard polynomials with only nonpositive zeros, define the factorial-weighted coefficient product

(f circ p)(x) = sum_j j! a_j b_j x^j.

Theorem 12 states, in particular:

1. if f circ p is nonzero, it again has only nonpositive zeros;
2. if g is in proper position with f, then g circ p is in proper position with f circ p.

This validates the source comment's Schur/Garloff--Wagner strategy in principle, but it does not yet prove jensenPencilBidiagonalPreserverStatement. The exact remaining outline is:

1. Convert the hypothesis that J_alpha,d + lambda * X * J_beta,d is PF for every lambda >= 0 into the correctly oriented proper-position relation between J_alpha,d and X * J_beta,d.
2. For an arbitrary PF input p of degree at most d, state and prove the exact factorial/binomial normalization identities that turn the two Theorem 12 compositions into diagonalOperator alpha p and X * diagonalOperator beta p. This step must track choose d k, k!, the shifted beta index, and zero padding.
3. Apply Theorem 12(b) to preserve proper position, then conclude that their sum bidiagonalOperator alpha beta p is PF.
4. Package the result as a checked theorem and only then internalize jensen_backend in the tactics.

The normalization in step 2 is the next algebraic target. Until it is checked, this paper theorem must not be cited as if it already matches the Lean operator. This direct route also avoids the refuted homogeneous finite-symbol implication; whether #240 should continue to require an affine-symbol detour can be reconsidered only after the normalization identity is explicit.

[PerAlexandersson]

Submitted a narrow Aristotle audit from current b3c2c13 for the shifted-beta Schur--Szegő normalization in jensenPencilBidiagonalPreserverStatement. Project/task: c4abf0b8-b757-4260-9e1f-93f9f7aa48e7 / 5bb2ba0c-708f-41db-a3ba-2ba66f50c50c.

The prompt forbids commits, tactic edits, sorry/axioms, and the refuted homogeneous finite-symbol route. It asks for exactly one of: a complete proof using the checked local Schur--Szegő API, a fully exact low-degree counterexample satisfying the whole Jensen certificate, or the exact missing shifted/binomial theorem signature. Status is QUEUED; no result is being treated as evidence.

[PerAlexandersson]

Source-proof correction after reading Garloff--Wagner, Theorem 12(b), p. 805:

The shifted beta branch should not be composed directly as X * J_beta. The paper-faithful route is:

1. obtain the oriented proper-position relation between J_alpha and X * J_beta from the full Jensen pencil certificate;
2. use Wagner's X-shift equivalence to convert it to a relation between J_beta and J_alpha;
3. apply the finite Schur--Szego proper-position transfer corresponding to Garloff--Wagner Theorem 12(b), with the same PF input;
4. use Wagner's X-shift in the forward direction on the composed pair;
5. identify both compositions with the diagonal operators and apply the checked PF addition consequence.

The repository already proves the factorial Theorem 12(b) as gwSchurProductPFAndPrec, but the exact finite Schur--Szego Prec0 wrapper is not currently exposed. That is the theorem-shaped intermediate target; it must be proved, not introduced as another def ...Statement : Prop.

Aristotle project c4abf0b8-b757-4260-9e1f-93f9f7aa48e7 has been continued with this exact route and the source passage. Tactics retain jensen_backend until the full chain is locally checked.

[PerAlexandersson]

Finite Schur--Szego worker result: the natural theorem target is

theorem schurSzegoComp_prec0
    {n : Nat} {f g p : R[X]}
    (hf : IsPFPolynomial f) (hg : IsPFPolynomial g)
    (hp : IsPFPolynomial p)
    (hfdeg : f.natDegree <= n) (hgdeg : g.natDegree <= n)
    (hpdeg : p.natDegree <= n) (hfg : Prec0 f g) :
    Prec0 (schurSzegoComp n f p) (schurSzegoComp n g p)

The checked finite-composition and Chudnovsky--Seymour APIs currently recover only the unoriented disjunction between this conclusion and its reverse. The exact remaining source step is the same-degree orientation preservation in Garloff--Wagner Theorem 12(b), including zero and degree-drop branches. No incomplete theorem or weaker substitute was added.

Aristotle task 33caa91b-2760-4f26-bb6e-ede3d0d07cf7 is still working on the full paper route. A separate read-only explorer, Newton (019fc011-af2a-79f1-ad9a-152470dead2a), is now restricted to locating/proving this orientation invariant from the existing reflect/root-order APIs.

[PerAlexandersson]

Corrected source audit: the proposed orientation step is false

The current BidiagonalJensenPencilCertificate does not imply either Prec0
orientation between J_{d,alpha} and X * J_{d,beta}.

An exact d = 2 witness is

alpha = (3, 2, 1)
beta  = (4, 1/2, 0)
J_{2,alpha}       = X^2 + 4X + 3 = (X+1)(X+3)
X * J_{2,beta}    = X^2 + 4X     = X(X+4)

For every lambda >= 0, the certified pencil is

3 + 4(1+lambda)X + (1+lambda)X^2,

whose discriminant is 4(1+lambda)(1+4lambda) >= 0; its coefficients are also
nonnegative. Nevertheless the roots occur in the nested order

-4 < -3 < -1 < 0,

so neither same-degree alternation orientation holds. Axle independently checked
the arithmetic/order calculation, and Aristotle produced the same obstruction.

This refutes the orientation inference, not the stated preserver conclusion: for
the same witness and a quadratic PF input p = a + bX + cX^2, the output is

3a + (2b+4a)X + (c+b/2)X^2,

with discriminant

4b^2 + 10ab + 16a^2 - 12ac >= b^2 + 10ab + 16a^2 >= 0

using b^2 >= 4ac. Thus this example's operator still preserves quadratic PF
polynomials.

What the source theorem actually gives

Garloff--Wagner Theorem 12(b) assumes an already oriented proper-position
relation and proves that their factorial Schur product preserves it. The checked
local counterpart is gwSchurProductPrec0. It does not derive an orientation
from one-sided compatibility of A + lambda B for lambda >= 0.

For P_{d,w}(X) = (1+wX)^d, direct expansion of the local definitions gives

bidiagonalOperator alpha beta (P_{d,w})
  = J_{d,alpha}(wX) + X * J_{d,beta}(wX).

The current certificate controls only

J_{d,alpha}(t) + lambda * t * J_{d,beta}(t),  lambda >= 0.

After t = wX, matching the exact affine symbol would require
lambda = 1/w, which is complex in the upper-half-plane symbol test. The
one-dimensional nonnegative pencil is therefore not the required bivariate
symbol condition.

Revised valid routes

Before further Lean implementation, the issue needs one of:

1. a stronger hypothesis asserting stability of the exact bivariate affine
   symbol, followed by finite-symbol sufficiency; or
2. a new source-backed common-interleaver transfer theorem tailored to the
   shifted bidiagonal action.

Ordinary Chudnovsky--Seymour compatibility and either Prec0 branch are
insufficient. Do not add a branch-selection lemma or tactic rule for the current
certificate.

[PerAlexandersson]

Read-only source audit confirms the latest correction and sharpens the boundary:

For the d = 2 witness alpha=(3,2,1), beta=(4,1/2,0), the current Jensen certificate holds, but the associated operator sends the real-rooted polynomial (1-2X)^2 = 1-4X+4X^2 to 3-4X+2X^2, discriminant -8. Hence the current certificate cannot imply stability of the genuine affine Borcea–Brändén symbol; that bridge would imply preservation of all real-stable inputs and is false.

This does not refute the desired PF-preserver conclusion: (1-2X)^2 is not PF (negative coefficient and positive root). Thus #240 should remain open only for a different source-backed PF-specific transfer, such as the revised common-interleaver route, or for a strengthened exact affine-symbol hypothesis. Garloff–Wagner Theorem 12(b) cannot choose an orientation from the one-sided pencil certificate.

No theorem or tactic change was made. jensen_backend must remain explicit, and no jensenCertificate_affineSymbol_stable lemma should be introduced.