The best known lower bound for the minimum Kochen-Specker vector system in $\mathbb{R}^3$ -- 24 vectors -- rests on a computational proof whose combinatorial half emits DRAT proofs but whose geometric half does not: the non-embeddability of thousands of candidate graphs is established by Z3's nonlinear real arithmetic, which produces no checkable proof objects. We close this gap for the proof's blocking database. We introduce exact rational case-tree certificates of real non-embeddability, whose splits are polynomial factorizations and rational sum-of-squares decompositions and whose leaves are discharged by injectivity, ideal-membership, or Positivstellensatz-shaped positivity arguments, and we certify all 291 source lines (180 distinct graphs) of the published pipeline's order-10 to order-13 blocking lists. Certificates are replayed by two independent checkers that share no code with the generator: a pure-Python replay over exact fractions, and a total checker implemented and proved sound in Lean 4. The soundness theorem -- acceptance implies that no injective-on-rays, orthogonality-respecting assignment of nonzero real vectors realizes the graph -- is kernel-checked with axiom closure {propext, Classical.choice, Quot.sound}, and a gcd-free rational arithmetic layer makes the entire verdict computation kernel-reducible, so each per-graph non-embeddability result is a closed kernel theorem proved by decide. The formalization surfaced findings about the published pipeline, including a load-bearing injectivity side condition in its embeddability notion, hidden WLOG case obligations invisible to Z3-based workflows, and an unreproducible candidate count that we resolve against the published artifacts. All certificates, checkers, and proofs are available and replayable from a single build.
The Peterson hit problem seeks a minimal set of generators for the polynomial algebra $\mathcal P_k=\mathbb F_2[x_1,\ldots,x_k]$ as a module over the mod--2 Steenrod algebra. While completely resolved for $k \leq 4$, the unrestricted problem remains widely open for $k \geq 5$, where the combinatorial explosion of basis elements renders exact algorithmic computation intractable. To bypass full Gaussian elimination, we model the degree--$d$ hit space via a sparse matrix driven by the Cartan formula and Lucas's theorem, shifting the focus to the construction of certified matrix minors. We first prove that strict spike monomials exactly characterize the zero rows, establishing a hard structural limit on coordinate-level annihilators. To bound the matrix rank from above (cohit lower bound), we derive exact zero-column formulae, which are strictly refined by the exact homology of the $\operatorname{Sq}^1$-layer and systematic linear dependencies induced by Adem relations. To bound the rank from below (cohit upper bound), we extract explicit independent column families: singleton columns yield permutation minors, acyclic pivot systems optimize triangular minors across all row orders, and $q$-support columns are formalized through hypergraph incidence. Crucially, we identify a congruence family that decomposes precisely into simplicial boundary matrices over $\mathbb F_2$, yielding a sharp closed-form rank formula. The resulting two-sided bounds are universally computable for every $k \geq 1$ and $d \geq 0$. Significantly, these results establish the absolute limits of purely combinatorial approaches to the hit problem, cleanly separating universal discrete certificates from the degree-specific resolutions provided by representation theory and weight filtrations.
We establish the conjecture by de Klerk and Pasechnik (2002), claiming that the semidefinite bounds $\vartheta^{(r)}(G)(r\geq 0)$ for the stability number $\alpha(G)$ are exact at $r=\alpha(G)-1$, by exhibiting an explicit sum-of-squares certificate. This certificate allows us to recover a known characterization of the minimizers of the Motzkin-Straus formulation for $1/\alpha(G)$. Additionally, we give sum-of-squares copositivity certificates for the matrices satisfying the Hoffman--Pereira sign condition, a crucial condition for characterizing copositive matrices with $\{-1,0,1\}$ entries.
Fraenkel's conjecture asserts that a partition of the integers into at least three Beatty sequences with distinct moduli has the binary densities $1,2,4,\ldots,2^{m-1}$, normalized by $2^m-1$. We prove the conjecture through a dimension-free intermediate statement: every such partition contains a component of density at least 1/3. After reducing the partition to primitive common-period data, Fourier cancellation produces a finite inverse-sine system. We prove that no such system can exist when every density is below 1/3. The proof combines a divisor-concentration identity with uniform analytic estimates and three exact finite verifications, all carried out with integer or rational arithmetic. The component supplied by the density bound has mean spacing at most three. Deleting it preserves balance, and every surviving periodic balanced set is again a rational Beatty set. Induction determines the surviving binary scales, while a two-sequence disjointness criterion forces the deleted density to be the next binary scale. This yields the asserted density pattern.
By using constant term manipulations, we present the first polynomial-time algorithm for lattice-point counting in fixed dimension that does not rely on Barvinok's unimodular decomposition. The algorithm instead operates directly on a rational generating function in the form of a nested root average, as produced by the \texttt{SimpCone[S]} framework. By means of a residue-lattice argument based on Minkowski's theorem, we construct a short multiplier that induces an exact non-coprime split of the outermost average. The resulting child terms are encoded as joint root averages, and Smith normal form is used to restore the recursive structure. Two structural invariants---the generation condition and full-column independence---ensure that the recursion is well defined and that all required pole exchanges are valid. For a fixed-dimensional simplicial cone, the algorithm achieves recursion depth \(O_d(1+\log\log(2+\ind(\mathcal K^*)))\) and produces a signed sum of at most \((1+\log \ind(\mathcal K^*))^{O_d(1)}\) unimodular cone generating functions. The framework uniformly handles numerators that are Laurent polynomials, not merely monomials, thereby giving a polynomial-time algorithm for MacMahon's partition analysis when the dimension is fixed.
We study a dimension-saturating fixed-core ansatz in which four copies of a fixed, non-tunable two-qutrit core $K\in SU(9)$ are interleaved with five adjustable local layers from $L=SU(3)\otimes SU(3)$. Since $\dim SU(9)=80$ and $5\dim L=80$, this is the shortest fixed-core architecture not excluded by parameter counting. We formulate the smooth map $\Phi_K:L^5\to SU(9)$ and use its right-trivialized differential to give verifiable certificates for local universality. We construct an explicit Clifford-word core whose Pauli-label splitting makes the identity-point differential an exact isometry, and we classify all 2304 symplectic actions satisfying the same splitting criterion. We also prove a structural obstruction for an important symmetry class: every complex-symmetric core $K=K^{T}$, including every core generated by a time-independent real-symmetric Hamiltonian in the chosen computational basis, has identity-point differential rank at most 78; hence any full-rank certificate for such a core must occur away from that point. We then assess a hardware-motivated superconducting core generated by a noncommuting, temporally asymmetric drive. Direct calculation verifies $K_{\rm sc}\neq K_{\rm sc}^{\mathsf T}$, and the core achieves $F_{\rm avg}\ge 0.999$ for all 1000 Haar-random targets tested under the stated restart protocol. We also report favorable sampled Jacobian-rank, structured-target, and robustness diagnostics. These results establish local universality at the parameter-counting-minimal, dimension-saturating depth, with an exact Clifford certificate complemented by a hardware-motivated numerical case study. Throughout, we separate exact local certificates from numerical evidence for broader synthesis performance.
Yurui Liu, Ruoting Dou, Peng Xu et al.· 0 citations
In a recent preprint, Simon proposed a polynomial-time quantum algorithm for the Dihedral Coset Problem and rested the analysis on four lemmas. Three of them carry only proof sketches, and this paper gives each of those three a statement that admits a single reading together with a complete proof. Lemma 1 follows from an exact second-moment computation for the subset-sum counts, and it holds with probability tending to one in place of the constant originally claimed. The amplitude bound of Lemma 3 follows from an exact Parseval identity on the cube of measurement outcomes and holds at every threshold with no well-behavedness hypothesis, so that predicate leaves the argument entirely. For Lemma 4, we compute both balls-in-bins covariances exactly and find that the second carries a term a fixed ball count leaves out. The assumption that the distinguished group contains no faulty samples can also be dropped. The two branch amplitudes share a signed prefactor, so the counting estimates control their difference and not the ratio the lemma states. We prove the additive form and show that the closing argument consumes nothing more than that. A single hypothesis survives all of this. It asks that the partition into the two sides be fixed independently of the measured string, and the rule the algorithm gives for choosing that partition does not supply it. Establishing these four lemmas therefore does not by itself establish the correctness of the algorithm.
Yuchen Guo, Shuo Yang· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.
