[LGV 6a] Identify ordered path matrices with oriented Toeplitz minors

[PerAlexandersson]

Parent: #617
Depends on: #613 and #623.

Scope

Build the thin matrix-orientation bridge in RealRooted after LeanLGV is published and pinned.

Owned file

Create a new RealRooted LGV Toeplitz adapter file; do not edit LeanLGV sources.

Checked deliverables

• Explicit source-row and sink-column index maps for a strict Toeplitz minor.
• Equality between the reindexed path matrix and the intended Toeplitz submatrix.
• A determinant equality with orientation fixed by theorem, not convention.

Acceptance

No PF conclusion yet, no NonNestingRooks import, placeholder, or new axiom. The integration owner runs focused and full builds.

[PerAlexandersson]

Dependency status: the standalone LeanLGV proof chain is complete locally through LGV.Resource.Ordered at clean LeanLGV/main 2972793 (umbrella/full builds: 1,417 jobs). This issue remains intentionally blocked on publication/pinning task #612; RealRooted currently has no LeanLGV dependency, so no relative local dependency or unpublished adapter has been introduced.