arxiv: 2604.02964 · v1 · submitted 2026-04-03 · 🧮 math.CO · math.PR

Recognition: 2 theorem links

· Lean Theorem

The record statistic and forward stability of Schubert products

Andrew Hardt , Reuven Hodges , Hanzhang Yin

Authors on Pith no claims yet

Pith reviewed 2026-05-13 18:52 UTC · model grok-4.3

classification 🧮 math.CO math.PR

keywords Schubert polynomialsforward stabilityrecord statisticleft-to-right maximapermutation avoidance132-avoiding231-avoidingBoolean permutations

0 comments

The pith

The record-set statistic is equidistributed on the 132-avoiding and 231-avoiding classes, forcing identical forward stability distributions for the corresponding Schubert products.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper initiates a probabilistic study of forward stability in Schubert polynomial products by tracking the record statistic, or left-to-right maxima, on pairs of permutations. It derives record probabilities for three families: uniform random permutations, Grassmannian permutations, and Boolean permutations. Asymptotics for the mean together with limiting distributions follow for the uniform and Grassmannian cases, while the Boolean case yields linear growth of the mean plus an explicit time-inhomogeneous Markov chain that samples uniformly in linear time. The central new result is that the full record-set distribution is identical on the 132-avoiding and 231-avoiding classes, so their forward stability distributions coincide exactly.

Core claim

Building on the explicit record formula for forward stability, the record-set statistic is equidistributed on the avoidance classes of 132 and 231. Consequently the corresponding forward stability distributions coincide. Asymptotics for the mean and limiting distributions are obtained for uniform and Grassmannian permutations, while Boolean permutations exhibit linear-order growth of the mean together with an explicit time-inhomogeneous Markov chain yielding an exact linear-time uniform sampler.

What carries the argument

The record-set statistic of a permutation (the set of left-to-right maxima), which determines forward stability exactly via the explicit formula relating record positions to the number of stable steps in the product.

Load-bearing premise

The explicit record formula for forward stability applies without additional restrictions to uniform, Grassmannian, and Boolean permutations.

What would settle it

Enumerate all 132-avoiding and all 231-avoiding permutations of length 5 and compare the exact frequencies of each possible record set; any mismatch disproves equidistribution.

Figures

Figures reproduced from arXiv: 2604.02964 by Andrew Hardt, Hanzhang Yin, Reuven Hodges.

**Figure 1.1.** Figure 1.1: Empirical density histograms of FS(u, v) at n = 500 for the three sampling models considered in the paper: uniform permutations, Boolean permutations, and Grassmannian permutations. We obtain analogous results for BS(u, v) in Section 6. In the Boolean case, our analysis produces an explicit time-inhomogeneous Markov chain together with transition probabilities that can be turned into an exact uniform sa… view at source ↗

read the original abstract

We initiate a probabilistic study of forward stability for products of Schubert polynomials through the record statistic (left-to-right maxima) of permutations. Building on the explicit record formula for forward stability obtained by Hardt and Wallach, we study random pairs of permutations drawn from three natural families: uniform permutations, Grassmannian permutations, and Boolean permutations. For each family, we determine record probabilities and use them to analyze the asymptotic behavior of forward stability. For uniform and Grassmannian permutations, we obtain asymptotics for the mean together with limiting distribution results. For Boolean permutations, we prove linear-order growth of the mean, and our analysis also produces an explicit time-inhomogeneous Markov chain that yields an exact linear-time uniform sampler. Beyond these cases, we prove that the record-set statistic is equidistributed on the avoidance classes of $132$ and $231$, and consequently the corresponding forward stability distributions coincide. We conclude with conjectures for numerous further permutation classes and a conjectural recursive criterion for when two avoidance classes have the same record-set distribution.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper applies the Hardt-Wallach record formula to three permutation families to get asymptotics, limits, a linear-time sampler for Boolean cases, and equidistribution for 132/231 avoiders.

read the letter

The main takeaway is that this work brings a probabilistic lens to forward stability of Schubert products by studying the record statistic on uniform, Grassmannian, and Boolean permutations. For uniform and Grassmannian cases they extract mean asymptotics and limiting distributions. For Boolean permutations they establish linear growth of the mean and derive an explicit time-inhomogeneous Markov chain that gives an exact linear-time uniform sampler. They also prove the record-set statistic is equidistributed on 132- and 231-avoiding classes, so the forward stability distributions match there. These pieces are new relative to the cited prior work and give concrete outputs a reader can use right away. The derivations for the record probabilities appear to be done separately for each family, which keeps the circularity low. The main soft spot is the dependence on the Hardt-Wallach explicit record formula. The abstract does not show an explicit check that the formula's hypotheses hold for Grassmannian or Boolean permutations; if those families violate an unstated condition, the asymptotics, limits, and sampler would not follow. A referee would reasonably ask for that verification spelled out. The conjectures for other classes are stated clearly but left open, which is appropriate. This is aimed at algebraic combinatorialists already working on Schubert calculus or permutation pattern statistics. A reader following stability questions or record statistics will find the sampler and the equidistribution result useful. The paper is narrow but internally consistent once the formula application is confirmed, so it deserves a serious referee.

Referee Report

2 major / 1 minor

Summary. The paper initiates a probabilistic study of forward stability for products of Schubert polynomials via the record statistic (left-to-right maxima) on random pairs of permutations from three families: uniform, Grassmannian, and Boolean. Building on Hardt and Wallach's explicit record formula, it derives record probabilities, mean asymptotics and limiting distributions for uniform and Grassmannian cases, linear-order mean growth plus an explicit time-inhomogeneous Markov chain sampler for Boolean permutations, and equidistribution of the record-set statistic on 132- and 231-avoiding classes, together with conjectures for further avoidance classes.

Significance. If the central claims hold, the work supplies concrete asymptotic and distributional information linking permutation statistics to Schubert calculus, with the explicit linear-time uniform sampler for Boolean permutations and the equidistribution result for two avoidance classes constituting clear strengths that enable further exact and computational study. The conjectural recursive criterion for equal record-set distributions on avoidance classes also opens a natural direction for generalization.

major comments (2)

[Introduction and main results sections] Introduction and the sections deriving results for each family: the manuscript substitutes the Hardt-Wallach explicit record formula directly into the analyses for uniform, Grassmannian, and Boolean permutations without re-deriving the formula or verifying that its hypotheses (e.g., conditions on descent sets or inversion tables) hold for these structured families. All stated results—asymptotics and limiting distributions for uniform/Grassmannian, linear growth and the Markov-chain sampler for Boolean, and equidistribution for 132/231-avoiders—rest on this substitution; if the formula requires additional unstated conditions that fail for Grassmannian or Boolean permutations, none of the claims follow.
[Equidistribution section] Section deriving the equidistribution result: the proof that the record-set statistic is equidistributed on the avoidance classes of 132 and 231 likewise rests on substituting the same Hardt-Wallach formula; an explicit check that the formula's hypotheses are satisfied on these avoidance classes is needed to support the claim that the corresponding forward-stability distributions coincide.

minor comments (1)

[Abstract] The abstract could state more explicitly that the results depend on substituting the Hardt-Wallach formula, to make the foundational reliance clear to readers.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their careful reading and constructive comments. We address the major concerns point by point below and will revise the manuscript accordingly to incorporate explicit verifications.

read point-by-point responses

Referee: [Introduction and main results sections] Introduction and the sections deriving results for each family: the manuscript substitutes the Hardt-Wallach explicit record formula directly into the analyses for uniform, Grassmannian, and Boolean permutations without re-deriving the formula or verifying that its hypotheses (e.g., conditions on descent sets or inversion tables) hold for these structured families. All stated results—asymptotics and limiting distributions for uniform/Grassmannian, linear growth and the Markov-chain sampler for Boolean, and equidistribution for 132/231-avoiders—rest on this substitution; if the formula requires additional unstated conditions that fail for Grassmannian or Boolean permutations, none of the claims follow.

Authors: The Hardt-Wallach formula is stated for arbitrary permutations and imposes no further restrictions beyond the standard definitions of descent sets and inversion tables. To address the referee's concern and improve the manuscript's self-containment, we will add a new subsection verifying that these hypotheses hold for Grassmannian permutations (via their descent sets) and Boolean permutations (via their inversion tables); the uniform case is immediate. These checks will confirm that the asymptotics, limiting distributions, linear growth, Markov sampler, and equidistribution results all follow directly from the formula. revision: yes
Referee: [Equidistribution section] Section deriving the equidistribution result: the proof that the record-set statistic is equidistributed on the avoidance classes of 132 and 231 likewise rests on substituting the same Hardt-Wallach formula; an explicit check that the formula's hypotheses are satisfied on these avoidance classes is needed to support the claim that the corresponding forward-stability distributions coincide.

Authors: We agree that an explicit verification strengthens the equidistribution claim. In the revised manuscript we will insert a short verification that 132-avoiding and 231-avoiding permutations satisfy the descent-set and inversion-table conditions of the Hardt-Wallach formula. This will rigorously justify that the record-set statistic is equidistributed on these classes and that the associated forward-stability distributions therefore coincide. revision: yes

Circularity Check

0 steps flagged

No circularity: prior formula applied to derive independent new results per family

full rationale

The paper cites the explicit record formula from Hardt and Wallach (with author overlap on Hardt) as the starting point and then computes record probabilities, mean asymptotics, limiting distributions for uniform and Grassmannian cases, linear growth plus an explicit time-inhomogeneous Markov chain sampler for Boolean permutations, and a new equidistribution proof for 132- and 231-avoiders. No equation or claim reduces by construction to a fitted parameter, self-definition, or renaming of a known result; the prior formula functions as an external input whose applicability is taken as given for the three families, after which all stated results are freshly derived. This is standard non-circular use of prior work and leaves the derivation self-contained.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claims rest on the explicit record formula from Hardt-Wallach (prior work) together with standard definitions of Schubert polynomials, permutation statistics, and pattern avoidance; no new free parameters or invented entities are introduced.

axioms (2)

standard math Standard definitions of Schubert polynomials and their products
Invoked throughout to define forward stability.
domain assumption The explicit record formula for forward stability from Hardt and Wallach
Cited as the foundation for all subsequent record-probability calculations.

pith-pipeline@v0.9.0 · 5477 in / 1415 out tokens · 45803 ms · 2026-05-13T18:52:49.592036+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Constants.lean, Cost/FunctionalEquation.lean phi_golden_ratio, phi_fixed_point echoes

?

echoes
ECHOES: this paper passage has the same mathematical shape or conceptual pattern as the Recognition theorem, but is not a direct formal dependency.

P(Rj(w)=1) = F_{2n-2} - F_{2j-4} F_{2(n-j)-1} / F_{2n-1} = [2ϕ^{2n-2} + …] / [√5 (ϕ^{2n-1} + ϕ^{1-2n})]
IndisputableMonolith/Foundation/ArithmeticFromLogic.lean LogicNat recovery, embed_eq_pow echoes

?

echoes
ECHOES: this paper passage has the same mathematical shape or conceptual pattern as the Recognition theorem, but is not a direct formal dependency.

|B_n| = F_{2n-1}; block-tag word bijection and recurrence U_m(0)=F_{2m+1}, U_m(1)=F_{2m+2}

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

3 extracted references · 3 canonical work pages

[1]

26 [DP09] Devdatt P

Update of, and a supplement to, the 1986 original. 26 [DP09] Devdatt P. Dubhashi and Alessandro Panconesi.Concentration of Measure for the Analysis of Randomized Algorithms. Cambridge University Press, Cambridge,

work page 1986
[2]

When do Schubert polynomial products stabilize?arXiv preprint arXiv:2412.06976, December

22 [HW24] Andrew Hardt and David Wallach. When do Schubert polynomial products stabilize?arXiv preprint arXiv:2412.06976, December

work page arXiv
[3]

1, 3, 35 [HW25] Andrew Hardt and David Wallach

Preprint. 1, 3, 35 [HW25] Andrew Hardt and David Wallach. Stability of products of double Grothendieck polynomials.Int. Math. Res. Not. IMRN, 2025(22):Paper No. rnaf338, 15,

work page 2025