Issues

• [formalization] PF-factor numerators via TN augmentation (extends Brändén–Leite and delayed PF renewals)

  formalization
  PerAlexandersson/RealRooted#2160 · Filter by author PerAlexandersson opened on Oct 29, 2026
  1

• [theory] Beraha–Kahane–Weiss with three or more dominant bases (Sokal Thm 1.5(b), general case)

  foundationtheory
  PerAlexandersson/RealRooted#2158 · Filter by author PerAlexandersson opened on Oct 29, 2026

• [theory] Balanced five-diagonal Toeplitz real-limit theorem via Schur signs

  PerAlexandersson/RealRooted#2157 · Filter by author PerAlexandersson opened on Oct 29, 2026
  1

• [theory] Exact finite-degree Tran curve localization via the fixed-lag recurrence

  theory
  PerAlexandersson/RealRooted#2153 · Filter by author PerAlexandersson opened on Oct 28, 2026
  1

• [formalization] Exact coupling thresholds for first-order differential recurrences, including zero parameters

  formalization
  PerAlexandersson/RealRooted#2150 · Filter by author PerAlexandersson opened on Oct 28, 2026
  1

• [theory] Explicit finite-prefix real-rootedness certificate for Hessenberg Toeplitz recurrences

  theory
  PerAlexandersson/RealRooted#2147 · Filter by author PerAlexandersson opened on Oct 28, 2026
  2

• [tactic] Replay PF transform certificates and recognize transformed row families

  tactic
  PerAlexandersson/RealRooted#2140 · Filter by author PerAlexandersson opened on Oct 28, 2026
  1

• [theory] Stirling root regions and grouped cubic factors for OEIS proofs

  theory
  PerAlexandersson/RealRooted#2134 · Filter by author PerAlexandersson opened on Oct 28, 2026
  1

• [formalization] Recognize Veronese sections from recurrences and reconstruct scalar parents

  formalization
  PerAlexandersson/RealRooted#2116 · Filter by author PerAlexandersson opened on Oct 28, 2026
  1

• [formalization] Limiting root measures, full support, and edge densities for quadratic differential orbits

  formalization
  PerAlexandersson/RealRooted#2114 · Filter by author PerAlexandersson opened on Oct 27, 2026

• [formalization] Newton-sum obstructions and eventual nonreal zeros of quadratic differential orbits

  formalization
  PerAlexandersson/RealRooted#2110 · Filter by author PerAlexandersson opened on Oct 27, 2026
  1

• [formalization] Common-interlacer quadratic PF preservers and strict constant-start orbits

  formalization
  PerAlexandersson/RealRooted#2108 · Filter by author PerAlexandersson opened on Oct 27, 2026
  1

• [formalization] Direct coefficient criterion for four-term nonnegative bidiagonal factorization

  formalization
  PerAlexandersson/RealRooted#2102 · Filter by author PerAlexandersson opened on Oct 27, 2026
  2

• [research] A275442: find a stronger bridge invariant; five-state interlacing closure fails

  open-problem
  PerAlexandersson/RealRooted#2096 · Filter by author PerAlexandersson opened on Oct 27, 2026

• [formalization] Effective finite-prefix classification and full-height region for weighted A304429

  formalization
  PerAlexandersson/RealRooted#2094 · Filter by author PerAlexandersson opened on Oct 27, 2026

• [formalization] Full weighted A304429 strip via cubic characteristic-root amplitudes

  formalization
  PerAlexandersson/RealRooted#2089 · Filter by author PerAlexandersson opened on Oct 27, 2026
  2

• [formalization] Weighted A304429 family via a three-state interlacing matrix

  formalization
  PerAlexandersson/RealRooted#2088 · Filter by author PerAlexandersson opened on Oct 27, 2026
  4

• [theory] Fixed Laguerre combinations from an auxiliary root test

  theory
  PerAlexandersson/RealRooted#2069 · Filter by author PerAlexandersson opened on Oct 26, 2026
  1

• [recognition] Hypergeometric row certificates via finite convolution

  tactic
  PerAlexandersson/RealRooted#2068 · Filter by author PerAlexandersson opened on Oct 26, 2026
  5

• [research] Shorter structural proof for A268434 and Lah polynomials of order s

  open-problem
  PerAlexandersson/RealRooted#2065 · Filter by author PerAlexandersson opened on Oct 26, 2026

• Make the row tactics transparent, fast to fail, and simpler

  tactic
  PerAlexandersson/RealRooted#2057 · Filter by author PerAlexandersson opened on Oct 26, 2026
  4

• [tactic] Row-reader gaps found while shortening CombinatorialExamples proofs

  tactic
  PerAlexandersson/RealRooted#2030 · Filter by author PerAlexandersson opened on Oct 25, 2026
  1

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

  weyl-program
  PerAlexandersson/RealRooted#2018 · Filter by author PerAlexandersson opened on Oct 25, 2026
  1

• [theory] Liu–Zhang Theorems 5.6–5.8: Morris constant term equals the stable eigenfunction

  theory
  PerAlexandersson/RealRooted#2017 · Filter by author PerAlexandersson opened on Oct 25, 2026

• [module-system] Migrate RealRooted to the Lean module system

  module-system
  PerAlexandersson/RealRooted#2016 · Filter by author PerAlexandersson opened on Oct 25, 2026
  5