[LGV 6b] Derive the Pólya-frequency endpoint from all ordered LGV certificates

[PerAlexandersson]

Parent: #617
Depends on: #624.

Scope

Consume the Toeplitz-minor bridge and existing RealRooted total-nonnegativity APIs.

Owned file

Create a separate RealRooted LGV PF endpoint file only.

Checked deliverables

• A theorem that ordered LGV certificates for every strict Toeplitz minor imply nonnegativity of every finite Toeplitz minor.
• The final checked implication to IsPolyaFreqSeq.

Acceptance

Keep all combinatorial cancellation inside LeanLGV and this file purely adaptational. No statement-only substitute, placeholder, or new axiom. The integration owner runs focused and full builds.