Issues

• [formalization] Compile finite-Weyl lag packets by a centered lift

  PerAlexandersson/RealRooted#1979 · Filter by author PerAlexandersson opened on Oct 20, 2026
  1

• [formalization] Certified recurrence spaces and lag–derivative trade-offs

  PerAlexandersson/RealRooted#1978 · Filter by author PerAlexandersson opened on Oct 20, 2026

• [formalization] Collapse universal adjacent-chain companions to the last pair

  PerAlexandersson/RealRooted#1977 · Filter by author PerAlexandersson opened on Oct 20, 2026
  2

• [formalization] Classify normalized higher companions by a Ferrers cone

  PerAlexandersson/RealRooted#1976 · Filter by author PerAlexandersson opened on Oct 20, 2026
  2

• [formalization] Classify constant-top normalized blocks by companion dilation

  PerAlexandersson/RealRooted#1975 · Filter by author PerAlexandersson opened on Oct 20, 2026
  2

• [formalization] Reduce fixed-anchor full blocks to synchronized simplex edges

  PerAlexandersson/RealRooted#1974 · Filter by author PerAlexandersson opened on Oct 20, 2026
  1

• [formalization] Classify finite-cap normalized companions modulo constant gauge

  PerAlexandersson/RealRooted#1973 · Filter by author PerAlexandersson opened on Oct 20, 2026
  4

• [formalization] Classify complete affine first-order spectral companions

  PerAlexandersson/RealRooted#1972 · Filter by author PerAlexandersson opened on Oct 20, 2026
  2

• [formalization] Classify pure derivatives in normalized Weyl companions

  PerAlexandersson/RealRooted#1970 · Filter by author PerAlexandersson opened on Oct 20, 2026
  2

• [formalization] Prove lag-Euler rigidity for normalized Weyl companions

  PerAlexandersson/RealRooted#1969 · Filter by author PerAlexandersson opened on Oct 20, 2026
  3

• [formalization] Classify affine Weyl companions on normalized parent cones

  PerAlexandersson/RealRooted#1968 · Filter by author PerAlexandersson opened on Oct 20, 2026
  6

• [formalization] Propagate normalized recurrences by rank-one parent states

  PerAlexandersson/RealRooted#1967 · Filter by author PerAlexandersson opened on Oct 20, 2026
  2

• [formalization] Lift normalized Weyl edges to symmetric arrowhead matrix states

  PerAlexandersson/RealRooted#1966 · Filter by author PerAlexandersson opened on Oct 20, 2026
  2

• [formalization] Transport PF-Gram certificates through common Weyl operators

  PerAlexandersson/RealRooted#1965 · Filter by author PerAlexandersson opened on Oct 20, 2026
  1

• [formalization] Compile normalized Weyl output pairs by determinant differences

  PerAlexandersson/RealRooted#1964 · Filter by author PerAlexandersson opened on Oct 20, 2026
  6

• [formalization] Compile affine root-weighted jets with anchored Bezout pencils

  PerAlexandersson/RealRooted#1963 · Filter by author PerAlexandersson opened on Oct 20, 2026
  1

• [formalization] Certify affine lag packets by projective polytopes and endpoint jets

  PerAlexandersson/RealRooted#1962 · Filter by author PerAlexandersson opened on Oct 20, 2026
  2

• [formalization] Close positive affine lags by projective ratio cones

  PerAlexandersson/RealRooted#1961 · Filter by author PerAlexandersson opened on Oct 20, 2026
  2

• [formalization] Decide strict asymptotic chambers of clustered Weyl recurrences

  PerAlexandersson/RealRooted#1960 · Filter by author PerAlexandersson opened on Oct 20, 2026
  1

• [formalization] Certify clustered Weyl multiplicities at every rank

  PerAlexandersson/RealRooted#1959 · Filter by author PerAlexandersson opened on Oct 20, 2026
  2

• [formalization] Bound uniform Weyl symbols and classify affine diagonal cores

  PerAlexandersson/RealRooted#1958 · Filter by author PerAlexandersson opened on Oct 20, 2026
  1

• [formalization] Compress bounded-order Weyl tests to 2d+1 root clusters

  PerAlexandersson/RealRooted#1957 · Filter by author PerAlexandersson opened on Oct 20, 2026
  3

• [formalization] Lift finite Weyl residuals to uniform rank certificates

  PerAlexandersson/RealRooted#1955 · Filter by author PerAlexandersson opened on Oct 20, 2026
  5

• [formalization] Compile unequal-cap and rectangular Weyl matrices on root prisms

  PerAlexandersson/RealRooted#1954 · Filter by author PerAlexandersson opened on Oct 20, 2026
  5

• [formalization] Compile arbitrary fixed-cap Weyl blocks on two root prisms

  PerAlexandersson/RealRooted#1953 · Filter by author PerAlexandersson opened on Oct 20, 2026
  5