diff --git a/research/dyadic-cut-family-optimum/PREDECESSOR.json b/research/dyadic-cut-family-optimum/PREDECESSOR.json new file mode 100644 index 0000000000..46d4aac738 --- /dev/null +++ b/research/dyadic-cut-family-optimum/PREDECESSOR.json @@ -0,0 +1,15 @@ +{ + "author": "CubeJerry", + "pr": 6784, + "commit": "c134aa6edc8ed6444bbf7bfcabbed8124ff26c39", + "url": "https://github.com/CubeJerry/integer-mult-bounds/blob/c134aa6edc8ed6444bbf7bfcabbed8124ff26c39/research/dyadic-omega-counterexample/PROOF.md", + "retained_path": "predecessor-proof.md", + "sha256": "986c4341bad842a30655ca959fdf8a13c95764f721499a5e580ad78b64dbac0c", + "git_blob": "e903af6bf67dfced9a235413bb6a7cdb8e08030f", + "used_claims": [ + "Section 6 equation (11) global upper envelope", + "Section 6 equation (12) cut-family mass and chronology" + ], + "review_status": "Cited mathematical input; not independently audited here.", + "license": "Apache-2.0; original notice retained verbatim." +} diff --git a/research/dyadic-cut-family-optimum/PROOF.md b/research/dyadic-cut-family-optimum/PROOF.md new file mode 100644 index 0000000000..4e9fc43cc9 --- /dev/null +++ b/research/dyadic-cut-family-optimum/PROOF.md @@ -0,0 +1,182 @@ +# Exact optimization of the dyadic cut family + +This contribution was produced by Nick Petalas. Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +## Mathematical input and claim boundary + +CubeJerry's [PR #6784](https://github.com/CrocSwap/integer-mult-bounds/pull/6784), +head `c134aa6edc8ed6444bbf7bfcabbed8124ff26c39`, section 6, supplies the +following exact mass for a chronological cut of the balanced dirty word. +For integers `h >= 2`, `0 <= k <= h-2`, and `m=h-k-1`, it reads scratch +`z_(m+1)` after `4^h-(4^k+2)/3` completed leaves and has total channel mass + +```text +6 K_h(k) = (48*4^m-4)*4^k + +(-36*4^m-24*2^m+12*3^m+3)*3^k + +24*2^(m+k)-5. (1) +``` + +The same source proves that the global formal peak `E_h=E_infinity(2^h)`, +over all cuts, registers and both orientations, satisfies + +```text +max_k K_h(k) <= E_h <= 2*4^h-3^h. (2) +``` + +We cite (1) and (2), without rechecking their free-algebra transport proofs. +The unchanged source proof is retained as [predecessor-proof.md](predecessor-proof.md), +with its original attribution. [PREDECESSOR.json](PREDECESSOR.json) binds its +exact bytes and source URL. The new proof below optimizes (1) and quantifies +its convergence. It does not determine the global finite-height peak. + +## The unique optimum at every height + +Let `D_h(k)=2*4^h-K_h(k)`. Substituting `m=h-k-1` in (1) gives + +```text +6 D_h(k) = 4*4^k + 9*4^h*(3/4)^k + 12*2^h*(3/2)^k + -4*3^h -3*3^k -12*2^h +5. (3) +``` + +Subtract (3) at adjacent indices. For `0 <= k <= h-3`, + +```text +8 [D_h(k+1)-D_h(k)] = T_h(k), +T_h(k) = 16*4^k -3^k [3*4^(h-k)-8*2^(h-k)+8]. (4) +``` + +The normalized quantity + +```text +T_h(k)/3^k = 16*(4/3)^k - f(2^(h-k)), +f(t)=3t^2-8t+8, (5) +``` + +is strictly increasing in `k`. Its first term increases. Its subtracted +term decreases, because `f` is strictly increasing for `t >= 4`, and the +arguments under consideration are at least eight. Thus the sign in (4) +changes at most once, from negative to positive. + +There are no ties. For `k >= 1`, `T_h(k)` is one modulo three. For `k=0` +and `h>=3`, `2^h>=8`, so `f(2^h)>=f(8)=136>16` and `T_h(0)<0`. +For `h=2` there is only one candidate. + +Consequently the following rule gives the unique maximizer of (1): + +```text +k_h = the first k in [0,h-3] for which T_h(k)>0; + use h-2 if that set is empty. +m_h = h-k_h-1. (6) +``` + +This is an exact integer criterion. Bisection uses at most +`ceil(log2(h-1))` sign comparisons. The count is a comparison bound, +not a bit-complexity or physical tape-cost claim. + +For example `h=11` gives `k_h=8`, `m_h=2`, cut `4^11-21846`, and readout +`z_3`. Its mass is `7,735,559`. The `m=1` member has mass `7,716,024`. +These values evaluate the cited formula, rather than replaying its native +realization. The improvement inside this explicit family is `19,535`. + +## A sharp exponent for the family's deficit + +Define real constants + +```text +alpha = log(4)/log(16/3), +lambda = 4^alpha, +beta = log_2(lambda) = 4*log(2)/log(16/3). +``` + +Here `beta` is about `1.656289`. For every integer `h>=2`, the optimized +family deficit `D_h=min_k D_h(k)` satisfies + +```text +lambda^h/6 <= D_h <= 6*lambda^h. (7) +``` + +Thus `D_h=Theta(lambda^h)=Theta(n^beta)` for dyadic `n=2^h`. The exponent +is sharp within the family (1). This does not assert that the global peak +has a deficit of this order. + +To prove the lower bound, put `Q=4^h*(3/4)^k`. Since `h-k>=2`, + +```text +9Q >= 16*3^h, +4*4^k-3*3^k >= 4^k, +12*2^h*((3/2)^k-1) >= 0. +``` + +Equation (3) therefore implies `6D_h(k) >= 4^k+Q`. +The two expressions `4^k` and `Q` are equal at the real index +`k=alpha*h`, with common value `lambda^h`. One increases in `k` and +the other decreases. Hence their maximum is always at least `lambda^h`, +proving the lower bound in (7). + +For the upper bound take `k=floor(alpha*h)`. For `h>=12` this is a legal +family index: `alpha<5/6` follows from `3^5<4^4`. Then + +```text +4^k <= lambda^h, +Q <= (4/3)*lambda^h, +2^h*(3/2)^k <= lambda^h. +``` + +For the third inequality it suffices that `2*(3/2)^alpha < 4^alpha`. +Indeed + +```text +alpha*log(8/3)-log(2) + = log(2)*log(4/3)/log(16/3) > 0. +``` + +Dropping the negative terms in (3) now gives +`6D_h(k) <= 28*lambda^h+5 <= 33*lambda^h < 36*lambda^h`. +For the ten remaining heights `h=2,...,11`, exact evaluation of (1),(6) +gives deficits + +```text +19, 64, 209, 668, 2109, 6624, 20809, 65668, 208949, 653049. +``` + +Each is at most `6*3^h`. Finally `lambda>3`, since +`log(4)^2-log(3)*log(16/3)=(log(4)-log(3))^2>0`. +This establishes the upper bound of (7) at every height. + +## Quantitative consequence for the global peak + +Combining the cited envelope (2) with the new constructive bound (7) gives + +```text +3^h <= 2*4^h-E_h <= 6*lambda^h, +n^(log_2(3)) <= 2*n^2-E_infinity(n) <= 6*n^beta, +0 <= 2-E_infinity(n)/n^2 <= 6*n^(-(2-beta)). (8) +``` + +The last two lines apply to dyadic `n>=4`. This gives an explicit +power-saving convergence rate where the predecessor supplied a limit. +The lower and upper exponents for the global deficit still differ. +No arbitrary-`n`, exact global optimum, error-budget profile, physical +rounding realization, new multiplier or new kappa follows. + +## Executable evidence and remaining obligations + +The verifier checks the new integer optimization, adjacent identity and +rational enclosures used for (7). It takes (1) as input and does not +execute any predecessor verifier or reconstruct its channel polynomials. +Its finite arithmetic checks corroborate the written proof; they do not +replace the all-height argument. The same explicit checks run under `-O`. + +Python allocates integers dynamically. This is the bounded managed-runtime +deviation to Power of Ten rule 3: height is restricted to `2..4096`, the +exhaustive range to `2..256`, and no word of length `4^h` is materialized. +All loops have bounds, functions are at most 60 lines, failure checks use +explicit exceptions, and there is no recursion, dynamic code or network +access. Warning-strict normal and optimized replay provide interpreted-code +diagnostics; no external static analyzer is a dependency. Expanding the +height bound requires revisiting integer resource bounds. + +All five selected framework assumptions remain. Independent human review, +formal proof-kernel review, native rounding, internal leaf errors, inverse +precision, physical storage/access and a complete selected caller are unrun. diff --git a/research/dyadic-cut-family-optimum/README.md b/research/dyadic-cut-family-optimum/README.md new file mode 100644 index 0000000000..16bf4a0a27 --- /dev/null +++ b/research/dyadic-cut-family-optimum/README.md @@ -0,0 +1,115 @@ +# The exact best cut in the dyadic two-parameter family + +This contribution was produced by Nick Petalas. Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +This scoped proof gives the unique best member of CubeJerry's +[PR #6784](https://github.com/CrocSwap/integer-mult-bounds/pull/6784) +cut family at every fixed height. It also sharpens the predecessor's +leading asymptotic to an explicit convergence rate. No new kappa is claimed. + +For height `h>=2`, write `m=h-k-1` with `0<=k<=h-2`. The family reads +scratch `z_(m+1)` at completed-leaf cut `4^h-(4^k+2)/3`. Its mass `K_h(k)` +is equation (12) of the cited predecessor, treated as a mathematical input. +The new adjacent-difference identity is + +```text +8 * [K_h(k)-K_h(k+1)] + = 16*4^k - 3^k*(3*4^(h-k)-8*2^(h-k)+8). +``` + +After division by `3^k` this expression strictly increases and never +vanishes. The first positive value gives the unique optimum; if there +is none, use `k=h-2`. Exact integer bisection finds it using logarithmically +many comparisons in `h`. + +Let `D_h=2*4^h-max_k K_h(k)`, and +`beta=4*log(2)/log(16/3)`, about `1.656289`. The new proof establishes + +```text +(2^h)^beta / 6 <= D_h <= 6*(2^h)^beta. +``` + +The exponent is sharp inside this family. For the global formal peak, +the source's envelope consequently gives the new quantitative statement + +```text +0 <= 2-E_infinity(n)/n^2 <= 6*n^(-(2-beta)) +``` + +for every dyadic `n>=4`. No matching global deficit exponent or exact global +maximizer is asserted. [PROOF.md](PROOF.md) proves the optimizer, the bounds, +the finite exceptional heights and the stated distinction. + +## Evidence and reproduction + +From the repository root, with CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -X dev -W error -B research/dyadic-cut-family-optimum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -X dev -W error -O -B research/dyadic-cut-family-optimum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/dyadic-cut-family-optimum +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/dyadic-cut-family-optimum --check-source-history +``` + +An equivalent CPython 3.12 interpreter path works elsewhere. Expected markers +are `PASS_DYADIC_CUT_FAMILY_OPTIMUM`, `PASS_REGISTERED_RESEARCH_PACKAGE`, and +`PASS_RESEARCH_COMMIT_BYTES`. The verifier prints a generated receipt bound to +all eight package files and writes nothing into the checkout. + +The finite arithmetic checks enumerate every family member at heights +`2..256`, check the adjacent identity and unique optimum, and check rational +rate enclosures through height 512 and at 1024, 2048 and 4096. Exact integer +powers bracket the logarithmic balance, so no floating-point decision is used. +The new `h=11` optimum is `k=8,m=2`, with mass `7,735,559`. Five wrong-decision +and formula controls and ten invalid-input rejections must pass in both modes. +These corroborate the new written proof. They do not replay predecessor +channel words or validate the predecessor's theorem. + +## Source boundary, credit and limitations + +The immediate mathematical input is CubeJerry's PR #6784, exact head +`c134aa6edc8ed6444bbf7bfcabbed8124ff26c39`, PROOF section 6, equations +(11), (12) and the family construction. Its unchanged proof is retained in +[predecessor-proof.md](predecessor-proof.md), including its original notice. +[PREDECESSOR.json](PREDECESSOR.json) records the public URL, head and byte +hash. No unavailable side-branch Git object is required for replay. + +Retained mathematical credit goes to Chafik Boukhalfa's balanced dirty word +in #628, Philippe Van Velzen's prefix/exit and inverse lemmas in #2177, +ywz65's support recurrences in #2735, Adam Gall's endpoint channel counts in +#2067, and their credited predecessors, including woklerx, Charles Bethin, +Arham Tahir and Hanson Sun. Their transport results are cited, not audited. +The new contribution is optimization of the stated two-parameter mass and +its quantitative rate. + +This is a formal free-algebra result for independent completed-leaf errors +on the unchanged balanced word. It does not prove simultaneous physical +rounding attainment, internal-leaf error behavior, non-dyadic bounds, a +complete error-budget profile, a native operator realization, precision/tape +costs or supplier admission. All five selected assumptions remain, and the +selected frontier is unchanged. No full selected replay, proof-kernel check +or independent human review is claimed. + +The original `uniform-transfer-audit` card is recorded as changed scope in +[TASK.json](TASK.json). This is a side result relevant to precision envelopes, +not discharge of the selected `precision_tape` assumption. + +## Related open work + +- #6784 is the immediate predecessor. It gives the family and global leading + limit; this package adds its exact finite optimizer and a quantitative rate. +- #6770 studies total mass of one interval transport row; this package sums + distinct completed-leaf error channels and optimizes one cut family. +- #6668 attains a small-error-budget channel segment for `n=2^g-1`; it does + not supply the total mass or optimizer studied here for `n=2^h`. + +## Open next questions + +1. Can another chronological cut family improve the exponent `beta` for the + global deficit? First derive its exact independent-channel total and + compare it to the proved `Theta(n^beta)` limit of this family. The existing + global lower exponent `log_2(3)` does not settle this. +2. Determine exact global finite-height maxima. Start with a phase recurrence + preserving collisions and complete profiles, then compare every phase + with the optimized family here. A mass-only relaxation is insufficient. diff --git a/research/dyadic-cut-family-optimum/SOURCES.json b/research/dyadic-cut-family-optimum/SOURCES.json new file mode 100644 index 0000000000..594089b9c7 --- /dev/null +++ b/research/dyadic-cut-family-optimum/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ] +} diff --git a/research/dyadic-cut-family-optimum/TASK.json b/research/dyadic-cut-family-optimum/TASK.json new file mode 100644 index 0000000000..99bcaf33e9 --- /dev/null +++ b/research/dyadic-cut-family-optimum/TASK.json @@ -0,0 +1,89 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "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": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "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 one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "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": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "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": "Exact optimizer of the dyadic two-parameter completed-leaf cut family and its quantitative convergence rate.", + "scope_change_reason": "Side result from the first open next question of another contributor, PR6784. This does not discharge a selected assumption. It replaces an unquantified family limit by a unique finite optimizer and a sharp within-family deficit exponent.", + "bottleneck_link": "Precision envelopes need chronological total error bounds. This is a formal side result and does not remove the selected precision_tape or physical-caller obligation.", + "budget_minutes": 60, + "stop_rule": "Stop after proving the exact family optimizer and its quantitative rate; leave other cut families and the global finite maximum open.", + "outcome": "completed", + "evidence": "PROOF.md and verify.py; generated hash-bound arithmetic receipt on stdout.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can another chronological cut family improve the global deficit exponent beta?", + "why_it_matters": "The current family has a proved sharp exponent but the global gap remains between exponents log_2(3) and beta.", + "first_step": "Derive an exact independent-channel mass formula for a changed phase path and compare its deficit.", + "blocked_by": "A complete collision-aware transport proof for the new path." + }, + { + "question": "What is the exact global finite-height peak?", + "why_it_matters": "An optimizer inside one family need not maximize across all cuts and registers.", + "first_step": "Develop a phase recurrence retaining complete channel profiles and collisions.", + "blocked_by": "Global comparison across every phase and readout." + } + ] +} diff --git a/research/dyadic-cut-family-optimum/VERIFY.json b/research/dyadic-cut-family-optimum/VERIFY.json new file mode 100644 index 0000000000..ff53074ddf --- /dev/null +++ b/research/dyadic-cut-family-optimum/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-X", + "dev", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact family optimization, adjacent identities, rational rate brackets, finite witness and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-X", + "dev", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same scientific checks and explicit failure paths with assertions disabled." + } + ] +} diff --git a/research/dyadic-cut-family-optimum/predecessor-proof.md b/research/dyadic-cut-family-optimum/predecessor-proof.md new file mode 100644 index 0000000000..e903af6bf6 --- /dev/null +++ b/research/dyadic-cut-family-optimum/predecessor-proof.md @@ -0,0 +1,358 @@ +# A later cut defeats the dyadic Omega conjecture + +Prepared for @CubeJerry with substantial OpenAI Codex assistance. +Apache-2.0. This is a scoped written proof and an exact finite counterexample; +no independent human or proof-kernel review is claimed. + +## 1. Model, statement and source boundary + +Use the unchanged balanced reserved-depth word of Chafik Boukhalfa (#628), +as specified by Philippe Van Velzen (#2177, PROOF.md and PROOF3.md). +A height-h call has n=2^h free, noncommuting factors and L_h=4^h leaves. +Its protected source is x, unread target is y, and distinct scratch fields +are z_1,...,z_h. Siblings reuse deeper scratch. Each leaf is +`destination += sign * factor * source`, with different source/destination. +A positive call runs U,V,U',V'; a negative call runs V,U,V',U'. U uses +the lower half of the factors from x to z_1; V uses the upper half from +z_1 to y. Primes denote the exact inverse calls, including reversed leaf +order. A complete call restores scratch and adds its signed ordered +factor product to y on arbitrary input. + +At each completed leaf destination allow a distinct formal additive error. +At a later cut, its channel to one register is a polynomial in the free +factors. Channel mass is the sum of absolute integer coefficients after +collecting equal words. Different error channels are kept separate. The +profile is the polynomial whose coefficient of u^j counts nonzero +channels of mass j. Its derivative at u=1 is the total channel mass. +Cuts throughout this proof count **completed leaves**, starting at zero. + +The cited source conjecture C1 says its specified cut Omega_n attains the +maximum for every budget of independent errors. The source's finite census +and ywz65's #2735 fixed-cut theorem are credited, not contradicted within +their stated coverage. The latter proves at n=2^h, h>=2, + + O_h = (11*4^h - 11*3^h + 1)/6 + +at Omega_h, whose cut is (11*4^(h-1)-2)/3 and readout is z_h. +It explicitly leaves global maximality open. + +**Theorem.** For every h>=2, in the positive word, read z_2 at cut + + c_h = 4^h - (4^(h-2)+2)/3. + +Its total independent-error channel mass is exactly + + K_h = (47*4^h - 68*3^h + 48*2^h - 20)/24. (1) + +Consequently + + K_h - O_h = 4^h/8 - 3^h + 2^(h+1) - 1 > 0 (2) + +for every h>=7. Thus C1 is false even restricted to dyadic sizes. +At h=7 (n=128), c_h=16042, z_2 is register 3 under x=0,y=1,z_j=j+1, +and K_h=26144 > 26028=O_h. All 16,384 possible leaf errors are an +admissible budget; only already completed leaves can contribute. + +This proves neither a global optimum for K_h nor that n=128 is the +smallest counterexample to C1. It is the first height of this family +with a strict total-mass excess. The factor alphabet, chronology, +restoration and independent-error model are unchanged. + +Section 6 further proves the uniform bound +`E_infinity(2^h) <= 2*4^h-3^h` and constructs a family implying +`E_infinity(2^h)/4^h -> 2`. This replaces the conjectured leading constant +11/6 for the global formal total mass, without asserting an exact +finite-size maximizer or changing the multiplication exponent. + +## 2. Imported complete-call profiles and inverse pairing + +From #2177, every completed-call exit channel has zero source entry and +zero or one signed monomial at each other register. From #2735, let G_j +count complete exit support size, and H_j its subprofile of channels with +a nonzero destination entry. Both are independent of call sign: + + G_0 = H_0 = u, + H_j = (u+2) H_(j-1), + G_j = 4 G_(j-1) + (u-1) H_(j-1). (3) + +In particular + + G_j(1)=4^j, H_j(1)=3^j, + S_j:=G_j'(1)=2*4^j-3^j. + +Define J_j to count only the nonzero **scratch projections** of these +exit channels. Removing the destination decreases the support by one +exactly for H_j. Precisely [u]H_j=2^j destination-only channels become +zero and must not be counted. Hence + + J_j = G_j + (u^(-1)-1) H_j - 2^j, + J_j'(1) = D_j := 2*(4^j-3^j). (4) + +There are no negative powers because H_j is divisible by u, and no +constant term remains. For j=0 this gives J_0=0. Equation (4) is a +projection identity, not erasure of a paid operation. + +We also use #2735's inverse-phase partition, following #2177 Corollary I. +If a positive call C with L leaves is followed by q leaves of C^-1, +put p=L-q. At any readout, errors from the first p leaves of C give the +same channels as at its forward cut p. Each remaining C error gives the +same channel as the matching already executed inverse leaf. The latter +leaf has its own independent error as well. Thus the combined profile is + + forward-prefix profile at p + 2 * inverse-prefix profile at q. (5) + +The matching leaf fixes its own destination basis vector, which is why +injection *after* that leaf is compatible with the cancellation. The +factor two counts distinct errors; it is not a superposition of them. +When applying (5) below, every intervening call is explicitly accounted +for by its action on the relevant column or ignored external target. + +## 3. Two target readouts + +Put p_j=(4^j+2)/3 and q_j=4^j-p_j. At p_j in a positive height-j call, +follow V at every level and finish its final-factor leaf. Read the +call's target. Let Y_j be its error profile. Let Z_j be the profile at +q_j in the negative call, again read at its target. Base values are +Y_0=u and Z_0=0. + +By #2177 Lemma P, the positive prefix target row has coefficient one on +the target and a positive monomial on its source and every scratch. +Their factor lengths are 2^j,2^(j-1),...,1, all distinct. The complementary +negative prefix is P_+(p_j) C^-1. Its target/source coefficient is zero; +its target and scratch coefficients are unchanged. (The complete inverse +subtracts precisely the full source-to-target product.) + +The following two bridges have **no cancellation**. Read a completed +lower-half exit through the positive upper-half row: every nonzero +exit coordinate contributes one distinct word, giving G_(j-1). Read it +through the complementary negative upper-half target row: the source +coefficient is zero, leaving exactly its scratch projection J_(j-1). +The reading coefficients use upper-half letters with distinct lengths; +exit coefficients use only lower-half letters. Their concatenations +cannot coincide. The analogous reverse-direction scratch bridge uses +distinct lower-half reading words followed by upper-half exit words. +These are free-algebra arguments, without commuting factors. + +At the positive readout, full U errors and current V errors therefore give + + Y_j = G_(j-1) + Y_(j-1). (6) + +At the negative readout, the preceding V and current V' errors pair by +(5); the intervening completed U reads the outer source, which is zero +in V-error columns. The U errors see the scratch-only bridge. Thus + + Z_j = Y_(j-1) + 2 Z_(j-1) + J_(j-1). (7) + +These identities include j=1 and the zero-length q_0 prefix. On taking +derivatives and using a_0=1,b_0=0, they imply + + a_j:=Y_j'(1) = (4*4^j - 3*3^j + 5)/6, + b_j:=Z_j'(1) = (8*4^j - 15*3^j + 12*2^j - 5)/6. (8) + +Substitution into a_j=a_(j-1)+S_(j-1) and +b_j=a_(j-1)+2b_(j-1)+D_(j-1) proves these formulas by induction. +They are not interpolations of finite data. + +## 4. The new chronological cut + +Write k=h-2. The cut c_h is in the top V' call, after + + 4^(h-1)-p_k = 3*4^k + q_k + +of that call's leaves. Thus its V,U,V' phases are complete, and its +final U' is at the q_k prefix. Read z_2, the destination of this U'. +Equivalently, the complementary positive prefix of the top V child +has p_k leaves: it lies in that child's U, at the Y_k target readout. + +First analyze this height-(k+1) child in isolation. Its positive-prefix +profile at that register is Y_k. At its complementary negative cut: + +- Its U and current U' errors give Y_k+2Z_k by (5). The intervening + complete V' writes only the external y, never read by the later U'. +- Its V and V' error columns have zero source z_2 and unchanged deeper + scratch after the intervening complete U, which reads an outer source + that is zero in these columns. Their external y is ignored by U'. + Each of the two completed V-type phases contributes J_k through + the scratch-only reverse bridge. Both signs have the same exit profile. + +The child's negative-prefix profile is therefore + + Y_k + 2Z_k + 2J_k. (9) + +Now place the child in the top word. The earlier top V and current V' +errors give, by (5) and (9), + + Y_k + 2(Y_k+2Z_k+2J_k). + +The intervening top U' reads outer x, zero in every V-error column, so +this pairing is legitimate. + +The top U and U' errors contribute two copies of G_(k+1). To see this, +the readout row of the top V' prefix at z_2 is also the row of its +complementary positive prefix: full V^-1 changes only the child's +target row, whereas z_2 is scratch. That row has one monomial on its +source and every scratch field, with distinct lengths 2^k,...,1,0, +and zero on the child's target. It therefore reads **all** of a top +U-type exit support with no cancellation, since the two top factor +alphabets are disjoint. For top U errors the intervening complete V +changes only the ignored outer y. Pairing the complete U with U' +then identifies its retained-footprint columns with the matching U' +exit columns. No scratch is refreshed or relabelled as independent input. + +The exact new profile is consequently + + R_h = 2G_(k+1) + 3Y_k + 4Z_k + 4J_k. (10) + +Taking derivatives in (10) and using (3),(4),(8) gives + + R_h'(1) = 2S_(k+1) + 3a_k + 4b_k + 4D_k + = (188*4^k - 153*3^k + 48*2^k - 5)/6, + +which is (1). This accounts for every earlier error class, including +both inverse phases; it does not count errors at unexecuted leaves. + +## 5. Strict excess and the finite witness + +Let Delta_h be the right side of (2). Its values at h=2,...,7 are +0,-4,-18,-52,-90,116. For h>=7, + + Delta_(h+1) - 3 Delta_h = 4^h/8 - 2^(h+1) + 2 > 0. + +Thus Delta_h>0 for every h>=7. Also K_h/O_h tends to 47/44; this is +a comparison of two fixed-cut masses, not a global-maximum formula. + +At h=7 the complete profiles are: + +| Mass per channel | New cut c_7, z_2 | Omega_7, z_7 | +| --- | ---: | ---: | +| 7 | 2 | 2 | +| 6 | 26 | 29 | +| 5 | 159 | 188 | +| 4 | 626 | 730 | +| 3 | 1822 | 1958 | +| 2 | 4250 | 4122 | +| 1 | 8709 | 7862 | +| Nonzero channels | 15594 | 14891 | +| Total mass | 26144 | 26028 | + +The new profile does not dominate at every error budget. Its first +strict win is at budget 15479: mass 26029 versus the already saturated +Omega mass 26028. This prevents replacing C1 by a new unsupported +universal-profile assertion. + +## 6. A uniform upper bound and the correct leading asymptotic + +Write E_infinity(2^h) for the maximum total channel mass over all cuts, +registers and both orientations. The following upper bound is a direct +consequence of the credited prefix and exit lemmas, rather than an +assumption of C1: + + E_infinity(2^h) <= S_h = 2*4^h-3^h. (11) + +For a scratch readout, the stronger bound D_h=2*(4^h-3^h) applies. + +**Proof.** Fix a positive prefix P at p and its complementary negative +prefix Q at q=L_h-p, so Q=P C^-1 for the complete call C. Transport +*every* full positive-call exit error column through Q. The inverse +partition (5) says their channel multiset is exactly the union of +positive-prefix channels at p and negative-prefix channels at q, one +copy of each. Every entry of Q is zero or one signed monomial (#2177 +Lemma L2, applied to the negative call). Thus the sum of their masses +at any row is at most the sum of all full exit support sizes, S_h. +This bounds each of the two nonnegative prefix sums separately and +covers both orientations. In a scratch row, Q has zero target column +because the target is never read; full exit columns have zero source. +Only scratch exit support contributes, giving D_h. This includes the +empty and complete prefixes. QED. + +The 47/44 fixed-cut comparison is not the end of the asymptotic story. +For integers m>=1,k>=0, let h=k+m+1. Read z_(m+1) in the positive word +at cut + + c_(h,m) = 4^h - p_k. + +In the complementary positive prefix of the top V child, this is m +successive U descents, followed by the positive height-k target readout +at p_k. The case m=1 is the preceding counterexample. Its exact mass is + + 6 K_(h,m) = (48*4^m-4)*4^k + +(-36*4^m-24*2^m+12*3^m+3)*3^k + +24*2^(m+k)-5. (12) + +Here is a derivation that retains every error class. The complete exit +channel count in scratch level ell of a height-r call is +`2*4^(ell-1)*3^(r-ell)`: two U target responses give the first level; +each deeper level receives four unchanged child scratch responses. +These are the endpoint counts credited to Adam Gall (#2067) and +restated in #2177. In a prefix row, let d be the sum of these counts +on its occupied scratch columns. All the rows in this construction +have a nonzero source coefficient and distinct reading words, so +cross-half bridges attain this weighted sum without cancellation. + +Start with a=a_k, b_0=b_k and d_0=D_k from (4),(8). After the first U +wrapper, the old target is the new first scratch; after each further +U wrapper the readout is deeper scratch and ignores the new first +scratch. Therefore + + d_1 = 2*3^k+4D_k, + d_j = 4d_(j-1) (2<=j<=m), + b_j = a+2b_(j-1)+2d_(j-1) (1<=j<=m). (13) + +The forward mass stays a. For b_j, U and its partial inverse contribute +`a+2b_(j-1)` by (5); the two completed V-type calls contribute +`2d_(j-1)` on shared scratch. Their sources are zero and their external +target is ignored. Reading coefficients lie in the lower-half alphabet +and have distinct lengths, while exit coefficients lie in the upper +half; hence these sums are exact, not triangle-inequality estimates. +The first d update adds the occupied new scratch identity; subsequent +ones only multiply older scratch weights by four. + +At the final top V' wrapper, the earlier top U and U' each contribute +`3^(k+m)+d_m`: its source column and the occupied scratch columns. +The earlier V and current V' contribute `a+2b_m`. The same disjoint +alphabet and ignored-target arguments of section 4 apply. Thus + + K_(h,m) = a+2b_m+2*(3^(k+m)+d_m). (14) + +Explicitly solving (13) gives + + d_m = 4^(m-1)*(2*3^k+4D_k), + b_m = (2^m-1)a_k + 2^m b_k + (4^m-2^m)D_k + +(4^m/2-2^m)3^k. + +Substitution of (8) proves (12). No limiting argument was used to +establish these finite identities. + +For each fixed m, divide (12) by 4^h and let k tend to infinity: + + lim K_(k+m+1,m)/4^(k+m+1) = 2 - 1/(6*4^m). + +Since E_infinity is at least this explicit cut mass, its liminf is at +least this number for every m. Letting m grow makes the lower bound +approach two. Equation (11) bounds the limsup by two. We obtain + + lim_(h->infinity) E_infinity(2^h)/4^h = 2. (15) + +Equivalently the exact formal peak is asymptotic to 2n^2 along dyadic +sizes, whereas the old fixed Omega cut is asymptotic to (11/6)n^2. +Equation (15) gives the leading constant, not an exact finite-size +maximum, maximizing cut or all-budget profile. It does not assert +simultaneous attainment by physical rounding or native operators. + +## 7. What the counterexample does and does not establish + +The finite exact witness alone refutes C1 in its stated formal model. +The written argument above additionally supplies all-height profiles and +a family of strict counterexamples and the leading asymptotic of the global +formal total mass. #2735's fixed-cut C2 theorem and the +single-error and maximum-mass-channel bounds are unaffected. This is not +a counterexample to the selected multiplication theorem: C1 is a separate +conjecture, not an adopted selected assumption. + +Channel mass bounds operator error for arbitrary contractive factors via +the triangle inequality. No simultaneous realization by the project's +native operators or actual rounding errors is asserted. Internal leaf +errors, inverse numerical implementations, aliasing, precision/tape costs, +and a full rounded caller remain outside this result. All five selected +framework assumptions remain. No new kappa, physical speedup, formal +kernel acceptance or exact finite-size global optimum is claimed. diff --git a/research/dyadic-cut-family-optimum/verify.py b/research/dyadic-cut-family-optimum/verify.py new file mode 100644 index 0000000000..33f2bda620 --- /dev/null +++ b/research/dyadic-cut-family-optimum/verify.py @@ -0,0 +1,201 @@ +#!/usr/bin/env python3 +"""Exact optimization of a cited dyadic cut formula. Apache-2.0.""" + +from fractions import Fraction +import hashlib +import json +from pathlib import Path + + +MAX_HEIGHT = 4096 +PACKAGE = Path(__file__).resolve().parent + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def validate_height(height: int) -> None: + require(type(height) is int and 2 <= height <= MAX_HEIGHT, "height outside 2..4096") + + +def mass(height: int, k: int) -> int: + """PR6784 equation (12), taken as the mathematical input.""" + validate_height(height) + require(type(k) is int and 0 <= k <= height - 2, "invalid family index") + m = height - k - 1 + numerator = ( + (48 * 4**m - 4) * 4**k + + (-36 * 4**m - 24 * 2**m + 12 * 3**m + 3) * 3**k + + 24 * 2 ** (m + k) - 5 + ) + quotient, remainder = divmod(numerator, 6) + require(remainder == 0 and quotient > 0, "nonintegral or nonpositive family mass") + return quotient + + +def deficit(height: int, k: int) -> int: + return 2 * 4**height - mass(height, k) + + +def difference_sign(height: int, k: int) -> int: + validate_height(height) + require(type(k) is int and 0 <= k <= height - 3, "invalid adjacent index") + t = 2 ** (height - k) + return 16 * 4**k - 3**k * (3 * t * t - 8 * t + 8) + + +def optimum(height: int) -> int: + """Find the first positive adjacent difference, with the right endpoint sentinel.""" + validate_height(height) + low, high = 0, height - 2 + for _ in range(height.bit_length()): + if low == high: + return low + middle = (low + high) // 2 + if difference_sign(height, middle) > 0: + high = middle + else: + low = middle + 1 + require(low == high, "bisection exhausted its bound") + return low + + +def balanced_index(height: int) -> int: + """Exactly floor(alpha*height), alpha=log(4)/log(16/3); no logarithms.""" + validate_height(height) + low, high = 0, height + for _ in range((height + 1).bit_length()): + if low == high: + return low + middle = (low + high + 1) // 2 + if 16**middle <= 4**height * 3**middle: + low = middle + else: + high = middle - 1 + require(low == high, "balance bisection exhausted its bound") + return low + + +def check_height(height: int) -> tuple[int, int]: + values = tuple(deficit(height, k) for k in range(height - 1)) + chosen = optimum(height) + require(values.count(min(values)) == 1, "nonunique optimum") + require(chosen == values.index(min(values)), "bisection missed exhaustive optimum") + previous_normalized = None + for k in range(height - 2): + sign = difference_sign(height, k) + require(sign == 8 * (values[k + 1] - values[k]), "adjacent identity failed") + require(sign != 0, "unexpected adjacent tie") + normalized = Fraction(sign, 3**k) + if previous_normalized is not None: + require(normalized > previous_normalized, "normalized signs not increasing") + previous_normalized = normalized + return len(values), max(0, height - 2) + + +def check_rate(height: int) -> None: + chosen = optimum(height) + d = deficit(height, chosen) + k = balanced_index(height) + require(16**k <= 4**height * 3**k, "bad balance lower bracket") + require(16 ** (k + 1) > 4**height * 3 ** (k + 1), "bad balance upper bracket") + # Both intervals contain lambda**height by the definition of alpha. + a = 4**k + q = Fraction(4**height * 3**k, 4**k) + lower = max(Fraction(a), 3 * q / 4) + upper = min(Fraction(4 * a), q) + require(lower <= upper, "empty rational rate enclosure") + require(6 * d >= upper, "lower deficit rate bound failed") + require(d <= 6 * lower, "upper deficit rate bound failed") + if height >= 12: + require(k <= height - 2, "balanced index outside family") + require(deficit(height, k) <= 6 * lower, "constructive rate choice failed") + + +def check_rejections() -> int: + bad_heights = (None, True, 1, -1, 4097, "11") + count = 0 + for bad in bad_heights: + try: + optimum(bad) + except ValueError: + count += 1 + else: + raise ValueError("invalid height accepted") + for bad in (-1, 10, True, "8"): + try: + mass(11, bad) + except ValueError: + count += 1 + else: + raise ValueError("invalid index accepted") + return count + + +def check_controls() -> int: + # These wrong decisions must violate the independently enumerated objective. + reference = tuple(deficit(11, k) for k in range(10)) + chosen = optimum(11) + require(chosen == 8 and mass(11, chosen) == 7735559, "new finite witness failed") + for wrong in (0, 7, 9): + require(reference[wrong] > reference[chosen], "wrong optimizer control survived") + sign = difference_sign(11, chosen) + actual = 8 * (reference[chosen + 1] - reference[chosen]) + require(-sign != actual, "reversed sign control survived") + require(sign + 8 * 3**chosen != actual, "omitted constant control survived") + return 5 + + +def check_sources() -> dict[str, str]: + record = json.loads((PACKAGE / "PREDECESSOR.json").read_text()) + require(record["commit"] == "c134aa6edc8ed6444bbf7bfcabbed8124ff26c39", "changed source head") + require(record["author"] == "CubeJerry", "changed source attribution") + raw = (PACKAGE / "predecessor-proof.md").read_bytes() + digest = hashlib.sha256(raw).hexdigest() + require(digest == record["sha256"], "retained predecessor bytes changed") + names = ( + "README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", + "PREDECESSOR.json", "predecessor-proof.md", "verify.py", + ) + return {name: hashlib.sha256((PACKAGE / name).read_bytes()).hexdigest() for name in names} + + +def main() -> None: + hashes = check_sources() + candidates = adjacent = heights = rate_brackets = 0 + for height in range(2, 257): + n, d = check_height(height) + candidates += n + adjacent += d + heights += 1 + for height in range(2, 513): + check_rate(height) + rate_brackets += 1 + for height in (1024, 2048, 4096): + check_rate(height) + rate_brackets += 1 + k = optimum(height) + require(k == 0 or difference_sign(height, k - 1) < 0, "left optimality failed") + require(k == height - 2 or difference_sign(height, k) > 0, "right optimality failed") + require(3**5 < 4**4, "alpha<5/6 proof ingredient failed") + for height in range(2, 12): + require(deficit(height, optimum(height)) <= 6 * 3**height, "small-height bound failed") + receipt = { + "result": "PASS_DYADIC_CUT_FAMILY_OPTIMUM", + "claim_type": "scoped proof with finite arithmetic corroboration", + "exhaustive_heights": heights, + "family_candidates": candidates, + "adjacent_identities": adjacent, + "rate_brackets": rate_brackets, + "input_rejections": check_rejections(), + "semantic_controls": check_controls(), + "witness": {"height": 11, "k": 8, "m": 2, "mass": mass(11, 8)}, + "sha256": hashes, + } + print(json.dumps(receipt, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()