Hydrology finite-spectrum rate identifiability — Lean v1

This immutable release records the exact finite-spectrum rate-set identifiability theorem for positive parallel reservoir models.

New theorem:

• HydrologyIdentifiability.finite_spectrum_rate_set_identifiable.

If two nondegenerate k-mode moment sequences have nonzero weights, injective (pairwise-distinct) rates, identical moments 0,...,2*k-1, and order-k recurrences, then their finite decay-rate sets are equal. The proof first identifies the recurrence coefficients through the nonsingular Hankel matrix, then constructs the monic characteristic polynomial, proves every rate is a root by Vandermonde extraction, and uses exact root counting to identify the two rate sets. The only remaining ambiguity is permutation of reservoir labels.

Verification:

• Lean 4.34.1 / pinned Mathlib.
• lake build Hydrology completed 1,807 jobs.
• The theorem's #print axioms audit contains only propext, Classical.choice, and Quot.sound.
• No sorry, admit, custom axiom, native_decide, or numerical approximation is used.

Scope: this is an exact finite positive parallel-reservoir theorem. It is not a general identifiability theorem for nonlinear, spatially distributed, signed-mode, or continuum hydrology models.

High-dimensional APPT endpoints — Lean verification v1

This immutable release records two additional kernel-checked endpoints for the high-dimensional APPT purity program.

Verified theorems:

• APPTReview.appt_fixed_local_excess_sup_tendsto: for every fixed integer m >= 2, the physical APPT purity supremum satisfies
  Tendsto (fun n => (m*n) * (P_sup(m,n) - 1/(m*n))) atTop (nhds (1/(m^2-1))).
• APPTReview.plateauScaledPurity_le_continuous: every two-level projection plateau lies below the continuous two-level value, with an exact square-deficit identity.
• APPTReview.plateauScaledPurity_even_rank_max: when (m-1)*n is even, rank ((m-1)*n)/2 attains that value and is maximal within the plateau family.

Verification:

• Lean 4.34.1 and the pinned Mathlib revision.
• lake build APPTReview completed 2,850 jobs.
• Direct compilation of APPTReview/PlateauOptimizer.lean passed.
• Kernel axiom checks for all three theorem roots use only propext, Classical.choice, and Quot.sound.

Scope: these endpoints strengthen the fixed-local and two-level plateau portions of the program. They do not claim the full higher-dimensional APPT purity maximum, matching growing-local-dimension lower bounds, all-maximizer classification, entropy extrema, or rigidity.

Erdős similarity with growing logarithmic gaps — complete Lean replay v1

This immutable release records the completed Lean replay for the stated growing-logarithmic-gap avoidance theorem.

The package proves the unconditional late-window bridge from WindowFilling to FiniteSequenceBlockerSpec, the resulting CompactRobustSpec, and the full countable-family Theorem 2 entry points for WindowFilling sequences and for the consecutive-log-gap little-o specialization. The companion preprint states the scope and limitations: this is not a claim of the full Erdős similarity conjecture.

Verification performed before release:

• Lean 4.34.1 / pinned Mathlib build completed.
• lake env lean -t 0 ErdosSimilarityGrowingGaps/Replay.lean passed.
• Replay roots use only propext, Classical.choice, and Quot.sound.
• checks/negative.py rejected the intentionally invalid controls.
• The 10-page PDF and source archive compile cleanly; the final pages were visually inspected.

The immutable tag is bound to commit 0f4c202daeddd9a031cdef6c11659e154a7eb459. The source package and preprint files are available from that tag in the repository:

• formalizations/erdos-similarity-growing-gaps/
• preprints/erdos-similarity-growing-gaps-2026-10/

Recorded SHA-256 values:

• Lean source archive: 99cdca59f788f51cc957ea00e1b2ebfd35a0fb106f75bf9c61d5a46fd3e0b822
• PDF: 812a41fa9cbd0b2615b08a9df23859cdf7d2555ae5daf006359e2e48dcb77e65
• TeX source: 1fa57626e2e83ea143c3a78e72915a3627986542da3bb875a89c22e07751c9bc

High-dimensional APPT entropy-head bridge — Lean verification v1

Scope

This immutable release records the completed Lean verification of the finite physical-to-entropy-head bridge for high-dimensional APPT states. It uses actual complex density matrices, the original all-global-unitary APPT condition, and canonically sorted eigenvalues.

The verified endpoint density_appt_paper_entropyHead proves the paper-pivot nonlinear entropy-head inequality from the physical hypotheses m >= 2, m <= n, density, and APPT. The release also contains the admissible-pivot theorem, sorted rank-two witness and determinant consequences, largest-eigenvalue bound, singular-spectrum consequence, and the PPT-but-not-APPT regression.

Verification

• Proof source commit: a3201c675616a8caf330786933171e424659a7eb
• Documentation and release-binding commit: 2bf35ac
• GitHub Actions: https://github.com/mxym/math/actions/runs/38127581602
• 2,745 build tasks passed
• 40,088 transitive declarations and 22 roots replayed at trust level zero
• Only propext, Classical.choice, and Quot.sound occurred
• The exact final theorem was replaced by True.intro in a negative control and rejected by the kernel

This release does not certify the full high-dimensional purity or Rényi-entropy extrema, graph-limit arguments, or rigidity theorems. Those remain separately marked as analytic or partially formalized. It is a verification release, not a new preprint or a claim of external peer review.

State-independent entanglement extraction: exact exponents and Gaussian threshold — analytic preprint v1

Nine-page analytic preprint by Yongxian Zhang: State-independent entanglement extraction: exact exponents, reliability and a Gaussian threshold.

Precise task and universal quantifiers

For every fixed pair 2 <= m <= n, construct one family of global unitaries on the original k-copy system followed by deterministic local product channels. The family is indexed only by m,n,k and requested target dimension K; it is independent of the input spectrum, eigenbasis, rank and entropy, and works simultaneously for every fixed density matrix. There is no preliminary tomography, measurement, additional pre-unitary ancilla, state-dependent random choice, or postselection. The initial global entangling operation is an explicit resource.

The family attains the same all-rate target-fidelity exponent as the state-aware completely-PPT optimum. For A=log m, L=log(mn), c_R=L-2 min(R,A):

E_p(R) = (R-A)_+ + max_{1<=alpha<=2} [(alpha-1)/alpha] (S_alpha(p)-c_R).

The faithful capacity is C=min{A,(L-H(p))/2}. Eventual-exact extraction has capacity C0=min{A,(L-log rank(rho))/2}. The fidelity convention is overlap with the normalized maximally entangled projector, not its square root.

New strict-direct and Gaussian laws

For C0 < R < C, set c=L-2R. The exact error-decay exponent is

lim -(1/k) log(1-F_k) = min_{H(q)>=c} D(q||p),

both for the universal local construction and for the state-aware completely-PPT optimum. Relative entropy is on the positive support. This strict range is essential; exact zero-error transition behavior is not obtained by continuity.

If 0 < C < log m and V(p)=Var_p(-log p)>0, then

log K_k = k C + z sqrt(k) + o(sqrt(k))
  implies F_k -> Phi(-2z/sqrt(V(p))).

This gives the same nondegenerate Gaussian threshold without any state knowledge. The protocol does not need C or V: it takes the requested integer K as its parameter.

Mathematical mechanism and attribution

A single simultaneous Schur-Weyl packing retains the entire unknown representation factor and a known fraction of its identity multiplicity factor in every block. It does not select a block after seeing the input. Large blocks retain enough mass for the optimal fidelity exponent, while small blocks are extracted exactly and preserve the reliability exponent. A universal dominating state reduces the Gaussian statement to ordinary iid self-information, without assuming a new Schur-measure central limit theorem.

Standard Schur-Weyl duality, Weyl/hook dimensions and highest-weight character bounds are explicit external mathematical inputs. Universal compression, pure-state concentration, universal ordinary mixed-state LOCC distillation, source-coding asymptotics, and state-agnostic work extraction are credited. Rains's fidelity-effect constraints and Lami's entropy converse are not claimed as new discoveries. The ordinary CLT is used for the Gaussian conclusion.

Verification and source binding

This is a written analytic argument, not Lean certification or external peer review. Independent ancillary CI run 38034511091 passed at 45c677c89cef268033b6d6c68c3e44eeb20a0b1e. It checks exact combinatorial and rational identities, noncommuting inputs, coherent code dyads, multiplicity truncation and packing. Two unchanged checker runs pass, including assertions disabled; nine modified programs are rejected for specified mathematical diagnostics. Finite regression counts do not certify the full unbounded argument.

Publication commit: f465a11c55101fd38a10046daed65feeef007eeb.
Repository directory: research/universal-schur-extraction.
CI: https://github.com/mxym/math/actions/runs/38034511091

From the extracted source archive:

python3 verify_sources.py
python3 check.py
python3 -O test_checker.py

The checks use only Python's standard library. Compile main.tex twice with pdfLaTeX, or rebuild from PROOF.md using build_manuscript.py with Pandoc and pdfLaTeX. The archive contains the full proof, manuscript, programs, source hashes and literal CI records. PREPRINT_BINDING.json and SHA256SUMS bind the assets to the tested and published sources.

Limits

This does not solve ordinary fixed-input LOCC distillation or its universal reliability questions: free global entangling preprocessing changes the task. No claim is made for uniform finite-block convergence over varying states, exact zero-error-boundary reliability, cap-limited/zero-varentropy Gaussian laws, efficient circuits, APPT=AS, or the finite-copy higher-dimensional APPT purity conjecture. No arXiv submission, new DOI, external peer review or exhaustive priority certification is asserted. The earlier immutable qutrit, negativity and extraction releases are unchanged. Funding and AI-assistance disclosures appear in the manuscript.

Global-unitary extraction: exact capacity and common LO/LOCC/PPT exponents — analytic preprint v1

Nine-page analytic preprint by Yongxian Zhang: Global-unitary entanglement extraction: capacity and exact strong-converse exponents.

Exact result and operation class

For every density matrix on C^m tensor C^n, with 2 <= m <= n and arbitrary spectrum p (zeros allowed), first permit a global unitary on the original k-copy system and then deterministic local product channels (LO), LOCC, or completely PPT channels. No additional ancilla is available before the global unitary. Target fidelity is the overlap with the normalized maximally entangled projector, not its square root.

All three operation classes have the same capacity:

C = min{log m, (log(mn)-H(p))/2}.

They also have the same exact fidelity exponent at every target rate R >= 0. Writing A=log m, L=log(mn), c_R=L-2 min(R,A):

E(R) = (R-A)_+ + max_{1<=alpha<=2} [(alpha-1)/alpha] (S_alpha(p)-c_R).

The value at alpha=1 is zero. Below capacity, LO already attains fidelity tending to one. Above it, even completely PPT fidelity tends to zero exponentially, and the exact exponent is attained by LO. The initial global unitary is an explicit resource: this is not a solution of ordinary fixed-input LOCC or PPT distillation.

Proof mechanism and attribution

A deterministic variable-dimension Bell packing gives a one-shot spectral-prefix lower bound with factor 4. The Rains fidelity-effect constraints give an upper bound within a harmonic-number factor. Spectral types and escort distributions determine the exact common exponent. The achieving postprocessing is a local product channel, with all failure/leftover coordinates included; there is no postselection. The final proof does not require random projectors or matrix concentration.

Rains's SDP and Lami's recent quadratic entropy converse are explicitly credited. The half-entropy-deficit upper bound is not claimed as a new discovery. The contribution is its matching spectrum-optimized local achievability and the exact common all-rate fidelity law. No exhaustive historical-priority certification is asserted.

Verification and reproducibility

This is a written analytic proof, not a Lean certification or external peer review. Independent exact ancillary CI run 38030907207 passed: rational Choi/PPT-Choi identities, local Kraus completeness and exact embedded Bell outputs, integer packing inequalities, type estimates, escort algebra, and seven deliberately corrupted checker programs. The positive checker also passed with Python assertions disabled. Finite checks support calculations but do not by themselves prove the unbounded theorem.

Publication commit: 8a5eaa8be917132e1d64e079a9ef5d1934a700c7.
Ancillary-tested source: abf483af25b252f8ddaee91c8612c9e678cd8ac4.
CI: https://github.com/mxym/math/actions/runs/38030907207
Directory: research/global-unitary-ppt-extraction.

From the extracted source root:

python3 verify_sources.py
python3 check.py
python3 -O test_checker.py

Only Python's standard library is needed for the checks. Compile main.tex twice with pdfLaTeX, or run build_manuscript.py with Pandoc and pdfLaTeX. The source archive contains the complete proof, source-bound manuscript, programs, exact reports, and literal CI records. PREPRINT_BINDING.json and SHA256SUMS bind the publication assets to the tested and published sources.

Limits and preserved publications

No arXiv submission, new DOI, peer review, efficient polynomial-in-copy circuit implementation, optimal below-capacity error exponent, or exact finite-copy fidelity optimum is claimed. The finite-copy higher-dimensional APPT purity conjecture and APPT=AS remain separate questions. The earlier qutrit Lean proof and preprint and the collective-negativity preprint are immutable and unchanged. Author affiliation, funding status, and AI-assistance disclosure appear in the manuscript.

Collective-unitary logarithmic negativity: exact all-spectrum rate — analytic preprint v1

Eight-page analytic preprint by Yongxian Zhang: The collective-unitary logarithmic-negativity rate of every bipartite spectrum.

For every density matrix rho on C^m tensor C^n, with 2 <= m <= n and spectrum p (zero eigenvalues allowed), the paper proves

lim_{k -> infinity} (1/k) max_U log ||(U rho^{tensor k} U*)^{Gamma_{A^k:B^k}}||_1
= min_{1 <= alpha <= 2} [log m + (alpha-1) log n + log sum_i p_i^alpha] / alpha.

For m=n=d this becomes (1/2) log(d^2 Tr(rho^2)). A fixed blockwise Bell output basis suffices at the exponential scale; only the assignment of eigenvalues changes. The unequal-dimension formula can require an interior Renyi parameter, and an exact 2 x 8 example has alpha=3/2.

The lower bound is supported by a dimension-uniform one-shot spectral-prefix estimate, using random Bell-basis projections and the published matrix Bernstein theorem of Tropp. Spectral types match the Schatten-norm upper bounds. This is an analytic proof, not a Lean-formalized theorem or external peer review. Exact ancillary calculations and deliberate corrupted-source controls passed independent CI run 38027937313. Those checks support the calculations and are not a certificate of the full unbounded proof.

Publication commit: 3fac265d142cbc5ce48700abce5cced59a1a4b8f.
Ancillary-tested source: a09f51daa1deed207ad39a9360ab8efd87d496f2.
Directory: research/collective-unitary-negativity-rate/.
CI: https://github.com/mxym/math/actions/runs/38027937313

The source archive contains the complete proof, standalone LaTeX, exact standard-library checker, source-mutation tests, source hashes, and literal CI records. From its extracted root:

python3 verify_sources.py
python3 check.py
python3 -O test_checker.py

Compile main.tex twice with pdfLaTeX, or rebuild from PROOF.md using python3 build_manuscript.py with Pandoc and pdfLaTeX. PREPRINT_BINDING.json and SHA256SUMS bind the PDF and source to the publication and tested commits.

The operation class permits unrestricted global unitaries but no extra ancilla, measurement, conditioning, or discarded system. The theorem does not claim a local distillation rate, efficient circuits, the exact one-copy maximum, APPT=AS, or a solution of the finite-copy higher-dimensional APPT purity conjecture. Prior finite-copy activation and finite-spectrum entanglement bounds are explicitly credited. No exhaustive novelty/priority certification, new DOI, or arXiv submission is asserted. Author affiliation, independent funding status, and AI-assistance disclosure are included.

The earlier complete qutrit Lean Release and its public preprint DOI 10.5281/zenodo.23269470 remain unchanged and are separate results.

Mutual-information continuity counterexample v2 — verified classical Lean proof

This immutable v2 release supplies the independently verified classical probability-table Lean formalization of the counterexample in unchanged written-proof v1.

Exact public source commit: 363224e0f7cf1d7ea7b4ed2546f8ed372da7b04c. Complete source and reproduction package.

The original Lean source is byte-preserved (SHA-256 1726a70d840a8af78ccde0fb0801273a5e9acc424b258684fce21c07d6c9419d). Actual classical 3-by-3 joint probability tables, their marginals, Shannon entropies, mutual information and exact half-L1 distance are formalized. The strict violation holds at every 0 < epsilon <= 1/16, and there are valid counterexamples in every positive-distance neighborhood. Both marginals change; this does not resolve the fixed-one-marginal proposal.

One freshly compiled owned module; all 38 owned declarations and the complete 16,161-declaration dependency closure passed replay in an initially empty kernel at trust level 0. Only propext, Classical.choice and Quot.sound, with their pinned actual signatures, are admitted. The invalid-proof control was rejected, dependency-cache fingerprints stayed unchanged, and separate literal-table semantic checks passed. This is an independently recorded local verification, not a claim about unrelated GitHub Actions workflows.

The standalone proof source, reproducible source archive, complete replay records, losslessly compressed dependency graph, replay summary, exact commit binding and asset checksums are attached. The source archive includes the pinned toolchain/dependency metadata, reproduction driver, every command log, ownership inventory and negative test. Archived build products are evidence; the reproduction driver freshly builds its own owned module.

Scope: the diagonal quantum embedding remains a written argument; no general quantum spectral-function library is formalized. The written paper's Section 5 necessary leading-coefficient lower bound is not closed in this Lean source and is not claimed formalized. Novelty/priority remain unconfirmed; no external human peer-review certificate is claimed. V1's content, original publication time and assets remain unchanged.

Ternary mutual-information continuity counterexample — written proof v1

Written-proof v1 of an explicit ternary classical counterexample to the general different-marginals mutual-information continuity proposal in arXiv:2408.15226v2, Eq. (106), also v1, Eq. (54).

For every 0 < epsilon <= 1/16, the two actual 3 × 3 joint probability tables have total variation distance exactly epsilon, mutual-information difference 2 h(epsilon) - epsilon log 2, and strictly positive excess h(epsilon) - epsilon log 16 over the proposed bound h(epsilon) + epsilon log 8. Thus the general proposal fails at arbitrarily small distances. As diagonal density matrices, the same tables also supply a commuting quantum example.

Scope and status: both marginals change. The fixed-one-marginal version remains unresolved by this note. Novelty and priority are unconfirmed. This release contains the complete written proof; Lean formalization is incomplete and not certified in this version. No external independent review is certified.

Source is fixed to commit a179e33532707abe09247d87aad484e9965847b4, directory notes/mutual-information-continuity-counterexample/. Source PR #12 contains the isolated addition.

Six assets: paper.md, paper.pdf, paper.tex, mutual-information-continuity-counterexample-v1-source.tar.gz, RELEASE_BINDING.json, and SHA256SUMS_ASSETS. The source archive contains all eight files at the fixed commit, including the full written proof, reproducible TeX/build script, three-page PDF, version manifest and source checksums.

Mechanical verification: both primary equation locations checked; all eight source files read back byte for byte from the fixed commit; all three rendered PDF pages and formulas checked; two builds in separate temporary directories yielded identical PDF bytes. RELEASE_BINDING.json records the exact commit, source-file hashes, publication scope and asset hashes; SHA256SUMS_ASSETS covers the other five assets.

PDF SHA-256: 86f45ddb61649676d8982d351b2958a0d44b2ba9ffcbff6b62f90ff46e4bdfc4.

All-graph Laplacian strong Chollet — complete Lean formalization (v2)

This version supplies the complete Lean formalization of the all-graph Laplacian strong Chollet theorem released in mathematical v1, together with a fresh independent compilation and empty-kernel replay.

For every finite simple unweighted graph G and every vertex subset S, let A be the principal submatrix of the real graph Laplacian on S. The formal theorem proves per(A ∘ A) ≤ per(A) · ∏_{v∈S} degree_G(v), with degrees taken in the original graph. It includes empty subsets, isolated vertices, disconnected graphs and singular Laplacians. The accompanying theorem covers the full graph Laplacian plus any entrywise nonnegative real diagonal addition.

• Main theorem: Chollet.strongChollet_all_graphs.
• Diagonal addition: Chollet.laplacianDiagonalStrong_all.
• Frozen PR #10 head: 4d2eefd40ee930216ccd8fc0f51e4bf694251967.
• Release/tag source: merge commit 7b7ac8da240aba15fb4af5d7d37c97458057e07e.
• Exact package: formalizations/laplacian-chollet-all-graphs-progress/, 124 files, including 83 fresh proof modules. All package blobs equal the frozen head; files outside the package equal the merge first parent.

Independent verification completed on 2026-10-09 with the pinned Lean 4.34.1 toolchain and nine pinned dependencies: all 83 modules compiled; all 168 recorded commands exited successfully; all 985 owned declarations and their 44,173-declaration dependency closure replayed in an initially empty kernel at trust level zero. The main theorem closure has 42,988 declarations. The only axioms are the three pinned standard axioms propext, Classical.choice and Quot.sound; an invalid proof of False was rejected by the negative kernel control. A separately compiled literal interface check confirms the original-degree principal-submatrix statement and the nonnegative diagonal extension. Dependency-cache fingerprints were unchanged during the replay.

The independent replay archive contains the fresh sources, complete command logs, declaration inventory, dependency closure, kernel audit, standard-axiom signatures, negative control and literal semantic check. The source archive retains the complete reproduction driver, pinned configuration, written proof, provenance records and licenses, including the attributed OpenAI PerfectMatching components and their Apache 2.0 license. Thirty-eight pinned upstream source files were independently checked.

Five assets:

• laplacian-chollet-general-v2-lean-source.tar.gz
• laplacian-chollet-general-v2-lean-independent-replay.tar.gz
• replay-summary.json
• RELEASE_BINDING.json
• SHA256SUMS_ASSETS

RELEASE_BINDING.json binds the exact source commits, source-package checksums, toolchain, dependencies and asset hashes. SHA256SUMS_ASSETS covers the other four assets. Extract the source archive and follow its README and reproduce.py instructions to reproduce the checks.

GitHub Actions had no runs, checks or commit statuses for the frozen head or merge commit at the post-merge check; no CI pass is claimed. This release records independent source, semantic-interface and kernel verification, without an external human peer-review certificate or a global priority claim.