Instantiate Braun-Jal Theorem 4.1 for the non-nesting rook model

[PerAlexandersson]

Priority

Erik priority 9.

Source

B. Braun and A. Jal, Order polytopes of generalized snake posets are
h-real-rooted*, arXiv:2607.00922v1:

• equation (2) and Lemma 3.3, pp. 7--8;
• Theorem 3.5, pp. 8--9;
• Theorem 4.1 and Claims (6)--(7), pp. 9--10.

Source-faithful definitions

For a word of list length n, the constant-word polynomial is P (n + 1).
For the nonconstant induction step, set

• Q m = P m - P (m - 1);
• H m = G m - G (m - 1).

The matrix displayed in the proof is
[[P (m - 1), G (m - 1)], [Q m, H m]], acting on [f, X * g].
It produces [M w', M w - M w']. Claim (6) is exactly its cross-affine
interlacing condition. The paper does not require consecutive proper
position of the G family and does not use an identity
G n = n * N^(2)_(n - 1).

PR #330 corrects the Lean matrix definition and the previous misleading
attribution.

Current Lean status

The intended concrete model is generalizedSnakeRookModel, with
generalizedSnakeRookModel.snakePolynomial w definitionally equal to
(generalizedSnakeBoard w).rookPolynomial.

Already formalized:

• the concrete modified Narayana family and consecutive P interlacing;
• Lemma 3.4 for the modified Narayana family;
• the analytic conversion from equation (2) and the side conditions to Claim (7);
• the Claim (6) / Claim (7) reindexing;
• the strong-induction skeleton and constant-word successor indexing;
• finite-board rook-polynomial coefficient nonnegativity.

Still missing for an unconditional source-faithful endpoint:

• the source [P, G; Q, H] matrix-preserver step yielding
  M w' << M w - M w', followed by Braun--Jal Lemma 2.6;
• all-index equation (2), or its documented combinatorial boundary hypothesis;
• coefficientwise nonnegativity of H m, or its documented board-model boundary hypothesis;
• the concrete Theorem 3.5 recurrence;
• the concrete deletion degree bridge;
• the constant-word staircase identity.

The previous issue text incorrectly said
theorem41NonNestingRook_modified_of_modelInputs already supplied the checked
analytic route. That theorem instead used an additional adjacent-G route and
therefore did not match the source proof.

Goal

Instantiate the corrected source proof for generalizedSnakeRookModel and
expose an actual theorem proving Theorem41NonNestingRookStatement for its
snake polynomial.

Acceptance criteria

• Use the concrete/model-facing M above.
• Follow equation (2), Lemma 3.4, Claims (6)--(7), the source matrix step, and strong induction.
• Permit only combinatorial interpretation facts as explicit boundary hypotheses.
• Give every boundary hypothesis a nearby source comment explaining why the full combinatorial model is omitted.
• Do not assume real-rootedness, splitting, proper position, or interlacing at the boundary.
• Do not reintroduce consecutive auxiliary-G proper position as a source requirement.
• Expose an actual theorem, not only a def ...Statement : Prop interface.

[PerAlexandersson]

Primary-source audit confirms the exact Theorem 4.1 statement but exposes one additional interface requirement.

For a nonempty snake word w, with w' obtained by deleting the final letter, Braun--Jal prove that the ordinary non-nesting rook polynomial M_{epsilon w} is real-rooted and M_{epsilon w'} interlaces M_{epsilon w}. The current deleteFinal and argument order are correct.

The defect is the arbitrary parameter M : SnakeWord -> R[X]: it is not tied to the canonical skew board or to the generating function sum over non-nesting rook placements. A source-faithful boundary hypothesis may identify M w with that ordinary rook-count polynomial, including constant term 1 and the required degree/coefficient facts. This combinatorial identification is appropriate to leave unformalized with a nearby explanation, but real-rootedness/interlacing must still be derived from the checked recurrence route.

Source: Braun--Jal, arXiv:2607.00922v1, Theorem 4.1, with the rook polynomial defined in Section 2.2.

[PerAlexandersson]

Primary-source refinement: the concrete Lean polynomial already exists as (generalizedSnakeBoard w).rookPolynomial (generalizedSnakeRookModel). The missing work is not inventing the model but wiring the checked analytic theorem to that concrete model.

Braun--Jal Theorem 4.1 (arXiv:2607.00922v1, pp. 9--10) states M_{epsilon w.deleteFinal} << M_{epsilon w} and real-rootedness for suffix length at least one. Theorem41NonNestingRookStatement M has the right deletion orientation and length guard, but for arbitrary M it is only a package, not the source theorem. A source-facing endpoint must specialize to generalizedSnakeRookModel and discharge or explicitly assume, with source comments, only the combinatorial identifications/recurrences. Real-rootedness, interlacing, Claim (7), and Narayana analytic inputs must remain proved analytic conclusions, not combinatorial assumptions.

[PerAlexandersson]

PR #330 now includes the source Claim-(6) matrix step and its word-level Theorem 3.5 application. The new route proves M w.deleteFinal << M w - M w.deleteFinal using [P,G;Q,H], then applies the nonnegative cone form of Braun--Jal Lemma 2.6 to obtain M w.deleteFinal << M w. It has no adjacent-G proper-position hypothesis. Comparator validation is pending; no local build was run.

[PerAlexandersson]

PR #330 now also contains the strong-induction endpoint theorem41NonNestingRook_modified_of_sourceInputs. Its assumptions are restricted to the documented combinatorial boundary: equation (2), H-difference nonnegativity, Theorem 3.5, model coefficient nonnegativity, the degree bridge, and the constant-word staircase identity. It assumes no splitting/interlacing/proper position and no adjacent-G theorem. Comparator validation is pending.

[PerAlexandersson]

PR #330 now exposes Challenges.BraunJal.generalizedSnakeRookModel_theorem41. It fixes M to the concrete generalized-snake rook model and derives its coefficient nonnegativity from FiniteSkewBoard.rookPolynomial_hasNonnegCoeffs. The old challenge-facing hG_model route and order-polytope wrapper were replaced by the source [P,G;Q,H] endpoint. Comparator validation is pending.

[PerAlexandersson]

Current PR #330 status at ca79f490: the full Lean library build is green, including MatrixInduction, Narayana/Claim7, and Challenges/BraunJal. The comparator workspace also built successfully and the three theorem kernel/axiom-closure checks are still running. I am leaving the branch unchanged so that gate can finish.

[PerAlexandersson]

Acceptance audit complete. PR #330 now passes the full Lean build and the independent comparator/kernel/axiom-closure check at ca79f490. It provides the concrete generalizedSnakeRookModel_theorem41, follows Braun--Jal equation (2), Claims (6)--(7), Theorem 3.5, and strong induction, and leaves only documented combinatorial model facts as assumptions. The PR is ready for review and closes this issue on merge.