diff --git a/research/dyadic-omega-counterexample/PROOF.md b/research/dyadic-omega-counterexample/PROOF.md new file mode 100644 index 0000000000..e903af6bf6 --- /dev/null +++ b/research/dyadic-omega-counterexample/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-omega-counterexample/README.md b/research/dyadic-omega-counterexample/README.md new file mode 100644 index 0000000000..a37b87677a --- /dev/null +++ b/research/dyadic-omega-counterexample/README.md @@ -0,0 +1,145 @@ +# The dyadic formal error peak has leading constant two + +**Exact counterexample and scoped written proof; No new κ.** In the unchanged +balanced dirty word, the proposed universal Omega cut does not maximize +accumulated independent completed-leaf errors. At 128 factors a later scratch +readout has total formal channel mass **26,144**, versus **26,028** at Omega. +The same mechanism gives a family of counterexamples at every dyadic size +from 128 onward, and an asymptotically sharp all-cut upper bound: + +\[ +E_\infty(2^h)\le 2\cdot4^h-3^h, +\qquad \lim_{h\to\infty}\frac{E_\infty(2^h)}{4^h}=2. +\] + +The old fixed Omega cut has leading constant 11/6. This is a result about +formal free-algebra error mass, not a multiplication speed improvement or +physical rounding lower bound. The complete argument is in [PROOF.md](PROOF.md). +It uses credited source lemmas; neither human independent review nor a formal +proof kernel is claimed. Finite checks corroborate, rather than prove, the +all-height statements. + +## Exact result and chronology + +For height h>=2, use the positive word on n=2^h factors; number registers +x=0, y=1, z_j=j+1. Read z_2 at completed-leaf count +`4^h-(4^(h-2)+2)/3`. Its exact total channel mass is + + K_h = (47*4^h - 68*3^h + 48*2^h - 20)/24. + +Subtracting the fixed Omega mass gives +`4^h/8-3^h+2^(h+1)-1`, positive for every h>=7. At h=7: + +| Readout | Completed leaves | Register | Nonzero channels | Total mass | +| --- | ---: | ---: | ---: | ---: | +| New cut | 16042 | 3 | 15594 | 26144 | +| Omega | 15018 | 8 | 14891 | 26028 | + +[WITNESS.json](WITNESS.json) includes both full profiles and SHA256 digests of +**every signed channel polynomial**, including zero channels. The first error +budget at which this new profile wins is 15479. At budget 29 the old cut still +wins, 176 versus 175: the new cut is not a replacement universal profile. + +A deeper version of the same cut family approaches leading constant two. +The upper bound pairs a forward prefix with its complementary inverse prefix, +and charges their combined mass to complete-call exit supports. Section 6 of +the proof gives explicit finite formulas and the limiting argument. We do not +claim the first possible counterexample, an exact finite-height global +maximum, or a maximizing cut for every error budget. + +## Source pins, novelty and credit + +Base and checkpoint canonical main: +`7c49fe32c55de02c2c873655c804b16e4c3fef0a`. +[SOURCES.json](SOURCES.json) pins all five live inputs by SHA256 and Git blob, +and the selected certificate/task catalogue as historical provenance. +The selected accepted value at this base is 0.003125804, from #6030's audited +source `772dd10a5859a1d15f4851feb371519789213ad8`; it is unchanged. + +- Chafik Boukhalfa's #628 supplies the balanced reserved-depth dirty word. +- Philippe Van Velzen (`philippeVV`), #2177, original head + `2cbbb48d3b580e018312278c97b63817de963be7`, supplies the single-error and + prefix/exit lemmas, finite accumulated-error census, and conjecture C1. + Its substantial Claude assistance and predecessor credit remain intact. +- ywz65, #2735, original head `90a507b39063cfaebdf92794fcb9d18f358439a6`, + proves the fixed Omega profile and complete-call support recurrences, + explicitly leaving C1 open. That fixed-cut theorem is unaffected. +- Adam Gall's #2067 supplies endpoint channel counts. Retain the earlier + transport lineage credited by #2177, including woklerx, Charles Bethin + (#1416), Arham Tahir (#1374) and Hanson Sun (#1085). +- The overlap review also considered #5938, #6668 and #6770. Their + single-channel/count or interval-transport scopes differ from the sum over + all independent errors in a chronological prefix here; they are not inputs. + +The new contribution is the C1 counterexample, its exact all-height family, +and the matching leading asymptotic for global formal total mass. No copied +source verifier or recurrence engine is used. The primary replay extracts only +an authenticated predecessor leaf generator for an explicit order comparison; +its own word and polynomial engines remain separate. The forward replay uses +neither that generator nor the primary engine. + +Prepared for **@CubeJerry**, with substantial **OpenAI Codex assistance** in +mathematics, code, verification and writing. All new files are Apache-2.0. +No delegated agents or independent human review are represented. + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3 -I -B scripts/research_package.py --package research/dyadic-omega-counterexample +``` + +Expected: `PASS_REGISTERED_RESEARCH_PACKAGE research/dyadic-omega-counterexample outcome=completed`, +with `PASS_DYADIC_OMEGA_COUNTEREXAMPLE`, `PASS_FORWARD_OMEGA_COUNTEREXAMPLE`, and +`PASS_COLD_OPTIMIZED_AND_TAMPER_CONTROLS`. The package authenticates its five +source inputs. A Git-free export runs the three registered commands directly; +provenance/metadata validation through the repository hook additionally uses Git. + +The bounded replay checks: + +- 134 literal source-order comparisons; 32 full profile comparisons through + height 8; 28 literal generalized-family cases; 4950 integer + recurrence/formula pairs through height 100. +- A separately written **forward** interpreter of all 16,384 witness leaves, + using reversed literal lists for inverses and integer-encoded words rather + than backward tuple words. Both complete signed polynomial digests match. + Another 1954 paired-prefix/readout cases check the upper-bound mechanism + through height 4, including scratch-bound equality. +- Ten primary and four forward controls, including wrong inverse order, + omitted restoration, endpoint/wrong-register substitutions, independent + versus shared opposite errors, and altered typed/profile/digest receipts. +- Cold Git-free replay under optimized Python (`-O`) with warnings treated + as errors, then actual corruption of each source input and the witness, + all required to fail. This is a portability/failure-detection check, + not a third independent mathematical implementation. + +[VALIDATION.md](VALIDATION.md) records the executed checks and their limits. +[TASK.json](TASK.json) records the changed scope, seed, local claim, +search/overlap coverage and stopping rule; [VERIFY.json](VERIFY.json) registers +exact commands. Sparse archive search and live term searches are not an +exhaustive novelty certificate. No repository-wide historical scientific +replay is needed or claimed for this isolated result. + +## Scope and inherited assumptions + +Errors are distinct formal symbols injected **after completed leaves**. +Factors are free and noncommuting; the source's prefix and exit lemmas and +exact scratch restoration are retained. Mass bounds operator error for +contractive factors by the triangle inequality; simultaneous realization +by native operators or rounding is not proved. The package does not cover +internal leaf intermediates, numerical inverses, aliasing, a rounded caller, +or precision/tape costs. All five selected assumptions remain: +`native_all_columns`, `owned_erasure`, `compiler`, `precision_tape`, +`analytic_recovery`. C1 is a separate conjecture, not a selected assumption. + +## Open next questions + +1. Determine exact finite-height maxima and error-budget tradeoffs. A useful + next step is a proved phase recurrence preserving complete channel profiles + and collisions; a mass-only exploratory recurrence is insufficient. +2. Connect this formal envelope to one pinned native rounding implementation, + including inverse phases, restoration, boundaries and tape costs, before + pricing any effect at the selected multiplication caller. + +The finished result requires neither question to be settled. **No new κ.** diff --git a/research/dyadic-omega-counterexample/SOURCES.json b/research/dyadic-omega-counterexample/SOURCES.json new file mode 100644 index 0000000000..be0d2b1fb6 --- /dev/null +++ b/research/dyadic-omega-counterexample/SOURCES.json @@ -0,0 +1,48 @@ +{ + "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" + }, + { + "path": "research/leaf-destination-transport-bound/PROOF.md", + "usage": "input", + "git_blob": "ff752af80689686a4d8732f4697accecface37ae", + "sha256": "c7ac98425cac43065cb146bb87c21ac490de7497c9d577074c03a8234397d2ad" + }, + { + "path": "research/leaf-destination-transport-bound/PROOF3.md", + "usage": "input", + "git_blob": "b08078b6968cb251d0fe28b0e69fb279edf32bac", + "sha256": "3d29811586a624633a960733fb23899fbfa8fc04aa59a7b2975614f4ec5e873a" + }, + { + "path": "research/leaf-destination-transport-bound/check2.py", + "usage": "input", + "git_blob": "446842aaa233624a19f192db36df4a1660a4b1da", + "sha256": "e4c7e04f421a62905c1f9a35caf0559cebde8c9dca4a5053fd46ab950222cc08" + }, + { + "path": "research/leaf-destination-transport-bound/omega.py", + "usage": "input", + "git_blob": "a8205f03c4e51329ee2dd3f1ab7a6deb38fb8d03", + "sha256": "f17d03e94daa1ca0292c136d194e456fe4faf37aa0881b444d0c00b4656abc56" + }, + { + "path": "research/leaf-omega-profile/README.md", + "usage": "input", + "git_blob": "5d8b2ed9ecca470d946092814827c36e4f8c7aef", + "sha256": "0bb9e452a29a4bd5490ac8153273f8acad1c79147b7f485b38b9bbc48acc4d47" + } + ] +} diff --git a/research/dyadic-omega-counterexample/TASK.json b/research/dyadic-omega-counterexample/TASK.json new file mode 100644 index 0000000000..94e7dee90e --- /dev/null +++ b/research/dyadic-omega-counterexample/TASK.json @@ -0,0 +1,120 @@ +{ + "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": "Test PR2177 Conjecture C1 for independent completed-leaf errors in the unchanged balanced dirty word; give an exact dyadic counterexample and a written all-height asymptotic bound.", + "scope_change_reason": "After the revision-8 selection and live overlap review, narrowed the precision audit to the explicitly open historical C1 conjecture in #2177/#2735. This is not an audit or discharge of the selected record's precision_tape assumption at its caller.", + "bottleneck_link": "Precision-side result: a proposed universal interior cut underestimates formal accumulated leaf-error mass. The new all-cut upper bound and matching leading asymptotic replace that conjectural estimate within the dirty-word model. No complete numerical compiler, supplier admission or improvement in kappa follows.", + "budget_minutes": 120, + "stop_rule": "One deterministic dyadic phase-structure investigation, heights 0..8 for candidate discovery; stop the global-optimality search after finding and independently replaying a strict witness. Extend only the same complementary-cut mechanism to an all-height family and upper bound. Freeze the mathematical scope before the final 30 minutes of the 120-minute budget; no unrelated search or parameter sweep.", + "outcome": "completed", + "evidence": "PROOF.md gives C1 counterexamples for h>=7, a source-derived upper bound, and E_infinity(2^h)/4^h -> 2. WITNESS.json records 26144 versus 26028 at n=128. verify.py and forward_check.py use different word generation, propagation directions and monomial encodings; they match complete signed channel digests. portable_check.py checks optimized Git-free replay and actual input/receipt corruption.", + "author": "@CubeJerry", + "ai_assistance": "Prepared for @CubeJerry with substantial OpenAI Codex assistance in source review, mathematics, implementation, testing and writing. No delegated agents, independent human review or proof-kernel acceptance is claimed.", + "open_questions": [ + { + "question": "What is the exact finite-height maximum, and which cuts maximize each error budget?", + "why_it_matters": "The new family fixes the asymptotic leading constant but does not replace C1 with a universal maximizing profile; at budget 29 the old cut still wins.", + "first_step": "Develop a proved finite-state phase recurrence that retains complete profiles or a certified dominance relation, then test all cuts and both orientations at small heights.", + "blocked_by": "A proof that the state representation preserves every channel collision and the tradeoffs between error budgets; the exploratory mass recurrence is not such a certificate." + }, + { + "question": "How does this formal error envelope enter an actual rounded compiler at the selected caller?", + "why_it_matters": "Formal free-algebra mass is only an upper error envelope; actual precision cost and attainability determine whether this affects the multiplication construction.", + "first_step": "Pin one native operator realization and its per-leaf rounding model, including inverse phases, internal intermediates, boundary values and restoration, before pricing a complete caller.", + "blocked_by": "No such native rounding or tape model is supplied by this package; all five selected framework assumptions remain." + } + ], + "track": "adversarial-audit", + "track_integer": 64, + "selection_seed": "00000000000000000000000000000064", + "claim": { + "created_utc": "2026-11-06T11:56:00Z", + "expected_finish_utc": "2026-11-06T13:51:00Z", + "method": "Complementary forward/inverse phase cuts; exact free-algebra replay. No randomized sampling.", + "coordination": "Local claim: no pinned sprint issue found; connected tools do not expose Discussions posting. Read Discussions #1163/#1166 and active discussion list; do not create a reservation issue." + }, + "overlap": { + "candidates": [ + "Net completion-tax application (#6769/#6771, recently covered)", + "Independent-leaf interior accumulation (chosen; C1 open in #2177/#2735)", + "Restored-helper compression contract (#6760, recently covered)" + ], + "sources": "Current priority and family files; PR ledger; live all-state PR searches for Omega/channel, C1/leaf, Omega/counterexample and 26144; #2177, #2735, #5938, #6668 and #6770.", + "limits": "Sparse offline search read 7 notes and omitted 8910 paths; live term searches and handoff review reduce overlap risk but are not an exhaustive novelty certificate.", + "distinct_result": "#2735 proves the fixed Omega profile and leaves C1 open. #6668 concerns maximal single-channel counts; #6770 concerns interval register transport. This package counts every independent error over a chronological prefix and disproves C1." + }, + "checkpoint": { + "at_utc": "2026-11-06T12:34:13Z", + "canonical_main": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "result": "Pre-publication canonical main unchanged after fetch; revision 8, selected certificate, guidance and frozen inputs unchanged. Live overlap rechecked; no same-scope result found in the documented term searches." + }, + "coverage": { + "literal_profiles": "32 full profiles for Y/Z at heights 0..8 and new/Omega at heights 2..8", + "general_family": "28 literal (h,m) pairs for 2<=h<=8, 1<=m actual['omega']['total_mass'], 'strict counterexample') + # A simple four-event calibration fixes update side, inverse order and error timing. + tiny = positive(2) + demand(tiny == [(0, 2, 0, 1), (2, 1, 1, 1), (0, 2, 0, -1), (2, 1, 1, -1)], + 'handwritten word') + calibration = forward(2, tiny, {4: [(0, 'source'), (1, 'target'), (2, 'scratch')]}) + demand([calibration[k]['total_mass'] for k in ('source', 'target', 'scratch')] == [0, 3, 2], + 'handwritten independent endpoint masses') + upper_cases = 0 + scratch_attainment = False + for h in range(5): + nw = positive(2**h) + left, right = [], [] + forward(2**h, nw, {}, mass_trace=left) + forward(2**h, inverse(nw), {}, mass_trace=right) + for t in range(len(nw) + 1): + for reg in range(h + 2): + value = left[t][reg] + right[-t - 1][reg] + bound = (0 if reg == 0 else (2 * 4**h - 3**h if reg == 1 + else 2 * (4**h - 3**h))) + demand(value <= bound, 'paired-prefix upper bound') + upper_cases += 1 + scratch_attainment |= reg >= 2 and value == bound and bound > 0 + demand(scratch_attainment, 'scratch upper-bound equality control') + controls = [] + altered = json.loads(json.dumps(actual['new'])); altered['profile']['7'] += 1 + controls.append(rejected(lambda: same(altered, witness['new'], 'altered profile'), + 'changed_channel_multiplicity')) + altered = json.loads(json.dumps(actual['new'])); altered['completed_leaves'] -= 1 + controls.append(rejected(lambda: same(altered, witness['new'], 'off-by-one receipt'), + 'off_by_one_cut_receipt')) + altered = json.loads(json.dumps(actual['new'])); altered['channel_polynomials_sha256'] = '0' * 64 + controls.append(rejected(lambda: same(altered, witness['new'], 'changed polynomial digest'), + 'changed_signed_polynomial_digest')) + # Run an actual semantically different interpreter: one common error symbol. + small = positive(2) + probe = {4: [(2, 'row')]} + correct = forward(2, small, probe, negative_errors=(2,))['row'] + shared = forward(2, small, probe, common_error=True, negative_errors=(2,))['row'] + demand(shared['total_mass'] == 0 and correct['total_mass'] == 2, + 'shared opposite-error cancellation is effective') + controls.append(rejected(lambda: same(shared, correct, 'independence lost'), + 'actual_shared_error_interpreter')) + print(json.dumps({'status': 'PASS_FORWARD_OMEGA_COUNTEREXAMPLE', + 'witness_leaves_executed': len(events), + 'full_signed_channel_digests_matched': 2, + 'all_cut_paired_prefix_cases': upper_cases, + 'new_mass': actual['new']['total_mass'], + 'omega_mass': actual['omega']['total_mass'], + 'negative_controls': controls}, sort_keys=True, indent=2)) + + +if __name__ == '__main__': + main() diff --git a/research/dyadic-omega-counterexample/portable_check.py b/research/dyadic-omega-counterexample/portable_check.py new file mode 100644 index 0000000000..0bc48df0ab --- /dev/null +++ b/research/dyadic-omega-counterexample/portable_check.py @@ -0,0 +1,80 @@ +#!/usr/bin/env python3 +"""Cold Git-free replay and actual source/receipt corruption controls. + +@CubeJerry with substantial OpenAI Codex assistance. Apache-2.0. +This is transport/failure-detection evidence, not a third mathematical engine. +""" +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def demand(value, label): + if not value: + raise ValueError(label) + + +def main(): + manifest = json.loads((HERE / 'SOURCES.json').read_text()) + inputs = [row['path'] for row in manifest['files'] if row['usage'] == 'input'] + with tempfile.TemporaryDirectory(prefix='dyadic-omega-cold-') as folder: + root = Path(folder) + package = root / 'research' / HERE.name + shutil.copytree(HERE, package, ignore=shutil.ignore_patterns('__pycache__', '*.pyc')) + for path in inputs: + target = root / path + target.parent.mkdir(parents=True, exist_ok=True) + target.write_bytes((ROOT / path).read_bytes()) + demand(not (root / '.git').exists(), 'Git-free tree') + + def run(script, expected=None): + result = subprocess.run([sys.executable, '-I', '-B', '-O', '-W', 'error', + str(package / script)], cwd=root, capture_output=True, + text=True, timeout=180, check=False) + if expected is not None: + demand(result.returncode == 0, script + ': ' + result.stderr) + data = json.loads(result.stdout) + demand(data['status'] == expected, script + ': wrong status') + return data + return result + + primary = run('verify.py', 'PASS_DYADIC_OMEGA_COUNTEREXAMPLE') + forward = run('forward_check.py', 'PASS_FORWARD_OMEGA_COUNTEREXAMPLE') + rejected_sources = [] + for path in inputs: + target = root / path + original = target.read_bytes() + try: + target.write_bytes(original + b'\n# deliberate source corruption\n') + result = run('verify.py') + demand(result.returncode != 0 and 'input SHA256: ' + path in result.stderr, + 'corrupt source was not rejected: ' + path) + rejected_sources.append(path) + finally: + target.write_bytes(original) + receipt = package / 'WITNESS.json' + original = receipt.read_bytes() + try: + data = json.loads(original) + data['new']['total_mass'] -= 1 + receipt.write_text(json.dumps(data)) + result = run('verify.py') + demand(result.returncode != 0 and 'exact typed receipt mismatch' in result.stderr, + 'actual corrupted witness was not rejected') + finally: + receipt.write_bytes(original) + print(json.dumps({'status': 'PASS_COLD_OPTIMIZED_AND_TAMPER_CONTROLS', + 'git_free': True, 'python_optimized': True, + 'primary_status': primary['status'], 'forward_status': forward['status'], + 'rejected_source_corruptions': rejected_sources, + 'rejected_witness_corruptions': 1}, sort_keys=True, indent=2)) + + +if __name__ == '__main__': + main() diff --git a/research/dyadic-omega-counterexample/verify.py b/research/dyadic-omega-counterexample/verify.py new file mode 100644 index 0000000000..dd2b9b720a --- /dev/null +++ b/research/dyadic-omega-counterexample/verify.py @@ -0,0 +1,323 @@ +#!/usr/bin/env python3 +"""Exact backward free-algebra replay for the dyadic Omega counterexample. + +@CubeJerry, with substantial OpenAI Codex assistance. Apache-2.0. +The word/model and fixed Omega profile retain #628/#2177/#2735 credit. +No predecessor verifier or profile engine is imported. +""" +import ast +from collections import Counter +from hashlib import sha256 +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def need(value, message): + if not value: + raise ValueError(message) + + +def authenticate(): + manifest = json.loads((HERE / 'SOURCES.json').read_text()) + count = 0 + for entry in manifest['files']: + if entry['usage'] != 'input': + continue + raw = (ROOT / entry['path']).read_bytes() + need(sha256(raw).hexdigest() == entry['sha256'], 'input SHA256: ' + entry['path']) + import hashlib + blob = hashlib.sha1(b'blob ' + str(len(raw)).encode() + b'\0' + raw).hexdigest() + need(blob == entry['git_blob'], 'input Git blob: ' + entry['path']) + count += 1 + return count + + +def word(n, sign=1, x=0, y=1, depth=2, offset=0, bad_inverse=False): + """Explicit signed-phase recursion; base event is (source,target,factor,sign).""" + if n == 1: + return [(x, y, offset, sign)] + b = n // 2 + u = lambda s: word(b, s, x, depth, depth + 1, offset, bad_inverse) + v = lambda s: word(n - b, s, depth, y, depth + 1, offset + b, bad_inverse) + if sign == 1: + return u(1) + v(1) + u(-1) + v(-1) + if bad_inverse: + return u(-1) + v(-1) + u(1) + v(1) + return v(1) + u(1) + v(-1) + u(-1) + + +def source_word_check(): + """Authenticate first, then extract only the pinned, inspected gen definition.""" + path = ROOT / 'research/leaf-destination-transport-bound/check2.py' + tree = ast.parse(path.read_text(), filename=str(path)) + definitions = [n for n in tree.body if isinstance(n, ast.FunctionDef) and n.name == 'gen'] + need(len(definitions) == 1, 'unique source gen') + module = ast.fix_missing_locations(ast.Module(body=definitions, type_ignores=[])) + namespace = {} + exec(compile(module, str(path), 'exec'), namespace) + cases = 0 + for n in list(range(1, 66)) + [128, 256]: + for sign in (1, -1): + expected = [event for event, _ in namespace['gen'](n, sign)] + need(word(n, sign) == expected, 'literal source order ' + str((n, sign))) + cases += 1 + return cases + + +def channels(events, cut, register): + """One reverse row sweep. Each returned dictionary is a separate leaf error.""" + need(type(cut) is int and 0 <= cut <= len(events), 'cut domain') + row = {register: {(): 1}} + result = [{} for _ in range(cut)] + for j in range(cut - 1, -1, -1): + x, y, factor, sign = events[j] + need(x != y and sign in (-1, 1), 'legal leaf') + source = row.get(y, {}) + result[j] = dict(source) # error is added AFTER this leaf + target = row.setdefault(x, {}) + for monomial, coefficient in source.items(): + mon = monomial + (factor,) + value = target.get(mon, 0) + sign * coefficient + if value: + target[mon] = value + else: + target.pop(mon, None) + return result + + +def profile(ch): + return Counter(sum(abs(c) for c in p.values()) for p in ch if p) + + +def mass(p): + return sum(j * count for j, count in p.items()) + + +def digest(ch): + """SHA256 of JSON [[leaf, [[word-list, signed-coefficient],...]],...]. + + Include empty channels; sort words lexicographically; separators ',',':'. + This convention is reproduced independently by forward_check.py. + """ + rows = [[i, [[list(w), p[w]] for w in sorted(p)]] for i, p in enumerate(ch)] + return sha256(json.dumps(rows, separators=(',', ':')).encode()).hexdigest() + + +def add(*items): + out = Counter() + for multiplier, p in items: + for j, count in p.items(): + out[j] += multiplier * count + return Counter({j: c for j, c in out.items() if c}) + + +def shift(p, amount): + return Counter({j + amount: c for j, c in p.items()}) + + +def recurrences(limit): + """Equations (3),(4),(6),(7),(10), with the credited Omega recurrence.""" + G = [Counter({1: 1})] + H = [Counter({1: 1})] + J = [Counter()] + Y = [Counter({1: 1})] + Z = [Counter()] + A = [None, Counter({1: 1})] # #2735 complementary scratch readouts + B = [None, Counter({1: 1})] + R, O = {}, {} + for h in range(1, limit + 1): + G.append(add((4, G[-1]), (1, shift(H[-1], 1)), (-1, H[-1]))) + H.append(add((2, H[-1]), (1, shift(H[-1], 1)))) + J.append(add((1, G[h]), (1, shift(H[h], -1)), (-1, H[h]), + (-2**h, Counter({0: 1})))) + Y.append(add((1, Y[-1]), (1, G[h - 1]))) + Z.append(add((1, Y[h - 1]), (2, Z[-1]), (1, J[h - 1]))) + for p in (G[h], H[h], J[h], Y[h], Z[h]): + need(all(j >= 1 and c > 0 for j, c in p.items()), 'nonzero profile coefficients') + if h >= 2: + A.append(add((1, A[-1]), (1, G[h - 1]))) + B.append(add((1, G[h - 1]), (1, A[h - 1]), (2, B[-1]))) + O[h] = add((2, G[h - 1]), (1, A[h - 1]), (2, B[h - 1])) + k = h - 2 + R[h] = add((2, G[k + 1]), (3, Y[k]), (4, Z[k]), (4, J[k])) + return G, H, J, Y, Z, R, O + + +def old_cut(h): + return (11 * 4**(h - 1) - 2) // 3 + + +def new_cut(h): + return 4**h - (4**(h - 2) + 2) // 3 + + +def K(h): + numerator = 47 * 4**h - 68 * 3**h + 48 * 2**h - 20 + need(numerator % 24 == 0, 'K integrality') + return numerator // 24 + + +def Omega(h): + numerator = 11 * 4**h - 11 * 3**h + 1 + need(numerator % 6 == 0, 'Omega integrality') + return numerator // 6 + + +def family_mass(h, m): + need(type(h) is int and type(m) is int and 1 <= m < h, 'family domain') + k = h - m - 1 + num = ((48 * 4**m - 4) * 4**k + + (-36 * 4**m - 24 * 2**m + 12 * 3**m + 3) * 3**k + + 24 * 2**(m + k) - 5) + need(num % 6 == 0, 'general family integrality') + return num // 6 + + +def family_from_wrappers(k, m): + # A separate integer recurrence evaluation of equations (13),(14). + a = (4 * 4**k - 3 * 3**k + 5) // 6 + b = (8 * 4**k - 15 * 3**k + 12 * 2**k - 5) // 6 + d = 2 * (4**k - 3**k) + for j in range(1, m + 1): + b, d = a + 2 * b + 2 * d, 4 * d + (2 * 3**k if j == 1 else 0) + return a + 2 * b + 2 * (3**(k + m) + d) + + +def witness_record(ch, cut, register): + p = profile(ch) + return {'completed_leaves': cut, 'register': register, + 'profile': {str(j): p[j] for j in sorted(p)}, + 'nonzero_channels': sum(p.values()), 'total_mass': mass(p), + 'channel_polynomials_sha256': digest(ch)} + + +def first_win(p, q): + left = sorted([j for j, c in p.items() for _ in range(c)], reverse=True) + right = sorted([j for j, c in q.items() for _ in range(c)], reverse=True) + a = b = 0 + for i in range(max(len(left), len(right))): + a += left[i] if i < len(left) else 0 + b += right[i] if i < len(right) else 0 + if a > b: + return {'budget': i + 1, 'new_mass': a, 'omega_mass': b} + return None + + +def make_witness(): + events = word(128) + ch = channels(events, new_cut(7), 3) + old = channels(events, old_cut(7), 8) + return {'schema_version': 1, 'factor_count': 128, 'height': 7, + 'word_leaves': len(events), 'orientation': 1, + 'new': witness_record(ch, new_cut(7), 3), + 'omega': witness_record(old, old_cut(7), 8), + 'strict_excess': mass(profile(ch)) - mass(profile(old)), + 'first_strict_win': first_win(profile(ch), profile(old))} + + +def reject(call, label): + try: + call() + except (ValueError, KeyError): + return label + raise ValueError('negative control unexpectedly passed: ' + label) + + +def same_json(a, b): + need(json.dumps(a, sort_keys=True) == json.dumps(b, sort_keys=True), 'exact typed receipt mismatch') + + +def checks(): + authenticated = authenticate() + source_cases = source_word_check() + G, H, J, Y, Z, R, O = recurrences(100) + literal_cases = 0 + for h in range(0, 9): + plus, minus = word(2**h), word(2**h, -1) + p = (4**h + 2) // 3 + for got, expected in [(channels(plus, p, 1), Y[h]), + (channels(minus, 4**h - p, 1), Z[h])]: + need(profile(got) == expected, 'target-prefix recurrence ' + str(h)) + literal_cases += 1 + if h >= 2: + for cut, register, expected in [(new_cut(h), 3, R[h]), + (old_cut(h), h + 1, O[h])]: + need(profile(channels(plus, cut, register)) == expected, + 'full profile recurrence ' + str((h, cut, register))) + literal_cases += 1 + family_literal = 0 + for h in range(2, 9): + events = word(2**h) + for m in range(1, h): + k = h - m - 1 + cut = 4**h - (4**k + 2) // 3 + actual = mass(profile(channels(events, cut, m + 2))) + need(actual == family_mass(h, m), 'general family literal ' + str((h, m))) + family_literal += 1 + for h in range(2, 101): + for m in range(1, h): + k = h - m - 1 + need(family_mass(h, m) == family_from_wrappers(k, m), 'closed family / wrapper recurrence') + need(family_mass(h, m) <= 2 * (4**h - 3**h), 'scratch upper envelope') + for h in range(101): + need(mass(G[h]) == 2 * 4**h - 3**h, 'exit mass') + need(mass(J[h]) == 2 * (4**h - 3**h), 'scratch mass') + need(6 * mass(Y[h]) == 4 * 4**h - 3 * 3**h + 5, 'Y closed form') + need(6 * mass(Z[h]) == 8 * 4**h - 15 * 3**h + 12 * 2**h - 5, 'Z closed form') + if h >= 2: + need(mass(R[h]) == K(h) and mass(O[h]) == Omega(h), 'total closed forms') + need((K(h) > Omega(h)) == (h >= 7), 'family crossing') + witness = make_witness() + same_json(witness, json.loads((HERE / 'WITNESS.json').read_text())) + need(witness['first_strict_win'] == {'budget': 15479, 'new_mass': 26029, 'omega_mass': 26028}, + 'first winning error budget') + controls = [] + controls.append(reject(lambda: need(K(7) <= Omega(7), 'C1 total bound'), 'C1_total_bound')) + # Omega still wins at a smaller budget: do not claim the new cut is universal. + new_29 = sum(sorted([j for j, c in R[7].items() for _ in range(c)], reverse=True)[:29]) + old_29 = sum(sorted([j for j, c in O[7].items() for _ in range(c)], reverse=True)[:29]) + need((new_29, old_29) == (175, 176), 'opposite budget comparison') + controls.append(reject(lambda: need(new_29 >= old_29, 'new universal cut'), + 'new_cut_does_not_dominate_all_budgets')) + controls.append(reject(lambda: need(K(6) > Omega(6), 'premature family threshold'), + 'height_six_is_not_a_counterexample_of_this_family')) + normal = word(8) + expected = R[3] + bad = word(8, bad_inverse=True) + controls.append(reject(lambda: need(profile(channels(bad, new_cut(3), 3)) == expected, + 'bad inverse profile'), 'wrong_inverse_order')) + dropped = normal[:-len(normal) // 4] + controls.append(reject(lambda: channels(dropped, new_cut(3), 3), 'missing_restoration_phase')) + controls.append(reject(lambda: need(profile(channels(normal, len(normal), 3)) == expected, + 'endpoint profile'), 'completed_endpoint_instead_of_interior_cut')) + controls.append(reject(lambda: need(profile(channels(normal, new_cut(3), 1)) == expected, + 'wrong register profile'), 'wrong_readout_register')) + # A top-U injection and its top-U' inverse mate have identical channels here. + h = 3 + ch = channels(normal, new_cut(h), 3) + block = 4**(h - 1) + pairs = [(i, 3 * block - 1 - i) for i in range(block) + if ch[i] and ch[i] == ch[3 * block - 1 - i]] + need(bool(pairs), 'nonzero paired channel control') + i, j = pairs[0] + independent = 2 * sum(abs(c) for c in ch[i].values()) + merged = {w: ch[i].get(w, 0) - ch[j].get(w, 0) for w in ch[i] | ch[j]} + need(independent > 0 and sum(abs(c) for c in merged.values()) == 0, + 'independent versus shared opposite errors') + controls.append('shared_opposite_errors_cannot_replace_independent_symbols') + mutated = json.loads(json.dumps(witness)); mutated['new']['total_mass'] -= 1 + controls.append(reject(lambda: same_json(witness, mutated), 'understated_receipt')) + mutated = json.loads(json.dumps(witness)); mutated['schema_version'] = True + controls.append(reject(lambda: same_json(witness, mutated), 'boolean_integer_receipt')) + return {'status': 'PASS_DYADIC_OMEGA_COUNTEREXAMPLE', 'source_inputs': authenticated, + 'source_word_comparisons': source_cases, 'literal_profile_comparisons': literal_cases, + 'recurrence_heights': [0, 100], 'general_family_literal_cases': family_literal, + 'general_family_integer_cases': 4950, 'negative_controls': controls, + 'new_mass': K(7), 'omega_mass': Omega(7), 'strict_excess': K(7) - Omega(7)} + + +if __name__ == '__main__': + print(json.dumps(checks(), sort_keys=True, indent=2))