Issues

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

• [formalization] Ma–Wang endpoint multiplicity induction and affine interval classification

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

• Private imports: make proof-only imports non-public (shake), cut rebuild fan-out

  module-system
  PerAlexandersson/RealRooted#2086 · Filter by author PerAlexandersson opened on Oct 27, 2026
  2

• [theory] Ma–Wang/Liu–Wang hierarchy: special cases as corollaries, remove duplicate arguments

  theory
  PerAlexandersson/RealRooted#2072 · Filter by author PerAlexandersson opened on Oct 26, 2026
  4

• [theory] Formalize the Beraha–Kahane–Weiss limit-of-zeros theorem

  theory
  PerAlexandersson/RealRooted#2071 · Filter by author PerAlexandersson opened on Oct 26, 2026
  3

• [theory] Discrete mesh-preserving operators and OEIS consumers

  PerAlexandersson/RealRooted#2070 · Filter by author PerAlexandersson opened on Oct 26, 2026
  3

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

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

• [recognition] Hypergeometric row certificates via finite convolution

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

• [theory] Wang–Zhang affine two-step criterion and OEIS recognition

  PerAlexandersson/RealRooted#2067 · Filter by author PerAlexandersson opened on Oct 26, 2026
  2

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

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

• Prune the tactic layer: remove theorem-wrapper tactics, subsumed special tactics and routes

  tactic
  PerAlexandersson/RealRooted#2061 · Filter by author PerAlexandersson opened on Oct 26, 2026
  1

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

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

• [tactics] Shrink Applications/ row proofs with the row tactics (recurring probe)

  PerAlexandersson/RealRooted#2042 · Filter by author PerAlexandersson opened on Oct 25, 2026
  4

• Formalize weighted variable-delay interlacing and PF renewal recurrences

  PerAlexandersson/RealRooted#2037 · Filter by author PerAlexandersson opened on Oct 25, 2026
  5

• [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

• [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
  4