diff --git a/.gitignore b/.gitignore index 499ecee80..b37ffac96 100644 --- a/.gitignore +++ b/.gitignore @@ -38,3 +38,4 @@ realrooted-interlacing-seminar-handout.html *.log *.out *.synctex.gz +__pycache__/ diff --git a/RealRooted.lean b/RealRooted.lean index c39d6a044..b377c75e4 100644 --- a/RealRooted.lean +++ b/RealRooted.lean @@ -427,7 +427,6 @@ import RealRooted.GeneralizedSnakePosets.Narayana.Recurrence import RealRooted.GeneralizedSnakePosets.Narayana.RootSums import RealRooted.GeneralizedSnakePosets.Narayana.Turan import RealRooted.GeneralizedSnakePosets.Narayana.TuranCertificates -import RealRooted.GeneralizedSnakePosets.CombinatorialPackages import RealRooted.GeneralizedSnakePosets.SnakeBoard import RealRooted.GeneralizedSnakePosets.SnakeCover import RealRooted.GeneralizedSnakePosets.SnakeReachability @@ -1497,7 +1496,6 @@ import RealRooted.GeneralizedSnakePosets.ChainPolynomial import RealRooted.GeneralizedSnakePosets.SnakeBand import RealRooted.GeneralizedSnakePosets.SnakeConstant import RealRooted.GeneralizedSnakePosets.SnakeRecurrence -import RealRooted.GeneralizedSnakePosets.SnakeInterlacing import RealRooted.GeneralizedSnakePosets.TruncatedStaircase.ColumnRecurrence import RealRooted.Challenges.LiuOppositeSigns import RealRooted.Challenges.PerronFrobenius diff --git a/RealRooted/GeneralizedSnakePosets.lean b/RealRooted/GeneralizedSnakePosets.lean index 7ea5aa79b..3828fe20d 100644 --- a/RealRooted/GeneralizedSnakePosets.lean +++ b/RealRooted/GeneralizedSnakePosets.lean @@ -1,5 +1,4 @@ import RealRooted.GeneralizedSnakePosets.SnakeStaircase -import RealRooted.GeneralizedSnakePosets.CombinatorialPackages import RealRooted.GeneralizedSnakePosets.MatrixInduction import RealRooted.GeneralizedSnakePosets.TruncatedStaircase @@ -10,11 +9,9 @@ This file contains the concrete finite-board interfaces for Braun--Jal, *Order polytopes of generalized snake posets are h^*-real-rooted*, arXiv:2607.00922v1. -The paper-facing theorem statements and the combinatorial packages live in -`RealRooted.GeneralizedSnakePosets.Statements` and -`RealRooted.GeneralizedSnakePosets.CombinatorialPackages`. This module imports the -package layer as an umbrella, so downstream files that import -`RealRooted.GeneralizedSnakePosets` keep the same public API. +The parametric predicates used by the snake-interlacing induction live in +`RealRooted.GeneralizedSnakePosets.Statements`; the induction itself is in +`RealRooted.GeneralizedSnakePosets.MatrixInduction`. -/ open Polynomial @@ -153,22 +150,6 @@ theorem ferrersRookPolynomial_ne_zero (lam : List ℕ) : ferrersRookPolynomial lam ≠ 0 := rookPolynomial_ne_zero _ -/-- The first-column deletion identity, stated for a straight Ferrers rook-polynomial -family indexed by integer partitions. The partition hypothesis is needed: -without positive row lengths, the one-row list `[0]` gives the false identity -`1 = 1 + X`. -/ -def FerrersFirstColumnDeletionStatement (M : List ℕ → ℝ[X]) : Prop := - ∀ lam : List ℕ, IsIntegerPartition lam → - M lam = - M (partitionSubOne lam) + - X * ((List.range lam.length).map fun i => - M (partitionPrefix (partitionSubOne lam) i)).sum - -/-- The first-column deletion identity as the target statement for the concrete finite -Ferrers-board rook-polynomial model. -/ -def ferrersFirstColumnDeletionStatement : Prop := - FerrersFirstColumnDeletionStatement ferrersRookPolynomial - /-- Valid Ferrers placements with no rook in the first column. -/ def nonNestingPlacementsWithoutFirstColumn (lam : List ℕ) : Finset (Finset (ℕ × ℕ)) := by @@ -942,11 +923,16 @@ theorem sum_firstColumnCells_nonNestingPlacementsWithCell_eq_mul_sum List.sum_map_mul_left (List.range lam.length) (fun i => ferrersRookPolynomial (partitionPrefix (partitionSubOne lam) i)) X -/-- The first-column deletion identity for the concrete finite Ferrers-board -non-nesting rook-polynomial model. -/ -theorem ferrersFirstColumnDeletionStatement_holds : - ferrersFirstColumnDeletionStatement := by - intro lam hpart +/-- The first-column deletion identity for the finite Ferrers-board +non-nesting rook polynomials. The partition hypothesis is needed: without +positive row lengths, the one-row list `[0]` gives the false identity +`1 = 1 + X`. -/ +theorem ferrersRookPolynomial_firstColumnDeletion (lam : List ℕ) + (hpart : IsIntegerPartition lam) : + ferrersRookPolynomial lam = + ferrersRookPolynomial (partitionSubOne lam) + + X * ((List.range lam.length).map fun i => + ferrersRookPolynomial (partitionPrefix (partitionSubOne lam) i)).sum := by calc ferrersRookPolynomial lam = ((ferrers lam).nonNestingPlacements).sum @@ -971,13 +957,11 @@ theorem ferrersFirstColumnDeletionStatement_holds : end FiniteSkewBoard -/-- The finite-board definition of `G_n` satisfies the truncated-staircase -interface. -/ -theorem FiniteSkewBoard.auxiliaryG_matchesTruncatedStaircases : - AuxiliaryGMatchesTruncatedStaircasesStatement - FiniteSkewBoard.truncatedStaircaseRookPolynomial - FiniteSkewBoard.auxiliaryG := by - intro n +/-- The auxiliary polynomial `G_n` is the sum of the non-nesting rook +polynomials of the truncated staircases `mu_{n,i}` for `i = 0, ..., n - 1`. -/ +theorem FiniteSkewBoard.auxiliaryG_matchesTruncatedStaircases (n : ℕ) : + FiniteSkewBoard.auxiliaryG n = + ((List.range n).map fun i => FiniteSkewBoard.truncatedStaircaseRookPolynomial n i).sum := rfl diff --git a/RealRooted/GeneralizedSnakePosets/CombinatorialPackages.lean b/RealRooted/GeneralizedSnakePosets/CombinatorialPackages.lean deleted file mode 100644 index ec3ccd053..000000000 --- a/RealRooted/GeneralizedSnakePosets/CombinatorialPackages.lean +++ /dev/null @@ -1,334 +0,0 @@ -import RealRooted.GeneralizedSnakePosets.Statements - -/-! -# The combinatorial packages - -This module bundles combinatorial recurrence and interlacing inputs used to -feed the abstract snake-interlacing induction route. It also contains the -order-polytope `h^*` statement wrappers that sit above the non-nesting rook -polynomial model. --/ - -open Polynomial - -noncomputable section - -namespace RealRooted -namespace GeneralizedSnakePosets - -universe u - -/-! ## Squarecase recurrence packages -/ - -/-- Existence statement for a squarecase model satisfying the computable -the snake-recurrence recurrence for some combinatorial families `P` and `G`. -/ -def SquarecaseRookRecurrenceStatement (model : SquarecaseRookModel) : Prop := - ∃ P G : ℕ → ℝ[X], - GeneralizedSnakeRecurrenceComputableStatement - model.snakePolynomial P G - -/-- Data package for a concrete squarecase/non-nesting rook recurrence. - -Later board files should construct this from the actual squarecase board model -and Braun--Jal's positive recurrence. -/ -structure SquarecaseRookRecurrencePackage (model : SquarecaseRookModel) where - P : ℕ → ℝ[X] - G : ℕ → ℝ[X] - recurrence : - GeneralizedSnakeRecurrenceComputableStatement - model.snakePolynomial P G - -namespace SquarecaseRookRecurrencePackage - -/-- Forget a recurrence data package to the corresponding existence -statement. -/ -theorem statement {model : SquarecaseRookModel} - (h : SquarecaseRookRecurrencePackage model) : - SquarecaseRookRecurrenceStatement model := - ⟨h.P, h.G, h.recurrence⟩ - -end SquarecaseRookRecurrencePackage - -/-- Existence statement for a squarecase model equipped with the combinatorial -inputs needed by the current snake-interlacing induction route. -/ -def SquarecaseRookCombinatorialStatement (model : SquarecaseRookModel) : Prop := - ∃ P G : ℕ → ℝ[X], - SnakeInterlacingComputableInputs model.snakePolynomial P G - -/-- Data package for the squarecase/non-nesting rook model together with the -Narayana and recurrence inputs from the combinatorial inputs. -/ -structure SquarecaseRookCombinatorialPackage (model : SquarecaseRookModel) where - P : ℕ → ℝ[X] - G : ℕ → ℝ[X] - auxiliaryGInterlacing : AuxiliaryGInterlacesStatement P G - affineNarayana : AffineModifiedNarayanaInterlacingStatement P - recurrence : - GeneralizedSnakeRecurrenceComputableStatement - model.snakePolynomial P G - -namespace SquarecaseRookCombinatorialPackage - -/-- The recurrence component of a combinatorial package as a standalone squarecase -recurrence package. -/ -def recurrencePackage {model : SquarecaseRookModel} - (h : SquarecaseRookCombinatorialPackage model) : - SquarecaseRookRecurrencePackage model where - P := h.P - G := h.G - recurrence := h.recurrence - -/-- Forget a combinatorial data package to the corresponding existence statement. --/ -theorem statement {model : SquarecaseRookModel} - (h : SquarecaseRookCombinatorialPackage model) : - SquarecaseRookCombinatorialStatement model := - ⟨h.P, h.G, ⟨h.auxiliaryGInterlacing, h.affineNarayana, h.recurrence⟩⟩ - -/-- A squarecase combinatorial package provides the existing computable input -bundle for the attached polynomial families. -/ -theorem computableInputs {model : SquarecaseRookModel} - (h : SquarecaseRookCombinatorialPackage model) : - SnakeInterlacingComputableInputs model.snakePolynomial h.P h.G where - auxiliaryGInterlacing := h.auxiliaryGInterlacing - affineNarayana := h.affineNarayana - recurrence := h.recurrence - -/-- A squarecase combinatorial package provides the predicate-form input bundle for -the attached polynomial families. -/ -theorem inputs {model : SquarecaseRookModel} - (h : SquarecaseRookCombinatorialPackage model) : - SnakeInterlacingInputs model.snakePolynomial h.P h.G := - snakeInterlacingInputs_of_computable h.computableInputs - -/-- Feed a squarecase combinatorial package into the abstract snake-interlacing induction -route. -/ -theorem snakeInterlacing {model : SquarecaseRookModel} - (h : SquarecaseRookCombinatorialPackage model) - (hroute : SnakeInterlacingInductionRouteStatement model.snakePolynomial h.P h.G) : - SquarecaseRookModelSnakeInterlacingStatement model := - snakeInterlacing_of_combinatorialInputs hroute h.inputs - -/-- Feed a squarecase combinatorial package into the computable form of the -abstract snake-interlacing induction route. -/ -theorem snakeInterlacingComputable {model : SquarecaseRookModel} - (h : SquarecaseRookCombinatorialPackage model) - (hroute : - SnakeInterlacingInductionRouteComputableStatement model.snakePolynomial h.P h.G) : - SquarecaseRookModelSnakeInterlacingStatement model := - hroute h.auxiliaryGInterlacing h.affineNarayana h.recurrence - -/-- A squarecase combinatorial package also gives the standalone recurrence -existence statement. -/ -theorem recurrenceStatement {model : SquarecaseRookModel} - (h : SquarecaseRookCombinatorialPackage model) : - SquarecaseRookRecurrenceStatement model := - h.recurrencePackage.statement - -end SquarecaseRookCombinatorialPackage - -/-- Data package for the squarecase/non-nesting rook model when the affine Narayana interlacing -lemma is -proved in shifted nonnegative-parameter form. -/ -structure SquarecaseRookCombinatorialShiftedPackage - (model : SquarecaseRookModel) where - P : ℕ → ℝ[X] - G : ℕ → ℝ[X] - auxiliaryGInterlacing : AuxiliaryGInterlacesStatement P G - affineNarayana : AffineModifiedNarayanaShiftedInterlacingStatement P - recurrence : - GeneralizedSnakeRecurrenceComputableStatement - model.snakePolynomial P G - -namespace SquarecaseRookCombinatorialShiftedPackage - -/-- Convert a shifted combinatorial package to the existing paper-shaped combinatorial -package. -/ -def combinatorialPackage {model : SquarecaseRookModel} - (h : SquarecaseRookCombinatorialShiftedPackage model) : - SquarecaseRookCombinatorialPackage model where - P := h.P - G := h.G - auxiliaryGInterlacing := h.auxiliaryGInterlacing - affineNarayana := affineModifiedNarayanaInterlacing_of_shifted h.affineNarayana - recurrence := h.recurrence - -/-- A shifted combinatorial package also gives the existing paper-shaped existence -statement. -/ -theorem statement {model : SquarecaseRookModel} - (h : SquarecaseRookCombinatorialShiftedPackage model) : - SquarecaseRookCombinatorialStatement model := - h.combinatorialPackage.statement - -/-- A shifted combinatorial package provides the computable shifted input bundle. --/ -theorem computableShiftedInputs {model : SquarecaseRookModel} - (h : SquarecaseRookCombinatorialShiftedPackage model) : - SnakeInterlacingComputableShiftedInputs - model.snakePolynomial h.P h.G where - auxiliaryGInterlacing := h.auxiliaryGInterlacing - affineNarayana := h.affineNarayana - recurrence := h.recurrence - -/-- A shifted combinatorial package provides the paper-shaped computable input -bundle. -/ -theorem computableInputs {model : SquarecaseRookModel} - (h : SquarecaseRookCombinatorialShiftedPackage model) : - SnakeInterlacingComputableInputs model.snakePolynomial h.P h.G := - snakeInterlacingComputableInputs_of_shifted h.computableShiftedInputs - -/-- A shifted combinatorial package provides the predicate-form shifted input -bundle. -/ -theorem shiftedInputs {model : SquarecaseRookModel} - (h : SquarecaseRookCombinatorialShiftedPackage model) : - SnakeInterlacingShiftedInputs model.snakePolynomial h.P h.G := - snakeInterlacingShiftedInputs_of_computable h.computableShiftedInputs - -/-- A shifted combinatorial package provides the existing predicate-form input -bundle. -/ -theorem inputs {model : SquarecaseRookModel} - (h : SquarecaseRookCombinatorialShiftedPackage model) : - SnakeInterlacingInputs model.snakePolynomial h.P h.G := - snakeInterlacingInputs_of_shifted h.shiftedInputs - -/-- The recurrence component of a shifted combinatorial package as a standalone -squarecase recurrence package. -/ -def recurrencePackage {model : SquarecaseRookModel} - (h : SquarecaseRookCombinatorialShiftedPackage model) : - SquarecaseRookRecurrencePackage model where - P := h.P - G := h.G - recurrence := h.recurrence - -/-- Feed a shifted squarecase combinatorial package into the abstract snake-interlacing -induction route. -/ -theorem snakeInterlacing {model : SquarecaseRookModel} - (h : SquarecaseRookCombinatorialShiftedPackage model) - (hroute : SnakeInterlacingInductionRouteStatement model.snakePolynomial h.P h.G) : - SquarecaseRookModelSnakeInterlacingStatement model := - snakeInterlacing_of_combinatorialShiftedInputs hroute h.shiftedInputs - -/-- Feed a shifted squarecase combinatorial package into the computable form of -the abstract snake-interlacing induction route. -/ -theorem snakeInterlacingComputable {model : SquarecaseRookModel} - (h : SquarecaseRookCombinatorialShiftedPackage model) - (hroute : - SnakeInterlacingInductionRouteComputableStatement model.snakePolynomial h.P h.G) : - SquarecaseRookModelSnakeInterlacingStatement model := - hroute - h.auxiliaryGInterlacing - (affineModifiedNarayanaInterlacing_of_shifted h.affineNarayana) - h.recurrence - -/-- A shifted squarecase combinatorial package also gives the standalone -recurrence existence statement. -/ -theorem recurrenceStatement {model : SquarecaseRookModel} - (h : SquarecaseRookCombinatorialShiftedPackage model) : - SquarecaseRookRecurrenceStatement model := - h.recurrencePackage.statement - -end SquarecaseRookCombinatorialShiftedPackage - -/-- The combinatorial inputs for a squarecase model include snake-recurrence recurrence -input needed by the Braun--Jal induction. -/ -theorem squarecaseRookRecurrenceStatement_of_combinatorialStatement - {model : SquarecaseRookModel} - (hsection : SquarecaseRookCombinatorialStatement model) : - SquarecaseRookRecurrenceStatement model := by - rcases hsection with ⟨P, G, hinputs⟩ - exact ⟨P, G, hinputs.recurrence⟩ - -/-- A statement-level squarecase combinatorial witness plus the abstract induction -route proves the non-nesting-rook form of the snake interlacing theorem. -/ -theorem snakeInterlacing_of_squarecaseCombinatorialStatement - {model : SquarecaseRookModel} - (hroute : - ∀ P G : ℕ → ℝ[X], - SnakeInterlacingInductionRouteStatement model.snakePolynomial P G) - (hsection : SquarecaseRookCombinatorialStatement model) : - SquarecaseRookModelSnakeInterlacingStatement model := by - rcases hsection with ⟨P, G, hinputs⟩ - exact snakeInterlacing_of_combinatorialComputableInputs (hroute P G) hinputs - -/-- A statement-level squarecase combinatorial witness plus a computable abstract -induction route proves the non-nesting-rook form of the snake interlacing theorem. -/ -theorem snakeInterlacing_of_squarecaseCombinatorialComputableStatement - {model : SquarecaseRookModel} - (hroute : - ∀ P G : ℕ → ℝ[X], - SnakeInterlacingInductionRouteComputableStatement model.snakePolynomial P G) - (hsection : SquarecaseRookCombinatorialStatement model) : - SquarecaseRookModelSnakeInterlacingStatement model := by - rcases hsection with ⟨P, G, hinputs⟩ - exact hroute P G hinputs.auxiliaryGInterlacing hinputs.affineNarayana hinputs.recurrence - -/-- Statement that a chosen order-polytope `h^*` model agrees with the -non-nesting rook polynomial model for generalized snake words. -/ -def OrderPolytopeHStarMatchesNonNestingRook - (hStar M : SnakeWord → ℝ[X]) : Prop := - ∀ w : SnakeWord, hStar w = M w - -/-- Final order-polytope `h^*` real-rootedness statement, isolated from the -rook-polynomial model. -/ -def OrderPolytopeHStarRealRootedStatement - (hStar : SnakeWord → ℝ[X]) : Prop := - ∀ {w : SnakeWord}, 1 ≤ w.length → hStar w ≠ 0 ∧ (hStar w).Splits - -/-- The snake interlacing theorem plus the Stanley/Alexandersson--Jal matching interface implies -the order-polytope `h^*` real-rootedness wrapper. -/ -theorem orderPolytopeHStarRealRooted_of_snakeInterlacing - {hStar M : SnakeWord → ℝ[X]} - (hBJ : NonNestingRookInterlacingStatement M) - (hmatch : OrderPolytopeHStarMatchesNonNestingRook hStar M) : - OrderPolytopeHStarRealRootedStatement hStar := by - intro w hw - simpa [hmatch w] using - nonNestingRook_ne_zero_and_splits_of_snakeInterlacing hBJ (w := w) hw - -/-- A statement-level squarecase combinatorial witness plus the abstract induction -route and order-polytope matching proves the final `h^*` real-rootedness -wrapper. -/ -theorem orderPolytopeHStarRealRooted_of_squarecaseCombinatorialStatement - {hStar : SnakeWord → ℝ[X]} {model : SquarecaseRookModel} - (hroute : - ∀ P G : ℕ → ℝ[X], - SnakeInterlacingInductionRouteStatement model.snakePolynomial P G) - (hsection : SquarecaseRookCombinatorialStatement model) - (hmatch : - OrderPolytopeHStarMatchesNonNestingRook hStar model.snakePolynomial) : - OrderPolytopeHStarRealRootedStatement hStar := - orderPolytopeHStarRealRooted_of_snakeInterlacing - (snakeInterlacing_of_squarecaseCombinatorialStatement hroute hsection) hmatch - -/-- A squarecase combinatorial package, a matching computable induction route, and -the order-polytope matching interface prove the final `h^*` real-rootedness -wrapper. -/ -theorem orderPolytopeHStarRealRooted_of_squarecaseCombinatorialPackage - {hStar : SnakeWord → ℝ[X]} {model : SquarecaseRookModel} - (hsection : SquarecaseRookCombinatorialPackage model) - (hroute : - SnakeInterlacingInductionRouteComputableStatement - model.snakePolynomial hsection.P hsection.G) - (hmatch : - OrderPolytopeHStarMatchesNonNestingRook hStar model.snakePolynomial) : - OrderPolytopeHStarRealRootedStatement hStar := - orderPolytopeHStarRealRooted_of_snakeInterlacing - (hsection.snakeInterlacingComputable hroute) hmatch - -/-- A statement-level squarecase combinatorial witness plus a computable abstract -induction route and order-polytope matching proves the final `h^*` -real-rootedness wrapper. -/ -theorem orderPolytopeHStarRealRooted_of_squarecaseCombinatorialComputableStatement - {hStar : SnakeWord → ℝ[X]} {model : SquarecaseRookModel} - (hroute : - ∀ P G : ℕ → ℝ[X], - SnakeInterlacingInductionRouteComputableStatement model.snakePolynomial P G) - (hsection : SquarecaseRookCombinatorialStatement model) - (hmatch : - OrderPolytopeHStarMatchesNonNestingRook hStar model.snakePolynomial) : - OrderPolytopeHStarRealRootedStatement hStar := - orderPolytopeHStarRealRooted_of_snakeInterlacing - (snakeInterlacing_of_squarecaseCombinatorialComputableStatement hroute hsection) - hmatch - -end GeneralizedSnakePosets -end RealRooted diff --git a/RealRooted/GeneralizedSnakePosets/MatrixInduction.lean b/RealRooted/GeneralizedSnakePosets/MatrixInduction.lean index eabf86a9c..e84a299bf 100644 --- a/RealRooted/GeneralizedSnakePosets/MatrixInduction.lean +++ b/RealRooted/GeneralizedSnakePosets/MatrixInduction.lean @@ -723,117 +723,5 @@ theorem snakeInterlacing_of_shiftedDifferenceInterlacing_of_constant_matches_suc (hM_nonneg := hM_nonneg) (hdeg := hdeg) (hconst := hconst) (w := w) hw -/-- Package the shifted difference-interlacing induction theorem as the abstract route predicate, -with the constant-word branch reduced to a length-model identity. -/ -theorem snakeInterlacingInductionRoute_of_shiftedDifference_of_constant_matches_length - {M : SnakeWord → ℝ[X]} {P G : ℕ → ℝ[X]} - (hclaim_of_inputs : - AuxiliaryGInterlacesStatement P G → - AffineModifiedNarayanaInterlacingStatement P → - ShiftedDifferenceInterlacingStatement P G) - (hP_interlaces : ∀ {m : ℕ}, 1 ≤ m → Interlaces (P (m - 1)) (P m)) - (hG : ∀ {m : ℕ}, 2 ≤ m → StrictInterl (G (m - 1)) (G m)) - (hP_one : P 1 = 1 + X) (hG_one : G 1 = 1) - (hP_nonneg : ∀ n, HasNonnegCoeffs (P n)) - (hG_nonneg : ∀ n, HasNonnegCoeffs (G n)) - (hM_nonneg : ∀ w, HasNonnegCoeffs (M w)) - (hdeg : - ∀ {w : SnakeWord}, 1 ≤ w.length → - (M w.deleteFinal).natDegree + 1 = (M w).natDegree) - (hM_const : ∀ {w : SnakeWord}, w.IsConstant → M w = P w.length) : - SnakeInterlacingInductionRouteStatement M P G := by - intro h33 h34 hrec - exact snakeInterlacing_of_shiftedDifferenceInterlacing_of_constant_matches_length - (M := M) (P := P) (G := G) - (hrec := hrec) (hclaim := hclaim_of_inputs h33 h34) - (hP_interlaces := hP_interlaces) (hG := hG) - (hP_one := hP_one) (hG_one := hG_one) - (hP_nonneg := hP_nonneg) (hG_nonneg := hG_nonneg) - (hM_nonneg := hM_nonneg) (hdeg := hdeg) (hM_const := hM_const) - -/-- Package the shifted difference-interlacing induction theorem as the abstract route predicate, -with the constant-word branch reduced to the concrete successor-length identity. -/ -theorem snakeInterlacingInductionRoute_of_shiftedDifference_of_constant_matches_succ_length - {M : SnakeWord → ℝ[X]} {P G : ℕ → ℝ[X]} - (hclaim_of_inputs : - AuxiliaryGInterlacesStatement P G → - AffineModifiedNarayanaInterlacingStatement P → - ShiftedDifferenceInterlacingStatement P G) - (hP_interlaces : ∀ n : ℕ, Interlaces (P n) (P (n + 1))) - (hG : ∀ {m : ℕ}, 2 ≤ m → StrictInterl (G (m - 1)) (G m)) - (hP_one : P 1 = 1 + X) (hG_one : G 1 = 1) - (hP_nonneg : ∀ n, HasNonnegCoeffs (P n)) - (hG_nonneg : ∀ n, HasNonnegCoeffs (G n)) - (hM_nonneg : ∀ w, HasNonnegCoeffs (M w)) - (hdeg : - ∀ {w : SnakeWord}, 1 ≤ w.length → - (M w.deleteFinal).natDegree + 1 = (M w).natDegree) - (hM_const : ∀ {w : SnakeWord}, w.IsConstant → M w = P (w.length + 1)) : - SnakeInterlacingInductionRouteStatement M P G := by - intro h33 h34 hrec - exact snakeInterlacing_of_shiftedDifferenceInterlacing_of_constant_matches_succ_length - (M := M) (P := P) (G := G) - (hrec := hrec) (hclaim := hclaim_of_inputs h33 h34) - (hP_interlaces := hP_interlaces) (hG := hG) - (hP_one := hP_one) (hG_one := hG_one) - (hP_nonneg := hP_nonneg) (hG_nonneg := hG_nonneg) - (hM_nonneg := hM_nonneg) (hdeg := hdeg) (hM_const := hM_const) - -/-- The auxiliary recurrence plus the local shifted difference-interlacing side conditions give -the abstract induction route, using the concrete successor-length indexing for -constant words. - -The shifted difference interlacing claim itself uses the auxiliary recurrence, the affine Narayana -interlacing lemma, and the bundled side -conditions; the auxiliary interlacing lemma remains part of the route interface but is not consumed -by -this shifted difference-interlacing assembly theorem. -/ -theorem snakeInterlacingInductionRoute_of_combinatorial_of_constant_matches_succ_length - {M : SnakeWord → ℝ[X]} {P G : ℕ → ℝ[X]} - (hrec2 : NarayanaAuxiliaryGRecurrenceStatement P G) - (hside : ShiftedDifferenceInterlacingSideConditions P G) - (hP_interlaces : ∀ n : ℕ, Interlaces (P n) (P (n + 1))) - (hG : ∀ {m : ℕ}, 2 ≤ m → StrictInterl (G (m - 1)) (G m)) - (hP_one : P 1 = 1 + X) (hG_one : G 1 = 1) - (hP_nonneg : ∀ n, HasNonnegCoeffs (P n)) - (hG_nonneg : ∀ n, HasNonnegCoeffs (G n)) - (hM_nonneg : ∀ w, HasNonnegCoeffs (M w)) - (hdeg : - ∀ {w : SnakeWord}, 1 ≤ w.length → - (M w.deleteFinal).natDegree + 1 = (M w).natDegree) - (hM_const : ∀ {w : SnakeWord}, w.IsConstant → M w = P (w.length + 1)) : - SnakeInterlacingInductionRouteStatement M P G := - snakeInterlacingInductionRoute_of_shiftedDifference_of_constant_matches_succ_length - (M := M) (P := P) (G := G) - (fun _h33 h34 => shiftedDifferenceInterlacing_of_combinatorial_sideConditions hrec2 h34 hside) - hP_interlaces hG hP_one hG_one hP_nonneg hG_nonneg hM_nonneg hdeg - hM_const - -/-- Root-sum version of the combinatorial induction route. - -This uses the endpoint-compatible shifted difference-interlacing assembly theorem in place of the -older strict-root-bound route. -/ -theorem snakeInterlacingInductionRoute_of_combinatorial_rootSum_of_constant_matches_succ_length - {M : SnakeWord → ℝ[X]} {P G : ℕ → ℝ[X]} - (hrec2 : NarayanaAuxiliaryGRecurrenceStatement P G) - (hside : ShiftedDifferenceInterlacingRootSumSideConditions P G) - (hP_interlaces : ∀ n : ℕ, Interlaces (P n) (P (n + 1))) - (hG : ∀ {m : ℕ}, 2 ≤ m → StrictInterl (G (m - 1)) (G m)) - (hP_one : P 1 = 1 + X) (hG_one : G 1 = 1) - (hP_nonneg : ∀ n, HasNonnegCoeffs (P n)) - (hG_nonneg : ∀ n, HasNonnegCoeffs (G n)) - (hM_nonneg : ∀ w, HasNonnegCoeffs (M w)) - (hdeg : - ∀ {w : SnakeWord}, 1 ≤ w.length → - (M w.deleteFinal).natDegree + 1 = (M w).natDegree) - (hM_const : ∀ {w : SnakeWord}, w.IsConstant → M w = P (w.length + 1)) : - SnakeInterlacingInductionRouteStatement M P G := - snakeInterlacingInductionRoute_of_shiftedDifference_of_constant_matches_succ_length - (M := M) (P := P) (G := G) - (fun _h33 h34 => - shiftedDifferenceInterlacing_of_combinatorial_rootSumSideConditions hrec2 h34 hside) - hP_interlaces hG hP_one hG_one hP_nonneg hG_nonneg hM_nonneg hdeg - hM_const - end GeneralizedSnakePosets end RealRooted diff --git a/RealRooted/GeneralizedSnakePosets/Narayana/LowRank.lean b/RealRooted/GeneralizedSnakePosets/Narayana/LowRank.lean index 334cc5ca8..212e76d31 100644 --- a/RealRooted/GeneralizedSnakePosets/Narayana/LowRank.lean +++ b/RealRooted/GeneralizedSnakePosets/Narayana/LowRank.lean @@ -825,35 +825,18 @@ theorem auxiliaryGInterlaces_modified_of_le_six_of_crosses · exact auxiliaryGInterlaces_modified_five · exact auxiliaryGInterlaces_modified_six_of_crosses hcross -/-- Conditional checked initial cases `n = 1, 2, 3, 4, 5, 6` of Braun--Jal -the auxiliary interlacing lemma from the single `P_6`/`G_6` sign certificate. -/ -theorem auxiliaryGInterlaces_modified_of_le_six_of_eval_signs - (hsign : ModifiedNarayanaSixAuxiliaryGSignCertificate) - {n : ℕ} (hn₁ : 1 ≤ n) (hn₆ : n ≤ 6) : - StrictInterl (FiniteSkewBoard.auxiliaryG n) (modifiedNarayanaPolynomial n) := - auxiliaryGInterlaces_modified_of_le_six_of_crosses - (fun {a b c d e r} hP_roots hab hbc hcd hde her => - ModifiedNarayanaSixAuxiliaryGCrossInequalities.of_eval_signs - (by simpa [modifiedNarayanaPolynomialSix] using hP_roots) - hab hbc hcd hde her hsign) - hn₁ hn₆ - /-- The checked initial cases `n = 1, 2, 3, 4, 5, 6` of Braun--Jal the auxiliary interlacing lemma, for the concrete modified Narayana family and the finite-board auxiliary `G`. -/ theorem auxiliaryGInterlaces_modified_of_le_six {n : ℕ} (hn₁ : 1 ≤ n) (hn₆ : n ≤ 6) : StrictInterl (FiniteSkewBoard.auxiliaryG n) (modifiedNarayanaPolynomial n) := - auxiliaryGInterlaces_modified_of_le_six_of_eval_signs - modifiedNarayanaPolynomial_six_auxiliaryG_signCertificate hn₁ hn₆ - -/-- The checked initial cases `n = 1, ..., 6` of the auxiliary interlacing lemma, -packaged in the generic bounded interlacing interface. -/ -theorem auxiliaryGInterlaces_modified_upTo_six : - AuxiliaryGInterlacesUpToStatement - modifiedNarayanaPolynomial FiniteSkewBoard.auxiliaryG 6 := by - intro n hn₁ hn₆ - exact auxiliaryGInterlaces_modified_of_le_six hn₁ hn₆ + auxiliaryGInterlaces_modified_of_le_six_of_crosses + (fun {a b c d e r} hP_roots hab hbc hcd hde her => + ModifiedNarayanaSixAuxiliaryGCrossInequalities.of_sorted_roots + (by simpa [modifiedNarayanaPolynomialSix] using hP_roots) + hab hbc hcd hde her) + hn₁ hn₆ end GeneralizedSnakePosets end RealRooted diff --git a/RealRooted/GeneralizedSnakePosets/Narayana/Modified.lean b/RealRooted/GeneralizedSnakePosets/Narayana/Modified.lean index f85801fd5..f6b5f3a88 100644 --- a/RealRooted/GeneralizedSnakePosets/Narayana/Modified.lean +++ b/RealRooted/GeneralizedSnakePosets/Narayana/Modified.lean @@ -65,10 +65,11 @@ theorem modifiedNarayanaPolynomial_posLeadingCoeff (n : ℕ) : simpa [modifiedNarayanaPolynomial] using (narayanaQuot_posLeadingCoeff (n + 1) (by lia)) -/-- The existing Narayana sequence and `modifiedNarayanaPolynomial` satisfy the -Braun--Jal modified-family interface. -/ +/-- `modifiedNarayanaPolynomial` is the Braun--Jal modified Narayana family: +`P_0 = 1` and `N_{n+1} = X * P_n`, i.e. `P_n(t) = t^{-1} N_{n+1}(t)`. -/ theorem modifiedNarayanaFamily_narayana : - ModifiedNarayanaFamilyStatement narayana modifiedNarayanaPolynomial := by + modifiedNarayanaPolynomial 0 = 1 ∧ + ∀ n : ℕ, narayana (n + 1) = X * modifiedNarayanaPolynomial n := by constructor · simp [modifiedNarayanaPolynomial] · intro n diff --git a/RealRooted/GeneralizedSnakePosets/Narayana/PFFacts.lean b/RealRooted/GeneralizedSnakePosets/Narayana/PFFacts.lean index abd0ae305..cf9220bd6 100644 --- a/RealRooted/GeneralizedSnakePosets/Narayana/PFFacts.lean +++ b/RealRooted/GeneralizedSnakePosets/Narayana/PFFacts.lean @@ -76,27 +76,11 @@ theorem affineModifiedNarayanaShiftedInterlacing_modified_zero_one simp rwa [hleft, hright] -/-- Concrete modified-Narayana wrapper: the shifted affine-Narayana target implies -the paper-shaped affine-Narayana target. -/ -theorem affineModifiedNarayanaInterlacing_modified_of_shifted - (h : - AffineModifiedNarayanaShiftedInterlacingStatement - modifiedNarayanaPolynomial) : - AffineModifiedNarayanaInterlacingStatement modifiedNarayanaPolynomial := - affineModifiedNarayanaInterlacing_of_shifted h - -/-- Concrete modified-Narayana wrapper: the paper-shaped affine-Narayana target -implies shifted nonnegative-parameter target. -/ -theorem affineModifiedNarayanaShiftedInterlacing_modified_of_affineNarayana - (h : AffineModifiedNarayanaInterlacingStatement modifiedNarayanaPolynomial) : - AffineModifiedNarayanaShiftedInterlacingStatement - modifiedNarayanaPolynomial := - affineModifiedNarayanaShiftedInterlacing_of_affineNarayana h - -/-- The coefficient-side modified Narayana family also satisfies the -Braun--Jal modified-family interface. -/ +/-- The coefficient-side modified Narayana family also satisfies +`P_0 = 1` and `N_{n+1} = X * P_n`. -/ theorem modifiedNarayanaFamily_coeff : - ModifiedNarayanaFamilyStatement narayana modifiedNarayanaCoeffPolynomial := by + modifiedNarayanaCoeffPolynomial 0 = 1 ∧ + ∀ n : ℕ, narayana (n + 1) = X * modifiedNarayanaCoeffPolynomial n := by constructor · simp · intro n diff --git a/RealRooted/GeneralizedSnakePosets/Narayana/RankSix.lean b/RealRooted/GeneralizedSnakePosets/Narayana/RankSix.lean index 05fb295a0..dd0579c51 100644 --- a/RealRooted/GeneralizedSnakePosets/Narayana/RankSix.lean +++ b/RealRooted/GeneralizedSnakePosets/Narayana/RankSix.lean @@ -422,14 +422,6 @@ theorem auxiliaryG_six_root4_qPlus : dsimp [auxiliaryG_six_root4, s, α] at * linarith -/-- The sign pattern of `P_6` at the named `G_6` roots. -/ -def ModifiedNarayanaSixAuxiliaryGSignCertificate : Prop := - modifiedNarayanaPolynomialSix.eval auxiliaryG_six_root0 < 0 ∧ - 0 < modifiedNarayanaPolynomialSix.eval auxiliaryG_six_root1 ∧ - modifiedNarayanaPolynomialSix.eval auxiliaryG_six_root2 < 0 ∧ - 0 < modifiedNarayanaPolynomialSix.eval auxiliaryG_six_root3 ∧ - modifiedNarayanaPolynomialSix.eval auxiliaryG_six_root4 < 0 - /-- `P_6` is negative at the first named `G_6` root. -/ theorem modifiedNarayanaPolynomial_six_eval_root0_neg : modifiedNarayanaPolynomialSix.eval auxiliaryG_six_root0 < 0 := by @@ -595,37 +587,28 @@ theorem modifiedNarayanaPolynomial_six_eval_root4_neg : rwa [modifiedNarayanaPolynomial_six_eval_of_qPlus_root hs_sq hroot4] linarith -/-- The concrete sign pattern of `P_6` at the five named `G_6` roots. -/ -theorem modifiedNarayanaPolynomial_six_auxiliaryG_signCertificate : - ModifiedNarayanaSixAuxiliaryGSignCertificate := - ⟨modifiedNarayanaPolynomial_six_eval_root0_neg, - modifiedNarayanaPolynomial_six_eval_root1_pos, - modifiedNarayanaPolynomial_six_eval_root2_neg, - modifiedNarayanaPolynomial_six_eval_root3_pos, - modifiedNarayanaPolynomial_six_eval_root4_neg⟩ - -/-- The roots of `P_6` are isolated across the five named `G_6` roots. -/ -def ModifiedNarayanaSixAuxiliaryGRootIntervalCertificate : Prop := - ∃ x0 x1 x2 x3 x4 x5 : ℝ, - modifiedNarayanaPolynomialSix.IsRoot x0 ∧ - x0 < auxiliaryG_six_root0 ∧ - modifiedNarayanaPolynomialSix.IsRoot x1 ∧ - auxiliaryG_six_root0 < x1 ∧ x1 < auxiliaryG_six_root1 ∧ - modifiedNarayanaPolynomialSix.IsRoot x2 ∧ - auxiliaryG_six_root1 < x2 ∧ x2 < auxiliaryG_six_root2 ∧ - modifiedNarayanaPolynomialSix.IsRoot x3 ∧ - auxiliaryG_six_root2 < x3 ∧ x3 < auxiliaryG_six_root3 ∧ - modifiedNarayanaPolynomialSix.IsRoot x4 ∧ - auxiliaryG_six_root3 < x4 ∧ x4 < auxiliaryG_six_root4 ∧ - modifiedNarayanaPolynomialSix.IsRoot x5 ∧ - auxiliaryG_six_root4 < x5 - -/-- Sign alternation of `P_6` across the named `G_6` roots gives one `P_6` -root in each complementary interval. -/ -theorem modifiedNarayanaPolynomial_six_rootIntervals_of_eval_signs - (hsign : ModifiedNarayanaSixAuxiliaryGSignCertificate) : - ModifiedNarayanaSixAuxiliaryGRootIntervalCertificate := by - rcases hsign with ⟨h0, h1, h2, h3, h4⟩ +/-- The roots of `P_6` are isolated across the five named `G_6` roots: the +sign alternation of `P_6` at those roots gives one `P_6` root in each +complementary interval. -/ +theorem modifiedNarayanaPolynomial_six_rootIntervals : + ∃ x0 x1 x2 x3 x4 x5 : ℝ, + modifiedNarayanaPolynomialSix.IsRoot x0 ∧ + x0 < auxiliaryG_six_root0 ∧ + modifiedNarayanaPolynomialSix.IsRoot x1 ∧ + auxiliaryG_six_root0 < x1 ∧ x1 < auxiliaryG_six_root1 ∧ + modifiedNarayanaPolynomialSix.IsRoot x2 ∧ + auxiliaryG_six_root1 < x2 ∧ x2 < auxiliaryG_six_root2 ∧ + modifiedNarayanaPolynomialSix.IsRoot x3 ∧ + auxiliaryG_six_root2 < x3 ∧ x3 < auxiliaryG_six_root3 ∧ + modifiedNarayanaPolynomialSix.IsRoot x4 ∧ + auxiliaryG_six_root3 < x4 ∧ x4 < auxiliaryG_six_root4 ∧ + modifiedNarayanaPolynomialSix.IsRoot x5 ∧ + auxiliaryG_six_root4 < x5 := by + have h0 := modifiedNarayanaPolynomial_six_eval_root0_neg + have h1 := modifiedNarayanaPolynomial_six_eval_root1_pos + have h2 := modifiedNarayanaPolynomial_six_eval_root2_neg + have h3 := modifiedNarayanaPolynomial_six_eval_root3_pos + have h4 := modifiedNarayanaPolynomial_six_eval_root4_neg rcases auxiliaryG_six_root_order_named with ⟨h01, h12, h23, h34⟩ have hP_pos : HasPosLeadingCoeff modifiedNarayanaPolynomialSix := by simpa [modifiedNarayanaPolynomialSix] using modifiedNarayanaPolynomial_posLeadingCoeff 6 @@ -730,16 +713,15 @@ def ModifiedNarayanaSixAuxiliaryGCrossInequalities /-- Six interval-isolated `P_6` roots determine the cross-root inequalities against any sorted `P_6` root list. -/ -theorem ModifiedNarayanaSixAuxiliaryGCrossInequalities.of_rootIntervals +theorem ModifiedNarayanaSixAuxiliaryGCrossInequalities.of_sorted_roots {a b c d e r : ℝ} (hP_roots : modifiedNarayanaPolynomialSix.roots = (↑[a, b, c, d, e, r] : Multiset ℝ)) (hab : a ≤ b) (hbc : b ≤ c) (hcd : c ≤ d) (hde : d ≤ e) - (her : e ≤ r) - (hintervals : ModifiedNarayanaSixAuxiliaryGRootIntervalCertificate) : + (her : e ≤ r) : ModifiedNarayanaSixAuxiliaryGCrossInequalities a b c d e r := by - rcases hintervals with + rcases modifiedNarayanaPolynomial_six_rootIntervals with ⟨x0, x1, x2, x3, x4, x5, hx0_root, hx0_lt, hx1_root, hx01, hx1_lt, hx2_root, hx12, hx2_lt, hx3_root, hx23, hx3_lt, hx4_root, hx34, hx4_lt, hx5_root, hx45⟩ @@ -819,21 +801,6 @@ theorem ModifiedNarayanaSixAuxiliaryGCrossInequalities.of_rootIntervals le_of_lt hx2_lt, le_of_lt hx23, le_of_lt hx3_lt, le_of_lt hx34, le_of_lt hx4_lt, le_of_lt hx45⟩ -/-- The `P_6`/`G_6` sign certificate gives the cross-root inequalities against -any sorted `P_6` root list. -/ -theorem ModifiedNarayanaSixAuxiliaryGCrossInequalities.of_eval_signs - {a b c d e r : ℝ} - (hP_roots : - modifiedNarayanaPolynomialSix.roots = - (↑[a, b, c, d, e, r] : Multiset ℝ)) - (hab : a ≤ b) (hbc : b ≤ c) (hcd : c ≤ d) (hde : d ≤ e) - (her : e ≤ r) - (hsign : ModifiedNarayanaSixAuxiliaryGSignCertificate) : - ModifiedNarayanaSixAuxiliaryGCrossInequalities a b c d e r := - ModifiedNarayanaSixAuxiliaryGCrossInequalities.of_rootIntervals - hP_roots hab hbc hcd hde her - (modifiedNarayanaPolynomial_six_rootIntervals_of_eval_signs hsign) - /-- Conditional `n = 6` auxiliary-interlacing certificate, reducing the remaining work to the `P_6` root list and cross inequalities. -/ theorem auxiliaryGInterlaces_modified_six_interlaces_of_roots @@ -900,22 +867,14 @@ theorem auxiliaryGInterlaces_modified_six_of_crosses StrictInterl (FiniteSkewBoard.auxiliaryG 6) (modifiedNarayanaPolynomial 6) := (auxiliaryGInterlaces_modified_six_interlaces_of_crosses hcross).toStrictInterl -/-- The `n = 6` auxiliary-interlacing follows from the -`P_6`/`G_6` sign certificate. -/ -theorem auxiliaryGInterlaces_modified_six_interlaces_of_eval_signs - (hsign : ModifiedNarayanaSixAuxiliaryGSignCertificate) : +/-- The checked `n = 6` auxiliary-interlacing case. -/ +theorem auxiliaryGInterlaces_modified_six_interlaces : Interlaces (FiniteSkewBoard.auxiliaryG 6) (modifiedNarayanaPolynomial 6) := by apply auxiliaryGInterlaces_modified_six_interlaces_of_crosses intro a b c d e r hP_roots hab hbc hcd hde her - exact ModifiedNarayanaSixAuxiliaryGCrossInequalities.of_eval_signs + exact ModifiedNarayanaSixAuxiliaryGCrossInequalities.of_sorted_roots (by simpa [modifiedNarayanaPolynomialSix] using hP_roots) - hab hbc hcd hde her hsign - -/-- The checked `n = 6` auxiliary-interlacing case. -/ -theorem auxiliaryGInterlaces_modified_six_interlaces : - Interlaces (FiniteSkewBoard.auxiliaryG 6) (modifiedNarayanaPolynomial 6) := - auxiliaryGInterlaces_modified_six_interlaces_of_eval_signs - modifiedNarayanaPolynomial_six_auxiliaryG_signCertificate + hab hbc hcd hde her /-- The checked `n = 6` auxiliary-interlacing case. -/ theorem auxiliaryGInterlaces_modified_six : diff --git a/RealRooted/GeneralizedSnakePosets/Narayana/Recurrence.lean b/RealRooted/GeneralizedSnakePosets/Narayana/Recurrence.lean index 0b3d4cb10..952a2e238 100644 --- a/RealRooted/GeneralizedSnakePosets/Narayana/Recurrence.lean +++ b/RealRooted/GeneralizedSnakePosets/Narayana/Recurrence.lean @@ -336,14 +336,6 @@ theorem narayanaAuxiliaryGRecurrence_modified_of_le_eight · exact narayanaAuxiliaryGRecurrence_modified_seven · exact narayanaAuxiliaryGRecurrence_modified_eight -/-- The checked initial cases `n = 1, ..., 8` of the auxiliary recurrence, -packaged in the generic bounded recurrence interface. -/ -theorem narayanaAuxiliaryGRecurrence_modified_upTo_eight : - NarayanaAuxiliaryGRecurrenceUpToStatement - modifiedNarayanaPolynomial FiniteSkewBoard.auxiliaryG 8 := by - intro n hn₁ hn₈ - exact narayanaAuxiliaryGRecurrence_modified_of_le_eight hn₁ hn₈ - /-- Unconditional consecutive interlacing for the modified Narayana family. -/ theorem modifiedNarayanaPolynomial_strictInterl_succ (n : ℕ) : diff --git a/RealRooted/GeneralizedSnakePosets/Narayana/RootSums.lean b/RealRooted/GeneralizedSnakePosets/Narayana/RootSums.lean index 1ae35ab64..001f9ba71 100644 --- a/RealRooted/GeneralizedSnakePosets/Narayana/RootSums.lean +++ b/RealRooted/GeneralizedSnakePosets/Narayana/RootSums.lean @@ -4,9 +4,9 @@ import RealRooted.GeneralizedSnakePosets.Narayana.Recurrence /-! # Modified-Narayana root-sum orientation -This module derives the Vieta/root-sum comparison used in the shifted difference interlacing claim, -packages the corresponding induction routes, and records the obstruction to -the older uniformly strict root-bound interface. +This module derives the Vieta/root-sum comparison used in the shifted difference interlacing claim +and records the obstruction to a uniformly strict negative root bound at the +endpoint `ν = -1`. -/ open Polynomial Filter @@ -16,39 +16,6 @@ noncomputable section namespace RealRooted namespace GeneralizedSnakePosets -/-- Concrete modified-Narayana/auxiliary-`G` route for the snake interlacing theorem. - -This discharges the standard modified-Narayana facts and the elementary -auxiliary-`G` facts from the generic combinatorial route. The remaining hypotheses -are the all-`n` auxiliary recurrence, the shifted difference-interlacing side conditions, adjacent -interlacing of the auxiliary `G` column, and the word-family side conditions. --/ -theorem snakeInterlacingInductionRoute_modified_of_combinatorial_of_constant_matches_succ_length - {M : SnakeWord → ℝ[X]} - (hrec2 : - NarayanaAuxiliaryGRecurrenceStatement - modifiedNarayanaPolynomial FiniteSkewBoard.auxiliaryG) - (hside : - ShiftedDifferenceInterlacingSideConditions - modifiedNarayanaPolynomial FiniteSkewBoard.auxiliaryG) - (hG : ∀ {m : ℕ}, 2 ≤ m → - StrictInterl (FiniteSkewBoard.auxiliaryG (m - 1)) (FiniteSkewBoard.auxiliaryG m)) - (hM_nonneg : ∀ w, HasNonnegCoeffs (M w)) - (hdeg : - ∀ {w : SnakeWord}, 1 ≤ w.length → - (M w.deleteFinal).natDegree + 1 = (M w).natDegree) - (hM_const : - ∀ {w : SnakeWord}, w.IsConstant → - M w = modifiedNarayanaPolynomial (w.length + 1)) : - SnakeInterlacingInductionRouteStatement - M modifiedNarayanaPolynomial FiniteSkewBoard.auxiliaryG := - snakeInterlacingInductionRoute_of_combinatorial_of_constant_matches_succ_length - (M := M) (P := modifiedNarayanaPolynomial) (G := FiniteSkewBoard.auxiliaryG) - hrec2 hside modifiedNarayanaPolynomial_interlaces_succ hG - modifiedNarayanaPolynomial_one FiniteSkewBoard.auxiliaryG_one - modifiedNarayanaPolynomial_hasNonnegCoeffs - FiniteSkewBoard.auxiliaryG_hasNonnegCoeffs hM_nonneg hdeg hM_const - /-- Arithmetic comparison between the Vieta expressions predicted by the leading and next coefficients of the modified-Narayana `U` window and the auxiliary-`G` `V` window. -/ @@ -475,17 +442,5 @@ theorem shiftedDifferenceInterlacing_modified_left_boundary_not_strictRootBound have hzero_le : (0 : ℝ) ≤ c := hle 0 hzero_mem linarith -/-- Consequently, the current bundled shifted difference-interlacing side-condition interface is -not satisfiable by the concrete modified-Narayana / auxiliary-`G` data. The -endpoint `ν = -1` needs a refined conversion route instead of a uniform strict -negative bound on the roots of `U`. -/ -theorem not_shiftedDifferenceInterlacingSideConditions_modified_auxiliaryG : - ¬ ShiftedDifferenceInterlacingSideConditions - modifiedNarayanaPolynomial FiniteSkewBoard.auxiliaryG := by - intro hside - exact shiftedDifferenceInterlacing_modified_left_boundary_not_strictRootBound - (hside.u_bound (m := 2) (lam := 0) (nu := -1) - (by norm_num) (by norm_num) (by norm_num)) - end GeneralizedSnakePosets end RealRooted diff --git a/RealRooted/GeneralizedSnakePosets/Narayana/ShiftedDifferenceInterlacing.lean b/RealRooted/GeneralizedSnakePosets/Narayana/ShiftedDifferenceInterlacing.lean index d4e8dc2de..c565828f2 100644 --- a/RealRooted/GeneralizedSnakePosets/Narayana/ShiftedDifferenceInterlacing.lean +++ b/RealRooted/GeneralizedSnakePosets/Narayana/ShiftedDifferenceInterlacing.lean @@ -79,10 +79,9 @@ theorem auxiliaryGInterlaces_modified (hH_nonneg : ∀ n : ℕ, 1 ≤ n → HasNonnegCoeffs (FiniteSkewBoard.auxiliaryG n - - FiniteSkewBoard.auxiliaryG (n - 1))) : - AuxiliaryGInterlacesStatement - modifiedNarayanaPolynomial FiniteSkewBoard.auxiliaryG := by - intro n hn + FiniteSkewBoard.auxiliaryG (n - 1))) + {n : ℕ} (hn : 1 ≤ n) : + StrictInterl (FiniteSkewBoard.auxiliaryG n) (modifiedNarayanaPolynomial n) := by rcases eq_or_lt_of_le hn with h | hn · subst n exact auxiliaryGInterlaces_modified_base @@ -125,37 +124,6 @@ theorem auxiliaryG_posComboRealRooted_of_narayanaRecurrence exact ⟨mul_ne_zero (by simpa using hmu_ne) hV_pos.ne_zero, hV_split.C_mul mu⟩ -/-- The Braun--Jal induction route for the concrete modified Narayana data. - -The recurrence `hrec2` and difference nonnegativity `hH_nonneg` are the -explicit combinatorial inputs described at `shiftedDifferenceInterlacing_modified`. The -remaining hypotheses are genuine properties of the chosen snake-polynomial -model and the auxiliary family; none assumes the induction-route conclusion. -/ -theorem snakeInterlacingInductionRoute_modified_of_modelInputs - {M : SnakeWord → ℝ[X]} - (hrec2 : NarayanaAuxiliaryGRecurrenceStatement - modifiedNarayanaPolynomial FiniteSkewBoard.auxiliaryG) - (hH_nonneg : ∀ n : ℕ, 1 ≤ n → - HasNonnegCoeffs - (FiniteSkewBoard.auxiliaryG n - - FiniteSkewBoard.auxiliaryG (n - 1))) - (hG : ∀ {m : ℕ}, 2 ≤ m → - StrictInterl (FiniteSkewBoard.auxiliaryG (m - 1)) - (FiniteSkewBoard.auxiliaryG m)) - (hM_nonneg : ∀ w : SnakeWord, HasNonnegCoeffs (M w)) - (hdeg : ∀ {w : SnakeWord}, 1 ≤ w.length → - (M w.deleteFinal).natDegree + 1 = (M w).natDegree) - (hM_const : ∀ {w : SnakeWord}, w.IsConstant → - M w = modifiedNarayanaPolynomial (w.length + 1)) : - SnakeInterlacingInductionRouteStatement M modifiedNarayanaPolynomial - FiniteSkewBoard.auxiliaryG := - snakeInterlacingInductionRoute_of_shiftedDifference_of_constant_matches_succ_length - (fun _h33 _h34 => shiftedDifferenceInterlacing_modified hrec2 hH_nonneg) - modifiedNarayanaPolynomial_interlaces_succ hG - modifiedNarayanaPolynomial_one FiniteSkewBoard.auxiliaryG_one - modifiedNarayanaPolynomial_hasNonnegCoeffs - FiniteSkewBoard.auxiliaryG_hasNonnegCoeffs hM_nonneg hdeg hM_const - private theorem strictInterl_narayanaPolynomial_two (n : ℕ) : StrictInterl (narayanaPolynomial 2 n) (narayanaPolynomial 2 (n + 1)) := by cases n with @@ -192,38 +160,6 @@ theorem auxiliaryG_strictInterl_succ_of_narayanaTwoModel have hright : m - 2 + 1 = m - 1 := by lia simpa [hleft, hright] using hscaled -/-- Concrete the snake-interlacing checkpoint with its proof boundary made explicit. -The recurrence, coefficient nonnegativity, word recurrence, degree, and -constant-word hypotheses are combinatorial model inputs, so accepting them is -consistent with the scope documented above. In contrast, `hG` is an analytic -premise still to be proved (or removed by a sharper matrix argument); this -theorem isolates that sole remaining analytic boundary rather than claiming -the final result unconditionally. -/ -theorem nonNestingRookInterlacing_modified_of_modelInputs_of_adjacentG - {M : SnakeWord → ℝ[X]} - (hrec2 : NarayanaAuxiliaryGRecurrenceStatement - modifiedNarayanaPolynomial FiniteSkewBoard.auxiliaryG) - (hH_nonneg : ∀ n : ℕ, 1 ≤ n → - HasNonnegCoeffs - (FiniteSkewBoard.auxiliaryG n - - FiniteSkewBoard.auxiliaryG (n - 1))) - (hG : ∀ {m : ℕ}, 2 ≤ m → - StrictInterl (FiniteSkewBoard.auxiliaryG (m - 1)) - (FiniteSkewBoard.auxiliaryG m)) - (hrec : GeneralizedSnakeRecurrenceStatement M - modifiedNarayanaPolynomial FiniteSkewBoard.auxiliaryG) - (hM_nonneg : ∀ w : SnakeWord, HasNonnegCoeffs (M w)) - (hdeg : ∀ {w : SnakeWord}, 1 ≤ w.length → - (M w.deleteFinal).natDegree + 1 = (M w).natDegree) - (hM_const : ∀ {w : SnakeWord}, w.IsConstant → - M w = modifiedNarayanaPolynomial (w.length + 1)) : - NonNestingRookInterlacingStatement M := by - exact - (snakeInterlacingInductionRoute_modified_of_modelInputs hrec2 hH_nonneg hG - hM_nonneg hdeg hM_const) - (auxiliaryGInterlaces_modified hrec2 hH_nonneg) - affineModifiedNarayanaInterlacing_modified hrec - /-- Snake-interlacing through the source `[P, G; Q, H]` matrix. The hypotheses are the intended combinatorial trust boundary. The auxiliary recurrence, @@ -263,35 +199,5 @@ theorem nonNestingRookInterlacing_modified_of_sourceInputs simpa [auxiliaryDifference] using hH_nonneg _ (by lia)) hM_nonneg hdeg hM_const -/-- An alternative snake-interlacing endpoint using the additional generalized -Narayana identity `hG_model`. - -Braun--Jal do not use or state this identity in their proof. The source-faithful -route goes through the `[P, G; Q, H]` matrix and the difference interlacing claim, so this result -must -not be presented as depending only on the paper's combinatorial boundary facts. -It remains useful when `hG_model` is independently established. -/ -theorem nonNestingRookInterlacing_modified_of_modelInputs - {M : SnakeWord → ℝ[X]} - (hrec2 : NarayanaAuxiliaryGRecurrenceStatement - modifiedNarayanaPolynomial FiniteSkewBoard.auxiliaryG) - (hH_nonneg : ∀ n : ℕ, 1 ≤ n → - HasNonnegCoeffs - (FiniteSkewBoard.auxiliaryG n - - FiniteSkewBoard.auxiliaryG (n - 1))) - (hG_model : ∀ n : ℕ, 1 ≤ n → - FiniteSkewBoard.auxiliaryG n = - C (n : ℝ) * narayanaPolynomial 2 (n - 1)) - (hrec : GeneralizedSnakeRecurrenceStatement M - modifiedNarayanaPolynomial FiniteSkewBoard.auxiliaryG) - (hM_nonneg : ∀ w : SnakeWord, HasNonnegCoeffs (M w)) - (hdeg : ∀ {w : SnakeWord}, 1 ≤ w.length → - (M w.deleteFinal).natDegree + 1 = (M w).natDegree) - (hM_const : ∀ {w : SnakeWord}, w.IsConstant → - M w = modifiedNarayanaPolynomial (w.length + 1)) : - NonNestingRookInterlacingStatement M := - nonNestingRookInterlacing_modified_of_modelInputs_of_adjacentG hrec2 hH_nonneg - (auxiliaryG_strictInterl_succ_of_narayanaTwoModel hG_model) hrec hM_nonneg hdeg hM_const - end GeneralizedSnakePosets end RealRooted diff --git a/RealRooted/GeneralizedSnakePosets/Narayana/Turan.lean b/RealRooted/GeneralizedSnakePosets/Narayana/Turan.lean index 447af0e52..713451162 100644 --- a/RealRooted/GeneralizedSnakePosets/Narayana/Turan.lean +++ b/RealRooted/GeneralizedSnakePosets/Narayana/Turan.lean @@ -3,9 +3,10 @@ import RealRooted.GeneralizedSnakePosets.Narayana.JacobiTransport /-! # Certificate-free Turan API for modified Narayana polynomials -This module contains the reusable Turan determinant statements and the -hypothesis-taking bridge lemmas for the affine Narayana interlacing lemma. Explicit finite -certificates live in `RealRooted.GeneralizedSnakePosets.Narayana.TuranCertificates`. +This module proves the modified Narayana Turan inequality on nonpositive +inputs and uses it for the affine Narayana interlacing lemma. Explicit +finite-range determinants live in +`RealRooted.GeneralizedSnakePosets.Narayana.TuranCertificates`. -/ open Polynomial @@ -111,26 +112,6 @@ theorem modifiedNarayanaTuran_eq_scale_mul_jacobi11NormalizedTuran rw [← e0, ← e1, ← e2] ring -/-- Statement form for the remaining Narayana Turan inequality needed by the -shifted affine-Narayana route. -/ -def ModifiedNarayanaTuranNonnegOnNonposStatement : Prop := - ∀ {m : ℕ} {r : ℝ}, 1 ≤ m → r ≤ 0 → 0 ≤ modifiedNarayanaTuran m r - -/-- The normalized Jacobi Turan inequality on `[-1, 1]` gives the modified -Narayana Turan inequality on nonpositive inputs through the Braun--Jal change -of variables. -/ -theorem modifiedNarayanaTuranNonnegOnNonpos_of_jacobi11NormalizedTuran - (hjacobi : ∀ {m : ℕ} {x : ℝ}, 1 ≤ m → x ∈ Set.Icc (-1 : ℝ) 1 → - 0 ≤ ((jacobi11NormalizedPolynomial m).eval x) ^ 2 - - (jacobi11NormalizedPolynomial (m + 1)).eval x * - (jacobi11NormalizedPolynomial (m - 1)).eval x) : - ModifiedNarayanaTuranNonnegOnNonposStatement := by - intro m r hm hr - have hr_ne : r ≠ 1 := by linarith - rw [modifiedNarayanaTuran_eq_scale_mul_jacobi11NormalizedTuran hm hr_ne] - exact mul_nonneg (jacobi11TuranScale_nonneg m r) - (hjacobi hm (jacobi11ChangeOfVariables_mem_Icc_of_nonpos hr)) - /-- Modified Narayana Turan determinants are nonnegative on nonpositive inputs. -/ theorem modifiedNarayanaTuran_nonneg_of_nonpos @@ -152,12 +133,6 @@ theorem modifiedNarayanaTuran_nonneg_of_nonpos (mul_nonneg (by linarith) (sq_nonneg _)) · positivity -/-- The all-`m` Narayana Turan package needed by the shifted affine-Narayana route. -/ -theorem modifiedNarayanaTuranNonnegOnNonpos : - ModifiedNarayanaTuranNonnegOnNonposStatement := by - intro m r hm hr - exact modifiedNarayanaTuran_nonneg_of_nonpos hm hr - /-- The normalized `R_n^(1,1)` Jacobi Turan inequality on `[-1, 1]`. -/ theorem jacobi11NormalizedTuran_nonneg_of_mem_Icc {m : ℕ} (hm : 1 ≤ m) {x : ℝ} (hx : x ∈ Set.Icc (-1 : ℝ) 1) : @@ -181,19 +156,6 @@ theorem jacobi11NormalizedTuran_nonneg_of_mem_Icc simpa [pow_mul] using pow_pos hsq m exact nonneg_of_mul_nonneg_right hmod hscale_pos -/-- Bounded statement form for the Narayana Turan inequality. This records -finite checkpoints while the all-`m` nonpositive-input proof is being built. -/ -def ModifiedNarayanaTuranNonnegOnNonposUpToStatement (N : ℕ) : Prop := - ∀ {m : ℕ} {r : ℝ}, 1 ≤ m → m ≤ N → r ≤ 0 → - 0 ≤ modifiedNarayanaTuran m r - -/-- The all-`m` Turan inequality implies every bounded Turan package. -/ -theorem modifiedNarayanaTuranNonnegOnNonposUpTo_of_statement - (hT : ModifiedNarayanaTuranNonnegOnNonposStatement) (N : ℕ) : - ModifiedNarayanaTuranNonnegOnNonposUpToStatement N := by - intro m r hm _hmN hr - exact hT hm hr - /-- At a root of the shifted affine-Narayana left-hand polynomial, the right-hand polynomial sign test is exactly the negative Narayana Turan determinant. -/ theorem affineModifiedNarayanaShifted_right_eval_mul_prev_eq_neg_turan @@ -238,33 +200,17 @@ theorem affineModifiedNarayanaShifted_right_eval_mul_prev_nonpos_of_turan /-- The global nonpositive-input Turan inequality gives the shifted affine-Narayana right-hand sign test at roots of the left-hand polynomial. -/ -theorem affineModifiedNarayanaShifted_right_eval_mul_prev_nonpos_of_turanNonneg +theorem affineModifiedNarayanaShifted_right_eval_mul_prev_nonpos {m : ℕ} {lam mu r : ℝ} (hm : 1 ≤ m) (hlam : 0 ≤ lam) (hmu : 0 ≤ mu) - (hT : ModifiedNarayanaTuranNonnegOnNonposStatement) (hr : (((C lam * X + C mu) * modifiedNarayanaPolynomial (m - 1) + narayanaDifference modifiedNarayanaPolynomial m).IsRoot r)) : (((C lam * X + C mu) * modifiedNarayanaPolynomial m + narayanaDifference modifiedNarayanaPolynomial (m + 1)).eval r) * (modifiedNarayanaPolynomial (m - 1)).eval r ≤ 0 := affineModifiedNarayanaShifted_right_eval_mul_prev_nonpos_of_turan hr - (hT hm (affineModifiedNarayanaShifted_left_isRoot_nonpos hm hlam hmu - (affineModifiedNarayanaShifted_left_ne_zero hm hlam hmu) r hr)) - -/-- A bounded nonpositive-input Turan package gives the shifted affine-Narayana -right-hand sign test in that range. -/ -theorem - affineModifiedNarayanaShifted_right_eval_mul_prev_nonpos_of_turanNonnegUpTo - {N m : ℕ} {lam mu r : ℝ} (hm : 1 ≤ m) (hmN : m ≤ N) - (hlam : 0 ≤ lam) (hmu : 0 ≤ mu) - (hT : ModifiedNarayanaTuranNonnegOnNonposUpToStatement N) - (hr : (((C lam * X + C mu) * modifiedNarayanaPolynomial (m - 1) + - narayanaDifference modifiedNarayanaPolynomial m).IsRoot r)) : - (((C lam * X + C mu) * modifiedNarayanaPolynomial m + - narayanaDifference modifiedNarayanaPolynomial (m + 1)).eval r) * - (modifiedNarayanaPolynomial (m - 1)).eval r ≤ 0 := - affineModifiedNarayanaShifted_right_eval_mul_prev_nonpos_of_turan hr - (hT hm hmN (affineModifiedNarayanaShifted_left_isRoot_nonpos hm hlam hmu - (affineModifiedNarayanaShifted_left_ne_zero hm hlam hmu) r hr)) + (modifiedNarayanaTuran_nonneg_of_nonpos hm + (affineModifiedNarayanaShifted_left_isRoot_nonpos hm hlam hmu + (affineModifiedNarayanaShifted_left_ne_zero hm hlam hmu) r hr)) /-- At a root of the paper-shaped affine-Narayana left-hand polynomial, the right-hand sign test is exactly the negative Narayana Turan determinant. -/ @@ -308,30 +254,16 @@ theorem affineModifiedNarayana_right_eval_mul_prev_nonpos_of_turan /-- The global nonpositive-input Turan inequality gives the paper-shaped the affine-Narayana right-hand sign test at roots of the left-hand polynomial. -/ -theorem affineModifiedNarayana_right_eval_mul_prev_nonpos_of_turanNonneg +theorem affineModifiedNarayana_right_eval_mul_prev_nonpos {m : ℕ} {lam nu r : ℝ} (hm : 1 ≤ m) (hlam : 0 ≤ lam) (hnu : -1 ≤ nu) - (hT : ModifiedNarayanaTuranNonnegOnNonposStatement) - (hr : (((C lam * X + C nu) * modifiedNarayanaPolynomial (m - 1) + - modifiedNarayanaPolynomial m).IsRoot r)) : - (((C lam * X + C nu) * modifiedNarayanaPolynomial m + - modifiedNarayanaPolynomial (m + 1)).eval r) * - (modifiedNarayanaPolynomial (m - 1)).eval r ≤ 0 := - affineModifiedNarayana_right_eval_mul_prev_nonpos_of_turan hr - (hT hm (affineModifiedNarayana_left_isRoot_nonpos hm hlam hnu hr)) - -/-- A bounded nonpositive-input Turan package gives the paper-shaped affine-Narayana -right-hand sign test in that range. -/ -theorem affineModifiedNarayana_right_eval_mul_prev_nonpos_of_turanNonnegUpTo - {N m : ℕ} {lam nu r : ℝ} (hm : 1 ≤ m) (hmN : m ≤ N) - (hlam : 0 ≤ lam) (hnu : -1 ≤ nu) - (hT : ModifiedNarayanaTuranNonnegOnNonposUpToStatement N) (hr : (((C lam * X + C nu) * modifiedNarayanaPolynomial (m - 1) + modifiedNarayanaPolynomial m).IsRoot r)) : (((C lam * X + C nu) * modifiedNarayanaPolynomial m + modifiedNarayanaPolynomial (m + 1)).eval r) * (modifiedNarayanaPolynomial (m - 1)).eval r ≤ 0 := affineModifiedNarayana_right_eval_mul_prev_nonpos_of_turan hr - (hT hm hmN (affineModifiedNarayana_left_isRoot_nonpos hm hlam hnu hr)) + (modifiedNarayanaTuran_nonneg_of_nonpos hm + (affineModifiedNarayana_left_isRoot_nonpos hm hlam hnu hr)) /-- The affine Narayana interlacing lemma in shifted nonnegative-parameter form for the modified Narayana family. -/ @@ -367,8 +299,8 @@ theorem affineModifiedNarayanaShiftedInterlacing_modified : affineModifiedNarayanaShifted_right_natDegree hlam hmu] · intro r hr exact - affineModifiedNarayanaShifted_right_eval_mul_prev_nonpos_of_turanNonneg - hm1 hlam hmu modifiedNarayanaTuranNonnegOnNonpos hr + affineModifiedNarayanaShifted_right_eval_mul_prev_nonpos + hm1 hlam hmu hr /-- The affine Narayana interlacing lemma in the paper's `ν ≥ -1` form for the modified Narayana family. -/ diff --git a/RealRooted/GeneralizedSnakePosets/Narayana/TuranCertificates.lean b/RealRooted/GeneralizedSnakePosets/Narayana/TuranCertificates.lean index 5b6f198f7..0f2b34afe 100644 --- a/RealRooted/GeneralizedSnakePosets/Narayana/TuranCertificates.lean +++ b/RealRooted/GeneralizedSnakePosets/Narayana/TuranCertificates.lean @@ -3,8 +3,9 @@ import RealRooted.GeneralizedSnakePosets.Narayana.Turan /-! # Finite Turan certificates for modified Narayana polynomials -This module contains the explicit checked finite-range Narayana Turan -certificates used while the all-`m` analytic proof is being formalized. +This module contains explicit finite-range Narayana Turan determinants and +their nonnegativity on nonpositive inputs. The all-`m` inequality is +`modifiedNarayanaTuran_nonneg_of_nonpos`. -/ open Polynomial @@ -513,12 +514,6 @@ theorem modifiedNarayanaTuran_nonneg_of_le_three exact mul_nonneg (by linarith) (modifiedNarayanaTuran_three_factor_nonneg_of_nonpos hr) -/-- Bounded Turan package through `m = 3`. -/ -theorem modifiedNarayanaTuranNonnegOnNonpos_upTo_three : - ModifiedNarayanaTuranNonnegOnNonposUpToStatement 3 := by - intro m r hm₁ hm₃ hr - exact modifiedNarayanaTuran_nonneg_of_le_three hm₁ hm₃ hr - /-- The first four Narayana Turan inequalities on nonpositive inputs. -/ theorem modifiedNarayanaTuran_nonneg_of_le_four {m : ℕ} {r : ℝ} (hm₁ : 1 ≤ m) (hm₄ : m ≤ 4) (hr : r ≤ 0) : @@ -534,12 +529,6 @@ theorem modifiedNarayanaTuran_nonneg_of_le_four · rw [modifiedNarayanaTuran_four] exact mul_nonneg (by linarith) (modifiedNarayanaTuran_four_factor_nonneg r) -/-- Bounded Turan package through `m = 4`. -/ -theorem modifiedNarayanaTuranNonnegOnNonpos_upTo_four : - ModifiedNarayanaTuranNonnegOnNonposUpToStatement 4 := by - intro m r hm₁ hm₄ hr - exact modifiedNarayanaTuran_nonneg_of_le_four hm₁ hm₄ hr - /-- The first five Narayana Turan inequalities on nonpositive inputs. -/ theorem modifiedNarayanaTuran_nonneg_of_le_five {m : ℕ} {r : ℝ} (hm₁ : 1 ≤ m) (hm₅ : m ≤ 5) (hr : r ≤ 0) : @@ -558,12 +547,6 @@ theorem modifiedNarayanaTuran_nonneg_of_le_five exact mul_nonneg (by linarith) (modifiedNarayanaTuran_five_factor_nonneg_of_nonpos hr) -/-- Bounded Turan package through `m = 5`. -/ -theorem modifiedNarayanaTuranNonnegOnNonpos_upTo_five : - ModifiedNarayanaTuranNonnegOnNonposUpToStatement 5 := by - intro m r hm₁ hm₅ hr - exact modifiedNarayanaTuran_nonneg_of_le_five hm₁ hm₅ hr - /-- The first six Narayana Turan inequalities on nonpositive inputs. -/ theorem modifiedNarayanaTuran_nonneg_of_le_six {m : ℕ} {r : ℝ} (hm₁ : 1 ≤ m) (hm₆ : m ≤ 6) (hr : r ≤ 0) : @@ -585,12 +568,6 @@ theorem modifiedNarayanaTuran_nonneg_of_le_six exact mul_nonneg (by linarith) (modifiedNarayanaTuran_six_factor_nonneg_of_nonpos hr) -/-- Bounded Turan package through `m = 6`. -/ -theorem modifiedNarayanaTuranNonnegOnNonpos_upTo_six : - ModifiedNarayanaTuranNonnegOnNonposUpToStatement 6 := by - intro m r hm₁ hm₆ hr - exact modifiedNarayanaTuran_nonneg_of_le_six hm₁ hm₆ hr - /-- The first seven Narayana Turan inequalities on nonpositive inputs. -/ theorem modifiedNarayanaTuran_nonneg_of_le_seven {m : ℕ} {r : ℝ} (hm₁ : 1 ≤ m) (hm₇ : m ≤ 7) (hr : r ≤ 0) : @@ -615,12 +592,6 @@ theorem modifiedNarayanaTuran_nonneg_of_le_seven exact mul_nonneg (by linarith) (modifiedNarayanaTuran_seven_factor_nonneg_of_nonpos hr) -/-- Bounded Turan package through `m = 7`. -/ -theorem modifiedNarayanaTuranNonnegOnNonpos_upTo_seven : - ModifiedNarayanaTuranNonnegOnNonposUpToStatement 7 := by - intro m r hm₁ hm₇ hr - exact modifiedNarayanaTuran_nonneg_of_le_seven hm₁ hm₇ hr - /-- The first eight Narayana Turan inequalities on nonpositive inputs. -/ theorem modifiedNarayanaTuran_nonneg_of_le_eight {m : ℕ} {r : ℝ} (hm₁ : 1 ≤ m) (hm₈ : m ≤ 8) (hr : r ≤ 0) : @@ -648,12 +619,6 @@ theorem modifiedNarayanaTuran_nonneg_of_le_eight exact mul_nonneg (by linarith) (modifiedNarayanaTuran_eight_factor_nonneg_of_nonpos hr) -/-- Bounded Turan package through `m = 8`. -/ -theorem modifiedNarayanaTuranNonnegOnNonpos_upTo_eight : - ModifiedNarayanaTuranNonnegOnNonposUpToStatement 8 := by - intro m r hm₁ hm₈ hr - exact modifiedNarayanaTuran_nonneg_of_le_eight hm₁ hm₈ hr - /-- The first nine Narayana Turan inequalities on nonpositive inputs. -/ theorem modifiedNarayanaTuran_nonneg_of_le_nine {m : ℕ} {r : ℝ} (hm₁ : 1 ≤ m) (hm₉ : m ≤ 9) (hr : r ≤ 0) : @@ -684,12 +649,6 @@ theorem modifiedNarayanaTuran_nonneg_of_le_nine exact mul_nonneg (by linarith) (modifiedNarayanaTuran_nine_factor_nonneg_of_nonpos hr) -/-- Bounded Turan package through `m = 9`. -/ -theorem modifiedNarayanaTuranNonnegOnNonpos_upTo_nine : - ModifiedNarayanaTuranNonnegOnNonposUpToStatement 9 := by - intro m r hm₁ hm₉ hr - exact modifiedNarayanaTuran_nonneg_of_le_nine hm₁ hm₉ hr - /-- The first ten Narayana Turan inequalities on nonpositive inputs. -/ theorem modifiedNarayanaTuran_nonneg_of_le_ten {m : ℕ} {r : ℝ} (hm₁ : 1 ≤ m) (hm₁₀ : m ≤ 10) (hr : r ≤ 0) : @@ -723,11 +682,5 @@ theorem modifiedNarayanaTuran_nonneg_of_le_ten exact mul_nonneg (by linarith) (modifiedNarayanaTuran_ten_factor_nonneg_of_nonpos hr) -/-- Bounded Turan package through `m = 10`. -/ -theorem modifiedNarayanaTuranNonnegOnNonpos_upTo_ten : - ModifiedNarayanaTuranNonnegOnNonposUpToStatement 10 := by - intro m r hm₁ hm₁₀ hr - exact modifiedNarayanaTuran_nonneg_of_le_ten hm₁ hm₁₀ hr - end GeneralizedSnakePosets end RealRooted diff --git a/RealRooted/GeneralizedSnakePosets/SnakeInterlacing.lean b/RealRooted/GeneralizedSnakePosets/SnakeInterlacing.lean deleted file mode 100644 index 4de6b2ce9..000000000 --- a/RealRooted/GeneralizedSnakePosets/SnakeInterlacing.lean +++ /dev/null @@ -1,91 +0,0 @@ -import RealRooted.GeneralizedSnakePosets.Narayana.ShiftedDifferenceInterlacing -import RealRooted.GeneralizedSnakePosets.SnakeConstant - -/-! -# The snake interlacing theorem for the concrete snake board - -This module discharges every source input of -`nonNestingRookInterlacing_modified_of_sourceInputs` for the concrete model -`generalizedSnakeRookModel` except snake recurrence itself: - -* the auxiliary recurrence and nonnegativity of `G_n - G_{n-1}` hold for every `n` - (`TruncatedStaircase.ColumnRecurrence`); -* snake polynomials are rook polynomials, so they have nonnegative - coefficients; -* constant words give `P_{n+1}` (`SnakeConstant`); -* the degree identity follows from the snake recurrence and the constant case, since - `deg M_w = |w| + 1`. --/ - -open Polynomial - -noncomputable section - -namespace RealRooted -namespace GeneralizedSnakePosets - -open FiniteSkewBoard - -/-- The snake recurrence for the concrete snake model. -/ -abbrev GeneralizedSnakeRecurrenceHolds : Prop := - GeneralizedSnakeRecurrenceStatement generalizedSnakeRookModel.snakePolynomial - modifiedNarayanaPolynomial auxiliaryG - -/-- Given the snake recurrence, every snake polynomial has degree `|w| + 1`. -/ -theorem generalizedSnakeRookModel_natDegree (hrec : GeneralizedSnakeRecurrenceHolds) - (w : SnakeWord) : - (generalizedSnakeRookModel.snakePolynomial w).natDegree = w.length + 1 := by - induction hn : w.length using Nat.strong_induction_on generalizing w with - | h n ih => - by_cases hc : w.IsConstant - · rw [generalizedSnakeRookModel_snakePolynomial_of_isConstant hc, - modifiedNarayanaPolynomial_natDegree, hn] - · obtain ⟨k, hk⟩ := SnakeWord.exists_isLastChangeIndex_of_not_isConstant hc - have hk1 := hk.succ_lt_length - have hlen1 : (w.takePrefix (k + 1)).length = k + 1 := by - simp [SnakeWord.takePrefix]; lia - have hlen0 : (w.takePrefix k).length = k := by - simp [SnakeWord.takePrefix]; lia - have hu := ih (k + 1) (by lia) (w.takePrefix (k + 1)) hlen1 - have hv := ih k (by lia) (w.takePrefix k) hlen0 - set s := w.length - (k + 1) with hs - have hs1 : 1 ≤ s := by lia - have hP := modifiedNarayanaPolynomial_natDegree s - have hG := auxiliaryG_natDegree_of_narayanaRecurrence - narayanaAuxiliaryGRecurrence_modified s hs1 - have hu0 : generalizedSnakeRookModel.snakePolynomial (w.takePrefix (k + 1)) ≠ 0 := - squarecaseRookModelOfFiniteSkewBoard_snakePolynomial_ne_zero _ _ - have hv0 : generalizedSnakeRookModel.snakePolynomial (w.takePrefix k) ≠ 0 := - squarecaseRookModelOfFiniteSkewBoard_snakePolynomial_ne_zero _ _ - have hP0 : modifiedNarayanaPolynomial s ≠ 0 := modifiedNarayanaPolynomial_ne_zero s - have hdeg1 : (generalizedSnakeRookModel.snakePolynomial (w.takePrefix (k + 1)) * - modifiedNarayanaPolynomial s).natDegree = n + 1 := by - rw [natDegree_mul hu0 hP0, hu, hP]; lia - have hdeg2 : (X * generalizedSnakeRookModel.snakePolynomial (w.takePrefix k) * - auxiliaryG s).natDegree ≤ n := by - refine (natDegree_mul_le).trans ?_ - rw [hG] - refine (Nat.add_le_add_right natDegree_mul_le _).trans ?_ - rw [natDegree_X, hv]; lia - rw [hrec hc hk, natDegree_add_eq_left_of_natDegree_lt (by rw [hdeg1]; lia), hdeg1] - -/-- **The snake interlacing theorem for the concrete snake board, from the snake recurrence.** -Given the snake-word recurrence (the snake recurrence), every generalized snake -polynomial is real-rooted, and deleting the final letter gives an interlacing -polynomial. -/ -theorem snakeInterlacing_generalizedSnakeRookModel_of_snakeRecurrence - (hrec : GeneralizedSnakeRecurrenceHolds) : - NonNestingRookInterlacingStatement generalizedSnakeRookModel.snakePolynomial := - nonNestingRookInterlacing_modified_of_sourceInputs - narayanaAuxiliaryGRecurrence_modified - (fun _ hn => auxiliaryG_sub_hasNonnegCoeffs hn) - hrec - (fun w => rookPolynomial_hasNonnegCoeffs (generalizedSnakeBoard w)) - (fun {w} hw => by - rw [generalizedSnakeRookModel_natDegree hrec, generalizedSnakeRookModel_natDegree hrec, - SnakeWord.length_deleteFinal] - lia) - (fun hw => generalizedSnakeRookModel_snakePolynomial_of_isConstant hw) - -end GeneralizedSnakePosets -end RealRooted diff --git a/RealRooted/GeneralizedSnakePosets/SnakeRecurrence.lean b/RealRooted/GeneralizedSnakePosets/SnakeRecurrence.lean index 21f1b78a1..9ad9b913d 100644 --- a/RealRooted/GeneralizedSnakePosets/SnakeRecurrence.lean +++ b/RealRooted/GeneralizedSnakePosets/SnakeRecurrence.lean @@ -1,5 +1,6 @@ import RealRooted.GeneralizedSnakePosets.SnakeBand -import RealRooted.GeneralizedSnakePosets.SnakeInterlacing +import RealRooted.GeneralizedSnakePosets.Narayana.ShiftedDifferenceInterlacing +import RealRooted.GeneralizedSnakePosets.SnakeConstant /-! # The snake recurrence for the concrete snake board @@ -222,7 +223,9 @@ theorem chainPolynomial_bandCells_split {m : ℕ} {b : SnakeLetter} end Split /-- **The snake recurrence for the concrete snake board.** -/ -theorem generalizedSnakeRecurrence : GeneralizedSnakeRecurrenceHolds := by +theorem generalizedSnakeRecurrence : + GeneralizedSnakeRecurrenceStatement generalizedSnakeRookModel.snakePolynomial + modifiedNarayanaPolynomial auxiliaryG := by intro w k _ hk have hk1 := hk.succ_lt_length obtain ⟨s, hs⟩ : ∃ s, w.length = k + 1 + s := ⟨w.length - (k + 1), by lia⟩ @@ -258,14 +261,65 @@ theorem generalizedSnakeRecurrence : GeneralizedSnakeRecurrenceHolds := by /-- Every generalized snake polynomial has degree `|w| + 1`. -/ theorem generalizedSnakeRookModel_natDegree_eq (w : SnakeWord) : - (generalizedSnakeRookModel.snakePolynomial w).natDegree = w.length + 1 := - generalizedSnakeRookModel_natDegree generalizedSnakeRecurrence w + (generalizedSnakeRookModel.snakePolynomial w).natDegree = w.length + 1 := by + induction hn : w.length using Nat.strong_induction_on generalizing w with + | h n ih => + by_cases hc : w.IsConstant + · rw [generalizedSnakeRookModel_snakePolynomial_of_isConstant hc, + modifiedNarayanaPolynomial_natDegree, hn] + · obtain ⟨k, hk⟩ := SnakeWord.exists_isLastChangeIndex_of_not_isConstant hc + have hk1 := hk.succ_lt_length + have hlen1 : (w.takePrefix (k + 1)).length = k + 1 := by + simp [SnakeWord.takePrefix]; lia + have hlen0 : (w.takePrefix k).length = k := by + simp [SnakeWord.takePrefix]; lia + have hu := ih (k + 1) (by lia) (w.takePrefix (k + 1)) hlen1 + have hv := ih k (by lia) (w.takePrefix k) hlen0 + set s := w.length - (k + 1) with hs + have hs1 : 1 ≤ s := by lia + have hP := modifiedNarayanaPolynomial_natDegree s + have hG := auxiliaryG_natDegree_of_narayanaRecurrence + narayanaAuxiliaryGRecurrence_modified s hs1 + have hu0 : generalizedSnakeRookModel.snakePolynomial (w.takePrefix (k + 1)) ≠ 0 := + squarecaseRookModelOfFiniteSkewBoard_snakePolynomial_ne_zero _ _ + have hv0 : generalizedSnakeRookModel.snakePolynomial (w.takePrefix k) ≠ 0 := + squarecaseRookModelOfFiniteSkewBoard_snakePolynomial_ne_zero _ _ + have hP0 : modifiedNarayanaPolynomial s ≠ 0 := modifiedNarayanaPolynomial_ne_zero s + have hdeg1 : (generalizedSnakeRookModel.snakePolynomial (w.takePrefix (k + 1)) * + modifiedNarayanaPolynomial s).natDegree = n + 1 := by + rw [natDegree_mul hu0 hP0, hu, hP]; lia + have hdeg2 : (X * generalizedSnakeRookModel.snakePolynomial (w.takePrefix k) * + auxiliaryG s).natDegree ≤ n := by + refine (natDegree_mul_le).trans ?_ + rw [hG] + refine (Nat.add_le_add_right natDegree_mul_le _).trans ?_ + rw [natDegree_X, hv]; lia + rw [generalizedSnakeRecurrence hc hk, + natDegree_add_eq_left_of_natDegree_lt (by rw [hdeg1]; lia), hdeg1] /-- **The snake interlacing theorem.** Every generalized snake polynomial is -real-rooted, and deleting the final letter gives an interlacing polynomial. -/ -theorem snakeInterlacing_generalizedSnakeRookModel : - NonNestingRookInterlacingStatement generalizedSnakeRookModel.snakePolynomial := - snakeInterlacing_generalizedSnakeRookModel_of_snakeRecurrence generalizedSnakeRecurrence +real-rooted, and deleting the final letter gives an interlacing polynomial. + +The source inputs of `nonNestingRookInterlacing_modified_of_sourceInputs` are: +the auxiliary recurrence and nonnegativity of `G_n - G_{n-1}` +(`TruncatedStaircase.ColumnRecurrence`); nonnegative coefficients of rook +polynomials; the constant-word case (`SnakeConstant`); the degree identity +`deg M_w = |w| + 1`; and the snake recurrence `generalizedSnakeRecurrence`. -/ +theorem snakeInterlacing_generalizedSnakeRookModel {w : SnakeWord} (hw : 1 ≤ w.length) : + (generalizedSnakeRookModel.snakePolynomial w ≠ 0 ∧ + (generalizedSnakeRookModel.snakePolynomial w).Splits) ∧ + Interlaces (generalizedSnakeRookModel.snakePolynomial w.deleteFinal) + (generalizedSnakeRookModel.snakePolynomial w) := + (nonNestingRookInterlacing_modified_of_sourceInputs + narayanaAuxiliaryGRecurrence_modified + (fun _ hn => auxiliaryG_sub_hasNonnegCoeffs hn) + generalizedSnakeRecurrence + (fun w => rookPolynomial_hasNonnegCoeffs (generalizedSnakeBoard w)) + (fun {w} hw => by + rw [generalizedSnakeRookModel_natDegree_eq, generalizedSnakeRookModel_natDegree_eq, + SnakeWord.length_deleteFinal] + lia) + (fun hw => generalizedSnakeRookModel_snakePolynomial_of_isConstant hw)) hw end GeneralizedSnakePosets end RealRooted diff --git a/RealRooted/GeneralizedSnakePosets/Statements.lean b/RealRooted/GeneralizedSnakePosets/Statements.lean index 47b406069..19651d9e5 100644 --- a/RealRooted/GeneralizedSnakePosets/Statements.lean +++ b/RealRooted/GeneralizedSnakePosets/Statements.lean @@ -3,15 +3,15 @@ import RealRooted.GeneralizedSnakePosets.SquarecaseModel import RealRooted.Mathlib.Algebra.Polynomial.Roots /-! -# Braun--Jal generalized snake poset statement interfaces - -This module contains the paper-facing theorem statements and the combinatorial-input -interfaces for Braun--Jal, *Order polytopes of generalized snake posets are -h^*-real-rooted*, arXiv:2607.00922v1. - -The declarations here are deliberately abstract in the polynomial model. The -concrete finite-board and squarecase geometry modules can construct these -interfaces without importing the higher-level package wrappers. +# Braun--Jal generalized snake poset predicates + +This module contains the predicates on abstract polynomial families `P`, `G` +and snake-word models `M` used by the snake-interlacing induction of +Braun--Jal, *Order polytopes of generalized snake posets are +h^*-real-rooted*, arXiv:2607.00922v1, together with the generic assembly of +the shifted difference interlacing claim. The concrete instances are proved +for `modifiedNarayanaPolynomial`, `FiniteSkewBoard.auxiliaryG`, and +`generalizedSnakeRookModel`. -/ open Polynomial @@ -35,53 +35,13 @@ def NonNestingRookInterlacingStatement (M : SnakeWord → ℝ[X]) : Prop := (M w ≠ 0 ∧ (M w).Splits) ∧ Interlaces (M w.deleteFinal) (M w) -/-- Snake-interlacing expressed for an abstract squarecase/non-nesting rook model. -/ -abbrev SquarecaseRookModelSnakeInterlacingStatement - (model : SquarecaseRookModel) : Prop := - NonNestingRookInterlacingStatement model.snakePolynomial - -/-- The real-rootedness part of the snake interlacing theorem. -/ -theorem nonNestingRook_ne_zero_and_splits_of_snakeInterlacing - {M : SnakeWord → ℝ[X]} - (hBJ : NonNestingRookInterlacingStatement M) - {w : SnakeWord} (hw : 1 ≤ w.length) : - M w ≠ 0 ∧ (M w).Splits := - (hBJ (w := w) hw).1 - -/-- The final-letter-deletion interlacing part of the snake interlacing theorem. -/ -theorem nonNestingRook_deleteFinal_interlaces_of_snakeInterlacing - {M : SnakeWord → ℝ[X]} - (hBJ : NonNestingRookInterlacingStatement M) - {w : SnakeWord} (hw : 1 ≤ w.length) : - Interlaces (M w.deleteFinal) (M w) := - (hBJ (w := w) hw).2 - /-! ## Narayana and recurrence interfaces from the combinatorial inputs -/ -/-- A family `P` is the modified Narayana family attached to Narayana -polynomials `N` when `N_{n+1} = X * P_n`, i.e. `P_n(t) = t^{-1} N_{n+1}(t)`. --/ -def ModifiedNarayanaFamilyStatement - (N P : ℕ → ℝ[X]) : Prop := - P 0 = 1 ∧ ∀ n : ℕ, N (n + 1) = X * P n - -/-- The auxiliary polynomial `G_n` as the sum of non-nesting rook polynomials -of truncated staircases `mu_{n,i}` for `i = 0, ..., n - 1`. -/ -def AuxiliaryGMatchesTruncatedStaircasesStatement - (Mtrunc : ℕ → ℕ → ℝ[X]) (G : ℕ → ℝ[X]) : Prop := - ∀ n : ℕ, G n = ((List.range n).map fun i => Mtrunc n i).sum - /-- The auxiliary recurrence of Braun--Jal: `X * G_{n-1} = P_n - (1 + X) * P_{n-1}`. -/ def NarayanaAuxiliaryGRecurrenceStatement (P G : ℕ → ℝ[X]) : Prop := ∀ {n : ℕ}, 1 ≤ n → X * G (n - 1) = P n - (1 + X) * P (n - 1) -/-- Auxiliary-interlacing statement: the auxiliary `G_n` interlaces modified Narayana -polynomial `P_n`. -/ -def AuxiliaryGInterlacesStatement - (P G : ℕ → ℝ[X]) : Prop := - ∀ {n : ℕ}, 1 ≤ n → StrictInterl (G n) (P n) - /-- Affine-Narayana statement for the modified Narayana family. -/ def AffineModifiedNarayanaInterlacingStatement (P : ℕ → ℝ[X]) : Prop := @@ -148,122 +108,6 @@ theorem affineModifiedNarayanaShiftedInterlacing_of_affineNarayana ring_nf rwa [hleft, hright] at hbase -/-- Equivalence between the paper's affine-Narayana statement and the shifted -nonnegative-parameter form. -/ -theorem affineModifiedNarayanaShiftedInterlacing_iff_affineNarayana - (P : ℕ → ℝ[X]) : - AffineModifiedNarayanaShiftedInterlacingStatement P ↔ - AffineModifiedNarayanaInterlacingStatement P := - ⟨affineModifiedNarayanaInterlacing_of_shifted, - affineModifiedNarayanaShiftedInterlacing_of_affineNarayana⟩ - -/-- Bounded form of the auxiliary recurrence, useful while finite initial -cases are being formalized before the all-`n` recurrence is available. -/ -def NarayanaAuxiliaryGRecurrenceUpToStatement - (P G : ℕ → ℝ[X]) (N : ℕ) : Prop := - ∀ {n : ℕ}, 1 ≤ n → n ≤ N → - X * G (n - 1) = P n - (1 + X) * P (n - 1) - -/-- Bounded form of the auxiliary interlacing lemma. -/ -def AuxiliaryGInterlacesUpToStatement - (P G : ℕ → ℝ[X]) (N : ℕ) : Prop := - ∀ {n : ℕ}, 1 ≤ n → n ≤ N → StrictInterl (G n) (P n) - -/-- Bounded form of the affine Narayana interlacing lemma. -/ -def AffineModifiedNarayanaInterlacingUpToStatement - (P : ℕ → ℝ[X]) (N : ℕ) : Prop := - ∀ {m : ℕ} {lam nu : ℝ}, 2 ≤ m → m ≤ N → 0 ≤ lam → -1 ≤ nu → - StrictInterl ((C lam * X + C nu) * P (m - 1) + P m) - ((C lam * X + C nu) * P m + P (m + 1)) - -/-- Bounded shifted nonnegative-parameter form of the affine Narayana interlacing lemma. -/ -def AffineModifiedNarayanaShiftedInterlacingUpToStatement - (P : ℕ → ℝ[X]) (N : ℕ) : Prop := - ∀ {m : ℕ} {lam mu : ℝ}, 2 ≤ m → m ≤ N → 0 ≤ lam → 0 ≤ mu → - StrictInterl ((C lam * X + C mu) * P (m - 1) + narayanaDifference P m) - ((C lam * X + C mu) * P m + narayanaDifference P (m + 1)) - -/-- The all-`n` auxiliary-interlacing statement implies every bounded auxiliary-interlacing -package. -/ -theorem auxiliaryGInterlacesUpTo_of_statement - {P G : ℕ → ℝ[X]} (h : AuxiliaryGInterlacesStatement P G) - (N : ℕ) : - AuxiliaryGInterlacesUpToStatement P G N := by - intro n hn _hnN - exact h hn - -/-- The all-`n` affine-Narayana statement implies every bounded affine-Narayana package. -/ -theorem affineModifiedNarayanaInterlacingUpTo_of_statement - {P : ℕ → ℝ[X]} (h : AffineModifiedNarayanaInterlacingStatement P) - (N : ℕ) : - AffineModifiedNarayanaInterlacingUpToStatement P N := by - intro m lam nu hm _hmN hlam hnu - exact h hm hlam hnu - -/-- The all-`n` shifted affine-Narayana statement implies every bounded shifted -the affine-Narayana package. -/ -theorem affineModifiedNarayanaShiftedInterlacingUpTo_of_statement - {P : ℕ → ℝ[X]} - (h : AffineModifiedNarayanaShiftedInterlacingStatement P) (N : ℕ) : - AffineModifiedNarayanaShiftedInterlacingUpToStatement P N := by - intro m lam mu hm _hmN hlam hmu - exact h hm hlam hmu - -/-- A bounded shifted affine-Narayana package implies the bounded paper-shaped -`nu ≥ -1` package. -/ -theorem affineModifiedNarayanaInterlacingUpTo_of_shifted - {P : ℕ → ℝ[X]} {N : ℕ} - (h : AffineModifiedNarayanaShiftedInterlacingUpToStatement P N) : - AffineModifiedNarayanaInterlacingUpToStatement P N := by - intro m lam nu hm hmN hlam hnu - have hmu : 0 ≤ nu + 1 := by linarith - have hbase := h (m := m) (lam := lam) (mu := nu + 1) hm hmN hlam hmu - have hC : (C (nu + 1) : ℝ[X]) = C nu + 1 := by simp - have hleft : - ((C lam * X + C (nu + 1)) * P (m - 1) + narayanaDifference P m) = - ((C lam * X + C nu) * P (m - 1) + P m) := by - rw [narayanaDifference, hC] - ring_nf - have hright : - ((C lam * X + C (nu + 1)) * P m + narayanaDifference P (m + 1)) = - ((C lam * X + C nu) * P m + P (m + 1)) := by - rw [narayanaDifference, hC] - simp only [Nat.add_sub_cancel] - ring_nf - rwa [hleft, hright] at hbase - -/-- A bounded paper-shaped affine-Narayana package implies the bounded shifted -nonnegative-parameter package. -/ -theorem affineModifiedNarayanaShiftedInterlacingUpTo_of_affineNarayana - {P : ℕ → ℝ[X]} {N : ℕ} - (h : AffineModifiedNarayanaInterlacingUpToStatement P N) : - AffineModifiedNarayanaShiftedInterlacingUpToStatement P N := by - intro m lam mu hm hmN hlam hmu - have hnu : -1 ≤ mu - 1 := by linarith - have hbase := h (m := m) (lam := lam) (nu := mu - 1) hm hmN hlam hnu - have hC : (C (mu - 1) : ℝ[X]) = C mu - 1 := by simp - have hleft : - ((C lam * X + C (mu - 1)) * P (m - 1) + P m) = - ((C lam * X + C mu) * P (m - 1) + narayanaDifference P m) := by - rw [narayanaDifference, hC] - ring_nf - have hright : - ((C lam * X + C (mu - 1)) * P m + P (m + 1)) = - ((C lam * X + C mu) * P m + narayanaDifference P (m + 1)) := by - rw [narayanaDifference, hC] - simp only [Nat.add_sub_cancel] - ring_nf - rwa [hleft, hright] at hbase - -/-- Bounded equivalence between the paper-shaped affine-Narayana statement and the -shifted nonnegative-parameter form. -/ -theorem affineModifiedNarayanaShiftedInterlacingUpTo_iff_affineNarayana - (P : ℕ → ℝ[X]) (N : ℕ) : - AffineModifiedNarayanaShiftedInterlacingUpToStatement P N ↔ - AffineModifiedNarayanaInterlacingUpToStatement P N := - ⟨affineModifiedNarayanaInterlacingUpTo_of_shifted, - affineModifiedNarayanaShiftedInterlacingUpTo_of_affineNarayana⟩ - /-- Difference `H_n = G_n - G_{n-1}` used in the snake-interlacing matrix step. -/ def auxiliaryDifference (G : ℕ → ℝ[X]) (n : ℕ) : ℝ[X] := G n - G (n - 1) @@ -283,54 +127,12 @@ def ShiftedDifferenceInterlacingStatement StrictInterl ((C lam * X + C nu) * G (m - 1) + G m) ((C lam * X + C nu) * P (m - 1) + P m) -/-- Leading-coefficient, degree, and root-location side conditions used by -the univariate conversion step in the proof of shifted difference interlacing claim. - -The bundle intentionally does not include the auxiliary recurrence or the affine Narayana -interlacing lemma: those -are the structural combinatorial inputs, while these are the local facts about the -three windows `U`, `V`, and `W` consumed by the conversion theorem. -/ -structure ShiftedDifferenceInterlacingSideConditions - (P G : ℕ → ℝ[X]) : Prop where - w_pos : - ∀ {m : ℕ} {lam nu : ℝ}, 2 ≤ m → 0 ≤ lam → -1 ≤ nu → - HasPosLeadingCoeff ((C lam * X + C nu) * P m + P (m + 1)) - wu_lc : - ∀ {m : ℕ} {lam nu : ℝ}, 2 ≤ m → 0 ≤ lam → -1 ≤ nu → - ((C lam * X + C nu) * P m + P (m + 1)).leadingCoeff = - ((C lam * X + C nu) * P (m - 1) + P m).leadingCoeff - deg_uw : - ∀ {m : ℕ} {lam nu : ℝ}, 2 ≤ m → 0 ≤ lam → -1 ≤ nu → - ((C lam * X + C nu) * P (m - 1) + P m).natDegree + 1 = - ((C lam * X + C nu) * P m + P (m + 1)).natDegree - w_nonpos : - ∀ {m : ℕ} {lam nu : ℝ}, 2 ≤ m → 0 ≤ lam → -1 ≤ nu → - ∀ r ∈ (((C lam * X + C nu) * P m + P (m + 1)).roots), r ≤ 0 - mid_pos : - ∀ {m : ℕ} {lam nu : ℝ}, 2 ≤ m → 0 ≤ lam → -1 ≤ nu → - HasPosLeadingCoeff - (((C lam * X + C nu) * P (m - 1) + P m) + - X * ((C lam * X + C nu) * G (m - 1) + G m)) - v_pos : - ∀ {m : ℕ} {lam nu : ℝ}, 2 ≤ m → 0 ≤ lam → -1 ≤ nu → - HasPosLeadingCoeff ((C lam * X + C nu) * G (m - 1) + G m) - v_nonpos : - ∀ {m : ℕ} {lam nu : ℝ}, 2 ≤ m → 0 ≤ lam → -1 ≤ nu → - ∀ r ∈ (((C lam * X + C nu) * G (m - 1) + G m).roots), r ≤ 0 - deg_vu : - ∀ {m : ℕ} {lam nu : ℝ}, 2 ≤ m → 0 ≤ lam → -1 ≤ nu → - ((C lam * X + C nu) * G (m - 1) + G m).natDegree + 1 = - ((C lam * X + C nu) * P (m - 1) + P m).natDegree - u_bound : - ∀ {m : ℕ} {lam nu : ℝ}, 2 ≤ m → 0 ≤ lam → -1 ≤ nu → - ∃ c : ℝ, - (∀ s ∈ (((C lam * X + C nu) * P (m - 1) + P m).roots), s ≤ c) ∧ - c < 0 - -/-- Root-sum replacement for `ShiftedDifferenceInterlacingSideConditions`. +/-- Side conditions for the shifted difference interlacing claim. -The strict negative upper bound in the older bundle fails at legitimate -zero-root endpoints. This bundle instead records nonpositivity of the roots +A uniform strict negative upper bound on the roots of `U` fails at the +zero-root endpoint `ν = -1` +(`shiftedDifferenceInterlacing_modified_left_boundary_not_strictRootBound`). +This bundle instead records nonpositivity of the roots of `U` explicitly and orients the same-degree Obreschkoff alternative by the root-sum comparison between `U` and `V`. -/ structure ShiftedDifferenceInterlacingRootSumSideConditions @@ -465,20 +267,9 @@ theorem shiftedDifferenceInterlacing_of_combinatorial (by simpa [U, V] using hdeg_VU hm hlam hnu) (by simpa [U] using hU_bound hm hlam hnu) -/-- Bundled-side-condition form of `shiftedDifferenceInterlacing_of_combinatorial`. -/ -theorem shiftedDifferenceInterlacing_of_combinatorial_sideConditions - {P G : ℕ → ℝ[X]} - (hrec : NarayanaAuxiliaryGRecurrenceStatement P G) - (h34 : AffineModifiedNarayanaInterlacingStatement P) - (hside : ShiftedDifferenceInterlacingSideConditions P G) : - ShiftedDifferenceInterlacingStatement P G := - shiftedDifferenceInterlacing_of_combinatorial hrec h34 - hside.w_pos hside.wu_lc hside.deg_uw hside.w_nonpos hside.mid_pos - hside.v_pos hside.v_nonpos hside.deg_vu hside.u_bound - /-- Bundled root-sum assembly theorem for the shifted difference interlacing claim. -Unlike `shiftedDifferenceInterlacing_of_combinatorial_sideConditions`, this route remains +Unlike `shiftedDifferenceInterlacing_of_combinatorial`, this route remains applicable when `U` has a root at zero. -/ theorem shiftedDifferenceInterlacing_of_combinatorial_rootSumSideConditions {P G : ℕ → ℝ[X]} @@ -555,191 +346,5 @@ def GeneralizedSnakeRecurrenceStatement M w = M (w.takePrefix (k + 1)) * P (w.length - (k + 1)) + X * M (w.takePrefix k) * G (w.length - (k + 1)) -/-- Computable form of the snake recurrence, using `lastChangeIndex?` instead of a -separate predicate-form witness. -/ -def GeneralizedSnakeRecurrenceComputableStatement - (M : SnakeWord → ℝ[X]) (P G : ℕ → ℝ[X]) : Prop := - ∀ {w : SnakeWord} {k : ℕ}, w.lastChangeIndex? = some k → - M w = M (w.takePrefix (k + 1)) * P (w.length - (k + 1)) + - X * M (w.takePrefix k) * G (w.length - (k + 1)) - -/-- The predicate-form recurrence implies the computable `lastChangeIndex?` -form. -/ -theorem snakeRecurrenceComputable_of_snakeRecurrence - {M : SnakeWord → ℝ[X]} {P G : ℕ → ℝ[X]} - (hrec : GeneralizedSnakeRecurrenceStatement M P G) : - GeneralizedSnakeRecurrenceComputableStatement M P G := by - intro w k hlast - exact hrec (SnakeWord.not_isConstant_of_lastChangeIndex?_eq_some hlast) - (SnakeWord.isLastChangeIndex_of_lastChangeIndex?_eq_some hlast) - -/-- The computable `lastChangeIndex?` recurrence implies the predicate-form -recurrence. -/ -theorem snakeRecurrence_of_snakeRecurrenceComputable - {M : SnakeWord → ℝ[X]} {P G : ℕ → ℝ[X]} - (hrec : GeneralizedSnakeRecurrenceComputableStatement M P G) : - GeneralizedSnakeRecurrenceStatement M P G := by - intro w k _hconst hlast - exact hrec (SnakeWord.lastChangeIndex?_eq_some_of_isLastChangeIndex hlast) - -/-- The predicate-form and computable forms of the generalized snake -recurrence are equivalent. -/ -theorem snakeRecurrenceComputable_iff_snakeRecurrence - (M : SnakeWord → ℝ[X]) (P G : ℕ → ℝ[X]) : - GeneralizedSnakeRecurrenceComputableStatement M P G ↔ - GeneralizedSnakeRecurrenceStatement M P G := - ⟨snakeRecurrence_of_snakeRecurrenceComputable, snakeRecurrenceComputable_of_snakeRecurrence⟩ - -/-- Statement-level package for the induction route from the combinatorial inputs -Narayana and recurrence ingredients to the snake interlacing theorem. -/ -def SnakeInterlacingInductionRouteStatement - (M : SnakeWord → ℝ[X]) (P G : ℕ → ℝ[X]) : Prop := - AuxiliaryGInterlacesStatement P G → - AffineModifiedNarayanaInterlacingStatement P → - GeneralizedSnakeRecurrenceStatement M P G → - NonNestingRookInterlacingStatement M - -/-- Computable-recursion variant of the current snake-interlacing induction route. -/ -def SnakeInterlacingInductionRouteComputableStatement - (M : SnakeWord → ℝ[X]) (P G : ℕ → ℝ[X]) : Prop := - AuxiliaryGInterlacesStatement P G → - AffineModifiedNarayanaInterlacingStatement P → - GeneralizedSnakeRecurrenceComputableStatement M P G → - NonNestingRookInterlacingStatement M - -/-- The predicate-form induction route also accepts a computable recurrence -input. -/ -theorem snakeInterlacingInductionRouteComputable_of_snakeInterlacingInductionRoute - {M : SnakeWord → ℝ[X]} {P G : ℕ → ℝ[X]} - (hroute : SnakeInterlacingInductionRouteStatement M P G) : - SnakeInterlacingInductionRouteComputableStatement M P G := by - intro h33 h34 hrec - exact hroute h33 h34 (snakeRecurrence_of_snakeRecurrenceComputable hrec) - -/-- The computable-recursion induction route implies the predicate-form route. -/ -theorem snakeInterlacingInductionRoute_of_snakeInterlacingInductionRouteComputable - {M : SnakeWord → ℝ[X]} {P G : ℕ → ℝ[X]} - (hroute : SnakeInterlacingInductionRouteComputableStatement M P G) : - SnakeInterlacingInductionRouteStatement M P G := by - intro h33 h34 hrec - exact hroute h33 h34 (snakeRecurrenceComputable_of_snakeRecurrence hrec) - -/-- Predicate and computable forms of the snake-interlacing induction route are -equivalent. -/ -theorem snakeInterlacingInductionRouteComputable_iff_snakeInterlacingInductionRoute - (M : SnakeWord → ℝ[X]) (P G : ℕ → ℝ[X]) : - SnakeInterlacingInductionRouteComputableStatement M P G ↔ - SnakeInterlacingInductionRouteStatement M P G := - ⟨snakeInterlacingInductionRoute_of_snakeInterlacingInductionRouteComputable, - snakeInterlacingInductionRouteComputable_of_snakeInterlacingInductionRoute⟩ - -/-- Bundled the combinatorial ingredients needed by the current snake-interlacing induction -interface. -/ -structure SnakeInterlacingInputs - (M : SnakeWord → ℝ[X]) (P G : ℕ → ℝ[X]) : Prop where - auxiliaryGInterlacing : AuxiliaryGInterlacesStatement P G - affineNarayana : AffineModifiedNarayanaInterlacingStatement P - recurrence : GeneralizedSnakeRecurrenceStatement M P G - -/-- Bundled the combinatorial ingredients using the computable recurrence form. -/ -structure SnakeInterlacingComputableInputs - (M : SnakeWord → ℝ[X]) (P G : ℕ → ℝ[X]) : Prop where - auxiliaryGInterlacing : AuxiliaryGInterlacesStatement P G - affineNarayana : AffineModifiedNarayanaInterlacingStatement P - recurrence : GeneralizedSnakeRecurrenceComputableStatement M P G - -/-- Bundled the combinatorial ingredients using shifted nonnegative-parameter -the affine-Narayana form. -/ -structure SnakeInterlacingShiftedInputs - (M : SnakeWord → ℝ[X]) (P G : ℕ → ℝ[X]) : Prop where - auxiliaryGInterlacing : AuxiliaryGInterlacesStatement P G - affineNarayana : AffineModifiedNarayanaShiftedInterlacingStatement P - recurrence : GeneralizedSnakeRecurrenceStatement M P G - -/-- Bundled the combinatorial ingredients using shifted the affine-Narayana form and the -computable recurrence form. -/ -structure SnakeInterlacingComputableShiftedInputs - (M : SnakeWord → ℝ[X]) (P G : ℕ → ℝ[X]) : Prop where - auxiliaryGInterlacing : AuxiliaryGInterlacesStatement P G - affineNarayana : AffineModifiedNarayanaShiftedInterlacingStatement P - recurrence : GeneralizedSnakeRecurrenceComputableStatement M P G - -/-- Convert computable combinatorial inputs into the predicate-form bundle. -/ -theorem snakeInterlacingInputs_of_computable - {M : SnakeWord → ℝ[X]} {P G : ℕ → ℝ[X]} - (hinputs : SnakeInterlacingComputableInputs M P G) : - SnakeInterlacingInputs M P G where - auxiliaryGInterlacing := hinputs.auxiliaryGInterlacing - affineNarayana := hinputs.affineNarayana - recurrence := snakeRecurrence_of_snakeRecurrenceComputable hinputs.recurrence - -/-- Convert shifted combinatorial inputs into the paper-shaped bundle. -/ -theorem snakeInterlacingInputs_of_shifted - {M : SnakeWord → ℝ[X]} {P G : ℕ → ℝ[X]} - (hinputs : SnakeInterlacingShiftedInputs M P G) : - SnakeInterlacingInputs M P G where - auxiliaryGInterlacing := hinputs.auxiliaryGInterlacing - affineNarayana := affineModifiedNarayanaInterlacing_of_shifted hinputs.affineNarayana - recurrence := hinputs.recurrence - -/-- Convert computable shifted combinatorial inputs into the paper-shaped -computable bundle. -/ -theorem snakeInterlacingComputableInputs_of_shifted - {M : SnakeWord → ℝ[X]} {P G : ℕ → ℝ[X]} - (hinputs : SnakeInterlacingComputableShiftedInputs M P G) : - SnakeInterlacingComputableInputs M P G where - auxiliaryGInterlacing := hinputs.auxiliaryGInterlacing - affineNarayana := affineModifiedNarayanaInterlacing_of_shifted hinputs.affineNarayana - recurrence := hinputs.recurrence - -/-- Convert computable shifted combinatorial inputs into the predicate-recurrence -shifted bundle. -/ -theorem snakeInterlacingShiftedInputs_of_computable - {M : SnakeWord → ℝ[X]} {P G : ℕ → ℝ[X]} - (hinputs : SnakeInterlacingComputableShiftedInputs M P G) : - SnakeInterlacingShiftedInputs M P G where - auxiliaryGInterlacing := hinputs.auxiliaryGInterlacing - affineNarayana := hinputs.affineNarayana - recurrence := snakeRecurrence_of_snakeRecurrenceComputable hinputs.recurrence - -/-- Feed the bundled combinatorial ingredients into the abstract snake-interlacing -induction route. -/ -theorem snakeInterlacing_of_combinatorialInputs - {M : SnakeWord → ℝ[X]} {P G : ℕ → ℝ[X]} - (hroute : SnakeInterlacingInductionRouteStatement M P G) - (hinputs : SnakeInterlacingInputs M P G) : - NonNestingRookInterlacingStatement M := - hroute hinputs.auxiliaryGInterlacing hinputs.affineNarayana hinputs.recurrence - -/-- Feed computable combinatorial ingredients into the abstract snake-interlacing -induction route. -/ -theorem snakeInterlacing_of_combinatorialComputableInputs - {M : SnakeWord → ℝ[X]} {P G : ℕ → ℝ[X]} - (hroute : SnakeInterlacingInductionRouteStatement M P G) - (hinputs : SnakeInterlacingComputableInputs M P G) : - NonNestingRookInterlacingStatement M := - snakeInterlacing_of_combinatorialInputs hroute - (snakeInterlacingInputs_of_computable hinputs) - -/-- Feed shifted combinatorial ingredients into the abstract snake-interlacing induction -route. -/ -theorem snakeInterlacing_of_combinatorialShiftedInputs - {M : SnakeWord → ℝ[X]} {P G : ℕ → ℝ[X]} - (hroute : SnakeInterlacingInductionRouteStatement M P G) - (hinputs : SnakeInterlacingShiftedInputs M P G) : - NonNestingRookInterlacingStatement M := - snakeInterlacing_of_combinatorialInputs hroute - (snakeInterlacingInputs_of_shifted hinputs) - -/-- Feed computable shifted combinatorial ingredients into the abstract Theorem -4.1 induction route. -/ -theorem snakeInterlacing_of_combinatorialComputableShiftedInputs - {M : SnakeWord → ℝ[X]} {P G : ℕ → ℝ[X]} - (hroute : SnakeInterlacingInductionRouteStatement M P G) - (hinputs : SnakeInterlacingComputableShiftedInputs M P G) : - NonNestingRookInterlacingStatement M := - snakeInterlacing_of_combinatorialComputableInputs hroute - (snakeInterlacingComputableInputs_of_shifted hinputs) - end GeneralizedSnakePosets end RealRooted diff --git a/RealRooted/Production.lean b/RealRooted/Production.lean index 1681c14fa..817b2c934 100644 --- a/RealRooted/Production.lean +++ b/RealRooted/Production.lean @@ -427,7 +427,6 @@ import RealRooted.GeneralizedSnakePosets.Narayana.Recurrence import RealRooted.GeneralizedSnakePosets.Narayana.RootSums import RealRooted.GeneralizedSnakePosets.Narayana.Turan import RealRooted.GeneralizedSnakePosets.Narayana.TuranCertificates -import RealRooted.GeneralizedSnakePosets.CombinatorialPackages import RealRooted.GeneralizedSnakePosets.SnakeBoard import RealRooted.GeneralizedSnakePosets.SnakeCover import RealRooted.GeneralizedSnakePosets.SnakeReachability @@ -1369,7 +1368,6 @@ import RealRooted.GeneralizedSnakePosets.ChainPolynomial import RealRooted.GeneralizedSnakePosets.SnakeBand import RealRooted.GeneralizedSnakePosets.SnakeConstant import RealRooted.GeneralizedSnakePosets.SnakeRecurrence -import RealRooted.GeneralizedSnakePosets.SnakeInterlacing import RealRooted.GeneralizedSnakePosets.TruncatedStaircase.ColumnRecurrence import RealRooted.Challenges.LiuOppositeSigns import RealRooted.Challenges.PerronFrobenius