Skip to content

Formalize the A262704 determinant model - #419

Merged
PerAlexandersson merged 8 commits into
mainfrom
proof/a262704-close
Aug 23, 2026
Merged

Formalize the A262704 determinant model#419
PerAlexandersson merged 8 commits into
mainfrom
proof/a262704-close

Conversation

@PerAlexandersson

Copy link
Copy Markdown
Owner

Adds the axiom-clean RealRooted support for A262704: the normalized determinant recurrence and PF certificate, coefficient identification, and a reusable positive X-lag helper used by the consecutive interlacing proof.

Verification:

  • lake-workspace build RealRooted.Tactic.WagnerX
  • lake-workspace build (9022 jobs, successful)

LGV and NonNestingRooks are intentionally out of scope.

@PerAlexandersson
PerAlexandersson merged commit 439e8cb into main Aug 23, 2026
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant