Add Karlin variation-diminishing base cases

[PerAlexandersson]

Source-faithful groundwork for reopened #241.

This adds only checked base cases for Karlin’s forward variation-diminishing theorem (Chapter 5, Sections 1 and 3):

• explicit handling of the local S^- (0) = 0 convention;
• TN matrices preserve nonnegative/nonpositive sectors;
• forward sign-variation bounds on those one-block sectors;
• the one-input-column base case.

It deliberately does not declare the full theorem. The module documents the first missing source step: total nonnegativity under monotone consecutive-column aggregation, followed by Karlin’s alternating-sector and non-strict-limit arguments. No sorry, axiom, or ...Statement : Prop backend is introduced.

The branch is restacked on current main after #286 and now includes its direct RealRooted.lean umbrella import.

Does not close #241.