Skip to content

Define source-faithful Hoster-Stump interlacing sequences - #331

Open
PerAlexandersson wants to merge 1 commit into
mainfrom
codex-hs326
Open

Define source-faithful Hoster-Stump interlacing sequences#331
PerAlexandersson wants to merge 1 commit into
mainfrom
codex-hs326

Conversation

@PerAlexandersson

Copy link
Copy Markdown
Owner

Summary

  • define the Section 2 zero/nonzero-splitting convention and source-specific pair relation
  • include the degree-at-most-one exception omitted by local Prec
  • define a nonnegative, elementwise-real-rooted, pairwise source interlacing sequence
  • preserve all four exact Lemma 2.3 list formulas and document the printed part (4) endpoint typo
  • prove checked counterexamples for all four false weak IsInterlacingSeq0Nonneg closure interfaces

Validation

RealRooted.HosterStumpInterlacing built successfully from current origin/main (8568/8568 jobs).

Fixes #326.

@PerAlexandersson

Copy link
Copy Markdown
Owner Author

Follow-up source audit: the source-exact predicate in this PR is faithful, but Hoster--Stump Lemma 2.3(2) is false under the paper's unconditional degree-at-most-one convention. Stacked PR #332 adds an exact checked counterexample and documents why issue #316 needs a stronger pairwise Prec0 hypothesis. No definition in #331 is changed by the stacked commit.

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.

Define the source-faithful Hoster--Stump interlacing-sequence predicate

1 participant