diff --git a/research/sharp-complex-entropy-defect/PROOF.md b/research/sharp-complex-entropy-defect/PROOF.md new file mode 100644 index 0000000000..01d608fd3f --- /dev/null +++ b/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 `00` 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. diff --git a/research/sharp-complex-entropy-defect/README.md b/research/sharp-complex-entropy-defect/README.md new file mode 100644 index 0000000000..ce54115dec --- /dev/null +++ b/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). diff --git a/research/sharp-complex-entropy-defect/SOURCES.json b/research/sharp-complex-entropy-defect/SOURCES.json new file mode 100644 index 0000000000..bc6891ea14 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/sharp-complex-entropy-defect/TASK.json b/research/sharp-complex-entropy-defect/TASK.json new file mode 100644 index 0000000000..3b28a22c12 --- /dev/null +++ b/research/sharp-complex-entropy-defect/TASK.json @@ -0,0 +1,129 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "joint-query-controller", + "question": "Can a changed query demand or caller remove real work while satisfying native chronology and restoration?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose an exact caller and a new demand/interface hypothesis. Read the scoped #5617/#5631/#5649/#5747 and #5720/#5745 objections before rebuilding an excluded schedule. Compare the complete matched source/consumer protocols including all retained helper outputs. For an active-mode injection, first check #5745: its canonical delivery claim repays the eight removed centre jobs. Audit that exact claim or change its channel/feedback hypothesis; do not repeat the same free-injection search. Stop if the full favorable budget fails or the required restored output is unobservable.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "query demand", + "active mode", + "5720", + "5745", + "5747", + "caller" + ], + "existing_checks": [ + { + "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.", + "evidence": "research/qq16-caller-install/README.md", + "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.", + "status": "author-checked", + "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove the sharp all-complex entropy-defect constant one and equality cases, then halve the coordinate-update coefficient in PR4036 and double its child-first sparse-volume lower bound.", + "scope_change_reason": "The donation assignment asks for an original result rather than an audit. This takes PR4036's explicitly nonsharp scalar step as a new analytic question. The revision-8 selected-baseline first command passed; no closed caller construction is reopened.", + "bottleneck_link": "A stronger necessary coordinate-update bound screens child-first sparse adapters under the exact cited conditioning and native-cut contract. This is a scoped analytical side result, not a fully priced supplier.", + "budget_minutes": 60, + "stop_rule": "Package the first proved coefficient improvement. Do not optimize the matrix constant, extend the native-jump model, or search for a supplier.", + "outcome": "completed", + "evidence": "PROOF.md gives the all-complex sharp inequality and its stronger sparse-feedback consequence. verify.py provides bounded rational-interval finite corroboration, exact dyadic checks, new mixing fixtures and rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the matrix update coefficient four be reduced using the joint old/new product constraints?", + "why_it_matters": "The sharp scalar bound does not prove sharpness of the complete matrix update bound.", + "first_step": "Optimize or bound one invertible two-row matrix and its inverse-dual image, with the preconditioner norm fixed.", + "blocked_by": "No universal sharper matrix inequality or attaining family is supplied." + }, + { + "question": "Can a named interleaved caller use the sharper accounting with its actual native jump?", + "why_it_matters": "The zero-jump corollary does not exclude general interleaving.", + "first_step": "Freeze the caller pre/post-native matrices and derive its potential jump and total paid volume.", + "blocked_by": "Conditioning, precision, physical costs and native-jump values remain caller-specific." + } + ], + "claim_type": "scoped written proof with exact finite corroboration", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19217796", + "environment": { + "python": "3.12.15", + "dependencies": "standard library only" + }, + "preserved_start": { + "branch": null, + "head": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "status": "Clean detached HEAD; no earlier branch was checked out. Prior commits preserved." + }, + "overlap": { + "main": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "coverage": "Live latest 100 open PRs; latest 200 same-account PRs; latest 30 handoffs and 20 active discussion entries; task overlap cache reports 470 open PRs and 5426 Discussion records with complete remote pagination, but only 216 local records of 7845 note paths; targeted all-state PR4036, sparse and entropy searches; distinctive all-main README and merged-PR searches; batch reservation sources/authors.", + "limitations": "Sparse local overlap helper coverage is incomplete. Main README searches do not cover arbitrary diffs, omitted proof files or unpublished work. Remote queries are non-atomic.", + "source": "PR #4036", + "source_author": "Clear1nsight" + }, + "verification": { + "local": "Warning-strict normal and optimized direct runs and both registered commands pass. Direct observations were 0.307s and 0.298s; total registered package run 0.889s. These are timeout-budget observations, not a benchmark.", + "counts": { + "scalar_pairs": 2401, + "nonzero_equalities": 48, + "exact_dyadic_pairs": 161, + "scaled_pairs": 100, + "mix_columns": 192, + "semantic_controls": 6, + "input_rejections": 6 + }, + "unrun": [ + "Independent human review", + "Formal proof-kernel review", + "Physical/native supplier replay", + "Complete precision/stock/compiler/outer obligations", + "Selected construction cold replay", + "Repository-wide static analysis" + ], + "diagnostics": "In-memory compile and AST inspection pass; largest function is 29 physical lines. Managed-runtime allocation and fixed test-only dispatch are documented deviations." + } +} diff --git a/research/sharp-complex-entropy-defect/VERIFY.json b/research/sharp-complex-entropy-defect/VERIFY.json new file mode 100644 index 0000000000..ed18b86d7f --- /dev/null +++ b/research/sharp-complex-entropy-defect/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact rational-interval scalar and conserved-sum mixing checks, equality/sharpness controls and package-hash receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete finite domain with assertions disabled; checks use explicit exceptions." + } + ] +} diff --git a/research/sharp-complex-entropy-defect/verify.py b/research/sharp-complex-entropy-defect/verify.py new file mode 100644 index 0000000000..6a439ce807 --- /dev/null +++ b/research/sharp-complex-entropy-defect/verify.py @@ -0,0 +1,237 @@ +"""Exact finite corroboration of the new complex entropy-defect lemma. + +The all-complex result is proved in PROOF.md. No predecessor code is executed. +All logarithm intervals below have rational endpoints and explicit tails. +""" + +from fractions import Fraction as F +from hashlib import sha256 +from itertools import product +import json +from math import isqrt +from pathlib import Path + + +Gaussian = tuple[F, F] +Interval = tuple[F, F] +TERMS = 48 +ROOT_BITS = 192 + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def add(x: Gaussian, y: Gaussian) -> Gaussian: + return x[0] + y[0], x[1] + y[1] + + +def mul(x: Gaussian, y: Gaussian) -> Gaussian: + return x[0] * y[0] - x[1] * y[1], x[0] * y[1] + x[1] * y[0] + + +def conjugate(x: Gaussian) -> Gaussian: + return x[0], -x[1] + + +def norm2(x: Gaussian) -> F: + return x[0] ** 2 + x[1] ** 2 + + +def interval_add(x: Interval, y: Interval) -> Interval: + return x[0] + y[0], x[1] + y[1] + + +def interval_scale(c: F, x: Interval) -> Interval: + a, b = c * x[0], c * x[1] + return min(a, b), max(a, b) + + +def log_series(x: F) -> Interval: + require(1 <= x <= 2, "series argument outside [1,2]") + z = (x - 1) / (x + 1) + power, total = z, F(0) + for j in range(TERMS): + total += 2 * power / (2 * j + 1) + power *= z * z + tail = 2 * power / ((2 * TERMS + 1) * (1 - z * z)) + return total, total + tail + + +def log2_interval(x: F) -> Interval: + require(isinstance(x, F) and x > 0, "log argument must be positive Fraction") + require(x.numerator.bit_length() <= 256, "log numerator too large") + require(x.denominator.bit_length() <= 256, "log denominator too large") + k = x.numerator.bit_length() - x.denominator.bit_length() + u = x / F(2) ** k + if u < 1: + k, u = k - 1, 2 * u + require(1 <= u < 2, "binary range reduction failed") + lower, upper = log_series(u) + base_lower, base_upper = log_series(F(2)) + return k + lower / base_upper, k + upper / base_lower + + +def root_interval(x: F) -> Interval: + require(isinstance(x, F) and x >= 0, "root argument must be nonnegative Fraction") + scale = 1 << ROOT_BITS + k = isqrt((x.numerator * scale * scale) // x.denominator) + lower, upper = F(k, scale), F(k + 1, scale) + require(lower * lower <= x < upper * upper, "root enclosure failed") + return lower, upper + + +def entropy(x: Gaussian, cache: dict[F, Interval]) -> tuple[Interval, Interval]: + n = norm2(x) + if n == 0: + return (F(0), F(0)), (F(0), F(0)) + if n not in cache: + require(len(cache) < 4096, "log cache capacity exceeded") + cache[n] = log2_interval(n) + return interval_scale(-x[0] / 2, cache[n]), interval_scale(-x[1] / 2, cache[n]) + + +def defect(p: Gaussian, q: Gaussian, cache: dict[F, Interval]) -> tuple[Interval, Interval]: + hp, hq, hs = entropy(p, cache), entropy(q, cache), entropy(add(p, q), cache) + return tuple( + interval_add(interval_add(hp[j], hq[j]), interval_scale(F(-1), hs[j])) + for j in range(2) + ) + + +def squared_upper(z: tuple[Interval, Interval]) -> F: + return sum(max(abs(a), abs(b)) ** 2 for a, b in z) + + +def check_scalar(p: Gaussian, q: Gaussian, cache: dict[F, Interval]) -> bool: + # Equal-input and zero-input cases are exact identities, so interval + # rounding cannot incorrectly reject equality in the sharp theorem. + if p == q: + if norm2(p): + d = defect(p, q, cache) + require(all(d[j][0] <= 2 * p[j] <= d[j][1] for j in range(2)), "equality lost") + return bool(norm2(p)) + if not norm2(p) or not norm2(q): + d = defect(p, q, cache) + require(all(a <= 0 <= b for a, b in d), "zero-input identity lost") + return False + d = defect(p, q, cache) + lower = root_interval(norm2(p))[0] + root_interval(norm2(q))[0] + require(squared_upper(d) < lower * lower, "strict scalar inequality failed") + return False + + +def check_mix(case: int, cache: dict[F, Interval]) -> int: + # Two rows of a forward matrix and its inverse-dual transform. + # Arbitrary N is allowed: the conservation identity is columnwise. + c = F(case % 5 - 2), F(case % 7 - 3) + if not norm2(c): + c = F(1), F(0) + checked = 0 + for j in range(3): + mt = F((case + j) % 5 - 2), F((case + 2 * j) % 3 - 1) + ms = F((case + 3 * j) % 7 - 3), F((case + j) % 3 - 1) + nt = F((case + 2 * j) % 5 - 2), F((case + j) % 5 - 2) + ns = F((case + j) % 7 - 3), F((case + 4 * j) % 3 - 1) + mt_new = add(mt, mul(c, ms)) + ns_new = add(ns, mul((-c[0], c[1]), nt)) + old = mul(mt, conjugate(nt)), mul(ms, conjugate(ns)) + new = mul(mt_new, conjugate(nt)), mul(ms, conjugate(ns_new)) + require(add(*old) == add(*new), "pair conservation failed") + for pair in (old, new): + check_scalar(*pair, cache) + h = [entropy(z, cache) for z in (*old, *new)] + delta = tuple( + interval_add(interval_add(h[2][i], h[3][i]), + interval_scale(F(-1), interval_add(h[0][i], h[1][i]))) + for i in range(2) + ) + limit = sum(root_interval(norm2(z))[0] for z in (*old, *new)) + require(squared_upper(delta) <= limit * limit, "mixing bound failed") + checked += 1 + return checked + + +def exact_dyadic(p: Gaussian, q: Gaussian) -> bool: + # An independent branch uses only exact log2 values of dyadic norms. + values = [] + for z in (p, q, add(p, q)): + n = norm2(z) + require(n.denominator == 1, "dyadic control expects integer inputs") + k = n.numerator + if k and k & (k - 1): + return False + factor = -F(k.bit_length() - 1, 2) if k else F(0) + values.append((factor * z[0], factor * z[1])) + d = add(add(values[0], values[1]), (-values[2][0], -values[2][1])) + a, b = norm2(p), norm2(q) + excess = norm2(d) - a - b + require(excess <= 0 or excess ** 2 <= 4 * a * b, "exact dyadic bound failed") + equality = excess >= 0 and excess ** 2 == 4 * a * b + require(equality == (p == q), "exact equality classification failed") + return True + + +def controls(cache: dict[F, Interval]) -> int: + one, zero = (F(1), F(0)), (F(0), F(0)) + d = defect(one, one, cache) + require(d == ((F(2), F(2)), (F(0), F(0))), "sharp witness not exact") + require(F(199, 100) ** 2 < squared_upper(d), "subunit-constant control failed") + require(defect(one, (-one[0], F(0)), cache) == ((F(0), F(0)),) * 2, + "cancellation control failed") + require(check_scalar(one, zero, cache) is False, "zero case control failed") + d = defect(one, (F(0), F(1)), cache) + require(d[0] == d[1] == (F(1, 2), F(1, 2)), "nonreal defect control failed") + bad = 0 + for function, argument in ((log2_interval, F(0)), (log2_interval, F(-1)), + (log2_interval, 1), (root_interval, F(-1)), + (log2_interval, F(1 << 257)), (log_series, F(3))): + try: + function(argument) + except ValueError: + bad += 1 + require(bad == 6, "invalid input accepted") + c, ms = (F(0), F(1)), one + wrong = add(mul(c, ms), mul(ms, conjugate((-c[0], -c[1])))) + require(norm2(wrong) > 0, "wrong-conjugation control failed") + return bad + 6 + + +def package_hashes() -> dict[str, str]: + root = Path(__file__).resolve().parent + names = ("PROOF.md", "README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + result = {} + for name in names: + path = root / name + require(path.is_file() and not path.is_symlink(), "invalid package file") + require(path.stat().st_size <= 128 * 1024, "package file too large") + result[name] = sha256(path.read_bytes()).hexdigest() + return result + + +def main() -> None: + cache: dict[F, Interval] = {} + points = tuple((F(x), F(y)) for x, y in product(range(-3, 4), repeat=2)) + equalities = sum(check_scalar(p, q, cache) for p, q in product(points, repeat=2)) + exact = sum(exact_dyadic(p, q) for p, q in product(points, repeat=2)) + scaled = 0 + for k, phase in product(range(-12, 13), range(4)): + unit = ((F(1), F(0)), (F(0), F(1)), (F(-1), F(0)), (F(0), F(-1)))[phase] + a = F(2) ** k + p, q = mul((a, a / 3), unit), mul((a / 5, -a / 7), unit) + check_scalar(p, q, cache) + scaled += 1 + mixed = sum(check_mix(case, cache) for case in range(64)) + rejected = controls(cache) + require(F(3, 2) / F(8, 3) == F(9, 16) < F(2, 3), "proof constants failed") + require(log_series(F(2))[0] > F(2, 3), "log lower bound failed") + print(json.dumps({"scalar_pairs": len(points) ** 2, "nonzero_equalities": equalities, + "exact_dyadic_pairs": exact, "scaled_pairs": scaled, + "mix_columns": mixed, "controls": rejected, + "log_intervals": len(cache), "package_sha256": package_hashes()}, sort_keys=True)) + print("PASS_SHARP_COMPLEX_ENTROPY_DEFECT scalar_constant=1 update_coefficient=4") + + +if __name__ == "__main__": + main()