PaperlayerView exact revision on arXiv

Source-linked AI summary

A $(\log n)^{1/4}$ Bound for the Koml\'os Problem

Eren Ercan

arXiv:2609.08885v1math.COcs.DMcs.DS

TL;DR

The Komlós conjecture asks whether discrepancy stays absolutely bounded for matrices with unit-norm columns. This paper tracks historical quantities through restriction changes and obtains an O((1 + log n)^(1/4)) bound independent of the number of rows.

  • Problem

    The Komlós conjecture asks whether discrepancy stays absolutely bounded for matrices with unit-norm columns, while the stated prior upper bound is O(√log n).

    Source: §1 · p. 1

  • Method

    The proof tracks historical exponential quantities across restriction-status changes while maintaining covariance-budget information for current restrictions.

    Source: §4 · p. 10

  • Results

    Taking b = 0 yields an O((1 + log n)^(1/4)) discrepancy bound independent of the number of rows.

    Source: §1 · p. 2

  • Takeaways & Limitations

    The finite construction also provides prescribed-depth partial colourings from a given starting point, retaining coordinates already fixed at ±1.

    Source: §1 · p. 1

    The direction-law step invokes Bansal–Jiang Theorem A.4 under its stated feasibility assumptions.

    Source: §2 · p. 5

Abstract

from arXiv · show

Let $A\in\mathbb{R}^{m\times n}$ have columns of Euclidean norm at most one. We prove that $\operatorname{disc}(A)\le2395\left(1+\log_+\frac n9\right)^{1/4}+2\sqrt2$. Here $\log_+t=\max\{0,\log t\}$. Building on Bansal and Jiang's affine spectral independence framework, we remove the $(\log\log n)^{7/4}$ factor from their bound. The fourth root comes from balancing the logarithmic decrease in the alive dimension against the fourth power of the row thresholds. Historical exponential sums control the covariance budget across size classes with summable thresholds. An exact threshold-sum certificate gives the coefficient $2395$, and rounding at most eight remaining fractional coordinates costs $2\sqrt2$. The finite construction also gives partial colourings from any prescribed starting point and at any prescribed depth, preserving existing signs. We formalize the partial- and full-colouring theorems in Lean, including the finite trajectory, exact threshold sum and final rounding, with Bansal--Jiang Theorem A.4 as the sole external research theorem assumption.

1 Introduction and results

Theorem 1.1 gives a discrepancy bound of order (1 + log n)^1/4, independent of the number of rows, and the paper also establishes prescribed-depth partial colourings. Its proof tracks successive restrictions of real rows with historical exponential sums, and the partial- and full-colouring results are formalized in Lean.

1.1 Relation to the Bansal–Jiang construction

  • Compared with the stated Bansal–Jiang bound [BJ26], the paper removes its (log log n)^7/4 factor and tracks successive restrictions of arbitrary real rows across size classes.A size class records the squared mass of a current row restriction, and thresholds across classes are summable.Source: §1 · p. 1, §1.1 · p. 2

1 Introduction and results

  • Theorem 1.1 gives an O((1 + log n)^1/4) discrepancy bound independent of the number of rows; Theorem 1.2 provides prescribed-depth partial colourings preserving existing signs.The construction starts from a given point, and the depth is chosen before its trajectory is constructed.Source: §1 · pp. 1–2

1.2 Overview of the proof

  • Historical exponential sums retain information from retired restrictions, while Jensen’s inequality bounds log(q/nt) by the prescribed depth R and the threshold schedule sums to O((1 + R)^1/4).The resulting dangerous-family count is small enough for the covariance theorem.Source: §1.2 · pp. 3–4

1.3 Notation and formalization

  • The Lean formalization covers the partial- and full-colouring theorems, including the historical trajectory, exact threshold sum, and final rounding; Bansal–Jiang Theorem A.4 is its sole external research theorem assumption.Source: §1.3 · p. 5

2 SDP feasibility and the direction law

The section turns the Bansal–Jiang covariance theorem into a finite-row form and uses a feasible covariance to construct a finite symmetric direction law. The law supports the blocking constraints while preserving the cube and the squared-norm identity.

2 SDP feasibility and the direction law

  • The Bansal–Jiang covariance theorem imposes annihilation, diagonal, trace, and affine spectral-independence constraints on the covariance matrix.The finite-row result is obtained from the original theorem by stacking repeated copies of each block’s response matrix.Source: §2 · pp. 5–6
  • The finite-row covariance theorem supplies a positive-semidefinite matrix under the section’s block-budget hypotheses, including when blocks have fewer rows than alive coordinates.Repeating rows within each block yields the stated form; its charge for a block is exactly ms/(α_sh).Source: §2 · pp. 5–6
  • A nonzero feasible positive-semidefinite matrix, normalized by its trace, is realized by a finite centrally symmetric law on unit directions.The spectral construction uses 2 rank U positive-weight atoms, with covariance Q = U / Tr U.Source: §2 · p. 6
  • Every direction-law atom lies in the range of U and is orthogonal to vectors annihilated by U, so blocking constraints hold for every possible successor.The finite law is used to choose a successor whose complete-successor potential is at most the finite average.Source: §2 · p. 6
  • A supported unit direction orthogonal to the current point keeps the update in the cube, fixes coordinates outside the alive set, and yields the squared-norm identity.The next alive set is a subset of the previous one.Source: §2 · p. 6

3 Successive restrictions of a real row

The construction decomposes each real row into successive size-class restrictions and anchored peeled pieces, controlling their discrepancies over each lifetime. A row identity preserves the contributions across retirement, yielding a bound from its history.

3.2 Regularized discrepancy and dangerous restrictions

  • The squared ℓ2 mass on alive coordinates defines a restriction’s size; a signed record becomes dangerous at its first threshold crossing while the restriction remains active.Blocking its moving gradient makes later regularized increments nonpositive, and each restriction’s discrepancy is bounded through retirement.Source: §3 · p. 7, §3.2 · pp. 8–9

3.1 Peeling and normalization

  • Peeling removes coefficients above s/B, bounding the removed part’s future discrepancy by 2B while capping retained coefficients at s/B.Normalization advances through finitely many classes, with peeled vectors and the terminal residual summing to the input.Source: §3.1 · pp. 7–8
  • Each original row has at most one birth and one peel per class, and at most one active unsigned restriction at any state.Successive normalization labels increase strictly; restriction and peeling preserve the original coefficients.Source: §3.1 · p. 8

3.3 The row identity through retirement

  • The affine row identity carries peeled, completed, current, and terminal contributions forward as restrictions retire and are normalized again.At retirement, the surviving restriction is normalized at the next class; frozen coordinates contribute only to the completed interval.Source: §3.3 · pp. 9–10
  • The row-history estimate bounds each row’s accumulated discrepancy using its peeled vectors, completed and current restrictions, terminal residual, and class thresholds.The proof charges at most 2B_k per peeled vector and 3B_k/2 + 2γ√s_k per tracked interval; the terminal residual costs at most two.Source: §3.3 · p. 10

4 Historical exponential sums and complete updates

Historical exponential sums retain the contributions of restrictions after retirement, allowing the potential to track dangerous restrictions across changing size classes. Complete updates order exponential changes, retirement, crossings, and births so that the outer exponential can control the potential.

4.1 Exponential sums and the two column estimates

  • The potential’s birth-mass difference is unchanged by a birth, and its nonnegative exponential sum includes capped dangerous records after their first crossing.Each signed slot keeps its coefficients and birth point; dangerous or retired records retain their exponential value.Source: §4 · p. 10, §4.1 · p. 11
  • Historical exponential sums retain past restriction records, while a separate current-family estimate controls the affine SDP charge.The historical estimate includes every birth in a fixed class; current restrictions are counted across classes with at most one current restriction per original row.Source: §4.1 · p. 11

4.2 The order of a complete event

  • A complete event updates old live records before classifying retirement and new crossings, then inserts normalized births at the new point.A threshold crossing simultaneous with retirement creates no new dangerous constraint.Source: §4.2 · p. 12
  • The complete-event increment is bounded using predecessor data and regularized increments along the chosen direction, even when new coefficients depend on that direction.New records contribute zero to the potential difference at birth, permitting differentiation of the old-state expression.Source: §4.2 · p. 12

4.3 The outer exponential and its normalization

  • The outer exponential’s normalization is chosen to cancel the combined regularized drift and second-derivative terms using the covariance–drift comparison.The covariance of the weighted sum is controlled by the same diagonal quantity as its negative drift; the buffer supplies slack for a finite-step estimate.Source: §4.3 · p. 13

5 The finite-step exponential estimate

The section proves a uniform one-step exponential bound for complete successors by combining covariance cancellation with negative curvature from the cube-boundary buffer. Symmetry removes odd Taylor terms, and the finite-step estimate applies uniformly over eligible predecessors and direction laws.

5.1 The covariance cancellation

  • The exact second-derivative identity decomposes the bound into nonnegative coordinate, affine, and cap contributions, enabling covariance cancellation.The outer covariance term is essential because it represents the variance of the sum of signed responses.Source: §5.1 · p. 14

5.2 Negative curvature from the buffer

  • The cube-boundary buffer supplies negative curvature of order γ per unit energy, producing a one-step term of order γ^3D.Symmetry removes odd Taylor terms, while a fourth-order remainder of order γ^4D can be absorbed by a mesh bound.Source: §5.2 · p. 15
  • A weighted remainder lemma provides explicit positive curvature and a fourth-order remainder bound from upper bounds on the weights and coefficients.Its constants depend only on σ, P0, and Q0.Source: §5.2 · p. 15

5.3 The one-step estimate for actual successors

  • The finite-step estimate does not require a positive lower bound on an eigenvalue or on a direction’s probability.The proof uses symmetry for the smooth predecessor expression, while a pointwise comparison covers differing freeze and retirement outcomes for opposite directions.Source: §5.2 · p. 15, §5.3 · p. 16
  • Theorem 5.3 gives a one-step exponential bound for actual complete successors when the class parameters, covariance conditions, and mesh satisfy its hypotheses.For fixed class parameters, the allowed mesh is uniform over all eligible predecessors and direction laws.Source: §5.3 · p. 16

6 The schedule and the covariance budget

The schedule chooses class parameters at the prescribed depth so dangerous restrictions consume only a controlled part of the alive dimension while row thresholds remain summable. The resulting count of dangerous restrictions supports a feasible next covariance.

6 The schedule and the covariance budget

  • At prescribed depth R, class parameters are chosen to bound dangerous restrictions by a fraction of the alive dimension and make row thresholds summable.The class choices are made for each prescribed depth.Source: §6 · p. 16

6.1 Why the threshold has a fourth root

  • The square-root summand ensures λ_k ≤ θ_k and strict slack in the fourth-power inequality; rational constants make the SDP budget and threshold sum explicit.Source: §6.1 · p. 17

The thresholds also satisfy the strict bound

6.2 Counting dangerous restrictions at the current state

  • When h> N_R(q), the dangerous-family count in each class is bounded using the current alive columns, with the resulting estimate strictly below δ_k h/2.The Jensen estimate uses q/h; historical records enter through a column estimate, not a union bound over rows or histories.Source: §6.2 · pp. 18–19

6.3 Feasibility of the next covariance

  • The dangerous-gradient count leaves room for a nonzero positive semidefinite covariance that annihilates large rows, dangerous gradients, and the current point.The covariance is supported on the current alive coordinates.Source: §6.3 · p. 19

7 The finite trajectory and the endpoint

The construction maintains a complete state through finite updates until few coordinates remain alive, then rounds the remaining coordinates. Its threshold sum and Euclidean completion provide the endpoint bounds while preserving existing signs.

7.1 Preserving the complete state

  • A finite trajectory from b reaches a state with at most N_R(q) alive coordinates, and each complete successor preserves the construction's invariant.At the endpoint, buffered frozen coordinates are rounded while alive coordinates remain unchanged; the original fixed signs are restored.Source: §7.1 · pp. 20–21

7.2 The threshold sum and finite attainment

  • The threshold sum is bounded by 25(1+R)^1/4, and its numerical reserve pays for buffered rounding and finite-mesh overshoot without a limiting trajectory.Source: §7.2 · p. 21

7.3 Euclidean completion

  • Independent rounding of at most r fractional coordinates has a finite outcome with squared Euclidean norm at most r, yielding the corresponding ℓ∞ estimate.Source: §7.3 · p. 22
  • For q>8, choosing R=log_+(q/9) leaves eight fractional coordinates; for q≤8, direct Euclidean rounding gives the stronger bound √q, preserving existing signs.Source: §7.3 · p. 22

A A uniform weighted fourth-derivative estimate

The appendix establishes a weighted fourth-derivative estimate that applies uniformly even when weights or weighted energy vanish. Its constants are independent of the live-record count, individual coefficients, and selected covariance eigenvalues.

A A uniform weighted fourth-derivative estimate

B The rational threshold-sum certificate

The threshold-sum certificate makes the numerical bound explicit using rational arithmetic and geometric-series bounds. It records the class threshold decomposition and exact logarithmic parameters.

B The rational threshold-sum certificate

B.1 Rational logarithm enclosures

The appendix certifies rational logarithm bounds and finite root comparisons using exact arithmetic. These provide the finite numerical certificate used in the proof.

B.1 Rational logarithm enclosures

  • For rational x ≥ 1, write x = 2^e y with 1 ≤ y < 2 and combine bounds for log 2 and y.The omitted logarithm-series terms are bounded by a geometric series because each denominator is at least 33.Source: §B.1 · p. 24
  • The logarithm enclosures are verified by substituting rational arguments and comparing fractions.The displayed decimals are exact rationals.Source: §B.1 · p. 24

B.2 The finite root comparisons

  • For 0 ≤ k ≤ 128, the finite root comparisons use positive integers A_k and D_k on grid g = 10^6.The table entries are the least integer choices for the rational upper radicands.Source: §B.2 · p. 24
  • Integer square roots evaluate the degree-2 and degree-4 root bounds exactly, and the certificate is checked by integer powers and fraction comparisons.Lower comparisons verify minimality; upper comparisons alone suffice for the proof.Source: §B.2 · p. 24

B.3 The two infinite tails

The appendix bounds both infinite tails after index 128, completing the schedule estimate. The Lean project formalizes the endpoint theorems and their scope, with A.4 as an explicit external theorem hypothesis.

B.3 The two infinite tails

  • The two tails, each starting at index 128, are bounded by 8a_128 and 4b_128, proving (7.6) beyond every possible finite cutoff.Table 1 gives integer upper bounds on grid g = 10^6; its pair at index 128 starts both tail bounds.Source: §B.3 · p. 25, Table 1 · p. 26

C The Lean formalization

  • The Lean project proves the endpoint theorems in Section 1 from the explicit parameter BansalJiangA4 and the covariance statement in Theorem 2.1.The formal derivation includes its finite-row consequence, the historical states and finite path, the numerical schedule bound, and final rounding.Source: C The Lean formalization · p. 27

C.1 The final declarations and their scope

  • The partial-colouring declaration preserves original signs and controls fractional coordinates, while the full-colouring declaration gives the arbitrary-start signing bound.A separate declaration proves the zero-start matrix discrepancy bound.Source: §C.1 · p. 27
  • For arbitrary starting points, A.4 is assumed on every alive coordinate space of the fractional face; it is the sole external research theorem parameter.The remaining ingredients are proved within the project.Source: §C.1 · p. 27

C.3 Reproduction

  • The project is pinned to Lean 4.33.1 and a specified mathlib revision, and its final declarations retain A.4 as an explicit theorem hypothesis.The ancillary directory includes source files, manifests, an axiom-query file, and build instructions.Source: §C.3 · p. 28

C.2 Correspondence with the written proof

The formal modules correspond to the written proof's analytic bound, state evolution, schedule, and endpoint steps. The implementation uses sufficient finite choices while preserving the proof's estimates.

C.2 Correspondence with the written proof

  • SDPSource and the SDP modules formalize the analytic bound for actual historical records and the source theorem's finite-row reduction.StateStep and SDPStep cover dangerous counts and preservation of the schedule invariant.Source: §C.2 · p. 27
  • ScheduledCounts and related modules cover initialization, finite paths, and the stopping count, while ledger modules handle the rational schedule and finite reserve.SectionLedger, SectionStep, PeelBudget, LedgerMemory, CoreLedger, and NumericalLedger are listed for the latter steps.Source: §C.2 · p. 27
  • The formal finite-row reduction may repeat a block more than the least choice, and the schedule uses q + 4 zero-indexed classes for cutoff K = q + 3.The estimates are uniform over that finite cutoff, and the formal mesh uses sufficient positive upper bounds with the reserve in (7.8).Source: §C.2 · p. 28
Loading 2609.08885v1…