diff --git a/research/t74-variable-frame-cap/.gitattributes b/research/t74-variable-frame-cap/.gitattributes new file mode 100644 index 0000000000..2b2787377d --- /dev/null +++ b/research/t74-variable-frame-cap/.gitattributes @@ -0,0 +1 @@ +vendor/fine_moment.py -text diff --git a/research/t74-variable-frame-cap/DUAL.json b/research/t74-variable-frame-cap/DUAL.json new file mode 100644 index 0000000000..cf07b22e9b --- /dev/null +++ b/research/t74-variable-frame-cap/DUAL.json @@ -0,0 +1,31 @@ +{ + "threshold": "4243/2500000", + "widths": [ + 4, + 5, + 7, + 8, + 9 + ], + "bin_ranks": [ + 8, + 16, + 32, + 48 + ], + "width_dual": [ + "-912953363/100000000", + "-335891303/25000000", + "-388541511/50000000", + "-493841927/100000000", + "-1645319/781250" + ], + "bin_dual": [ + "246920463/50000000", + "987682853/100000000", + "987683353/50000000", + "1006577813/50000000" + ], + "nomination": "SciPy 1.18.1 HiGHS LP; rational values independently checked without an optimizer", + "scope": "The nine dual coefficients, not a claimed solver optimum, certify a lower bound for every fractional or integral bin-pattern fill." +} diff --git a/research/t74-variable-frame-cap/EXPECTED.json b/research/t74-variable-frame-cap/EXPECTED.json new file mode 100644 index 0000000000..eec79b7284 --- /dev/null +++ b/research/t74-variable-frame-cap/EXPECTED.json @@ -0,0 +1,384 @@ +{ + "bin_stock": { + "8": 49728, + "16": 33152, + "32": 33152, + "48": 33152 + }, + "controls": { + "complete_three_space_counts": [ + 1, + 7, + 7, + 1 + ], + "cyclic_assignments": 81, + "cyclic_optimum": 25, + "fixed_anchors_preserved": true, + "split_climb_saving_units": 1534483722264, + "unbalanced_node_preserved": true + }, + "dual_sha256": "d5505e857536fa8109ca1f4d1f41ba76deca9a7fe27e071f8d580f678bc723f5", + "helper_widths": { + "4": 33, + "5": 9, + "7": 38, + "8": 114, + "9": 240 + }, + "integer_costs": [ + 0, + 4734627351677, + 7934770981090, + 10556988031076, + 12804182756988, + 14772655725922, + 16519100331045, + 18080964209012, + 19484855097718, + 20750662625403 + ], + "margin": "824673665595638106669/70231305224192000000000000000", + "minimum_pattern_slack": "60005024013923739860491382274552557245618001163581785772535589428564005511804081/5997385676683747768337545036521762610124811339554600991447980089667668567654400000000", + "moment_lower": "70231306048865665595638106669/70231305224192000000000000000", + "packing_excess_lower": "35293674197651/50000000", + "rejected": [ + "undercharged invoice", + "singular logical transport", + "overstated dual" + ], + "schema": 1, + "sources": { + "sources": [ + { + "commit": "002304ef01c4416a127916169ae6d94c1bee052b", + "path": "inputs/base.json.gz", + "sha256": "93c32c9dc8ca18394b7f3afac2cb4fa8582a6cb77399441b5107b396e63ca0f9", + "upstream_path": "research/t74-joint-owner-hillclimb/words/base.json.gz" + }, + { + "commit": "002304ef01c4416a127916169ae6d94c1bee052b", + "path": "inputs/extra.json.gz", + "sha256": "aae6592eaa4cf8638f21d50c44d09d4f8a6bb079ddcf5e377711a10ee2ddb526", + "upstream_path": "research/t74-joint-owner-hillclimb/words/extra.json.gz" + }, + { + "commit": "b479fc5567bc09ab9185bffe89b62594f36d74e5", + "path": "inputs/plan.json.gz", + "sha256": "5acf889dcd38741677635372fa32313f3e27ecc03aa480125c3ce70027c6b763", + "uncompressed_sha256": "bf1abd33c8ba946371cae37e021747343ef6603a31297bcc962197cc23f535e2", + "upstream_path": "research/gmx-t74-borrow43/new/PLAN.json" + }, + { + "commit": "002304ef01c4416a127916169ae6d94c1bee052b", + "path": "vendor/fine_moment.py", + "sha256": "bdfc492be6a663b219d76beff444db14bd67bb53c7c8ec4086ab0f56e48323c0", + "upstream_path": "research/t74-joint-owner-hillclimb/vendor/fine_moment.py" + } + ] + }, + "threshold": "4243/2500000", + "total_rank_mass": 4816512, + "words": { + "base": { + "components": [ + { + "max_table_states": 2, + "minimum": 15291615382753, + "nodes": 1 + }, + { + "max_table_states": 2, + "minimum": 15291615382753, + "nodes": 1 + }, + { + "max_table_states": 2, + "minimum": 15291615382753, + "nodes": 1 + }, + { + "max_table_states": 2, + "minimum": 15291615382753, + "nodes": 1 + }, + { + "max_table_states": 2, + "minimum": 15291615382753, + "nodes": 1 + }, + { + "max_table_states": 2, + "minimum": 15291615382753, + "nodes": 1 + }, + { + "max_table_states": 2, + "minimum": 12669398332767, + "nodes": 1 + }, + { + "max_table_states": 2, + "minimum": 12669398332767, + "nodes": 1 + }, + { + "max_table_states": 4, + "minimum": 4734627351677, + "nodes": 2 + }, + { + "max_table_states": 400, + "minimum": 51216731027952, + "nodes": 4 + }, + { + "max_table_states": 400, + "minimum": 51216731027952, + "nodes": 4 + }, + { + "max_table_states": 400, + "minimum": 51216731027952, + "nodes": 4 + }, + { + "max_table_states": 400, + "minimum": 51216731027952, + "nodes": 4 + }, + { + "max_table_states": 400, + "minimum": 51216731027952, + "nodes": 4 + }, + { + "max_table_states": 400, + "minimum": 51216731027952, + "nodes": 4 + }, + { + "max_table_states": 400, + "minimum": 51216731027952, + "nodes": 4 + }, + { + "max_table_states": 20, + "minimum": 150391387557265, + "nodes": 8 + }, + { + "max_table_states": 20, + "minimum": 150391387557265, + "nodes": 8 + }, + { + "max_table_states": 64, + "minimum": 312740917681692, + "nodes": 21 + }, + { + "max_table_states": 64, + "minimum": 312740917681692, + "nodes": 21 + }, + { + "max_table_states": 64, + "minimum": 312740917681692, + "nodes": 21 + }, + { + "max_table_states": 64, + "minimum": 312740917681692, + "nodes": 21 + }, + { + "max_table_states": 64, + "minimum": 312740917681692, + "nodes": 21 + }, + { + "max_table_states": 128, + "minimum": 2301114962317097, + "nodes": 189 + }, + { + "max_table_states": 1953125, + "minimum": 8349259085809027, + "nodes": 770 + } + ], + "contracted_nodes": 1434, + "local_rank_mass": 5371, + "minimum_excess_units": 21868976198927591, + "reconstructed_profile": { + "1": 2335, + "2": 512, + "3": 426, + "4": 120, + "5": 38, + "8": 8 + }, + "scale": 1099511627776, + "source_profile": { + "1": 2335, + "2": 512, + "3": 426, + "4": 120, + "5": 38, + "8": 8 + }, + "variable_nodes": 1118 + }, + "extra": { + "components": [ + { + "max_table_states": 2, + "minimum": 15291615382753, + "nodes": 1 + }, + { + "max_table_states": 2, + "minimum": 15291615382753, + "nodes": 1 + }, + { + "max_table_states": 2, + "minimum": 15291615382753, + "nodes": 1 + }, + { + "max_table_states": 2, + "minimum": 15291615382753, + "nodes": 1 + }, + { + "max_table_states": 2, + "minimum": 15291615382753, + "nodes": 1 + }, + { + "max_table_states": 2, + "minimum": 15291615382753, + "nodes": 1 + }, + { + "max_table_states": 2, + "minimum": 12669398332767, + "nodes": 1 + }, + { + "max_table_states": 2, + "minimum": 12669398332767, + "nodes": 1 + }, + { + "max_table_states": 4, + "minimum": 4734627351677, + "nodes": 2 + }, + { + "max_table_states": 400, + "minimum": 51216731027952, + "nodes": 4 + }, + { + "max_table_states": 400, + "minimum": 51216731027952, + "nodes": 4 + }, + { + "max_table_states": 400, + "minimum": 51216731027952, + "nodes": 4 + }, + { + "max_table_states": 400, + "minimum": 51216731027952, + "nodes": 4 + }, + { + "max_table_states": 400, + "minimum": 51216731027952, + "nodes": 4 + }, + { + "max_table_states": 400, + "minimum": 51216731027952, + "nodes": 4 + }, + { + "max_table_states": 400, + "minimum": 51216731027952, + "nodes": 4 + }, + { + "max_table_states": 20, + "minimum": 150391387557265, + "nodes": 8 + }, + { + "max_table_states": 20, + "minimum": 150391387557265, + "nodes": 8 + }, + { + "max_table_states": 64, + "minimum": 312740917681692, + "nodes": 21 + }, + { + "max_table_states": 64, + "minimum": 312740917681692, + "nodes": 21 + }, + { + "max_table_states": 64, + "minimum": 312740917681692, + "nodes": 21 + }, + { + "max_table_states": 64, + "minimum": 312740917681692, + "nodes": 21 + }, + { + "max_table_states": 64, + "minimum": 312740917681692, + "nodes": 21 + }, + { + "max_table_states": 128, + "minimum": 2301114962317097, + "nodes": 189 + }, + { + "max_table_states": 1953125, + "minimum": 8349259085809027, + "nodes": 770 + } + ], + "contracted_nodes": 1434, + "local_rank_mass": 5371, + "minimum_excess_units": 21868976198927591, + "reconstructed_profile": { + "1": 2335, + "2": 512, + "3": 426, + "4": 120, + "5": 38, + "8": 8 + }, + "scale": 1099511627776, + "source_profile": { + "1": 2335, + "2": 512, + "3": 426, + "4": 120, + "5": 38, + "8": 8 + }, + "variable_nodes": 1118 + } + } +} diff --git a/research/t74-variable-frame-cap/INPUTS.json b/research/t74-variable-frame-cap/INPUTS.json new file mode 100644 index 0000000000..4ebceb3cae --- /dev/null +++ b/research/t74-variable-frame-cap/INPUTS.json @@ -0,0 +1,29 @@ +{ + "sources": [ + { + "path": "inputs/base.json.gz", + "upstream_path": "research/t74-joint-owner-hillclimb/words/base.json.gz", + "commit": "002304ef01c4416a127916169ae6d94c1bee052b", + "sha256": "93c32c9dc8ca18394b7f3afac2cb4fa8582a6cb77399441b5107b396e63ca0f9" + }, + { + "path": "inputs/extra.json.gz", + "upstream_path": "research/t74-joint-owner-hillclimb/words/extra.json.gz", + "commit": "002304ef01c4416a127916169ae6d94c1bee052b", + "sha256": "aae6592eaa4cf8638f21d50c44d09d4f8a6bb079ddcf5e377711a10ee2ddb526" + }, + { + "path": "inputs/plan.json.gz", + "upstream_path": "research/gmx-t74-borrow43/new/PLAN.json", + "commit": "b479fc5567bc09ab9185bffe89b62594f36d74e5", + "sha256": "5acf889dcd38741677635372fa32313f3e27ecc03aa480125c3ce70027c6b763", + "uncompressed_sha256": "bf1abd33c8ba946371cae37e021747343ef6603a31297bcc962197cc23f535e2" + }, + { + "path": "vendor/fine_moment.py", + "upstream_path": "research/t74-joint-owner-hillclimb/vendor/fine_moment.py", + "commit": "002304ef01c4416a127916169ae6d94c1bee052b", + "sha256": "bdfc492be6a663b219d76beff444db14bd67bb53c7c8ec4086ab0f56e48323c0" + } + ] +} diff --git a/research/t74-variable-frame-cap/NOTICE.md b/research/t74-variable-frame-cap/NOTICE.md new file mode 100644 index 0000000000..7c62b497b7 --- /dev/null +++ b/research/t74-variable-frame-cap/NOTICE.md @@ -0,0 +1,27 @@ +# Attribution and source notice + +New work: Jeremy Diviney, with substantial OpenAI Codex assistance, Apache-2.0. +Source commits, paths and byte hashes: INPUTS.json. + +The two word inputs are unchanged PR2322 words by Vlado Vojdanovski, building +on Jeremy Kothe's PR2312 width exchange, existing frame refits and helper-donor +kernels, Cinna Davis's PR2226 anticipatory borrowing, Rohan Arun's supplier and +ownership lineage and the predecessors credited in vendor/GENERATOR-NOTICE.txt. +The parent plan is Jeremy Kothe's PR2269 plan, compressed without changing its +original bytes. These sources are from CrocSwap/integer-mult-bounds under the +repository's Apache-2.0 contribution terms. + +vendor/fine_moment.py is copied without modification from PR2322. The verifier +sets lower runtime precision parameters while retaining the explicit outward +series and tail bounds. The original repository notice is preserved at +vendor/UPSTREAM-NOTICE, and the original generator/borrow lineage notice at +vendor/GENERATOR-NOTICE.txt. Those notices are source attribution, not statements +that every named upstream result is executed or admitted by this package. +The Apache-2.0 license is included at vendor/LICENSE for standalone exports. + +The literal frame-invoice traversal follows PR2322 generate_words.py:paid_profile, +reimplemented with explicit GF(2)^9 subsets. Subspace propagation, variable +elimination and weak LP duality are standard techniques, not claimed inventions. +Ali Romman/PR1129 and the incorporated R480 pattern-dual audit previously apply +the same packing-pattern domain to an older inventory. PR2360's cost-gate +implementation supplied the starting directed-price and source-export scaffold. diff --git a/research/t74-variable-frame-cap/README.md b/research/t74-variable-frame-cap/README.md new file mode 100644 index 0000000000..82d380e7ef --- /dev/null +++ b/research/t74-variable-frame-cap/README.md @@ -0,0 +1,234 @@ +# Variable-frame cap for the PR2322 T74 words + +**Exact scoped cost bound; no new κ.** The two borrowed words of +[PR2322](https://github.com/CrocSwap/integer-mult-bounds/pull/2322) cannot reach +primitive **b = 0.0016972**, even after jointly optimizing all their A, B, +restoration and rank-zero handoff frames and allowing arbitrary fractional +whole-helper packing into the unchanged T74 bin stock. Both source words are +identical as parsed JSON to those in +[PR2374](https://github.com/CrocSwap/integer-mult-bounds/pull/2374), head +`5449da65da12bdfd94675dccc38731eaa91e93b6`, whose conditional κ claim is +0.001697194950901770. That comparison was checked locally; this package does +not independently admit PR2374's complete supplier or outer theorem. + +This narrows one constructive question: **can a frame refit, including moving +the handoff charts, improve this fixed scalar/operator word substantially?** +The bound leaves less than 5.05e-9 above PR2374's primitive endpoint. It permits +repacking, so changing only its owner assignment does not escape the result. +Changing scalar gates, their order, logical handoff maps, helper endpoints or +the parent inventory remains outside the theorem. + +The concurrent [PR2402](https://github.com/CrocSwap/integer-mult-bounds/pull/2402) +by Sagar Thakrar, head `2e2cb4ffa2785e40f6e3443fec8765e4dade7cff`, gives the tighter +**b < 0.001697195759** packing cap when the local frames are fixed, and prices +hypothetical circuit moves. The new question answered here is whether changing +all permitted intermediate and transported handoff frames escapes that narrow +packing regime. This package's broader but slightly looser cap covers those +frame changes. PR2402 was read for overlap; its certificate is not replayed or +used in this proof. Earlier #1995/#2013 frame bounds concern the selected older +scalar word and cleanup contract; they do not bind these changed borrowed words. + +The computational contribution is a small exact min-sum elimination engine. +It resolves the complete finite frame-assignment relaxation in about one second +for both providers together on the author's machine. General CP-SAT searches +had left a lower-bound gap after minutes; those unsuccessful searches are not +used as proof. No claim of a new variable-elimination algorithm is made. + +## Fixed inputs and permitted changes + +`INPUTS.json` pins the two PR2322 words, the PR2269 T74 parent plan and the +inherited directed power engine. Prefix/precondition/compensation frames, cut +producer frames, target levels and all initial/final frames remain fixed. +The scalar A/B/restoration gate sequence, operands and coefficients remain fixed. +Every handoff keeps its role, chronological position and invertible binary map +G; its entry and exit subspaces may change jointly subject to **E = G(U)**. +The initial target response and exact scalar operators are not resynthesized. + +Every variable frame can be *any* binary subspace of GF(2)^9 satisfying the +literal monotonicity and transported-equality constraints. Domains are not +restricted to frames occurring in the input. A physically valid native refit +must satisfy these conditions; this proof may admit more possibilities, so it +needs no claim that every allowed assignment has a native implementation. + +Each source word has local profile +`{1:2335, 2:512, 3:426, 4:120, 5:38, 8:8}`, including COPY64, and local rank +mass 5371. Both have 434 helper widths +`{4:33, 5:9, 7:38, 8:114, 9:240}`, total 3515. The parent has 666 calls, +m = 73, W = 66304 and bins +`{8:49728, 16:33152, 32:33152, 48:33152}`. These counts are recounted from the +pinned words and plan. The cap permits any mixture of the two providers. + +## Why the finite frame computation is complete + +A node represents a scalar gate's common frame. Each role contributes an edge +from its previous frame to the gate's frame. Initial/final/cut nodes are fixed. +A handoff has two nodes with E = G(U), rather than a paid edge between them. +Ordinary edges require inclusion and charge the rank difference. Parallel edges +are retained with their multiplicity: two shared roles pay twice. + +For a variable node, propagate a lower subspace forward by span/join of incoming +bounds and an upper subspace backward by intersection of outgoing bounds. +Across a handoff use G forward and G^-1 backward. Induction in the chronological +DAG proves every feasible frame lies in its resulting interval [L,U]. +`domains.py` enumerates every subspace between them by generating all subspaces +of the quotient U/L. It checks the full GF(2)^3 lattice as a control; there are +1, 7, 7 and 1 subspaces in the respective dimensions. + +A lossless reduction simplifies the graph before enumeration. Let a free node +have equal incoming and outgoing multiplicity, and a single distinct predecessor +with frame P. Assign that node the frame P. It remains below every successor Q. +For each continued role, its two increments x and y become x+y. For +0 < p = 1-b < 1, + + c_x + c_y >= c_(x+y), c_r = (r/73)^p, c_0 = 0. + +Thus the change cannot increase true cost. The analogous assignment to a single +distinct successor is also valid. Fixed anchors and transport nodes are never +contracted. Repeating this operation preserves an optimum of the true objective; +it removes 1434 nodes for each provider. The final assignment is reconstructed +and checked against every edge and transport in the original graph. + +After bounds and contractions, each provider has 1118 variable nodes in 25 +components. Factor tables record every legal adjacent frame pair, its paid +cost, and every transport equality. Variable elimination sums all factors +containing one node and minimizes over *all* its possible frames, retaining the +result on its neighbors. Induction proves that this is exact minimization over +the eliminated variables. The largest table contains 1,953,125 entries; no +branch-and-bound solver or heuristic stopping criterion is involved. + +`eliminate.py` uses NumPy int64 arrays for these exact integer operations. +Invalid entries have saturated infinity 2^60; every addition is capped at that +value, and two such entries sum below int64's limit. A feasible complete cost is +checked to lie below infinity. A separate exhaustive 81-assignment cyclic +factor problem verifies elimination and reconstruction. A split-climb positive +control exercises an actual improving graph contraction; fixed anchors and +unbalanced incidences are preserved. + +## Directed prices and the cap + +Set b = 4243/2500000 = 0.0016972. Define + + f_b(r) = [73 (r/73)^(1-b) - r]/b, f_b(0) = 0. + +The immutable directed moment engine from PR2322 computes rational lower +bounds for every f_b(r), with explicit logarithm and exponential tail bounds. +Its runtime grid is 2^-256, with 100 logarithm and 96 exponential terms. +Each local table uses the **floor** of 2^40 times that lower bound. The +min-sum engine therefore proves a lower bound for the local excess, using +only integer operations. No floating-point result enters a proof comparison. +The floats printed on success are diagnostics only. + +Contraction is justified for the true concave costs, **not** for their rounded +versions: every original feasible assignment has a no-more-expensive contracted +assignment, whose true cost is at least the minimum rounded-down cost computed +on the contracted graph. This distinction avoids assuming that rounding +preserves subadditivity. + +The rounded optimum equals the source profile's rounded cost for each word. +This is not a claim of exact real-valued optimality: a gain below the rounding +resolution is left open. The cap below incorporates all downward rounding. +Rank mass remains exactly 5371 for every assignment because edge differences +telescope and transports preserve dimension; the eight fixed rank-eight cut +copies are separately included. + +Whole-helper packing uses the established PR1129/PR2360 relaxation. All 1163 +integer patterns for capacities 8,16,32,48 and widths 4,5,7,8,9 are enumerated. +The rational dual in `DUAL.json` is checked against directed lower costs, giving +an idle-excess lower bound D for every nonnegative fractional combination of +patterns with these helper and bin counts. It ignores chronology, family and +physical-port restrictions. Nine dual coefficients were nominated with SciPy +HiGHS; verification neither calls nor trusts an optimizer. + +Let L be the smaller certified local excess of the two providers. Total rank +mass is 4,816,512 = 73 × 66304 - 23680. For every permitted frame assignment, +provider mixture and packing, the recurrence moment satisfies + + M(b) >= [4,816,512 + b (666 L + D)] / (73 × 66304) > 1. + +The exact rational lower endpoint in `EXPECTED.json` exceeds 1 by approximately +**1.17422517347e-8**. Each positive child rank is less than 73, so every fixed +assignment's moment increases with b. The same lower bound at this b therefore +excludes every larger b as well. This proves **b < 0.0016972** for the stated +model. It establishes no new outer κ or unconditional multiplication theorem. + +## Reproduce + +Python 3.12 and NumPy 2.5.4; no network during replay. With those installed: + +```sh +python3 -I -O -B research/t74-variable-frame-cap/verify.py +python3 -I -B research/t74-variable-frame-cap/check_export.py +``` + +Expected: `PASS_T74_VARIABLE_FRAME_CAP 4243/2500000 ... max_table_states 1953125` +and `PASS_T74_VARIABLE_FRAME_EXPORT controls 8`. + +The repository's registered runner uses the exact dependency pin: + +```sh +python3 scripts/research_package.py --package research/t74-variable-frame-cap --check-only +python3.12 scripts/research_package.py --package research/t74-variable-frame-cap +``` + +`--record NEW_PATH` regenerates the complete receipt and refuses overwrite. +Normal verification writes nothing and compares every receipt field. Source +hashes, incorrect billing, singular transports, an overstated packing dual, +input/receipt tampering, optimized execution and standalone export are checked. +The original plan is gzip-compressed locally with its uncompressed upstream +hash retained. `.gitattributes` preserves the directed engine's original CRLFs. +The finite verifier needs no Git history; the repository metadata checker needs +history for `SOURCES.json`'s historical task/selected-result provenance. + +The arithmetic loader executes the exact source bytes checked against +`INPUTS.json`, without consulting Python bytecode caches. `-B` alone suppresses +cache writes but still permits cache reads. Four export controls install +conflicting timestamp or unchecked-hash caches and replay in both normal and +optimized mode; every run must retain the original receipt and leave the export +unchanged. This repairs the same source/cache distinction identified in the +related [PR2766](https://github.com/CrocSwap/integer-mult-bounds/pull/2766). +[PR2553](https://github.com/CrocSwap/integer-mult-bounds/pull/2553) isolates the +registered runner's cache namespace; this fix also covers direct verifier calls. +The arithmetic source, inputs, dual and expected mathematical receipt are unchanged. + +## Open next questions + +1. **Change a logical circuit choice, not just its frame.** The proof fixes the + scalar gates, ordering and G maps. A new kernel, different lender or retimed + preparation can escape it. First generate a valid changed word and run the + frame optimizer and whole-width cost check before native/global admission. + The blocker is an exact arbitrary-input construction with favorable total cost. + New words need their own source pins, fixed-point prices and bill: the small + elimination engine is reusable, while `verify.py` checks this pinned cap. +2. **Optimize a changed parent inventory.** Different capacity counts change + the dual constraint. First derive the parent's coverage and fully charged + costs, then rerun the packing bound. A hypothetical bin histogram is insufficient. +3. **Reuse the elimination engine on wider frame domains.** Larger changes may + create a large separator table. First inspect domain sizes and elimination + widths; seek a proved contraction or separator decomposition before raising + the memory cap. The current implementation deliberately rejects tables above + ten million states. + +## Credit and limits + +Jeremy Diviney, with substantial OpenAI Codex assistance: this source-bound +variable-frame relaxation, transported-domain computation, contraction and +exhaustive elimination implementation, exact cap and controls. The algorithms +of subspace propagation and min-sum variable elimination are standard; the +contribution is their checked application to these newer borrowed words. + +Cinna Davis/PR2226 supplies anticipatory dirty borrowing. Jeremy Kothe's +PR2269/2312/2374 and Rohan Arun's T74 lineage supply the parent, kernels, +existing frame refits and ownership. Vlado Vojdanovski/PR2322 supplies the +coherent handoff words, reference frame invoice and directed numerical engine. +WildIdeas' earlier refit work remains credited. Ali Romman/PR1129 and the +incorporated R480 pattern-dual audit supply the existing packing-relaxation +lineage; our PR2360 applied it to a different fixed 400-helper inventory. +PR2359 independently audits the original raw frame delta. Sagar Thakrar's +PR2339/2387 provides related low-alias construction and packing evidence; it is +not an input to this cap. Original notices are retained under `vendor/`. + +No local scalar/phase replay, complete physical owner admission, compiler, +stock/precision, all-size or outer theorem is newly certified. Such constraints +can only remove assignments or add costs inside the stated fixed model. The +selected frontier and predecessor packages are unchanged. No independent human +review is claimed. New work is Apache-2.0; see `NOTICE.md`. diff --git a/research/t74-variable-frame-cap/SOURCES.json b/research/t74-variable-frame-cap/SOURCES.json new file mode 100644 index 0000000000..392737aa2a --- /dev/null +++ b/research/t74-variable-frame-cap/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + } + ] +} diff --git a/research/t74-variable-frame-cap/TASK.json b/research/t74-variable-frame-cap/TASK.json new file mode 100644 index 0000000000..8ce1969fa2 --- /dev/null +++ b/research/t74-variable-frame-cap/TASK.json @@ -0,0 +1,125 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "starting_points": [ + "research/complex-local-word-ceiling/README.md", + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json", + "research/selected-k8-unrestricted-ends/README.md" + ], + "methods": [ + "Propose a changed helper inventory and derive an optimistic exact moment.", + "Design a small completed instance and independently verify its endpoint and rank bill." + ], + "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin.", + "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.", + "allowed_variations": [ + "Narrow to one changed boundary or helper type with explicit counts.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Mixing only providers already inside the pinned catalogue.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013." + ], + "overlap_terms": [ + "helper inventory", + "heterogeneous-owner", + "mutable leaver" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove a directed cap for every A/B/restoration frame and fixed-G handoff chart refit of the PR2322 words, combined with fractional whole-helper packing on the same T74 stock.", + "scope_change_reason": "New lender/early-restoration probes and source-alias count reductions did not improve the complete cost. The useful result is an exhaustive frame-optimization method and a cap on the newer fixed borrowed circuit, not a new helper inventory or the original construction acceptance gate.", + "bottleneck_link": "Determines whether frame and owner optimization can materially lift the leading borrowed circuit before investing in another full replay.", + "budget_minutes": 60, + "stop_rule": "Stop fixed-word frame search once complete finite-domain elimination and a directed packing dual establish a cap within 5.05e-9 of the observed primitive endpoint. Leave changes to gates, logical maps, endpoints and stock open.", + "outcome": "negative-result", + "evidence": "EXPECTED.json: exhaustive min-sum elimination on complete transported subspace domains; maximum table 1953125 entries; both words, exact downward prices and 1163 packing inequalities force b<0.0016972. Rejection, independent brute-force, contraction and export controls.", + "author": "Jeremy Diviney, with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance with research, implementation, proof and verification. NumPy2.5.4 performs exact bounded int64 table operations. SciPy1.18.1/HiGHS nominated rational packing prices; OR-Tools and heuristic searches were discovery-only and are not proof dependencies.", + "open_questions": [ + { + "question": "Can a changed scalar kernel, gate order or G map beat the cap?", + "why_it_matters": "Those circuit choices are fixed by this result.", + "first_step": "Build an exact changed word and run the frame and whole-width gates before native/global admission.", + "blocked_by": "A fully correct arbitrary-input changed circuit." + }, + { + "question": "Can a changed parent inventory fit the helper widths more cheaply?", + "why_it_matters": "The bin stock is a hypothesis of the cap.", + "first_step": "Derive valid changed coverage and costs, then rerun the pattern dual.", + "blocked_by": "A fully charged parent construction." + }, + { + "question": "Can the elimination engine handle wider frame domains?", + "why_it_matters": "Changed circuits may have much larger separators.", + "first_step": "Inspect the complete domain and separator sizes, then seek a lossless contraction.", + "blocked_by": "Memory growth of exact tables beyond the registered limit." + } + ], + "validation_environment": { + "python": "CPython3.12.3", + "platform": "Linux", + "numpy": "2.5.4", + "workers": 1, + "priority": "nice15/idle I/O" + }, + "predecessor_comparison": { + "pr": 2374, + "head": "5449da65da12bdfd94675dccc38731eaa91e93b6", + "result": "Both PR2374 new/borrow/words/BORROW-WORD-43{base,extra}.json.gz files equal the bundled PR2322 words as complete parsed JSON; author-side comparison, no full supplier replay." + }, + "upstream_refresh": { + "checked_at": "2026-10-15T07:41:48.497695+00:00", + "main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "decision": "Main, guidance and selected record unchanged. Retain scoped source pins; refresh comparison to PR2374 text-only new head." + }, + "overlap_review": { + "searched_at": "2026-10-15T07:29:53.965368+00:00", + "terms": [ + "frame optimality", + "handoff frames", + "variable elimination", + "2374" + ], + "coverage": { + "open_prs": { + "fetched_at": "2026-10-15T07:25:30.316797+00:00", + "complete_pagination": true, + "records": 602 + }, + "discussions": { + "fetched_at": "2026-10-15T07:29:53.882935+00:00", + "complete_pagination": true, + "records": 1129 + } + }, + "warnings": [], + "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "direct_followup": { + "checked_at": "2026-10-15T07:41:48.497695+00:00", + "pr2402": "2e2cb4ffa2785e40f6e3443fec8765e4dade7cff", + "distinction": "PR2402 prices fixed local words and gives a tighter owner-only cap. This package exhausts variable scalar and fixed-G handoff frames plus packing. No priority for the packing cap or standard variable-elimination algorithm is claimed.", + "pr2374": "5449da65da12bdfd94675dccc38731eaa91e93b6", + "pr2387": "20fb6953b0d2077c19e45f731ec587ebefb9a380", + "coordination": "Read-only PR/Discussion coverage; no new Discussion claim posted. Claims are not exhaustive novelty evidence." + } + } +} diff --git a/research/t74-variable-frame-cap/VERIFY.json b/research/t74-variable-frame-cap/VERIFY.json new file mode 100644 index 0000000000..9c03f0435d --- /dev/null +++ b/research/t74-variable-frame-cap/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [ + "numpy==2.5.4" + ], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete transported frame domains, lossless contractions, exact min-sum elimination, directed costs, whole-helper dual, positive and rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/check_export.py" + ], + "timeout_seconds": 120, + "checks": "Read-only standalone replay, immutable source and receipt tampering, no-clobber. Four source/bytecode binding controls: timestamp and unchecked-hash caches under normal and optimized Python." + } + ] +} diff --git a/research/t74-variable-frame-cap/check_export.py b/research/t74-variable-frame-cap/check_export.py new file mode 100644 index 0000000000..3a57388038 --- /dev/null +++ b/research/t74-variable-frame-cap/check_export.py @@ -0,0 +1,123 @@ +#!/usr/bin/env python3 +"""Verify source-only read-only replay, evidence binding and no-clobber.""" + +import importlib.util +import py_compile +import struct +import hashlib +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +ROOT = Path(__file__).resolve().parent + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def snapshot(root): + return { + str(p.relative_to(root)): hashlib.sha256(p.read_bytes()).hexdigest() + for p in root.rglob("*") + if p.is_file() + } + + +def replay(root, *args): + return subprocess.run( + [sys.executable, "-I", "-O", "-B", str(root / "verify.py"), *map(str, args)], + cwd=root.parent, + capture_output=True, + text=True, + timeout=30, + ) + + +def check_bytecode_caches(root): + """Cached code must not replace the authenticated arithmetic source.""" + source = root / 'vendor/fine_moment.py' + original = source.read_bytes() + stamp = source.stat() + cache_dir = source.parent / '__pycache__' + # This root is a new source-only export: no existing cache may be removed. + need(not cache_dir.exists(), 'unexpected cache in fresh export') + with tempfile.TemporaryDirectory(prefix='t74-cache-control-') as tmp: + wrong_source = Path(tmp) / 'wrong.py' + wrong_source.write_text("raise RuntimeError('UNAUTHENTICATED_BYTECODE_EXECUTED')\n") + for mode in (py_compile.PycInvalidationMode.TIMESTAMP, + py_compile.PycInvalidationMode.UNCHECKED_HASH): + for optimized in (False, True): + cache = Path(importlib.util.cache_from_source( + str(source), optimization='1' if optimized else '')) + cache.parent.mkdir(exist_ok=True) + py_compile.compile(str(wrong_source), cfile=str(cache), dfile=str(source), + doraise=True, optimize=int(optimized), invalidation_mode=mode) + if mode == py_compile.PycInvalidationMode.TIMESTAMP: + data = bytearray(cache.read_bytes()) + data[8:16] = struct.pack('> i & 1: + y ^= g + return y + + +@lru_cache(None) +def image(m, G): + return F.mask(tuple(linear(G, x) for x in F.basis(m))) + + +@lru_cache(None) +def inverse(G): + back = {linear(G, x): x for x in range(512)} + F.need(len(G) == 9 and len(back) == 512, "singular transport") + return tuple(back[1 << i] for i in range(9)) + + +def bounds(fs, loc, pr, nx, transports): + F.need( + all(a < z for z, aa in pr.items() for a in aa), + "edges must follow chronological order", + ) + F.need( + all(a < z for a, z in transports), "transports must follow chronological order" + ) + before = {b: (a, G) for (a, b), G in transports.items()} + after = {a: (b, inverse(G)) for (a, b), G in transports.items()} + low = list(fs) + high = list(fs) + for i in range(len(fs)): + if loc[i] is not None: + low[i] = 1 + for j in pr[i]: + low[i] = F.join(low[i], low[j]) + if i in before: + j, G = before[i] + low[i] = image(low[j], G) + for i in reversed(range(len(fs))): + if loc[i] is not None: + high[i] = F.FULL + for j in nx[i]: + high[i] &= high[j] + if i in after: + j, G = after[i] + high[i] = image(high[j], G) + F.need(all(a & b == a for a, b in zip(low, high)), "inconsistent frame bounds") + return low, high + + +def components(low, high, pr, nx, transports): + adj = collections.defaultdict(list) + for a, b in transports: + adj[a].append(b) + adj[b].append(a) + todo = {i for i, (a, b) in enumerate(zip(low, high)) if a != b} + result = [] + while todo: + i = min(todo) + todo.remove(i) + todo2 = [i] + component = [] + while todo2: + i = todo2.pop() + component.append(i) + for j in pr[i] + nx[i] + adj[i]: + if j in todo: + todo.remove(j) + todo2.append(j) + result.append(sorted(component)) + return sorted(result, key=lambda x: (len(x), x)) + + +_DOM = {} + + +def domain(L, U): + key = (L, U) + if key not in _DOM: + extra = [] + s = L + for x in F.basis(U): + if not ((s >> x) & 1): + extra.append(x) + s = F.join(s, F.mask((x,))) + states = {L} + front = [L] + vectors = [] + for mask in range(1, 1 << len(extra)): + v = 0 + for i, x in enumerate(extra): + if mask >> i & 1: + v ^= x + vectors.append(v) + while front: + cur = front.pop() + for x in vectors: + nxt = F.join(cur, F.mask((x,))) + if nxt not in states: + states.add(nxt) + front.append(nxt) + _DOM[key] = sorted(states, key=lambda m: (F.rank(m), m)) + return _DOM[key] diff --git a/research/t74-variable-frame-cap/eliminate.py b/research/t74-variable-frame-cap/eliminate.py new file mode 100644 index 0000000000..5e73e3130a --- /dev/null +++ b/research/t74-variable-frame-cap/eliminate.py @@ -0,0 +1,61 @@ +"""Exact int64 min-sum elimination; saturated infinity prevents overflow.""" + +import math +import numpy as np + +INF = 1 << 60 + + +def solve(dom, factors): + for scope, table in factors: + if scope != sorted(set(scope)) or any(i not in dom for i in scope): + raise ValueError("factor scope must contain sorted distinct domain keys") + if table.dtype != np.int64 or table.shape != tuple(len(dom[i]) for i in scope): + raise ValueError("factor shape or exact integer dtype") + if np.any(table < 0) or np.any(table > INF): + raise ValueError("factor outside bounded nonnegative integer range") + adj = {i: set() for i in dom} + for scope, a in factors: + for i in scope: + adj[i].update(set(scope) - {i}) + steps = [] + maxstates = 0 + while adj: + i = min( + adj, + key=lambda i: ( + math.prod(len(dom[j]) for j in adj[i] | {i}), + len(adj[i]), + i, + ), + ) + nb = sorted(adj.pop(i)) + scope = sorted(nb + [i]) + shape = [len(dom[j]) for j in scope] + maxstates = max(maxstates, math.prod(shape)) + need = math.prod(shape) + if need > 10000000: + raise ValueError(("table exceeds registered budget", need)) + total = np.zeros(shape, dtype=np.int64) + used = [] + for k, (ss, a) in enumerate(factors): + if i not in ss: + continue + used.append(k) + view = [len(dom[j]) if j in ss else 1 for j in scope] + total = np.minimum(INF, total + a.reshape(view)) + used = set(used) + factors = [f for k, f in enumerate(factors) if k not in used] + axis = scope.index(i) + arg = np.argmin(total, axis=axis).astype(np.int32) + best = total.min(axis=axis) + steps.append((i, nb, arg)) + factors.append((nb, best)) + for j in nb: + adj[j].remove(i) + adj[j].update(set(nb) - {j}) + score = sum(int(a) for ss, a in factors) + chosen = {} + for i, nb, arg in reversed(steps): + chosen[i] = int(arg[tuple(chosen[j] for j in nb)]) + return score, chosen, maxstates diff --git a/research/t74-variable-frame-cap/frame_model.py b/research/t74-variable-frame-cap/frame_model.py new file mode 100644 index 0000000000..bcb180527a --- /dev/null +++ b/research/t74-variable-frame-cap/frame_model.py @@ -0,0 +1,144 @@ +"""Literal role/frame graph, with variable scalar and handoff frames. +Frame-invoice model follows PR2322 paid_profile. No producer is imported. +""" + +import collections +from functools import lru_cache + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def incident(g): + need(g[0] in ("add", "scale"), "unsupported scalar gate") + return g[1:3] if g[0] == "add" else g[1:2] + + +FULL = (1 << 512) - 1 + + +@lru_cache(None) +def mask(bs): + s = [0] + for x in bs: + if x not in s: + s += [y ^ x for y in s] + return sum(1 << x for x in s) + + +@lru_cache(None) +def basis(m): + out = [] + space = 1 + for x in range(1, 512): + if (m >> x) & 1 and not ((space >> x) & 1): + out.append(x) + space = mask(tuple(out)) + return tuple(out) + + +@lru_cache(None) +def join(a, b): + if a & b == a: + return b + if a & b == b: + return a + return mask(basis(a) + basis(b)) + + +def rank(m): + return m.bit_count().bit_length() - 1 + + +def model(w): + frames = [] + locations = [] + edges = [] + transports = {} + last = {} + live = set(range(704)) - set(w["removed"]) + + def new(F, loc=None): + i = len(frames) + frames.append(F) + locations.append(loc) + return i + + def touch(r, node): + if r in last: + edges.append((last[r], node)) + last[r] = node + + for r in sorted(live): + bs = [w["ports"][r]] if r < 112 else w["start_extra"].get(str(r), []) + touch(r, new(mask(tuple(bs)))) + + def gate(sec, i): + g = w[sec][i] + node = new(mask(tuple(g[-1])), (sec, i)) + for r in incident(g): + touch(r, node) + + for i in range(len(w["A"])): + gate("A", i) + for r, fr in zip(w["centers"], w["center_frames"]): + touch(r, new(mask(tuple(fr)))) + for r in range(112, 224): + touch(r, new(mask(tuple(w["target_levels"].get(str(r - 112), []))))) + warps = collections.defaultdict(list) + for op, rec in enumerate(w["warps"]): + warps[rec[0]].append((op, rec)) + for i in range(len(w["B"]) + 1): + for op, (_, r, G, U, V) in warps[i]: + before = new(mask(tuple(U)), ("warp_old", op)) + touch(r, before) + after = new(mask(tuple(V)), ("warp_new", op)) + last[r] = after + transports[before, after] = tuple(G) + if i < len(w["B"]): + gate("B", i) + for i in range(len(w["restore"])): + gate("restore", i) + for r in sorted(live): + F = FULL + if 112 <= r < 224: + F = sum( + 1 << x + for x in range(512) + if (x & w["ports"][r - 112]).bit_count() % 2 == 0 + ) + elif str(r) in w["helper_final"]: + F = mask(tuple(w["helper_final"][str(r)])) + touch(r, new(F)) + preds = collections.defaultdict(list) + succs = collections.defaultdict(list) + for a, b in edges: + if frames[a] & frames[b] != frames[a]: + raise ValueError(("invalid initial edge", locations[a], locations[b])) + preds[b].append(a) + succs[a].append(b) + fixed = collections.Counter() + lev = {int(t): mask(tuple(fr)) for t, fr in w["target_levels"].items()} + for r, fr in zip(w["centers"], w["center_frames"]): + f = mask(tuple(fr)) + readers = {lev.get(g[1] - 112, 1) for g in w["cut"] if g[2] == r} + for t in sorted(readers, key=lambda t: -rank(t)): + if f != t: + fixed[rank(f) - rank(t)] += 1 + f = t + + def profile(fs): + p = fixed.copy() + for a, b in edges: + d = rank(fs[b]) - rank(fs[a]) + if d: + p[d] += 1 + return dict(sorted(p.items())) + + need( + profile(frames) == {int(k): v for k, v in w["report"]["local_profile"].items()}, + "source invoice mismatch", + ) + return frames, locations, preds, succs, profile, transports diff --git a/research/t74-variable-frame-cap/inputs/base.json.gz b/research/t74-variable-frame-cap/inputs/base.json.gz new file mode 100644 index 0000000000..f4dda9147a Binary files /dev/null and b/research/t74-variable-frame-cap/inputs/base.json.gz differ diff --git a/research/t74-variable-frame-cap/inputs/extra.json.gz b/research/t74-variable-frame-cap/inputs/extra.json.gz new file mode 100644 index 0000000000..471e4819c0 Binary files /dev/null and b/research/t74-variable-frame-cap/inputs/extra.json.gz differ diff --git a/research/t74-variable-frame-cap/inputs/plan.json.gz b/research/t74-variable-frame-cap/inputs/plan.json.gz new file mode 100644 index 0000000000..45a832a85f Binary files /dev/null and b/research/t74-variable-frame-cap/inputs/plan.json.gz differ diff --git a/research/t74-variable-frame-cap/reduce_frames.py b/research/t74-variable-frame-cap/reduce_frames.py new file mode 100644 index 0000000000..131176a180 --- /dev/null +++ b/research/t74-variable-frame-cap/reduce_frames.py @@ -0,0 +1,51 @@ +"""Lossless graph contraction for concave rank costs, with fixed scalar word. +A free node with a single distinct predecessor can take that predecessor's +frame: c(x)+c(y)>=c(x+y) on each incident role. Symmetric for one successor. +Transport nodes are excluded; multiplicities must balance. +""" + +from collections import defaultdict + + +def reduce(loc, pr, nx): + loc = list(loc) + pr = defaultdict(list, {i: list(v) for i, v in pr.items()}) + nx = defaultdict(list, {i: list(v) for i, v in nx.items()}) + aliases = {} + changed = True + while changed: + changed = False + for i, where in enumerate(loc): + if ( + where is None + or where[0].startswith("warp_") + or not pr[i] + or len(pr[i]) != len(nx[i]) + ): + continue + if len(set(pr[i])) == 1: + a = pr[i][0] + for j in nx[i]: + pr[j].remove(i) + pr[j].append(a) + nx[a] = [j for j in nx[a] if j != i] + list(nx[i]) + elif len(set(nx[i])) == 1: + a = nx[i][0] + for j in pr[i]: + nx[j].remove(i) + nx[j].append(a) + pr[a] = [j for j in pr[a] if j != i] + list(pr[i]) + else: + continue + aliases[i] = a + loc[i] = None + pr[i] = [] + nx[i] = [] + changed = True + + def resolve(i): + while i in aliases: + i = aliases[i] + return i + + return loc, pr, nx, {i: resolve(i) for i in aliases} diff --git a/research/t74-variable-frame-cap/vendor/GENERATOR-NOTICE.txt b/research/t74-variable-frame-cap/vendor/GENERATOR-NOTICE.txt new file mode 100644 index 0000000000..b075f7180e --- /dev/null +++ b/research/t74-variable-frame-cap/vendor/GENERATOR-NOTICE.txt @@ -0,0 +1,129 @@ +Generator for PR2312 width exchange plus coherent four-handoff transformation +========================================================================== + +generate_words.py is new portable code prepared with substantial AI +assistance, under the repository Apache-2.0 license. It directly transforms +the pinned PR2312 width-exchange BORROW-WORDs and regenerates cleanup. The existing source +builder is not copied or imported at runtime. The independent native chain, +rather than the generator or its hashes, proves all-column circuit correctness +and exact physical Clifford phases. + +PR2312 width exchange is credited to Jeremy Kothe (@jeremykothe2), with +AI assistance: alias 651 is re-lent from lender 530 and alias 653 is dropped, +freeing register 554 for cold restoration and changing two width-8 helpers +to width 7. The exact frame re-solve of both borrowed words and the owner +fill for that source width inventory retain the source's credit to Jeremy +Kothe, with AI assistance. This generator consumes the resulting complete +source words; it does not reapply their kernels or width exchange. + +Consumed PR2312 source head: + fb76f799ccf078f51780076ebed3fd26b1db11c0 +Package: + research/gmx-t74-borrow43-width-exchange +Manifest SHA-256: + c545968fb8cf6e550b82ba631e92fd756484db75e621aee211347749cff55313 + +The two helper-donor kernels at pivots 518 and 506 are retained from +PR2302. Their kernel shape is credited to mdumitrean (PR1625); their search, +exact pricing and frame re-solve are credited to Jeremy Kothe +(@jeremykothe2), with AI assistance, as stated by the source. The PR2302 +source and this necessary derivative generator were prepared with AI +assistance. This generator composes the four block-616 handoffs after those +kernels, preserving all kernel scalar gates and their re-solved frames. + +Predecessor PR2302 source head: + d520b92d7bf18efcb7d84f12757face6fe9541f1 +Package: + research/gmx-t74-borrow43-k518-506 +Manifest SHA-256: + 74634d13d27026e2867973b58dfef5e31958d92c54454b29e52292b7fc2e1f0d + +WildIdeas is credited for the exact frame refits retained from PR2288. +The source's additional frame-solver credit to Jeremy Kothe, with AI +assistance, is retained. The predecessor's full credit and licensing notice +is reproduced below. + +Anticipatory dirty borrowing is credited first to Cinna Davis +(@1337isnot1337), PR2226, with substantial OpenAI Codex assistance. The +retired-register K_G handoff and inverse-reverse FULL cleanup with proper-ended +private zero buffers derive from that construction and its PR2288 realization. +PR2288 source head: 614c74a63b0f6d4a24c7740d7ddb90d37861b3c7. + +This code is licensed under Apache-2.0, inherited from the repository. +The original repository LICENSE and NOTICE remain in the predecessor source; +the consumed package NOTICE is reproduced verbatim below, along with the +additional PR2226 notice. The PR2312 and PR2302 package NOTICE files are byte-identical to the +PR2288 package NOTICE reproduced here. + +--- PR2288 package NOTICE (verbatim) --- + +Anticipatory dirty borrowing: PR2226 (Cinna Davis / 1337isnot1337, with substantial OpenAI Codex assistance) is credited first. Its alias rule, changed-reference K_G handoffs, initial compensation and exact free-operator replay (vendored under new/code/borrow/vendor, see new/code/borrow/NOTICE-PR2226.md) are applied here to the T74 pivot-566+554 words; the native lowering, window-exact owner fill and independent audit of the borrow words are new in this package. Bootstrap carried-cutoff repair: PR1956 (Josie Elliston); Lemma G label/adapter checks and X/Y/Z mutants: PR1964 (thakrarsagar), extended here with borrow warp/zero-buffer controls. + +New research prepared by Rohan Arun with substantial OpenAI Codex assistance. Apache-2.0. Parent words and build recipe method derive from Jeremy Kothe PR1274 and Rohan Arun PR1218, with lineage credited in README.md. All inherited mathematical qualifications are retained. +Additional pivot555 and567 composition by Rohan Arun with substantial OpenAI Codex assistance. + +T74 exact-fill owner construction by Rohan Arun with substantial OpenAI Codex assistance. + +PR1377 grid refinement credited to Jeremy Kothe. Outer witness refinement by Rohan Arun with OpenAI Codex assistance; construction unchanged. + +Pivot-566 kernel, words, edits, rebuild.py and rebind.py: PR1625 (mdumitrean). Endpoint/outer-witness stacking, fine_cache.py and oracle stage by jeremykothe2 with oh-my-pi assistance. + + +--- PR2226 native-chain notice (verbatim) --- + +# Credit: anticipatory dirty borrowing (PR2226) + +The construction realised by this native chain is **PR2226, "anticipatory dirty borrowing"**, by Cinna Davis +(@1337isnot1337), prepared with substantial OpenAI Codex assistance (Apache-2.0): the logical reference change +K_G of a lender register (a monomial Clifford: a permutation of the 512 columns with phase mod 4), the initial +compensation terms c K_G z, the early cold tail, the exact cold restoration and the private zero buffers of the +FULL-frame cleanup. `vendor/pr2226_operators.py`, `vendor/pr2226_replay.py` and `vendor/PR2226-NOTICE.md` are byte copies +of PR2226's `operators.py`, `replay.py` and `NOTICE.md`. `bw_gauss.py` is a port of `operators.py` (change, monomial, +apply_mono, coord, frame, check) and adds a decoder from a serialized `clifford_exact` monomial to its exact 512 x 512 +Gaussian matrix. + +What this chain adds (the P3 native realisation, with the Borrow campaign's explicit chronological BORROW-WORD as input): +warp events and zero buffers in `LOCAL-PROGRAMS`, warp recipes in `CLIFFORD-RECIPES.json` (lowered with the unchanged +`lower_child`, rank zero, then compared with the exact numpy column product), logical K_G recipes in +`RESIDUAL-ADAPTERS.json`, an independent local replay in both orientations that checks every warp product on all 512 +columns, and the negative controls listed in `INDEPENDENT-LOCAL-REPLAY.json`, `WRAPPER-CHECKS.json`, `WARP-RECIPE-CHECKS.json` +and `bw_tamper.py`. + +Lineage retained: icekylinx (PR425/433/514, scalar and wrapper machinery), DreamingOfClouds (PR458/484/593 hyperplane/cold-HPE +extensions), the clifford_exact compiler (vendor531), and the owners named in the package README. `vendor/clifford/clifford_exact.py` +is a byte copy. + + +Reproduction and equality +======================== + +Run: + python3 generate_words.py --source-root FETCHED_REPOSITORY --out NEW_DIRECTORY + +The generator checks the pinned source manifest and both consumed compressed +source-word hashes. It writes base.json.gz, extra.json.gz and GENERATION.json. +Canonical JSON hashes cover every output field, including frames, scalar +gates, operators, endpoints, cleanup and invoices. These hashes determine +regenerated circuit equality. The compressed container hashes are recorded +for provenance; Python/zlib changes can produce different gzip streams for +the same circuit. The OS header byte is normalized to 255. In the recorded generation +environment both output containers also exactly match the composed +word hashes. Recompression alone does not require repeating native phases. + +The four binary G maps are explicit construction constants, checked for +invertibility and the measured source-to-handoff chart identity on each run. +The native replay independently lowers their exact physical representatives. +Two old warp-basis representatives are rewritten only after verifying equal +GF(2) spans, preserving the frozen input serialization. No JSON patch file or +unrecorded local dependency is needed. + +Composition binding +=================== + +The source-manifest and source-word constants bind the consumed PR2312 +inputs. The canonical JSON target hashes cover every composed output field. +The literal base tag names PR2312 width exchange plus coherent joint616; +SOURCE_COMMIT and SOURCE_MANIFEST identify the consumed source. +This generation receipt does not establish native phases, owner admission, +or a new exponent; those require their separate independently replayed +native and global receipts. diff --git a/research/t74-variable-frame-cap/vendor/LICENSE b/research/t74-variable-frame-cap/vendor/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/t74-variable-frame-cap/vendor/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/research/t74-variable-frame-cap/vendor/UPSTREAM-NOTICE b/research/t74-variable-frame-cap/vendor/UPSTREAM-NOTICE new file mode 100644 index 0000000000..59d8e0cf31 --- /dev/null +++ b/research/t74-variable-frame-cap/vendor/UPSTREAM-NOTICE @@ -0,0 +1,415 @@ +A sharper exponent for integer multiplication +Copyright 2026 Douglas Colkitt + +This project includes unmodified source files from OpenAI's manuscript +"Integer multiplication below n log n" and its accompanying repository: +https://github.com/openai/math +Commit: adc7f1241b42e322a6451854ab7e4b4c146bf78a + +The original manuscript identifies OpenAI as its author. Its Apache-2.0 +license is retained at upstream/LICENSE. The exact source URLs and hashes +are recorded in upstream/manifest.json. Proposed modifications are supplied +as separate files under patches/; upstream source files remain unchanged. + +The original local research note, scripts, certificates, patches, and +documentation were prepared by Douglas Colkitt with assistance from OpenAI +Codex. The community release incorporates work by the contributors identified +in the notices below; it is not solely Douglas Colkitt's work. +This project is not an official OpenAI release or an OpenAI endorsement. + +Related contributions (not imported in this checkpoint): +Zhihao Chen (jacklightChen), PR #7, supplied an earlier ternary five-subset +motif, finite-alphabet transfer and a different compressed producer: +https://github.com/CrocSwap/integer-mult-bounds/pull/7 +The present checkpoint claims no priority for that motif. Related compressed +complex-network work was submitted by eumemic in PR #3: +https://github.com/CrocSwap/integer-mult-bounds/pull/3 +The pending contributions and their stronger bounds require their own review; +this notice does not represent adoption or verification of their claims. + +Additional community work, including parallel and superseded submissions, is +acknowledged in CONTRIBUTORS.md, with pinned submission metadata in +docs/research/contribution-snapshot.json. These acknowledgements do not imply +joint authorship of the checkpoint, incorporation of pending code, or verification +of submitted mathematical claims. Original source-specific notices remain in force. + +Community release (accepted by conditional maintainer audit): +The following original contributor notices apply to the imported PR #39 chain. +The preceding non-import statements describe the preserved 2^-30 checkpoint. + +Ternary five-subset construction and common-four-point resynthesis +Copyright 2026 Zhihao Chen (jacklightChen) + +This is Zhihao Chen's first submission of this specific construction to this +repository. Research, proof development, code and verification were prepared +with substantial assistance from GPT-6 Astra (OpenAI Codex), as identified by +the contributor. This is not independent review or an OpenAI endorsement. +Future research building on this contribution should explicitly acknowledge +Zhihao Chen (jacklightChen), cite the accompanying note and pull request, and +retain the preceding contributors' attribution. This notice records research +provenance; the repository's Apache-2.0 license remains unchanged. + +Dependencies retained from eumemic's Claude-assisted PRs #3 and #5: +https://github.com/CrocSwap/integer-mult-bounds/pull/3 +https://github.com/CrocSwap/integer-mult-bounds/pull/5 +PR #5 commit: d3d370c34937503bd3fa63c83d505a05e8e50893 +These include complex_circuit.py, complex_network.py, fast_gaussian.py, +their generators, construction notes and certificates. The Gaussian input +scaling proof is corrected in this derivative; see the modification notice below. +Aligned pairing also appears in Bortlesboat's PR #2. Retained totals and bank +sharing appear in dleen's PR #4 and cheaper retained centers in eumemic's PR #6. +Their results and ideas are credited separately from this new construction. + +Bulk recursion and controlled tensor basis, 8 October 2026 +Copyright 2026 icekylinx + +The new projector batching, controlled simultaneous basis, mixed-width tape +recursions, whole-residual complex recursion, and dependency-path precision +guard in the batched-23 proof package are contributed by icekylinx, developed +with substantial OpenAI GPT-6 Astra assistance. Review corrections and +repository integration were prepared with OpenAI Codex assistance. They build on the retained +PR #7 finite producers and the preceding contributions credited above. +The new package retains the repository's Apache-2.0 license and the original +authors' attribution. It is not an official OpenAI release or endorsement. + +Modification notice, 8 October 2026 (icekylinx): the retained fast Gaussian +proof now bounds shifted approximation error by F=2^ceil(1.14 alpha^2). +The P=34p precision budget and asymptotic exponent are unchanged. New batching +checks are integrated into make verify. Existing attribution and licenses +are retained. + +Partial-swap extension, 8 October 2026 +Copyright 2026 icekylinx + +The partial-swap framing, binary retained-total triple construction, +dependency-preserving positive labels and carrier reuse, unequal (25,23,57) +common basis, improved complex batching, and exact assembly are contributed +by icekylinx with substantial OpenAI GPT-6 Astra and Codex assistance. +This extension directly inherits PR #10, commit +62691e395a0458ce089a1c7b5d89e74291e95e29. The portable producer adapters +modify the retained paired-exclusion and shared-point implementations credited +above. The original licenses, attribution, and Gaussian correction are retained. + +Endpoint-gauge extension, 8 October 2026 +Copyright 2026 icekylinx + +The complementary auxiliary endpoint gauges, (32,30,40) controlled basis, +general nondegenerate binary phase residuals, retained-center complex producer, +updated path guard and exact assembly are contributed by icekylinx with +substantial OpenAI GPT-6 Astra and Codex assistance. This extension inherits +f2ab41aebad47861caf6316282c1793e5513845e and its PR #10 ancestry. New portable +adapters retain the paired-exclusion and shared-point contributions credited +above. Original licenses, notices and the Gaussian correction are retained. + +Structured-basis and semantic-bulk extension, 8 October 2026 +Copyright 2026 icekylinx + +The selected (32,30,36) bit construction, A1/A5 block refinements, fixed +middle-axis I+J profiles with bounded-minor CRT certificates, mixed dyadic +complex centers, complete data-front batching and circuit-specific assembly +are contributed by icekylinx with substantial OpenAI GPT-6 Astra and Codex +assistance. The immediate parent is ed90fd940279c336ebc45968631bdebfb087b505. + +The semantic/bulk compatibility argument, literal scalar charge, product row +stock and parameterization adapt Zhihao Chen (jacklightChen)'s PR #23, +commit 661ebabc1076c9f525d7ce4967c876b203fa9827. Translated complex endpoints +are adopted from the same contributor's PR #21, +commit 5ba6cf0bfb68f2be8d15610e7972207c50254d6a, following eumemic's source-frame +work and the earlier nested-basis contributions. + +Completed-child semantic precision, arbitrary-coordinate routing, phase-cell +Gaussian inversion and bulk tape transfer are credited to the RaD project +(hipotures), commit 45d9b60355872041f9275f77c057514def0d45bc, exposed through +PR #20 at 4f8d6c8272b5ff307a0da51df545ec3cd96a8b6e. Their selected proof +sources retain their separate CC0 license and original NOTICE under +references/semantic-bulk/rad20. The PR #23 source retains its recorded OpenAI +Codex assistance; RaD retains its recorded Codex and GPT-6.1-Sol Ultra +assistance. These are source attributions, not claims about this session's +runtime model. Related contributions by Rohan Arun and Aurel Prosz remain +acknowledged in the imported notices. No exclusive priority or additional +license condition is asserted. + +Copied retained-center extension, 8 October 2026 +Copyright 2026 icekylinx + +The copied retained-center schedule in both orientations, its complex-phase +transfer, the Wm-N+L rank budget, and the selected (25,23)/(28,28) composition +are contributed by icekylinx with substantial OpenAI GPT-6 Astra and Codex +assistance. This extension inherits PR #32 at +0ef3aeb61f55cc0b321ce6a0ef00acee25cefe52 and the preceding PR #10/#18/#24 work. + +The two-stage topology and paid copied-stream endpoint correction are due +to Aurel Prosz (Paureel), c82d09eb4781b68435e3fa3eb6beea72fa900fab, +through Zhihao Chen (jacklightChen)'s PR #29 unequal-axis composition, +9d963275075fa98f1da821e27757b238dafd6b3c. That source also credits Swapnil +Jain's two-stage development at ae405eb474d1486b2d8aef90139869f927f4836a. + +The contiguous corner method, incidence factorization and exact partition +certificates are due to Rohan Arun (PR #31), method commit +02f68f95369c39955c5ffcfddbd75cd83e26b305. The selected (25,23) certificate +specializes Dominik Scholz's parameterization (PR #33), +a499a345c040aa15b68e984a0904eadc485c7a7e. Their source notices and proof +snapshots are preserved in references/copied-centers. Historical OpenAI +Codex, GPT-6 Astra and Anthropic Claude Opus 5.5 assistance is credited to +the respective imported sources. Existing PR #21/#23 and RaD attribution, +licenses and the Gaussian correction remain in force. + +Copied centers with reversed (23,25) data corners, 2026-10-08 +Rohan Arun with substantial OpenAI Codex assistance supplies the composition, +exact dimension23 controls and cost/assembly integration. James Chang's PR34 +supplies the reversed boundary family; icekylinx's PR36 supplies copied retained +centers and the selected complex graph. The balanced assembly remains attributed +to RaD/hipotures and its PR34 specialization. Retain Dominik Scholz PR33, Rohan +Arun PR31, Zhihao Chen PR29/21/23, Paureel/Aurel Prosz, Swapnil Jain, icekylinx, +eumemic, Douglas Colkitt, OpenAI and all earlier notices and hypotheses. +This is not a claim of formal verification, new foundational rank identities, +global optimality or measured runtime speedup. + +Fixed middle basis with copied reversed corners (2026-10-08): +Rohan Arun, with substantial OpenAI Codex assistance. Composition and +simultaneous-basis proof retain icekylinx PR32/36, James Chang PR34, +Dominik Scholz PR35/38, Zhihao Chen, Paureel, Swapnil Jain, RaD/hipotures, +eumemic and all preceding attribution and licenses. See research/copied-fixed-reversed. + +Changed-graph composition with copied centers and fixed bases, 8 October 2026 +Prepared with OpenAI Codex assistance. +The new composition uses icekylinx PR36 copied centers and PR32 fixed-I+J +projectors/profiler, Dominik Scholz PR35 two fixed factors and CRT argument, +Zhihao Chen (jacklightChen) PR29/23 interfaces, Aurel Prosz (Paureel) and +Swapnil Jain's two-stage development, Rohan Arun PR25/31 corner methods, +Dominik Scholz PR33/38 dimension/composition work; James Chang (jamesyc) +PR34 reversed geometry and balanced transfer; Rohan Arun PR37/39/40 +reversed integration, modular data tests and both-fixed baseline; +RaD (hipotures) PR41 changed scalar DAGs, alternating point order and +independent role compiler; RaD balanced routing/bulk interfaces, and all +retained predecessors. +Complete attribution and the conditional proof boundary are recorded in +research/copied-fixed/PROOF.md; imported originals and source pins are retained. +Original Apache-2.0 and CC0 notices remain applicable. + +Community follow-up integration (PRs #49, #45 and #26), 8 October 2026: +Rohan Arun contributes weighted carrier matching and climbed summand/leave-one-out +orders (PRs #44/#47/#49), with Anthropic Claude assistance. The final construction +composes Chafik Boukhalfa's changed-graph checks, exact rational data recovery and +reordered exclusion sums (PRs #43/#46/#48, OpenAI Codex assistance) with RaD / +hipotures's alternating pair order and independent physical role compiler (#41). +All predecessor attribution and conditional proof interfaces remain in force. + +Alejandro Zarzuelo Urdiales contributes Gaussian parity and canonical arithmetic +proofs, finite tensor execution, profile precision accounting and mixed-center +reference checks (#45), with substantial OpenAI Codex assistance. See +research/gaussian-parity-synthesis/PROVENANCE.md for his full attribution. +Ryan S / princezuda contributes historical Lean certificate arithmetic, algebraic +frame/movement/guard lemmas and independent paired-circuit checks (#26). Original +source notices and historical snapshots are preserved. Neither formal package +claims a full formal proof of the multiplication algorithm or a new kappa. + +Joint frame compilation of skip-prefix strips + +The local compiler and exact finite witnesses were prepared by eumemic with +substantial OpenAI Codex assistance. Avi Eisenberg / ikeboy with Anthropic +Claude assistance supplied the unmodified PR #53 skip-prefix producer. +The pinned PR #48 pipeline is Chafik Boukhalfa's contribution, incorporating +Rohan Arun, RaD / hipotures, icekylinx, Dominik Scholz, James Chang, +Zhihao Chen, Aurel Prosz / Paureel, Swapnil Jain, eumemic, Douglas Colkitt, +OpenAI, David Harvey, Joris van der Hoeven and the earlier contributors +credited in the retained sources. See references/frame-compiler/pr48/NOTICE +and references/frame-compiler/pr53/NOTICE for their original attribution. +No authorship or review by those predecessors is claimed for this compiler. + +Joint dual-skip/frame-compiler composition (2026-10-08) +--------------------------------------------------- +Rohan Gupta / gupt1156 with Anthropic Claude assistance: PR55 dual-skip +scalar graph; original LICENSE and NOTICE are retained under +references/frame-compiler/pr55. eumemic with substantial OpenAI Codex +assistance: PR57 joint reversible frame compiler, serialized physical-word +replay and profile reconstruction. Chafik Boukhalfa with OpenAI Codex +assistance: this composition, independent integration and exact certificate. +Avi Eisenberg / ikeboy, Rohan Arun, RaD / hipotures, icekylinx, and all +predecessor authors retain the notices above and in pinned source files. +No original copyright or Apache-2.0 notice is removed. + +Ranked reclamation after the PR58 joint-dual composition (2026-10-08) +---------------------------------------------------------------- +Chafik Boukhalfa with OpenAI Codex assistance: prioritize retired physical +slots by descending current frame rank, retaining slot ID as the tie-breaker; +complete replay, exact profiles, comparison and adversarial controls. +The dedicated joint_dual_reclaim_compiler.py is derived from eumemic's PR57 +compiler. Its original shared compiler remains byte-identical. The PR55 +producer and all preceding attribution remain unchanged. The complete PR58 +comparison certificate and its original source/proof provenance are retained +under references/frame-compiler/pr58. + +Skip-prefix strip producer, 8 October 2026 +By Avi Eisenberg (ikeboy), with Anthropic Claude (Claude Opus 5.5) +assistance. The skip-prefix leave-one-out strip layout in +research/skip-strips/skip_graph.py is new. Everything else reuses Chafik +Boukhalfa's PR #43/#46/#48 research/copied-fixed pipeline, its verification +code, exact data recovery and support-order sorting, together with: +- Rohan Arun's PR #44 weighted carrier matching optimizer; +- RaD (hipotures) PR #41 alternating point order; +- every predecessor credited above. +Complete attribution and the conditional proof boundary are recorded in +research/skip-strips/PROOF.md. Original Apache-2.0 and CC0 notices remain +applicable. + +Local split-pair skip-prefix research continuation (2026-10-08) +Prepared with substantial OpenAI Codex assistance at the user's request. +New contribution: singleton/pair recursive partition refinement, finite summand +order and moment search, and verified composition with inherited paid clones. +Avi Eisenberg/ikeboy with Anthropic Claude assistance: PR53 skip-prefix strips. +Chafik Boukhalfa with OpenAI Codex assistance: PR54 original-envelope clone +specialization and PR43/46/48 checking interfaces. RaD/hipotures: PR51 +whole-chain/source-partition cloning and earlier producer/interfaces. +Rohan Arun: PR44 weighted matching and earlier fixed/reversed work, with all +stated historical AI assistance. All predecessor notices remain applicable. + +Original-envelope whole-chain clones on skip-prefix strips (research/skip-clones): +Chafik Boukhalfa, prepared with OpenAI Codex assistance. The complete-chain +source-partition clone operation is adapted from RaD / hipotures, PR #51, +with original envelopes retained here. The scalar base is Avi Eisenberg's +PR #53 skip-prefix layout, prepared with Anthropic Claude assistance. +All credited PR #43/#46/#48, PR #44 and earlier code/proof notices remain +in force. This extension is provided under the repository's Apache-2.0 terms. + +Community review checkpoint #50–#61, 8 October 2026 +Maintainer integration and independent arithmetic: Douglas Colkitt, with OpenAI Codex. +Avi Eisenberg / ikeboy: skip-prefix strip framework (#53), with Anthropic Claude. +Rohan Gupta / gupt1156: parallel order search (#50, stated Antigravity assistance) +and dual-suffix strips (#55, Anthropic Claude assistance). +Eumemic: equal-frame joint compilation and paid signal reclamation (#57), with Codex. +Chafik Boukhalfa: original-envelope paid clones (#54), composition (#58) and ranked +reclamation (#60), with Codex. Rohan Arun: order search (#52) and positive-frame +composition (#56), with Anthropic Claude and stated Codex validation assistance. +RaD / hipotures: enlarged frames, source partitions and paid whole-chain clones +(#51), with Codex. Rohan Garg / rohangar1: singleton/pair recursion and paid-clone +composition (#59), with Codex. Alejandro Zarzuelo Urdiales: exact parameter +refinement, scoped Lean arithmetic, matrix/parity and search tools (#61), with +his disclosed multi-tool and Codex assistance. +Parallel #50/#52 records are reviewed and credited without replacing the earlier +climbed-48 implementation; their exact commit history is retained. The separate +#51 witness is retained as research; its source-graph/negative-basis data proof +has not received the same full replay as #56's consumed compiler machinery. +See docs/research/community-round2-review.md for precise validation boundaries. +All earlier licenses, contributions and notices remain applicable. + +Interval strips and core-aware pair assembly + +The interval leave-one-out strips and the core-aware group-pair assembly in +research/pair-assembly were prepared by Avi Eisenberg / ikeboy with Anthropic +Claude assistance. They build on PR #53's skip-prefix pipeline and its +inherited PR #48 sources. The stacked witness in research/pair-assembly/frame +uses eumemic's PR #57 joint frame compiler unchanged; its driver and verifier +are adaptations of PR #57's skip_frame_compiler.py, skip_frame_compose.py and +verify_skip_frame.py. Original notices are retained. + +Stopped product-ring extension, 9 October 2026 +Copyright 2026 icekylinx + +The opposite-bank generic projector factorization, componentwise atom-ring +adapters, stopped recurrence and outer ordinary-interchange conversion, +aligned pair-star producer with rational centers, exact denominator-21 +grid and selected (23,23)/(24,24) composition are contributed by icekylinx +with substantial OpenAI GPT-6 Astra and Codex assistance. This extension +builds on merged PR #36, 11817ccacb564bb7f98789c20dc11d3fece207e3, and is +integrated on upstream main 56b66d58297deca1d7dd130247d720e960f77a37. + +The retained ordinary leaf uses the preceding projector, corner and +copied-center proofs. The selected two-stage topology retains Aurel Prosz +(Paureel), Swapnil Jain and Zhihao Chen's credits; the semantic assembly +retains PR #21/#23 and RaD's attribution. Paired producers, carrier matching, +original source notices and each imported license remain unchanged. + +Partial-gauge extension, 9 October 2026 +Copyright 2026 icekylinx + +The pair-first cube assembly, compatible backward frame enlargement, +partial source-gauge schedule and stopped whole-projector composition are +contributed by icekylinx with substantial OpenAI GPT-6 Astra and Codex +assistance, extending PR #104 at 948ce1510df750f4c18b96bdaef436a86f8bf834. + +The physical deferred bit word, reflected event accounting, fan-order +clarification and signed two-stage endpoint are adopted from Zhihao Chen +(jacklightChen), PR #97, e15350b66e4bf796153a68c240a6cc1b788abe3e, with +Codex assistance. Its deferred readouts, V leaves, lifted frames and frozen +witness originate in Swapnil Jain's 741e7aa078392553815df7926ee17ac5e25a8c38, +with the original Claude disclosure retained. Cyclic interval and core-aware +pair primitives build on Avi Eisenberg (ikeboy), PR #62, +ad0f25ff7b23cff7f08ad237c2254e6ecf74257e, with Anthropic Claude assistance. +Prior two-stage, copied-center, ordinary-leaf, semantic/bulk, routing and +precision credits remain in force. Imported source notices and licenses +are preserved under references/partial-gauge/; see SOURCES.json. + +Three-stage cover extension, 9 October 2026 +Copyright 2026 icekylinx + +The arbitrary-subspace Clifford frame theorem, three-stage Cayley geometry, +weighted q-adic GL cover, unit-lower weighted compiler, charged local-ring +fallback, uniform batching, internal row borrowing and exact composition +are contributed by icekylinx with substantial OpenAI GPT-6 Astra assistance. This +repository integration uses Codex assistance and extends +PR #115, cf60442983c153a3a0f5272ea4713f99eba13c86. + +The selected local complex DAG and support/label replay are adopted from +Copyright 2026 eumemic, PR #117, cbb05ce504d571546d9b7794c186a613c659c3bf, +with its original Apache-2.0 terms and Claude assistance disclosure. +The unchanged bit physical word retains Zhihao Chen (jacklightChen), +PR #97, and Swapnil Jain's underlying witness and assistance notices. +The prior opposite-bank, stopped ordinary-leaf, copied-center, topology, +semantic/bulk, precision and analytic credits remain applicable. +Original source notices and license bytes are preserved in +references/three-stage-cover/pr117/ and references/partial-gauge/. + +Paired-cube and shared-core extension, 9 October 2026 +Copyright 2026 icekylinx + +The paired-coordinate triple-cube identity, signed overlap channels, +original-source involution, coordinate-star centers, concrete frame/carrier +compiler, chronological source gauges, PR97 gauge-subset selection, +orthogonal cross-stage routing and exact supplier/assembly integration +are contributed by icekylinx with substantial OpenAI GPT-6 Astra assistance. +Repository integration uses Codex assistance and extends PR #130 at +6a9970a530119174507904e23592fd59ede19a5d. + +The substantial completed-core workspace-sharing principle is credited to +an664, PR #128, 530588a019b4a74f09180680c9e3961bf649ec89, with its reported +OpenAI Codex assistance. No source code, partition or serialized witness +from that PR is imported. The new routing and paired-motif integration +are described separately and claim no exclusive priority for broad sharing, +paired-coordinate, Fourier or carrier-matching ideas. + +Selected coarse queries restrict the retained eumemic PR #117 positive DAG; +its original Apache-2.0 and Claude assistance notices remain unchanged. +The bit word and original frames retain Zhihao Chen's PR #97 and Swapnil +Jain's frozen witness, notices and historical assistance disclosures. +Earlier generalized Clifford, three-stage, uniform weighted recursion, +ordinary-leaf, semantic/bulk, precision and analytic credits remain in force. +Source-specific license bytes are preserved under references/. + +October 9 recycled-bit integration: +DaysSky (#150), William Porter/hpst3r (#147), Thomas Marchand/Th0rgal (#146), +Rohan Gupta/gupt1156 (#148), James Chang/jamesyc (#124), SovereignSteak (#122). +The original notices and assistance disclosures are retained under research/, +including research/recycled-bit-integration/NOTICE. Andrew Barnes/Bortlesboat +(#101) repairs shared verifiers using rfu08's #64 counterexample. rfu08's +scoped finite and formal-transfer packages are included separately; they do +not establish the full multiplication theorem. Earlier and parallel credits +remain applicable. Douglas Colkitt integrated these with OpenAI Codex assistance. + +SovereignSteak PR151 independently supplies the matching gauge/recycling +composition and the selected 473/10^6 atom refinement; its original package +and assistance disclosure are retained under research/gauge-recycling/. + +October 9 coordinated-frame and completed-entrance-bank integration: +Dugongue PR186, 166a34d75e853e933855f0f7e940fe77c4bb6b8d, builds on +Chafik Boukhalfa/chafreaky's PR181, 7fb2194801e3a10f54772c7f0d5505035a4fc0ad, +and eumemic's PR168 v4, 4a3c769e5c5430e7114c4d3e099ff34664677f17. +The frozen package and prerequisite archive preserve all author, source-license +and assistance notices, including PR175's compiler optimization. DaysSky's +carrier closure, James Chang's terminal substitution and balanced assembly, +geckods' stopping refinements and all preceding framework credits remain. +Rohan Arun's PR185 bootstrap and chafreaky's PR182 bit refinement are reviewed +parallel contributions; their gains are not added to the selected witness. +Douglas Colkitt integrated the package and supplied the bank scheduling +supplement with OpenAI Codex assistance, under Apache-2.0. The all-size +interfaces remain conditional; finite verification is not full formalization. diff --git a/research/t74-variable-frame-cap/vendor/fine_moment.py b/research/t74-variable-frame-cap/vendor/fine_moment.py new file mode 100644 index 0000000000..9d7d774d62 --- /dev/null +++ b/research/t74-variable-frame-cap/vendor/fine_moment.py @@ -0,0 +1,59 @@ +"""Higher-precision independent base-two moment enclosure (same algorithm as base_two_moment.py, finer constants), evaluated in directed-rounding +integer fixed point on the 2^-10239 grid (lower bounds: floor every non-negative intermediate; upper bounds: ceil every intermediate), which is +monotone and therefore sound; same enclosure semantics as the exact-rational original, far faster.""" +from fractions import Fraction as Q +from functools import lru_cache +try: + from gmpy2 import mpz # optional accelerator: identical integer results, much faster +except ImportError: + mpz = int +GRID = 1 << 10239 +LOG_TERMS = 3226 +EXP_TERMS = 1542 +def require(c, msg): + if not c: raise ValueError(msg) +def _cd(a, b): return -((-a)//b) +SH = 10239 +@lru_cache(None) +def log_unit(x): + require(1 <= x <= 2, "logarithm range") + z = (x-1)/(x+1) + p, q = mpz(z.numerator), mpz(z.denominator) + p2, q2 = p*p, q*q + pl = GRID*p//q; ph = _cd(GRID*p, q) # z^1 bounds + sl = sh = mpz(0) + for j in range(LOG_TERMS): + sl += pl//(2*j+1); sh += _cd(ph, 2*j+1) + pl = pl*p2//q2; ph = _cd(ph*p2, q2) # z^(2j+3) + # tail 2 z^(2N+1) / ((2N+1)(1-z^2)), rounded up; ph = z^(2N+1) upper bound + tail = _cd(2*ph*q2, (2*LOG_TERMS+1)*(q2-p2)) + return Q(int(2*sl), GRID), Q(int(2*sh+tail), GRID) +def log_bounds(x): + require(x >= 1, "logarithm range") + k = 0 + while x > 2: + x /= 2; k += 1 + lo, hi = log_unit(x) + l2, u2 = log_unit(Q(2)) + lo, hi = lo+k*l2, hi+k*u2 + return Q((lo*GRID).__floor__(), GRID), Q((hi*GRID).__ceil__(), GRID) +def exp_bounds(x): + """Outward enclosure of exp(x), 0 <= x < 1, on the 1/GRID grid: lower = partial sum through x^(EXP_TERMS-1)/(EXP_TERMS-1)! (positive terms), + upper = partial sum + 2*x^EXP_TERMS/EXP_TERMS! (tail <= that for x < 1).""" + require(0 <= x < 1, "exponential range") + xl = mpz(x.numerator)*GRID//x.denominator; xu = _cd(mpz(x.numerator)*GRID, x.denominator) + tl = th = mpz(GRID); sl = sh = mpz(GRID) + for j in range(1, EXP_TERMS): + tl = ((tl*xl) >> SH)//j; th = _cd(-((-th*xu) >> SH), j) + sl += tl; sh += th + tn = _cd(-((-th*xu) >> SH), EXP_TERMS) + return Q(int(sl), GRID), Q(int(sh+2*tn+2), GRID) +def moment(m, W, entries, saving): + lo = hi = Q(0) + for t, count in entries: + t, count = int(t), int(count) + require(0 < t < m and count > 0, "improper child") + l, u = log_bounds(Q(m, t)) + lo += Q(t*count, m*W)*exp_bounds(saving*l)[0] + hi += Q(t*count, m*W)*exp_bounds(saving*u)[1] + return Q((lo*GRID).__floor__(), GRID), Q((hi*GRID).__ceil__(), GRID) diff --git a/research/t74-variable-frame-cap/verify.py b/research/t74-variable-frame-cap/verify.py new file mode 100644 index 0000000000..7ff0f6fe46 --- /dev/null +++ b/research/t74-variable-frame-cap/verify.py @@ -0,0 +1,382 @@ +#!/usr/bin/env python3 +"""Exact lower bound for all monotone scalar and transported handoff frames.""" + +import argparse, copy, gzip, hashlib, importlib.util, itertools, json, math, sys +from collections import Counter +from fractions import Fraction as Q +from pathlib import Path +import numpy as np + +ROOT = Path(__file__).resolve().parent +sys.path.insert(0, str(ROOT)) +import frame_model as F +import domains as J +import reduce_frames +from eliminate import solve, INF + +SCALE = 1 << 40 + + +def read(path): + b = path.read_bytes() + return json.loads(gzip.decompress(b) if path.suffix == ".gz" else b) + + +def canonical(x): + return json.dumps(json.loads(json.dumps(x)), sort_keys=True, separators=(",", ":")) + + +def engine(source_bytes): + s = importlib.util.spec_from_file_location( + "fine_moment", ROOT / "vendor/fine_moment.py" + ) + m = importlib.util.module_from_spec(s) + # Use the exact authenticated bytes; -B does not prevent reading .pyc files. + exec(compile(source_bytes, str(ROOT / "vendor/fine_moment.py"), "exec"), m.__dict__) + m.SH = 256 + m.GRID = 1 << 256 + m.LOG_TERMS = 100 + m.EXP_TERMS = 96 + return m + + +def optimize(w, cost): + fs, loc, pr, nx, profile, transports = F.model(w) + for (a, z), G in transports.items(): + J.inverse(G) + F.need(J.image(fs[a], G) == fs[z], "source warp image") + original_loc = list(loc) + loc, pr, nx, aliases = reduce_frames.reduce(loc, pr, nx) + L, U = J.bounds(fs, loc, pr, nx, transports) + comps = J.components(L, U, pr, nx, transports) + variables = {i for c in comps for i in c} + best = list(fs) + rows = [] + minimum = 0 + # All child costs not incident to a variable, plus cut-copy charges. + edge_profile = Counter() + for z, aa in pr.items(): + for a in aa: + if a not in variables and z not in variables: + d = F.rank(L[z]) - F.rank(L[a]) + F.need(d >= 0 and L[a] & L[z] == L[a], "fixed edge") + minimum += cost[d] + # Copy descents are the only invoice entries absent from the graph edges. + _, _, raw_pr, _, _, _ = F.model(w) + for z, aa in raw_pr.items(): + for a in aa: + d = F.rank(fs[z]) - F.rank(fs[a]) + if d: + edge_profile[d] += 1 + copies = Counter({int(k): v for k, v in w["report"]["local_profile"].items()}) + copies.subtract(edge_profile) + F.need( + all(n >= 0 for n in copies.values()) + and {r: n for r, n in copies.items() if n} == {8: 8}, + "private copy invoice", + ) + minimum += sum(n * cost[r] for r, n in copies.items()) + for ci, comp in enumerate(comps): + dom = {i: J.domain(L[i], U[i]) for i in comp} + cs = set(comp) + F.need(all(fs[i] in dom[i] for i in comp), "source outside complete domains") + edges = set((a, i) for i in comp for a in pr[i]) | set( + (i, j) for i in comp for j in nx[i] + ) + factors = [] + for a, z in sorted(edges): + da = dom.get(a, [L[a]]) + dz = dom.get(z, [L[z]]) + arr = np.full((len(da), len(dz)), INF, dtype=np.int64) + for ia, fa in enumerate(da): + for iz, fz in enumerate(dz): + if fa & fz == fa: + arr[ia, iz] = pr[z].count(a) * cost[F.rank(fz) - F.rank(fa)] + scope = sorted({a, z} & cs) + factors.append((scope, arr.reshape([len(dom[i]) for i in scope]))) + for (a, z), G in transports.items(): + if a not in cs and z not in cs: + continue + da = dom.get(a, [L[a]]) + dz = dom.get(z, [L[z]]) + lookup = {f: j for j, f in enumerate(dz)} + arr = np.full((len(da), len(dz)), INF, dtype=np.int64) + for i, f in enumerate(da): + image = J.image(f, G) + if image in lookup: + arr[i, lookup[image]] = 0 + scope = sorted({a, z} & cs) + factors.append((scope, arr.reshape([len(dom[i]) for i in scope]))) + score, chosen, maxstates = solve(dom, factors) + F.need(0 <= score < INF, "no feasible component") + minimum += score + for i, j in chosen.items(): + best[i] = dom[i][j] + rows.append(dict(nodes=len(comp), minimum=score, max_table_states=maxstates)) + for i, j in aliases.items(): + best[i] = best[j] + # Check the reconstructed assignment against the original, uncontracted graph. + for z, aa in raw_pr.items(): + for a in aa: + F.need(best[a] & best[z] == best[a], "reconstructed inclusion") + for (a, z), G in transports.items(): + F.need(J.image(best[a], G) == best[z], "reconstructed transport") + for i, where in enumerate(original_loc): + if where is None: + F.need(best[i] == fs[i], "changed fixed anchor") + p = profile(best) + original = profile(fs) + F.need( + sum(r * n for r, n in p.items()) + == sum(r * n for r, n in original.items()) + == 5371, + "invariant local mass", + ) + F.need( + minimum <= sum(n * cost[r] for r, n in p.items()), + "lower bound exceeds reconstructed cost", + ) + F.need( + minimum == sum(n * cost[r] for r, n in original.items()), + "expected rounded optimum changed", + ) + return dict( + minimum_excess_units=minimum, + scale=SCALE, + local_rank_mass=5371, + source_profile=original, + reconstructed_profile=p, + contracted_nodes=len(aliases), + variable_nodes=len(variables), + components=rows, + ) + + +def packing(dual, stock, inventory, flo): + y = list(map(Q, dual["width_dual"])) + z = list(map(Q, dual["bin_dual"])) + sizes = dual["widths"] + ranks = dual["bin_ranks"] + slacks = [] + F.need( + sizes == [4, 5, 7, 8, 9] + and ranks == [8, 16, 32, 48] + and len(y) == 5 + and len(z) == 4, + "dual dimensions", + ) + for R, v in zip(ranks, z): + for ns in itertools.product(*(range(R // s + 1) for s in sizes)): + rem = R - sum(s * n for s, n in zip(sizes, ns)) + if rem < 0: + continue + slack = flo[rem] - v - sum(n * q for n, q in zip(ns, y)) + F.need(slack >= 0, "invalid packing dual") + slacks.append(slack) + F.need(len(slacks) == 1163, "pattern enumeration") + return sum(666 * inventory[s] * v for s, v in zip(sizes, y)) + sum( + stock[R] * v for R, v in zip(ranks, z) + ), min(slacks) + + +def controls(cost): + # Complete F2^3 lattice has 1,7,7,1 subspaces. Independent cardinality control. + ds = J.domain(1, F.mask((1, 2, 4))) + F.need( + Counter(F.rank(m) for m in ds) == {0: 1, 1: 7, 2: 7, 3: 1}, + "complete lattice control", + ) + # Brute-force a nontrivial cyclic factor graph, including infeasible pairs. + dom = {i: [0, 1, 2] for i in range(4)} + factors = [] + for a, z in [(0, 1), (1, 2), (2, 3), (0, 3), (1, 3)]: + table = np.array([[0, 9, INF], [4, 1, 7], [INF, 2, 5]], dtype=np.int64) + ( + a + z + ) + table = np.minimum(table, INF) + # Competing pairwise preferences make the optimum depend on the cycle. + table = np.roll(table, (a + z) % 3, axis=1) + factors.append(([a, z], table)) + optimum = min( + sum(int(t[assignment[a], assignment[z]]) for (a, z), t in factors) + for assignment in itertools.product(range(3), repeat=4) + ) + score, choices, _ = solve(dom, copy.deepcopy(factors)) + F.need( + score + == optimum + == sum(int(t[choices[a], choices[z]]) for (a, z), t in factors), + "elimination vs brute force", + ) + # Actual reduction of a split rank-2 climb, with fixed endpoints. + loc = [None, ("scale", 0), None] + pr = {1: [0], 2: [1]} + nx = {0: [1], 1: [2]} + reduced, rpr, rnx, aliases = reduce_frames.reduce(loc, pr, nx) + F.need( + aliases == {1: 0} and rpr[2] == [0] and rnx[0] == [2], + "contraction reconstruction", + ) + F.need(2 * cost[1] > cost[2], "contraction must improve split positive control") + fixed = [None, None, None] + F.need(not reduce_frames.reduce(fixed, pr, nx)[3], "fixed anchors must survive") + F.need( + not reduce_frames.reduce(loc, {1: [0], 2: [1]}, {0: [1], 1: [2, 2]})[3], + "unbalanced incidence must survive", + ) + return dict( + complete_three_space_counts=[1, 7, 7, 1], + cyclic_assignments=81, + cyclic_optimum=optimum, + split_climb_saving_units=2 * cost[1] - cost[2], + fixed_anchors_preserved=True, + unbalanced_node_preserved=True, + ) + + +def run(): + pins = read(ROOT / "INPUTS.json") + verified = {} + for p in pins["sources"]: + data = (ROOT / p["path"]).read_bytes() + F.need( + hashlib.sha256(data).hexdigest() == p["sha256"], + "source digest: " + p["path"], + ) + verified[p["path"]] = data + if "uncompressed_sha256" in p: + F.need( + hashlib.sha256(gzip.decompress(data)).hexdigest() + == p["uncompressed_sha256"], + "uncompressed digest", + ) + dual = read(ROOT / "DUAL.json") + b = Q(dual["threshold"]) + F.need(b == Q(4243, 2500000), "threshold") + e = engine(verified["vendor/fine_moment.py"]) + flo = {0: Q(0)} + for r in range(1, 49): + flo[r] = (73 * e.moment(73, 1, [(r, 1)], b)[0] - r) / b + cost = [int((flo[r] * SCALE).__floor__()) for r in range(10)] + F.need(all(0 <= c < INF // 20000 for c in cost), "integer range") + words = {tag: read(ROOT / f"inputs/{tag}.json.gz") for tag in ["base", "extra"]} + inventory = None + results = {} + for tag, w in words.items(): + F.need( + (w["report"]["v"], w["report"]["h"], w["report"]["R"]) == (112, 9, 480), + "word geometry", + ) + live = set(range(224, 704)) - set(w["removed"]) + inv = Counter( + F.rank( + F.mask(tuple(w["helper_final"].get(str(r), [1 << i for i in range(9)]))) + ) + - F.rank(F.mask(tuple(w["start_extra"].get(str(r), [])))) + for r in live + ) + F.need(dict(inv) == {4: 33, 5: 9, 7: 38, 8: 114, 9: 240}, "helper widths") + inventory = inv + results[tag] = optimize(w, cost) + plan = read(ROOT / "inputs/plan.json.gz") + stock = Counter() + F.need( + (plan["M"], plan["live"], plan["deficit"]) == (73, 66304, 23680), + "parent dimensions", + ) + F.need( + len(plan["order"]) == 666 and len({tuple(x) for x in plan["order"]}) == 666, + "call count", + ) + F.need( + set(plan["windows"]) == {f"{r},{c}" for r in range(74) for c in range(18)}, + "window keys", + ) + for rank, times in plan["windows"].values(): + stock[rank] += 112 + F.need(dict(stock) == {8: 49728, 16: 33152, 32: 33152, 48: 33152}, "bin stock") + D, slack = packing(dual, stock, inventory, flo) + local = min(Q(r["minimum_excess_units"], SCALE) for r in results.values()) + idle_mass = sum(r * n for r, n in stock.items()) - 666 * sum( + r * n for r, n in inventory.items() + ) + mass = 666 * 5371 + idle_mass + F.need(mass == 73 * 66304 - 23680, "total mass") + lower = (mass + b * (666 * local + D)) / (73 * 66304) + F.need(lower > 1, "cap not established") + tests = controls(cost) + rejected = [] + bad = copy.deepcopy(words["extra"]) + bad["report"]["local_profile"]["1"] -= 1 + try: + optimize(bad, cost) + except ValueError: + rejected.append("undercharged invoice") + else: + raise ValueError("undercharged invoice accepted") + bad = copy.deepcopy(words["extra"]) + bad["warps"][0][2][0] = 0 + try: + optimize(bad, cost) + except ValueError: + rejected.append("singular logical transport") + else: + raise ValueError("singular transport accepted") + bad = copy.deepcopy(dual) + bad["bin_dual"][0] = str(Q(bad["bin_dual"][0]) + 1) + try: + packing(bad, stock, inventory, flo) + except ValueError: + rejected.append("overstated dual") + else: + raise ValueError("overstated dual accepted") + return dict( + schema=1, + threshold=str(b), + sources=pins, + dual_sha256=hashlib.sha256((ROOT / "DUAL.json").read_bytes()).hexdigest(), + integer_costs=cost, + words=results, + helper_widths=dict(inventory), + bin_stock=dict(stock), + packing_excess_lower=str(D), + minimum_pattern_slack=str(slack), + total_rank_mass=mass, + moment_lower=str(lower), + margin=str(lower - 1), + controls=tests, + rejected=rejected, + ) + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--record", type=Path) + a = ap.parse_args() + if a.record: + F.need(not a.record.exists(), "receipt already exists") + result = run() + if a.record: + with a.record.open("x") as f: + f.write(json.dumps(result, sort_keys=True, indent=2) + "\n") + else: + F.need( + canonical(result) == canonical(read(ROOT / "EXPECTED.json")), + "receipt mismatch", + ) + print( + "PASS_T74_VARIABLE_FRAME_CAP", + result["threshold"], + "margin", + float(Q(result["margin"])), + "max_table_states", + max( + c["max_table_states"] + for w in result["words"].values() + for c in w["components"] + ), + ) + + +if __name__ == "__main__": + main()