[weyl-program] Roadmap: themes, entry points and subsumptions #2018

Roadmap for the weyl-program formalization issues (umbrella #601; router #1873). It organizes them only and makes no mathematical claims. Each theme lists its suggested in-theme order, where the issues in one layer are mutually independent; ★ marks the smallest self-contained entry points. Hubs used across themes: #1781 (cited by 47 issues), #1763, #1872, #1936.

Generated 2026-10-25 from the issue texts and a name grep of main (8072d82). The dependencies are the ones the issues state; a few are inferred and flagged.

T1. Bounded operator matrices and first-order weighted Weyl blocks (17)

Degree-capped operator-matrix local-to-global, composition, the three common-input tests (#1781), and exact criteria for nonnegative first-order blocks: weighted polar-Euler, affine-derivative, linear-multiplier, reciprocal conjugation, common right factors.

Entry points: #1761 ★, #1774 ★, #1781 ★

Order: #1759,#1761,#1763,#1774,#1779,#1781,#1865 → #1760,#1764,#1765,#1766,#1775 → #1767 → #1768,#1769,#1780,#1867

T2. Finite-alphabet {D,I,theta,X} atlases and weighted shifted-derivative matrices (20)

Unit-weight classification of 2x2 blocks over {D,I,theta,X,0} (14/24/113 tables), weighted D/I/theta atlases with row-symbol, Rayleigh, determinant and zero-face dispatchers, and the shifted-derivative (theta+nu X+a)(D+nu) weight matrices.

Entry points: #1776 ★, #1782 ★

Order: #1776,#1782 → #1777,#1783,#1896 → #1778,#1784,#1897 → #1842,#1898,#1902,#1985 → #1899,#1903 → #1900,#1904 → #1901 → #1927 → #1906,#1907

T3. Derivative lifts and PF-symbol factor theory (18)

Polynomial derivative-lift comparisons (A D + P, Q), their transfer through right factors (quadratic tests, shifted derivatives, PF-symbol factors), factor-deletion state lifts, root-turn/root-jet criteria for quadratic PF symbols, and certified-column / TN-sandwich matrix lifts.

Entry points: #1908 ★

Order: #1908 → #1910 → #1911 → #1912 → #1914 → #1915 → #1917,#1920 → #1918,#1921 → #1922,#1939 → #1923,#1924 → #1925 → #1926 → #1940 → #1941

T4. Aligned affine Weyl defect blocks and Euler shift ceilings (17)

Factored signed-lag / controlled-defect blocks [[L,I],[cT.L,T]], triangular affine alignment, rank-one weight boundary, slope alignment, the aligned Euler/affine shift ceilings, and the complete structured weighted affine defect classification.

Entry points: #1785 ★

Order: #1785 → #1786 → #1787 → #1788 → #1789 → #1790 → #1791 → #1792 → #1794,#1795 → #1796 → #1797 → #1798,#1799 → #1801 → #1800 → #1808

T5. Lag-recurrence certificates: affine and mixed-affine lags, root-sign, root-flux, ratio cones (22)

Turning block classifications into recurrence certificates and recognizers: nonautonomous affine defect lags, aligned-factor recognition, orientation/Riccati paths, mixed-affine common-factor recurrences, root-sign band-one/tight-cap/cubic-current steps, forced root-flux budgets, and projective ratio cones for affine lags.

Entry points: #1772 ★, #1849 ★

Order: #1772,#1802,#1804,#1810,#1849,#1879 → #1805,#1806,#1811,#1812,#1848,#1850,#1881,#1961 → #1807,#1813,#1851,#1882,#1962 → #1814,#1852,#1963

T6. Scalar off-diagonal lifts, zero-upper-left blocks, scalar PF successors, projective transfer (16)

Realizing two-step recurrences as 2x2 Weyl blocks with scalar upper-right entry; origin-filtration and differential-order barriers; zero-upper-left (positive-X lag) block classification; classification of all (finite-cap) first-order Weyl PF successors; A157 boundary-cone transfers; Bernstein/Cayley projective interval transfer.

Entry points: #1818 ★

Order: #1809,#1815,#1818,#1835 → #1816,#1819,#1822,#1836 → #1820,#1823 → #1821,#1824 → #1825,#1826 → #1827 → #1828

T7. Decorated and factored companions, moving Euler lags, right-factor lifts and decorator paths (25)

Constrained-state templates for lag recurrences: derivative-X^2 and composed-successor cones, moving-Euler-shift companions, exact classification of decorated companions [[0,B],[K,E]] (polynomial, derivative, shifted-derivative, affine-Euler tops), right-factor recognition and semiconjugacy, decorator-path search and periodic lassos.

Entry points: #1829 ★, #1834 ★

Order: #1829,#1834,#1857 → #1830,#1837,#1858,#1883,#1884 → #1831,#1832,#1838,#1885 → #1839,#1859,#1886 → #1840,#1887 → #1841,#1888 → #1890 → #1891 → #1892 → #1893 → #1894 → #1895

T8. Quadratic Euler, finite-turn Euler thresholds and PF exponential symbols (12)

Second-order Euler-type operators theta^2+(c-1)theta+X+a and affine-raising generalizations: scalar sharp thresholds, independent-shift rows/matrices, ray-local and finite-turn Euler preservers, varying-c rows, parabolic-boundary obstruction, PF exponential symbols, valuation-shifted symbols.

Entry points: #1770 ★, #1860 ★

Order: #1770,#1860 → #1771,#1861,#1862 → #1863,#1866 → #1871 → #1929 → #1930 → #1931 → #1932

T9. Finite Weyl normal forms, block symbols, constant-coefficient and homogeneous-face classification (20)

Degree-shift normal form and cap recognizer; finite complex-stability symbol bridge, companion rigidity, Mobius-slice criterion; Euler-diagonal blocks; pure-D stable kernel, Branden cap-one multiplier criterion, Weyl star products, asymptotic shadows, dilation faces, homogeneous degree boards, pivot-image blocks, bounded symbol cores.

Entry points: #1853 ★, #1854 ★, #1944 ★

Order: #1853,#1854,#1944 → #1855,#1856,#1942 → #1933,#1943 → #1934,#1945 → #1935,#1946 → #1947 → #1948 → #1949 → #1950 → #1951,#1958 → #1952,#1986

T10. Root-prism / Bezout compilers and uniform-rank certificates (10)

Root-simplex Bezout compiler for Euler successors, Bernstein-Polya positivity certificates, exact quadratic Jensen caps, fixed-cap/unequal-cap/rectangular root-prism compilers, 2d+1 root-cluster compression, uniform-rank and clustered-multiplicity certificates, finite Gram LMI backend.

Entry points: #1937 ★, #1991 ★

Order: #1936,#1991 → #1937,#1938 → #1953 → #1954 → #1955 → #1957 → #1959 → #1960

T11. Normalized parent cones, spectral companions, centered lifts and Bell reachable states (18)

Normalized-difference compiler, PF-Gram transport, arrowhead/trace-resolvent lifts, rank-one parent states, affine/lag-Euler/pure-derivative spectral companions (merged in #1972), finite-cap normalized companions and Ferrers cones, centered lag packets, newest-atom and retained-window slack for threshold-Bell, Euler-jet lifts.

Entry points: #1964 ★, #1990 ★

Order: #1964,#1990 → #1965 → #1966 → #1967 → → → → #1972 → #1973 → #1974 → #1975 → #1976 → #1977 → #1979 → #1981 → #1982,#1983 → #1984 → #1987 → #1989

T12. Canonical companion states, recurrence spaces and OEIS consumers (6)

Reachable-orbit state-space layer for linear derivative recurrences (formal kernel for the #1873 router), recurrence-space certificates (#1978), and concrete consumers: A059022/3 half-step windows, A395497 Euler-completion lift, A087727/A318107 production matrices, A157012 capacity matrices.

Entry points: #1872 ★, #1877 ★

Order: #1872,#1877,#1978 → #1875,#1876,#1878

Subsumptions stated in the issues

When working an issue, check here first. Each line is "general ⊇ special" as the general issue itself states. A special case can be closed once its general issue lands with the specialization recovered.

• [formalization] Classify complete affine first-order spectral companions #1972 ⊇ [formalization] Classify affine Weyl companions on normalized parent cones #1968, [formalization] Prove lag-Euler rigidity for normalized Weyl companions #1969, [formalization] Classify pure derivatives in normalized Weyl companions #1970 (closed as merged); [formalization] Classify finite-cap normalized companions modulo constant gauge #1973 generalizes [formalization] Classify complete affine first-order spectral companions #1972.
• [formalization] Classify right divisibility of first-order Weyl operators #1892 ⊇ [formalization] Recognize affine-Euler right factors of first-order Weyl lags #1890 · [formalization] Classify polynomial derivative lifts #1908 ⊇ [formalization] Classify derivative-only adjacent Weyl comparisons #1907 (keep [formalization] Classify derivative-only adjacent Weyl comparisons #1907 while [formalization] Dispatch zero faces of nonnegative D/I/theta blocks #1906 calls it) · [formalization] Transfer derivative lifts through PF-symbol factors #1912 ⊇ [formalization] Transfer derivative lifts through quadratic-test right factors #1910, [formalization] Transfer derivative lifts through shifted derivatives #1911 · [formalization] Compile derivative-polar 2x2 blocks by polarized symbols #1985 ⊇ [formalization] Finite Rayleigh cone for weighted {D,I,theta} 2x2 symbols #1897
• [formalization] Classify quadratic Euler matrices with independent raising parameters #1866 ⊇ [formalization] Sharp affine-raising quadratic Euler operators and matrices #1861 ⊇ [formalization] Sharp quadratic Euler PF threshold and common-shift matrices #1770, [formalization] Independent-shift quadratic Euler rows and Weyl matrices #1771 · [formalization] Finite-turn Euler preservers and the degree-rise band #1863 ⊇ [formalization] One-turning-point Euler preservers and shifted-row certificate #1862 and part of [formalization] Ray-local Euler-type second-order PF and interlacing theorem #1860
• [formalization] All admissible shifts for aligned affine Weyl defect blocks #1801 ⊇ [formalization] Exact all-degree aligned affine Weyl defect criterion #1799 · [formalization] All-degree aligned affine Weyl shift ceiling #1796 ⊇ [formalization] All-degree aligned Euler shift ceiling #1794 ⊇ [formalization] Quantitative aligned Euler shift obstruction #1792 · [formalization] Four-branch degree-gap Weyl companion classification #1851 ⊇ [formalization] Exact tight-cap Weyl companion cone and A14443x recurrences #1850 · [formalization] Composed-successor cones for factored Weyl lag recurrences #1830, [formalization] Real Euler-shift preserver and weighted derivative-lag invariant #1837 ⊇ [formalization] Decorated derivative-X² lag invariant for two-step recurrences #1829
• [formalization] Classify polynomial-multiplier decorated Weyl companions #1884 ⊇ the all-degree part of [formalization] Endpoint-monomial deflation for decorated Weyl companions #1883 · [formalization] Expose Brändén cap-one multiplier criterion and sparse Wronskian classifiers #1944 ⊇ [formalization] Sharp nonnegative linear-multiplier 2x2 matrix criterion #1779 · [formalization] Forest scaling and weighted zero-aware {D,I,theta} atlas #1901 ⊇ [formalization] Complete positive-weight {D,I,theta} support atlas #1900 · [formalization] Scalar off-diagonal Weyl realization of two-step recurrences #1818 recovers the algebraic lift of [formalization] Factored signed-lag recurrences via ordered auxiliary Weyl states #1785
• Inferred, check first: [formalization] Classify all first-order Weyl PF successors and zero-upper-left blocks #1823/[formalization] Every finite-cap Weyl PF successor is weighted polar-Euler #1826 ⊇ [formalization] No positive D term in unrestricted affine PF successors #1809; [formalization] Classify all-degree constant-coefficient 2x2 blocks by one stable kernel #1942 ⊇ [formalization] Affine-derivative row and column criteria with directed anchor #1774, [formalization] Complete nonnegative affine-derivative 2x2 matrix criterion #1775 (same PF-pair convention?); [formalization] Sharp weighted polar-Euler PF pencil and three OEIS consumers #1759, [formalization] Derivative-polar Weyl operator preserves ordered PF pairs iff quadratic condition #1760 and [formalization] Classify affine first-order Weyl preservers and factor A241171 #1865 share one scalar/pair core.

Partly on main (name grep of 8072d82)

• [formalization] Certified recurrence spaces and lag–derivative trade-offs #1978: phases A and B merged (Recurrence spaces, phase A: shift operators, filtered finite check, defect identity (#1978) #1997, Recurrence spaces, phase B: certificate replay, exceptional indices, row-tactic adapter (#1978) #1998); phase C open.
• [formalization] Replace A298668 proof by alternating decorator paths #1894: done A298668-locally by Formalize the A298668 Weyl matrix orbit and transition graph #2001 (OperatorMatrix/EulerDerivativeLag.lean); the generic [formalization] Search compatible paths of right-factor decorators #1893/[formalization] Certified lassos for ultimately periodic recurrence-state graphs #1895 route and the downstream replacement remain.
• [formalization] Compose degree-bounded Weyl matrices and derive factored second-order preservers #1765: only unrestricted composition exists (PreservesOrderedPF.mul, .pow); the degree-bounded version is missing.
• [formalization] Canonical Weyl companion states and reachable orbit certificates #1872, [formalization] Exact endpoints for band-one Weyl lag recurrences #1849, [formalization] Classify right divisibility of first-order Weyl operators #1892: small overlaps only. Ingredients exist for [formalization] Sharp weighted polar-Euler PF pencil and three OEIS consumers #1759/[formalization] Derivative-polar Weyl operator preserves ordered PF pairs iff quadratic condition #1760/[formalization] Sharp row and column criteria for nonnegative first-order Weyl operators #1766/[formalization] Every finite-cap Weyl PF successor is weighted polar-Euler #1826 (polar Euler API), [formalization] Ray-local Euler-type second-order PF and interlacing theorem #1860/[formalization] Sharp affine-raising quadratic Euler operators and matrices #1861/[formalization] Sharp quadratic Euler PF threshold and common-shift matrices #1770 (EulerBidiagonal.generalStep), [formalization] Classify finite Euler-diagonal 2x2 block symbols #1933/[formalization] Classify PF-only finite Euler-diagonal blocks #1934/[formalization] Add exact quadratic Jensen caps and no-cutoff regressions #1938 (Jensen / Pólya–Schur), [formalization] Alternating Euler-completion lift and A395497 migration #1876, [formalization] Expose Brändén cap-one multiplier criterion and sparse Wronskian classifiers #1944.

🤖 Generated with Claude Code