[LGV application] Repeated-chip tiling kernel PF certificate

[PerAlexandersson]

Parents: #416, #668
Depends on: #612, #624, #625

Goal

Use the finalized standalone LeanLGV package to prove the repeated-chip tiling
kernel certificate from the note as a concrete RealRooted consumer.

For finite products G,K of nonnegative lower-bidiagonal chip matrices, with
K strictly lower triangular, prove that

a_k = (G * (K * G)^k)[N,0]

extended by zero is a Pólya-frequency sequence, hence its row polynomial is
IsPFPolynomial.

Route

• encode the repeated word G,K,G,K,… as a finite ranked network for each
  requested Toeplitz minor;
• prove the path matrix is the correctly oriented transpose of the Toeplitz
  submatrix using [LGV 6a] Identify ordered path matrices with oriented Toeplitz minors #624;
• use the published ordered/resource-disjoint LGV determinant endpoint and
  [LGV 6b] Derive the Pólya-frequency endpoint from all ordered LGV certificates #625 for nonnegativity/PF;
• prove strict-lower support gives a_k=0 for k>N (and the sharper r bound).

This issue is an application landmark, not a second implementation of LGV.
The sign-reversing tail swap and ordered-boundary theorem remain owned by the
standalone LeanLGV repository.

Boundaries

No interlacing claim for general repeated-chip rows, no new generic planar-graph
framework, and no dependency pin change before #612 publishes LeanLGV.

Acceptance

One end-to-end repeated-chip PF theorem and a small rod-tiling regression are
checked. Focused/full builds, guards, and axiom audits pass.