Quarantine the admitted Jensen-pencil backend and shrink PF-bidiagonal scaffolding

[PerAlexandersson]

Scope

Make the genuinely conjectural Jensen-pencil implication an explicit admitted theorem, clearly documented and isolated from the checked affine-symbol route. Collapse wrappers and smoke examples that only thread the same backend assumption.

The admitted theorem must remain visibly marked as unproved; it must not be reported as resolving the mathematical conjecture.

Acceptance

• one narrow sorry boundary for the conjecture;
• checked affine-symbol APIs require no admitted input;
• redundant aliases, wrapper matrices, and duplicated examples are removed;
• build warnings identify the admission clearly.

[PerAlexandersson]

Completed on main in commits bb78474 and 4ff4788. The Jensen-pencil implication is now a single explicit theorem with one sorry, documented as admitted; theorem-shaped backend parameters, forwarding macros, and the repeated smoke matrix were removed. The checked affine-symbol route remains the preferred endpoint, and the full external-cache build passes.

[PerAlexandersson]

Proof work resumed on 2026-08-12. The primary-source audit confirms that #355 was closed as a quarantine task, not as a proof: Garloff--Wagner Theorem 12(b) requires an already oriented proper-position relation, while the current one-sided Jensen pencil can have nested endpoints and supplies neither orientation. No Lean proof attempt was started from that stale outline. The smallest checked increment is now tracked in #370: prove the backend for d <= 1 via a direct positive-rescaling identity, retaining the full admission. Bounded exact screens found no full counterexample but are being treated only as evidence. Aristotle advisory project 30dc1740-493a-42eb-b507-a33bb1555e3d is reviewing the general mathematical implication.

[PerAlexandersson]

Concrete follow-up landed in 858e06a and child issue #370 is complete: the one-sided Jensen-pencil implication is now fully checked for d <= 1. The general admitted theorem is unchanged. The same patch corrects the stale Garloff--Wagner proof-route comment, records the low-degree endpoint in PROOF_STATUS.md, and passes the full 8,982-job build.

[PerAlexandersson]

Second checked follow-up landed in a5b5a2e and child issue #371 is complete: the Jensen-pencil implication now holds in degree two under beta 2 = 0. Together with 858e06a, the admitted theorem is checked for all d <= 1 and this degree-two boundary. The general admission is unchanged; the remaining d=2, beta 2 > 0 branch needs a genuinely new interlacing-transfer lemma.