Retire the false homogeneous finiteSymbolBBStatement interface

[PerAlexandersson]

Priority

Erik priority 1. Parent roadmap: #238. Source-proof route: #297. Jensen application: #240.

Problem

finiteSymbolBBStatement is a legacy proposition scaffold for the homogeneous tactic symbol, not the affine algebraic-symbol theorem of Borcea--Branden.

It is formally unsuitable and mathematically false. For d = 1, alpha = [1, 0], and beta = [2, 1], the homogeneous symbol is (X + Y)^2, while the operator sends 1 + 2X to 1 + 2X + 2X^2, whose discriminant is negative.

The source-faithful real theorem uses the affine symbol T((z + w)^d); see Borcea--Branden I, arXiv:0809.0401, equations (1.1)--(1.2) and Theorem 1.2(b). The complex counterpart is Theorem 1.1(b). The degree-d source-box extension is tracked by #297.

Goal

Retire the false homogeneous interface and migrate every live caller to either the genuine affine-symbol theorem or an explicit still-open backend.

Acceptance criteria

• Do not prove or assume finiteSymbolBBStatement.
• Remove it, rename it as legacy/false scaffolding, or replace it by a checked negation theorem with the explicit d = 1 counterexample.
• Audit every caller of finiteSymbolBBStatement.
• Migrate applicable callers to the affine-symbol route from Extend affine finite-symbol sufficiency to degree-d source boxes #297.
• Keep unmatched tactic backends explicit rather than hiding the gap.
• Preserve a nearby source comment explaining the homogeneous/affine mismatch.

[PerAlexandersson]

Primary-source audit confirms the issue diagnosis and sharpens the replacement.

For T(X^k) = alpha_k X^k + beta_k X^(k+1), Borcea--Branden's degree-d algebraic symbol is

sum_{k=0}^d choose(d,k) * (alpha_k X^k + beta_k X^(k+1)) * Y^(d-k).

The current tactic symbol inserts an extra Y only in the alpha branch, making a homogeneous bivariate polynomial that is not T((X+Y)^d). Genuine homogenization would require a third variable and a separate stability theorem.

finiteSymbolTheoremStatement in Challenges/BorceaBranden.lean does use the correct algebraic symbol and is a valid sufficient branch of Borcea--Branden I, Theorem 1.2(b). It is not the complete real classification, which also has the rank-at-most-two proper-position branch, the G_T(X,-Y) branch, and the reverse implication.

The PF specialization should therefore be derived in two stages: apply the genuine nonhomogeneous algebraic-symbol theorem for splitting/zero, then use coefficient nonnegativity (needed only for k <= d) to obtain the PF conclusion.