Prove forward Aissen-Schoenberg-Whitney

[PerAlexandersson]

Target

Prove the exact Lean proposition:

aissenSchoenbergWhitneyForwardStatement

currently exposed from RealRooted/AissenSchoenbergWhitney.lean.

Acceptance criteria

• Add a checked theorem inhabiting the proposition without accepting it as a hypothesis.
• Connect the theorem to downstream Hadamard, Veronese, PosCombo, and tactic interfaces so callers no longer need a forward-ASW backend argument.
• Preserve the already checked reverse ASW direction.
• Run focused and aggregate Lake builds and report the proof witness by name.

The proposition alias itself is not a proof.

[PerAlexandersson]

Current proof boundary audit: all forward ASW wrappers (aissenSchoenbergWhitneyForward, splitting/no-nonnegative/zero-aware variants, and root-count projections) are already present. The only admitted dependency is aswKarlinKernelSignVariationClassicalInput in ASWKarlinVariation.lean, the specialized full-row-rank totally-nonnegative one-block Karlin kernel sign-variation lower bound.

A concurrent worker currently has substantial local edits in ASWKarlinKernel.lean, ASWKarlinThreshold.lean, ASWKarlinVariation.lean, and AissenSchoenbergWhitney.lean, so I am not editing this lane to avoid a conflict. Closing #241 requires removing that final sorry and then validating the existing forward wrappers against it.

[PerAlexandersson]

Tactic follow-up after the final kernel theorem is proved without sorry: RealRooted/Tactic/PosCombo.lean still requires callers to supply asw := ... for its ASW-based right-pencil routes. At that point these macros should use the checked forward ASW theorem internally and remove the strategy argument. This should not happen before #241 is genuinely closed, because doing it now would hide the admitted dependency.

[PerAlexandersson]

The forward ASW concern is now substantively resolved: aissenSchoenbergWhitneyForward is already a checked theorem in AissenSchoenbergWhitney.lean. PR #249 removes the misleading legacy aissenSchoenbergWhitneyForwardStatement alias and updates callers to use the theorem directly. Unlike the status-only conversions in #242-#245, this does not replace a proposition by by sorry; it exposes an existing proof. The remaining PR failure is only the root-import check.

[PerAlexandersson]

Resolved by checked theorem aissenSchoenbergWhitneyForward and the proof-status/API cleanup merged in PR #249 as b3c2c13. Downstream Hadamard, Veronese, PosCombo, and tactic interfaces now use the theorem directly rather than accepting a forward-ASW backend or exposing the misleading ...Statement alias. Post-merge comparator run https://github.com/PerAlexandersson/RealRooted/actions/runs/30722922343 completed both the aggregate library build and independent kernel/axiom-closure check successfully.

[PerAlexandersson]

Post-merge tactic audit on current main confirms the migration is complete:

• no file under RealRooted/Tactic/** accepts an asw := strategy/backend argument;
• rr_pos_combo_asw_right_pencil requires only the mathematical nonzero and pf inputs and calls PosComboRealRooted.of_aissenSchoenbergWhitney_right_pencil directly;
• the TNN variant likewise requires only nonzero and tnn;
• RealRooted.PosCombo invokes checked theorem aissenSchoenbergWhitneyForward directly;
• Veronese applications also invoke the checked theorem directly.

The remaining hASW : ...Statement parameters found in foundational bridge modules are generic conditional theorem interfaces, not tactic defaults. They should not be removed indiscriminately because they preserve dependency direction and theorem generality. No additional tactic patch is needed for ASW at this point.

[PerAlexandersson]

Reopening after a source-faithful audit of Karlin, Total Positivity, Vol. I, Ch. 8, §3, Thm. 3.1 and Cor. 3.1 (pp. 398–399). The public ASW wrapper exists, but the forward proof is not closed: ASWKarlinVariation.lean still admits aswKarlinRepeatedZeroFreeKernelSignVariationClassicalInput with sorry. This is an analytic variation-diminishing assertion, not a combinatorial interpretation, so it cannot remain an assumed fact under the project assumption-boundary policy.

The exact remaining source-route obligations are:

1. a checked rectangular totally-nonnegative variation-diminishing theorem;
2. Karlin’s sufficiently-small perturbation argument, giving the nr - 1 sign-variation inequality (not the currently stronger fixed-size boundary);
3. the sampled-sine sign-count/asymptotic estimate;
4. the n → ∞ deduction of the sector threshold.

Existing checked infrastructure already supplies the repeated Karlin matrix, its TN property, full row rank/surjectivity, the root kernel vector, alternating-output variation count, threshold convergence, removal/reinsertion of zero constant terms, and conversion of all sector bounds to splitting. The implementation should therefore follow those four remaining steps from Karlin rather than inventing a recurrence or treating the admitted analytic statement as an allowed model fact.

[PerAlexandersson]

Exact source-route refinement:

• Karlin Ch. 5, §1, Thm. 1.4 (printed p. 222) is the finite-matrix source for S⁻(Mx) ≤ S⁻(x); the dimension-independent form literally covering the wide repeated matrix is Ch. 5, §3, Thm. 3.1(i),(v) (pp. 233–234). No rank hypothesis belongs in the forward inequality.
• Karlin Ch. 8, §3, Thm. 3.1 (pp. 397–399) then uses the full-row-rank repeated matrix only to solve Mₙ x* = y* for a small alternating output, applies forward variation diminution, proves S⁻(x⁰+x*) ≤ S⁻(x⁰)+2, counts sampled-sine variations, divides by n, and lets n → ∞.
• Ch. 5, §2, Thm. 2.2 gives a different, stronger zero-free kernel statement via S⁺; that could justify the repository’s current phased route, but it is not the printed Chapter 8 proof and local S⁺ infrastructure is absent. We will therefore not silently relabel that route as forward variation diminution.

Implementation order for this issue is now fixed by the source: (1) rectangular TN forward variation diminution; (2) source-shaped small perturbation; (3) sampled-sine count/asymptotics; (4) the Chapter 8 assembly and existing threshold-to-splitting endpoint.

[PerAlexandersson]

Draft groundwork PR #285 is open at dd2c9ad. It adds only proved one-block/base cases for the forward variation-diminishing theorem and documents the first missing Karlin step, monotone consecutive-column aggregation. It intentionally does not declare the full theorem, does not close this issue, and adds no admitted backend. Comparator CI is running. The umbrella import is deferred until the concurrent tactic worker releases RealRooted.lean ownership.

[PerAlexandersson]

Merged source-faithful base PR #285 as 47d7d87 after full Comparator success. This establishes the zero-vector convention, nonnegative/nonpositive one-block sectors, and the one-input-column case for forward variation diminution. It does not close this issue. The first unmerged source step remains monotone consecutive-column aggregation; an unpushed candidate exists but has a reported one-line elaboration correction awaiting explicit permission before modification.