We prove an improved lower bound of 0.097387436922 on the largest normalised Ingleton violation among four-variable almost-entropic vectors. Previously reported constructions reach approximately 0.0925, used as a rounded benchmark; the best published universal upper bound is 19/124. Conditional parity hashing combines local binary parity labels, one common linear hash, simultaneous conditional privacy amplification and joint conditioning. Applied to a 24-atom source of Matúš and Csirmaz, it subtracts a multiple of the uniform-matroid rank function U(3,4) from all fifteen entropy coordinates. The limiting signed score lies in [-0.097387436923, -0.097387436922], and finite-alphabet distributions with score below -0.09738 exist. This record contains the preprint PDF, manuscript sources, Lean proof sources, exact numerical checkers, build instructions and verification evidence. The main theorem, including the closed rate interval, score enclosure and finite-alphabet existence statement, was rebuilt and kernel-checked in Lean 4.35.0-rc2 with pinned Mathlib dependencies. The finite sampler and fixed-path optimality argument are written proofs rather than separate Lean declarations. Søren Riis is the creator and coordinator and directed the research. Astra/Codex and Claude contributed mathematical development, computation and verification; Claude contributed the Lean formalisation and adversarial review. The source construction is due to Matúš and Csirmaz; the paper gives full references to the earlier entropy-region and privacy-amplification work. AI checks do not constitute independent human peer review. Licences by component: the paper PDF, LaTeX sources and original figures are CC BY 4.0; Lean sources, Python checkers and build scripts are Apache-2.0. Third-party dependencies retain their own licences. Repository: https://github.com/SR123/conditional-parity-hashing
We prove an improved lower bound of 0.097387436922 on the largest normalised Ingleton violation among four-variable almost-entropic vectors. Previously reported constructions reach approximately 0.0925, used as a rounded benchmark; the best published universal upper bound is 19/124. Conditional parity hashing combines local binary parity labels, one common linear hash, simultaneous conditional privacy amplification and joint conditioning. Applied to a 24-atom source of Matúš and Csirmaz, it subtracts a multiple of the uniform-matroid rank function U(3,4) from all fifteen entropy coordinates. The limiting signed score lies in [-0.097387436923, -0.097387436922], and finite-alphabet distributions with score below -0.09738 exist. This record contains the preprint PDF, manuscript sources, Lean proof sources, exact numerical checkers, build instructions and verification evidence. The main theorem, including the closed rate interval, score enclosure and finite-alphabet existence statement, was rebuilt and kernel-checked in Lean 4.35.0-rc2 with pinned Mathlib dependencies. The finite sampler and fixed-path optimality argument are written proofs rather than separate Lean declarations. Søren Riis is the creator and coordinator and directed the research. Astra/Codex and Claude contributed mathematical development, computation and verification; Claude contributed the Lean formalisation and adversarial review. The source construction is due to Matúš and Csirmaz; the paper gives full references to the earlier entropy-region and privacy-amplification work. AI checks do not constitute independent human peer review. Licences by component: the paper PDF, LaTeX sources and original figures are CC BY 4.0; Lean sources, Python checkers and build scripts are Apache-2.0. Third-party dependencies retain their own licences. Repository: https://github.com/SR123/conditional-parity-hashing
For four finite discrete random variables, we prove that the negative of the Ingleton expression, divided by the joint entropy, is at most 19/124≈0.15323, improving the previously reported upper bound 3/19 by 11/2356. The proof uses a copy program with four copy steps and six auxiliary variables, certified by exact rational linear-programming certificates. We also show that two published information inequalities, due to Dougherty-Freiling-Zeger and Csirmaz, imply the bound 5/32 by an explicit nonnegative combination with Shannon inequalities, and that 5/32 is the exact optimum both of the union of the three published inequality catalogues considered here and of the full copy-lemma extensions of all 213 distinct copy programs occurring in them. The new program is not among these programs, and the bound 19/124 remains optimal when all of them and all catalogue inequalities are added. Ancillary files provide the parsed catalogues, exact primal and dual certificates, exact extension certificates, and verifiers that use only the Python standard library.
Abstract A nonzero real vector can be mapped to a unit vector by taking signed square roots of its normalized absolute coordinates. The associated rank-one projector retains relative magnitudes and signs while forgetting total mass and common sign. We apply this construction to an optimal residual and an optimal dual witness for a finite-dimensional minimum-distance problem in the sum norm. Their trace distance defines an alignment statistic. Complementary slackness gives a strict upper bound below one for every optimal pair, and characterizes the zero-distance case. Successive coordinate minimization selects a unique pair once a coordinate order is fixed. The construction is undefined at a zero residual; a separate convention assigns the statistic the value zero there. We give proofs, an explicit example, and a selection policy that uses the statistic only after primary residual comparisons. The accompanying numerical implementation and discrete Lean results have distinct, stated scopes. Why This Matters The paper distinguishes what its diagnostic inequalities measure from stronger claims that do not follow. Explicit definitions and counterexamples make the selection policy and its limits inspectable. Core Theorems The numbered propositions and proofs in the manuscript state their domains and hypotheses. The revision separates quotient residuals, input norms, discrete formal lemmas and numerical evaluations rather than treating them as equivalent. Formal Verification and Computational Artifacts The package includes source code, tests, a pinned standalone Lean project, an explicit declaration census and source-bound rendered files. The quick start gives commands for replay. Each formal result retains the scope described in the manuscript; test outcomes do not supply a theorem beyond that scope. Scope Boundaries and Non-Claims The real projector construction and strict primal-dual distance bound have prose proofs. Lean checks discrete integer and rational statements. Numerical vector evaluation does not establish optimality or compute the canonical selector. Reproduction See [quick_start.md](quick_start.md) for installation, tests, the Lean census, rendering and independent archive checks. The manuscript and documentation use CC-BY-4.0; reference software and tests use MIT. The renderer, Lua filter and path helperretain Apache-2.0; see the component table in README.md. Related Identifiers and Citations Verified scholarly sources are listed in [references.md](references.md).The new revision has no assigned DOI. The previous record is [10.5281/zenodo.20192297](https://doi.org/10.5281/zenodo.20192297); its verified parent is [10.5281/zenodo.20192296](https://doi.org/10.5281/zenodo.20192296). The metadata records these version relationships.
The Ingleton inequality is a classical linear information inequality that holds for representable matroids but fails to be universally valid for entropic vectors. Understanding the extent to which this inequality can be violated has been a longstanding problem in information theory. In this paper, we show that for a broad class of jointly distributed random variables (X,Y) the Ingleton inequality holds up to a small additive error, even even though the mutual information between X and Y is far from being extractable. Contrary to common intuition, strongly non-extractable mutual information does not lead to large violations of the Ingleton inequality in this setting. More precisely, we consider pairs (X,Y) that are uniformly distributed on their joint support and whose associated biregular bipartite graph is an expander. For all auxiliary random variables A and B jointly distributed with (X,Y), we establish a lower bound on the Ingleton quantity I(X:Y|A)+I(X:Y|B)+I(A:B) - I(X:Y) in terms of the spectral parameters of the underlying graph. Our proof combines the expander mixing lemma with a partitioning technique for finite sets.
This paper characterizes the fixed finite positive semidefinite composition partners whose tensor powers test strong positivity of every finite Hermitian matrix: a partner is universal exactly when it has a nonreal entry in the specified history basis. Constructive proofs give explicit copy bounds, finite-depth spectral and tolerance certificates, a finite-family obstruction, and a quantum-history realization. For a noisy two-history family, all-event lower bounds and explicit exposing events establish sharp weak-imaginary resource scaling. Further results include an exact pure-phase onset and conditional finite-composition CHSH certificates. The accompanying ZIP contains the LaTeX source, six exact standard-library Python checkers and their results, a package verifier and file hashes. Priority remains unestablished. No derivation of a physical probability law is claimed.Robert Barritz directed the research and its preparation for publication. OpenAI’s ChatGPT and Codex systems contributed substantially to mathematical formulation, proof development and examination, examples, exact computational verification, literature comparison, and manuscript preparation. Anthropic’s Claude contributed mathematical, computational, and literature review that informed revisions. The AI contribution extended substantially beyond language editing. AI-assisted review does not constitute human expert or journal peer review.
The Ingleton inequality is a classical linear information inequality that holds for representable matroids but fails to be universally valid for entropic vectors. Understanding the extent to which this inequality can be violated has been a longstanding problem in information theory. In this paper, we show that for a broad class of jointly distributed random variables (X,Y) the Ingleton inequality holds up to a small additive error, even even though the mutual information between X and Y is far from being extractable. Contrary to common intuition, strongly non-extractable mutual information does not lead to large violations of the Ingleton inequality in this setting. More precisely, we consider pairs (X,Y) that are uniformly distributed on their joint support and whose associated biregular bipartite graph is an expander. For all auxiliary random variables A and B jointly distributed with (X,Y), we establish a lower bound on the Ingleton quantity I(X;Y∣A)+I(X;Y∣B)+I(A;B)−I(X;Y) in terms of the spectral parameters of the underlying graph. Our proof combines the expander mixing lemma with a partitioning technique for finite sets.
A source-inclusive coherence observable is useful only when its measurement resources are admitted. This preprint constructs a bounded local reader for the conserved exchange observable of a specified finite quantum-record apparatus. A degree-three graph uses one independently prepared probe, twenty relays with arbitrary joint states, and finite-duration two-register extraction and full-SWAP interactions. The original apparatus Hamiltonian and an independently added archive-gated process remain active throughout their respective implementations. A prefix-dependent control-frame comparison, symmetry-resolved effect estimate, and explicit gain, phase and finite-slew waveform bounds yield a sufficient response separation greater than 0.005139889 for the stated fixed, fully accessible sixteen-position source and remaining response-error budgets. This is a conditional mathematical result, not measured hardware calibration, a partial-source-access theorem, or a unique diagnosis or derivation of fundamental collapse. The package contains the main manuscript, technical supplement, editable LaTeX, direct numerical reproduction sources, and accepted returned Mac evidence for 56 paper-specific supporting Lean declarations. That subset verifies selected algebra, scalar inequalities and the actual-constant numerical expression; it does not formalize the full physical/continuous-time theorem end-to-end. Separate-session AI review, numerical reproduction and returned kernel evidence are distinguished. Author-owned manuscripts, documentation and mathematical data are CC BY 4.0; newly authored numerical and Lean software is MIT. Predecessor and third-party notices remain unchanged; the reproduction package contains the licence map. No external funding; no competing interests declared. Public preprint v1.0; edition date 18 October 2026; DOI 10.5281/zenodo.23442579.