diff --git a/research/ck-dyadic-forest-seed22/CLAIM.md b/research/ck-dyadic-forest-seed22/CLAIM.md new file mode 100644 index 0000000000..9c3f9fda11 --- /dev/null +++ b/research/ck-dyadic-forest-seed22/CLAIM.md @@ -0,0 +1,65 @@ +# Local sprint claim + +Track: complex supplier. OS assignment seed **22**, drawn once with Python +`secrets.randbelow(100)` at 2026-10-13 15:03:42 UTC. +Base: `007664306fff84fbb1c9a1b4053b69f439764034`. +Contributor: Lauren, with substantial OpenAI Codex assistance, including +separate AI implementations and proof review. New work is Apache-2.0. + +Claim: investigate arbitrary dyadic parent coefficients for the historical +PR626 CK compensation panel and PR816 one-parent target-forest class. +Use exact coefficient pricing, PR961's all-dyadic tail reduction and +same-parent exchange argument, applied to the different CK matrix. Check +all 1,086 coefficients n/8, 0<|n|<=543, and 12,432 directed target pairs. +Deliver a concrete checked improvement or a scoped negative result with +reproducer, source pins, adverse controls and independently computed census. +Expected finish: 2026-10-13 15:43 UTC (11:43 America/New_York). +Budget: 40 minutes, final 10 minutes reserved for verification/handoff. + +Three candidates considered: (1) fixed factory diagonal scaling, already +covered by PR949; (2) U8 owner packing beyond T21, overlapping PR942/962; +(3) CK non-power-of-two dyadic parent weights, the explicit remaining gap +in PR964. Candidate 3 is chosen. Seed22 fixes equal-cost MST tie order; +it does not restrict the coefficient/pair domain or create novelty by itself. + +Overlap inspected: required contribution/status/ledger files, selected PR890 +construction and review, latest 100 updated open PRs, plus targeted Horner +and signed-digit PR searches. PR964 head +`7a3bf8460cf6ca16a2bf008ff51fdb06df1af938` closes only signed powers of two +on CK; PR961 head `4257ddf4b755cd0ac3bd3b0f6281cc5b2b1f72ad` closes all +dyadics on X4. This contribution deliberately transports PR961's mathematical +method to the distinct CK matrix; it claims neither that method nor PR816's +original savings as new. No pending executable implementation is imported. + +At initial public API inspection the only open issues were #650 (Discussions) +and #913 (all-size/compiler). No open coordination issue existed. The GitHub +connector returned USER_NOT_LOGGED_IN, so the claim is recorded here. No +separate reservation issue was opened. The checkout needed its local Git +long-path option enabled before the complete Windows checkout could succeed. + +Stopping rule: complete the entire declared finite core once per implementation +and prove the tails. If domination fails, report the explicit improving edge; +do not infer a full forest improvement without a valid complete forest. +No expanded search or new exponent model is planned. + +## Result update + +Completed the full 13,501,152-case census with two separately written checkers. +They agree on every ordered edge cost via digest +`8419c238a791375dd846ba7558aeea9185af8b776f148731c377ad21fe311e6d`. +All dyadic forests in the declared class retain floor 16364; the finite +nonunit margin is 63. A total of 941 nonunit edges beat a root, so same-parent unit +replacement is necessary. See [the result and reproducer](README.md). + +The final refresh after resumption found Adam Gall's PR1220 already reporting +the same result, so this is labeled **independent corroboration**, with no +priority claim. Our two scalar-arithmetic implementations do not use its +packed lanes or executable code. Its pinned receipt agrees on the quantitative +claims. Main advanced to `dadfea6e8a78ff6ba901705f87532a71c6f5bbb8`; both CK +inputs remain identical. No posting credentials were available at that handoff, +so a clean patch and ready-to-submit description were delivered locally. + +Publication resumed after the user connected GitHub. The mathematical scope +is unchanged; the contribution remains independent corroboration of PR1220. +The publication refresh and its coverage limits are recorded in OVERLAP.json. +The scoped result and claim are complete; the pull request is the review route. diff --git a/research/ck-dyadic-forest-seed22/OVERLAP.json b/research/ck-dyadic-forest-seed22/OVERLAP.json new file mode 100644 index 0000000000..0b693aa741 --- /dev/null +++ b/research/ck-dyadic-forest-seed22/OVERLAP.json @@ -0,0 +1,91 @@ +{ + "checked_utc": "2026-10-13T21:05:42.094830+00:00", + "base": "007664306fff84fbb1c9a1b4053b69f439764034", + "refreshed_main": "dadfea6e8a78ff6ba901705f87532a71c6f5bbb8", + "open_prs_scanned": 100, + "latest_open_pr_number": 1247, + "source_files_unchanged": true, + "coordination_issue": "No open sprint coordination issue; only #650 and #913 open", + "github_posting": "Connector USER_NOT_LOGGED_IN; noninteractive Git credential check found no credential", + "relevant_prs": [ + { + "number": 968, + "title": "Research: frame-pair decoders and the exact 8-term complex copy-cost floor (no new kappa)", + "head": "eb1423f701aa8dd30ee6b2465e982bd6de9c3abb", + "author": "themilkman216" + }, + { + "number": 966, + "title": "Research: exact prescribed three-target deletion thresholds (no new kappa)", + "head": "7eaf5665ac246310293fda06a3cf245fe72f6012", + "author": "woklerx" + }, + { + "number": 965, + "title": "Finite bit construction: coupled R439 helper triples save 140 further ADDs (no new kappa)", + "head": "6292e3774abd82f2d5202190b498f35cc1628c39", + "author": "RossRichardson" + }, + { + "number": 964, + "title": "Scoped negative result: power-of-two weights cannot improve CK target forests (no new kappa)", + "head": "7a3bf8460cf6ca16a2bf008ff51fdb06df1af938", + "author": "bitplane" + }, + { + "number": 962, + "title": "Conditional \u03ba = 0.001661960547713947: T37 owner map on PR890's U8 word (independent cross-check of #942)", + "head": "50c6ae8151493af21d284afe34fb35f68f6d4934", + "author": "GamingPuzzled" + }, + { + "number": 961, + "title": "Scoped negative result: X4 target-forest floor holds for all dyadic parent coefficients (no new kappa)", + "head": "4257ddf4b755cd0ac3bd3b0f6281cc5b2b1f72ad", + "author": "woklerx" + } + ], + "distinct_evidence": "PR961 cutoff/exchange method transported to historical CK, closing PR964 non-power-of-two gap: 941 root-improving nonunit edges, all dominated by same-parent unit/root; exact finite minimum margin63.", + "final_checked_utc": "2026-10-13T21:08:21.207162+00:00", + "status": "Independent corroboration of concurrent PR1220, no priority claim", + "same_result": { + "pr": 1220, + "author": "Adam Gall (adamgall)", + "head": "9cd42fb94d2b74e7308ad783b20081aa85b868a1", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1220", + "receipt_url": "https://raw.githubusercontent.com/adamgall/integer-mult-bounds/9cd42fb94d2b74e7308ad783b20081aa85b868a1/research/ck-all-dyadic-forest-seed23/EXPECTED.json", + "receipt_sha256": "790ef24a65801ccb84e528f3b25190590b6de271b2541b94b069533deee41acc", + "checked_equal": [ + "domain", + "cases", + "nonunit cases", + "minimum domination and witness", + "minimum root margin and witness", + "nonunit edges beating root", + "signed floor" + ], + "not_compared": "Different digest encodings; no assertion that the cross-PR raw digest strings coincide", + "distinct_method": "Both local checkers use separate scalar costs and no packed lanes; no PR1220 executable code consumed" + }, + "publication_refresh": { + "checked_utc": "2026-10-13T22:38:58.867416+00:00", + "refreshed_main": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "source_files_unchanged": true, + "open_prs_retrieved": 811, + "unique_prs": 811, + "rest_pages": 9, + "pr_coverage": "All open PR REST pages at refresh; titles and bodies screened by CK/dyadic/Horner/forest and all-dyadic/same-parent keywords; not a code review of every PR. Concurrent changes can affect pagination.", + "same_result_pr": 1220, + "same_result_head": "9cd42fb94d2b74e7308ad783b20081aa85b868a1", + "discussions_read": [ + 1163, + 1166, + 1167, + 1210 + ], + "discussion_index": "https://github.com/CrocSwap/integer-mult-bounds/discussions", + "discussion_coverage": "Index plus coordination, handoff, mechanism and masked-star threads read through public web snapshots; no new same-result overlap found. Not a complete or instantaneous archive of comments.", + "github_posting": "User connected GitHub; publication via applebees2 fork authorized", + "scope_status": "unchanged; independent corroboration, no novelty claim" + } +} diff --git a/research/ck-dyadic-forest-seed22/PROOF.md b/research/ck-dyadic-forest-seed22/PROOF.md new file mode 100644 index 0000000000..96b5364c3e --- /dev/null +++ b/research/ck-dyadic-forest-seed22/PROOF.md @@ -0,0 +1,166 @@ +# CK forests with arbitrary dyadic parent weights + +This is a source-specific scalar cost result, not an integer-multiplication +lower bound. The forest mechanism and signed-unit optimum are PR816's work. +The finite reduction and same-parent exchange method follow concurrent PR961 +on its different X4 matrix. The evidence here is an independently computed CK +census, corroborating Adam Gall's concurrent PR1220 discovered at final refresh. + +## Interface and complete price + +The pinned PR626 CK compensation is `(y,h) -> (y+C h,h)`. There are 112 +targets, 254 used helper columns and 8,704 nonzero entries. Every entry is +`a/4` with `a in {-4,-3,-2,-1,1,2,3,4}`. Source and target registers are +disjoint and all these operations and entrance frames are zero. These facts +are checked from the immutable canonical word and its selected historical SPEC. + +For nonzero reduced dyadic `q=n/2^d`, use the inherited independent binary +Horner price + +``` +H(q) = 3 + floor(log2 |n|) + popcount(|n|) + d; H(0)=0. +``` + +The three fixed operations are initial private-work clearing, signed target +accumulation and final clearing. Every source addition, numerator doubling +and denominator halving is charged. Each price is for one scalar component; +two real components of a complex register cost twice this number. PR816 +calls these component prices its complex-primitive bill. This note does not +substitute PR696's cheaper lowering, share work, or silently omit clears. + +For each nonroot target i, choose one parent j and nonzero dyadic lambda. +The directed parent graph must be a forest. Prepare `y_i -= lambda*y_j` in +leaf-before-parent order, so parents still carry their original target data. +The resulting matrix T has row `e_i-lambda*e_j`. Add `TC h`, then reverse +the preparation with negated coefficients. The exact endpoint is + +``` +T^-1 (T y + T C h) = y + C h. +``` + +This holds for arbitrary target and helper dirt; helpers are never changed in +the forward panel. T is unit triangular in a forest order. With +`R(v)=sum_k H(v_k)`, each root costs `R(C_i)` and each directed edge costs + +``` +E(i,j,lambda) = 2 H(lambda) + R(C_i-lambda*C_j). +``` + +Both preparation and restoration shears are paid. Descendants use the ORIGINAL +parent row C_j, even if that parent itself has a parent. There are no new +helpers, frame transitions, copied target registers or recursive children in +this class. Unchanged work outside the panel contributes the same bill to +every comparison. The result concerns this fixed scalar price, not a fresh +global compiler invoice or admission of an alternative recursive supplier. + +## Infinite tails reduce to 1,086 coefficients + +The original magnitude prices H(a/4), a=1,2,3,4, are 6,5,8,4; thus every +original coordinate costs at most eight. + +Let lambda=s*m/2^k be reduced, m positive odd and s a sign, with k>=4. +For a parent quarter numerator b!=0, the residual is + +``` +(a*2^k-s*m*b)/2^(k+2). +``` + +The numerator has 2-adic valuation v2(b)<=2, because its two summands have +distinct valuations; this also holds when a=0. It is nonzero and its reduced +denominator exponent is k+2-v2(b)>=4. Consequently its H-price is at least +4+4=8. When b=0 the original coordinate is unchanged. Summing coordinates +and adding both positive-cost shears gives E>R(C_i). + +For |lambda|>=68 and b!=0, + +``` +|(a-lambda*b)/4| >= (|lambda|-4)/4 >=16. +``` + +A reduced q=n/2^d with |q|>=16 has floor(log2|n|)>=d+4, and therefore +H(q)>=3+(d+4)+1+d>=8. Again coordinates with b=0 are unchanged, and E>root. + +Every remaining nonzero dyadic has denominator exponent at most three and +magnitude below 68. It therefore belongs to + +``` +Lambda = {n/8 : n=-543,...,-1,1,...,543}. +``` + +These arguments prove the two infinite-tail exclusions; no finite replay of +large coefficients is represented as a proof of an infinite domain. + +## CK-specific finite certificate + +For each ordered pair i!=j, define + +``` +B(i,j)=min(R(C_i), E(i,j,1), E(i,j,-1)). +``` + +The two implementations enumerate all 1,086 coefficients and 112*111=12,432 +ordered pairs: **13,501,152** exact edge prices, including **13,476,288** +nonunit comparisons. Histograms group equal quarter-numerator pairs; the +independent checker additionally identifies (a,b) with (-a,-b), which preserves +every sign-invariant H-price. All ordered cases are retained in the census +digest and multiplicities. +There is no stochastic cutoff or sampled pair subset. + +The minimum nonunit `E-B` is **63**, attained four times. One witness is +child 123, parent 125, lambda=-3: E=453 and B=390. The complete receipt records +the domain, extrema, multiplicities, exact digest and an attaining unit tree. + +**941 nonunit edges beat their root.** The minimum `E-root` is -116 at +child 114, parent 184, lambda=-3: E=353 versus root 469. Thus extending PR964's +power-of-two root-domination statement directly to all dyadics would be false. +The same-parent signed-unit alternative is essential. These are improving +edges relative to a root, not an improved complete forest or new supplier. + +The quarter alphabet by itself does not imply finite dominance: two repeated +coordinates C_i=3/4 and C_j=1/4 have root 16, unit prices 18 and 16, but +E(i,j,3)=12. This adverse control must exhibit a negative margin (-4). +It guards against a checker that assumes its intended negative result. + +## Forest exchange and the retained optimum + +Take any nonunit edge in any admissible dyadic forest. If outside Lambda, +delete it, making its child a root, which strictly reduces its price. If +inside Lambda, choose the minimizing alternative in B: either delete the +edge or keep the SAME child/parent relation with coefficient +1 or -1. +Topology remains acyclic. The descendant subtree remains attached, and all +other local costs are unchanged because they depend on original parent rows. +The replacement has its own valid leaf-before-parent schedule and reverse +restoration. Repeating strictly decreases cost until all edges are units. + +For signed units only, edge prices are symmetric, since +`C_j-s*C_i=-s*(C_i-s*C_j)` and H is sign invariant. The standard superroot +MST reduction then applies. The primary checker constructs a tree and checks +all 12,544 signed/root cycle inequalities. The independent checker uses Prim. +Both obtain **16,364 per scalar component**, or **32,728 real-component +primitives for the complex panel**. An existing signed-unit forest attains +this number, so the all-dyadic optimum is equal. Every optimizer in this +specific class has only signed-unit edges. The finite margin 63 is NOT claimed +as a uniform lower margin across the infinite tails. + +Do not run an undirected MST directly on nonunit edges: their prices need not +be orientation symmetric. The exchange argument removes them first. + +## Limits + +This result fixes the CK matrix, one-parent acyclic preparation, clearing after +every coefficient, original binary-Horner lowering and separate boundary +shears. It excludes neither multiple parents, arbitrary sequential target +bases, helper-basis changes, shared coefficient work, other lowerings nor +folding work into neighboring phases. It closes PR964's non-power-of-two +coefficient gap only under this fixed model. + +Logical inverse-transposition swaps target/source and negates each shear; +H is sign invariant, so the component bill is unchanged. It does not mean +transposing noninvertible private CLEAR instructions. The unchanged attaining +unit construction retains PR816's own scalar/precision checks; its independent +boundary verifier was replayed for this contribution. No new precision bound, +physical frame/phase replay, hosted supplier, global invoice, outer assembly, +or kappa certificate is issued. Inherited all-size/compiler, common-label and +mutable-source realization, whole-call hosting, precision/tape/recovery, +analytic transfer and bit H1-H5 obligations remain. This is not a formal +proof of the complete multiplication theorem or independent human review. diff --git a/research/ck-dyadic-forest-seed22/README.md b/research/ck-dyadic-forest-seed22/README.md new file mode 100644 index 0000000000..c454850311 --- /dev/null +++ b/research/ck-dyadic-forest-seed22/README.md @@ -0,0 +1,86 @@ +# Independent corroboration of the CK all-dyadic forest floor + +**Independent verification of a scoped negative result; no new kappa.** The historical CK +target-forest minimum remains **16,364 primitives per scalar component** when +each parent coefficient may be any nonzero dyadic, under the fixed independent +binary-Horner price and forest schedule. Both real components cost 32,728. + +This independently checks the gap explicitly left by PR964. +It uses PR961's all-dyadic reduction and same-parent exchange method on CK, +rather than claiming that method or PR816's original circuit savings as new. +The checked CK census is not a rerun of the X4 matrix. In particular **941 +nonunit edges beat a root**, but all are dominated by a signed-unit relation +to the same parent. The minimum nonunit margin against the best such +alternative is **63**, across **13,476,288** nonunit comparisons. + +Run from the repository root, offline with standard-library Python 3.10+: + +```sh +python -I -B research/ck-dyadic-forest-seed22/verify.py +python -I -O -B research/ck-dyadic-forest-seed22/test_package.py +``` + +The first command reconstructs the complete census and spanning-tree +certificate, invokes the separate integer checker and compares the frozen +receipt. Expected final marker: + +```text +PASS_CK_DYADIC_FOREST cases=13501152 minimum_margin=63 floor=16364 no_new_kappa +``` + +The [proof](PROOF.md) gives the complete bill, infinite-tail reduction and +scope. [RESULT.json](RESULT.json) contains the finite certificate; +[SOURCES.json](SOURCES.json) binds the two mathematical input files and source +heads. [CLAIM.md](CLAIM.md) records assignment seed22, three candidates, +overlap selection and stopping rule. [VALIDATION.md](VALIDATION.md) records +executed verification and unrun gates. This package does not alter the selected +frontier, which at the base is PR890 with conditional kappa +0.001661957774647029. + +Exact base: `007664306fff84fbb1c9a1b4053b69f439764034`. +At the final metadata refresh, main was +`dadfea6e8a78ff6ba901705f87532a71c6f5bbb8`, selecting PR1094 at conditional +kappa 0.001672660197076918. Both consumed CK inputs are byte-identical to the +base. This historical result neither depends on nor changes that selection. + +The final overlap refresh found **Adam Gall's concurrent +[PR1220](https://github.com/CrocSwap/integer-mult-bounds/pull/1220)** at +`9cd42fb94d2b74e7308ad783b20081aa85b868a1`, which already reports the same +mathematical result. No priority or additional coefficient-domain coverage is +claimed here. This package adds independently written scalar-arithmetic +checks without its 16/20-bit packed cost lanes, an independent full ordered +census digest, and a Windows/minimal-tree/recompression replay. PR1220's +pinned receipt agrees on the domain, extrema, witnesses and floor. No PR1220 +executable code was consumed; its receipt was inspected only after both +implementations here agreed. This is corroborating evidence that can be +reviewed alongside that PR, not a proposed replacement of its contribution. + +Credit **dd-hemant PR816** for the CK signed-unit forest and its attained +floor; **woklerx PR961** for the all-dyadic cutoff and exchange method on X4; +**Gareth Davidson (bitplane) PR964** for the CK power-weight exclusion and +**ToikY PR909** for earlier tail work; +**Ross Richardson PR932** for the X4 forest; **Oscar Fennell PR759** and +**Sricharan Vagvala PR749** for predecessor forest/restored-pair mechanisms. +Credit **Adam Gall PR1220** for the concurrent same-result contribution. +The CK supplier lineage includes **Jeremy Kothe**, **Chafik Boukhalfa**, +**icekylinx**, and the contributors retained in the source notices and +repository CONTRIBUTORS.md. Pending PR961/964 executable code is not imported. + +Prepared for **Lauren with substantial OpenAI Codex assistance** in research, +code, independent implementation, proof review and writing. Both checkers and +the review are AI-assisted; no independent human review is claimed. New files +are licensed under the repository's Apache-2.0 license. The inherited +all-size/compiler, realization, hosting, precision/tape, analytic and bit +interface assumptions remain; finite checking is not a full theorem proof. + +## Publication scope and open next questions + +Scope is **unchanged**: the historical CK matrix, all nonzero dyadic parent +weights and the declared one-parent forest cost model. Publication status is +independent corroboration after the PR1220 overlap was identified. Assignment +seed22 predates the current task-card workflow; no reassignment is claimed. + +**Open next questions: none justified by this corroboration.** It supplies +independent evidence for the existing scoped result, without a new mechanism +that would justify reopening the closed coefficient search. The exclusions +listed above remain scope limits, not proposed investigations. diff --git a/research/ck-dyadic-forest-seed22/RESULT.json b/research/ck-dyadic-forest-seed22/RESULT.json new file mode 100644 index 0000000000..6a44c683f5 --- /dev/null +++ b/research/ck-dyadic-forest-seed22/RESULT.json @@ -0,0 +1,710 @@ +{ + "cases": 13501152, + "census_sha256": "8419c238a791375dd846ba7558aeea9185af8b776f148731c377ad21fe311e6d", + "coefficients": 1086, + "minimum_margin_count": 4, + "minimum_nonunit_margin": 63, + "minimum_root_margin": -116, + "minimum_witness": { + "alternative": 390, + "child": 123, + "cost": 453, + "lambda": "-3", + "parent": 125 + }, + "nonunit_beats_alternative": 0, + "nonunit_beats_root": 941, + "nonunit_cases": 13476288, + "nonunit_ties_alternative": 0, + "ordered_pairs": 12432, + "original_panel_cost": 49624, + "pair_histograms": 8275, + "root_witness": { + "child": 114, + "cost": 353, + "lambda": "-3", + "parent": 184, + "root": 469 + }, + "source_columns": 254, + "targets": 112, + "unit_tree": { + "cost": 16364, + "cycle_inequalities": 12544, + "edges": [ + [ + 8, + 5, + 68, + 1 + ], + [ + 8, + 2, + 72, + 1 + ], + [ + 8, + 48, + 98, + 1 + ], + [ + 8, + 54, + 101, + 1 + ], + [ + 8, + 21, + 36, + 1 + ], + [ + 8, + 12, + 100, + 1 + ], + [ + 8, + 14, + 15, + 1 + ], + [ + 8, + 0, + 76, + 1 + ], + [ + 8, + 34, + 49, + 1 + ], + [ + 8, + 70, + 71, + 1 + ], + [ + 8, + 67, + 80, + 1 + ], + [ + 8, + 73, + 83, + 1 + ], + [ + 8, + 13, + 78, + 1 + ], + [ + 8, + 6, + 82, + 1 + ], + [ + 18, + 26, + 88, + 1 + ], + [ + 18, + 7, + 87, + 1 + ], + [ + 18, + 29, + 74, + 1 + ], + [ + 18, + 28, + 75, + 1 + ], + [ + 18, + 1, + 86, + 1 + ], + [ + 18, + 9, + 89, + 1 + ], + [ + 18, + 25, + 79, + 1 + ], + [ + 18, + 110, + 111, + 1 + ], + [ + 18, + 10, + 90, + 1 + ], + [ + 18, + 60, + 84, + 1 + ], + [ + 18, + 52, + 105, + 1 + ], + [ + 18, + 51, + 104, + 1 + ], + [ + 18, + 44, + 99, + 1 + ], + [ + 18, + 27, + 81, + 1 + ], + [ + 18, + 53, + 106, + 1 + ], + [ + 18, + 46, + 47, + 1 + ], + [ + 18, + 4, + 65, + 1 + ], + [ + 18, + 3, + 66, + 1 + ], + [ + 18, + 69, + 97, + 1 + ], + [ + 18, + 11, + 91, + 1 + ], + [ + 22, + 23, + 33, + 1 + ], + [ + 22, + 50, + 109, + 1 + ], + [ + 22, + 35, + 85, + 1 + ], + [ + 22, + 24, + 32, + 1 + ], + [ + 22, + 31, + 77, + 1 + ], + [ + 22, + 19, + 102, + 1 + ], + [ + 22, + 38, + 56, + 1 + ], + [ + 22, + 39, + 55, + 1 + ], + [ + 28, + 16, + 43, + 1 + ], + [ + 28, + 41, + 42, + 1 + ], + [ + 28, + 61, + 94, + 1 + ], + [ + 28, + 57, + 92, + 1 + ], + [ + 28, + 62, + 63, + 1 + ], + [ + 28, + 20, + 37, + 1 + ], + [ + 30, + 22, + 108, + 1 + ], + [ + 30, + 64, + 96, + 1 + ], + [ + 30, + 18, + 40, + 1 + ], + [ + 30, + 30, + 59, + 1 + ], + [ + 30, + 17, + 103, + 1 + ], + [ + 30, + 45, + 107, + 1 + ], + [ + 30, + 8, + 95, + 1 + ], + [ + 30, + 58, + 93, + 1 + ], + [ + 151, + 22, + 33, + 1 + ], + [ + 177, + 85, + 107, + 1 + ], + [ + 178, + 4, + 68, + -1 + ], + [ + 178, + 9, + 72, + 1 + ], + [ + 180, + 14, + 106, + -1 + ], + [ + 182, + 67, + 88, + -1 + ], + [ + 185, + 13, + 104, + -1 + ], + [ + 190, + 77, + 100, + -1 + ], + [ + 195, + 39, + 101, + 1 + ], + [ + 196, + 4, + 64, + 1 + ], + [ + 197, + 73, + 74, + -1 + ], + [ + 200, + 88, + 95, + 1 + ], + [ + 203, + 40, + 55, + 1 + ], + [ + 205, + 17, + 31, + 1 + ], + [ + 210, + 6, + 28, + -1 + ], + [ + 220, + 24, + 48, + -1 + ], + [ + 222, + 24, + 107, + -1 + ], + [ + 223, + 33, + 49, + -1 + ], + [ + 223, + 1, + 6, + -1 + ], + [ + 229, + 30, + 74, + 1 + ], + [ + 240, + 19, + 54, + -1 + ], + [ + 242, + 58, + 82, + -1 + ], + [ + 244, + 38, + 100, + -1 + ], + [ + 249, + 36, + 110, + -1 + ], + [ + 254, + 68, + 97, + -1 + ], + [ + 254, + 60, + 83, + -1 + ], + [ + 259, + 66, + 67, + -1 + ], + [ + 264, + 33, + 109, + -1 + ], + [ + 265, + 11, + 71, + -1 + ], + [ + 266, + 44, + 104, + 1 + ], + [ + 268, + 0, + 92, + 1 + ], + [ + 275, + 16, + 51, + 1 + ], + [ + 280, + 62, + 71, + 1 + ], + [ + 286, + 10, + 11, + 1 + ], + [ + 302, + 7, + 81, + 1 + ], + [ + 306, + 9, + 79, + 1 + ], + [ + 308, + 72, + 94, + 1 + ], + [ + 323, + 74, + 107, + 1 + ], + [ + 324, + 55, + 88, + -1 + ], + [ + 327, + 81, + 110, + -1 + ], + [ + 330, + 4, + 31, + 1 + ], + [ + 330, + 42, + 53, + 1 + ], + [ + 330, + 105, + 106, + 1 + ], + [ + 332, + 22, + 28, + -1 + ], + [ + 336, + 70, + 104, + 1 + ], + [ + 337, + 76, + 81, + -1 + ], + [ + 338, + 46, + 110, + 1 + ], + [ + 346, + 36, + 37, + 1 + ], + [ + 361, + 9, + 106, + 1 + ], + [ + 378, + -1, + 33, + 0 + ], + [ + 380, + -1, + 4, + 0 + ], + [ + 384, + -1, + 55, + 0 + ], + [ + 385, + -1, + 104, + 0 + ], + [ + 385, + -1, + 74, + 0 + ], + [ + 431, + 0, + 72, + 1 + ], + [ + 445, + -1, + 76, + 0 + ] + ], + "minimum_cycle_slack": 0 + } +} diff --git a/research/ck-dyadic-forest-seed22/SOURCES.json b/research/ck-dyadic-forest-seed22/SOURCES.json new file mode 100644 index 0000000000..a29716895b --- /dev/null +++ b/research/ck-dyadic-forest-seed22/SOURCES.json @@ -0,0 +1,43 @@ +{ + "base_commit": "007664306fff84fbb1c9a1b4053b69f439764034", + "spec_path": "research/complex-k492-owner-repair/data/SPEC.json", + "files": { + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/CANONICAL-WORD.json.gz": { + "encoding": "gzip-payload", + "sha256": "9bbc75dede090cfd7a0a0252424ea9d9f6211e2350d2a801d4e4f2f0784167c7" + }, + "research/complex-k492-owner-repair/data/SPEC.json": { + "encoding": "bytes", + "sha256": "2a2577ac526535826fed9d5f7f83f6e2e0ec058a146c64f7286720b995fa2323" + } + }, + "source_heads": { + "PR626": "660de893d27bb7abd1d5b01b1640207528a5c851", + "PR816": "133735a2cc2319c12ba5d786214b2217e083e7da", + "PR961": "4257ddf4b755cd0ac3bd3b0f6281cc5b2b1f72ad", + "PR964": "7a3bf8460cf6ca16a2bf008ff51fdb06df1af938", + "PR1220": "9cd42fb94d2b74e7308ad783b20081aa85b868a1" + }, + "related_sources": { + "PR816": { + "author": "dd-hemant", + "role": "CK forest mechanism and original floor" + }, + "PR961": { + "author": "woklerx", + "role": "all-dyadic cutoff and forest exchange on X4; mathematical method reused" + }, + "PR964": { + "author": "Gareth Davidson (bitplane)", + "role": "CK signed-power exclusion; non-power gap addressed here" + }, + "PR909": { + "author": "ToikY", + "role": "prior quarter-grid tail method" + }, + "PR1220": { + "author": "Adam Gall (adamgall)", + "role": "Concurrent same result; receipt inspected after this independent implementation; no executable dependency" + } + } +} diff --git a/research/ck-dyadic-forest-seed22/VALIDATION.md b/research/ck-dyadic-forest-seed22/VALIDATION.md new file mode 100644 index 0000000000..a12a6e6fb8 --- /dev/null +++ b/research/ck-dyadic-forest-seed22/VALIDATION.md @@ -0,0 +1,64 @@ +# Verification and scope + +Environment: Windows, CPython 3.12.10, Python standard library only. +Starting base: `007664306fff84fbb1c9a1b4053b69f439764034`. +Final upstream refresh: `dadfea6e8a78ff6ba901705f87532a71c6f5bbb8`. +No existing repository file, generator, selected certificate or upstream input +is modified. Only this research package is added. + +Executed: + +* `python -I -O -B research/ck-dyadic-forest-seed22/verify.py`: + both implementations complete all 13,501,152 finite-core prices and agree on + the full ordered census SHA256 + `8419c238a791375dd846ba7558aeea9185af8b776f148731c377ad21fe311e6d`. + The nonunit minimum is 63; 941 edges beat their root, but none beats or ties + its best root/same-parent signed-unit alternative. Independent Kruskal and + Prim yield 16364 and both check all 12,544 cycle inequalities. +* `python -I -O -B research/ck-dyadic-forest-seed22/test_package.py`: + nine focused tests pass. They cover exact price/sign/reduction, arbitrary + target/source/private-work columns, deletion of each primitive from a + nontrivial lowering, source corruption, equivalent gzip recompression, + strict certificate number types, synthetic nonunit improvements, the + actual CK root-only counterexample and diagnostic tail boundary cases. + The independent checker also executes 5,512 literal Horner coefficient + atoms, rejects five arithmetic mutations and checks synthetic improvements + for both coefficient signs. +* `python -I -B research/complex-ck-target-forest/independent.py`: + `PASS_CK_FOREST_INDEPENDENT floor=16364 active_columns=366 + untouched_columns=350 orientations=2`. This rechecks the inherited attaining + forest's scalar boundary; it is distinct from the new cost census. +* `python scripts/verify_selected_result.py` (the selected-record-check + Make target's Python command): the base's original selected PR890 record + passes with exact kappa 1661957774647029/10^18. +* The source-file diff against refreshed main is empty for both consumed files. +* Full primary and independent replay passed in a minimal directory with spaces, + no Git metadata and only the package plus its two pinned inputs. The input + gzip was recompressed at a different compression level and timestamp. The + replay took 64.482 seconds in this environment; this is an execution receipt, + not a controlled benchmark or speedup claim. +* Final refreshed metadata revealed concurrent PR1220. Its pinned receipt + matches the domain, nonunit count, minimum 63 (child 123, parent 125, lambda=-3), root + margin -116 (child 114, parent 184, lambda=-3), 941 root improvements and floor 16364. + This package's code was completed before inspecting that receipt, and + uses no packed cost lanes. Its final status is independent corroboration. + +The independent implementation does not import the primary checker or any +predecessor executable. It parses the source separately, uses literal Horner +arithmetic and a sign-normalized histogram census, and computes the unit +floor using Prim instead of Kruskal. It shares the deliberately specified +mathematical model and domain. Independent implementations and AI proof/code +review are not independent human review. + +The finite receipt contains the complete tree, source-specific extrema, +multiplicities and a digest of every ordered edge price. The all-dyadic +statement additionally relies on the written tail and forest-exchange proof; +the finite command alone is not an infinite-domain formal proof. + +Full `make verify`, selected cold replay, physical frame/phase replay, global +supplier adoption/invoice/assembly, remote CI and Lean were not run. The broad +Make suite regenerates unrelated historical artifacts; this additive research +note changes none of their generators or construction inputs. The relevant +local certificate, independent boundary and selected-record checks above were +run instead. All inherited all-size/compiler, realization, hosting, +precision/tape, analytic and bit H1-H5 obligations remain. diff --git a/research/ck-dyadic-forest-seed22/independent.py b/research/ck-dyadic-forest-seed22/independent.py new file mode 100644 index 0000000000..a005f5c7be --- /dev/null +++ b/research/ck-dyadic-forest-seed22/independent.py @@ -0,0 +1,390 @@ +#!/usr/bin/env python3 +"""Independent exact census of the pinned CK single-parent compensation edges. + +Lauren, with substantial OpenAI Codex assistance. + +This program imports no other research checker. It reads the original compressed +word, builds its own matrix, literally counts Horner operations, enumerates the +finite n/8 candidate domain, and obtains the signed-unit floor using Prim's +algorithm and the full cycle criterion. Extending the finite census to every +dyadic coefficient requires the analytic bounds in the accompanying proof. +Only the Python standard library is needed. Run from any working directory. +""" + +from __future__ import annotations + +import gzip +import hashlib +import json +from collections import Counter, defaultdict +from fractions import Fraction +from functools import cache +from pathlib import Path + + +WORD = (Path(__file__).resolve().parents[2] / + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/" + "CANONICAL-WORD.json.gz") +WORD_PAYLOAD_SHA256 = "9bbc75dede090cfd7a0a0252424ea9d9f6211e2350d2a801d4e4f2f0784167c7" +TARGETS = tuple(range(112, 224)) +NUMERATORS = tuple(range(-543, 0)) + tuple(range(1, 544)) + + +def require(condition, message): + """Checks remain active under python -O.""" + if not condition: + raise ValueError(message) + + +@cache +def horner(numerator: int, exponent: int) -> tuple[int, Fraction]: + """Return literal primitive count and the accumulated source coefficient. + + One clear, binary doublings/additions, halvings, one signed accumulation, + and the final clear are charged. The work register is represented by its + exact coefficient on the unchanged source. Its arbitrary initial value + disappears at the first clear. A zero macro emits nothing. + """ + require(exponent >= 0, "negative denominator exponent") + if numerator == 0: + return 0, Fraction(0) + sign = -1 if numerator < 0 else 1 + magnitude = abs(numerator) + while exponent and magnitude % 2 == 0: + magnitude //= 2 + exponent -= 1 + digits = [] + unprocessed = magnitude + while unprocessed: + unprocessed, bit = divmod(unprocessed, 2) + digits.append(bit) + operations = 1 # work <- 0 + work = Fraction(0) + for position, bit in enumerate(reversed(digits)): + if position: + work += work + operations += 1 + if bit: + work += 1 # unchanged source has formal coefficient one + operations += 1 + for _ in range(exponent): + work /= 2 + operations += 1 + accumulated = sign * work # target <- target +/- work + operations += 1 + work = Fraction(0) + operations += 1 + require(work == 0, "private work not cleared") + return operations, accumulated + + +def h(numerator: int, exponent: int) -> int: + return horner(numerator, exponent)[0] + + +def closed_price(value: Fraction) -> int: + """Separate reduced-Fraction/bit-count oracle, used only for controls.""" + if value == 0: + return 0 + denominator = value.denominator + require(denominator & (denominator - 1) == 0, "non-dyadic value") + n = abs(value.numerator) + return 3 + n.bit_length() - 1 + n.bit_count() + denominator.bit_length() - 1 + + +def check_macro_claim(numerator, exponent, claimed_count, claimed_coefficient): + count, coefficient = horner(numerator, exponent) + require(count == claimed_count, "incorrect primitive count") + require(coefficient == claimed_coefficient, "incorrect accumulated coefficient") + + +def rejected(label, operation): + try: + operation() + except ValueError: + return label + raise ValueError("negative control was accepted: " + label) + + +def arithmetic_controls(): + # Every possible residual coefficient (8*a - n*b)/32, plus every shear. + # This interval deliberately includes unused atoms, avoiding a shared + # assumption about which histogram entries happen to occur. + checked = set((n, 5) for n in range(-2204, 2205)) + checked.update((n, 3) for n in NUMERATORS) + checked.update((n, 2) for n in range(-8, 9)) + for n, exponent in checked: + value = Fraction(n, 1 << exponent) + count, coefficient = horner(n, exponent) + require(count == closed_price(value), "Horner/formula price disagreement") + require(coefficient == value, "Horner coefficient disagreement") + failures = [ + rejected("unreduced 6/8 price", lambda: check_macro_claim(6, 3, 10, Fraction(3, 4))), + rejected("omitted closing clear", lambda: check_macro_claim(3, 3, 8, Fraction(3, 8))), + rejected("wrong accumulation sign", lambda: check_macro_claim(3, 3, 9, Fraction(-3, 8))), + rejected("wrong halving exponent", lambda: check_macro_claim(3, 3, 9, Fraction(3, 4))), + rejected("non-dyadic denominator", lambda: closed_price(Fraction(1, 3))), + ] + return {"exact_macro_atoms_checked": len(checked), "rejected_mutations": failures} + + +def load_matrix(): + compressed = WORD.read_bytes() + payload = gzip.decompress(compressed) + digest = hashlib.sha256(payload).hexdigest() + require(digest == WORD_PAYLOAD_SHA256, "pinned decompressed word digest mismatch") + word = json.loads(payload) + panel = word["compensation"] + require(len(panel) == 8704, "unexpected compensation gate count") + sparse = {target: {} for target in TARGETS} + alphabet = set() + for row in panel: + require(isinstance(row, list) and len(row) == 6, "malformed compensation gate") + operation, target, source, numerator, denominator, frame = row + require(all(type(x) is int for x in row[1:]), "noninteger gate field") + require(operation == "add" and frame == 0, "unexpected operation or frame") + require(target in sparse and 224 <= source < 716, "target/source interface mismatch") + require(word["start"][target] == word["start"][source] == 0, "nonzero entrance frame") + require(denominator > 0, "nonpositive denominator") + coefficient = Fraction(numerator, denominator) * 4 + require(coefficient.denominator == 1, "coefficient not an integer quarter") + require(coefficient != 0 and abs(coefficient) <= 4, "coefficient outside certified alphabet") + require(source not in sparse[target], "duplicate target/source gate") + sparse[target][source] = int(coefficient) + alphabet.add(int(coefficient)) + require(all(sparse.values()), "missing target row") + require(alphabet == {-4, -3, -2, -1, 1, 2, 3, 4}, "unexpected coefficient alphabet") + sources = sorted({source for row in sparse.values() for source in row}) + require(len(sources) == 254, "unexpected source count") + matrix = tuple(tuple(sparse[t].get(s, 0) for s in sources) for t in TARGETS) + encoded = json.dumps({"targets": TARGETS, "sources": sources, "quarter_rows": matrix}, + sort_keys=True, separators=(",", ":")).encode() + metadata = {"decompressed_word_sha256": digest, + "matrix_sha256": hashlib.sha256(encoded).hexdigest(), + "target_count": len(matrix), "source_count": len(sources), + "nonzero_entries": len(panel), "quarter_numerator_alphabet": sorted(alphabet)} + return matrix, metadata + + +def edge_price(left, right, numerator): + return 2 * h(numerator, 3) + sum(h(8 * a - numerator * b, 5) + for a, b in zip(left, right)) + + +def synthetic_controls(): + results = [] + for sign in (1, -1): + left = (3, 3, 3, 3) # four coefficients of 3/4 + right = (sign, sign, sign, sign) + baseline = min(sum(h(a, 2) for a in left), edge_price(left, right, 8), + edge_price(left, right, -8)) + winning_numerator = 24 * sign + exact = edge_price(left, right, winning_numerator) + candidates = [(edge_price(left, right, n), n) for n in NUMERATORS] + optimum = min(price for price, _ in candidates) + minimizers = [str(Fraction(n, 8)) for price, n in candidates if price == optimum] + require(baseline == 24 and exact == 12 and optimum == 12, + "synthetic non-unit improvement not detected") + require(str(3 * sign) in minimizers, "synthetic lambda=3 minimizer missing") + results.append({"left_quarters": list(left), "right_quarters": list(right), + "signed_or_root_baseline": baseline, "best_cost": optimum, + "minimizing_lambdas": minimizers, "improvement": baseline - optimum}) + return results + + +def histogram_census(matrix): + # H is sign symmetric, so (a,b) and (-a,-b) have identical contribution + # for every lambda. No interchange of parent and child is performed. + letters = tuple((a, b) for a in range(5) for b in range(-4, 5) + if a > 0 or b > 0) + index = {letter: i for i, letter in enumerate(letters)} + groups = defaultdict(list) + for child, left in enumerate(matrix): + for parent, right in enumerate(matrix): + if child == parent: + continue + histogram = Counter() + for a, b in zip(left, right): + if a == b == 0: + continue + if a < 0 or (a == 0 and b < 0): + a, b = -a, -b + histogram[index[a, b]] += 1 + groups[tuple(sorted(histogram.items()))].append((child + 112, parent + 112)) + records = [] + for signature, pairs in groups.items(): + root = sum(count * h(letters[code][0], 2) for code, count in signature) + plus = 8 + sum(count * h(letters[code][0] - letters[code][1], 2) + for code, count in signature) + minus = 8 + sum(count * h(letters[code][0] + letters[code][1], 2) + for code, count in signature) + baseline = min(root, plus, minus) + # A direct dense-row Fraction oracle checks each distinct histogram's + # baseline, independently of its sign normalization and atom indexing. + child, parent = pairs[0] + left, right = matrix[child - 112], matrix[parent - 112] + oracle_root = sum(closed_price(Fraction(a, 4)) for a in left) + oracle_plus = 8 + sum(closed_price(Fraction(a - b, 4)) for a, b in zip(left, right)) + oracle_minus = 8 + sum(closed_price(Fraction(a + b, 4)) for a, b in zip(left, right)) + require((root, plus, minus) == (oracle_root, oracle_plus, oracle_minus), + "histogram/dense signed-unit baseline disagreement") + positions = tuple((child - 112) * 111 + (parent - 112) - int(parent > child) + for child, parent in pairs) + records.append((signature, len(pairs), pairs[0], baseline, root, positions)) + ordered_pairs = sum(record[1] for record in records) + require(ordered_pairs == 112 * 111, "ordered-pair coverage mismatch") + + minimum = None + witness = None + ties = 0 + improving = 0 + equal = 0 + root_improvements = 0 + root_minimum = None + by_denominator = {} + minima_digest = hashlib.sha256() + full_census_digest = hashlib.sha256() + evaluated = 0 + for numerator in NUMERATORS: + atom_costs = [h(8 * a - numerator * b, 5) for a, b in letters] + basis = 2 * h(numerator, 3) + lambda_minimum = None + is_unit = abs(numerator) == 8 + reduced = Fraction(numerator, 8) + expanded_costs = [None] * ordered_pairs + exponent = reduced.denominator.bit_length() - 1 + if not is_unit and exponent not in by_denominator: + by_denominator[exponent] = {"lambda_count": 0, "comparison_count": 0, + "minimum_margin": None} + for signature, multiplicity, pair, baseline, root, positions in records: + cost = basis + sum(count * atom_costs[code] for code, count in signature) + for position in positions: + expanded_costs[position] = cost + margin = cost - baseline + evaluated += multiplicity + if lambda_minimum is None or margin < lambda_minimum: + lambda_minimum = margin + if is_unit: + require(margin >= 0, "unit edge below its own baseline") + continue + stat = by_denominator[exponent] + if stat["minimum_margin"] is None or margin < stat["minimum_margin"]: + stat["minimum_margin"] = margin + if margin < 0: + improving += multiplicity + if margin == 0: + equal += multiplicity + root_margin = cost - root + if root_minimum is None or root_margin < root_minimum: + root_minimum = root_margin + if root_margin < 0: + root_improvements += multiplicity + if minimum is None or margin < minimum: + minimum, ties = margin, multiplicity + witness = {"child": pair[0], "parent": pair[1], + "lambda": str(reduced), "lambda_numerator_over_8": numerator, + "edge_cost": cost, "baseline_cost": baseline} + elif margin == minimum: + ties += multiplicity + minima_digest.update(f"{numerator}:{lambda_minimum}\n".encode("ascii")) + require(all(cost is not None for cost in expanded_costs), "digest expansion omitted a pair") + full_census_digest.update((json.dumps([numerator, expanded_costs], sort_keys=True, + separators=(",", ":")) + "\n").encode("utf-8")) + if not is_unit: + by_denominator[exponent]["lambda_count"] += 1 + by_denominator[exponent]["comparison_count"] += ordered_pairs + require(evaluated == 1086 * 12432, "census comparison count mismatch") + require(sum(x["comparison_count"] for x in by_denominator.values()) == 1084 * 12432, + "non-unit comparison count mismatch") + # Re-evaluate the reported minimizing witness densely without histogram + # compression, so a wrong pair representative cannot silently pass. + require(edge_price(matrix[witness["child"] - 112], matrix[witness["parent"] - 112], + witness["lambda_numerator_over_8"]) == witness["edge_cost"], + "dense minimum-witness cost disagreement") + return {"ordered_pairs": ordered_pairs, "distinct_pair_histograms": len(records), + "lambdas": len(NUMERATORS), "cases": evaluated, + "nonunit_cases": 1084 * ordered_pairs, + "nonunit_improvements": improving, "nonunit_equalities": equal, + "nonunit_beats_alternative": improving, "nonunit_ties_alternative": equal, + "nonunit_beats_root": root_improvements, "minimum_root_margin": root_minimum, + "minimum_nonunit_margin": minimum, "minimum_margin_count": ties, + "minimum_witness": witness, + "by_reduced_denominator_exponent": by_denominator, + "lambda_minima_sha256": minima_digest.hexdigest(), + "full_census_sha256": full_census_digest.hexdigest()} + + +def signed_unit_prim(matrix): + count = len(matrix) + superroot = count + adjacency = [[None] * (count + 1) for _ in range(count + 1)] + all_edges = [] + for i, row in enumerate(matrix): + root_cost = sum(h(a, 2) for a in row) + adjacency[superroot][i] = adjacency[i][superroot] = root_cost + all_edges.append((superroot, i, root_cost)) + for j in range(i): + plus = 8 + sum(h(a - b, 2) for a, b in zip(row, matrix[j])) + minus = 8 + sum(h(a + b, 2) for a, b in zip(row, matrix[j])) + adjacency[i][j] = adjacency[j][i] = min(plus, minus) + all_edges.extend(((i, j, plus), (i, j, minus))) + require(len(all_edges) == 12544, "signed multigraph edge count mismatch") + used = set() + distances = [10**30] * (count + 1) + predecessors = [None] * (count + 1) + distances[superroot] = 0 + tree = [[] for _ in range(count + 1)] + total = 0 + while len(used) < count + 1: + vertex = min((i for i in range(count + 1) if i not in used), + key=lambda i: (distances[i], i)) + require(distances[vertex] < 10**30, "disconnected signed-unit graph") + total += distances[vertex] + parent = predecessors[vertex] + if parent is not None: + tree[parent].append((vertex, distances[vertex])) + tree[vertex].append((parent, distances[vertex])) + used.add(vertex) + for neighbor, weight in enumerate(adjacency[vertex]): + if neighbor not in used and weight is not None and weight < distances[neighbor]: + distances[neighbor] = weight + predecessors[neighbor] = vertex + max_on_path = [] + for start in range(count + 1): + maxima = [None] * (count + 1) + stack = [(start, -1, 0)] + while stack: + vertex, parent, path_maximum = stack.pop() + maxima[vertex] = path_maximum + stack.extend((neighbor, vertex, max(path_maximum, weight)) + for neighbor, weight in tree[vertex] if neighbor != parent) + require(all(weight is not None for weight in maxima), "Prim tree disconnected") + max_on_path.append(maxima) + for left, right, weight in all_edges: + require(weight >= max_on_path[left][right], "spanning-tree cycle criterion failed") + require(total == 16364, "independent signed-unit floor differs from 16364") + return {"complex_primitive_floor": total, "vertices": count + 1, + "multigraph_edges": len(all_edges), "cycle_inequalities_checked": len(all_edges), + "forest_components": len(tree[superroot]), + "target_edges": count - len(tree[superroot])} + + +def main(): + arithmetic = arithmetic_controls() + synthetic = synthetic_controls() + matrix, metadata = load_matrix() + prim = signed_unit_prim(matrix) + census = histogram_census(matrix) + result = {"attribution": "Lauren, with substantial OpenAI Codex assistance", + "scope": "independent finite dyadic single-parent edge census and signed-unit floor", + "matrix": metadata, "arithmetic_controls": arithmetic, + "synthetic_nonunit_improvements": synthetic, "signed_unit_prim": prim, + "census": census, + "finite_edge_dominance_verified": census["nonunit_improvements"] == 0, + "all_dyadic_extension": "requires the analytic bounds in the accompanying proof"} + print(json.dumps(result, indent=2, sort_keys=True)) + return 0 if result["finite_edge_dominance_verified"] else 1 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/ck-dyadic-forest-seed22/test_package.py b/research/ck-dyadic-forest-seed22/test_package.py new file mode 100644 index 0000000000..1999d08ba5 --- /dev/null +++ b/research/ck-dyadic-forest-seed22/test_package.py @@ -0,0 +1,92 @@ +"""Focused adverse controls; Lauren, substantial OpenAI Codex assistance.""" +import importlib.util +from pathlib import Path +import gzip +import json +import tempfile +import unittest +from fractions import Fraction as Q + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location("ck_dyadic_verify", HERE / "verify.py") +v = importlib.util.module_from_spec(spec) +spec.loader.exec_module(v) + + +class ExactControls(unittest.TestCase): + def test_prices(self): + self.assertEqual([v.price(Q(a, 4)) for a in range(5)], [0, 6, 5, 8, 4]) + for a in range(-100, 101): + for k in range(8): + self.assertEqual(v.price(Q(a, 2**k)), v.price(Q(-a, 2**k))) + with self.assertRaises(ValueError): + v.price(Q(1, 3)) + + def test_nonunit_can_win_on_other_data(self): + child, parent = [3] * 2, [1] * 2 + best = min(v.row_price(child), v.edge_price(child, parent, Q(1)), + v.edge_price(child, parent, Q(-1))) + self.assertEqual(v.edge_price(child, parent, Q(3)) - best, -4) + + def test_boundary_work_is_charged(self): + self.assertEqual(v.edge_price([3] * 8, [1] * 8, Q(3)), 12) + + def test_cost_matches_literal_horner(self): + for a in range(-35, 36): + for k in range(6): + q = Q(a, 2**k) + word = v.horner(q) + self.assertEqual(len(word), v.price(q)) + self.assertEqual(v.run_horner(word), (Q(1), q, Q(0))) + + def test_mutated_lowerings_rejected(self): + word = v.horner(Q(3, 4)) + wanted = (Q(1), Q(3, 4), Q(0)) + for i in range(len(word)): + try: + actual = v.run_horner(word[:i] + word[i+1:]) + except ValueError: + continue # Removing the final clear must fail the work check. + self.assertNotEqual(actual, wanted) + + def test_certificate_types(self): + self.assertFalse(v.exact_equal({"count": 1}, {"count": True})) + self.assertFalse(v.exact_equal({"count": 1}, {"count": 1.0})) + + def test_actual_ck_needs_same_parent_alternative(self): + rows, _ = v.source_rows() + child, parent = rows[114-112], rows[184-112] + cost = v.edge_price(child, parent, Q(-3)) + self.assertEqual((cost, v.row_price(child)), (353, 469)) + self.assertLess(min(v.edge_price(child, parent, Q(1)), + v.edge_price(child, parent, Q(-1))), cost) + + def test_source_corruption_and_recompression(self): + pins = json.loads((HERE / "SOURCES.json").read_text()) + with tempfile.TemporaryDirectory(prefix="ck dyadic ") as directory: + root = Path(directory) + for name in pins["files"]: + dest = root / name + dest.parent.mkdir(parents=True, exist_ok=True) + dest.write_bytes((v.ROOT / name).read_bytes()) + rows, _ = v.source_rows(root) + path = root / v.WORD + original = gzip.decompress(path.read_bytes()) + path.write_bytes(gzip.compress(original, compresslevel=1, mtime=123)) + self.assertEqual(v.source_rows(root)[0], rows) + altered = json.loads(original) + altered["compensation"][0][3] *= -1 + path.write_bytes(gzip.compress(json.dumps(altered).encode(), mtime=0)) + with self.assertRaisesRegex(ValueError, "source pin"): + v.source_rows(root) + + def test_written_tail_boundaries(self): + # Diagnostic boundary checks complement the universal written proof. + for a in range(-4, 5): + for b in range(-4, 5): + for q in (Q(1,16), Q(-1,16), Q(3,32), Q(-33,16), Q(68), Q(-68), Q(1025)): + self.assertGreaterEqual(v.price(Q(a,4)-q*Q(b,4)), v.price(Q(a,4))) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/ck-dyadic-forest-seed22/verify.py b/research/ck-dyadic-forest-seed22/verify.py new file mode 100644 index 0000000000..18fba1eab2 --- /dev/null +++ b/research/ck-dyadic-forest-seed22/verify.py @@ -0,0 +1,252 @@ +"""Exact CK dyadic edge census. Lauren, substantial OpenAI Codex assistance. + +Apache-2.0. New census implementation; cost model/forest mechanism credited +to PR816 and all-dyadic reduction/exchange argument credited to PR961. +""" +import argparse +from collections import Counter +from fractions import Fraction as Q +import gzip +import hashlib +import json +from pathlib import Path +import subprocess +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +WORD = "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/CANONICAL-WORD.json.gz" + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")) + + +def exact_equal(left, right): + return canonical(left) == canonical(right) + + +def price(q): + q = Q(q) + if not q: + return 0 + a, b = abs(q.numerator), q.denominator + need(b & (b - 1) == 0, "non-dyadic coefficient") + return 3 + a.bit_length() - 1 + a.bit_count() + b.bit_length() - 1 + + +def row_price(row): + return sum(price(Q(a, 4)) for a in row) + + +def edge_price(child, parent, coefficient): + return 2 * price(coefficient) + sum( + price(Q(a, 4) - coefficient * Q(b, 4)) for a, b in zip(child, parent)) + + +def horner(q): + q = Q(q) + if not q: + return [] + price(q) # validate domain + result = ["clear"] + for i, bit in enumerate(bin(abs(q.numerator))[2:]): + if i: + result.append("double") + if bit == "1": + result.append("source") + result += ["halve"] * (q.denominator.bit_length() - 1) + return result + ["target+" if q > 0 else "target-", "clear"] + + +def run_horner(word): + # Exact target row in independent (target, source, dirty work) columns. + work, target = [Q(0), Q(0), Q(1)], [Q(1), Q(0), Q(0)] + for step in word: + if step == "clear": + work = [Q(0)] * 3 + elif step == "source": + work[1] += 1 + elif step in ("double", "halve"): + work = [v * (2 if step == "double" else Q(1, 2)) for v in work] + elif step in ("target+", "target-"): + target = [a + (1 if step == "target+" else -1) * b for a, b in zip(target, work)] + else: + raise ValueError("unknown primitive") + # Include uncleared work in a separate check; q=0 emits no macro. + if word: + need(work == [0, 0, 0], "uncleared private work") + return tuple(target) + + +def source_rows(root=ROOT): + pins = json.loads((HERE / "SOURCES.json").read_text()) + for name, pin in pins["files"].items(): + raw = (root / name).read_bytes() + if pin["encoding"] == "gzip-payload": + raw = gzip.decompress(raw) + need(hashlib.sha256(raw).hexdigest() == pin["sha256"], "source pin: " + name) + word = json.loads(gzip.decompress((root / WORD).read_bytes())) + spec = json.loads((root / pins["spec_path"]).read_bytes())["providers"]["ck"] + need(hashlib.sha256(canonical(word).encode()).hexdigest() == + spec["artifact_semantic_sha256"]["CANONICAL-WORD.json.gz"], "SPEC word binding") + need((word["v"], word["R"], word["h"]) == (112, 492, 9), "geometry") + sparse = {i: {} for i in range(112, 224)} + for op, t, s, a, b, frame in word["compensation"]: + need(op == "add" and t in sparse and 224 <= s < 716 and frame == 0, + "panel interface") + need(word["start"][t] == word["start"][s] == 0, "panel entrance") + value = 4 * Q(a, b) + need(value.denominator == 1 and 0 < abs(value) <= 4, "quarter alphabet") + need(s not in sparse[t], "duplicate cell") + sparse[t][s] = int(value) + sources = sorted({s for row in sparse.values() for s in row}) + need(len(sources) == 254 and sum(map(len, sparse.values())) == 8704, "panel coverage") + return [[sparse[t].get(s, 0) for s in sources] for t in sparse], sources + + +def minimum_tree(rows, roots, unit_edges): + edges = [(roots[i], -1, i, 0) for i in range(len(rows))] + for (i, j), weights in unit_edges.items(): + if i < j: + edges += [(w, i, j, s) for s, w in zip((-1, 1), weights)] + parent = list(range(len(rows) + 1)) + + def find(a): + a += 1 + while a != parent[a]: + a = parent[a] + return a + + tree = [] + # Seed22 selects equal-price edges only; the mathematical domain is full. + key = lambda e: (e[0], hashlib.sha256(("22:" + canonical(e)).encode()).hexdigest()) + for edge in sorted(edges, key=key): + w, i, j, s = edge + a, b = find(i), find(j) + if a != b: + parent[a] = b + tree.append(edge) + need(len(tree) == len(rows), "spanning tree") + adjacency = {i: [] for i in range(-1, len(rows))} + for w, i, j, _ in tree: + adjacency[i].append((j, w)) + adjacency[j].append((i, w)) + maxima = {} + for start in adjacency: + pending = [(start, None, 0)] + for vertex, previous, maximum in pending: + maxima[start, vertex] = maximum + for nxt, w in adjacency[vertex]: + if nxt != previous: + pending.append((nxt, vertex, max(maximum, w))) + slacks = [w - maxima[i, j] for w, i, j, _ in edges] + need(min(slacks) >= 0, "MST cycle inequality") + return {"cost": sum(e[0] for e in tree), "edges": tree, + "cycle_inequalities": len(slacks), "minimum_cycle_slack": min(slacks)} + + +def census(rows): + roots = list(map(row_price, rows)) + pairs, signatures = [], {} + for i, child in enumerate(rows): + for j, parent in enumerate(rows): + if i == j: + continue + signature = tuple(sorted(Counter(zip(child, parent)).items())) + index = signatures.setdefault(signature, len(signatures)) + pairs.append((i, j, index)) + sigs = list(signatures) + units = {sign: [edge_price(rows[i], rows[j], Q(sign)) for i, j, _ in pairs] + for sign in (-1, 1)} + benchmarks = [min(roots[i], units[-1][k], units[1][k]) + for k, (i, j, _) in enumerate(pairs)] + minimum, root_minimum = None, None + minima_count = negative_root = nonunit_ties = nonunit_better = 0 + witness, root_witness = None, None + digest = hashlib.sha256() + coefficients_done = cases_done = nonunit_done = 0 + for n in [*range(-543, 0), *range(1, 544)]: + coefficients_done += 1 + cases_done += len(pairs) + coefficient = Q(n, 8) + table = {(a, b): price(Q(8*a - n*b, 32)) + for a in range(-4, 5) for b in range(-4, 5)} + edge_values = [2 * price(coefficient) + sum(count * table[cell] for cell, count in sig) + for sig in sigs] + values = [edge_values[k] for _, _, k in pairs] + digest.update((canonical([n, values]) + "\n").encode()) + if abs(n) == 8: + need(values == units[n//8], "unit comparison disagrees") + continue + nonunit_done += len(pairs) + for index, (i, j, signature) in enumerate(pairs): + cost = edge_values[signature] + gap, root_gap = cost - benchmarks[index], cost - roots[i] + if minimum is None or gap < minimum: + minimum, minima_count = gap, 1 + witness = {"child": i+112, "parent": j+112, "lambda": str(coefficient), + "cost": cost, "alternative": benchmarks[index]} + elif gap == minimum: + minima_count += 1 + if root_minimum is None or root_gap < root_minimum: + root_minimum = root_gap + root_witness = {"child": i+112, "parent": j+112, "lambda": str(coefficient), + "cost": cost, "root": roots[i]} + negative_root += root_gap < 0 + nonunit_ties += gap == 0 + nonunit_better += gap < 0 + unit_edges = {(i, j): (units[-1][k], units[1][k]) for k, (i, j, _) in enumerate(pairs)} + need(coefficients_done == 1086 and cases_done == 13501152 and nonunit_done == 13476288, + "incomplete coefficient/pair coverage") + return {"targets": len(rows), "ordered_pairs": len(pairs), "coefficients": coefficients_done, + "cases": cases_done, "nonunit_cases": nonunit_done, + "pair_histograms": len(sigs), "minimum_nonunit_margin": minimum, + "minimum_margin_count": minima_count, "minimum_witness": witness, + "minimum_root_margin": root_minimum, "root_witness": root_witness, + "nonunit_beats_root": negative_root, "nonunit_ties_alternative": nonunit_ties, + "nonunit_beats_alternative": nonunit_better, + "census_sha256": digest.hexdigest(), "original_panel_cost": sum(roots), + "unit_tree": minimum_tree(rows, roots, unit_edges)} + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--write", type=Path, help="create a new receipt, refusing overwrite") + parser.add_argument("--primary-only", action="store_true", help="omit separate checker") + args = parser.parse_args() + rows, sources = source_rows() + result = census(rows) + result["source_columns"] = len(sources) + need(result["minimum_nonunit_margin"] > 0, "nonunit domination failed: inspect census") + need(result["unit_tree"]["cost"] == 16364, "unit floor changed") + if not args.primary_only: + independent = subprocess.run([sys.executable, "-I", "-B", str(HERE / "independent.py")], + check=True, capture_output=True, text=True) + second = json.loads(independent.stdout) + for key in ("cases", "nonunit_cases", "ordered_pairs", "minimum_nonunit_margin", + "minimum_root_margin", "minimum_margin_count", "nonunit_beats_root", + "nonunit_beats_alternative", "nonunit_ties_alternative"): + need(exact_equal(result[key], second["census"][key]), "independent mismatch: " + key) + need(result["census_sha256"] == second["census"]["full_census_sha256"], + "independent full edge census mismatch") + need(result["unit_tree"]["cost"] == second["signed_unit_prim"]["complex_primitive_floor"], + "independent Prim mismatch") + print("PASS_INDEPENDENT_CK_CENSUS digest=" + result["census_sha256"]) + if args.write: + with args.write.open("x", encoding="utf-8") as out: + json.dump(result, out, indent=2, sort_keys=True) + out.write("\n") + else: + need(exact_equal(result, json.loads((HERE / "RESULT.json").read_text())), "receipt mismatch") + print("PASS_CK_DYADIC_FOREST cases=%s minimum_margin=%s floor=16364 no_new_kappa" % + (result["cases"], result["minimum_nonunit_margin"])) + + +if __name__ == "__main__": + main()