Skip to content

Add Karlin sign-block aggregation foundations - #291

Open
PerAlexandersson wants to merge 5 commits into
mainfrom
codex-karlin-v12
Open

Add Karlin sign-block aggregation foundations#291
PerAlexandersson wants to merge 5 commits into
mainfrom
codex-karlin-v12

Conversation

@PerAlexandersson

Copy link
Copy Markdown
Owner

Source route

This is the first implementation layer for Karlin, Total Positivity, Vol. I, Chapter V, Section 1, Theorem 1.2, tracked in #290.

It adds:

  • a fully proved consecutive sign-block decomposition for every nonzero finite real vector, with block count Fin.signVariations x + 1, monotone block assignment, a nonzero witness in every block, constant nonzero sign within blocks, and alternating adjacent block signs;
  • Matrix.IsTotallyNonnegRect.aggregate_monotone, proved by determinant multilinearity over block fibers, monotonicity of chosen source columns, source total nonnegativity, and nonnegative weight products.

No axioms, sorry, or def ...Statement : Prop wrappers are introduced.

This PR is intentionally stacked on #289. The final V.1.2 strict-positive witness step and application of the V.1.1 theorem are not claimed here.

@PerAlexandersson
PerAlexandersson changed the base branch from codex-karlin-strict-maximal to main August 2, 2026 14:09
@PerAlexandersson
PerAlexandersson marked this pull request as ready for review August 2, 2026 14:10
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