Fix Braun--Jal Theorem 4.1 source matrix

[PerAlexandersson]

Summary

• correct Braun--Jal's Theorem 4.1 step matrix to the displayed [P,G;Q,H] matrix
• prove the Claim-(6) matrix action and strong-induction route without adjacent-G proper position
• specialize the analytic route to the modified Narayana and finite-board auxiliary families
• expose Challenges.BraunJal.generalizedSnakeRookModel_theorem41 for the concrete rook model
• replace the old challenge-facing parameter-two Narayana shortcut with the source proof

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

Trust boundary

The concrete theorem leaves only combinatorial model facts explicit:

• equation (2)
• coefficientwise nonnegativity of H_m = G_m - G_(m-1)
• Theorem 3.5
• the deletion degree identity
• the constant-word staircase identity

Model coefficient nonnegativity is derived from FiniteSkewBoard.rookPolynomial_hasNonnegCoeffs. No boundary hypothesis assumes real-rootedness, splitting, proper position, or interlacing.

Acceptance audit

• concrete generalizedSnakeRookModel
• source [P,G;Q,H] matrix and Claim (6)
• source successor indexing P (w.length + 1)
• documented combinatorial boundary assumptions
• actual theorem endpoint rather than another def ...Statement : Prop
• no adjacent-G source requirement

Validation

GitHub's full Lean library build and comparator workspace build are green at ca79f490. The independent three-theorem kernel/axiom-closure comparator step is still running.

Closes #320.

[PerAlexandersson]

Scheduled cleanup pass: removed three unreferenced wrappers that reindexed Claim (6) to Claim (7) and then used the stronger consecutive-G route. This leaves the corrected source [P,G;Q,H] matrix API unambiguous. No build was run.

[PerAlexandersson]

Scheduled cleanup: removed the separately threaded Q_m != 0 hypothesis from the source matrix step and all downstream endpoints. Claim (6) at lam = mu = 0 already supplies this nonzero fact, so the concrete modified-Narayana proof was duplicate information. No build was run.

[PerAlexandersson]

Comparator repair: the only reported error was rewrite order in the word-level source step. The patch now proves the raw matrix-expression Prec first and rewrites hrec_del and hrec_diff in reverse, preserving both patterns. No local build was run.

[PerAlexandersson]

Scheduled mechanical cleanup: comparator for ffdc34aa exposed an endpoint elaboration ambiguity after the already-fixed rewrite error. The successor-length wrapper now introduces w and hw explicitly, matching the established neighboring wrapper. No local build was run.

[PerAlexandersson]

Scheduled cleanup only: replaced the comparator-reported convert ... <;> ring sequence with a named polynomial identity and direct rewrite. No theorem statement, assumption, or dependency changed. The previous comparator run was green; the new head will rerun CI.