Add Karlin sign-block aggregation foundations

[PerAlexandersson]

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]

Superseded by merged PR #294. The later branch contains the completed stronger sign-regular/rank-sensitive variation-diminishing route, its finite sign-block construction, and the rectangular TNN endpoint. Keeping codex-karlin-v12 available as a recovery/reference branch; closing this PR avoids merging a second parallel sign-block API.