[petalas]

Summary

Scoped written proof with exact finite corroboration. For h(z)=-z log_2|z|, h(0)=0, prove the sharp all-complex inequality

|h(p)+h(q)-h(p+q)| <= |p|+|q|.

Except for the zero pair, equality holds exactly at p=q != 0. Applying this new scalar step to Chris R / Clear1nsight's PR #4036 strengthens its sparse-feedback contract:

- 8 sum_t K_t + Re(Delta_Q) >= lambda f V
+ 4 sum_t K_t + Re(Delta_Q) >= lambda f V

- child-first, lambda=1/2: S >= fV/(16K)
+ child-first, lambda=1/2: S >= fV/(8K)

The new lemma and consequence were produced by Nick Petalas. Credit Chris R / Clear1nsight for the coupling preconditioner, endpoint potential, native-cut accounting and clean/dirty auxiliary reduction; PR #4009/#3989, Gonzalo Mier #3975 and their retained Pauli/native lineage for the boundary; and Nir Ailon and Gal Yehuda for the classical potential method. These are cited premises. No predecessor code, endpoint fixture or numerical result is audited or replayed as this contribution. No general literature priority is claimed.

Only research/sharp-complex-entropy-defect/ is added. Advance CLAIM.

Evidence

Before, #4036 used an explicitly nonsharp scalar constant two and update coefficient eight. After, PROOF.md proves scalar constant one for every complex pair, classifies equality and derives update coefficient four.

Local CPython 3.12.15 normal and optimized warning-strict checks pass:

• All 2,401 Gaussian-integer pairs with components in [-3,3], including 48 nonzero equality cases. A separate exact-logarithm branch covers 161 dyadic-norm pairs.
• 100 scaled rational complex pairs, 192 conserved-sum columns in 64 new mixing fixtures, six semantic controls and six rejected input-domain cases.
• Both registered commands, metadata/source pins, in-memory compilation, AST inspection, staged whitespace checks, exact committed bytes/modes and full source-history preflight.
• Official committed-package export integrity and normal/optimized read-only Git-free exported replays, with all seven exported files and modes unchanged.

All finite logarithm and square-root comparisons use rational enclosures with explicit tails. The direct checks took 0.307s and 0.298s locally; the complete registered run took 0.889s. These observations establish the local timeout budget, not a performance claim. The verifier prints a generated six-file SHA256 receipt.

Reproduce from the repository root, with standard-library CPython 3.12:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/sharp-complex-entropy-defect/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/sharp-complex-entropy-defect/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/sharp-complex-entropy-defect
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/sharp-complex-entropy-defect --check-source-history

The first command prints PASS_SHARP_COMPLEX_ENTROPY_DEFECT scalar_constant=1 update_coefficient=4. The registered command also prints PASS_REGISTERED_RESEARCH_PACKAGE. Another CPython 3.12 executable may replace the absolute path.

Limitations and unrun obligations

The universal statement rests on the written proof. The finite checks are corroboration. Scalar constant one is optimal; optimality of circuit coefficient four is not claimed.

The source-relative consequence retains every full-prefix condition-number and boundary hypothesis. The actual native jump remains in the interleaved bound; its zero value requires the cited child-first, payload-preserving monomial premise. General interleaving and unbounded conditioning remain open.

No physical caller, native supplier replay, complete precision/stock/compiler/outer proof, selected construction cold replay, independent human review or proof-kernel formalization was run. No new kappa or selected-frontier change is claimed.

Open next questions

1. Can the matrix coefficient four be reduced by exploiting joint constraints on old/new products? Start with a single invertible two-row matrix and its inverse-dual image; a universal bound or attaining family is missing.
2. Can a named interleaved caller benefit after its actual native jump, conditioning, precision and complete paid volume are supplied? Begin with the exact matrices on both sides of its native cut.

Related open work

No open PR studying this scalar defect or PR #4036's update coefficient was found in the targeted 4036, quasi-entropy and sparse-feedback searches. PR #4036 and #4009 are merged predecessors. At the finish-line refresh, this account had no open PR created since the advance CLAIM at 2026-10-27 13:27:26 UTC. Thus there is no additional related open contribution to compare. No extra mathematical computations were run to validate other contributions. These searches do not certify unpublished work or every arbitrary diff.

CI notes

At exact contribution head 318c0d7a3a76878c36ee13e9a28d97635d6673e1, run 40513547383 has plan failed; replay skipped. The only failed step is Onboarding helper tests.

All ten unittest failure/error entries are in unchanged tests/test_research_current_assignment.py, ending FAILED (failures=8, errors=2, skipped=22). The two errors are missing follow_up_steps and catalog_first_step keys. The eight assertion failures concern frozen/current routing, missing-reference rejection and sparse-reference omission lists. The complete ten failure/error headers, exception/assertion messages and final summary match the same step in PR #5921 run 40513532365. This is the reported shared main de5ec2e7a onboarding failure; maintainers will handle it. No shared code or tests were changed.

Hosted replay has not certified this package. Only the local scientific and publication checks described above have run. The replay job was skipped after planning failed. The PR's archival merge does not change that verification status or constitute scientific acceptance or a selected-frontier update.

Merge danger

Two-way. The six additive package files have isolated scope; shared code and selected-frontier records are unchanged.