Erdős, Rocky Mountain Journal of Mathematics 15(2) (1985), page 361 (verbatim from the rendered scan at https://users.renyi.hu/~p_erdos/1985-27.pdf):

Put (21) ∏_{i=1}^{k} (x + i) = u_k(x) v_k(x), (u_k(x), v_k(x)) = 1 where v_k(x) is squarefree and all prime factors of u_k(x) occur with an exponent greater than 1. The representation in (21) is clearly unique. Clearly for k > k_0(x), u_k(x) > v_k(x). Perhaps one can estimate the smallest k_0(x) so that u_k(x) > v_k(x) for all k > k_0(x) quite well. I have not done this. For small values of k usually v_k(x) > u_k(x). I thought that for every x there is a k for which v_k(x) > u_k(x). x = 7 seemed a likely counterexample but if k = 7, u_7(7) = 2^7 3^3 < v_7(7) = 5·7·11·13. On the other hand a simple computation shows that n = 23 is a counterexample, i.e., for every k, v_k(23) < u_k(23). The reason for this is the existence of 24, 25, 27 and 32. I would not be surprised if 23 is the only counterexample. Perhaps in fact there is a k_0 so that for every k > k_0 and all n > n_0(k) (22) v_k(n) > u_k(n). (22) is perhaps too optimistic.

The literal refuted statement is

∀ x ≥ 1, x ≠ 23 → ∃ k ≥ 1, u(x,k) < v(x,k).

For P(x,k) = ∏_{i=1}^k (x+i), v(x,k) is the product of the primes whose exponent in P(x,k) is exactly one. It is not the squarefree part: a prime occurring to exponent at least two is absent from v. The factor u(x,k) is the product of every prime power whose exponent in P(x,k) is at least two, with its full exponent. Thus u(x,k)·v(x,k)=P(x,k).

The result refutes only the sentence proposing 23 as the unique counterexample. It makes no claim about conjecture (22), an estimate of k_0(x), the assertion that 23 and 47 are the only counterexamples, or the statement that 23 itself is a counterexample.

I. Benjamini, H. Helman Tov and M. Zhukovskii, Global information from local observations of the noisy voter model on a graph, Annals of Probability 51(5), 1963–1992 (2023), Section 2.2, asks:

May Var(ζ₁ + … + ζ_t) be sublinear? We do not have an answer. However, we prove that it is either linear in t or O(ln t).

The quotation is from arXiv:2207.01224v2, p. 6. The answer is no. For a connected locally finite simple graph with a neighbour at every vertex, noise $0<\varepsilon<1$, observation vertex $u$ of degree $D$ and lag $d\ge1$, put $\zeta_i=\mathbf{1}{X_i(u)=X_{i+d}(u)}$ and $W_t=\sum_{i=1}^{t}\zeta_i$. The formal settlement is D5.S3.StatisticalMechanics.NoisyVoter.RepetitionVarianceLinear.result : claim. Preregistration: #16646. The Library note supplies the publication locator and quotations.

Statement echo

| Source clause | Lean counterpart | Fidelity | | --- | --- | --- | | Connected graph, possibly infinite | G : SimpleGraph V, G.LocallyFinite, Model.connected | No finite-vertex restriction; finite neighbour sets make uniform choices meaningful | | A vertex has a neighbour to copy | Model.hasNeighbor; Value G (Coord.choice k v) is the neighbour subtype | Excludes an isolated one-vertex graph whose uniform copying law is undefined | | Independent fair initial opinions | Coord.initial, coordinateLaw, Model.independent, Model.laws | Bernoulli one-half | | Independent fair fresh opinions and Bernoulli noise controls | Coord.fresh, Coord.refresh, coordinateLaw, Model.ε, its strict bounds | True means refresh | | Independent uniform neighbour choices | Coord.choice, neighbour-subtype value and uniform finite law | The choice is an actual neighbour | | Synchronous recursion | nvm | Initial, refresh and copying cases mirror Section 1 | | Repetition indicator at lag $d$ | W, sum over Finset.Icc 1 t, positive lag in claim | No normalization; the observation reaches time $t+d$ | | Every graph, vertex and probability model | The closed quantifiers of claim | Arbitrary vertex type and measurable probability space | | Variance is never sublinear | result, negated little-o in claim | Private model_explicitBound supplies the explicit lower bound for every natural $t$ | | Encoding requirements | Decidable equality, measurable-space and local-finiteness instances | Decidable equality is representational; no additional graph hypothesis |

E. Bäumer, V. Gitton, T. Kriváchy, N. Gisin and R. Renner (arXiv:2405.08939, quant-ph; Phys. Rev. A 111, 052453 (2025)) study classical (local) models in the triangle network with four outcomes per party. Their best local fully symmetric construction has p(A = B = C) = 1/4, and their conclusion states:

Open problem. Does there exist a distribution p(A,B,C) that is local in the triangle network and fully symmetric such that p(A=B=C) > 1/4?

Issue #11256 fixes the reading. Locality is eq. trilocal: sources uniform on [0, 1] and measurable conditional distributions p_A(a|β,γ), p_B(b|γ,α), p_C(c|α,β). Full symmetry is invariance under every permutation of the parties and every joint relabelling of the four outcomes. The formal claim is the negative answer, s₁₁₁(p) ≤ 1/4 for every local fully symmetric p; the result refutes it, so the answer is yes.

F. Hiai, M. Mosonyi and M. Hayashi, Quantum hypothesis testing with group symmetry, J. Math. Phys. 50 (2009) 103304, Section 7, verbatim excerpt with the indicated omissions:

To get a complete solution of the problems of the Chernoff and the Hoeffding bounds and of Stein's lemma, … the key point is to show that (4.5) holds with equality … This can be done, for instance, … [by showing] that the function ψ exists and is differentiable on the interval (0, 1). As the examples of Section 6 suggest, one can expect the differentiability of ψ to hold in our setting of group-invariant state discrimination. The main open question of the present work is to show that this is indeed the case.

| Source object or quantifier | Formal reading | |---|---| | Finite-dimensional Hilbert space | Complex coordinate space of arbitrary dimension d | | Compact group and unitary representation | Finite group G and a homomorphism into unitary complex matrices; finite groups with the discrete topology are compact | | Faithful states | Positive definite matrices with trace one | | Equation (2.1), tensor conditional expectation | Defs.twirlPower, the uniform finite-group Haar average of tensor conjugates, indexed by words Fin n → Fin d | | Finite logarithmic overlap | Defs.psiN, the real logarithm of the real part of the trace of the product of CFC powers | | Equation (3.1), asymptotic overlap | Defs.psi, the selected limit of psiN / n, with convergence at every s in (0,1) an explicit premise | | Differentiability assertion | Defs.claim, universal differentiability on (0,1) under these premises |

Refuting this finite-group restriction with faithful states refutes the compact-group assertion on its faithful domain.

P.-E. Emeriau, M. Howard and S. Mansfield (arXiv:2007.15643, quant-ph; PRX Quantum 3, 020307 (2022)) introduce the dimension-d Torpedo Game: Alice receives x, z ∈ Z_d and sends one dit; Bob is asked q ∈ {∞, 0, …, d − 1} and must answer a ≠ x for q = ∞ and a ≠ qx − z otherwise. They find the classical values 3/4 and 11/12 for d = 2, 3, perfect classical strategies for 5 ≤ d ≤ 23, and state

Conjecture: θ^C_{d≥5} = 1.

Issue #11350 fixes the reading: classical strategies use finite shared randomness with stochastic encodings and decodings, and θ^C_d = 1 means that 1 is the greatest classical winning probability.

W. van Dam, R. D. Gill and P. D. Grünwald, “The Statistical Strength of Nonlocality Proofs”, IEEE Transactions on Information Theory 51(8), 2812–2835 (2005), arXiv:quant-ph/0307125v2, Section VI.D, p. 11, Conjecture 5 states:

There is an experiment on pairs of Bell singlets, of the $2\times4\times4$ type, more than twice as strong as CHSH, and involving joint measurements on the pairs.

The counts are two parties, four settings per party and four outcomes per setting. The source measures strength by KL divergence in bits, minimized over every local response mixture, with uniform, product or arbitrary correlated setting laws (Section IV.B, Definitions 1–3).

A. Milekhin, Z. Adamska and J. Preskill, Observable and computable entanglement in time, arXiv:2502.12240v2, define the spacetime density matrix T_AB of a subsystem A at time 0 and a subsystem B at time t.

• The definition. Tr(T_AB (O_A ⊗ 1_B)(1_A ⊗ O_B)) = ⟨O_A(0) O_B(t)⟩ = Tr(ρ O_A U† O_B U) (Eqs. (4), (9)); A and B "do not have to be related to each other in any particular way". The Schatten norm is ||M||_p = (Tr (M†M)^{p/2})^{1/p} (footnote a).
• The conjecture. After Audenaert's inequality for density matrices (Theorem 1, Eq. (24)), §IV item 9 states: "Conjecture 1 For any T_AB on a finite-dimensional H_A ⊗ H_B and p > 1: 1 + ||T_AB||_p ≥ ||Tr_A T_AB||_p + ||Tr_B T_AB||_p. (25)"

The verbatim statements are in the literature note.

Issue #17385 fixes the reading: for every finite dimension, every density matrix ρ, every unitary U between the factorizations H_A ⊗ H_Ā and H_B ⊗ H_B̄ of the whole system, every T satisfying Eq. (9) for all O_A and O_B, and every real p > 1, inequality (25) holds.

The conjecture is refuted.

Z. Li, E. Theil, A. W. Harrow and I. Chuang, An Exponential Sample-Complexity Advantage for Coherent Quantum Inference, arXiv:2605.21457v2, Section S3 A, p. 9, states:

This channel is optimal for m ≤ n (see Ref. [S2]), and we conjecture that it is also optimal for m > n.

Preregistration #19410 fixes $n=1$, $m=2$ and the one-site worst-case squared-infidelity reading. The universal optimality assertion is refuted by $d=r=2$. A strict-improvement theorem for every $d\ge r\ge2$ is not part of this settlement. The Library note identifies the source and conventions.

Statement echo

| Source clause or binding convention | Lean counterpart | | --- | --- | | Squared fidelity and infidelity | sqFidelity is the squared real trace of the positive square root; the loss uses one minus that value. | | All purifications, equation (S34) | purifications contains every positive trace-one rank-one matrix with the specified environment partial trace. | | One joint system-environment site | oneSiteMarginal retains both registers of either output pair. | | One common target before the maximum, equation (S13) | oneSiteLoss takes the infimum over the convex hull of purifications after forming the maximum of the two infidelities. | | Worst-case rank-at-most-$r$ domain, equation (7) | worstCaseOneSiteRisk takes the supremum over every canonical density state with matrix rank at most $r$. Infima and suprema use EReal. | | Totally symmetric output restriction | TotallySymmetricSupport asserts $S\Xi S=\Xi$, with $S=(I+F)/2$, on both sides. | | Werner cloner and the one-input RP map | wernerOneToTwo, randomPurifyOne and purifyAndClone retain the source matrix expressions, with cloning dimension $dr$. | | Genuine channel competitors | AdmissibleChannel uses QuantumChannel and the support restriction on every admissible input. | | Positive dimensions $1\le r\le d$ | claim retains these quantifiers; the counterexample instantiates them at two. | | Claimed optimality | claim compares the two worst-case risks for every admissible channel; result proves its negation. |

Hiai and Ruskai, Contraction coefficients for noisy quantum channels, arXiv:1508.03551v1, Section 6, Theorem 6.2 and Conjecture 6.3 (PDF p. 19), state:

Although the bounds in the above theorem are sufficient to disprove two conjectures as remarked below, we believe that they are optimal, i.e.,

Conjecture 6.3. Equality holds in (45c) through (45e) above.

The map on complex qubit matrices is $\Phi_{\alpha,\tau}(w_0I+\mathbf w\cdot\boldsymbol\sigma) =w_0I+\alpha w_1\sigma_1+\tau w_0\sigma_3$. For every $\alpha\geq0$, $0<|\tau|<1$ and $\alpha^2+\tau^2\leq1$, the conjecture asks for the three equalities

$$ \begin{aligned} \eta_{\widehat{\mathrm{WY}}}^{\mathrm{Riem}}(\Phi_{\alpha,\tau}) &=\frac{\alpha^2(1+\sqrt{1-\tau^2})}{2(1-\tau^2)},\ \eta_{x^{-1/2}}^{\mathrm{Riem}}(\Phi_{\alpha,\tau}) &=\frac{\alpha^2}{\sqrt{1-\tau^2}},\ \eta_{\mathrm{BKM}}^{\mathrm{Riem}}(\Phi_{\alpha,\tau}) &=\frac{\alpha^2}{2\tau}\log\frac{1+\tau}{1-\tau}. \end{aligned} $$

The kernels are $(1+\sqrt{x})^2/(4x)$, $x^{-1/2}$ and $\log(x)/(x-1)$, with the BKM value $1$ at $x=1$. The contraction coefficient is the literal supremum of $\langle\Phi(A),\Omega_{\Phi(\rho)}^\kappa(\Phi(A))\rangle/ \langle A,\Omega_\rho^\kappa(A)\rangle$ over all positive definite trace-one $2\times2$ complex matrices $\rho$ and all nonzero traceless Hermitian matrices $A$. The spectral action is $(\Omega_\rho^\kappa(X)){ij}=\kappa(\lambda_i/\lambda_j)X{ij}/\lambda_j$.

Koutschan, Krattenthaler and Schlosser, arXiv:2401.08481v1, Conjecture 23, states: “Moreover, the following identities are conjectured to hold for all n ≥ 3:”. Equation (10.10) is

$G_{3,0,3,3}(n)=\frac23G_{0,1,-2,-4}(n+1)=-\frac1{672}G_{1,3,-2,-8}(n+1)=\frac1{63}G_{5,4,3,-5}(n)=\frac4{1002001}G_{6,6,3,-9}(n)=-\frac85G_{9,5,8,-2}(n-1)$.

The preregistration is #19236. The Library note records the source definition and all three equations.

Statement echo

| Source clause | Lean counterpart | Fidelity | | --- | --- | --- | | Equation (1.2): falling factorial divided by $p!$ for $p\ge0$, zero for $p<0$ | ShiftedG.binom | Rational Ring.choose on the nonnegative branch, integer lower argument. | | Section 10 determinant | ShiftedG.G | Integer parameters, rational entries, integer powers of 2 and zero-based Fin n indices. | | “for all n ≥ 3” | TenTen.claim | Natural size and the original lower bound. | | Every consecutive equality of (10.10) | TenTen.claim and TenTen.result | Original coefficients, signs and size shifts; a chain is a conjunction of adjacent equalities. |

Natural subtraction is truncated at zero; within the source range it agrees with integer subtraction. The rational/integer coercions express the same source entries. There are no additional assumptions on the conjecture.

Erdős's 1989 reminiscence, page 2 (verbatim):

He told me about his last paper. Let e_i = 0 or 1. Then Σ_{i=1}^{n} e_i k^i = x^2 has infinitely many solutions for k = 2, 3 and 4. He conjectured that it has only a finite number of solutions for k > 4. In fact, the only nontrivial solution he found was 7^3 + 7^2 + 7 + 1 = 20^2, and perhaps there are no others (1 + (k^2 − 1) = k^2 counts as trivial).

The literal refuted statement is the proposition claim:

∀ (k x : ℕ) (S : Finset ℕ),
  5 ≤ k → 1 < x → BinaryBaseSquare k x S →
    (k = 7 ∧ x = 20) ∨ k = x ^ 2 - 1

Here BinaryBaseSquare k x S means Nat.Coprime k x ∧ ∑ i ∈ S, k ^ i = x ^ 2. The exponent set includes zero because the printed example contains k^0 = 1. "Trivial" means the two-digit family x^2 = k + 1, equivalently k = x^2 − 1, matching Erdős's parenthetical after renaming the base variable. The coprimality condition gcd(k, x) = 1 comes from Mahler's setting and excludes digit-shift scalings x ↦ k·x. The counterexamples (12, 521) and (8, 11677) are in no trivial family under either reading.

This refutation makes no claim about Mahler's finiteness conjecture for any fixed k > 4 and no claim about infinitude for k = 2, 3, 4.

C.-F. Chen, K. Kato and F. G. S. L. Brandão, Matrix Product Density Operators: when do they have a local parent Hamiltonian?, arXiv:2010.14682v3, Section III.C (PDF p. 17), Conjecture III.2:

For any channel $\mathcal E: C \rightarrow C'$ with local contraction ratio $\eta_{1,C}:=\sup_{\rho_C,\rho'C}\frac{\lVert\mathcal E_C[\rho{C}]-\mathcal E_C[\rho'{C}]\rVert_1 }{\lVert\rho{C}-\rho'{C}\rVert_1} <1$ There exists a global constant $\eta < 1$ such that for any tripartite system $ABC$ and any state $\rho{ABC}$, it holds that $I_1(A:C'|B){\mathcal E(\rho)} \le \eta I_1(A:C|B)\rho$.

Here $I_1(A:C|B)=\lVert\rho_{ABC}-\rho_A\otimes\rho_{BC}\rVert_1-\lVert\rho_{AB}-\rho_A\otimes\rho_B\rVert_1$ (Definition 2, PDF p. 14). The verbatim texts are in the literature note. Issue #14728 preregisters the reading over finite-dimensional Kraus channels and density matrices, and the refutation.

J.-C. Bourin and E.-Y. Lee, Eigenvalue inequalities for positive block matrices with the inradius of the numerical range, arXiv:2111.15180v1, printed page 6, Conjecture 3.3, states:

Let $X\in\mathbb{M}_n$. If the inequality

$$\left|\begin{bmatrix}A&X\X^*&B\end{bmatrix}\right|\infty\le|A+B|\infty$$

holds for all positive block-matrix with $X$ as off-diagonal block, then $X$ is essentially Hermitian.

The source says: “If W(T) is line segment, then T is a so-called essentially Hermitian matrix.” The binding convention of #13752 is the literal affine expression $X=\alpha H+\beta I$, with $H=H^*$ and $\alpha,\beta\in\mathbb C$, including points. The norm is the Euclidean operator norm, and positive means positive semidefinite. The same question is Conjecture 7.3.3 of Bourin's A journey into Matrix Analysis, arXiv:2307.03064v1, printed page 114.

J. Sud, J. Marshall, Z. Wang, E. Rieffel and F. A. Wudarski, Dual-map framework for noise characterization of quantum computers, arXiv:2112.04414v1 (2021); Phys. Rev. A 106, 012606 (2022), Section IV, “Local vs Non-Local Channels”, state:

We conjecture that the effective channel with the maximally entangled $\chi$ matrix is the worst case scenario for the proposed MATEN protocol.

However, this conjecture requires more rigorous treatment, which we leave as an open problem.

These sentences occur in main.tex, lines 289 and 290, respectively, in the downloaded v1 source (709 lines; MD5 b2275e7db7e3a63cc4c871c172f7943a). The source specifies $\chi=|\Psi\rangle\langle\Psi|$ with $|\Psi\rangle=\tfrac12\sum_{i=0}^3|ii\ldots i\rangle$ on $N$ four-dimensional process factors (lines 286–289), and evaluates $F(\chi,\chi_{\mathrm{MA}})=4^{-N}$ (lines 292–296). Its MATEN definition is at lines 226–232. See also the literature note.

Issue #20689 fixes the settlement as a universal fidelity lower bound and attainment by cyclic wire permutations. The source's particular GHZ witness and its trace-preservation assertion require the qualification in Triage.

Write $a\in{0,1,2,3}^N$ for a Pauli string and $P_a=\bigotimes_k\sigma_{a_k}$, with $\sigma_0=I$, $\sigma_1=X$, $\sigma_2=Y$ and $\sigma_3=Z$, without Hilbert–Schmidt normalization. The formal definitions are:

• IsProcessCPTP means $\chi\succeq0$ and $\sum_{a,b}\chi_{ab}P_bP_a=I$. This is the process representation of $\mathcal E_\chi(\rho)=\sum_{a,b}\chi_{ab}P_a\rho P_b$, matching the source's CP and TP conditions at lines 93–100.
• marginal is the single-site partial trace: $(\chi_k){ij}=\sum{y:y_k=i}\chi_{y,y[k\leftarrow j]}$. productMap forms $\chi_{\mathrm{MA}}=\bigotimes_k\chi_k$, entrywise $(\chi_{\mathrm{MA}}){ab}=\prod_k(\chi_k){a_kb_k}$.
• The fidelity used is squared Uhlmann fidelity, $F(\rho,\sigma)=(\operatorname{Re}\operatorname{tr}\sqrt{\sqrt\rho,\sigma\sqrt\rho})^2$, exactly sqFidelity. This convention agrees with the source's projector calculation and distinguishes squared fidelity from root fidelity.
• Put $U_N=(\mathtt{qubitPermutation}(\mathtt{finRotate},N))^{\mathsf T}$. Here the untransposed permutation matrix has entries $1$ when $y=x\circ\mathtt{finRotate},N$ and $0$ otherwise. shiftCoeff is $\psi_N(a)=2^{-N}\operatorname{tr}(P_aU_N)$, and rankOneDensity gives $\chi_N=\psi_N\psi_N^\dagger$, with entries $\psi_N(a)\overline{\psi_N(b)}$.

Bonetto and Jardón Kojakhmetov, On the Eigenvalues of Graphs with Mixed Algebraic Structure, arXiv:2408.00487v1, Section 3, Conjecture 1 states:

The signature of the matrix M(ε) is a monotonic decreasing function of ε.

For every universe-polymorphic finite vertex type V with Fintype and DecidableEq instances, let F,G,H be simple undirected loopless graphs on V with disjoint G,H and G union H = F. Set M(u)=L_G+u A_H over the reals, using the ordinary combinatorial Laplacian and 0/1 adjacency matrix. For every real 0<s≤t, the entire assertion is

signature(M(t)) ≤ signature(M(s)).

Signature is the integer number of positive roots minus negative roots of the actual characteristic polynomial, counted with algebraic multiplicity; zero roots contribute zero. For these symmetric matrices, the full root multiset equals the indexed spectral eigenvalue multiset. Decreasing means nonincreasing, allowing equality and constant intervals. Singular matrices, persistent kernels, disconnected graphs, empty edge classes, the empty vertex type, s=t and the whole positive parameter axis remain included. Transition counts, limiting signatures, strict decrease and substitution of zero for a positive parameter are separate assertions and are not claimed.

Conjecture 2. For a c-q state ρXB, the conditional subentropy Q(X|B) satisfies the following bound: Q(X|B) ≤ Hmin(X|B) = − ln pguess(X|B).

The supplied locator is arXiv:1310.1312v1, §2.5.1, Conjecture 2. Let p be any finite probability distribution and rho_x any finite-dimensional density states. Conditional subentropy is Q(recordState p rho) minus Q(mixtureState p rho), using the canonical states. The strengthened target is

$$ Q(X|B)\le1-p_{\rm guess}(X|B)\le-\log p_{\rm guess}(X|B). $$

D. Gabrić and J. Shallit, Smallest and Largest Block Palindrome Factorizations, arXiv:2302.13147v2, §3, p. 5, Conjecture 5; WORDS 2023, DOI 10.1007/978-3-031-33180-0_14:

Let $k\geq2$. Then $E_k=1+\sum_{i=1}^{\infty}a_i k^{-i}$ where the sequence $(a_n/2)_{n\geq1}$ is A274199 in the On-Line Encyclopedia of Integer Sequences (OEIS).

A274199 has offset zero. The paper's displayed coefficients $2,4,6,10,16,\ldots$ fix $a_i=2,\mathrm{A274199}(i)$ for $i\geq1$.

Statement echo

| Source clause | Lean counterpart | Fidelity | | --- | --- | --- | | A word is over a $k$-letter alphabet | Lists over Fin k, enumerated by DepthBudgetIidGreedyOptimality.words | Uniform cardinality is $k^n$. | | $w=w_m\cdots w_1w_0w_1\cdots w_m$, with nonempty outer blocks and possibly empty centre | GreedyRenewal.IsBPFactorization | bs lists the outer blocks from the centre outwards; the two flattenings have the source order. | | Width $2m$ or $2m+1$ according to the centre | GreedyRenewal.bpWidth | The empty word has width zero, extending the source without affecting a limit at infinity. | | Largest width over all valid factorizations | GreedyRenewal.largestBPWidth | The supremum is over valid widths; its boundedness is proved. | | $E_{n,k}=k^{-n}\sum_{i=1}^n i,\mathrm{LBP}k(n,i)$ | LargestFactorizationExpectedWidth.expectedWidth | The definition is the uniform function-space average. The private expectedWidth_weighted_count identity gives the source's weighted width-count expression. | | A274199 is the limiting reverse row of A274190 | CompositionInversion.a274190_stable and a274190_diagonal_limit | For $N\geq2d$, the diagonal equals $g(2d,d)$. The triangle includes $g(n,0)=1$ and the recurrence for every positive column. | | Every integer $k\geq2$ and convergence to $1+2\sum{i\geq1}\mathrm{A274199}(i)k^{-i}$ | LargestFactorizationExpectedWidth.claim and result | claim states existence of every reverse-row limit, summability of the positively indexed series, and convergence of the uniform average to one plus that series. result applies coefficient_limit_results to all three clauses. |

The auxiliary parameters in border and peeling statements range over arbitrary list alphabets. They strengthen the supporting statements and add no hypothesis to the settling result.

Open Problem 1 of the linked paper asks:

Give a bijective proof of the factorization of Corollary 1 for d=1, refining Theorem 2 to a canonical bijection between each anchor class {E=j} intersect C_kappa and the set of classical parking functions.

The relevant specialization has n>=1, m=n+1, s=2, and d=1. Every car has an ordered pair consisting of an anchor and a distinct second choice. The anchor is tried first. If it is occupied, the car begins a clockwise scan at the second choice itself, so offset zero must be inspected before later spots. The matrix kappa fixes the positive clockwise increment from anchor to second for every car, and j fixes the actual unique vacancy.

The exact formal target is result n hn increments j: for every natural n with 1<=n, every per-car increment matrix with entries in 1..n, and every circular spot j, it certifies Function.Bijective (fixedFiberEquiv n increments j). The referenced equivalence remains the explicit forward map and inverse between the corresponding literal actual fiber and classical length-n parking functions; result is its sole source-level settlement theorem.

Benjamin Testart, On minimal pattern-containing inversion sequences, arXiv:2602.12130v2, Section 7, Question 1, printed page 17, asks:

Find bijections between the families $\mathrm{IP}{n,k}$ or $\mathcal T{n,k}$ of Section 6 and other families of combinatorial objects known to be counted by the poly-Bernoulli numbers of type C.

The question offers an IP-side or a T-side answer. The target here is the entire T-side family, rather than the source's already published IP/T correspondence. Section 6 defines unordered rooted increasing trees. For every pair of integers $a,b\ge1$, write $N=a+b-1$. The source $T(a,b)$ consists of trees on distinct labels $0,\ldots,N$, rooted at zero, whose internal labels are exactly $0,\ldots,a-1$ and whose leaves are exactly $a,\ldots,N$. Every parent label is smaller than its child label. The target $P(a,b)$ consists of permutations of $[N]$ whose strict excedance-position set is exactly $[b-1]$, allowing fixed points. Here $[0]=\varnothing$.

The fixed forward map deletes zero, reads each component root-first by DFS with decreasing child-root labels, and makes each word a directed cycle, sending each letter to the next and the last to the first. If the resulting permutation is $\sigma$, the output is $F(t)=D_N(\sigma)$, where

$$ D_N(\sigma)(i)=N+1-\sigma(N-i)\quad(1\le i<N),\qquad D_N(\sigma)(N)=N+1-\sigma(N). $$

The fixed reverse map applies $D_N$, starts each directed cycle at its minimum without reversing direction, attaches every later letter to the rightmost preceding smaller letter, and attaches each cycle minimum to a restored zero root. Forgetting traversal order gives $H$. The target is both landings and both identities $H(F(t))=t$ and $F(H(\pi))=\pi$, for every source tree and target permutation and every positive $a,b$. There is no bound on $N$, no plane or binary restriction, and no omission of $a=1$, $b=1$, $N=1$ or singleton cycles. The unchanged fixed-map statement is specified in #22578.

G. Champagne, N. Johnston, M. MacDonald and L. Pipes, Spectral properties of symmetric quantum states and symmetric entanglement witnesses, Linear Algebra Appl. 649, 273–300 (2022), arXiv:2108.10405v1, study the eigenvalues of symmetric entanglement witnesses.

• Witnesses. A symmetric entanglement witness is a Hermitian W on C^d ∨ C^d with (v ⊗ v)*W(v ⊗ v) ≥ 0 for all v (§2.3); positive semidefinite W are included (footnote 1).
• Theorem 3. For d = 2 and real µ1 ≥ µ2 ≥ µ3, the inequalities (a) µ2 ≥ 0 and (b) µ3 ≥ −√(µ1µ2) are sufficient for the existence of a symmetric witness with these eigenvalues, and necessary for decomposable ones. Every symmetric witness satisfies (a) and a weaker inequality (c).
• The conjecture. After Theorem 3 and in §6(c) (page 20): "We conjecture that inequalities (a) and (b) from that theorem provide the correct characterization."

The verbatim statements are in the literature note.

Issue #17536 fixes the reading:

• C²∨C² is identified with C³ through the orthonormal Dicke basis e₀₀, (e₀₁ + e₁₀)/√2, e₁₁, in which v ⊗ v has coordinates (v₀², √2 v₀v₁, v₁²).
• "Eigenvalues µ1 ≥ µ2 ≥ µ3" means that the characteristic polynomial is (X − µ1)(X − µ2)(X − µ3).
• The conjecture: for all real µ1 ≥ µ2 ≥ µ3, a symmetric witness with these eigenvalues exists if and only if µ2 ≥ 0 and µ3 ≥ −√(µ1µ2).

The conjecture is proved in this reading.

Duncan Adamson, Moritz Dudey, Pamela Fleischmann and Annika Huch, Word Chain Generators for Prefix Normal Words, arXiv:2508.19619v1, Conclusion, pp. 17–18, ask:

Is there a path from any prefix normal generator to all others, just by swapping neighbouring numbers?

The institutional 18-page accepted author manuscript (AAM) poses the same question. For every positive n, the vertices are permutations of 1,...,n whose complete flip-to-zero chains are prefix normal. Starting at the all-one word, each entry names the position to flip. All n+1 states, including both endpoints, must satisfy the comparison of every contiguous factor with the prefix of the same length. A move exchanges entries at adjacent positions; their distinct values can be arbitrary. Every intermediate permutation must remain a valid generator. The requested path is finite and may have zero moves. No shortest-path, direction or complexity requirement is imposed.

Campoamor-Stursberg, Herranz, Latini, Marquette and Blasco, Nonlinearity 39, 055008, arXiv:2502.02491v2, Conjecture 1(iii), asks for number and ladder operators constructed from the quantum symmetries (2.8), satisfying (2.9)–(2.10) with the factorization (5.1) for every $N\geq1$. Preregistration: #19957.

The binding polynomial formulation is proved by D5.S3.Quantum.CampoamorStursbergZernikeLadder.result. Operators are complex linear endomorphisms of $\mathbb C[q_1,q_2]$. For every $N\geq1$ and every complex coefficient sequence there are two symmetries with the kinetic terms and correction span of (2.6), and number and ladder operators in the unital algebra generated by $K_1,K_2,K_3$, satisfying all four identities of the claim.

Statement echo

| Source clause | Lean counterpart | Scope | | --- | --- | --- | | Coordinate multiplication and $-i$ times partial differentiation, (2.1) | Core q, p | Fin 2 indices 0 and 1 encode source coordinates 1 and 2. | | Hamiltonian and angular momentum, (2.3), (2.5) | Core dot, hamiltonian, angularMomentum | Composition of polynomial endomorphisms; arbitrary complex coefficients. | | Normal-ordered correction monomials of positive degree at most $2N$ and grading zero, (2.6) | Core monomial, corrections | The defining span uses exactly these conditions. | | Two commuting symmetries with prescribed kinetic terms, (2.6)–(2.7) | Core IsSymmetry; both first conjuncts of claim | Momentum-order upper bound; no exact-order assertion at degenerate coefficients. | | $K_1=C$, $K_2=(I'-I)/2$, $K_3=[K_1,K_2]$, (2.8) | Core k1, k2, k3 | Literal binding definitions. | | Operators constructed from these three generators | Three Algebra.adjoin memberships in claim | The unital generated algebra; no extra hypotheses. | | Raising and lowering commutators, (2.9) | First two final conjuncts of claim | Equalities of endomorphisms. | | $K_+K_-=\Phi(H,K)$ and the shifted commutator, (2.9)–(2.10) | Last two conjuncts of claim | Core phi1, phi2, phi give exactly (5.1). | | Every order and every coefficient choice | Universal binders of claim | $N\geq1$; only indices 1 through $N$ are used. |

The divided-difference definitions are auxiliary polynomial expressions. The claim has no localization, invertibility, nondegeneracy or analytic-domain hypothesis. No clause of the binding claim is dropped.

R. Dumitru, J. Franco, and A. Merino, On The Linearization of Alternative Means, arXiv:2606.25150v1, §1, ask in the supplied verbatim text:

Question : Can we characterize all functions f : (0, ∞) → (0, ∞) such that Aσ̂_f B is linearizable if and only if AB = BA and |Spec(A⁻¹♯B)| ≤ 2 ?

Remark 4.4 restates this question. Definition 2.3 specifies $A\widehat\sigma_fB=f(Y)Af(Y)$ with $Y=A^{-1}\sharp B$, for continuous positive $f$ with $f(1)=1$. Remark 2.2 calls a mean linearizable when it equals $aA+bB$ for real $a,b$.

Conjecture: T(n+m+1,m+1) = (n+m)! * (Product_{i=1..m} (n+i)^i) * Sum_{j_1=0..n} Sum_{j_2=0..j_1} ... Sum_{j_m=0..j_{m-1}} (-1)^(n*m + j_1 + j_2 + ... + j_m) * (Product_{1 <= q < p <= m} (j_q - j_p + p - q)^2) * Product_{t=1..m} (n+t-1){j_t} / ((n-j_t+t)^(m+1) * (j_t+m-t)!) where (x){n} is the falling factorial defined as (x){n} = Product{k=0..n-1} (x-k). - Mikhail Kurkov, May 24 2026

The target quantifies over every natural n and every m >= 1, with equality in the rationals. T is the unsigned Stirling number of the first kind. The chain is n >= j_1 >= ... >= j_m >= 0. Falling factorial means the displayed descending product. This is the exact source assertion registered before formal probes in https://github.com/the-omega-institute/trureturing/issues/9456.

Conjecture: For all integers m > 0, Sum_{n>=0} L(n)^m * log(1+x)^n/n! is an integer series whenever Sum_{n>=0} L(n)*log(1+x)^n/n! is an integer series.

A167138, A167139 and A167141 repeat this one general Hanna question. An integer series has integer ordinary coefficients. Let K be any characteristic-zero field and L any function from natural numbers to K. Put E_L(t)=sum L(n)t^n/n! and ell(X)=log(1+X). The exact conclusion is integrality of E_(L^m)(ell(X)) for every positive integer m whenever E_L(ell(X)) is integral, at every degree including zero. The natural positive exponent in Lean is the equivalent representation of a positive integer exponent. L(0) is arbitrary. No extra integral-L assumption, analytic convergence, finite support or degree/power bound is introduced.

S. N. Santalla, S. Singha Roy, G. Sierra and J. Rodríguez-Laguna, The hyperlink representation of entanglement and the inclusion-exclusion principle, arXiv:2601.17926v2, Phys. Rev. A 114, 022431 (2026), define the entanglement hyperlinks J_I = Σ_{A⊆I} (−1)^{|I|−|A|} S_A of the entanglement entropies S_A of a pure state on N parties (Eq. (5)).

Appendix B proposes the even-legged reconstruction S_A = Σ_{|I| even} Λ_{|I|,|I∩A|} J_I (B2), with Λ_{2l,0} = Λ_{2l,2l} = 0 and Λ_{2l,p} = Λ_{2l,2l−p}. It lists the leg-factors for 2l ≤ 8 (B5) and states: "It is still to be proved that the leg-factors Λ_{2l,p} exist and do not depend on N" and "the validity of Eq. (B2), with leg-factors that do not depend on N, has only been checked up to N = 9". The verbatim statements are in the literature note.

Issue #16381 fixes the reading: there are leg-factors, independent of N, with the zero and symmetry laws, such that (B2) holds for every N. It is proved.

P. Kagey's OEIS A350532 COMMENT states verbatim:

Conjecture: T(2*n,2) = n.

The settled statement is $T(2n,2)=n$ for every $n\in\mathbb N$, including zero.

The source's NAME defines the count verbatim:

Triangle read by rows: T(n,k) is the number of degree-n polynomials over Z/2Z of the form f(x)^m for some m > 1 with exactly k nonzero terms; 1 <= k <= n + 1.

Statement echo

| Source clause | Lean counterpart | Fidelity | | --- | --- | --- | | Degree-n polynomials over Z/2Z, exactly k nonzero terms, some exponent m > 1 | KageyA350532Binomials.T | The literal cardinality subtype; distinct nonzero polynomials, with witnesses for base and exponent. | | Conjecture: T(2*n,2) = n. | KageyA350532Binomials.claim and KageyA350532Binomials.result | Literal universal assertion under the preregistered conventions. | | No restriction to positive degree in the definition | p ≠ 0 together with p.natDegree | The preregistered nonzero convention prevents zero from entering the degree-zero count. | | Natural-number variables | The natural-number binders and arithmetic | Subtraction and division in the trinomial assertion are natural-number operations. |

Charles Cornell Norton, OEIS A398542, August 1, 2026; revision 18, August 30, 2026, 18:45:04, exact selected %F:

Conjecture: for every m >= 1 and every b in S(m), d(b,k) = p(k)*binomial(2*k,k) + q(k)*4^k for polynomials p and q depending on b, with deg p <= m-1 and deg q <= m-2. Verified for m <= 6 and k <= 12.

S(m)=Av_m(132). For every m>=1 and b in S(m), choose p_b,q_b in Q[X] independently of k such that the displayed identity holds for every k>=0. The degree bounds are m-1 and m-2 for m>=2, with q_b=0 when m=1. Here d(b,k) counts actual permutations of 1,...,m+k avoiding 1324 whose lower-value subsequence is exactly b and whose standardized upper-value subsequence avoids 213. The value cut is fixed, the empty upper cell is allowed, and d(b,0)=1. Rational coefficients are an explicit sufficient choice beyond the source's unspecified coefficient field.

M. Adamaszek, Hard squares on cylinders revisited, arXiv:1202.1655v2, Section 7, Conjecture 7.4, states:

The length of every cycle in the graph Neck(k, n) divides n−3k. In other words, for every (k, n)-necklace N we have Tⁿ⁻³ᵏN = N.

The section assumes even positive circumference n and positive k. A necklace has 2k distinct stones, each with signed vector −2, −1, 1 or 2. Consecutive stones have opposite directions. Away-facing gaps are odd; toward-facing gaps plus both vector lengths are odd. A toward-facing gap is at least three, and at gap three both vectors have length one. Necklaces are identified under circle isometries. T performs simultaneous JUMP, then TURN (−2→1, −1→2, 1→−2, 2→−1), then FIX of facing gaps three by shortening length-two vectors to one. Issue #11582 fixes this reading before the probe.

F. Ding and X. Hu, Masking quantum information on hyperdisks, Phys. Rev. A 102, 042404 (2020), arXiv:1909.11256v3, state in the conclusion at line 651 of masking.tex:

Nevertheless, it is an open question for a nondegenerate masking machine whether the number of hyperdisks in the set of maskable states is always finite. A related open question is whether a regular subset of a hyperdisk can be covered with finite number of hyperdisks.

The settled question is the second sentence. In the module, a hyperdisk is a set of unit vectors in EuclideanSpace ℂ (Fin n) represented by an orthonormal family φ, positive real coefficient moduli r, equality of the span of φ with the span of the set, and equality with the full unit-vector level set having those coefficient moduli. A regular subset c of s satisfies IsHyperdisk s and (Submodule.span ℂ c : Set _) ∩ s = c. The claim asks, for every natural n and every such c and s, for a natural k and a map h : Fin k → Set (EuclideanSpace ℂ (Fin n)) such that every h i is a hyperdisk contained in c and c = ⋃ i, h i.

A. Kumar, S. Peng and V. Tran, Integer Complexity Generalizations in Various Rings, arXiv:2211.04379v1, Section 4, Conjecture 4.4:

E(m, 2) is the third most inefficient for odd m.

The source defines expressions from copies of $x$ using addition, multiplication and parentheses, evaluates them in $\mathbb{Z}/m\mathbb{Z}$ at a base $s$, and defines $E(m,s)$ as the maximum expression complexity over residues. The binding proposition reads “third” by individual unit bases: for every odd $m \ge 3$, at most two units $s$ satisfy $E(m,2)<E(m,s)$. Bases $3$ and $16$ tie in the witness, so dense ranking by distinct inefficiency values is outside this proposition.

Statement echo

• The universal modulus binder is $m : \mathbb{N}$ with an anonymous $[\operatorname{NeZero}(m)]$ instance.
• The hypotheses are $3 \le m$ and $\operatorname{Odd}(m)$.
• The base is the residue $2 : \mathbb{Z}/m\mathbb{Z}$.
• The comparison domain is all units $s : (\mathbb{Z}/m\mathbb{Z})^\times$, coerced to $\mathbb{Z}/m\mathbb{Z}$.
• The conclusion is that the cardinality of the filtered units satisfying $E(m,2)<E(m,s)$ is at most $2$.
• The expression, leaf-count, evaluation, complexity and inefficiency clauses are represented by Expr, Expr.leaves, Expr.eval, complexity and inefficiency in the settling module.

Conjecture 5.2 of arXiv:2408.14632v2, as printed:

Set U_n := U_n(p, q), and let m >= 1 and n in Z. Assume that both p and m are even. If U_{2n} = 0 (mod m) and U_{2n+1} = q^n (mod m), then exactly one of the following two conclusions occur: (i) U_n = 0 (mod m), or (ii) U_n = m/2 (mod m) where n = c * e_U(m)/2, where c is some odd integer and e_U(m) is the entry point of m in (U_n).

The paper adds a second sentence: "Can we give conditions for when Conclusion (i) versus Conclusion (ii) occurs?"

D. Sain, J. Manna, K. Paul, On local preservation of orthogonality and its application to isometries, arXiv:2407.08900v1, Linear Algebra and its Applications (2024), states:

Definition 1. Let X be a Banach space. A set A ⊂ S_X is said to be a Koldobsky-set, for the sake of brevity, a K-set, if any operator T ∈ L(X) that preserves Birkhoff-James orthogonality at each point of A, is necessarily a scalar multiple of an isometry.

Definition 3. Let X be a Banach space having a finite K-set. Then the K-number of X is defined by min{|A| : A is a K-set of X}. We denote the K-number of X by κ(X).

The Open Question at the end of §2 is:

Open Question: Characterize the minimal K-sets in ℓ^n_∞ and hence find κ(ℓ^n_∞).

The spaces are real, and minimality is under inclusion. The result determines the K-number for $n\ge2$ and characterizes the minimal K-sets consisting of extreme points; it leaves the classification involving non-extreme points open.

For every normalized pure state $\psi\in(\mathbb C^2)^{\otimes4}$, the average two-qubit marginal von Neumann entropy in bits satisfies

$$\frac{S(\rho_{AB})+S(\rho_{AC})+S(\rho_{AD})}{3}\le 1+\frac12\log_2 3.$$

Equality is attained at the explicit Higuchi–Sudbery state

$$|M_4\rangle=\frac1{\sqrt6}\bigl[|0011\rangle+|1100\rangle+\omega(|1010\rangle+|0101\rangle)+\omega^2(|1001\rangle+|0110\rangle)\bigr],\qquad\omega=e^{2\pi i/3}.$$

Higuchi–Sudbery, Section 3: “Given that a four-qubit state cannot have maximal entropy of entanglement for every two-qubit subset, we now ask what is the greatest possible average for such entropies, i.e. we seek to maximise”. Their average over the six pairs equals the displayed average over the three complementary cuts.

Conjecture 1. Subentropy is subadditive: Q(ρAB) ≤ Q(ρA) + Q(ρB).

The supplied locator is arXiv:1310.1312v1, §2.3.1, Conjecture 1. The related restatement in arXiv:1510.08859v2, §7.1 is:

At present, we do not know wether the subadditivity inequality of subentropy is true or not

The assertion concerns every finite-dimensional bipartite density state, with no commutation, rank or separability restriction. In the canonical partial-trace interface, marginalRight retains A and marginalLeft retains B.

Robert Davis, Width-k Generalizations of Classical Permutation Statistics, JIS 20 (2017), gives the following descent-set line, generating function, and MacMahon identification together at the top of printed page 2. Printed page 1 ends with the preceding descent-count formula:

where Des σ = {i ∈ [n − 1] | a_i > a_{i+1}}. Given any statistic st, one may form the generating function F_n^{st}(q) = Σ_{σ∈S_n} q^{st σ}. A famous result due to MacMahon [6] states that F_n^{des}(q) = F_n^{exc}(q), and that both are equal to the Eulerian polynomial A_n(q). The Eulerian polynomials themselves may be defined via the identity Σ_{j≥0} (1 + j)^n q^j = A_n(q)/(1 − q)^{n+1}.

Printed page 2 defines width-k descents:

For each of the following definitions, we assume n ∈ Z_{>0}, k ∈ [n − 1], ∅ ≠ K ⊆ [n − 1], and σ = a_1 a_2 ··· a_n ∈ S_n. We define a width-k descent of σ to be an index i ∈ [n − k] for which a_i > a_{i+k}. Thus the width-1 descents are the usual descents of a permutation. Let Des_k(σ) = {i ∈ [n − k] | a_i > a_{i+k}} denote the set of all width-k descents of σ, and set des_k(σ) = |Des_k(σ)|.

Printed page 6 introduces the Laurent polynomial and the named conjecture:

We now show that interesting behavior occurs when considering the function G_{n,k}(q) = Σ_{σ∈S_n} q^{des_k(σ)−des_{n−k}(σ)}. According to computational data, the following conjecture holds for all n ≤ 9 and 1 ≤ k < n for which gcd(k, n) = 1.

Conjecture 9. If gcd(k, n) = 1, then G_{n,k}(q) = n q^{1−k} A_{n−1}(q).

The formal theorem makes the surrounding range explicit: for all natural n and k, if 1 <= k, k < n, and Nat.Coprime k n, then

G(n,k) = n * q^(1-k) * eulerian(n-1).

Here eulerian(m) is the descent generating function that the paper identifies with A_m by MacMahon's theorem. The paper's separate infinite-series definition of the Eulerian polynomials is not formalized. One-based positions are transported to Fin n, and signed exponents live in the Laurent polynomial ring over the integers.

Wiseman, Steinberg and Hallaji, “Obtaining a single-photon weak value from experiments using a strong (many-photon) coherent state”, AVS Quantum Science 5, 024401 (2023), arXiv:2211.15761v2, Section V, page 6:

This supports earlier approximate results which suggested that if a photon-number resolving detector were used, the weak value post-selected on detecting m photons would exceed the no-click weak value by precisely m times the single-photon number. We leave a rigorous proof of this conjecture for future work.

Issue #17772 fixes the finite-mode Fock conventions. For every $k+1$-mode passive network $A,B$, coherent amplitude $\alpha\ne0$, and natural count $m$ of nonzero resolved probability, the conclusion is $W_m-W_0=mw$ when $m>0$. For $m=0$ the difference is zero without requiring a single-photon denominator. The detector acts on mode zero and ignores the remaining modes; the probed mode is also indexed zero, with arbitrary passive evolution between probing and detection.

Statement echo

| Source clause | Lean counterpart | Fidelity | | --- | --- | --- | | Arbitrary passive linear network | Every natural $k$ and $A,B:\operatorname{EuclideanSpace},\mathbb C,(\operatorname{Fin}(k+1))\simeq_{\mathbb C}^{\mathrm{iso}}\operatorname{EuclideanSpace},\mathbb C,(\operatorname{Fin}(k+1))$ | No fixed dimension, network or intensity | | Coherent input in one mode, vacuum in the others | coherentInput k α, EuclideanSpace.single (0 : Fin (k+1)) α | Literal binding conventions | | Weak measurement of number, with other modes ignored | number, numberProjector m, generalizedWeakValue | Unbounded occupation; exact number-domain proofs; projector retains ignored-mode carrier | | Detect exactly $m$ photons | Every natural $m$ with coherentProbability A B α m ≠ 0 | Conditional values retain nonzero-denominator certificates | | Compare with no click | Existential nonzero vacuum probability and coherentWeakValue ... 0 | Vacuum condition is proved, not an added hypothesis | | Precisely $m$ times the single-photon value | claim, proved by result | Same $A,B$ and probed mode; the positive-count branch proves nonzero single-photon probability | | Zero count | The explicit if m = 0 branch of claim | Difference zero; no single-photon value assigned when its probability vanishes |

All public model definitions and the claim retain the mathematical bodies fixed by #17772; its mode-amplitude carrier is written as $\operatorname{EuclideanSpace},\mathbb C,(\operatorname{Fin} k)$ without a forwarding declaration. BeamSplitter.exponentialCoeff and BeamSplitter.exponentialVector supply the one-mode coefficients and vectors. The arbitrary finite-mode completion and totalness are supplied by PassiveFockModel.

Wei and Yang, Associated Mersenne graphs, arXiv:2407.08237v1, Question 6.2: “For given n and k, how many vertices of Associated Mersenne graph ℳₙ have degree k?” The vertices are labelled binary words for which every circular run of ones is followed by a strictly longer run of zeros. Adjacent vertices differ at one position. The conventions are $\mathbf M_0={\lambda}$ and $\mathbf M_1={0}$.

The original locator is Conjecture 3.1, printed page 124, of the paper identified by DOI 10.13001/1081-3810.3108. The fixed restatement is arXiv:1609.08231v1, §3, Example 3.5. Its setup states:

we assume that [A X; X∗ B], where A, X, B are n × n, is positive semidefinite.

Definition 1.1(iv) states:

M is said to have g-property if sj (M12 ) ≤ λj (M11 ♯ M22 ), j = 1, . . . , n.

Example 3.5 states:

[Φ(A) Φ(X); Φ(X∗) Φ(B)] where Φ : X ↦ X+(trX)In , is PPT … Numerical experiments suggest that the matrix [Φ(A) Φ(X); Φ(X∗) Φ(B)] has g-property, which we haven't been able to prove yet.

The concluding §5 refers to:

Besides the challenging problems described in Example 3.5 and Example 3.6, …

For every natural dimension, all complex matrices A, X, B with positive semidefinite block matrix W=[A X; X* B], and every decreasing index j, the target is

$$ s_j(\Phi(X))\le\lambda_j(\Phi(A)#\Phi(B)), \qquad \Phi(T)=T+(\operatorname{Tr}T)I. $$

S. Rana, P. Parashar and M. Lewenstein, Trace-distance measure of coherence, Phys. Rev. A 93, 012110, arXiv:1511.01854v2, Section III.2, Conjecture 7:

Conjecture 7. For all states ρ, C_{l1}(ρ) ≥ C_r(ρ).

The resolution is Proved for every finite dimension and every complex density matrix, including singular states. Preregistration #16965 fixes the conventions. The source note locates the conjecture and the definitions.

Statement echo

| Source clause | Lean counterpart | Fidelity | | --- | --- | --- | | Every finite-dimensional state | claim quantifies over every natural n and every complex matrix on Fin n; IsState is positive semidefiniteness and trace one | No invertibility or rank hypothesis. In dimension zero the state premise is impossible. | | Section II, Eq. (3b), off-diagonal absolute-value sum | D5.S3.Quantum.Information.CorrelatedCoherenceMonogamyRefutation.l1Coherence | The complex norm gives the absolute value; both indices range over the full basis. | | Section III after Eq. (13), base-two entropy | vonNeumann2 | Negative real trace of continuous functional calculus for $x\log_2x$, with its value zero at zero. | | $C_r(\rho)=S_2(\Delta\rho)-S_2(\rho)$ | coherenceRel | The diagonal map retains exactly the diagonal entries. | | $C_{l1}(\rho)\ge C_r(\rho)$ | claim, proved by result | Literal preregistered inequality. |

IsState and vonNeumann2 have the unchanged defining bodies shared with QuantumTriangularJensenShannonRefutation; the latter imports their general owner. The claim uses the frozen D5.S3.Quantum.Information.CorrelatedCoherenceMonogamyRefutation.l1Coherence for $\sum_{i\ne j}|\rho_{ij}|$; exchanging the branches of its diagonal test gives the same off-diagonal sum term by term. The state and entropy definitions retain the source conventions.

T. Simnacher, J. Czartowski, K. Szymański, K. Życzkowski, Confident entanglement detection via the separable numerical range, Phys. Rev. A 104, 042420 (2021), arXiv:2107.04365v1, Conjecture 8:

For a single measurement on a two-qubit system, the minimal volume ratio is $\mu_{2,1} = \frac{1}{2}$.

Here $\mu_{2,1}$ is the minimum over Hermitian two-qubit observables $A$ of $\operatorname{vol}L_{\mathrm{Sep}}(A)/\operatorname{vol}L(A)$, where $L_X(A)={\operatorname{Tr}\rho A\mid\rho\in X}$ for the set of all states ($L$) or of separable states ($L_{\mathrm{Sep}}$), and vol is the Euclidean volume (Definitions 1 and 2). The paper proves $\mu_{2,1}\ge\sqrt2-1$ (Proposition 7) and $\mu_{2,1}\le\frac12$ with the projector onto $|\phi^+\rangle=(|00\rangle+|11\rangle)/\sqrt2$.

Frederik vom Ende, A Sufficient Criterion for Divisibility of Quantum Channels, arXiv:2407.17103v3, Section V, asks:

An open question at this point is whether our sufficient condition is also necessary, and whether our necessary condition is also sufficient.

The source is arXiv v3, with publication identifier DOI 10.1063/5.0231812. Definition 1 and Lemmas 2–3 specify the elementary channel and inverse; Proposition 1 and Theorem 1 specify the necessary and sufficient conditions. This dossier anchors the combined classification of the two reversals, including their fixed-pair and existential-pair readings.

Let the complex dimension be any finite n ≥ 2, let Φ be an actual CPTP map, and let (Kⱼ) be any finite Kraus representation of Φ. For an ordered pair of orthogonal unit vectors (x,y), E(x,y) means that Φ composed on the right with the inverse of the elementary channel Ψₜ(x,y) is completely positive for some real 0 < t < 1. N(x,y) means ⟨y,KⱼGx⟩ = 0 for every index j and every complex matrix G in the Hilbert–Schmidt orthogonal complement of the whole complex Kraus span. S(x,y) means N(x,y) together with the additional diagonal tests ⟨x,KⱼGx⟩ = 0 over the same indices and complement.

The classification established by the designated result has four cells:

| Reading | Answer | | --- | --- | | Fixed ordered pair: N(x,y) iff E(x,y) | Proved for every map and representation in the stated scope. | | Existential ordered pair: some N pair iff some E pair | Proved for the same map and representation. | | Fixed ordered pair: E(x,y) implies S(x,y) | Refuted in every dimension n ≥ 2. | | Existential ordered pair: some E pair implies some S pair | Refuted in every dimension n ≥ 2; the counterexample has no S pair in any finite Kraus representation. |

The Scribe claim's Proved kind refers to this combined classification, whose statement includes the counterexample. It does not label either E ⇒ S assertion as proved.

The source is the unnumbered request in the conclusion of the paper identified by adamson2026twoword in the Library. Its literal wording is:

We did not find an example of a graph G such that G ∉ G₂. By Remark 30 we know that such a graph exists. Finding such a graph remains an open problem.

Let V = Fin 24 ⊕ Finset (Fin 24). The candidate U₂₄ has an edge from inl a to inr S exactly when a ∈ S, the same adjacency in reverse, and no within-part edges. Its endpoint states that there do not exist lists w,v over V such that (∀ z : V, count z w = 2), (∀ z : V, count z v = 2), and ∀ x,y : V, x ≠ y → (U₂₄.Adj x y ↔ filter (z = x ∨ z = y) w = filter (z = x ∨ z = y) v). These are Definitions 1 and 14 at k = 2. Positive counts give the full vertex set as the alphabet of both words.

The primary source is Question 3.5:

Suppose that F has the n-sum property with respect to U. Is it true that F[G] also has the n-sum property with respect to U_{ε_G}?

The complete statement quantifies over a finite field F with more than two elements, every finite group G, a subgroup U of F's units containing minus one, and the original natural number n at least two. If every field element is a sum of exactly n elements of U, every element of the actual group algebra must be a sum of exactly n genuine units whose coefficient-sum augmentations lie in U. Repetition is allowed. Modular characteristic, noncommutative groups, characteristic two with more than two field elements, and the trivial group remain in scope.

OEIS A059894, NAME (%N, verbatim):

Complement and reverse the order of all but the most significant bit in binary expansion of n. n = 1ab..yz -> 1ZY..BA = a(n), where A = 1-a, B = 1-b, ... .

Ralf Stephan's recurrence conjecture (%F, verbatim):

a(1) = 1, a(2n) = a(n) + 2^(floor(log_2(n))+1), a(2n+1) = a(n) + 2^floor(log_2(n)) (conjectured). - Ralf Stephan, Aug 21 2003

Ralf Stephan's digit-count conjecture (%F, verbatim):

A000120(a(n)) = A000120(A054429(n)) = A023416(n) + 1 (conjectured). - Ralf Stephan, Oct 05 2003

AUTHOR (%A, verbatim):

Marc LeBrun, Feb 06 2001

The definition a applies the quoted transformation to the little-endian list Nat.digits 2 n: drop its last entry, reverse the remaining list, map natural subtraction 1 - d, append [1], and evaluate with Nat.ofDigits 2. The definition complementRest omits only the reversal and represents A054429 on positive inputs. A000120 counts one bits and A023416 counts zero bits in the positive canonical binary expansion.

The literal theorem statement is:

a 1 = 1 ∧
(∀ n : ℕ, 0 < n → a (2 * n) = a n + 2 ^ (Nat.log 2 n + 1)) ∧
(∀ n : ℕ, 0 < n → a (2 * n + 1) = a n + 2 ^ (Nat.log 2 n)) ∧
(∀ n : ℕ, 0 < n →
  (Nat.digits 2 (a n)).count 1 = (Nat.digits 2 (complementRest n)).count 1 ∧
  (Nat.digits 2 (a n)).count 1 = (Nat.digits 2 n).count 0 + 1)

Here Nat.log 2 n agrees with the floor of the base-two logarithm on the positive domain. The counting and recurrence clauses have the explicit guard 0 < n; no such clauses at zero are asserted.

Robin D.P. Zhou and Xinyang Yu, Arrow-Wilf equivalences and enumerative results for short arrow patterns, arXiv:2609.29392v1, abstract:

Together with earlier work of Archer and Laudone, this leaves only (32;1→3) unresolved for |ν|≤2, which we pose as an open problem.

Here S_n(32; 1 → 3) consists of permutations of 1, …, n avoiding the arrow pattern in the paper's sense: the selected values have the required order in the one-line word, and the prescribed arrow holds in π̂ = θ⁻¹(π).

Ahiable, Kothakonda and Winter, arXiv:2608.03390v2, Conjecture 6.7, asks:

Let $\mathcal P_{m,n}\subseteq \mathrm{APPT}{m,n}$ be the inscribed absolute PPT polytope with $2\leq m\leq n,; n>2$. Then $$\max{\lambda\in \mathrm{APPT}{m,n}}\sum{i=1}^{mn}\lambda_i^2=\max_{\lambda\in\mathcal P_{m,n}}\sum_{i=1}^{mn}\lambda_i^2$$ and occurs at the spectra given by Eq. (44).

The resolved sector is $m=3$, every integer $n\geq3$. For a positive semidefinite, trace-one matrix $\rho$ on $\mathbb C^3\otimes\mathbb C^n$, APPT means $(U\rho U^\dagger)^\Gamma\succeq0$ for every unitary $U$, with $\Gamma$ the second-factor partial transpose. The purity is $\operatorname{Re}\operatorname{Tr}(\rho^2)$.

Mohamed Ayad and Rachid Bouchenna, Which Integer Divides the Reverse of Any of Its Multiples?, INTEGERS 25 (2025), #A37, printed p. 9, Problem 1:

Let B ≥ 2 be any number base. Are the divisors of B² − 1 the only positive integers satisfying the property P*_B ?

Section 4.1 on printed p. 8 defines the base-B reverse m*_B by reversing the positional digits of the positive integer m. The property P*_B means that n divides m*_B for every positive multiple m of n. The exact statement is: for all natural B ≥ 2 and all natural n > 0, (∀ m : ℕ, 0 < m → n ∣ m → n ∣ Nat.ofDigits B (Nat.digits B m).reverse) ↔ n ∣ B ^ 2 - 1.

Shane Chern and Shishuo Fu, Signed counting of partition matrices, arXiv:2508.21318v2, Section 5, Question 5.5, page 26:

Find a characterization (possibly in terms of pattern avoidance) of the inversion sequences produced by improper partition matrices under the action of the Claesson–Dukes–Kubitzke bijection.

For each integer $n\geq1$, write $[n]={1,\ldots,n}$ and let $\mathbf I_n={e:[n]\to\mathbb N:0\leq e_j\leq j-1\text{ for all }j\in[n]}$. A native partition matrix on $[n]$ is an upper triangular square matrix $P$ of sets, of any permitted positive dimension $k$, whose nonempty cells partition $[n]$, every row and column is nonempty, and $\operatorname{col}_P(a)\leq\operatorname{col}_P(b)$ whenever $a<b$. The row and column of a label are those of its unique cell.

An adjacent pair $i,i+1$, with $1\leq i<n$, is an ascent or descent only when its labels share a column and have respectively increasing or decreasing row indices. Such a pair is proper precisely when $i$ has the parity of the least label of that column. An improper matrix has no proper ascent or descent; equal-row pairs are neither. Write $\operatorname{IPPM}_n$ for this class.

The fixed source map is

$$ \Pi_n(P)j=\sum{d=1}^{\operatorname{row}P(j)-1} n_d, \qquad n_d=\sum{r=1}^{k}|P_{r,d}|. $$

Thus the summands are column cardinalities, and the sum is zero in the first row. The requested image uses this map and all permitted dimensions.

K. H. Kua, A. Serafini and M. G. Genoni, Daemonic ergotropy of Gaussian quantum states and the role of measurement-induced purification via general-dyne detection, arXiv:2506.22288v2; Quantum Sci. Technol. 11, 015014 (2026), DOI 10.1088/2058-9565/ae2200, Section VI after Eq. (66), state:

We have also numerically verified that non-zero phases ϑ_m lead to worse result, and we can thus conjecture that this fully characterizes the optimal steady-state general-dyne monitoring.

The Library note gives the source locators and Eq. (66). Write $r=2\chi/\kappa$, $\nu=2n_{\rm th}+1$ and $c=\sqrt{1-r^2}$, with $\kappa>0$, $0\le\chi<\kappa/2$ and $n_{\rm th}\ge0$. For every finite physical general-dyne measurement covariance $M$ and physical stationary conditional covariance $S$, the result proves

$$\sqrt{\det S}\ge v_* = \frac{(\nu-1)c+\sqrt{(\nu-1)^2c^2+4\nu}}{2}.$$

The pure aligned covariance

$$M_*=\operatorname{diag}\left(\frac{1-r}{1+r},\frac{1+r}{1-r}\right)$$

has a physical stationary solution attaining this value. No uniqueness of the minimizing measurement is asserted by the public theorem.

Statement echo

| Source clause | Lean counterpart | Fidelity | | --- | --- | --- | | Stable thermal OPO, Eqs. (57)–(58) | claim parameters κ, χ, nth and its four hypotheses; driftA | All damping, pump and thermal parameters in the stated regime | | Thermal input and diffusion | Literal scalar multiples of the identity inside eMat, bMat, steadyEq | $\sigma_{\rm in}=\nu I$ and $D=\kappa\nu I$ | | Passive coupling in physical q,p coordinates | coupling | $C=\sqrt\kappa,\Omega$, with $\Omega=\begin{pmatrix}0&1\-1&0\end{pmatrix}$ | | Source E and B, Eqs. (21)–(25) | eMat, bMat | The inverse matrix square root is CFC.sqrt of the inverse positive matrix | | Stationary Riccati equation, Eq. (55) | steadyEq | Every matrix product, transpose and diffusion term is retained | | Every physical measurement and stationary covariance | claim first conjunct; frozen IsGaussianMeasurementCov (m := 1) | Symmetry and the complex uncertainty matrix being positive semidefinite; arbitrary phase, squeezing and impurity | | Global optimum | vStar; result first conjunct | Universal determinant-square-root lower bound | | Aligned pure measurement, Eq. (66) | optMeas; result second conjunct | Existence of a physical stationary attainer with equality |

The symplectic, thermal-input and diffusion expressions are inlined in the public formulas. Proofs use the frozen PositiveOneModeWilliamson.physicalJ2 through omega_sq, and the frozen physical covariance predicate and public GaussianThermometryJointMeasurementRefutation.physical_data. The finite $2\times2$ real matrix carrier is the source's single-mode covariance representation. Requiring $S$ to be physical restricts the conclusion to conditional covariance solutions; it adds no hypothesis to the source's physical statement. The damping scale cancels without restricting its positive value.

Adrián Lillo and Mercedes Rosas, The Priority Lattice, arXiv:2603.28905v1, Section 6, item 3, pp. 24–25, ask for the number of principal filters $[P,\hat1]$ isomorphic to a priority lattice $\Pi(m)$ with $m\le n$. Their data $2,4,10,34,154,874$ suggest the left factorials, OEIS A003422. The displayed formula is $\theta_n=\sum_{i=0}^{n-1}k!$, whose summation variable and bound do not match the data.

The question and its source conventions are preregistered in #14857. The Library note quotes the source definitions: increasing rooted trees with consecutive label sets, ordered by their root labels; edge inclusion; and an adjoined greatest element.

Q. Tang and T. Zhang, Sharp Schoenberg type inequalities and the de Bruin–Sharma problem, arXiv:2508.10341v3, §1.3, Conjecture 1.13. The source is tang2025schoenberg.

Conjecture 1.13. Let P(z) = z ∏_{j=1}^n (z − z_j), z_j ∈ C \ {0}, and let w_1, …, w_n be the zeros of P′(z). Then for every real number p ≥ 1 we have Σ_{k=1}^n 1/|w_k|^p ≤ ((n+1)^p + n − 1)/n · Σ_{j=1}^n 1/|z_j|^p. Moreover, equality holds if and only if z_1 = ⋯ = z_n.

For every natural $n\ge1$ and every family $z_1,\ldots,z_n\in\mathbb C\setminus{0}$, put

$$ P(Z)=Z\prod_{j=1}^n(Z-z_j),\qquad c(n,p)=\frac{(n+1)^p+n-1}{n}. $$

Let $w_1,\ldots,w_n$ be all roots of $P'$, counted with algebraic multiplicity. No distinctness, simplicity, reality or common argument hypothesis is imposed on the nonzero roots. The result proves the following three clauses:

1. For every real $p\ge1$, $$\sum_{k=1}^n|w_k|^{-p}\le c(n,p)\sum_{j=1}^n|z_j|^{-p}.$$
2. For every real $p>1$, equality holds if and only if $z_i=z_j$ for every $i,j$.
3. Conjecture 1.13 as stated is false: at $p=1$, $n=2$ and $(z_1,z_2)=(1,2)$ give equality although $z_1\ne z_2$.

The formal claim is the conjunction of (i), (ii), and ¬ conjecture, where the original conjecture has its full dimension, root and order quantifiers:

def conjecture : Prop :=
    ∀ (n : ℕ) (hn : 1 ≤ n) (z : Fin n → ℂ), (∀ j, z j ≠ 0) → ∀ p : ℝ, 1 ≤ p →
      (((Polynomial.derivative (P z)).roots.map (fun w => ‖w‖ ^ (-p))).sum ≤
        c n p * ∑ j, ‖z j‖ ^ (-p)) ∧
      ((((Polynomial.derivative (P z)).roots.map (fun w => ‖w‖ ^ (-p))).sum =
        c n p * ∑ j, ‖z j‖ ^ (-p)) ↔ ∀ i j, z i = z j)

Every norm power is a real Real.rpow, including nonintegral orders. The named conjecture is refuted by its endpoint equality clause. The sharp inequality for all $p≥1$ and the strict-order equality case are proved in the same result.

Khoi-Nguyen Huynh-Vu, Lin Htoo Zaw and Valerio Scarani, Certification of genuine multipartite entanglement in spin ensembles with measurements of total angular momentum, arXiv:2311.00806v2, §III, Conjecture 2, Eq. (32), PDF p. 8:

The separable bound for {ȷ̃, ȷ̃′} = {1, K/2} with K ≥ 7 is Psep_K({1, K/2}) = ½ [1 + 2^{−(K−1)} binom(K−1, (K−1)/2) (K−1)/(K+1)].

The protocol takes odd K, J_k = cos(2πk/K)J_x + sin(2πk/K)J_y, and Q_K = (1/K) Σ_k pos(J_k), where 2 pos acts on an eigenvalue m as 1+sgn(m), including half weight at zero. Eqs. (7) and (10) express the separable bound as the maximum over unit product pure states. The two factors here have dimensions 3 and K+1. Preregistration: https://github.com/the-omega-institute/trureturing/issues/11873.

O. Makuta, B. Kuzaka and R. Augusiak, Fully non-positive-partial-transpose genuinely entangled subspaces, arXiv:2203.16902v2; Quantum 7, 915 (2023), Section 3, Conjecture 1 (final_5.tex, lines 458–463):

Given a stabilizer $\mathbb{S}=\langle G_{1},\dots,G_{k}\rangle$, if the local dimension $d$ is a prime number and the corresponding stabilizer subspace $V$ is genuinely entangled, then

$\dim K(\mathbb{S}) \geqslant \left\lceil \frac{N-1}{d-1} \right\rceil.$

The source defines $K(\mathbb{S})$ using the local commutation exponents (lines 375–391). In the Lean coordinates, write the prime local dimension as $p$. A Pauli word is a phase residue together with $x,z:\mathrm{Fin},N\to\mathbb F_p$, acting as $\omega^{\mathrm{phase}}\bigotimes_n X^{x(n)}Z^{z(n)}$, with $\omega=\exp(2\pi i/p)$. For words $a,b$, the commutation vector has coordinates $z_a(n)x_b(n)-x_a(n)z_b(n)$; commutationSpace G is the $\mathbb F_p$-span of all generator-pair vectors.

IsStabilizer G requires pairwise commuting generator matrices and excludes every scalar matrix other than the identity from their generated matrix submonoid. stabilizerSubspace G is the intersection of the generators' fixed subspaces. genuinelyEntangled G says that every nonzero vector in this intersection fails to factor across every bipartition with two nonempty sides. Factorization means an amplitude of the form $u(x|Q)v(x|{Q^c})$; normalization is not required.

Issue #20105 fixes the statement for every $N\ge1$, prime $p$, and finite generator family. claim uses natural-number division:

$(N-1+(p-2))/(p-1)\le\operatorname{finrank}_{\mathbb F_p}(\operatorname{commutationSpace}G)$.

For $N\ge1$ and prime $p$, the left side is $\lceil(N-1)/(p-1)\rceil$. The conjecture is proved.

A. Mayumi, G. Kimura, H. Ohno and D. Chruściński, “Böttcher-Wenzel inequality for weighted Frobenius norms and its application to quantum physics”, arXiv:2403.04199v2, Conjecture 1, equation (15), ask whether

$$|[A,B]|\omega\leq\sqrt{\frac{\lambda_m+\lambda_M}{\lambda_m}},|A|\omega|B|$$

holds for all $A,B\in M_n(\mathbb C)$ and every positive definite weight $\omega$. Here $[A,B]=AB-BA$, $|A|_\omega^2=\operatorname{tr}(A^*A\omega)$, $|B|^2=\operatorname{tr}(B^*B)$, and $\lambda_m,\lambda_M$ are the attained minimum and maximum eigenvalues of $\omega$. Issue #13715 preregisters this case as a tier-3 research line.

Feng Zhang and Hefang Jing, More inequalities for positive semidefinite matrices, Electronic Journal of Linear Algebra 41 (2025), 595–601, Question 2.14, p. 601:

Let A ∈ M_n. Then [[f(|A|), A*], [A, g(|A|)]] ≥ 0 if and only if A is normal under the conditions that f(x)g(x) = x² for x ≥ 0, f(x) ≥ g(x) (x ≥ 1) and g(x) ≥ f(x) (0 ≤ x ≤ 1).

The notation on p. 595 is “|A| = (AA)^{1/2} and A is the conjugate transpose of A”. The assertion quantifies over every admissible pair of real functions, every natural dimension, and every complex matrix in that dimension. Preregistration: #18699.

Statement echo

| Source clause | Lean counterpart | Fidelity | | --- | --- | --- | | $|A|=(A^*A)^{1/2}$ | CFC.sqrt of the conjugate-transpose product, inlined in block | Literal expression; the existing CFC.abs construction is not redeclared. | | Four displayed blocks, in their given order | block, using Matrix.fromBlocks and cfc | Every block is retained. | | $f(x)g(x)=x^2$ for $x\ge0$ | First quantified premise of claim | Same range and equality. | | $f(x)\ge g(x)$ for $x\ge1$ | Second quantified premise | Same inequality and range. | | $g(x)\ge f(x)$ for $0\le x\le1$ | Third quantified premise | Both endpoints included. | | Every $A\in M_n$, block nonnegative iff $A$ normal | Final quantifiers and equivalence in claim | Fin n labels the indices; positivity is Matrix.PosSemidef and normality is $A^A=AA^$. | | The universal assertion is false | result | Its conclusion is the literal negation of claim. |

No continuity, invertibility or spectral injectivity premise is added. The counterexample functions are continuous and satisfy the three required scalar conditions.

J. B. DeBrota, C. A. Fuchs and B. C. Stacey, “The Varieties of Minimal Tomographically Complete Measurements”, arXiv:1812.08762v5 (quant-ph), Conjecture 1 on printed page 6 states:

A rank-1 MIC in dimension 3 can have no more than 7 pairs of orthogonal elements.

A MIC is a POVM of exactly d² positive semidefinite effects summing to the identity whose real span is the Hermitian operators. Orthogonality is tr(E_a E_b) = 0; distinct unordered pairs are counted once. Issue #11474 preregisters the literal reading for d = 3 before Lean implementation. The conjecture imposes no unbiasedness condition, although its preceding seven-pair example is explicitly called unbiased.

K. Beyer, R. Uola, K. Luoma and W. T. Strunz, Joint measurability in nonequilibrium quantum thermodynamics, arXiv:2111.02854v2, Physical Review E 106, L022101 (2022), p. 4, state:

The ansatz for the effects W^U_ab in Eq. (6) is a priori not the most general one [54]. However, numerical simulations suggest that our visibility bounds are tight and we conjecture that our construction is optimal to satisfy condition (ii) for the given model Eq. (5)

The Supplemental Material repeats:

Therefore, we conjecture that the proposed form of the joint POVM is optimal for the given noise model if one wants to satisfy the fluctuation condition (ii).

For $d\ge2$ and $0<\lambda,\gamma<1$, set $A_a=\lambda\Pi_a+(1-\lambda)I/d$ and $B_b=\gamma\Pi'_b+(1-\gamma)I/d$, with $B_b^U=U^\dagger B_bU$. If every unitary admits a parent POVM satisfying the average and fluctuation conditions, then

$$\gamma\le\frac{2\kappa}{d+2\kappa-d\kappa},\qquad \kappa=2\sqrt{\lambda+(1-\lambda)/d}\sqrt{(1-\lambda)/d} +(d-2)(1-\lambda)/d.$$

The Library note records conditions (i)–(ii), Eq. (5), Eqs. (8)–(9), and both conjecture passages. Issue #16507 is the first-tier preregistration of the literal conventions and universal necessity statement.

Statement echo

| Source clause | Lean counterpart | Fidelity | | --- | --- | --- | | Eq. (5), initial white-noise effects | effA | Literal scalar-weighted matrix unit plus identity | | Eq. (5), final white-noise effects | effB | Literal scalar-weighted matrix unit plus identity | | Arbitrary relative energy bases | effBU and unitary quantifier in claim | Standard matrix units with arbitrary unitary rotation cover every relative basis | | Lüders instrument | luders | The positive square root is CFC.sqrt | | Condition (i), all energy assignments | AverageCondition | All real functions on both outcome sets | | Condition (ii), every diagonal state and outcome | FluctuationCondition | PSD, trace one, zero off-diagonals, and every outcome pair | | A parent POVM for every unitary | claim and frozen ConcealmentKernelNecessityRefutation.IsPOVM | Every effect is PSD and the effects sum to identity | | $d\ge2$ and strict visibility bounds | Binders and antecedents in claim | Every natural dimension and every pair of real visibilities in the source's range | | Eqs. (8)–(9) | kappa, visibilityBound, result | Necessity of the literal bound |

The finite index type represents $d$ outcomes and a $d$-dimensional Hilbert space. The universal unitary quantifier absorbs the choice of the final energy basis. PSD and trace-one hypotheses define a density matrix; the zero-entry hypothesis defines its diagonality. These are source conditions, not additional restrictions on admissible parents. The public effects are literal source expressions; the proof uses the frozen Tomiyama noise map phi through the private consumed correspondence source_effect_eq_phi.

A. Critch and J. Morton, Algebraic geometry of matrix product states, SIGMA 10 (2014), 095, state Conjecture 8 in the source TeX sigma14-095.tex, lines 430–434:

For $N\geq 4$, a~generic~$N$-qubit state can be recovered from its improper margina-li-zation to any three consecutive states. That is, each improper marginalization map $\overline\OB(2,2,N)\to\overline\OB(2,2,3)$ is a~birational equivalence of varieties.

The paper defines an open-boundary state by $\Psi_{i_1\dots i_N}=b_0^TA_{i_1}\cdots A_{i_N}b_1$ and defines $\overline\OB(2,2,N)$ as the Zariski closure of these states (source lines 349–363). Its improper marginalization sums amplitudes over all indices outside a chosen consecutive triple (lines 419–426). The Lean reading uses closure n for the affine zero locus of the vanishing ideal and improperMarginal n a h for this coherent amplitude sum, where $h:a+3\le n$.

Avgustinovich, Karhumäki and Puzynina, On abelian versions of critical factorization theorem, RAIRO–ITA 46(1), Open problem 6.2, ask:

Let k be an integer. Does there exist a non-periodic word w and integers l₁, l₂, such that w contains a central abelian 2k-power of length l₁ or l₂ at every position?

The answer is negative for every $k\geq1$, every finite alphabet and every pair of block lengths. The public theorem is D5.S1.Words.TwoCenteredAbelianPeriods.result.

Statement echo

| Source clause | Lean counterpart | Fidelity | | --- | --- | --- | | Biinfinite word over a finite alphabet | $w:\mathbb Z\to\mathrm{Fin}(r)$, every natural $r$ | Alphabet labels are immaterial. | | Position between $w_i$ and $w_{i+1}$ | Integer cut $i$ | The first block starts at $i-lk+1$. | | Central abelian $2k$-power with period length $l$ | CentralAbelianPower w k l i | All $2k$ consecutive length-$l$ blocks have the same letter counts; $l>0$. | | Two lengths, one available at every position | The disjunction inside the universal integer-position hypothesis of claim | Both lengths are fixed globally. | | No non-periodic example | result : claim concludes Periodic w | A positive natural ordinary period is produced. | | Positive exponent | $1\leq k$ | Nonempty centered powers; no assertion about $k=0$. | | Natural lengths may equal zero | Positivity is part of each central-power predicate | A zero length never satisfies that predicate, so only the other length remains. |

OEIS A001108, NAME (%N, verbatim):

a(n)-th triangular number is a square: a(n+1) = 6*a(n) - a(n-1) + 2, with a(0) = 0, a(1) = 1.

Jaroslav Krizek's COMMENT conjecture (%C, verbatim, with its preceding context sentence):

The squares of NSW numbers (A008843) interleaved with twice squares from A084703, where A008843(n) = A002315(n)^2 and A084703(n) = A001542(n)^2. Conjecture: Also numbers n such that sigma(n) = A000203(n) and sigma(n-th triangular number) = A074285(n) are both odd numbers. - Jaroslav Krizek, Aug 05 2016

The literal proved statement is forall n : Nat, 0 < n -> (IsSquare (n * (n + 1) / 2) iff (Odd (sigma 1 n) and Odd (sigma 1 (n * (n + 1) / 2)))). The recurrence for A001108, Pell-type completeness, the NSW/A084703 interleaving structure, and all other A001108 comments are NOT claimed. The guard excludes n=0: although T_0=0 is a square, Mathlib defines sigma(0)=0, which is even, so the unguarded parity equivalence is false.

B. Mukherjee, D. Banerjee, K. Sengupta and A. Sen, Minimal model for Hilbert space fragmentation with local constraints (Phys. Rev. B 104, 155117, 2021; arXiv:2106.14897v3), section “Construction of bubble eigenstates”, TeX fragmentation_prb_v2.tex, lines 729–731, immediately following Table I:

While we have not been able to find a closed form expression for the degeneracy of the different bubble eigenstates for an arbitrary $L$, we can still place a lower bound on the degeneracy of such states when $L \gg 1$.

The counting prescription is explicit in the same source, lines 670–674:

The number of bubble eigenstates at an integer energy $E=n_1-n_2$ can be calculated for a given system size from the number of configurations that satisfy the hard core constraint of at least two consecutive $\downarrow$ spins separating any of the $n_1$ $X$ and $n_2$ $Y$ units on the periodic one-dimensional lattice.

Here $X$ and $Y$ are three-site units with energies $+1$ and $-1$, respectively (the source's construction, lines 634–647). Issue #26367 fixes the combinatorial reading: sites are $\mathrm{Fin},L$, a centre set $B$ is admissible when every ordered pair of distinct centres has clockwise separation at least five, and a subset $x\subseteq B$ specifies the $X$ labels, with the other centres labelled $Y$. Its energy is $2|x|-|B|$. Translations are counted separately, and the empty placement contributes one configuration at energy zero. Let $D_B(L,E)$ denote this count, defined by bubbleCount.

For $1\le n\le\lfloor L/5\rfloor$, write

$$C(L,n)=\left(L\binom{L-4n-1}{n-1}\right)\mathbin{\mathrm{div}}n,$$

where $\mathrm{div}$ is natural-number division, and put

$$A(n,E)=\begin{cases}\displaystyle\binom{n}{(n+E)/2},&n+E\text{ is even and }|E|\le n,\0,&\text{otherwise}.\end{cases}$$

The module proves claim: for every natural $L\ge5$ and every integer $E$,

$$D_B(L,E)=[E=0]+\sum_{n=1}^{\lfloor L/5\rfloor}C(L,n)A(n,E).$$

Here $[E=0]$ is one when $E=0$ and zero otherwise; the equality is evaluated in the integers by casting the natural count and placement coefficients. The guarded index $(n+E)/2$ is a nonnegative integer. This settles the stated closed-form gap for labelled configurations; identifying these configurations with eigenstates of $H_3$ uses the source's construction and is not part of the Lean theorem.

Matijasevick, Rodriguez and Salazar, Perfect squares in reciprocal-sum sequences and primes that are inert in quadratic fields, arXiv:2610.00765v1, Section 7, question 2, asks:

For the recursions of this paper the exponent m=2 is forced. Is there a natural family of rational recursions for which c a_n+b_n is always a cube, other than those conjugate to z -> z^3?

The reduced-fraction convention is inherited from Problem 1.1: a_n,b_n are coprime positive integers, starts are positive integers, c is positive rational, and indices are n>=2. “Natural” is undefined. The explicit minimal reading here is a uniform autonomous rational family over Q of fixed degree, parameterized by a nonnegative integer, with one formula and a single c independent of the parameter, initial value and index. An unstated stricter author intent is not resolved by this reading.

For every t in N, including zero, put

$$F_t(x)=\frac{x+t}{(x+t+1)^3-(x+t)},\qquad x_n=F_t^{\circ n}(x_0).$$

The proved endpoint is: for every positive rational x_0, the intrinsic reduced numerator a_n and denominator b_n are positive and coprime for every n>=0; for every n>=1,

$$a_n+b_n=\bigl(a_{n-1}+(t+1)b_{n-1}\bigr)^3.$$

Thus c=1 works uniformly and the inherited integer starts and n>=2 follow. Each map has degree exactly 3 and no M in PGL_2(C) has M F_t M^{-1}(z)=z^3 on the entire projective line. No assertion at n=0 of a cube sum, or classification of all cube recursions, is made.

Sucharita Biswas, Umesh Shankar and Sivaramakrishnan Sivasubramanian, Matchings and shape-Wilf-Equivalence of sets of patterns of length three I: Triples, arXiv:2609.08562v1, Section 6, Question 1: "Can we enumerate the matchings that avoid the set of patterns P1 = {123, 132, 213} and P13 = {132, 213, 321}?" Matching patterns follow Section 4 and Figure 1: three arcs form an occurrence only when all three left endpoints precede all three right endpoints, and the label records the complement of the order of the right endpoints. This dossier settles the P1 clause and records an all-size structural scan bridge, finite continuation recurrence and exact all-size enumeration for the P13 clause. The P13 result concerns the original ordinary matching carrier, including empty and disconnected matchings.

Johann Cigler, Some sequences and number triangles which are related to Narayana polynomials and to q-Narayana polynomials for q=-1, arXiv:2608.03363v2, Section 4, Conjecture 2, equation (79) (Conjecture 1, equation (62), in v1): for m ≥ 1,

C^{(4m)}(t², z²) = c^{(4m)}(t, z) c^{(4m)}(−t, −z), C^{(4m+1)}(t², z²) = c^{(4m+1)}(t, z) c^{(4m+1)}(−t, −z).

Here C^{(h)}(t, z) = Σ_n C_n^{(h)}(t) zⁿ and c^{(h)}(t, z) = Σ_n c_n^{(h)}(t) zⁿ, where C_n^{(h)}(t) and c_n^{(h)}(t) are the weighted counts of Dyck paths of semilength n in the strip 0 ≤ y ≤ h, a down-step to height k having weight τ_k with τ = (1, t, 1, t, …) and τ = (1, t, −1, −t, …) respectively. The identity is the bounded analogue of the unrestricted identity c(t, z) c(−t, −z) = C(t², z²), equation (6) of the source.

P. Kagey's OEIS A350532 COMMENT states verbatim:

Conjecture: T(2*n,3) = (n^2 - n)/2 for n >= 1.

The settled statement is $T(2n,3)=(n^2-n)/2$ for every $n\in\mathbb N$ with $1\leq n$.

The source's NAME defines the count verbatim:

Triangle read by rows: T(n,k) is the number of degree-n polynomials over Z/2Z of the form f(x)^m for some m > 1 with exactly k nonzero terms; 1 <= k <= n + 1.

Statement echo

| Source clause | Lean counterpart | Fidelity | | --- | --- | --- | | Degree-n polynomials over Z/2Z, exactly k nonzero terms, some exponent m > 1 | KageyA350532Binomials.T | The literal cardinality subtype; distinct nonzero polynomials, with witnesses for base and exponent. | | Conjecture: T(2*n,3) = (n^2 - n)/2 for n >= 1. | KageyA350532Trinomials.claim and KageyA350532Trinomials.result | Literal universal assertion under the preregistered conventions. | | No restriction to positive degree in the definition | p ≠ 0 together with p.natDegree | The preregistered nonzero convention prevents zero from entering the degree-zero count. | | Natural-number variables | The natural-number binders and arithmetic | Subtraction and division in the trinomial assertion are natural-number operations. |

For every finite field F of cardinality q, every positive integer k, and nonincreasing nonnegative masks lambda, mu : Fin k -> Nat satisfying mu j <= lambda j, lambda j <= k - j, and mu j < k - j, count the pairs of actual (k+1) x k matrices (M1, M2) that respect the two zero regions and are nondegenerate. The source's nondegeneracy condition is the nonvanishing of Cayley's second hyperdeterminant; equivalently, every nonzero linear combination of the two faces has rank k over the algebraic closure.

The resolved formula is

q^(k*k) * (q-1)^(2*k)
  * product (q-bracket (k+1-j-lambda j))
  * product (q-bracket (k-j-mu j)),

where the products range over j : Fin k and [r]_q = sum_{e=0}^{r-1} q^e. The count is over the literal matrix-pair subtype, with no count, bijection, inverse, normalization, or rational-combination premise added.

Leila Muney, Holes in Valid-Extension Sets of Finite Gilbreath Sequences, arXiv:2606.23721v2, Section 16(4), asks:

Is max_{S∈G_n} #comp(K_S)=2^(n-4) for all n≥5? Verified for n≤10.

The integer triangle is s_a^0=s_a and s_a^b=|s_(a+1)^(b-1)-s_a^(b-1)| at every valid index. A prefix is Gilbreath when every positive-row left entry is one. The family G_n consists of every strictly increasing Gilbreath integer prefix of length n beginning with two and three. K_S contains every integer k for which appending k is Gilbreath; no increasing condition is imposed on this appended integer. Components are literal maximal runs of common difference two in the finite one-parity extension set.

Peter Kagey's OEIS A334595, revision 18, gives the sequence name "Binary interpretation of the right diagonal of the XOR-triangle with first row generated from the binary expansion of n." Its fourth %C comment states:

Conjecture: a(n) = 1 if and only if n is a power of two.

The entry's definition uses the unpadded binary expansion of n. The literal formal claim is forall n : Nat, 1 <= n -> (a n = 1 <-> exists k : Nat, n = 2 ^ k). The exponent is allowed to be zero, so n = 1 is included; n = 0 is outside the positive-index domain. The right edge is read from the upper-right corner to the apex with every position retained, including zero bits.

OEIS A392387 (Thore Posske, 2026) is the nullspace dimension of the periodic spin-1/2 XX Heisenberg chain on n > 1 sites. Its COMMENTS give the count

Also, the number of subsets K of {1,...,n} such that the sum of cosines of the angles in {(2j + (1 + (-1)^|K|)/2 )*Pi/n | j in K} is zero.

and its FORMULA section records

Conjecture: a(2*p) = 2*(6^((p-1)/2)+1) for odd prime p.

Issue #10063 fixes the readings: the formal object is this subset count, the combinatorial description common to the entry and to Hu, Gerken and Posske (arXiv:2602.15098, appendix on the XX model); its identification with the dimension of the zero-energy subspace is the source's Jordan–Wigner reading and is not formalized; the empty set is counted; p ranges over odd primes and n = 2p.

Alexander Bastien and Omid Khormali, On Link-irregular Digraphs, arXiv:2512.20494v1, Conjecture 6, assert that a link-irregular tournament exists on n vertices if and only if n >= 6. The precise resolution here is its nonvacuous reading:

∀ n : Nat, 2 ≤ n →
  ((∃ R : Fin n → Fin n → Prop, IsTournament R ∧ LinkIrregular R) ↔ 6 ≤ n)

IsTournament R requires irreflexivity and exactly one directed edge between each two distinct vertices. DirectedLink R v is Subrel R on the carrier {w // R v w ∨ R w v}, the union of the out- and in-neighbors. LinkIrregular R requires IsEmpty (DirectedLink R u ≃r DirectedLink R v) for every two distinct vertices u and v. Thus the isomorphisms excluded are arbitrary bijections preserving and reflecting the directed relation. In a tournament the neighbor union is exactly the complement of the vertex, so these links are the actual vertex-deleted directed tournaments.

The restriction 2 ≤ n is essential. At orders zero and one the pairwise condition is vacuous and a tournament exists, while 6 ≤ n is false. The result does not prove the literal unrestricted equivalence at those orders. It proves both directions for every order in the stated domain.

S. Akella, N. Iizuka and A. Miyata, Genuine Multi-Entropy in the Toric Code, arXiv:2607.06050v2, state for stabilizer states the reduction $\mathrm{GM}^{(4)}_{3}(A:B:C:D)=-\left(a-\tfrac19\right)I_3$ (Eq. (3)), where $I_3$ is the Rényi tripartite information and $a$ the convention parameter of the genuine multi-entropy, note that "this reduction is not a consequence of the Coxeter structure", and ask in §6 "Whether there is a similar counting argument for $n = 3$ case is an open question." The verbatim definitions are in the literature note.

Issue #13575 reads Eq. (3) as a theorem about every normalized pure qubit stabilizer state and every assignment of its qubits to four labelled parties (parties may be empty), for every real $a$, together with positivity of every replica partition function $Z_3^{(\mathtt q)}$ so that every logarithm is defined.

M. Bouras, OEIS A363347, COMMENTS, Conjecture 3:

Conjecture 3: Except for 5, the primes all appear exactly twice.

M. Bouras, OEIS A363102, COMMENTS, Conjecture 2:

Conjecture 2: All prime numbers appear either twice (same as A356247 and A357127) or three times.

For $n\ge3$, let $K(n,x)$ be the reciprocal of the right-folded fraction $2-3/(3-4/(\cdots- n/x))$. Define $a_4(n)=\operatorname{den}(K(n,-4))$ and $a_2(n)=\operatorname{den}(K(n,-2))$, using the positive reduced rational denominator. The first claim counts exactly two indices for every occurring prime $p\ne5$; the second counts exactly two or three for every occurring prime $p$. This dossier anchors A363347 Conjecture 3; the sibling settlement has its own dossier. Neither statement asserts that every prime occurs. This is the binding reading in preregistrations #18626 and #18627, both tier 1 external OEIS problems.

Statement echo

| Source clause | Formal counterpart | Fidelity | | --- | --- | --- | | Continued fraction, terminal value $-4$ | BourasA363347.a, using BourasA356360.K and nested | Literal reciprocal and right fold; Rat.den | | Continued fraction, terminal value $-2$ | BourasA363102.a, using the same K | Literal reciprocal and right fold; Rat.den | | Prime values | Nat.Prime and an existential occurrence guard | Includes precisely the primes taken by the sequence | | Except for $5$ | BourasA363347.claim has the guard $p\ne5$ | No exclusion is added to the second claim | | Indices start at three | Both occurrence sets include $3\le n$ | Matches the OEIS offsets | | Exactly twice | BourasA363347.claim uses Set.ncard = 2 | Its proof constructs a finite pair | | Twice or three times | BourasA363102.claim uses the disjunction of cardinalities two and three | Its proof constructs a pair or triple |

The natural polynomial BourasPolynomials.U is $U(n)=n^2-2$, with truncated natural subtraction. At $n\ge3$ it agrees with the integer polynomial. The source's rational fold expressions are represented by the existing frozen BourasA356360.nested and K declarations in this module. The public BourasA372763OnceRefutation.nested and K owners are textually equal; reusing them here would require changing or removing those frozen declarations, so both copies remain. No duplicate-retention authorization is claimed.

A. Enciso, F. Finkel, A. González-López and M. A. Rodríguez, arXiv:0704.3046v1, §3, printed p. 13, after Eqs. (31)–(32), state:

The first one is the requirement that ξ be the unique minimum of the potential U in the domain C. Although our numerical calculations suggest that this is indeed the case, we have not been able to provide a rigorous proof of this fact.

The chamber is $C={x\in\mathbb R^N:x_1<\cdots<x_N}$ from Eq. (10). With cyclic indices $x_0=x_N$ and $x_{N+1}=x_1$, Eq. (31) is

$$ U(x)=\sum_i x_i^2+\sum_i\frac{2}{(x_i-x_{i+1})^2} +\sum_i\frac{2}{(x_i-x_{i-1})(x_i-x_{i+1})}. $$

The sites obey Eq. (6), $\xi_i=1/(\xi_i-\xi_{i-1})+1/(\xi_i-\xi_{i+1})$. Issue #11857 fixes the settlement for every natural $N\geq3$, with existence of an increasing site configuration and equality only there.

M. Fannes, F. de Melo, W. Roga and K. Życzkowski, Matrices of fidelities for ensembles of quantum states and the Holevo quantity, arXiv:1104.2271v1, page 10, Conjecture 1:

For any ensemble E₃ = {(pᵢ, ϱᵢ)} with K = 3 three states of arbitrary dimension d the corresponding Holevo quantity χ(E₃) is bounded from above by the entropy of the matrix C√F(E₃) defined in (16): χ(E₃) ≤ S(C√F(E₃)).

Here $S(X)=-\operatorname{Re}\operatorname{tr}(X\log X)$, $\chi=S(\sum_i p_i\rho_i)-\sum_i p_iS(\rho_i)$, and $C_{ij}=\sqrt{p_ip_j}\operatorname{tr}|\sqrt{\rho_i}\sqrt{\rho_j}|$. The logarithm is natural. The matrices are positive semidefinite of trace one; weights are nonnegative and sum to one.

Statement echo

| Source clause | Lean counterpart | Scope | | --- | --- | --- | | Three states of arbitrary dimension | claim quantifies d : ℕ, three matrices indexed by Fin 3 on Fin d | No invertibility assumption; dimension zero has no trace-one state | | Density matrices | Each matrix is positive semidefinite and has trace one | Singular matrices included | | Ensemble probabilities | Each weight is nonnegative, and their sum is one | Zero weights included | | Fidelity and matrix (16) | The literal trace-norm/square-root expression in rootFidelityMatrix | The trace norm is the existing FiniteTraceDistance.traceNorm | | Holevo quantity and entropy | holevo; the literal trace-log expression in claim | Ordinary complex matrices, with the L2 operator norm for functional calculus | | Upper bound | FannesRootFidelityHolevo.result | The full expanded claim |

Gibilisco and Isola, On the monotonicity of scalar curvature in classical and quantum information geometry, arXiv:math-ph/0407007v2, Conjecture 4.2, printed page 11:

Suppose $n\geq2$. For the function $\mathrm{Scal}_p(\cdot):\mathcal D^1_n\to\mathbb R$ one has the following properties: if $p\in(1,2)$ then $\mathrm{Scal}_p$ is strictly Schur-decreasing; if $p\in(2,+\infty]$ then $\mathrm{Scal}_p$ is strictly Schur-increasing.

This settlement proves the quantum $p=3$ slice, equivalently $\alpha=1/3$, in every dimension $n\ge2$. The faithful density states are positive definite complex Hermitian matrices of trace one. The metric is the Euclidean pull-back of $A\mapsto3A^{1/3}$, with real trace inner product. Scalar curvature is defined by coordinate Christoffel symbols and Ricci contraction, rather than by the spectral formula proved below. The source's order calls $x$ more mixed than $y$ when the decreasingly sorted prefix sums of $x$ are at most those of $y$, with equal total sums.

Statement echo

| Source clause | Lean counterpart | Fidelity | | --- | --- | --- | | Every dimension $n\ge2$ | claim quantifies natural n with hypothesis 2 ≤ n. | Exact. | | Faithful complex density states | densityStates requires PosDef and trace one for both matrices; positive definiteness supplies Hermiticity. | Exact. | | Cube-root pull-back geometry | HermitianCubeDerivative.alphaEmbed3, HermitianDensityCoordinates.rho, and metric give the literal derivative pull-back. scal3 contracts coordinate curvature at chartPoint. | Exact; the fixed trace-one chart is proved equivalent to the Hermitian trace-one space. | | Eigenvalue majorization | eig selects the Hermitian eigenvalue vector; PositiveSimplexGeometryAndMixing.moreMixed is the existing decreasing-sort owner. | Exact and independent of permutation order. | | Schur increase | result concludes scal3 B ≤ scal3 A when eig A is more mixed than eig B. | Exact source convention. | | Strictness outside permutations | The second conjunct concludes scal3 B < scal3 A unless the eigenvalue vectors differ by a permutation. | Exact. | | Other values of $p$ and the decreasing clause | No corresponding conclusion in claim. | Open; outside this slice. |

C. Godsil, Average mixing of continuous quantum walks, arXiv:1103.2578v3, section 11, Question 1 (PDF page 20), asks:

Is it true that if $D$ is the discriminant of the minimal polynomial of $X$, then $D\widehat M_X$ is an integer matrix?

For a finite simple graph $X$ with adjacency matrix $A$, the minimal polynomial is taken over $\mathbb Q$. The source's Lemma 1.1 identifies $\widehat M_X=\sum_\theta E_\theta\circ E_\theta$, with one orthogonal spectral projector for each distinct eigenvalue. Lemma 3.1 establishes only the factor $D^2$. Issue #12339 preregisters the exact all-graphs assertion, with no connectedness or simple-spectrum restriction.

Conjecture 1 of Lichtenfelz, Modin and Preston, arXiv:2508.09833v1, section 2.2, asserts all four identities (2.10)–(2.13). The complete quotation and the two Wigner-symbol conventions are in the literature note lichtenfelz2026zeitlin. The domain is every integer N ≥ 2, with 1 ≤ j,l < N; only (2.10) assumes j ≠ l. The sums traverse i = 1,...,N−1, λ(i) = i(i+1), and H(j) is the j-th harmonic number. The preregistration is issue #11604.

I. Perito, R. D'Avino, M. Jung, P. Mironowicz, A. Acín and R. Augusiak, Bell inequalities tailored to optimal global randomness certification, arXiv:2606.21362v3, §III.2, define for $d$-outcome measurements in unitary notation ($A_x=\sum_a\omega^a\Pi_{a|x}$, $\omega=e^{2\pi i/d}$) $\mathcal I_d=\frac12\sum_{x<2}\sum_{y<d}\omega^{xy}A_x\otimes B_y+\text{h.c.}$ and state:

Conjecture 1. The Tsirelson bound of $\mathcal{I}_d$ is given by Eq. (tsir_bound) [$2/\sin(\pi/(2d))$] and is attained by taking $A_0=Z$, $A_1=X$; the state $\ket{\psi_d} = \frac{1}{\sqrt d} \sum_k \ket{kk}$; and $B_y$ defined by Eq. (optbob).

The verbatim statements are in the literature note. Issue #14106 reads it for every $d\ge2$, every pair of finite dimensions, every density matrix and every projective strategy ($A_x$, $B_y$ unitary with $A_x^d=B_y^d=I$), together with the validity and the value of the stated strategy.

D. G. Roldán, Graph Energy Maximisation for Integral Circulant Graphs of Order n = p^2q^3, arXiv:2604.09491v1, Section 1, Conjecture 1.3 (Universality):

For every pair of distinct odd primes (p, q), the set D* = {1, p^2, pq, q^2, p^2q^2, pq^3} is the unique maximiser of E(p^2q^3, D) over all nonempty D ⊆ div(p^2q^3) ∖ {p^2q^3}.

The graph has vertices $\mathbb Z_n$ and adjacency condition $\gcd(a-b,n)\in D$. Its energy is the sum of the absolute values of its adjacency eigenvalues, with multiplicity. Source quotations and locators are in the literature note. Preregistration: #19144.

Statement echo

| Source clause | Lean counterpart | Fidelity | | --- | --- | --- | | Vertices $\mathbb Z_n$, modular difference, gcd adjacency | adjacency n D, on Fin n | Literal preregistered expression; subtraction is modulo $n$. | | Energy sums $|\lambda_i|$ with multiplicity | energy n D, using the multiset roots of the real characteristic polynomial | The proof identifies all roots through Fourier diagonalization of the real symmetric adjacency. | | Distinct odd primes $p,q$ | claim quantifies $p,q$ with both primality, inequality and oddness hypotheses | No ordering of $p,q$ and no restriction $q\ge5$. | | $D^={1,p^2,pq,q^2,p^2q^2,pq^3}$ | Dstar p q | Literal six-term finite set. | | Allowed, nonempty proper-divisor sets | First conjunct of claim and the guards on its quantified D | The first conjunct proves admissibility of $D^$; $1\in D^*$ gives nonemptiness. | | Unique maximizer | Strict energy inequality for every different allowed nonempty D | Full proposition, proved by result : claim. |

No additional premise restricts the published conjecture. The spectral argument proves the comparison even when the competing divisor set is empty.

John B. DeBrota and Christopher A. Fuchs, Negativity Bounds for Weyl–Heisenberg Quasiprobability Representations, arXiv:1703.08272v2, Section 6, page 17, write:

Although dimension $5$ was the last in which we were able to explicitly calculate the sum negativity for the SIC Q-reps by exhaustive combinatorial searching, we suspect that we have found the correct sum negativity for ${Q_j^-}$ constructed with the Hoggar SIC in dimension $8$. Rather than calculating the eigenvalues of every partial sum matrix (since this is infeasible for $2^{64}$, $8\times8$ matrices), we used a numerical local maximization procedure and around $10^6$ random pure state seeds. The overall maximum value we found, $7/8$, occurred frequently in our data and is significantly larger than all of the smaller local maxima. Of course, we could still be falling short of the global maximum value if it occurs at very hard to access positions. The states whose quasiprobability representations achieve the sum negativity of $7/8$ consist of $28$ copies of value $-1/32$ and $36$ copies of value $5/96$.

The precise question, preregistered in issue #11512, is whether $7/8$ is the attained greatest value of sum negativity over all density matrices. With the three-qubit Pauli orbit of $v=(-1+2i,1,1,1,1,1,1,1)^T$, write $\Pi_j=u_ju_j^*/12$, $Q_j^-=3\Pi_j-I/4$ and $q_\rho(j)=\operatorname{Re}\operatorname{Tr}(\rho Q_j^-)/8$. Equations (8)–(11) define $N^1(\rho)=\sum_j(|q_\rho(j)|-q_\rho(j))/2$ and maximize it over positive-semidefinite complex $8\times8$ matrices of trace one.

Johan Kok, Paul Fisher, Bettina Wilkens, Mokhwetha Mabula and Vivian Mukungunugwa pose Proposition 4.4 in Section 4 of https://arxiv.org/abs/1404.1714v1. Its proof placeholder is “(Conjectured)”; the final list explicitly asks “[Open problem: Prove Proposition 4.4]”.

For every natural $k\geq7$ and every Fibonacci bracket index $i$ with $F_i<k\leq F_{i+1}$, the complete question is

$$ \bigl(d^+(v_{k-1})\ne d^+(v_k)\ \land\ d^+(v_k)\ne d^+(v_{k+1})\bigr) \quad\Longleftrightarrow\quad \bigl(\psi(v_{k-1})\ne\psi(v_k)\ \land\ \psi(v_k)\ne\psi(v_{k+1})\bigr). $$

The vertices have positive labels. An original directed arc goes from $v_h$ to $v_j$ exactly when $h<j$ and $j\leq2h-d^-(v_h)$. The degree is the infinite outdegree. Each $\psi(v_n)$ counts distinct shortest directed edge sequences from $v_1$ to $v_n$ in that endpoint's own induced finite truncation $J_n(1)$. Length counts edges. Both adjacent comparisons, the iff, the lower bound and all bracket indices are part of the claim.

Cui, Mehta, Mousavi and Nezhadi, A generalization of CHSH and the algebraic structure of optimal strategies, Quantum 4, 346 (2020), arXiv:1911.01593v5, Section 1.4 (Further work), item 2, ask:

In Section 5, we give efficient explicit presentations for G_n and its multiplication table. Can we go further and characterize these groups in terms of direct and semidirect products of small well-known groups? The first few cases are as follows

For every natural $n\ge2$, the answer is

$$G_n\cong\left(C_{2n}\times C_2^{,n-2}\right)\rtimes_{\alpha_n}C_n.$$

The group $G_n$ has the source's Section 5 presentation on $P_0,P_1,J$: the relators are $P_0^n,P_1^n,J^n,[J,P_0],[J,P_1]$ and $J^i(P_0^iP_1^{-i})^2$ for $1\le i\le\lfloor n/2\rfloor$.

Statement echo

| Source clause | Lean counterpart | Fidelity | | --- | --- | --- | | The Section 5 presentation | P0, P1, J, rels, G | The relators are words equal to the identity; the negative exponent uses the integer cast of the natural index. | | Every $n\ge2$ | claim quantifies over natural n with 2 ≤ n | No further assumption on $n$. | | Small cyclic factors | L is Multiplicative (ZMod (2*n)) times the functions from Fin (n-2) to Multiplicative (ZMod 2) | The independent involutions have zero-based indices. | | An explicit semidirect product | alpha and the MulEquiv in claim | The action is the binding action in the definition comment on #16204. | | A product characterization | result : claim | An actual multiplicative equivalence, rather than an order comparison. |

The binding comment fixes cyclicHom, s, t, liftL, ts, u, e, step, stepAut and alpha. Here t n i represents the source's $t_{i+1}$, and u n k uses one-based indices. In particular, $u_{n-1}=s^n\prod_{i=1}^{n-2}t_i$, while $u_k=1$ outside the indicated range. For $n=2$, $u_1=s^2$. The action below two is trivial; the claim has no conclusion for those values.

Karp, Normalized incomplete beta function: log-concavity in parameters and other properties, §3, Conjecture 2:

Conjecture 2 The coefficients ψ_k are negative for all a, α, β > 0 and x ∈ (0, 1) if 0 < b < 1 and positive if b > 1, so that a → x^{−a}(1 − x)^{−b} I_x(a, b) is strictly coefficient-wise Wright log-convex on (0, ∞) for α, β > 0, x ∈ (0, 1) and 0 < b < 1; and a → x^{−a}(1 − x)^{−b} I_x(a, b) is strictly coefficient-wise Wright log-concave on (0, ∞) for α, β > 0, x ∈ (0, 1) and b > 1.

Equations (1) and (6) give

$$c_j(t,b)=\frac{\Gamma(t+b+j)}{\Gamma(b)\Gamma(t+j+1)},\qquad \psi_n=\sum_{k=0}^n\bigl[c_k(a+\alpha,b)c_{n-k}(a+\beta,b) -c_k(a,b)c_{n-k}(a+\alpha+\beta,b)\bigr],$$

$$\psi_{a,b,\alpha,\beta}(x) =x^{2a+\alpha+\beta}(1-x)^{2b}\sum_{n\ge0}\psi_nx^n.$$

Formal reading

Unless otherwise indicated, Lean names have prefix D5.S3.Analytic.IncompleteBetaShape.

| Source object | Lean name | Correspondence | | --- | --- | --- | | $c_j(t,b)$ in (1) | D5.S3.Analytic.IncompleteBeta.coeff | The same Gamma quotient; no new coefficient definition. | | $\psi_n$ in (6) | Defs.psi | Exactly the displayed finite convolution difference, with natural index $n$. | | $S_n(p,q;b)$ | Mixture.convolution | $\sum_{k=0}^n c_k(p,b)c_{n-k}(q,b)$. | | Uniform shifted beta mixture | Mixture.mixtureDensity | The average of Beta$(p+k+1,q+n-k+1)$ densities for $0\le k\le n$. | | Sliding kernel | Kernel.F, Kernel.H | The uniform affine average and its beta average used below. | | Conjecture 2 | Defs.claim, Result.result | Both strict signs for all real $a,b,\alpha,\beta>0$ and all natural $n$. | | $x\in(0,1)$ | No additional coefficient hypothesis | The coefficients do not depend on $x$, so this quantifier is vacuous for them. |

Zhen Lin, Lianying Miao, Guanglong Yu and Han Sheng, On the Ky Fan k-norm of the LI-matrix of graphs, Electronic Journal of Linear Algebra 38 (2022), 680–696, Conjecture 5.11 (page 694), states:

Among all connected graphs with n and m edges n ≤ m ≤ 2n−3, the Gₘ,ₙ is the unique graph with maximal value of ‖LI(G)‖F₂ and ‖LI(G)‖F₃.

Here $n$ is the number of vertices, $m$ the number of unordered edges, $L(G)=D(G)-A(G)$, $LI(G)=L(G)-(2m/n)I_n$, and the Ky Fan $k$-norm is the sum of the $k$ largest singular values, with multiplicity. The assertion is read as a separate maximum and equality characterization for each of $k=2$ and $k=3$. The interpretation involving a unique simultaneous maximizer is outside the claim.

Statement echo

| Source clause | Lean counterpart | Fidelity | | --- | --- | --- | | Finite simple undirected graphs of order $n$ | SimpleGraph (Fin n) | Every finite labelled graph of that order is represented. | | Connected, with $m$ edges | G.Connected, Nat.card G.edgeSet = m | Mathlib connectivity and unordered edges. | | $n\le m\le2n-3$ | The two range hypotheses in claim | m + 3 ≤ 2 * n avoids truncated subtraction; together the hypotheses force $n\ge3$. | | $LI(G)=L(G)-(2m/n)I_n$ | LI | Literal source-specific shift of Mathlib's Laplacian. | | $G_{m,n}$ in Figure 2.1 | Gmn n m | Vertex $0$ is universal; vertex $1$ meets $2,\ldots,m-n+2$. Argument order is $n,m$. | | Separate assertions for $F_2$ and $F_3$ | claim quantifies over $k=2$ or $k=3$ | Both the upper bound and the equality iff isomorphism are retained. | | Refutation | result | The public theorem proves the negation of that whole claim using its $k=2$ equality clause. |

Section 2 prints $2n-m+3$ pendant edges. That count conflicts with the stated order, size and figure; the figure's construction has $2n-m-3$ pendant vertices. The definition uses the figure and order/size convention fixed in #21801. There is no additional mathematical hypothesis in the public result.