You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This is the supplied analytic proof for a formalization challenge. The
existing Lean theorem has cutoff 256. Lowering that cutoff to 90 remains Lean
work; no estimate of that work is implied by the availability of this proof.
proof.md gives the finite-dimensional real proof, compact cyclic
maximum, sharpness, and transfer to complex coordinates. Its two appendices
include the bootstrap lemma and constant logarithm bounds used in the proof.
formalization-map.md connects the numbered proof statements to the Lean goals and existing library.
verify_b9.py uses Python's standard library and exact rational
arithmetic. It writes exact-b9.json and a timestamped validation-b9.json
beside itself. Run a copy in a temporary directory to preserve this record:
exact-b9.json records 31 decisions. Two are deliberate
rejection controls; the expected rejection is a passing control. These
calculations support particular rational bounds, not the whole proof.
PROVENANCE.json records hashes of the original materials
and the editorial changes used to prepare this portable copy.
The target is all real exponents p ≥ 90, arbitrary unequal-norm triples,
and all finite complex coordinate dimensions. The constant is exactly the
existing DiagonalConstruction.cyclicConstant, the supremum of the cyclic
ratio on [1/2,2]. The proof introduces a supremum over t ≥ 0 and proves
its equality with that compact maximum in Section 5. This identification must
be preserved in a formalization.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
The task is to formalize the supplied argument for every real exponent
p ≥ 90. A proof at a selection of integer exponents does not establish this
claim. The existing Lean development proves the corresponding tail p ≥ 256.
Explicit logarithm and rational estimates supporting the proof, not a substitute for formalizing it.
The proof first writes K_p as a supremum over t ≥ 0. Section 5 identifies it
with the compact maximum over [1/2,2]. The Lean goal uses this latter definition.
Do not change the shared definition or silently assume the identification.
The existing cutoff-256 development is organized around weighted convexity,
normalization, scalar confinement, localization, Hessian bounds, sparsification,
and real-to-complex transfer. Its definitions and statements at p > 1 or p > 2
can be reused with their actual hypotheses. Statements assuming p ≥ 256 cannot
be invoked at p = 90: the improved estimates and bootstrap in this note supply
the additional work. Section 6 transfers one real inequality simultaneously
across all seven norms and takes a limit in the undivided inequality, including
triples with zero pair deficit.
The exact checker uses only Python's standard library. Follow the temporary-copy
instructions in README.md; all 31 decisions must reproduce, including
the two intended rejection controls. It verifies rational calculations, not
the continuous-exponent argument or the Lean theorem.
Authors: Ezzeri Esa and project contributors (2026). Supplied for the
cutoff-90 formalization challenge; not yet formalized.
For every real $p\ge90$, the dimension-independent sharp constant for
real $\ell_p$ spaces is the cyclic constant $K_p$. The bound holds in
every finite dimension and is sharp in each dimension at least three.
Section 6 extends the result to complex coordinates.
Proof outline. An upper bound forces a hypothetical counterexample to
have nearly equal norms. In three coordinates, its nearly vanishing pair
gaps force the triple close to the cyclic sign matrix — in two stages,
the second sharpening the first. On an explicit box around that matrix,
the deficit is convex. Averaging over permutations puts it in the cyclic
family and proves the bound.
For a triple $X=[x_1,x_2,x_3]$, write
$$
S=\sum_i|x_i|_p,\qquad
T=|x_1+x_2+x_3|p,\qquad
P=\sum{i<j}|x_i+x_j|_p.
$$
Thus $\Delta_3=S-T$, $\Delta_2=2S-P$, and
$R=\Delta_3/\Delta_2$ when $\Delta_2>0$.
For $t\ge0$, set
$$
A_p(t)=(t^p+2)^{1/p},\quad
B_p(t)=(2|1-t|^p+2^p)^{1/p},
$$
$$
R_p(t)=
\frac{3A_p(t)-3^{1/p}|2-t|}{6A_p(t)-3B_p(t)},\qquad
K_p=\sup_{t\ge0}R_p(t).
\tag{1}
$$
These are the ratios of the triples with columns
$(-t,1,1),(1,-t,1),(1,1,-t)$. Their pair-gap sums are positive by strict
convexity. The absolute value in $B_p$ is necessary for real exponents.
Theorem 1. The real bound
Theorem 1. For every real $p\ge90$, every positive integer $n$, and
every $x_1,x_2,x_3\in\mathbb R^n$,
$$
\Delta_3\le K_p\Delta_2.
\tag{2}
$$
Consequently $K_p$ is the dimension-independent sharp constant, and the
sharp constant in each dimension $n\ge3$.
Frozen parameters
$$
\delta=\frac{2369}{100000},\qquad
q_0=\frac13+\delta=\frac{107107}{300000},\qquad
\rho=\frac{19}{100},
$$
$$
D=\frac{43}{30p},\qquad
E_1=\frac9{4p},\qquad
E_2=\frac{287}{200p},\qquad
t=p^{-1/p}.
$$
Here $D$ bounds the total pair gap$\Delta_2$; $E_1$ and $E_2$ are
the first- and second-stage coordinate deficits, and they are not the same
quantity as $D$. The box radius $\rho$ is unchanged from the p ≥ 256
version. The same witness $t$ serves throughout.
Write $L=\log2$, $C=\log3$, $\ell=\log p$ and $h=\ell-9/10$.
Certified constants: $693/1000<L<347/500$ and $0<C<11/10$, with
$\log90<9/2$ and
$$
\ell\ge\log90>\log16=4L>\frac{2772}{1000}>\frac{12}5>\frac{19}{10}.
$$
Hence $\ell/p$, $\ell/p^2$ and $h/p$ all decrease on the whole real
interval $p\ge90$; their derivative numerators are $1-\ell$, $1-2\ell$
and $19/10-\ell$.
1. Existing bounds and reductions
The following reductions use real $p>1$.
Put $a_i=|x_i|p$ and $b{ij}=|x_i+x_j|_p$. Triangle inequalities give
$\Delta_2\ge0$ before any division. If $S=0$ all vectors vanish; if
$\Delta_3\le0$ the conclusion is immediate for $K\ge0$; if $\Delta_2=0$
every pair gap vanishes, strict convexity places all nonzero vectors on one
nonnegative ray, and $\Delta_3=0$. A strict counterexample therefore has
$S,\Delta_2,\Delta_3$ all positive.
The weighted scalar convexity inequality gives
$$
\sum_{i<j}\frac{b_{ij}^p}{(a_i+a_j)^{p-1}}
\le S+\frac{T^p}{S^{p-1}}. \tag{3}
$$
One elementary proof starts with scalar Hlawka applied to
$a_i(r_i-h)$. Integrating in $h$ represents any convex function on a
compact interval as an affine function plus a nonnegative combination of
$|r-h|$. Apply the resulting weighted inequality to $f(r)=|r|^p$,
take $r_i=(x_i)_k/a_i$, and sum over coordinates $k$.
Zero $a_i$ follow by continuity. The mixed-sign scalar case
$a\ge b\ge0,-c$ has gaps $2c,2b,2(a+b-c),0$ in the four ranges cut at
$b,a,a+b$, all nonnegative.
For $q=T/S<1$, Hölder applied to (3) yields
$$
P\le2Sg_p(q),\qquad
g_p(q)=\left(\frac{1+q^p}{2}\right)^{1/p},
$$
$$
R\le f_p(q):=\frac{1-q}{2(1-g_p(q))}. \tag{4}
$$
The function $g_p$ is convex and $g_p(1)=1$, so its secant slope is
nondecreasing and $f_p$ is nonincreasing on $[0,1)$.
We also need the rough bound $R\le p$. Write
$\ell_{ij}=a_i+a_j$ and $r_{ij}=b_{ij}/\ell_{ij}\in[0,1]$.
Subtract (3) from $\sum\ell_{ij}=2S$, then use
$1-r^p\le p(1-r)$:
$$
S(1-q^p)\le\sum_{i<j}\ell_{ij}(1-r_{ij}^p)
\le p\Delta_2.
$$
Since $1-q^p\ge1-q$, this proves
$$
\Delta_3\le p\Delta_2,\qquad K_p\le p. \tag{5}
$$
It suffices to exclude counterexamples in $\mathbb R^3$. Indeed, for
fixed $K\ge1/2$, the target is
$$
KP\le(2K-1)S+T.
$$
Multiply coordinate $k$ of all three vectors by $w_k^{1/p}$, and
constrain the three pair $p$-th powers to remain fixed. After deleting
zero rows, the feasible nonnegative weights form a compact polytope:
every column of the three constraint coefficients has positive sum, since
all three pair sums could vanish only if every entry in that row vanished.
The quantity $(2K-1)S+T$ is concave in these weights, so it has a
minimizer at an extreme point. At most three weights are positive there:
otherwise a nonzero two-sided perturbation preserves all three constraints.
Thus a strict counterexample in any dimension produces one in dimension
at most three, which can be padded with zeros.
Finally, in searching for a strict counterexample with $R>1$, we can
require
$$
T\ge\max_i a_i.
\tag{6}
$$
Permute the zero-sum quadruple $x_1,x_2,x_3,-\sum x_i$.
Its three complementary pair norms, and hence $P$, are unchanged.
If $L_4$ is the sum of its four norms and $d$ is the distinguished
fourth norm, its ratio is $(L_4-2d)/(2L_4-2d-P)$.
For $R>K>1$, $P>L_4$, and this expression increases with $d$, its
derivative being $2(P-L_4)/(2L_4-2d-P)^2>0$.
The denominators remain positive: a zero pair-gap sum would force
collinearity on a positive ray, and then $P=L_4$.
Choosing a largest fourth norm proves (6). Normalizing $S=1$, the reduced
counterexample satisfies $q=T\ge\max_i a_i\ge1/3$ and $q<1$.
Section 2 supplies $K>1$ independently of either localization stage, so
these reduction domains hold for both constants used below.
2. Scalar confinement for p ≥ 90, and both witness bounds
Use the cyclic witness $t=p^{-1/p}$ throughout. Put $u=1-t$ and
$a=\log(2+1/p)$; then $0<t<1$, $0<u\le\ell/p$,
$A_p(t)=\exp(a/p)$ and $|2-t|=1+u$.
(A) Numerator. For $0\le z\le1$, $e^z-1\le z+z^2$, the tail being
bounded by $z^2\sum_{k\ge2}1/k!<z^2$ since $e<3$; here $C/p<11/900<1$.
As $3A_p(t)\ge3+3L/p$, the numerator
$N=3A_p(t)-e^{C/p}(1+u)$ satisfies
$$
N\ge2-\frac{\ell+C-3L+(C\ell+C^2)/p+C^2\ell/p^2}{p}.
$$
With the coarse $C-3L<-97/100$, the correction other than $\ell$ is
strictly less than
$$
-\frac{97}{100}+\frac{(11/10)(9/2)}{90}+\frac{121/100}{90}
+\frac{(121/100)(9/2)}{90^2}
=-\frac{54053}{60000}<-\frac9{10},
$$
with slack $53/60000$. Hence
$$
N>2-h/p>0. \tag{A}
$$
(B) Denominator. For $0\le z<3$, a geometric majorant of the Taylor
terms from degree two gives $e^z-1\le z+z^2/[2(1-z/3)]$. Here
$$
a=L+\log!\left(1+\tfrac1{2p}\right)<L+\frac1{2p}
<a_{\max}:=\frac7{10}+\frac1{180}=\frac{127}{180},
$$
so $a/p<a_{\max}/90<3$ and the remainder denominator is positive. The
endpoint coefficient check is
$$
\frac12+\frac{a_{\max}^2}{2(1-a_{\max}/270)}
=\frac{145333}{193892}<\frac34,
$$
with slack $43/96946$. Therefore
$$
A_p(t)-1<\frac Lp+\frac3{4p^2}. \tag{B}
$$
(C) The ratio. The cyclic denominator is positive by strict convexity and
$B_p(t)\ge2$. Combining (A)–(B) with these signs,
$$
\frac{K_p}p\ge\frac{R_p(t)}p>
\frac{2-h/p}{6(L+3/(4p))}. \tag{C}
$$
This is a bound for the chosen witness itself, not merely for a supremum.
(D) The comparator.$q_0\in(0,1/2)$ and $2^{90}>200\cdot90$ exactly.
The logarithmic derivative of $p2^{-p}$ is $1/p-L<1/90-693/1000<0$, so
$q_0^p<2^{-p}<1/(200p)$ throughout $p\ge90$. With
$d=L-\log(1+q_0^p)$ we get $0<L-1/(200p)<d<L<7/10$, and from
$1-e^{-z}\ge z-z^2/2$,
$$
p(1-e^{-d/p})\ge d-\frac{d^2}{2p}
L-\frac{1/200+49/200}{p}=L-\frac1{4p}>0.
$$
Since $g_p(q_0)=e^{-d/p}$ and $1-q_0=(2-3\delta)/3$,
$$
\frac{f_p(q_0)}p<\frac{2-3\delta}{6(L-1/(4p))}. \tag{D}
$$
Confinement through $F$, with no additive constant. Subtracting the
right-hand side of (D) from the bound in (C), clearing their positive
denominators and multiplying by $p$, gives the sign of
$$
F(p)=L(3\delta p-h)-2+\frac{9\delta}4+\frac h{4p}. \tag{F}
$$
The net coefficient of $h$ is $-L+1/(4p)<0$ on the whole range, which is
what makes a single upper bound on $h$ valid in both places $h$ occurs;
the two appearances must not be estimated separately. At $p=90$,
$h<9/2-9/10=18/5$, and $3\delta\cdot90-18/5=27963/10000>0$ permits use of
$L>693/1000$. Thus
$$
F(90)>\frac{693}{1000}\left(3\delta\cdot90-\frac{18}5\right)-2
+\frac{9\delta}4+\frac{18/5}{360}
=\frac{1423}{1250000}=:B_{90}>0. \tag{F90}
$$
$B_{90}$ is a strict rational lower bound, not the value of $F(90)$.
For every real $p\ge90$,
$$
F'(p)=L\left(3\delta-\frac1p\right)+\frac{19/10-\ell}{4p^2},
$$
where $3\delta-1/p\ge3\delta-1/90>0$, while $\ell/p^2$ decreases and
$\ell(90)<9/2$. Discarding the positive $19/(40p^2)$ term,
$$
F'(p)>\frac{693}{1000}\left(3\delta-\frac1{90}\right)
-\frac{9/2}{4\cdot90^2}=\frac{37271359}{900000000}>0. \tag{F'}
$$
Together (F90) and (F′) prove $F(p)>0$ for every real $p\ge90$, and hence
$R_p(t)>f_p(q_0)$. This is a positivity-plus-monotonicity argument: no
additive constant $\Gamma$, rounded effective constant, endpoint search or
lower-cutoff claim enters.
Stronger linear bound from the same witness. Retain $h/p$ as one
decreasing expression, so $h/p<(9/2-9/10)/90=1/25$. Then (C) with
$L<347/500$ gives
$$
\frac{R_p(t)}p>
\frac{2-1/25}{6(347/500+3/(4\cdot90))}
=\frac{49/25}{2107/500}=\frac{20}{43}. \tag{W}
$$
Strictness holds even at $p=90$. Hence, uniformly,
$$
p\ge K_p\ge R_p(p^{-1/p})>\max{20p/43,\ f_p(q_0)},
\qquad K_p>1. \tag{7}
$$
Both bounds for the compact maximum, before $D$ is used. Let
$I=[1/2,2]$ and $K_p^I=\max_{t\in I}R_p(t)$; the cyclic denominator is
positive and the ratio continuous on $I$, so this maximum exists, and (5)
gives $K_p^I\le p$ independently. Since
$0<\ell/p<(9/2)/90=1/20<693/1000<L$, we have $1/2<p^{-1/p}<1$, so the
same witness lies in $I$ and
$$
K_p^I\ge R_p(p^{-1/p})>20p/43>1,\qquad
K_p^I\ge R_p(p^{-1/p})>f_p(q_0). \tag{8}
$$
These precede any use of $D$ and either localization stage, and assume no
global maximizer.
3a. First stage: the total gap and the preliminary box
Let $K$ be either $K_p$ or $K_p^I$, with both lower bounds established
above. Suppose a reduced strict counterexample has $R>K$. Then
$q\ge\max_ia_i\ge1/3$ and $q<1$; since $R\le f_p(q)$, $f_p$ is
nonincreasing and $K>f_p(q_0)$, we must have $q<q_0$. With
$\sum_ia_i=1$,
$$
\frac{42893}{150000}=1-2q_0<a_i<q_0=\frac{107107}{300000}.
$$
Only now, and only from the stronger witness bound (W), does
$$
\Delta_2=\frac{1-q}R<\frac{2/3}{(20/43)p}=\frac{43}{30p}=D
\tag{Total-gap}
$$
follow. This bounds $\Delta_2$; it is not yet a coordinate deficit.
For each pair choose any coordinate of greatest absolute value $m$. In three
dimensions its pair norm $b$ satisfies $m\ge3^{-1/p}b$. With
$\ell_{ij}=a_i+a_j<2q_0$ and a nonnegative triangle gap at most
$\Delta_2$,
$$
\ell_{ij}-m\le(1-3^{-1/p})\ell_{ij}+3^{-1/p}(\ell_{ij}-b)
<\frac{2q_0\log3+43/30}p
<\frac{3328177}{1500000,p}<\frac9{4p}=E_1,
\tag{First-deficit}
$$
using $1-e^{-C/p}<C/p$ and $C<11/10$; the coefficient slack is
$46823/1500000$. This first stage is established on the new parameters and
the whole range; the bootstrap of Section 3b does not supply it.
Reflect each chosen row's sign so the selected pair coordinate is positive.
Each of the pair's two entries is then at least its singleton norm minus
$E_1$, and these are positive because
$1-2q_0-E_1(90)=39143/150000>0$, with the margin increasing in $p$.
If two pairs chose the same row, their shared nonzero entry forces their sign
choices to agree, and all three entries of that row would sum to at least
$1-3E_1$, contradicting $q<q_0$ since
$1-3E_1(90)-q_0=170393/300000>0$. Hence the selected rows are distinct;
arbitrary ties in the original selection are allowed, and this argument shows
any such choice occupies distinct rows. Permute rows so row $i$ selects the
complementary pair $j,k$, fixing one orientation with positive off-diagonal
entries.
For $k\ne i$ the selected-pair estimate and the other entry's singleton
upper bound give $X_{ki}\ge a_i-E_1$. For diagonal row $i$ retain the
combined pair bound $m_{jk}\ge1-a_i-E_1$; since $X_{ii}+m_{jk}\le q$,
$$
-a_i\le X_{ii}\le q-1+a_i+E_1.
$$
With the singleton interval and $q\le q_0$,
$$
-3\delta\le3X_{ii}+1\le6\delta+3E_1,\qquad
-6\delta-3E_1\le3X_{ki}-1\le3\delta\quad(k\ne i),
$$
so with $X_0=J-2I$,
$$
|3X-X_0|_{\max}\le r_1(p):=6\delta+3E_1(p)
\le r_1(90)=\frac{10857}{50000}<\frac14.
\tag{Preliminary-box}
$$
The margin is $1643/50000$ and $r_1$ decreases in $p$. The factor three
scales a single entry of $X$; it is not a sum or division of row deficits.
This box is used only for coordinate estimates. No convexity of $H_K$ on
it is asserted or used.
3b. Second stage: the bootstrap, its positive tail, and contraction
Apply the bootstrap lemma proved in Appendix A. Its domain is finite real $p>1$,
$\delta\ge0$, $q_0=1/3+\delta$, $D>0$ and $0\le r<1/2$; its hypotheses
for a real three-column $X$ in a fixed orientation are
$$
\sum_ia_i=1,\quad a_i\le q_0,\quad
q=\Big|\sum_ix_i\Big|p\le q_0,\quad
\Delta_2<D,\quad |3X-X_0|{\max}\le r.
$$
All hold with $r=r_1(p)$: normalization and the singleton and total-norm
bounds from Sections 1 and 3a, the strict gap from (Total-gap), the
orientation and box from (Preliminary-box), and $0<r_1(p)<1/4<1/2$. No
equal-singleton assumption is made and the configuration does not change
between stages.
Put $\eta(p)=r_1(p)/(1-r_1(p))$. Since $r_1$ decreases and
$r\mapsto r/(1-r)$ increases,
$$
0<\eta(p)\le\frac{10857}{39143}<\frac13,\qquad
\frac13-\frac{10857}{39143}=\frac{6572}{117429}>0,
$$
so the complementary coordinate is positive and uniquely dominant. With
$c=(1+2\eta(p)^p)^{-1/p}$, D-LEMMA concludes
$\ell_{ij}-m<E_{\rm new}=D+2q_0(1-c)$, the coordinate bounds
$$
X_{ki}\ge a_i-E_{\rm new}\ (k\ne i),\qquad
-a_i\le X_{ii}\le q-1+a_i+E_{\rm new},
$$
and the same-orientation enclosure $r_{\rm new}=6\delta+3E_{\rm new}$. The
diagonal conclusion is exactly where the total-norm hypothesis $q\le q_0$ is
needed.
The tail is strictly positive and must be carried. Since $\eta>0$ and
$p$ is finite, $c<1$, so
$$
0<1-c<\frac{2\eta(p)^p}p<\frac{2\cdot3^{-p}}p,
\qquad
D<E_{\rm new}<\frac{43/30+4q_0,3^{-p}}p.
$$
It is never replaced by zero. The available coefficient allowance is
$$
\frac{287}{200}-\frac{43}{30}=\frac1{600}>0,
$$
and the exact comparison $3^7-4q_0\cdot600=166268/125>0$ with
$p\ge90\ge7$ gives $4q_0 3^{-p}\le4q_03^{-7}<1/600$. Hence
$E_{\rm new}<E_2$ for every real $p\ge90$, and in the same orientation
$$
|3X-X_0|{\max}\le r{\rm new}<r_2(p):=6\delta+3E_2(p)
\le r_2(90)=\frac{1781}{9375}=\rho-\frac1{37500}<\rho.
\tag{Final-box}
$$
The displayed constant equality is at $p=90$; $r_2$ decreases thereafter.
Contraction is verified separately on the whole interval:
$$
r_1(p)-r_2(p)=3(E_1-E_2)=\frac{489}{200p}>0.
$$
4. Convexity on the entire entry box
Define the closed convex box
$$
\mathcal B={X:|X-X_0|_{\max}\le\rho},\qquad \rho=\frac{19}{100}.
$$
All nine entries vary independently. Singleton absolute coordinates lie in
$[81/100,119/100]$, total coordinates in $[43/100,157/100]$, and each pair
has a positive complementary coordinate at least $162/100$ with its other
coordinates of absolute value at most $38/100$. Every one of the seven norm
vectors stays nonzero on an open neighbourhood of $\mathcal B$; since
$p\ge90>2$, $|v|_p$ is $C^2$ at these vectors including those with
zero individual coordinates, because $|s|^p$ has vanishing second
derivative at $s=0$. This covers pair-coordinate zeros and the whole closed
boundary.
For real $p\ge90$ and any $1\le K\le p$, put $w=\sum_ix_i$ and
$$
H_K(X)=\left(2-\frac1K\right)\sum_i|x_i|_p
+\frac1K|w|p
-\sum{i<j}|x_i+x_j|_p=\Delta_2-\frac{\Delta_3}K.
$$
We prove $H_K$ convex on $\mathcal B$.
The intrinsic $p>2$ norm-Hessian identity is
$$
D^2|v|_p[h,h]
=\frac{p-1}{|v|p^{p-1}}
\min{\lambda\in\mathbb R}
\sum_k|v_k|^{p-2}(h_k-\lambda v_k)^2. \tag{9}
$$
The minimizing scalar has denominator $\sum_k|v_k|^p>0$, so zero individual
weights do not affect validity; the Hessian annihilates its radial direction,
mixed terms included.
For a singleton or total vector the Hessian is at least
$b_p\operatorname{dist}(h,\mathbb Rv)^2$ with
$$
b_p=\frac{(p-1)(43/100)^{p-2}}{3^{1-1/p}(157/100)^{p-1}}>0,
$$
using the minimum coordinate weight and the norm upper bound in (9).
Write $Z=[h_1,h_2,h_3]$ and set
$$
e^2=\sum_i\operatorname{dist}(h_i,\mathbb Rx_i)^2,\qquad
d=\operatorname{dist}\Big(\sum_ih_i,\mathbb Rw\Big).
$$
The positive part of $D^2H_K$ is at least $b_p(e^2+d^2)/p$, since
$2-1/K\ge1\ge1/p$ and $1/K\ge1/p$.
Relative column scalings must be controlled as well as perpendicular
directions. Write $h_i=t_ix_i+e_i$ with $e_i\perp x_i$. The singular
values of $X_0$ are $1,2,2$, and
$|X-X_0|_{\rm op}\le|X-X_0|F\le3\rho=57/100$, so
$\sigma{\min}(X)\ge43/100$ and $\max_i|x_i|_2\le119\sqrt3/100$.
With $w=X\mathbf1$,
$$
\frac{43}{100}\operatorname{dist}(t,\mathbb R\mathbf1)
\le\operatorname{dist}(Xt,\mathbb RX\mathbf1)\le d+\sqrt3e.
$$
Choosing a closest common scalar to $t$, and $\kappa=119\sqrt3/43$,
$$
\operatorname{dist}_F(Z,\mathbb RX)\le\kappa d+(1+\sqrt3\kappa)e,
\qquad
\kappa^2+(1+\sqrt3\kappa)^2=\frac{202483}{1849}<110,
$$
so $e^2+d^2\ge\operatorname{dist}_F(Z,\mathbb RX)^2/110$. This includes
independent relative radial motion of all three columns; only the common
radial scaling remains unpenalized, and it is zero by homogeneity.
For a pair vector take $\lambda=h_{\rm large}/v_{\rm large}$ in (9),
removing the dominant coordinate's term. The two remaining coordinate ratios
are bounded by $19/81$, and the corresponding two-by-three map has squared
operator norm at most $1+2(19/81)^2$. Hence its Hessian is at most
$d_p|h|2^2$ with
$$
d_p=\frac{p-1}{162/100}\left(\frac{19}{81}\right)^{p-2}
\left(1+2\left(\frac{19}{81}\right)^2\right).
$$
Radial annihilation permits subtracting one common multiple of $X$ from
$Z$ in every pair term; the independent pair-perturbation factor is four,
since
$$
\sum{i<j}|h_i+h_j|_2^2
=\sum_i|h_i|_2^2+\Big|\sum_ih_i\Big|_2^2
\le4\sum_i|h_i|_2^2.
$$
The exact fixed-radius comparison is
$$
\frac{d_p}{b_p}
=3^{1-1/p}\frac{157}{162}
\left(1+2\left(\frac{19}{81}\right)^2\right)
\left(\frac{2983}{3483}\right)^{p-2}
<4\left(\frac67\right)^{p-2},
$$
since $2983/3483<6/7$, $p-2>0$, and the prefactor is strictly less than
$3(157/162)(1+2(19/81)^2)=1143431/354294<4$. The factor four above is
retained separately. Therefore
$$
D^2H_K(X)[Z,Z]\ge
b_p\left[\frac1{110p}-16\left(\frac67\right)^{p-2}\right]
\operatorname{dist}_F(Z,\mathbb RX)^2\ge0. \tag{10}
$$
The bracket is strictly positive for every real $p\ge90$. The endpoint
certificate is exact:
$$
(7/6)^{88}=\big((7/6)^8\big)^{11}>3^{11}>1760\cdot90,
$$
with margins $(7/6)^8-3=725953/1679616>0$ and
$3^{11}-1760\cdot90=18747>0$. The logarithmic derivative of
$(7/6)^{p-2}/p$ is $\log(7/6)-1/p>1/7-1/90=83/630>0$, the logarithm bound
following by integrating $1/x$ on $[1,7/6]$. Hence
$(7/6)^{p-2}>1760p$ on the whole real interval. Integrating (10) along
every segment in $\mathcal B$ proves $H_K$ convex there, for all real
$p\ge90$ and every $1\le K\le p$; the verified $C^2$ neighbourhood makes
this valid on the boundary.
5. Cyclic averaging finishes the proof
Let $K$ be $K_p$ or $K_p^I$; by (5), (7) and (8), $1<K\le p$, so
Section 4 applies. Simultaneous row and column permutations
$X\mapsto QXQ^T$ preserve $X_0$, $\mathcal B$ and $H_K$. The average
over all six permutations,
$$
\overline X=\frac16\sum_{Q\in S_3}QXQ^T,
$$
has a common diagonal $d\in[-119/100,-81/100]$ and a common off-diagonal
$o\in[81/100,119/100]$, so it is $o$ times the cyclic matrix with
parameter $t=-d/o$ satisfying
$$
\frac{81}{119}\le t\le\frac{119}{81},\qquad t\in I=[1/2,2],
$$
an interval independent of $p$. All averaging segments lie in the closed
box. Convexity and invariance give $H_K(X)\ge H_K(\overline X)$, and
$H_K(\overline X)\ge0$: for $K_p$ by the defining cyclic supremum, for
$K_p^I$ because $t\in I$ and by the definition of that compact maximum.
In each case the cyclic denominator is positive, $K>0$, and
$H_K({\rm cyclic})=\Delta_2({\rm cyclic}),(1-R_p(t)/K)\ge0$.
A strict counterexample to either constant has, by Sections 1–3b, a
normalized oriented matrix $X$ with $3X\in\mathcal B$, and
$H_K(3X)=3H_K(X)<0$ by positive homogeneity — contradicting the
nonnegativity just proved. This proves (2) for both constants in every finite
dimension.
Attainment is not assumed. Section 2 established continuity, the positive
denominator, existence of $K_p^I$, the independent bound $K_p^I\le p$,
witness membership in $I$, and both inequalities (8) before $D$ or
either localization stage. Applying the global real inequality with $K_p^I$
to every cyclic $t\ge0$, whose denominator is positive, gives
$R_p(t)\le K_p^I$ and hence $K_p\le K_p^I$; the reverse holds because
$I$ lies in the defining domain of $K_p$. Thus $K_p=K_p^I$, and the
compact maximum gives a cyclic attainer in dimension three with
$\Delta_2>0$. Zero-padding proves sharpness in every dimension $n\ge3$;
the inequality itself has no lower dimension restriction.
6. Complex coordinates
Corollary 2. For every real $p\ge90$ and every finite complex coordinate dimension, $\Delta_3\le K_p\Delta_2$ for every triple. The constant is least among those valid uniformly over all such dimensions, and sharp in each dimension at least three.
The zero-dimensional real and complex cases both reduce to $0\le0$; Theorem 1 covers every positive integer dimension over the reals.
The dimension-independent result passes to complex $\ell_p$ spaces. Let
$$
c_p=\frac1{2\pi}\int_0^{2\pi}|\cos\theta|^p,d\theta>0.
$$
Rotation invariance shows the real-linear map sending $z\in\mathbb C^n$ to
$c_p^{-1/p}\operatorname{Re}(e^{i\theta}z_j)$, over coordinates $j$ and
the circle with uniform measure, preserves the complex $\ell_p$ norm.
For a finite real approximation take $\theta_k=2\pi k/N$,
$k=0,\dots,N-1$, and define a vector in $\mathbb R^{nN}$ by the entries
$(Nc_p)^{-1/p}\operatorname{Re}(e^{i\theta_k}z_j)$.
For a fixed triple the seven circle integrands — three singletons, three
pairs, the total — are continuous, so their equally spaced Riemann sums
converge simultaneously along the same $N$, with limits the
corresponding complex $\ell_p$ norms. Real-linearity preserves every pair
and total sum at each finite $N$. Apply the real theorem to this one finite
map and pass to the limit in the undivided inequality
$\Delta_3\le K_p\Delta_2$; this handles a limiting $\Delta_2=0$ with no
ratio division. The real cyclic attainer is also a complex triple, so the
constant is sharp in every complex dimension $n\ge3$, again by
zero-padding.
If three matrices are simultaneously unitarily diagonalizable, conjugation by
their common unitary identifies all seven Schatten $p$ norms with the
complex scalar $\ell_p$ norms of their diagonals, so the inequality and the
sharp constant transfer to that class.
Appendix A. Localization bootstrap
Lemma A.1 (localization bootstrap). Fix a finite real p>1, delta>=0,
q0=1/3+delta, D>0 and 0<=r<1/2.
Let X=[x1,x2,x3] be a real 3-by-3 matrix in a fixed row, sign and
input orientation, with x_i in R^3. Put
a_i=||x_i||_p, q=||x1+x2+x3||_p,
b_ij=||x_i+x_j||_p and
The singleton interval follows from these assumptions:
1/3-2delta<=a_i<=1/3+delta. No equality between singleton norms is imposed.
Set eta=r/(1-r) and c=(1+2eta^p)^{-1/p}. Then every pair has its
positive unique dominant coordinate in the complementary row. For its
value m in X, norm b and singleton-norm sum ell,
Contraction requires the additional comparison r_new<r. Section 3b verifies
that comparison for the parameters used here.
Dominance and pair estimate. In 3X a diagonal coordinate lies in
[-1-r,-1+r] and an off-diagonal coordinate lies in [1-r,1+r].
For pair i,j, complementary row k has pair value at least 2-2r>0.
The other two pair coordinates have absolute values at most 2r.
As r<1/2, one has 2-2r>2r, so the complementary coordinate is uniquely
dominant. Its two coordinate ratios are at most eta=r/(1-r).
Scaling back by three preserves those ratios. Consequently
b^p<=m^p(1+2eta^p), hence m>=cb, with 0<c<=1.
The pair gap ell-b is nonnegative and no larger than Delta2, by the
triangle inequality. Also ell<=2q0. Therefore
The first strict inequality follows from e^{-u}>1-u for u>0;
the last from log(1+v)0. Since q0>=1/3>0,
this gives strict (L-tail). If r=0, eta=0, c=1 and
E_new=D, so (L-tail) is equality with zero tail.
Singleton and total-norm step. The sum-one and singleton upper
bounds imply a_i=1-a_j-a_k>=1-2q0=1/3-2delta.
For k!=i, take the pair i,j complementary to row k. Its dominant
coordinate m=X_ki+X_kj satisfies m> a_i+a_j-E_new.
Since X_kj<=a_j, we obtain X_ki>=a_i-E_new.
For diagonal row i use the complementary pair j,k, retaining the
combined estimate m_jk>=1-a_i-E_new.
The i-th coordinate of the total vector is at most its norm q, so
This is exactly where the explicit total-norm hypothesis q<=q0 is
needed. Combining it with a_i<=q0 gives the upper diagonal bound
-1/3+2delta+E_new.
The resulting scaled entry deviations satisfy
The denominators in the remaining terms exceed 2N+1, giving the strict
geometric upper tail. Exact comparisons certify
693/1000<L<347/500 and 0<C<11/10.
The positive degree-16 Taylor sum for exp(9/2) exceeds 90 by
2848223598331/170993385472000>0. Therefore log90<9/2.
Also log p>=log90>log16=4L>2772/1000>12/5>19/10.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
