Remove Statement-wrapper scaffolding (GeneralizedSnakePosets)

[PerAlexandersson]

Removes Statement-wrapper scaffolding from the GeneralizedSnakePosets (Braun–Jal) development. The main theorem was already proved through the source [P, G; Q, H] matrix route. Everything removed here was packaging or alternative routes around that proof.

Deleted

• Files: CombinatorialPackages.lean (squarecase packages, SquarecaseRook*Statement, OrderPolytopeHStar* wrappers) and SnakeInterlacing.lean (its two _of_snakeRecurrence conditionals were folded into SnakeRecurrence.lean).
• Statements.lean:
  • SquarecaseRookModelSnakeInterlacingStatement and the two projection wrappers.
  • ModifiedNarayanaFamilyStatement and AuxiliaryGMatchesTruncatedStaircasesStatement.
  • AuxiliaryGInterlacesStatement and all four …UpToStatements, with their _of_statement, _of_shifted and _iff wrappers.
  • The GeneralizedSnakeRecurrenceComputableStatement and SnakeInterlacingInductionRoute(Computable)Statement defs, plus the _of_/_iff conversions between them.
  • The four SnakeInterlacing*Inputs structures, their conversions, and the snakeInterlacing_of_combinatorial*Inputs theorems.
  • ShiftedDifferenceInterlacingSideConditions and its bundled wrapper. This bundle was refuted for the concrete family; the explicit obstruction lemma …_left_boundary_not_strictRootBound is kept, and the ¬ …SideConditions wrapper is dropped.
• Alternative routes:
  • The four snakeInterlacingInductionRoute_* theorems in MatrixInduction.
  • The vacuous route in RootSums, which took the refuted side conditions.
  • snakeInterlacingInductionRoute_modified_of_modelInputs and the two nonNestingRookInterlacing_modified_of_modelInputs* theorems.
• Turan:
  • ModifiedNarayanaTuranNonnegOnNonpos(UpTo)Statement, its witness wrapper and the Jacobi reduction.
  • The _of_statement wrapper, the two …_of_turanNonnegUpTo theorems and the eight …_upTo_N packagings.
• RankSix and LowRank:
  • The ModifiedNarayanaSixAuxiliaryGSignCertificate and …RootIntervalCertificate Props, together with their _of_eval_signs wrappers.
  • …_of_le_six_of_eval_signs and …_upTo_six.
  • narayanaAuxiliaryGRecurrence_modified_upTo_eight.

Restated or renamed

• snakeInterlacing_generalizedSnakeRookModel is restated with explicit binders, and generalizedSnakeRookModel_natDegree_eq is now proved directly. The catalog call sites are unchanged.
• generalizedSnakeRecurrence now has the predicate type directly; the GeneralizedSnakeRecurrenceHolds abbrev is gone.
• Ferrers: ferrersFirstColumnDeletionStatement_holds → FiniteSkewBoard.ferrersRookPolynomial_firstColumnDeletion (explicit).
• FiniteSkewBoard.auxiliaryG_matchesTruncatedStaircases, modifiedNarayanaFamily_narayana/_coeff and auxiliaryGInterlaces_modified are stated explicitly.
• modifiedNarayanaPolynomial_six_rootIntervals (explicit ∃) and ModifiedNarayanaSixAuxiliaryGCrossInequalities.of_sorted_roots replace the certificate-taking versions.
• affineModifiedNarayana(Shifted)_right_eval_mul_prev_nonpos drop the now-redundant Turan hypothesis (formerly _of_turanNonneg).

Kept

• These parametric predicates on abstract P, G, M stay, because the generic induction in MatrixInduction and Statements takes them as hypotheses:

  • NonNestingRookInterlacingStatement
  • NarayanaAuxiliaryGRecurrenceStatement
  • AffineModifiedNarayana(Shifted)InterlacingStatement
  • Snake/ShiftedDifferenceInterlacingStatement
  • GeneralizedSnakeRecurrenceStatement

  Their concrete witnesses keep the predicate type so they can still be passed to that generic induction.

• The genuine reductions shiftedDifferenceInterlacing_of_combinatorial(_rootSumSideConditions) stay, along with ShiftedDifferenceInterlacingRootSumSideConditions (it is on the proof path).

• The finite Turan determinants and _nonneg_of_le_N lemmas stay.

• auxiliaryG_strictInterl_succ_of_narayanaTwoModel stays. It is a conditional lemma whose hypothesis is unverified.

• Several modified-family lemmas still take hrec2 : NarayanaAuxiliaryGRecurrenceStatement … as a hypothesis. This comes from import order: the recurrence is proved later, in ColumnRecurrence.

🤖 Generated with Claude Code