Theoretical Computer Science

Nearly every measure of Boolean function complexity was known to be equivalent — except sensitivity. Proving the conjecture unified the whole picture.

Motivation

A polynomial threshold function makes a Boolean decision by evaluating a real polynomial and keeping only its sign. Its average sensitivity measures how often that decision changes after one uniformly chosen input coordinate is reversed, summed over all coordinate choices. This is a basic quantitative question in the analysis of Boolean functions: how much can a low-degree decision rule vary across the edges of the Boolean cube?

The result collected here is a uniform bound with an explicit coefficient. The OpenAI weighted-grading development supplies a complete coefficient-eight construction. Lagdive, Aglave and Damre sharpen its probability estimate and obtain the sufficient coefficient 3.83. The present fixed-source development formalizes the refined estimate, extracts the coefficient 3.762, and connects it to the full polynomial-threshold statement.

This mission organizes that completed result and its reusable supporting theorems. Its goal and both milestones already have accepted Lean proofs. It does not present the coefficient as optimal, and it makes no claim of exhaustive historical priority.

Setting

Let $n,d$ be positive integers, and let $p$ be a real polynomial in $n$ variables with total degree at most $d$. Choose an input $x$ uniformly from the sign cube $\{-1,1\}^n$. For a coordinate $i$, write $x^{\oplus i}$ for the same input with coordinate $i$ negated. The threshold convention is

In particular, a zero of the polynomial is assigned the positive sign. The average sensitivity is

For the scalar supporting statements, let $B_n$ have the symmetric binomial distribution with parameters $n$ and $1/2$. Its mean absolute deviation is

The accompanying definition module fixes this finite sum and the normalized central coefficient $c_k=4^{-k}\binom{2k}{k}$. These definitions contain no estimates or unproved hypotheses.

Formalization targets

Goal — the coefficient 3.762 for arbitrary real polynomials

For every $n,d\ge1$ and every real polynomial of total degree at most $d$, prove

The goal is the published theorem AverageSensitivity.polynomial_bound_3762_general. It has no multilinearity hypothesis and no requirement that $d\le n$. The narrower range $1\le d\le n$ used by the Big O board is therefore included. The goal's fixed coefficient records this particular verified result; a future sharper coefficient would be a separate statement.

Milestone 1 — the refined finite one-sided coupling estimate

Let a finite set carry nonnegative probability weights $w$, and let real functions $U,V$ have identical weighted distributions. Let $m$ be any real centre and let $a\ge0$. If $V-U\le a$ on the support of the weights, prove

This is the finite form of the first estimate in Lemma 2 of Lagdive, Aglave and Damre. The centre is arbitrary; independence, exchangeability and a two-sided displacement bound are not hypotheses. Its published formalization is already proved.

Milestone 2 — exact extraction of the universal coefficient

For positive integers $n,d$ and a real number $A$, prove the scalar implication

This is AverageSensitivity.extract_constant. Its statement is independent of the polynomial and matrix constructions. It records the coefficient extraction proved in this development, rather than attributing 3.762 to the earlier paper.

Significance and current status

The result gives one coefficient that works simultaneously for every positive dimension and degree. Such uniformity distinguishes it from estimates that hold only for a fixed degree or only as the dimension tends to infinity. It also preserves the stated convention at polynomial zeros, so the class of threshold functions is unchanged at the boundary.

The formal contribution is a complete connection from the polynomial and the actual finite cube to the numerical bound. The final theorem does not assume the existence of a grading, an energy bound, a coupling estimate or a small-dimension certificate. Those mathematical components are discharged inside the proof chain. The two supporting milestones are independently importable results, and the live dependency graph records both as actual prerequisites of the goal's accepted reduction.

All three theorem nodes are currently Proved. The closed repository proof was rebuilt with Lean 4.33.1 and the platform's Mathlib revision, and an independent Linux build also passed. The final theorem's axiom dependencies are exactly propext, Classical.choice and Quot.sound. These checks establish the formal result under the displayed definitions; they do not establish optimality of the coefficient or independent human peer review.

Difficulty

A one-sided bound on the difference of two variables does not by itself bound the difference in the opposite direction. The equal-distribution condition is therefore essential to the coupling milestone. Omitting it would change the problem into a false assertion. In the polynomial application, the relevant distributions also have to come from the actual block masses of the constructed grading; treating those masses or the grading properties as free assumptions would omit the central analytic work.

The constant extraction must cover all admissible dimension-degree pairs. A calculation for finitely many dimensions cannot establish the universal statement, while an asymptotic first-moment estimate can leave uncontrolled small dimensions or degree-dependent errors. The formal target includes both the infinite range and every exceptional finite case. Numerical optimization and floating-point experiments are not premises of the accepted result.

Formalization scope

Cube vertices are functions Fin n → Bool, interpreted coordinatewise as signs. A coordinate flip is an explicit function update, and each probability is a finite cardinality divided by $2^n$. The polynomial is a Mathlib MvPolynomial (Fin n) ℝ; the degree bound refers to its total degree. General polynomial inputs are included through a proved value-preserving, degree-nonincreasing multilinearization. Positive dimensions ensure the normalizing denominator is nonzero. Degree zero and dimension zero are outside the displayed goal's quantifiers.

The two definition references provide the original cube/threshold interface and the exact scalar moment interface. The coupling milestone uses finite weighted sums, so equality of distributions is stated for every real test function without additional measurability assumptions. The scalar milestone quantifies over an arbitrary real $A$ satisfying its two explicit upper bounds. The main goal has no analogous auxiliary assumptions.

This is a Research Paper mission for a completed fixed-source development, with the main theorem and both milestones linked by their existing identities. It creates no duplicate theorem statements. Alternative proofs and subsequent sharper bounds can reuse these interfaces, but they are not claimed as completed by this mission. The construction and earlier probability refinement remain attributed to their original sources. Proof development and source preparation used OpenAI Codex.

Selected references

• OpenAI, Average sensitivity of polynomial threshold functions, preprint and Lean source, 2026. Fixed Lean development.
• Prathmesh Lagdive, Vaibhav Aglave and Suraj Damre, An elementary improvement of the average sensitivity bound for polynomial threshold functions, 2026, Lemma 2 and the dimension-degree estimate. Fixed manuscript source.
• Anchen0823, Average sensitivity: a Lean proof with coefficient 3.762, source development, 2026. Verified source revision. Prove2Me accepted main submission: 0f539328-c783-4509-a78e-a86ac777468c.

Why offer sets with overbooking matter

A firm with $k$ open positions often cannot interview and offer sequentially: hiring seasons are short, and offers go out in one batch. Some recipients decline, so the firm overbooks, sending more offers than it has positions, and pays for every hire beyond capacity. The same trade-off appears in airline and hotel overbooking and in university admissions. Epstein and Ma (arXiv:2210.04059v3, Operations Research 2024) study this Simultaneous Offering problem as one of three hiring-pipeline models, and analyse the natural class of value-ordered policies, which offer to the best candidates first. Their Theorem 3 shows that a value-ordered policy built from a linear-programming relaxation guarantees a fraction $\alpha^\tau_k$ of the optimum when every value is at least $\tau$. This mission formalizes the converse, Theorem 4: no value-ordered policy can guarantee more than $\beta^\tau_k$.

Setting

An instance has $k \ge 1$ positions and $n \ge k$ candidates. Candidate $i$ accepts an offer with probability $p_i \in [0,1]$, independently of the others, and then adds value $v_i \ge 0$. The firm chooses a set $S$ of candidates and sends all offers at once. If $A \subseteq S$ is the random set of acceptances, the reward is

so each hire beyond capacity costs $1$ (the paper rescales values so that this cost is $1$). Write $R(I, S)$ for the expected reward of offering to $S$, and $\mathrm{OPT}_{\mathrm{sim}}(I) = \max_S R(I, S)$ for the best expected reward; randomizing over offer sets cannot do better.

Candidates are labelled so that $v_1 \ge v_2 \ge \cdots \ge v_n$. A value-ordered policy with parameter $m \in [n]$ offers to $\{1, \dots, m\}$. An instance is $\tau$-bounded, $I \in \mathcal{I}^\tau_{\mathrm{sim}}$, if $v_i \ge \tau$ for all $i$. Without such a bound value-ordered policies can be arbitrarily poor (§6.1); $\tau$ measures how soft the capacity is, from nearly hard ($\tau$ close to $0$) to nearly compensated by any hire ($\tau$ close to $1$), and both theorems take $\tau \in (0,1)$.

For $\lambda \ge 0$ let $\mathbb{E}[\min\{\mathrm{Pois}(\lambda), k\}]$ be the mean of a Poisson variable truncated at $k$, and

In Lean these are SimInstance, reward, OPTsim, valueOrdered, TauBounded, expMinPois, ratioObj, alpha and beta in the namespace HiringLP.SimUpper.

Formalization targets

Goal: Theorem 4 (p. 30)

For every $k \ge 1$, $\varepsilon > 0$ and $\tau \in (0,1)$ there is a valid, sorted instance $I \in \mathcal{I}^\tau_{\mathrm{sim}}$ with $k$ positions such that

Milestones on the hard instance (App. D.7)

The instance has $j^2$ type-1 candidates with $p_i = k/j$, $v_i = \tau + \delta$, $\delta = \varepsilon\tau/j$, and $k$ type-2 candidates with $p_i = 1$, $v_i = \tau$. With $B \sim \mathrm{Bin}(m, k/j)$ and $0 \le m \le j^2$:

Companions: the maximisers (App. D.8)

Proposition EC.5: optimal $s^*_\alpha$, $s^*_\beta$ exist, $s^*_\alpha = \min\{s^*_\beta, 1\}$, and $\tau = 1 - e^{-s^*_\beta k}\sum_{j<k} (s^*_\beta k)^j/j!$. Proposition EC.6: $s^*_\alpha = s^*_\beta$ if and only if $\tau \le 1 - e^{-k}\sum_{j<k} k^j/j!$, which holds whenever $\tau \le 1/2$.

Significance

Theorem 4 bounds what any value-ordered policy can guarantee on $\tau$-bounded instances, against the true optimum rather than an LP relaxation. With Theorem 3 it brackets the best guarantee of the class between $\alpha^\tau_k$ and $\beta^\tau_k$, and by Proposition EC.6 the two coincide when $\tau \le \Pr[\mathrm{Pois}(k) \ge k]$, in particular for all $k$ when $\tau \le 1/2$. In that region the paper's truncated-LP policy is the best value-ordered policy in the worst case. The instance also shows why the restriction to value-ordered policies costs something: the optimum offers to the reliable type-2 candidates, while a value-ordered policy must first exhaust the slightly more valuable unreliable ones.

The results are proved in the paper. None of them has a machine-checked proof; this mission produces a formal version of Theorem 4 and the finite-$j$ estimates on which its proof rests, together with a reusable finite-sum encoding of independent acceptances, truncated Poisson and Binomial expectations, and the constants $\alpha^\tau_k$, $\beta^\tau_k$.

Difficulty

The milestones are exact identities and inequalities at a fixed $j$; the hard part is the passage to the limit. The page's proof lets $j \to \infty$ with $m_j/j \to s$ and replaces $\mathrm{Bin}(m_j, k/j)$ by $\mathrm{Pois}(sk)$. The goal, however, asks for one finite instance on which the bound holds for every $m$ simultaneously, including $m$ of order $j^2$ and the values $m > j^2$ that also offer to type-2 candidates. A pointwise limit for each fixed $s$ does not give this; the Binomial–Poisson error has to be controlled uniformly in $m$, and the error must fit inside the slack $\varepsilon$, part of which the term $\delta$ already uses. Note also that the comparison runs the wrong way for the obvious argument: $\min\{\cdot, k\}$ is concave and the Binomial is less spread than the Poisson, so $\mathbb{E}[\min\{k, B\}]$ is at least its Poisson counterpart and a one-sided comparison cannot replace an approximation bound.

Formalization scope

All randomness is finite. The expected reward is an explicit sum over the $2^n$ accepting sets with product probabilities; the Binomial pmf, its truncated mean and its tail are finite sums written by hand. The truncated Poisson mean is the series with the Poisson pmf. All quantities are real. Candidates are Fin n, so the paper's candidate $i$ is index $i - 1$; sortedness is the hypothesis Antitone v in Valid, which also contains $1 \le k \le n$, $p \in [0,1]^n$ and $v \ge 0$. $\mathrm{OPT}_{\mathrm{sim}}$ is the maximum over all offer sets, never over value-ordered ones. $\beta^\tau_k$ is the supremum over $[0, \infty)$ and $\alpha^\tau_k$ over $[0, 1]$. The page leaves $k$ implicit in $\beta^\tau_k$; the goal quantifies over every $k \ge 1$ and requires the instance to have exactly $k$ positions. The quantifiers are "for all $k, \varepsilon, \tau$, there is an instance, for all $m$".

The goal does not fix the hard instance: any instance proves it. A formalization in which the comparison is with the best value-ordered policy, in which $\beta^\tau_k$ is a free parameter, or in which the reward is defined by the proof's Binomial formula would be a different statement and is ruled out by the definitions above. The definitions are not specialized to the hard instance, which appears only as a separate definition used by the milestones.

A complete development needs: finite sums over subsets with product weights and the reduction to a Binomial count for identical candidates; summability and continuity of the truncated Poisson mean; a Binomial–Poisson approximation bound uniform in the number of trials; concavity of $f_{k,\tau}$ in $s$. The Poisson and Binomial infrastructure is reusable well beyond this mission. Proofs of the milestones, of the companions, and of auxiliary approximation lemmas are all welcome.

Selected references

• B. Epstein, W. Ma, Selection and Ordering Policies for Hiring Pipelines via Linear Programming, arXiv:2210.04059v3, 2023; Operations Research, 2024. https://arxiv.org/abs/2210.04059
• M. Mitzenmacher, E. Upfal, Probability and Computing, 2nd ed., Cambridge University Press, 2017 (Exercise 5.14, cited for $\Pr[\mathrm{Pois}(k) \ge k] \ge 1/2$). https://doi.org/10.1017/9781316651124
• A. D. Barbour, P. Hall, On the rate of Poisson convergence, Mathematical Proceedings of the Cambridge Philosophical Society 95, 1984. https://doi.org/10.1017/S0305004100061402

Verified completion - 15 October 2026

The original exact goal EndStatement.ThreeSum.SolvedInTime 1.960614 is Proved on Prove2Me. All seven original milestones are complete. The complete machine extension has 481 accepted theorem proofs and reuses 110 proved theorem nodes; its accepted dependencies connect to the original main reduction. The independent fixed-model lower bound remains separate from the algorithm proof. Scientific priority and global optimality are not asserted by these formal verification results.

Why improve the deterministic integer 3SUM exponent?

3SUM asks whether three entries at distinct positions in an integer input sum to zero. Its familiar quadratic algorithm makes it a benchmark for studying how much arithmetic structure can reduce the cost of an exhaustive search. The relevant comparison is the exponent of input size in a precisely specified machine model. An improvement to that exponent is an asymptotic statement; it need not provide better measured running times at accessible input sizes.

Alman and Vassilevska Williams, 2026 developed a deterministic truly subquadratic framework for polynomially bounded integer 3SUM. The c0ldzy17 source snapshot, dated 11 October 2026, develops a subsequent deterministic construction with a formally stated 1.962 target. The author-supplied certificate package 3sum_certificate_1p960614_v3, dated 14 October 2026, studies a further parameter and switch refinement. It contains mathematical arguments and exact rational checks, and explicitly leaves the complete modified machine-program theorem unproved. This mission studies that remaining extension together with its supporting certificates.

Inputs, word instructions and analytic quantities

An input of size $n$ is an integer-valued function on the positions $0,\ldots,n-1$. For each fixed natural number $\kappa$, every value has absolute value at most $n^\kappa$. A YES instance has pairwise distinct positions $i,j,k$ satisfying $x_i+x_j+x_k=0$. Equal values at different positions are allowed. The problem asks for a decision, so a successful algorithm need not return the positions. Inputs of size less than three are NO instances.

The word RAM is the existing campaign foundation specification. A program is a finite list of instructions for constants, arithmetic, direct and indirect memory access, branching, acceptance and rejection. Words have a fixed width and a signed integer interpretation. For each fixed $\kappa$, one program, one word-width constant and one time function must work for every input size and every sufficiently large word width. The mission retains that specification without introducing an alternative computation model.

The supporting binary entropy is measured in bits:

For an integer expansion $c\ge3$, write

These are analytic quantities used to describe local encoding and reporting costs. The source's twelve charges also depend on a representation-scale parameter $e$, a band shift $b$, a box saving $S$, an initial threshold $\theta$, a terminal fraction $\tau$, and a uniform entropy coefficient $\rho$.

Formalization targets

The campaign goal is the exact proposition

For $1.960614=980307/500000$, its time requirement is

Correctness and termination still cover all input sizes. The integer-size exponent includes $\kappa=0$, and the same program must be correct for every word width above its specified threshold.

The primary certificate uses $c=232$ and the rational quartic

Supporting targets establish its validity on $[0,1/2]$, its derivative and tangent bounds, and the uniform inequality $H(t)<0.27905030(1+P(t))$. The fixed parameters are $e=0.203889696$, $b=-0.062656016$, $S=0.193175570$, $\theta=0.040409899$, and $\tau=13/20$. The parameter theorem bounds every one of the twelve costs strictly below $1.96061388<1.960614$. Integer scheduling and general local-cover identities are separate milestones. A further independent milestone proves $R>1.96061349120$ for the explicitly defined relaxed fixed-expansion cost model. That model bound concerns its admissible parameter tuples; it is not a lower bound for 3SUM itself.

What these results establish

The supplied certificate demonstrates that a quartic switch already suffices for the proposed 1.960614 cost target. It also separates a uniform analytic inequality from a numerical experiment: the statement quantifies over the full closed interval. Its finite scheduling statement uses integer comparisons and accounts for the rounding error at every admissible level, rather than requiring executable logarithms.

Formalization adds checked statements about these continuous and finite objects and a reusable dependency structure. The full campaign goal requires an additional result: the actual modified program must obey the certified costs, and its operational correctness must reach the foundation specification. The upstream parameter certificate likewise distinguishes its exponent ledger from its separate implementation obligations. An exact rational checker passing is evidence for the numerical certificates; it does not establish the full new machine theorem.

Why the program extension remains substantive

Changing expansion from 256 to 232 changes the local universe and the vertex, output and degree counts together. The representation scale, band denominator and polynomial switch also change. Consequently, the original fixed-parameter runtime result cannot simply be invoked after replacing a few numerical constants. The new local construction, global encoding, sparse queries, reporting and arithmetic operations must share consistent parameters and a complete cost account.

The small gap between the principal cost cap and the target must absorb the proved subpolynomial overheads, including exceptional-size handling and the conversion to word instructions. The machine bridge has now been proved in this mission. Its accepted dependency tree connects the modified program and its runtime analysis to the unchanged campaign specification. Its statement has no assumed solver callback or unproved runtime contract. The fixed-model lower-bound milestone is an independent analytic root, and is not used to justify a faster algorithm.

Formalization scope and source boundaries

The campaign pins Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Entropy and its derived quantities are real-valued; the final exponent is rational; finite subset counts and cleared switch comparisons use natural numbers. Theorems explicitly restrict logarithmic arguments and denominators to their intended domains. Natural-number subtraction in the switch is used only below the final level, with positive even microblock size.

The local-cover milestone covers every natural $c\ge3$ and positive half-block size. The cost-model milestone quantifies over all tuples satisfying its written assumptions and includes a whole-interval entropy constraint. Neither finite testing nor a floating-point optimizer substitutes for these universal statements. The initial package includes no Lean proof of the new machine goal, and the mission does not represent it as an established record.

The underlying algorithms and formal infrastructure retain their attribution to Alman and Vassilevska Williams; Björklund, Husfeldt, Kaski and Koivisto; Swapnil Jain; c0ldzy17; Anthropic; Jihoon Hyun; and Lean/Mathlib, as documented by the upstream source. The certificate development and this formalization use AI assistance. Scientific priority and global optimality are outside the mission's claims.

Selected references

• Author-supplied 3SUM: Positive-Coefficient Entropy Switch, 1.960614 Cost Certificate and Fixed-Model Lower Bound, certificate package v3, 14 October 2026. Exact source: 3sum_certificate_1p960614_v3/3sum_certificate_v3/PROOF.md, Sections 0–8; certificates/c232_quartic.json; verify_certificate.py. This is a supplied research artifact, not a claimed public publication.
• c0ldzy17, Deterministic 3SUM in O(n^1.962): method and proof, source documentation, 2026. Pinned METHOD.md, Parameters.lean, and LocalCoverBounds.lean.
• Josh Alman and Virginia Vassilevska Williams, Truly Subquadratic 3SUM and Truly Subcubic APSP via Triangles in Sparse Lopsided Graphs, arXiv preprint, 2026. arXiv:2610.06783v1.
• Anthropic, Truly Subquadratic 3SUM and Truly Subcubic APSP, Lean formalization, 2026. Pinned formal-math source. The campaign imports its shared word-RAM statement.

Source code and complete Lean formalization: GitHub repository. Fixed source revision: 8c25c0325de5.

Why sharpen the integer 3SUM exponent?

3SUM asks whether an input sequence contains three entries at different positions whose sum is zero. The classical quadratic running time makes it a benchmark for fine-grained algorithm design: even a small fixed improvement in the exponent changes its asymptotic complexity. The setting here is polynomially bounded integers and a deterministic word RAM; the input-size exponent, rather than an experimental speedup, is the quantity being studied.

Alman and Vassilevska Williams (2026) give a deterministic truly subquadratic integer 3SUM algorithm through thin matrix products and reductions involving Exact Triangle. Xu's manuscript, Deterministic Integer 3SUM in O(n^1.999017) Time via a Sharper Binomial-Tail Analysis, dated 13 October 2026, refines the analysis of that framework. Its claimed bound is the formalization target here. The Hexagon link identifies the author's submission page, which may require authentication; it is not presented as a public article identifier or evidence of peer review.

Inputs, machine model, and analytic quantities

An input of size $n$ is a function $x:\{0,\ldots,n-1\}\to\mathbb Z$. For a fixed natural number $\kappa$, every entry obeys $|x_i|\le n^\kappa$. Acceptance means that there are pairwise distinct indices $i,j,k$ with $x_i+x_j+x_k=0$. Repeated values at different positions are allowed. This is a decision problem, so the algorithm need not return a witness triple.

The word-RAM specification is the campaign's existing EndStatement definition, imported from its foundation mission. For each fixed $\kappa$, one finite deterministic program, one word-width threshold constant, and one time-bound function must work for all input sizes and all word widths above that threshold. Words have finite signed interpretations; arithmetic, indirect memory access, branching, acceptance, and rejection are defined operationally. The result concerns this exact model.

For the supporting analysis, let $H(u)=-u\log u-(1-u)\log(1-u)$, with endpoint values $H(0)=H(1)=0$. All logarithms are natural. For an integer $c>10$, a positive integer $m$, and $0<\theta<0.9$, set $L=cm$, $D=4^m$, $t=\lceil\theta m\rceil$, and

The sharp preprocessing saving, query exponent, and encoding exponent are

These auxiliary definitions describe costs; they neither redefine 3SUM nor assume the existence of a fast algorithm.

Formalization targets

The campaign goal is the exact fixed bound

The first supporting milestone is the two-sided binomial entropy estimate. The second is the manuscript's normalized tail bound

A further milestone establishes strict improvement over the earlier preprocessing saving $\gamma(c,\theta)=\theta\log((c-1)/9)/\log4$ at fixed parameters. The algorithmic milestone combines the manuscript's Propositions 4.1 and 5.1: admissible sharp-tail parameters must yield a program satisfying the shared 3SUM specification, not merely a numerical inequality.

The final supporting milestone certifies the exact choice

It includes the preprocessing, query, encoding, prime-selection, and instance-construction inequalities, together with

Every terminating decimal denotes an exact rational number. The target is the fixed big-$O$ exponent 1.999017; the smaller cutoff is accompanied by residual asymptotic losses in the manuscript and is not asserted as the same fixed bound.

What completing this mission would establish

A complete proof would certify the manuscript's improved integer 3SUM bound in the campaign's common machine model. The gain is an analysis refinement of the inherited algorithm and reductions. It does not claim a new algorithmic framework, optimal parameters, global optimality, or priority over all other work.

The manuscript also gives an auxiliary $O(n^{1.999073})$ bound by retuning the previous estimate. That weaker result is background, not this mission's campaign value. The existing upstream formalization is prior work; it does not automatically certify either refinement. The supplied rational interval verifier checks the parameter inequalities, but those checks alone do not prove a word-RAM running-time theorem. The main goal and the newly drafted supporting statements remain open Lean proof obligations.

Where the difficulty lies

A better tail estimate is insufficient unless every other cost remains within the final budget. Shared encoding work, all queries, deterministic prime selection, witness scanning, and instance construction must be included. The word-size and address bounds must remain valid after changing parameters. Ceiling operations, restricting $D$ to powers of four, and bounded-size exceptions must also be handled.

The central formalization burden is the connection between the analytic estimates and an actual deterministic program. Assuming an oracle with the desired running time would remove that burden and would not establish the stated target. Likewise, checking a finite range of sizes or a floating-point optimizer's output cannot establish the universal algorithmic statement.

Formalization scope and conventions

The environment is Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. The foundation reference and the campaign goal's import are retained. Supporting definitions use real logarithms, real powers, natural binomial coefficients, finite sums, and a natural ceiling. Domain hypotheses exclude invalid entropy-tail regimes; endpoint binomial cases are included explicitly.

For $r=1999017/1000000$, the shared time predicate means that there exists $K\in\mathbb N$ such that $T(n)^{1000000}\le K n^{1999017}$ for every $n\ge2$. Correctness and termination still cover every input size, including $n<3$. The manuscript's $\kappa\ge1$ convention must be extended to the campaign's $\kappa=0$ case, and its word-size analysis must justify uniform correctness at every sufficiently large word width. Both are explicit interface obligations.

Reusable contributions include entropy and tail estimates, rigorous logarithm enclosures, and parameterized cost-to-program results. Existing compatible library results should be reused where available. The manuscript and metadata were prepared with AI assistance; this mission makes no claim of completed human review or completed formal verification of the improved bound.

Selected references

• Yuxuan Xu, Deterministic Integer 3SUM in O(n^1.999017) Time via a Sharper Binomial-Tail Analysis, manuscript, 13 October 2026. Author-supplied Hexagon submission page. Target: Theorem 1.1; supporting analysis: Sections 3–6.
• Josh Alman and Virginia Vassilevska Williams, Truly Subquadratic 3SUM and Truly Subcubic APSP via Triangles in Sparse Lopsided Graphs, arXiv preprint, 2026. arXiv:2610.06783v1. Inherited ingredients: Section 4, Lemma 29, Theorem 30, Corollary 31, and the deterministic reductions cited in Xu's Section 2.
• Anthropic, Truly Subquadratic 3SUM and Truly Subcubic APSP: a Lean 4 formalization, source repository, 2026. Pinned source at commit e1a4e6508154ea59f030480661590a9fe3018011. Its EndStatement.lean supplies the shared specification, not a proof of this mission's new exponent.

Motivation

The general number field sieve (GNFS) is the most efficient classical algorithm known for factoring integers larger than about $10^{100}$. Its heuristic running time for an integer $n$ is

super-polynomial but sub-exponential in the bit length of $n$. Every record factorization of a general RSA modulus of recent decades (RSA-768, RSA-240, RSA-250) was obtained with it, so the security margins of RSA key sizes are calibrated against it (Pomerance, A Tale of Two Sieves, 1996; Boudot et al., 2020).

Like the rational and quadratic sieves, GNFS works by producing a congruence of squares $x^2 \equiv y^2 \pmod n$ and then taking $\gcd(x-y,n)$. Its gain comes from searching for smooth values that are sub-exponential in the size of $n$, which forces the algorithm to compute in algebraic number fields.

Setting

Let $f \in \mathbb{Z}[x]$ be a polynomial of degree $d$ and $\theta \in \mathbb{C}$ a root of $f$. The number field $\mathbb{Q}(\theta)$ is the set of complex numbers $\sum_{i<d} a_i\theta^i$ with $a_i \in \mathbb{Q}$; it is $d$-dimensional over $\mathbb{Q}$ when $f$ is irreducible over $\mathbb{Q}$. The ring $\mathbb{Z}[\theta]$ is the subring of $\mathbb{C}$ generated by $\theta$; the ring of integers $\mathcal{O}_{\mathbb{Q}(\theta)}$ consists of the elements of $\mathbb{Q}(\theta)$ that are roots of monic integer polynomials. It contains $\mathbb{Z}[\theta]$ when $f$ is monic, and the two can differ.

GNFS chooses two irreducible integer polynomials $f_1, f_2$ with a common root $m$ modulo $n$, i.e. $n \mid f_1(m)$ and $n \mid f_2(m)$. A simple choice is the base-$m$ polynomial: write $n = a_d m^d + \dots + a_1 m + a_0$ with digits $0 \le a_i < m$, put $f_1(x) = \sum a_i x^i$ and $f_2(x) = x - m$. Pairs of integers $(a,b)$ (relations) are sieved so that both homogenized values $F_j(a,b) = b^{\deg f_j} f_j(a/b)$ are smooth; up to the leading coefficient these are the norms $N(a - b\theta_j)$. Linear algebra over $\mathbb{F}_2$ then selects a set $S$ of relations for which

Because $m$ is a root of both polynomials mod $n$, there are ring homomorphisms $\varphi_j : \mathbb{Z}[\theta_j] \to \mathbb{Z}/n\mathbb{Z}$ with $\varphi_j(\theta_j) = m$. Both send $\prod_S(a - b\theta_j)$ to $\prod_S(a - bm)$.

Formalization targets

Goal: the congruence of squares

For $f_1, f_2$ irreducible in $\mathbb{Z}[x]$ with complex roots $\theta_1,\theta_2$, a common root $m$ mod $n$, and $S$, $\gamma_1$, $\gamma_2$ as above:

This is the correctness statement of the algebraic part of GNFS: whatever relations the sieve and linear algebra produce, the square-root step yields $x = \varphi_1(\gamma_1)$, $y = \varphi_2(\gamma_2)$ with $n \mid x^2 - y^2$.

Supporting statements (milestones)

1. $[\mathbb{Q}(\theta):\mathbb{Q}] = d$ for $f$ irreducible over $\mathbb{Q}$.
2. $\mathbb{Z}[\theta]$ can be strictly smaller than the ring of integers.
3. The base-$m$ polynomial has digits $0\le a_i<m$ as coefficients and $f(m)=n$, so $m$ is a root mod $n$.
4. Existence of the homomorphism $\mathbb{Z}[\theta]\to\mathbb{Z}/n\mathbb{Z}$, $\theta\mapsto m$.
5. $c_d\,N_{\mathbb{Q}(\theta)/\mathbb{Q}}(a-b\theta) = b^d f(a/b)$, where $c_d$ is the leading coefficient.
6. If $n\mid x^2-y^2$, $n\nmid x-y$, $n\nmid x+y$, then $1<\gcd(x-y,n)<n$.
7. For odd $n$ with at least two prime factors and a unit $x$, at least half of the square roots of $x^2$ mod $n$ differ from $\pm x$ (the "probability at least $1/2$" of the final step).

Significance

The goal and milestones together certify that every output of the GNFS pipeline that passes the square-root step is a genuine congruence of squares, and that such a congruence splits $n$ with probability at least $1/2$ over the choice of square root. This is the part of the algorithm whose correctness is unconditional; the running-time bound is heuristic and is not a target here.

These results are classical and appear in standard references (Lenstra–Lenstra 1993; Crandall–Pomerance 2005, §6.2). The mission's contribution is a machine-checked formal version connecting number fields in $\mathbb{C}$, integer polynomials, and residue rings, which current libraries do not package for this purpose.

Difficulty

The ring homomorphism $\mathbb{Z}[\theta] \to \mathbb{Z}/n\mathbb{Z}$ is the delicate point. $\mathbb{Z}[\theta]$ is a subring of $\mathbb{C}$, not a quotient ring, so a map defined by $\theta \mapsto m$ is well defined only if every integer polynomial vanishing at $\theta$ is a multiple of $f$ in $\mathbb{Z}[x]$. This needs $f$ irreducible over $\mathbb{Z}$ (in particular primitive), via Gauss's lemma; for $f(x) = 2x$ and $n = 2$, every $m$ is a root mod $n$, but $\theta = 0$ only admits $\theta \mapsto 0$. The norm identity requires identifying $f/c_d$ as the minimal polynomial of $\theta$ and expressing the norm as a product over conjugates. The probability milestone needs the Chinese remainder theorem and counting square roots of units modulo odd prime powers.

Formalization scope

All statements live in the namespace GNFS. Number fields are realized inside $\mathbb{C}$: $\mathbb{Q}(\theta)$ is ℚ⟮θ⟯ and $\mathbb{Z}[\theta]$ is Algebra.adjoin ℤ {θ}. Residues mod $n$ are ZMod n with $n \in \mathbb{N}$ ($n = 0$ gives $\mathbb{Z}$, consistent with every statement). Two definitions are shared: GNFS.baseMPolynomial n m, the polynomial whose coefficients are the base-$m$ digits of $n$ (via Nat.digits), and GNFS.homogenize f a b $= \sum_{i\le d} c_i a^i b^{d-i}$.

Irreducibility "over the rationals" with integer coefficients is encoded as irreducibility in $\mathbb{Z}[x]$ (primitive and irreducible over $\mathbb{Q}$) where a homomorphism to $\mathbb{Z}/n\mathbb{Z}$ is needed. Without primitivity the claimed homomorphism can fail to exist. The goal asserts both the existence of the homomorphisms and the equality for every such pair, so it cannot be satisfied by the trivial choice $x = y$. The sieving, smoothness, linear-algebra and complexity aspects of the article are out of scope.

Reusable by-products: norms of linear elements in simple extensions, homomorphisms out of $\mathbb{Z}[\theta]$, and square-root counting in $\mathbb{Z}/n\mathbb{Z}$.

Selected references

• Wikipedia, General number field sieve, revision 1377718368. https://en.wikipedia.org/w/index.php?title=General_number_field_sieve&oldid=1377718368
• C. Pomerance, A Tale of Two Sieves, Notices of the AMS 43(12), 1996. https://www.ams.org/notices/199612/pomerance.pdf
• A. K. Lenstra, H. W. Lenstra Jr. (eds.), The development of the number field sieve, Lecture Notes in Math. 1554, Springer, 1993. https://doi.org/10.1007/BFb0091534
• R. Crandall, C. Pomerance, Prime Numbers: A Computational Perspective, 2nd ed., Springer, 2005, §6.2. https://doi.org/10.1007/0-387-28979-8
• F. Boudot et al., Comparing the difficulty of factorization and discrete logarithm: a 240-digit experiment, CRYPTO 2020. https://eprint.iacr.org/2020/697

This entry records a deterministic $O(n^{1.962})$ bound for 3SUM on polynomially bounded integers, using the campaign's shared word-RAM model with $O(\log n)$-bit words. Three distinct input positions must sum to zero; repeated values are allowed. The exact exponent is $981/500$.

References

• Source repository: complete Lean proof and verification record

Why column-subset selection and curvature

The column-subset selection problem (CSSP) asks for $k$ columns of a real matrix $A$ whose span approximates all of $A$ as well as possible in squared Frobenius norm. It is a basic primitive of low-rank approximation, feature selection and numerical linear algebra, studied both for its exact complexity and for approximation algorithms (see Boutsidis, Drineas and Magdon-Ismail, doi:10.1137/12086755X, cited as [2] in the source paper).

Sviridenko, Vondrák and Ward study submodular maximization and supermodular minimization when the objective has bounded total curvature, a parameter $c \in [0,1]$ introduced by Conforti and Cornuéjols that measures how far a monotone set function is from being linear. Their guarantees improve as $c$ decreases. Section 8 of the paper applies this to CSSP: it bounds the curvature of the CSSP objective in terms of the condition number of $A$, so that a well-conditioned matrix has small curvature. This mission formalizes that bound (Lemma 8.2) and the steps of its proof.

Setting

Let $A$ be a real $m \times n$ matrix with columns $c_1, \dots, c_n \in \mathbb{R}^m$, so that $Ax = \sum_i x_i c_i$ for $x \in \mathbb{R}^n$, and let $\|\cdot\|$ be the Euclidean norm. For $S \subseteq [n]$ write $\mathrm{proj}_S(x)$ for the orthogonal projection of $x$ onto $\mathrm{span}\{c_i : i \in S\}$, the point of that subspace nearest to $x$ ($\mathrm{proj}_\emptyset = 0$). The CSSP objective is

the squared Frobenius distance from $A$ to the nearest matrix whose columns lie in the span of the selected columns.

For a set function $f$ on a finite set $X$, the marginal value of $i$ at $A$ is $f_A(i) = f(A+i) - f(A)$. The function $f$ is monotone decreasing if every $f_A(i) \le 0$. Following (1.1) of the paper, a monotone decreasing $f$ has total curvature at most $c$ when, for every $j \in X$,

i.e. the last marginal of $j$ is at least a $(1-c)$ fraction of its first marginal in absolute value.

When the columns of $A$ are linearly independent, the condition number is

Formalization targets

Goal: Lemma 8.2 (p. 11)

For $A$ with linearly independent columns,

Milestones

1. The identity $f^A(S) = \sum_i (\|c_i\|^2 - \|\mathrm{proj}_S(c_i)\|^2)$ (p. 11).
2. Lemma 8.1, monotone part: $S \mapsto \|\mathrm{proj}_S(v)\|^2$ is monotone increasing (p. 11).
3. $f^A$ is monotone decreasing (p. 11).
4. $|f^A_\emptyset(i)| = \sum_j \|\mathrm{proj}_{\{i\}}(c_j)\|^2$ (p. 11).
5. Some unit $x$ has $\|Ax\| \ge \sqrt{|f^A_\emptyset(i)|}$ (p. 12).
6. $|f^A_{[n]-i}(i)| = \|c_i - \mathrm{proj}_{[n]-i}(c_i)\|^2$ (p. 12).
7. Some unit $x'$ has $\|Ax'\| \le \sqrt{|f^A_{[n]-i}(i)|}$ (p. 12).
8. $\kappa^2(A) \ge f^A_\emptyset(i)/f^A_{[n]-i}(i)$ for each $i$, under independence (p. 12).

Items 1–7 hold for arbitrary columns; only item 8 and the goal assume independence.

Significance

Lemma 8.2 turns a spectral quantity into a combinatorial one. With it, any curvature-dependent guarantee for monotone decreasing set functions can be stated for CSSP in terms of $\kappa(A)$. The paper's Lemma 8.3 shows the bound is asymptotically tight, so $1 - \Theta(1/\kappa^2)$ is the right order of the curvature.

There is a caveat that the formalization makes explicit. The paper deduces from Lemma 8.1 that $f^A$ is supermodular, and on that basis quotes its supermodular-minimization algorithm for CSSP with factor $1 + (\kappa^2 - 1)e^{-1} + \kappa^2 O(\epsilon)$ (p. 12). Both the submodularity half of Lemma 8.1 and the supermodularity of $f^A$ are false as printed. With $c_1 = e_1$, $c_2 = e_1 + e_2$ and $v = e_2$ in $\mathbb{R}^2$, the function $F(S) = \|\mathrm{proj}_S(v)\|^2$ has $F(\{1,2\}) + F(\emptyset) = 1 > \tfrac12 = F(\{1\}) + F(\{2\})$. With columns $e_1, e_1+e_2, 2e_2$, $f^A(\{1\}) + f^A(\{2\}) = \tfrac{15}{2} > 7 = f^A(\{1,2\}) + f^A(\emptyset)$. A small perturbation gives a counterexample with independent columns. This is the "suppressor variable" phenomenon of regression. The curvature bound itself does not depend on supermodularity and is true, so it is the goal here. The approximation factor for CSSP is not posed, because it rests on the false claim and is stated with $O(\epsilon)$.

As far as is known, none of these statements has a machine-checked proof. The results are proved on paper, except the two false claims above. The mission adds a formal proof of the curvature–conditioning bound, and makes explicit which parts of §8 survive.

Difficulty

The individual steps are short linear algebra, but they rest on infrastructure that has to be assembled: orthogonal projections onto spans of finite column families, the Pythagorean identities that relate $f^A$ to projections, and the variational characterization of $\sup$ and $\inf$ of $\|Ax\|$ over the unit sphere.

The paper's own route to the large unit vector (milestone 5) does not work as printed. It sets $x_j \propto \|\mathrm{proj}_{\{i\}}(c_j)\|$ and uses $c_i \cdot c_j = \|c_i\|\,\|\mathrm{proj}_{\{i\}}(c_j)\|$, which is false when $c_i \cdot c_j < 0$, so the signs of the inner products have to be accounted for. In the final step, the ratio $f^A_\emptyset(i)/f^A_{[n]-i}(i)$ is a quotient of two negative numbers. Comparing it with $\kappa^2$ requires the supremum to be finite and the infimum to be strictly positive, which is exactly what independence of the columns provides.

Formalization scope

• Columns are a family c : Fin n → EuclideanSpace ℝ (Fin m), and $Ax$ is ∑ j, x j • c j. Subsets of $[n]$ are Finset (Fin n). $[n] - i$ is Finset.univ.erase i and $S + i$ is insert i S.
• $\mathrm{proj}_S$ is Mathlib's Submodule.starProjection onto Submodule.span ℝ (c '' S), which is finite-dimensional, so the argmin of the page exists and is unique.
• $\kappa(A)$ is a real quotient of ⨆ and ⨅ of $\|Ax\|$ over the unit-sphere subtype of $\mathbb{R}^n$. It is used only under LinearIndependent ℝ c, the page's "non-singular", where both are finite and positive. The page's $\kappa = \infty$ for dependent columns is not encoded.
• Monotonicity is the marginal form of §2.1. Curvature is the product form above, which agrees with the ratio of (1.1) whenever $f_\emptyset(j) \ne 0$ and avoids Lean's $x/0 = 0$.
• For $n = 0$ the goal has no $j$ and is empty, as on the page.
• A trivializing reading is ruled out by the encoding: had $\kappa$ evaluated to a junk value $0$, the goal would reduce to monotonicity. Under independence the supremum and infimum are genuine, so the bound $1 - 1/\kappa^2$ is the paper's.
• Not in scope: Lemma 8.3 (stated with $O(\cdot)$), the CSSP approximation factor, and the false submodularity and supermodularity claims.

Useful infrastructure that would be reusable beyond this mission includes Pythagoras for starProjection, monotonicity of projection norms under inclusion of subspaces, and extremal characterizations of $\sup_{\|x\|=1}\|Ax\|$ and $\inf_{\|x\|=1}\|Ax\|$. Contributions of any of the milestones, or of these general lemmas, are welcome.

Selected references

• M. Sviridenko, J. Vondrák, J. Ward, Optimal approximation for submodular and supermodular optimization with bounded curvature, SODA 2015 (version of Oct. 9, 2014); journal version Math. Oper. Res. 42(4), 2017. https://doi.org/10.1287/moor.2016.0842
• M. Conforti, G. Cornuéjols, Submodular set functions, matroids and the greedy algorithm: tight worst-case bounds and some generalizations of the Rado–Edmonds theorem, Discrete Appl. Math. 7(3), 1984. https://doi.org/10.1016/0166-218X(84)90003-9
• C. Boutsidis, P. Drineas, M. Magdon-Ismail, Near-optimal column-based matrix reconstruction, SIAM J. Comput. 43(2), 2014. https://doi.org/10.1137/12086755X
• A. Das, D. Kempe, Submodular meets spectral: greedy algorithms for subset selection, sparse approximation and dictionary selection, ICML 2011. https://arxiv.org/abs/1102.3975

Motivation

Retailers that carry a limited range of products often know something about a customer before choosing which of those products to display. The customized assortment problem asks which products to carry when the displayed assortment may be tailored to the arriving customer's type. This separates the first-stage capacity decision from the later offer decision. El Housni and Topaloglu study the problem under a mixture of multinomial logit choice models and develop an approximation framework for it in their SSRN paper. This mission isolates their structural guarantee for Augmented Greedy, Theorem 4.2 of the PDF version dated 7 December 2021. The theorem identifies the revenue recovered from customer types whose optimal personalized offers agree with a chosen product subset.

The paper contrasts this setting with ordinary assortment optimization, where every type sees the same products. Its later approximation results use the structural guarantee here as a component. The classical comparison is the cardinality-constrained greedy bound for monotone submodular functions, associated with Nemhauser, Wolsey and Fisher (1978). The paper's Appendix B gives an instance in which the customized revenue function lacks global submodularity, so that classical result does not apply directly. El Housni and Topaloglu, §§4 and App. B.

Setting

Let $N=\{1,\ldots,n\}$ be a finite product set. Product $i$ has positive revenue $r_i$, and products are indexed with $r_1\ge\cdots\ge r_n>0$. Let $M=\{1,\ldots,m\}$ be customer types. A type-$j$ customer arrives with probability $\theta_j\ge0$, with $\sum_{j\in M}\theta_j=1$, and assigns each product $i$ a nonnegative preference weight $v_{ij}$. The no-purchase option has weight one. Offering an assortment $T\subseteq N$ to that customer gives MNL expected revenue

If the retailer initially carries only $S\subseteq N$, it can still choose the best offer to each customer type. Thus $f_j(S)=\max_{T\subseteq S}\operatorname{Rev}_j(T)$. For $C\subseteq M$, write $f^C(S)=\sum_{j\in C}\theta_j f_j(S)$, and abbreviate $f=f^M$. The first-stage capacity is $K$; an optimal solution $S^*$ of CAP maximizes $f(S)$ among sets with at most $K$ products. These definitions and the standing data assumptions are stated in §2 and §4 of the paper.

For each product $i$, the prefix $V_i=\{1,\ldots,i\}$ contains products at least as early in the revenue ordering. Greedy starts at the empty set, repeatedly adds an available product that maximizes the new objective value, and stops at cardinality $k$ or when the prefix is exhausted. Augmented Greedy runs Greedy on $V_i$ for each $i$, using $S\mapsto\sum_{j\in C}\theta_j\min(f_j(S),r_i)$, and returns whichever candidate has the greatest $f^C$ value. Both stages may break ties arbitrarily. El Housni and Topaloglu, §4.1.

For type $j$, use the optimal personalized assortment $S_j^*=\{i\in S^*:r_i\ge f_j(S^*)\}$, characterized by Lemma E.1. A type $j\in C$ is complete with respect to $P\subseteq N$ when $P\cap S_j^*=P\cap S^*$; let $C_P$ collect these types. The threshold choice matters because zero-weight products can be present in other optimal offers without helping a customer. El Housni and Topaloglu, Definition 4.1 and App. E.

Formalization targets

Theorem 4.2: complete-type revenue

For every $C\subseteq M$, $P\subseteq N$, $k$ with $|P\cap S^*|\le k$, and every output $\Delta$ of Augmented Greedy on $C,k$,

This is the mission goal, the structural performance statement of Theorem 4.2, p. 11. It does not assert a constant-factor approximation to all of CAP: it identifies the contribution from complete customer types.

Supporting targets

The milestone list follows the results used with this bound: monotonicity of $f_j$ from Appendix C; the MNL threshold assortment of Lemma E.1; submodularity of $S\mapsto\min(f_j(S),r_i)$ on $V_i$ from Lemma 4.3; and the cited $1-1/e$ Greedy guarantee for a nonnegative monotone submodular objective. The greedy milestone compares its output against every feasible set of cardinality at most $k$.

Significance

The theorem says that one algorithmic output captures a fixed fraction of the benchmark supplied by complete types, despite the absence of global submodularity of $f$. It connects the local behavior of truncated type revenues to the full customized assortment objective. The paper uses this result in the development of later algorithms; without it, the standard submodular greedy theorem gives no immediate conclusion for CAP. El Housni and Topaloglu, §§4–5.

The mathematical results are proved in the 2021 paper. The formalization work here is to give machine-checkable statements for the objective, the algorithm with all its legal tie choices, and the four supporting targets, then supply proofs. The MNL revenue formula is already available as a published platform definition; the local CAP and algorithm definitions specify the extra model needed by this theorem. A completed development could also support later CAP missions that use the same threshold and submodularity properties.

Difficulty

The tempting argument applies the classical greedy guarantee directly to $f$, since $f$ increases when more products are carried. Appendix B of the paper shows that this fails: even for one customer type, $f$ need not be submodular. Restricting the ground set to a revenue prefix and truncating each $f_j$ at that prefix's revenue level changes the submodularity question, but the final guarantee must still concern the untruncated $f^C$ objective. The threshold condition in the definition of $C_P$ is what makes that comparison meaningful. El Housni and Topaloglu, App. B, Lemma 4.3 and Theorem 4.2.

Formalization scope

Products and types are Fin n and Fin m; their zero-based Lean indices correspond to the paper's indices plus one. Assortments and type groups are finite sets. The model assumes $r_i>0$, $v_{ij}\ge0$, $\theta_j\ge0$, $\sum_j\theta_j=1$, and decreasing revenue order. The no-purchase weight is exactly one. CAP and personalized revenue use maxima over nonempty finite powersets, so empty input sets have their intended value rather than an arbitrary real supremum. The theorem keeps the source's optimality assumption on $S^*$, even though its particular inequality uses less.

The Greedy predicate describes each successive maximizer and the exact stopping rule. Augmented Greedy requires a Greedy output at every prefix and an $f^C$-maximizing choice among them. Thus the output is constrained by the printed algorithm, and the statement covers every tie-break. The type-$j$ assortment is defined from $S^*$ by the Lemma E.1 threshold, rather than supplied as a free set. These choices rule out a size-only output condition, an arbitrarily chosen $S_j^*$, a vacuous run predicate, and real supremum defaults. The target includes the corner cases $k=0$, $C=\varnothing$, and $P\cap S^*=\varnothing$, where its right side is zero. Arrival probabilities summing to one force $m\ge1$; Augmented Greedy has an output only when at least one product exists.

The reusable parts are the MNL threshold characterization, finite-set submodularity and the general Greedy bound. Contributions toward those lemmas, the paper's case analysis for Lemma 4.3, and the final structural theorem are in scope. Runtime claims, the paper's later logarithmic approximation theorems and its computational experiments are outside this mission.

Selected references

• Omar El Housni and Huseyin Topaloglu, Joint Assortment Optimization and Customization under a Mixture of Multinomial Logit Models: Value of Personalized Assortments, SSRN 3830082, version of 7 December 2021; published as Operations Research 71(4), 2023. SSRN preprint. The mission's numbering and page citations use the pinned 2021 PDF.
• George L. Nemhauser, Laurence A. Wolsey and Marshall L. Fisher, An Analysis of Approximations for Maximizing Submodular Set Functions—I, Mathematical Programming 14, 265–294, 1978. DOI.

Motivation

A text index answers questions about occurrences of a pattern without scanning the whole text. One reason to compress such an index is that many stored texts are repetitive: multiple versions of a document or genome often share long passages. The Burrows–Wheeler transform (BWT) rearranges a text's symbols in a way that groups related contexts. A small number of equal-symbol runs in the BWT is therefore a useful measure of repetition. Gagie, Navarro, and Prezza use the number of runs to state space bounds for text searching and suffix-tree operations in Fully-Functional Suffix Trees and Optimal Text Searching in BWT-runs Bounded Space.

This mission isolates one exact counting result underneath those data-structure bounds. A length-$s$ substring is called an $s$-mer. The number of different $s$-mers measures how many local patterns the text contains; repeated occurrences of the same string count once. Lemma 9 of the 2019 preprint bounds this number directly in terms of BWT runs. The result makes a relation between two notions of text repetition precise: clustering in the BWT and diversity of fixed-length substrings.

Setting

Let $T[1..n]$ be a text over the ordered alphabet $[1..\sigma]$. Its final symbol is a unique terminator \=1$, smaller than every other symbol in the text. For each$i\in[1..n]$, the **suffix**$T[i..n]$starts at$i$and ends at the terminator. The **suffix array**$SA[1..n]$is the permutation of$[1..n]$that lists these suffixes in increasing lexicographic order. Thus$SA[p]$is the starting position of the$p$th suffix. This is the setup of §2 of the source preprint, pp. 7–9.

The BWT symbol at position $p$ is the character just before the suffix at $SA[p]$. When that suffix is the whole text and has no preceding character, its predecessor is read cyclically as T[n]=\$$. The BWT partitions into maximal runs of equal symbols; r$denotes their number. The first and last BWT positions in each run correspond to **sampled text positions**. A text substring$T[i..j]$ is primary when its interval contains a sampled text position, as in Definition 5, p. 16.

For $1\le s\le n$, let $\mathcal S_s(T)$ be the set of length-$s$ strings occurring in $T$:

The braces matter: two windows with identical contents give one element. The final allowed window includes the terminator. The text is not padded in this definition.

Formalization targets

Primary occurrences

Lemma 8, p. 17 states that every nonempty substring of $T$ has an occurrence with the same contents that is primary. With $\operatorname{Sampled}(T)$ denoting sampled text positions, the assertion is

The mission's milestones also capture the suffix-array interval of a pattern, the sampled occurrence of each individual character, and the bound $|\operatorname{Sampled}(T)|\le 2r$ stated in the proof of Lemma 9. These give precise intermediate claims in the paper's route to the count.

Distinct $s$-mers

The main goal is Lemma 9, p. 17:

Here $r$ is calculated from the BWT of the text's suffix array. Both inequalities on $s$ are part of the source statement. The bound concerns distinct strings of a fixed length, not the number $n-s+1$ of substring windows.

Significance

The theorem gives an explicit upper bound on the number of different length-$s$ strings that can appear when the BWT has few runs. In §4.2 the authors use it to bound the text area holding all distinct length-$s$ substrings; that area supports the alphabet-mapping component of their compressed index. This exact combinatorial assertion remains meaningful independently of a machine model or a choice of data structure. Its role in the broader construction is described around Lemmas 8 and 9, pp. 16–17.