Halve the sparse-feedback coefficient with a sharp complex entropy bound

research/sharp-complex-entropy-defect/PROOF.md

@@ -0,0 +1,165 @@
+# A sharp complex entropy defect and a stronger sparse-feedback bound
+
+This scoped proof was produced by Nick Petalas. Apache-2.0.
+
+## The new scalar lemma
+
+Use base-two logarithms in `h(z)=-z log_2|z|`, with `h(0)=0`.
+For every pair of complex numbers,
+
+```text
+|h(p)+h(q)-h(p+q)| <= |p|+|q|.                         (1)
+```
+
+The constant one is sharp. For a nonzero pair, equality holds exactly when
+`p=q != 0`. The zero pair also gives equality. In particular, this is a
+modulus bound on the full complex defect, rather than just its real part.
+
+Here is a self-contained proof. Work first with natural logarithms and put
+`D=-p ln|p|-q ln|q|+(p+q)ln|p+q|`, using continuous zero conventions.
+The terms containing `ln|gamma|` cancel, so
+`D(gamma p,gamma q)=gamma D(p,q)` for every complex gamma. If either input
+is zero, the defect is zero. Otherwise divide by `|p|+|q|` and exchange
+the inputs if necessary. Write
+
+```text
+a=|p| >= b=|q| > 0,    a+b=1,    s=p+q,    r=|s| <= 1.
+```
+
+If `r=0`, then `q=-p`, `a=b`, and the defect is zero. For `r>0`,
+
+```text
+D = s ln(r/a) + q ln(a/b).                            (2)
+```
+
+For `r>=a`, both logarithms in (2) are nonnegative. The function
+`u ln(u/a)` is increasing for `u>=a`, so the triangle inequality gives
+
+```text
+|D| <= r ln(r/a)+b ln(a/b)
+     <= ln(1/a)+b ln(a/b)
+      = -a ln a-b ln b <= ln 2.                       (3)
+```
+
+The last inequality is the binary entropy maximum, obtained by differentiating
+in `a`. Equality requires `r=1` and `a=b=1/2`. Equality in the ordinary triangle
+inequality `|p+q|<=|p|+|q|` then makes the inputs parallel with the same phase,
+so `p=q`. Conversely, equal nonzero inputs give `D=2p ln 2`.
+
+For `0<r<=a`, the first logarithm in (2) is nonpositive. The standard
+calculus inequality `u ln(1/u)<=1/e` for `u>0` gives
+
+```text
+r ln(a/r) <= a/e.
+```
+
+Apply the same inequality to `u=2b/a` to obtain
+
+```text
+b ln(a/b) = b ln 2 + (a/2)*(2b/a)*ln(a/(2b))
+          <= b ln 2 + a/(2e).
+```
+
+Consequently
+
+```text
+|D| <= 3a/(2e)+b ln 2 < (a+b)ln 2 = ln 2.            (4)
+```
+
+For an exact coarse justification of strictness, `e>8/3` follows from its
+positive power series. Cauchy-Schwarz on the integral of `1/u` over `[1,2]`
+gives `ln 2>2/3`, whereas `3/(2e)<9/16<2/3`.
+Equations (3) and (4), homogeneity, and division by `ln 2` prove (1) and its
+equality classification. No matrix premise is needed for this lemma.
+
+## Application to the cited sparse-feedback contract
+
+Chris R / Clear1nsight's [PR #4036](https://github.com/CrocSwap/integer-mult-bounds/pull/4036),
+at the source bytes pinned in SOURCES.json, supplies the following premises.
+They are cited results here, not new verification claims:
+
+- The fixed machine prefix is an invertible complex matrix `M`.
+  With its fixed analytical preconditioner `J`, `||J||_2=1`, put
+  `N=M^{-*}J`, `p_ij=M_ij conjugate(N_ij)` and `Phi(M)=sum_ij h(p_ij)`.
+- The legal coupled endpoint has `Re Phi = lambda f V`; the initial value
+  is zero. This includes the source's restored dirty auxiliaries and its
+  returned-clean auxiliary reduction. Its boundary is
+  `F=[[C,lambda B],[0,I]]`, `C=BA`, with unitary `A,B`, and each `B` row
+  has `2^f` equal-magnitude nonzero entries.
+- The actual sole native call has jump `Delta_Q`. Invertible monomial steps
+  preserve Phi. Under the source's child-first, payload-preserving monomial
+  premise, the native jump is zero. General interleaving retains the jump.
+
+Replace only the local scalar estimate in that argument. An arithmetic update
+`G=I+c e_t e_s^T` changes row `t` of `M` and row `s` of `N`, since
+`N'=G^{-*}N`. For each column `j`, its two affected products obey
+
+```text
+p'_tj+p'_sj = p_tj+p_sj.
+```
+
+Subtract the common `h(p_tj+p_sj)` from the old and new pair sums.
+Applying (1) to each pair yields
+
+```text
+|Delta Phi| <= sum_j (|p_tj|+|p_sj|+|p'_tj|+|p'_sj|).
+```
+
+For any row at a prefix, Cauchy-Schwarz gives the already cited row estimate
+
+```text
+sum_j |p_ij| <= ||row_i M||_2 ||row_i N||_2
+             <= ||M||_2 ||M^{-1}||_2 ||J||_2 = cond_2(M).
+```
+
+Writing `kappa^-` and `kappa^+` for the conditions before and after the update,
+we have the stronger local estimate
+
+```text
+|Delta Phi| <= 2*(kappa^-+kappa^+) <= 4 K_t,             (5)
+```
+
+where `K_t=max(kappa^-,kappa^+)`. Telescope exactly as in the source. The new
+necessary conditions are
+
+```text
+4 sum_t K_t + Re(Delta_Q) >= lambda f V,
+4 K S       + Re(Delta_Q) >= lambda f V.                (6)
+```
+
+Here `S` counts every updated scalar coordinate and `K` bounds every full
+formal machine prefix, including the internal cuts of masked operations.
+At `lambda=1/2`, the source's child-first zero-jump class therefore satisfies
+
+```text
+S >= f V / (8 K).                                     (7)
+```
+
+The predecessor states `8 sum K_t` and `fV/(16K)`. Equations (6) and (7)
+halve the former coefficient and double the latter lower bound. This
+improvement uses the new sharp scalar inequality. It does not require
+recounting any predecessor endpoint or numerical fixture.
+
+The scalar constant in (1) is optimal. We do not claim optimality of the
+matrix coefficient four: the triangle inequality and row estimates in (5)
+may leave joint slack. The native jump, conditioning premise and original
+boundary hypotheses remain explicit. General ill-conditioned or native-
+interleaved sparse algorithms are not excluded by (7).
+
+## Credit and limits
+
+Credit Chris R / Clear1nsight #4036 for the preconditioner, boundary potential,
+native-cut accounting and returned-clean argument, and #4009/#3989 with
+Gonzalo Mier #3975 and their retained selected/native lineage for the Pauli
+boundary. Nir Ailon and Gal Yehuda supply the classical conditioning and
+preconditioned quasi-entropy method cited by #4036. Triangle inequalities,
+binary entropy and elementary calculus are classical. No general literature
+priority is claimed for them or for scalar entropy bounds.
+
+The new contribution is the sharp all-complex defect proof, equality
+classification and its stronger source-relative sparse-feedback consequence.
+This is a written scoped proof with finite corroboration. It supplies no
+physical caller, new native word, complete multiplication theorem, supplier
+admission or new kappa. Physical routing, precision, stock and all-size
+compiler/outer obligations remain outside this package. Independent human
+and formal proof-kernel review are unclaimed.

research/sharp-complex-entropy-defect/README.md

@@ -0,0 +1,111 @@
+# Halve the complex sparse-feedback update coefficient
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped written proof with exact finite corroboration. The new
+all-complex inequality is
+
+```text
+h(z) = -z log_2|z|, h(0)=0,
+|h(p)+h(q)-h(p+q)| <= |p|+|q|.
+```
+
+The constant one is sharp. Apart from the zero pair, equality holds exactly
+when `p=q != 0`. The proof covers cancellation, arbitrary complex phases
+and every magnitude. It is self-contained in [PROOF.md](PROOF.md).
+
+Applied to Chris R / Clear1nsight's [PR #4036](https://github.com/CrocSwap/integer-mult-bounds/pull/4036)
+sparse-feedback contract, the lemma strengthens its necessary conditions to
+
+```text
+4 sum_t K_t + Re(Delta_Q) >= lambda f V,
+4 K S       + Re(Delta_Q) >= lambda f V.
+```
+
+At `lambda=1/2`, the source's child-first zero-jump class therefore needs
+`S >= fV/(8K)`, twice its stated `fV/(16K)` bound. The predecessor's
+preconditioner, endpoint value, auxiliary reduction and native-cut accounting
+are cited premises. No predecessor verifier or fixture is imported or replayed.
+This package proves the new scalar step and derives its stronger consequence.
+Optimality of the circuit coefficient four is not claimed.
+
+`S` charges every updated scalar coordinate. `K` bounds every full formal
+machine prefix condition number, including masked-operation internal cuts.
+`Delta_Q` is the actual jump across the sole native call. Its zero value
+requires the cited child-first, payload-preserving monomial premise.
+The source allows arbitrary restored dirty auxiliaries and returned clean
+auxiliaries. All its remaining boundary and linear-operation hypotheses apply.
+
+## Reproduce
+
+From the repository root, using standard-library CPython 3.12:
+
+```sh
+/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
+```
+
+Another CPython 3.12 executable may replace the absolute interpreter path.
+The direct verifier is read-only and Git-free. It prints
+`PASS_SHARP_COMPLEX_ENTROPY_DEFECT scalar_constant=1 update_coefficient=4`
+and a generated receipt containing all six package-file SHA256 hashes.
+The receipt records checked bytes; it is not a proof-kernel certificate.
+
+The complete finite grid has 2,401 ordered pairs of Gaussian integers with
+real and imaginary parts in `[-3,3]`. It checks all 48 nonzero equality
+cases and strictness of every other nonzero-input pair. Logarithms use exact
+rational enclosures from 48 terms of the atanh series with its explicit
+geometric tail. Square roots use 192-bit rational enclosures. A separate
+branch checks 161 dyadic-norm pairs with exact logarithm identities and
+squared rational comparisons. The checker also covers 100 scaled rational
+complex pairs, 192 columns from 64 new complex mixing fixtures, six semantic
+controls and six rejected input-domain cases. These fixtures belong to this
+new lemma; they are not a replay of #4036's endpoint evidence.
+
+The universal result rests on the written proof. Finite enumeration alone
+does not prove it. `SOURCES.json` pins the predecessor proof/README and the
+original revision-8 card as historical provenance. The standalone checker
+has no live external input, network dependency or third-party dependency.
+
+## Scope, credit and verification limits
+
+Credit Chris R / Clear1nsight #4036 for its coupling potential and boundary
+argument; #4009/#3989, Gonzalo Mier #3975 and their retained Pauli/native
+lineage for the coupled boundary; and Nir Ailon and Gal Yehuda for the
+classical preconditioned quasi-entropy method. Elementary calculus and binary
+entropy are classical. No literature-wide priority is claimed. The new step
+is the sharp complex defect, its equality classification and this stronger
+source-relative bound.
+
+This package does not supply a native word, supplier admission or a new
+kappa. General interleaving retains `Delta_Q`; unbounded conditioning remains
+outside the zero-jump obstruction. Complete physical routing, precision,
+stock, compiler and outer multiplication obligations remain unrun.
+Independent human and formal proof-kernel review are unclaimed. The selected
+frontier remains unchanged.
+
+The checker has no recursion or unbounded loop. It fixes all enumeration domains,
+caps logarithm input numerators/denominators at 256 bits and the cache at
+4,096 entries, and caps each of six receipt files at 128 KiB. Functions fit
+within 29 physical lines. Python and Fraction allocate dynamically, so fixed
+post-initialization storage is a documented managed-runtime deviation. The
+domain bounds limit live data; no allocation instrumentation is claimed.
+The six invalid-input control calls use a fixed tuple of known functions.
+Warning-strict normal/optimized runs and AST inspection are the local
+diagnostics. No repository-wide static analysis or historical suite is claimed.
+
+## Open next questions
+
+1. Can the matrix update coefficient four be reduced by using joint constraints
+   on the old/new pair products? Its scalar constituent is sharp, but the
+   two triangle bounds and four row-norm bounds need not be jointly tight.
+   Start with a single invertible two-row matrix and its inverse-dual image.
+   A universal matrix bound or attaining family is missing.
+2. Can a named interleaved native caller exploit the sharper accounting?
+   First compute its actual pre/post-native potential and complete paid
+   arithmetic volume. Its jump, conditioning, precision and physical bill
+   must be supplied before any supplier conclusion.
+
+Structured first steps and blockers are in [TASK.json](TASK.json).

research/sharp-complex-entropy-defect/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/selected-sparse-feedback-volume/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "0afdb973ca23929dbc909218dacf2bfff4497b4b",
+      "sha256": "f1b91f21604796fb2c3e7e75e8e620ee92752846ad9792696da100603b2bdb4d"
+    },
+    {
+      "path": "research/selected-sparse-feedback-volume/README.md",
+      "usage": "provenance",
+      "git_blob": "725a61b3fc002577d80ee04fcc203f0cce2a5f08",
+      "sha256": "b1f0843c10a6959b8f8119238ecc1e7323704f9bf89ed6c9a2b7815f2485328c"
+    }
+  ]
+}