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.