From 4c35687d7c0da8e6cf33f17e418ecf31c95ff3ad Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Tue, 13 Oct 2026 13:44:47 -0500 Subject: [PATCH] Research: classify rounded restoration under port borrowing --- .../rounded-borrowing-contract/CLAIM.json | 23 + .../rounded-borrowing-contract/COVERAGE.md | 107 ++ .../rounded-borrowing-contract/EXPECTED.json | 1182 +++++++++++++++++ .../HANDOFF-OVERLAP.json | 84 ++ research/rounded-borrowing-contract/LICENSE | 201 +++ research/rounded-borrowing-contract/NOTICE.md | 39 + .../rounded-borrowing-contract/OVERLAP.json | 313 +++++ research/rounded-borrowing-contract/PROOF.md | 384 ++++++ research/rounded-borrowing-contract/README.md | 69 + .../rounded-borrowing-contract/SOURCES.json | 75 ++ .../VALIDATION.json | 64 + .../context/base-selected-result.json | 177 +++ .../context/refresh-selected-result.json | 194 +++ .../rounded-borrowing-contract/contracts.py | 92 ++ .../test_package.py | 97 ++ .../vendor/pr1054/NOTICE.md | 46 + .../vendor/pr1054/PROOF.md | 338 +++++ .../vendor/pr1057/NOTICE.md | 42 + .../vendor/pr1057/PROOF.md | 238 ++++ .../vendor/pr1057/borrow.py | 152 +++ .../vendor/pr985/NOTICE.md | 41 + .../vendor/pr985/PROOF.md | 428 ++++++ .../vendor/pr985/dirty_stride.py | 409 ++++++ research/rounded-borrowing-contract/verify.py | 403 ++++++ 24 files changed, 5198 insertions(+) create mode 100644 research/rounded-borrowing-contract/CLAIM.json create mode 100644 research/rounded-borrowing-contract/COVERAGE.md create mode 100644 research/rounded-borrowing-contract/EXPECTED.json create mode 100644 research/rounded-borrowing-contract/HANDOFF-OVERLAP.json create mode 100644 research/rounded-borrowing-contract/LICENSE create mode 100644 research/rounded-borrowing-contract/NOTICE.md create mode 100644 research/rounded-borrowing-contract/OVERLAP.json create mode 100644 research/rounded-borrowing-contract/PROOF.md create mode 100644 research/rounded-borrowing-contract/README.md create mode 100644 research/rounded-borrowing-contract/SOURCES.json create mode 100644 research/rounded-borrowing-contract/VALIDATION.json create mode 100644 research/rounded-borrowing-contract/context/base-selected-result.json create mode 100644 research/rounded-borrowing-contract/context/refresh-selected-result.json create mode 100644 research/rounded-borrowing-contract/contracts.py create mode 100644 research/rounded-borrowing-contract/test_package.py create mode 100644 research/rounded-borrowing-contract/vendor/pr1054/NOTICE.md create mode 100644 research/rounded-borrowing-contract/vendor/pr1054/PROOF.md create mode 100644 research/rounded-borrowing-contract/vendor/pr1057/NOTICE.md create mode 100644 research/rounded-borrowing-contract/vendor/pr1057/PROOF.md create mode 100644 research/rounded-borrowing-contract/vendor/pr1057/borrow.py create mode 100644 research/rounded-borrowing-contract/vendor/pr985/NOTICE.md create mode 100644 research/rounded-borrowing-contract/vendor/pr985/PROOF.md create mode 100644 research/rounded-borrowing-contract/vendor/pr985/dirty_stride.py create mode 100644 research/rounded-borrowing-contract/verify.py diff --git a/research/rounded-borrowing-contract/CLAIM.json b/research/rounded-borrowing-contract/CLAIM.json new file mode 100644 index 0000000000..4cc61ed67a --- /dev/null +++ b/research/rounded-borrowing-contract/CLAIM.json @@ -0,0 +1,23 @@ +{ + "route": "7: exact-additive versus rounded child restoration", + "base_commit": "abdc6a7002abdbcd9e21bfc5e1a795784deacfdf", + "branch": "codex/k9-rounded-borrowing", + "claim_time_utc": "2026-10-13T18:04:45Z", + "object": "Translation defects, exact helper restoration, and residual storage for rational rounded leaf shears in a fixed dirty pool", + "method": "Algebraic characterization; exact finite-grid replay; dyadic residual state count", + "expected_deliverable": "Scoped obstruction and resource tradeoff with a uniform proof and exact checks", + "coordination": "Local claim; the coordinator reports no pinned sprint issue", + "candidates": [ + "Compute a rounded child on a zero target, copy its increment, and uncompute. Target independence does not imply additive dependence on the source.", + "Lift dyadic arithmetic to exact residual states. Charge clean low bits, widths, source access, and inverse execution.", + "Characterize the translation defect required by dirty-port composition and prove a finite-grid obstruction for rational rounded leaves." + ], + "selected": 3, + "dependency_heads": { + "1057": "78a062df1dcab2bffea5ff4d8243f3da6e465414", + "985": "da1cdf8ed4ac9b1b8378dfec73f77ff4e81a4f70", + "1054": "6bc675be1554b3a3be771147f21f9dc2c6dae50a" + }, + "kappa": "No selected exponent change is claimed. Fixed-pool storage alone does not reduce the inherited all-role call moment.", + "expected_finish_utc": "2026-10-13T18:50:00Z" +} diff --git a/research/rounded-borrowing-contract/COVERAGE.md b/research/rounded-borrowing-contract/COVERAGE.md new file mode 100644 index 0000000000..739ba67df9 --- /dev/null +++ b/research/rounded-borrowing-contract/COVERAGE.md @@ -0,0 +1,107 @@ +# Evidence scope and check ownership + +## Defined finite domains + +There is no random search. No random seed is used. Each declared loop runs +to completion; the stopping rule is the end of its finite domain. + +- Scalar ratios: every reduced p/q with `2<=q<=24` and `-2q<=p<=2q`. + For each of the 716 ratios, translations run from -2q through 2q. + The safe-lattice check uses all q residue representatives. The residue + adapter check uses all old values and translations from -2q through 2q. + It checks 47,340 translation classes and 3,495,180 exact responses. + Offset averaging uses every z from -q through q, for 24,028 identities. +- Matrix quotients: the six matrices and moduli are explicit in + `verify.py` and `EXPECTED.json`. Each check covers all vectors in its + full residue cube. Singular matrices and composite moduli are included. + The response partition is built separately from the residue image. +- Joint summaries: the denominator pairs (2,3), (3,9), and (3,7). + Every old value and translation in one least-common-multiple period + is checked. The expected state count is that period. +- Borrowed boundaries: all normalized functions on `Z/qZ`, for q=2,3,4,5. + This gives 700 functions and 82,480 input triples. The checker executes + the actual ten-record child subword emitted by pinned PR1057. It checks + helper restoration separately from additivity. Exactly q functions + pass at each group order. These finite groups check the algebraic + equivalence; they are not used as a real-valued rounding model. +- Physical accuracy: W=0 through 8, every point in the physical grid + `[-1,1]`, and integer slopes -2 through 4. Slopes outside this interval + are farther from 4/3 and cannot improve the bound. The code separately + checks the ordinary rounded map, whose error decreases with W. +- Pinned PR985: 336 signed diagonal executions for B=2 through 8, + `b=2^-B`, eight signed source choices, and three arbitrary targets. + Another 44 signed executions cover the complete four-factor borrowed + word and its literal inverse. The four exact half-grid tie cases are + checked directly against the pinned data rounder. +- Finite exact lifts: distinct optimized and balanced binary trees for factor + counts 2,3,4,5,8,16, each at lengths 1 and 3. The 22 cases compare + every prefix with a Fraction oracle, check the closed-form product, + execute the integer forward/inverse pair, and check source and helper + restoration. Each receipt gives the prefix degree, denominator, width, + and full local arithmetic/access counts. No physical tape compiler is + claimed for this comparison construction. + +The scalar classification has a second method: the proof uses the bounded +rounding error and a subgroup argument, while the finite checker builds +all differences on complete residue periods. Matrix tests compare a +direct response partition with an independently formed residue image. +The integer lift uses a free symbolic degree bound and a separate exact +rational interpreter. All methods are AI-authored; this is not independent +human review. + +## Test authoring gate + +The checks protect externally stated mathematical contracts, not code +shape. The main credible faults are a wrong data tie rule, an ignored +residue, an incomplete safe lattice, a change from boundary restoration +to whole-word inversion, a physical/grid-unit mix-up, an uncharged +denominator extension, and an omitted inverse execution. + +PR1057 already checks exact additive words and one arbitrary nonlinear +witness. It does not classify the rounded safe lattice or test the stated +finite rational and function domains. PR985/1054 check their retained +excluded-ancestor interface; they do not assert this borrowing contract. +The new checker owns those distinct statements. It uses no production +test seam, hidden flag, or altered predecessor implementation. + +Nine mathematical controls distinguish nearest-even and truncation from +the specified data rounder, reject an ignored residue and false additivity, +detect the scaled averaging output and missing exact precision, and verify +two actual escapes: reaccess with zero saved state and different grids. +The latter two controls keep the obstruction's scope honest. + +Three subprocess controls verify the real command boundary. A changed +pinned source must fail its digest check. A changed residue implementation +must fail the response equation, not an import or syntax error. An occupied +receipt path must be rejected without changing its bytes. A relocated, +read-only optimized-Python replay must return the complete expected receipt. + +## Attempts and stopping decision + +Three candidate approaches were considered before implementation. + +1. Compute a child on a zero target, copy its increment, then uncompute it. + This can remove target dependence if its clean array or recomputation + is paid. It does not make the rounded source increment additive. The + physical-range theorem rules out that stronger generic wrapper contract. +2. Keep exact rational residuals. A finite integer construction was executed. + It works on an embedded coarse lattice and has an explicit denominator + and width bill. The endpoint alone needs n log2(q) bits of fractional + resolution in this representation for n repeated coprime p/q factors. + It is not a free bounded-width + replacement for PR1054's rounded child, and no supplier bill was built. +3. Characterize the restoration equation and its precise resource escapes. + This is the selected result. The proof and complete finite domains are + finished. No search was stopped merely because a first example failed. + +Reaccess was checked as a concrete alternative. If the changed helper and +its displacement are readable, no saved residue is necessary. At the +borrowed boundary, an inverse C call recovers the old target. This also +undoes the output contribution. A complete changed schedule must retain, +recompute, or otherwise account for that contribution and prove its next +parent interface. No lower bound on all such schedules is claimed. + +The result does not establish a new rounded recursive construction, +physical hosting rule, fixed-tape implementation, supplier moment, or +integer-multiplication exponent. Full repository regeneration, the selected +cold replay, and remote CI are outside this isolated package's validation. diff --git a/research/rounded-borrowing-contract/EXPECTED.json b/research/rounded-borrowing-contract/EXPECTED.json new file mode 100644 index 0000000000..0e81f66d66 --- /dev/null +++ b/research/rounded-borrowing-contract/EXPECTED.json @@ -0,0 +1,1182 @@ +{ + "base_commit": "abdc6a7002abdbcd9e21bfc5e1a795784deacfdf", + "borrowed_probe": [ + { + "additive": 2, + "boundary_states": 16, + "group_order": 2, + "normalized_functions": 2, + "restoring": 2 + }, + { + "additive": 3, + "boundary_states": 243, + "group_order": 3, + "normalized_functions": 9, + "restoring": 3 + }, + { + "additive": 4, + "boundary_states": 4096, + "group_order": 4, + "normalized_functions": 64, + "restoring": 4 + }, + { + "additive": 5, + "boundary_states": 78125, + "group_order": 5, + "normalized_functions": 625, + "restoring": 5 + } + ], + "controls": [ + "nearest_even_is_not_the_data_rounder", + "coefficient_truncation_is_not_data_rounding", + "discarded_residue_changes_a_required_response", + "nearest_source_increment_is_not_additive", + "full_period_refutes_constant_first_differences", + "offset_averaging_returns_the_scaled_integer_map", + "readable_current_and_shift_allow_zero_summary", + "zero_precision_extension_rejects_inexact_division", + "different_input_and_output_grids_escape_integer_slope" + ], + "finite_exact_lifts": [ + { + "calls": 4, + "denominator": "9", + "factors": 2, + "invoice": { + "additions": 4, + "denominator_bits": 4, + "exact_divisions": 4, + "initial_products": 5, + "initial_reads": 5, + "initial_writes": 5, + "peak_signed_bits": 9, + "products": 4, + "source_reads": 4, + "target_reads": 4, + "writes": 4 + }, + "length": 1, + "maximum_prefix_degree": 2, + "round_trip_divisions": 8, + "signed_width_bound": 13, + "tree": [ + 0, + 1 + ] + }, + { + "calls": 4, + "denominator": "9", + "factors": 2, + "invoice": { + "additions": 12, + "denominator_bits": 4, + "exact_divisions": 12, + "initial_products": 15, + "initial_reads": 15, + "initial_writes": 15, + "peak_signed_bits": 10, + "products": 12, + "source_reads": 12, + "target_reads": 12, + "writes": 12 + }, + "length": 3, + "maximum_prefix_degree": 2, + "round_trip_divisions": 24, + "signed_width_bound": 16, + "tree": [ + 0, + 1 + ] + }, + { + "calls": 8, + "denominator": "27", + "factors": 3, + "invoice": { + "additions": 8, + "denominator_bits": 5, + "exact_divisions": 8, + "initial_products": 5, + "initial_reads": 5, + "initial_writes": 5, + "peak_signed_bits": 11, + "products": 8, + "source_reads": 8, + "target_reads": 8, + "writes": 8 + }, + "length": 1, + "maximum_prefix_degree": 3, + "round_trip_divisions": 16, + "signed_width_bound": 16, + "tree": [ + 0, + 1, + 2 + ] + }, + { + "calls": 8, + "denominator": "27", + "factors": 3, + "invoice": { + "additions": 24, + "denominator_bits": 5, + "exact_divisions": 24, + "initial_products": 15, + "initial_reads": 15, + "initial_writes": 15, + "peak_signed_bits": 13, + "products": 24, + "source_reads": 24, + "target_reads": 24, + "writes": 24 + }, + "length": 3, + "maximum_prefix_degree": 3, + "round_trip_divisions": 48, + "signed_width_bound": 19, + "tree": [ + 0, + 1, + 2 + ] + }, + { + "calls": 10, + "denominator": "27", + "factors": 3, + "invoice": { + "additions": 10, + "denominator_bits": 5, + "exact_divisions": 10, + "initial_products": 5, + "initial_reads": 5, + "initial_writes": 5, + "peak_signed_bits": 11, + "products": 10, + "source_reads": 10, + "target_reads": 10, + "writes": 10 + }, + "length": 1, + "maximum_prefix_degree": 3, + "round_trip_divisions": 20, + "signed_width_bound": 20, + "tree": [ + 0, + [ + 1, + 2 + ] + ] + }, + { + "calls": 10, + "denominator": "27", + "factors": 3, + "invoice": { + "additions": 30, + "denominator_bits": 5, + "exact_divisions": 30, + "initial_products": 15, + "initial_reads": 15, + "initial_writes": 15, + "peak_signed_bits": 13, + "products": 30, + "source_reads": 30, + "target_reads": 30, + "writes": 30 + }, + "length": 3, + "maximum_prefix_degree": 3, + "round_trip_divisions": 60, + "signed_width_bound": 22, + "tree": [ + 0, + [ + 1, + 2 + ] + ] + }, + { + "calls": 14, + "denominator": "81", + "factors": 4, + "invoice": { + "additions": 14, + "denominator_bits": 7, + "exact_divisions": 14, + "initial_products": 5, + "initial_reads": 5, + "initial_writes": 5, + "peak_signed_bits": 14, + "products": 14, + "source_reads": 14, + "target_reads": 14, + "writes": 14 + }, + "length": 1, + "maximum_prefix_degree": 4, + "round_trip_divisions": 28, + "signed_width_bound": 23, + "tree": [ + 0, + 1, + [ + 2, + 3 + ] + ] + }, + { + "calls": 14, + "denominator": "81", + "factors": 4, + "invoice": { + "additions": 42, + "denominator_bits": 7, + "exact_divisions": 42, + "initial_products": 15, + "initial_reads": 15, + "initial_writes": 15, + "peak_signed_bits": 15, + "products": 42, + "source_reads": 42, + "target_reads": 42, + "writes": 42 + }, + "length": 3, + "maximum_prefix_degree": 4, + "round_trip_divisions": 84, + "signed_width_bound": 25, + "tree": [ + 0, + 1, + [ + 2, + 3 + ] + ] + }, + { + "calls": 16, + "denominator": "81", + "factors": 4, + "invoice": { + "additions": 16, + "denominator_bits": 7, + "exact_divisions": 16, + "initial_products": 5, + "initial_reads": 5, + "initial_writes": 5, + "peak_signed_bits": 13, + "products": 16, + "source_reads": 16, + "target_reads": 16, + "writes": 16 + }, + "length": 1, + "maximum_prefix_degree": 4, + "round_trip_divisions": 32, + "signed_width_bound": 22, + "tree": [ + [ + 0, + 1 + ], + [ + 2, + 3 + ] + ] + }, + { + "calls": 16, + "denominator": "81", + "factors": 4, + "invoice": { + "additions": 48, + "denominator_bits": 7, + "exact_divisions": 48, + "initial_products": 15, + "initial_reads": 15, + "initial_writes": 15, + "peak_signed_bits": 14, + "products": 48, + "source_reads": 48, + "target_reads": 48, + "writes": 48 + }, + "length": 3, + "maximum_prefix_degree": 4, + "round_trip_divisions": 96, + "signed_width_bound": 24, + "tree": [ + [ + 0, + 1 + ], + [ + 2, + 3 + ] + ] + }, + { + "calls": 20, + "denominator": "243", + "factors": 5, + "invoice": { + "additions": 20, + "denominator_bits": 8, + "exact_divisions": 20, + "initial_products": 5, + "initial_reads": 5, + "initial_writes": 5, + "peak_signed_bits": 16, + "products": 20, + "source_reads": 20, + "target_reads": 20, + "writes": 20 + }, + "length": 1, + "maximum_prefix_degree": 5, + "round_trip_divisions": 40, + "signed_width_bound": 25, + "tree": [ + [ + 0, + 1 + ], + 2, + [ + 3, + 4 + ] + ] + }, + { + "calls": 20, + "denominator": "243", + "factors": 5, + "invoice": { + "additions": 60, + "denominator_bits": 8, + "exact_divisions": 60, + "initial_products": 15, + "initial_reads": 15, + "initial_writes": 15, + "peak_signed_bits": 17, + "products": 60, + "source_reads": 60, + "target_reads": 60, + "writes": 60 + }, + "length": 3, + "maximum_prefix_degree": 5, + "round_trip_divisions": 120, + "signed_width_bound": 27, + "tree": [ + [ + 0, + 1 + ], + 2, + [ + 3, + 4 + ] + ] + }, + { + "calls": 28, + "denominator": "243", + "factors": 5, + "invoice": { + "additions": 28, + "denominator_bits": 8, + "exact_divisions": 28, + "initial_products": 5, + "initial_reads": 5, + "initial_writes": 5, + "peak_signed_bits": 16, + "products": 28, + "source_reads": 28, + "target_reads": 28, + "writes": 28 + }, + "length": 1, + "maximum_prefix_degree": 5, + "round_trip_divisions": 56, + "signed_width_bound": 29, + "tree": [ + [ + 0, + 1 + ], + [ + 2, + [ + 3, + 4 + ] + ] + ] + }, + { + "calls": 28, + "denominator": "243", + "factors": 5, + "invoice": { + "additions": 84, + "denominator_bits": 8, + "exact_divisions": 84, + "initial_products": 15, + "initial_reads": 15, + "initial_writes": 15, + "peak_signed_bits": 17, + "products": 84, + "source_reads": 84, + "target_reads": 84, + "writes": 84 + }, + "length": 3, + "maximum_prefix_degree": 5, + "round_trip_divisions": 168, + "signed_width_bound": 31, + "tree": [ + [ + 0, + 1 + ], + [ + 2, + [ + 3, + 4 + ] + ] + ] + }, + { + "calls": 48, + "denominator": "19683", + "factors": 8, + "invoice": { + "additions": 48, + "denominator_bits": 15, + "exact_divisions": 48, + "initial_products": 5, + "initial_reads": 5, + "initial_writes": 5, + "peak_signed_bits": 24, + "products": 48, + "source_reads": 48, + "target_reads": 48, + "writes": 48 + }, + "length": 1, + "maximum_prefix_degree": 9, + "round_trip_divisions": 96, + "signed_width_bound": 41, + "tree": [ + [ + 0, + 1, + 2 + ], + 3, + [ + 4, + 5, + [ + 6, + 7 + ] + ] + ] + }, + { + "calls": 48, + "denominator": "19683", + "factors": 8, + "invoice": { + "additions": 144, + "denominator_bits": 15, + "exact_divisions": 144, + "initial_products": 15, + "initial_reads": 15, + "initial_writes": 15, + "peak_signed_bits": 25, + "products": 144, + "source_reads": 144, + "target_reads": 144, + "writes": 144 + }, + "length": 3, + "maximum_prefix_degree": 9, + "round_trip_divisions": 288, + "signed_width_bound": 43, + "tree": [ + [ + 0, + 1, + 2 + ], + 3, + [ + 4, + 5, + [ + 6, + 7 + ] + ] + ] + }, + { + "calls": 64, + "denominator": "19683", + "factors": 8, + "invoice": { + "additions": 64, + "denominator_bits": 15, + "exact_divisions": 64, + "initial_products": 5, + "initial_reads": 5, + "initial_writes": 5, + "peak_signed_bits": 23, + "products": 64, + "source_reads": 64, + "target_reads": 64, + "writes": 64 + }, + "length": 1, + "maximum_prefix_degree": 9, + "round_trip_divisions": 128, + "signed_width_bound": 40, + "tree": [ + [ + [ + 0, + 1 + ], + [ + 2, + 3 + ] + ], + [ + [ + 4, + 5 + ], + [ + 6, + 7 + ] + ] + ] + }, + { + "calls": 64, + "denominator": "19683", + "factors": 8, + "invoice": { + "additions": 192, + "denominator_bits": 15, + "exact_divisions": 192, + "initial_products": 15, + "initial_reads": 15, + "initial_writes": 15, + "peak_signed_bits": 24, + "products": 192, + "source_reads": 192, + "target_reads": 192, + "writes": 192 + }, + "length": 3, + "maximum_prefix_degree": 9, + "round_trip_divisions": 384, + "signed_width_bound": 42, + "tree": [ + [ + [ + 0, + 1 + ], + [ + 2, + 3 + ] + ], + [ + [ + 4, + 5 + ], + [ + 6, + 7 + ] + ] + ] + }, + { + "calls": 160, + "denominator": "3486784401", + "factors": 16, + "invoice": { + "additions": 160, + "denominator_bits": 32, + "exact_divisions": 160, + "initial_products": 5, + "initial_reads": 5, + "initial_writes": 5, + "peak_signed_bits": 45, + "products": 160, + "source_reads": 160, + "target_reads": 160, + "writes": 160 + }, + "length": 1, + "maximum_prefix_degree": 20, + "round_trip_divisions": 320, + "signed_width_bound": 70, + "tree": [ + [ + [ + 0, + 1 + ], + 2, + [ + 3, + 4, + 5 + ] + ], + [ + 6, + 7, + 8 + ], + [ + [ + 9, + 10, + 11 + ], + 12, + [ + 13, + 14, + 15 + ] + ] + ] + }, + { + "calls": 160, + "denominator": "3486784401", + "factors": 16, + "invoice": { + "additions": 480, + "denominator_bits": 32, + "exact_divisions": 480, + "initial_products": 15, + "initial_reads": 15, + "initial_writes": 15, + "peak_signed_bits": 45, + "products": 480, + "source_reads": 480, + "target_reads": 480, + "writes": 480 + }, + "length": 3, + "maximum_prefix_degree": 20, + "round_trip_divisions": 960, + "signed_width_bound": 72, + "tree": [ + [ + [ + 0, + 1 + ], + 2, + [ + 3, + 4, + 5 + ] + ], + [ + 6, + 7, + 8 + ], + [ + [ + 9, + 10, + 11 + ], + 12, + [ + 13, + 14, + 15 + ] + ] + ] + }, + { + "calls": 256, + "denominator": "1162261467", + "factors": 16, + "invoice": { + "additions": 256, + "denominator_bits": 31, + "exact_divisions": 256, + "initial_products": 5, + "initial_reads": 5, + "initial_writes": 5, + "peak_signed_bits": 43, + "products": 256, + "source_reads": 256, + "target_reads": 256, + "writes": 256 + }, + "length": 1, + "maximum_prefix_degree": 19, + "round_trip_divisions": 512, + "signed_width_bound": 73, + "tree": [ + [ + [ + [ + 0, + 1 + ], + [ + 2, + 3 + ] + ], + [ + [ + 4, + 5 + ], + [ + 6, + 7 + ] + ] + ], + [ + [ + [ + 8, + 9 + ], + [ + 10, + 11 + ] + ], + [ + [ + 12, + 13 + ], + [ + 14, + 15 + ] + ] + ] + ] + }, + { + "calls": 256, + "denominator": "1162261467", + "factors": 16, + "invoice": { + "additions": 768, + "denominator_bits": 31, + "exact_divisions": 768, + "initial_products": 15, + "initial_reads": 15, + "initial_writes": 15, + "peak_signed_bits": 43, + "products": 768, + "source_reads": 768, + "target_reads": 768, + "writes": 768 + }, + "length": 3, + "maximum_prefix_degree": 19, + "round_trip_divisions": 1536, + "signed_width_bound": 75, + "tree": [ + [ + [ + [ + 0, + 1 + ], + [ + 2, + 3 + ] + ], + [ + [ + 4, + 5 + ], + [ + 6, + 7 + ] + ] + ], + [ + [ + [ + 8, + 9 + ], + [ + 10, + 11 + ] + ], + [ + [ + 12, + 13 + ], + [ + 14, + 15 + ] + ] + ] + ] + } + ], + "format": 1, + "joint_census": [ + { + "classes_per_coordinate": 6, + "ratios": [ + [ + 1, + 2 + ], + [ + 1, + 3 + ] + ] + }, + { + "classes_per_coordinate": 9, + "ratios": [ + [ + 2, + 3 + ], + [ + 4, + 9 + ] + ] + }, + { + "classes_per_coordinate": 21, + "ratios": [ + [ + 4, + 3 + ], + [ + 8, + 7 + ] + ] + } + ], + "matrix_census": [ + { + "domain": 4, + "matrix": [ + [ + 1, + 0 + ], + [ + 0, + 1 + ] + ], + "q": 2, + "response_classes": 4, + "safe_residues": 1 + }, + { + "domain": 16, + "matrix": [ + [ + 2, + 0 + ], + [ + 0, + 2 + ] + ], + "q": 4, + "response_classes": 4, + "safe_residues": 4 + }, + { + "domain": 16, + "matrix": [ + [ + 1, + 1 + ], + [ + 2, + 2 + ] + ], + "q": 4, + "response_classes": 4, + "safe_residues": 4 + }, + { + "domain": 36, + "matrix": [ + [ + 2, + 3 + ], + [ + 4, + 0 + ] + ], + "q": 6, + "response_classes": 6, + "safe_residues": 6 + }, + { + "domain": 64, + "matrix": [ + [ + 1, + 2, + 3 + ], + [ + 0, + 1, + 1 + ] + ], + "q": 4, + "response_classes": 16, + "safe_residues": 4 + }, + { + "domain": 25, + "matrix": [ + [ + 0, + 0 + ] + ], + "q": 5, + "response_classes": 1, + "safe_residues": 25 + } + ], + "physical_accuracy": [ + { + "best_additive_error": "1/3", + "rounded_error": "1/3", + "source_points": 3, + "width": 0 + }, + { + "best_additive_error": "1/3", + "rounded_error": "1/6", + "source_points": 5, + "width": 1 + }, + { + "best_additive_error": "1/3", + "rounded_error": "1/12", + "source_points": 9, + "width": 2 + }, + { + "best_additive_error": "1/3", + "rounded_error": "1/24", + "source_points": 17, + "width": 3 + }, + { + "best_additive_error": "1/3", + "rounded_error": "1/48", + "source_points": 33, + "width": 4 + }, + { + "best_additive_error": "1/3", + "rounded_error": "1/96", + "source_points": 65, + "width": 5 + }, + { + "best_additive_error": "1/3", + "rounded_error": "1/192", + "source_points": 129, + "width": 6 + }, + { + "best_additive_error": "1/3", + "rounded_error": "1/384", + "source_points": 257, + "width": 7 + }, + { + "best_additive_error": "1/3", + "rounded_error": "1/768", + "source_points": 513, + "width": 8 + } + ], + "pinned_execution": { + "borrowed_calls": 22, + "borrowed_forward_and_inverse_meter": { + "divisions": 44, + "products": 0, + "reads": 176, + "tape_moves": 220, + "writes": 44 + }, + "borrowed_tree": [ + 0, + [ + [ + 1, + 2 + ], + 3 + ] + ], + "diagonal_families": [ + { + "coefficient_bits": 2, + "p": 4, + "q": 3, + "residue_states_per_coordinate": 3 + }, + { + "coefficient_bits": 3, + "p": 8, + "q": 7, + "residue_states_per_coordinate": 7 + }, + { + "coefficient_bits": 4, + "p": 16, + "q": 15, + "residue_states_per_coordinate": 15 + }, + { + "coefficient_bits": 5, + "p": 32, + "q": 31, + "residue_states_per_coordinate": 31 + }, + { + "coefficient_bits": 6, + "p": 64, + "q": 63, + "residue_states_per_coordinate": 63 + }, + { + "coefficient_bits": 7, + "p": 128, + "q": 127, + "residue_states_per_coordinate": 127 + }, + { + "coefficient_bits": 8, + "p": 256, + "q": 255, + "residue_states_per_coordinate": 255 + } + ], + "final_units": [ + -2, + -10, + -2, + 2, + -2 + ], + "initial_units": [ + -2, + -2, + -2, + 1, + -2 + ], + "leaf_executions": 380, + "literal_inverse_units": [ + -2, + -2, + -2, + 1, + -2 + ], + "width": 12 + }, + "pinned_files": 10, + "scalar_census": { + "denominators": [ + 2, + 24 + ], + "numerator_rule": "-2q<=p<=2q; gcd(p,q)=1", + "offset_identity_tests": 24028, + "ratios": 716, + "residue_response_tests": 3495180, + "signature_sha256": "a7c6223d293f8bdd5866b5ffb08c7362041977d010fac2d35acffdf8ad5e3059", + "translation_tests": 47340 + }, + "selected_context": { + "base": { + "kappa": "1661960547713947/1000000000000000000", + "primary_pr": 942 + }, + "refresh": { + "kappa": "1672188119205421/1000000000000000000", + "primary_pr": 1042 + } + } +} diff --git a/research/rounded-borrowing-contract/HANDOFF-OVERLAP.json b/research/rounded-borrowing-contract/HANDOFF-OVERLAP.json new file mode 100644 index 0000000000..10431d20a9 --- /dev/null +++ b/research/rounded-borrowing-contract/HANDOFF-OVERLAP.json @@ -0,0 +1,84 @@ +{ + "checked_utc": "2026-10-13T18:39:00Z", + "query": "repo:CrocSwap/integer-mult-bounds created:>=2026-10-13T18:20:00Z", + "matches": [ + { + "number": 1122, + "title": "Finite bit construction: compose R439 A/B/star D to 10,652 ADDs", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1122" + }, + { + "number": 1121, + "title": "Conditional κ = 0.001672965558289236: rank-seven helper ends and T16 owner packing on the seven-slot k8 word", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1121" + }, + { + "number": 1120, + "title": "Research: local block splitting excludes 49 mixed-rank patterns", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1120" + }, + { + "number": 1119, + "title": "Finite complex construction: two-sided Markowitz LPR cleanup refactorization on U8 (-2,580 macros, -37,320 real prims per orientation, seed 30, no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1119" + }, + { + "number": 1118, + "title": "Finite complex construction: CK grid-preserving circuits save 1,310 per orientation (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1118" + }, + { + "number": 1117, + "title": "Conditional κ = 0.001672846995880185: rank-seven helper ends and T16 owner packing on the seven-slot k8 word", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1117" + }, + { + "number": 1116, + "title": "Construction: restored CK helper butterflies beat the single-shear scalar floor", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1116" + }, + { + "number": 1115, + "title": "Finite complex construction: four exact U8 B-stage shear rewrites (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1115" + }, + { + "number": 1114, + "title": "Research audit: exact two-choice classification of six frame coalescences (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1114" + }, + { + "number": 1113, + "title": "Research: exclude a finite precision neighborhood of R439 matching optima", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1113" + }, + { + "number": 1112, + "title": "Independent verification: selected PR1042 finite invoice, 9 guards, 14 bootstrap steps and 94 outer slacks (seed 81, no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1112" + }, + { + "number": 1111, + "title": "Conditional κ = 0.001672780159952542: reverse one entrance promotion to fill T16 gaps", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1111" + }, + { + "number": 1110, + "title": "Research consolidation: reconcile PR225 five-stage pricing with exact intervals (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1110" + }, + { + "number": 1108, + "title": "Research: exact compact-control boundary cancellation obstruction (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1108" + } + ], + "followup": { + "number": 1108, + "head": "b76bb2853be4e7001508582b10913e32ad7aba9f", + "title": "Research: exact compact-control boundary cancellation obstruction (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1108", + "scope": "The PR description concerns an earlier-source parity law in the compact-control construction. It explicitly lists PR1057 as a different interface. This is not the rounded grid contract studied here." + }, + "coverage_limit": "New-arrival title screening plus the complete PR1108 description; not a new source review or an exhaustive novelty claim." +} diff --git a/research/rounded-borrowing-contract/LICENSE b/research/rounded-borrowing-contract/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/rounded-borrowing-contract/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/rounded-borrowing-contract/NOTICE.md b/research/rounded-borrowing-contract/NOTICE.md new file mode 100644 index 0000000000..f25d5272dd --- /dev/null +++ b/research/rounded-borrowing-contract/NOTICE.md @@ -0,0 +1,39 @@ +# Attribution and license + +Prepared for **Ali Romman (@aliromman)** with substantial **OpenAI Codex +assistance** in research, proof, implementation, checks, and text. The +coordinator reviewed the main proof separately. These are AI reviews; +no independent human or proof-assistant review is claimed. New material +is under Apache-2.0. The repository license is copied in `LICENSE`. + +- **Gareth Davidson (@bitplane), PR1057**, supplies the exact additive + three-array allocator, its uniform proof, the arbitrary nonlinear + eight-factor boundary, and the explicit backend bill. Its `borrow.py`, + proof, and notice are retained unchanged at + `78a062df1dcab2bffea5ff4d8243f3da6e465414`. This work resolves a stated + rounded-contract question. It does not claim the allocator or its + earlier nonlinear counterexample as new. +- **Ali Romman, PR985**, supplies the dirty arbitrary-stride leaf and its + exact inverse, with the later read-accounting correction. Its source, + proof, and notice are retained unchanged at + `da1cdf8ed4ac9b1b8378dfec73f77ff4e81a4f70`. +- **Ali Romman, PR1054**, supplies the conditional all-length cubic + precision proof for the retained rounded word. Its proof and notice + are retained at `6bc675be1554b3a3be771147f21f9dc2c6dae50a`. That proof + does not claim the new borrowed-ancestor interface tested here. +- The retained notices preserve credit to **shhxera / PR822** for the + excluded-ancestor nonlinear contract, **androolloyd / PR673** for the + multiway echo, **Sagar Thakrar / PR730** for the ordered optimizer, + **Chafik Boukhalfa / PR628, PR862, PR905** for the rounded and precision + lineage, **Rohan Guliani / PR846** for the cyclic decomposition, and + **Charles Bethin / PR764** for the shared-suffix estimate. Those works + have their own stated scope and attribution. +- PR1057 credits **Michael Ben-Or and Richard Cleve** for the classical + constant-register algebraic principle. This package makes no priority + claim for group homomorphisms, elementary commutators, residue classes, + rational rounding, or reversible computation. + +The contribution is the uniform rounded substitution obstruction at this +borrowed boundary, the full safe-translation lattice, and the stated sharp +resource tradeoffs. Immutable source and context hashes are in `SOURCES.json`. +Relative links in retained predecessor files refer to their original layout. diff --git a/research/rounded-borrowing-contract/OVERLAP.json b/research/rounded-borrowing-contract/OVERLAP.json new file mode 100644 index 0000000000..2bea125fca --- /dev/null +++ b/research/rounded-borrowing-contract/OVERLAP.json @@ -0,0 +1,313 @@ +{ + "checked_utc": "2026-10-13T18:30:25Z", + "queries": [ + "repo:CrocSwap/integer-mult-bounds borrowing", + "repo:CrocSwap/integer-mult-bounds rounding", + "repo:CrocSwap/integer-mult-bounds rounded in:title", + "repo:CrocSwap/integer-mult-bounds borrowing in:title" + ], + "initial_matches": [ + { + "number": 1057, + "title": "Research: exact additive echoes with three dirty arrays at any depth (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1057" + }, + { + "number": 1021, + "title": "Research: heterogeneous stage-rank rigidity for exact two-bank exchange", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1021" + }, + { + "number": 982, + "title": "Research: output-borrowed fanout with an exact scratch/work tradeoff (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/982" + }, + { + "number": 752, + "title": "Tooling: accelerate exact quadratic-affine witness replay", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/752" + }, + { + "number": 743, + "title": "Research consolidation: uniform proof of the archived 2P+1 stage bound", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/743" + }, + { + "number": 553, + "title": "[Lean] Certify PR531 ownership, controller windows and width matching", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/553" + }, + { + "number": 522, + "title": "Conditional kappa 0.001402213284556683: rank-factor coordinate totals merge 56 recursive pairs", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/522" + }, + { + "number": 466, + "title": "Conditional κ = 0.001274415506145115: complex response kernel + rank151/mixed bit word on #451 (+0.670%)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/466" + }, + { + "number": 397, + "title": "Formalize the indexed B_K scalar bridge and bind the pinned B3 word", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/397" + }, + { + "number": 471, + "title": "Conditional kappa = 0.001274548075945587: full-nine-axis kernel normalization and same-owner spectator borrowing", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/471" + }, + { + "number": 387, + "title": "Conditional kappa 0.000998634658090835: finite bootstrap and exact coarse precision", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/387" + }, + { + "number": 392, + "title": "Conditional kappa 0.001000220224856110: six fixed levels on #390", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/392" + }, + { + "number": 363, + "title": "Complex supplier b = 9.32783e-4: E8 in a seven-stage bridged word (+6.45 % over #352; no new κ, raises the complex cap)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/363" + }, + { + "number": 185, + "title": "Finite leaf bootstrap above PR182: conditional kappa = 0.000660627334074291", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/185" + }, + { + "number": 143, + "title": "Late compensation and joint frame refinement: conditional κ = 4.24830828577e-4", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/143" + }, + { + "number": 142, + "title": "Restricted h22 padded triple covers: conditional κ = 4.20151003347e-4", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/142" + }, + { + "number": 137, + "title": "Padded triple covers with sequential dirty reuse: conditional κ = 4.13596233702e-4", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/137" + }, + { + "number": 1069, + "title": "Independent verification: code-disjoint pricing of all 16 pending kappa claims; every one has deficit W - 64N (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1069" + }, + { + "number": 1060, + "title": "Construction: exact complex P111 COPY word with a smaller paid recursive moment", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1060" + }, + { + "number": 1052, + "title": "Independent verification: T37 positive-binomial moments, all-T lemma, and 1024-bit reduction (seed 78, no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1052" + }, + { + "number": 985, + "title": "Research: dirty arbitrary-stride cyclic inverse on two tapes (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/985" + }, + { + "number": 1026, + "title": "[Lean] Prove all-length cyclic Schur elimination and indexed passes (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1026" + }, + { + "number": 997, + "title": "Recursive-interface construction: signed Hadamard batch saves 126 leaf calls (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/997" + }, + { + "number": 902, + "title": "Research audit: tighter Gaussian correction-power endpoint bound (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/902" + }, + { + "number": 892, + "title": "Research: rank-eight coded-helper endpoint and complete mixed-cost obstruction (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/892" + }, + { + "number": 846, + "title": "Research: pay for preparation, execution, restoration and tape for #621's cyclic inverse at every stride (no κ claim)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/846" + }, + { + "number": 803, + "title": "Research: degree-controlled cyclic inverse bound by root reflection (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/803" + }, + { + "number": 764, + "title": "Research: sharp inverse-square rounding bound for cyclic scans", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/764" + }, + { + "number": 736, + "title": "Tooling: skip exact zero row updates in cyclic-inverse replay", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/736" + }, + { + "number": 697, + "title": "Research construction: direct-source E8 with 120 fewer helpers", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/697" + }, + { + "number": 692, + "title": "Independent verification: weighted-stride closures and bilinear dual (no kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/692" + }, + { + "number": 684, + "title": "Audit Gaussian chirp domain and exact block budgets", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/684" + }, + { + "number": 672, + "title": "Tooling: exact integer exponential intervals with pinned replay evidence", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/672" + }, + { + "number": 668, + "title": "Independent verification: exact CRT resultants through radix 27", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/668" + }, + { + "number": 667, + "title": "[Tooling] Exact integer-Horner logarithm intervals with pinned equivalence tests", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/667" + }, + { + "number": 665, + "title": "Research note: price a width-9 spectral split with dirty restoration", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/665" + }, + { + "number": 628, + "title": "Uniform rounded prime-power cyclic inversion (no κ claim)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/628" + }, + { + "number": 605, + "title": "[Lean] Prove the pinned PR588 native Real moment bound", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/605" + }, + { + "number": 489, + "title": "Replace local Gaussian inverse branches with two convolutions", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/489" + }, + { + "number": 585, + "title": "[Lean] Verify selected rational certificate arithmetic", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/585" + }, + { + "number": 481, + "title": "Batch Gaussian boundary right-hand sides to reduce their cost", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/481" + }, + { + "number": 522, + "title": "Conditional kappa 0.001402213284556683: rank-factor coordinate totals merge 56 recursive pairs", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/522" + }, + { + "number": 387, + "title": "Conditional kappa 0.000998634658090835: finite bootstrap and exact coarse precision", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/387" + }, + { + "number": 390, + "title": "E8 prefix restoration and heterogeneous helper banks: conditional kappa = 1.000220222889528e-3", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/390" + }, + { + "number": 371, + "title": "Account for final-grid rounding in the Gaussian block enclosure", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/371" + }, + { + "number": 255, + "title": "Conditional κ = 7.10465204542247e-4: fixed prime, seven finite levels and η = 10⁻²⁴ on #254", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/255" + }, + { + "number": 75, + "title": "Zero-circuit live clearing: conditional kappa = 5.14154245470094e-5 above #71", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/75" + } + ], + "recent_title_matches": [ + { + "number": 744, + "title": "Independent verification: fixed-space ternary echo minima and rounded leaves", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/744" + }, + { + "number": 628, + "title": "Uniform rounded prime-power cyclic inversion (no κ claim)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/628" + }, + { + "number": 1103, + "title": "Research: rectangular output borrowing and complete minimum-word census (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1103" + }, + { + "number": 471, + "title": "Conditional kappa = 0.001274548075945587: full-nine-axis kernel normalization and same-owner spectator borrowing", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/471" + } + ], + "metadata_pins": [ + { + "number": 1057, + "head": "78a062df1dcab2bffea5ff4d8243f3da6e465414", + "title": "Research: exact additive echoes with three dirty arrays at any depth (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1057", + "updated_at": "2026-10-13T17:23:04Z" + }, + { + "number": 1054, + "head": "6bc675be1554b3a3be771147f21f9dc2c6dae50a", + "title": "Conditional accuracy: all-length cubic precision for the dirty stride inverse", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1054", + "updated_at": "2026-10-13T17:19:01Z" + }, + { + "number": 985, + "head": "da1cdf8ed4ac9b1b8378dfec73f77ff4e81a4f70", + "title": "Research: dirty arbitrary-stride cyclic inverse on two tapes (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/985", + "updated_at": "2026-10-13T17:10:42Z" + }, + { + "number": 1103, + "head": "92822cb99a7e1a28cb9d03ae5adb8e7988f30d1c", + "title": "Research: rectangular output borrowing and complete minimum-word census (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1103", + "updated_at": "2026-10-13T18:14:09Z" + }, + { + "number": 744, + "head": "302383e0c1ec71c50860362d3f394f85664c2445", + "title": "Independent verification: fixed-space ternary echo minima and rounded leaves", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/744", + "updated_at": "2026-10-13T05:10:23Z" + } + ], + "scope_notes": { + "744": "Metadata states disjoint ancestor/child scratch pools and fixed-space ternary rounded replay. It does not claim unrestricted ancestor-port borrowing.", + "985": "Consumed exact rounded implementation at the unchanged public head.", + "1054": "Consumed accuracy proof. It retains the excluded-ancestor word.", + "1057": "Consumed exact additive allocator and proof. The rounded substitution contract is the present question.", + "1103": "Metadata states a rectangular output borrowing construction for arbitrary noncommuting operators. Its batching and minimum-word census differ from the same-grid rounded contract investigated here." + }, + "coverage_limit": "Targeted public metadata screening. PR744 and PR1103 were screened by their full PR descriptions, not by a new source replay. No exhaustive novelty claim." +} diff --git a/research/rounded-borrowing-contract/PROOF.md b/research/rounded-borrowing-contract/PROOF.md new file mode 100644 index 0000000000..dd452ddfc6 --- /dev/null +++ b/research/rounded-borrowing-contract/PROOF.md @@ -0,0 +1,384 @@ +# Rounded leaves and borrowed ports + +## 1. Result and scope + +PR1057 proves that three dirty arrays are sufficient at every echo depth +when each child is an exact additive shear. PR985 and PR1054 prove a +different interface. Their rounded leaf restores its source, and its +literal inverse reverses the call. Its increment can depend on its target. +Those statements do not give the PR1057 child contract. + +This package gives three results for that gap. + +1. A borrowed-port subword has a necessary and sufficient translation + condition. With identity neighbors, it requires additivity. A wrapper + on the same unrestricted grid cannot meet that condition and approximate + the admissible scalar inverse `x -> 4x/3` to error below `1/3` on + the full physical interval `[-1,1]`. This statement permits arbitrary + computation, restored workspace, source reads, and inverse executions. +2. For componentwise nearest rounding of `Pz/q`, the safe translations + are exactly `H={h: Ph belongs to q Z^m}`. A correction that has access + only to a saved summary of the old helper needs at least + `[Z^d:H]` summary states. The residue `Pz mod q` attains this count. + A diagonal coprime scalar needs `q^L` states for an array of length L + when the admitted source and displacement ranges contain a complete + residue domain. Smaller finite domains can need fewer states. +3. In the specified fixed-offset averaging class, a nonzero additive + result needs at least q signed calls. Exactly q calls give the + q-scaled integer map. They do not give an additive fractional map. + +The second result is an interface tradeoff, not a lower bound for all +algorithms. Section 6 pays for access to an old helper and explains this +escape. A different recursive contract, changed grids, or clean precision +extensions can also escape. No impossibility result for arbitrary rounded +programs, no new supplier, and no new kappa is claimed. + +All data arithmetic below has enough signed headroom. There is no wrap, +saturation, or overflow. All rounding is to nearest with ties toward +positive infinity, as in PR985's `rnd`. PR985's separate `trunc` function +prepares coefficients; it does not round the diagonal data output. + +## 2. The exact restoration condition at a borrowed boundary + +Let V be an abelian group. Let `A,B,C: V -> V` be deterministic maps. +On distinct rows x, y, z, put + + g_x(y) = B(y+A(x)) - B(y). + +The four leaf calls + + y += A(x); z += B(y); y -= A(x); z -= B(y) + +implement `U: z += g_x(y)` and restore y. Now use y as the output of +`W: y += C(z)`. The full outer word is `U W U^-1 W^-1`. At entry +write the rows as x, y, z, and put + + z1 = z + g_x(y), + y1 = y + C(z1), + z2 = z1 - g_x(y1). + +The final W inverse does not change z2. Thus the helper z restores for +every x, y, z if and only if + + g_x(y+c) = g_x(y) for every c in the image of C. (1) + +Necessity follows because z1 runs through all V when z does. Sufficiency +follows by substitution. Invariance under these translations is equivalent +to invariance under the subgroup generated by the image of C. This is an +exact condition; a small nonzero defect still violates restoration. + +If `A=C=identity`, (1) says that `B(y+x)-B(y)` is independent of y. +If `B(0)=0`, set y=0 to get + + B(y+x) = B(y) + B(x). (2) + +Conversely, (2) restores z and gives the usual composed shear. A constant +offset in B cancels, so the general statement applies to `B-B(0)`. + +This subword occurs inside the PR1057 allocator. In the ordered tree +`(0,((1,2),3))`, the root uses row 2 as a connector. Its right child +uses row 3. The child's `(1,2)` grandchild borrows row 1, which is the +right child's output. Set factors 1 and 3 to identity and factor 2 to B. +The displayed word is precisely this completed right-child boundary. +The external row 0 stays read-only. The probe tests restoration of an +actual lent ancestor port, not an unrelated equation for roundoff. + +The condition is necessary for this universal substitution interface. +It is not necessary for every fixed factor list. Some nonadditive factors +have safe translation subgroups that happen to contain all later updates. +Section 4 describes those subgroups. A schedule that avoids this boundary +must prove its own child interface. + +## 3. A physical-range obstruction for every same-grid wrapper + +Let `delta=2^-W`, with integer `W>=0`. Suppose a wrapper implements + + target += F(source), + +on arbitrary source and target data in `delta Z^L`. It restores all other +data and has no dependence on the incoming target or private dirt in its +completed increment. Suppose its child contract gives (2) whenever the +arguments and their sum are in `[-1,1]^L`. + +For a coordinate vector e_j, write `F(delta e_j)=delta v_j`, where v_j +has integer entries. Repeated addition inside the interval gives + + F(e_j) = 2^W F(delta e_j) = v_j. (3) + +Thus F acts as an integer matrix on the grid in this interval. If its +ideal map is the real matrix M, its error at some e_j is at least + + max_i distance(M_ij, Z). + +In particular, `M=(4/3) I` forces infinity-norm error at least `1/3` at +a physical unit input. More generally, on `[-D,D]` with D a positive +grid point, the scalar lower bound is + + D * distance(alpha, Z). + +This is not the smaller error `delta/3` at one grid step. The complete +physical input range is used in (3). Increasing W does not remove the +bound when arbitrary dirty sources can use every bit of the same grid. +The result also excludes a wrapper whose roundoff is uniformly bounded +by `C(D+1) delta` once that bound is below the displayed positive gap. + +The map `4x/3` is an actual PR985 case: use a real coefficient `b=1/4`, +stride zero, multiplier one, and `beta=1/2`. Its diagonal call returns +`rnd(4x/3,W)`, with source restoration and an exact inverse. At W=12 +the original admission `48*2^-W<=beta^3` holds. The scalar source grid +can be as fine as the working grid. Identity neighbors are also admissible +PR985 cases, with b=0. Thus this obstruction applies to a proposed generic +same-grid wrapper of the pinned leaf, not only to an arbitrary nonlinear +oracle unrelated to that implementation. + +The wrapper can use unlimited computation and restored workspace. Those +resources cannot change (3). The conclusion is narrower than saying that +rounded recursion is impossible: it excludes a wrapper that retains the +same arbitrary-grid domain, the exact additive contract, and a small +uniform approximation error at the same time. + +Ordinary guarded precision is not contradicted. If source data is restricted +to the coarser lattice `Delta Z` and output uses `delta Z`, a slope can be +an integer multiple of `delta/Delta`. Such slopes can approximate 4/3. +However, a borrowed ancestor port with arbitrary incoming fine-grid dirt +does not satisfy that coarser-source restriction. An implementation must +preserve or create that restriction and pay for it. Section 7 gives one +finite exact extension with explicit width costs. + +## 4. The complete safe-translation lattice + +Let P be an integer `m by d` matrix and let `q>=1`. Define + + R(t) = floor(t+1/2), + F(z) = R(Pz/q), z in Z^d, + +where R acts on each component. A translation h is safe when +`F(z+h)-F(z)` is independent of z for every z in Z^d. + +Then + + h is safe <=> Ph belongs to q Z^m. (4) + +For sufficiency, use `R(t+k)=R(t)+k` for integer k. For necessity, let +the constant difference be c. Iteration gives `F(kh)=F(0)+kc=kc` for +every positive integer k. The rounding error in `F(kh)-kPh/q` has +each component at most 1/2 in absolute value. Divide by k and let k +increase. This gives `c=Ph/q`. Since c has integer entries, (4) follows. + +For a reduced scalar `p/q`, the safe translations are exactly qZ. For +the diagonal map on L independent coordinates, they are `q Z^L`. +The same proof applies to floor, ceiling, or any bounded rounder with +integer-translation covariance and F(0)=0. It does not cover nearest-even +ties without a separate period analysis. + +For the scalar nearest rounder, a finite complete test is sufficient: +the differences at z=0,...,q-1 are constant if and only if q divides h. +They repeat with period q. Their sum is ph, because `F(z+q)=F(z)+p`. +If they are constant, that integer constant must be ph/q. Coprimality +then gives q dividing h. This justifies the finite census in the checker. + +## 5. Exact residual summaries and their sharp state count + +Specify the following correction interface. The entry helper is z. Before +that value becomes unavailable, an encoder stores E(z). Later the adapter +receives E(z), a displacement h, and the immutable rounding descriptor. It +must return `F(z+h)-F(z)` exactly for every z and h. It cannot reread z or +an equivalent value from which z can be recovered. This restriction is +part of the theorem, not a property of every borrowing program. + +Two helpers z,z' have the same complete response function if and only if +`z'-z` is safe. To prove the forward direction, rearrange equality of the +responses to get + + F(z'+h)-F(z+h) = F(z')-F(z) for every h. + +The variable `z+h` runs through the whole domain. This is exactly the +safe-translation condition. The reverse direction follows from the same +identity. Therefore E must distinguish all cosets of H. At least +`[Z^d:H]` states, or `ceil(log2 [Z^d:H])` bits, are necessary. + +They are sufficient. Store the componentwise residue `r=Pz mod q`, with +`0<=r_i=2`. The diagonal slope is the reduced ratio +`2^B/(2^B-1)`, and `beta=1/2` is valid. The exact residual summary needs +`(2^B-1)^L` states, hence at least `ceil(L log2(2^B-1))` bits. A constant +number of B-bit scalar registers cannot hold this summary for arbitrary L. +This gives a concrete price for one proposed repair; it does not require +the entire P-bit original helper when B is much smaller than P. + +For finite physical data, require a complete residue system in the allowed +range. For example, take `W>=max(B,9)` and physical grid `delta=2^-W`. +The integers `z,h=0,...,q-1` represent physical old helpers and shifts +below one; the evaluated sums are below two. All q scalar response +classes are distinct on these finite sets. Thus the q^L count already +holds in that bounded physical range. At a fixed W whose admitted source +set has fewer than q entries, do not claim q states. The correct lower +bound is the number of distinct response functions on the specified +source and displacement sets. + +For several coprime scalar ratios `p_i/q_i`, one summary that supports all +their responses has safe subgroup `lcm(q_i) Z` per coordinate. Its exact +minimum is `lcm(q_i)^L` states. This can exceed each separate q_i count. + +## 6. Reaccess, replay, and fixed-offset averaging + +The summary lower bound does not apply when z+h and h are both readable: +one subtraction recovers z. The checker includes this zero-summary escape. +At the actual boundary of Section 2, the state after W is `(x,y1,z1)`. +The old y is exactly `y1-C(z1)`. A full `W^-1` recovers it with one +negative C execution. If a coordinate evaluator for C is available, one +can instead pay for that evaluator and each source read. A dense scalar +map can make this cheap. There is no claimed general lower bound on that +evaluation cost. + +After `W^-1 U^-1`, however, both y and z are back at entry. The desired +output change is gone. Keeping `C(z1)` in a new array uses L values. A +replay can compute it again, but must also retain the old/new state needed +for the subtraction and prove restoration at the next parent. Such calls, +reads, arrays, and clean scalar work must be in its new recurrence. This +package does not assert that no cheaper changed schedule exists. + +Even a successful local correction cannot make an accurate same-grid +fractional increment additive: Section 3 still applies. Thus rereading +the helper can escape the summary bound, but cannot validate an unchanged +use of the PR1057 additive induction. It needs a different child contract. + +One concrete changed schedule removes base dependence by fixed offsets. +Consider the class + + H(z) = sum_j epsilon_j [F(z+t_j)-F(t_j)], + +where each `epsilon_j` is +1 or -1 and each integer offset t_j is fixed +independently of z. Count each signed occurrence as one variable call; +constant preparation and source movement are additional costs. Let +`S=sum_j epsilon_j`. Since the roundoff is bounded, `H(z)-(Sp/q)z` +is bounded on all integers. If H is additive, it has an integer slope a. +It follows that `a=Sp/q`. For coprime p,q this requires q to divide S. +If a is nonzero, the number of variable calls is at least `|S|>=q`. +In particular, S=1 cannot produce an additive fractional approximation. + +The q-call bound is attained by offsets 0,...,q-1, all with positive +sign. The residues `pr mod q` form a permutation. Direct summation of +the q floors gives + + sum_(r=0)^(q-1) [F(z+r)-F(r)] = pz. (6) + +This is the q-scaled integer map. Dividing a dirty target by q is not a +free final step; it changes its arbitrary old contents and reintroduces +a fractional/residual contract. For `b=2^-B`, (6) needs `2^B-1` calls. +It is exponential in the descriptor width B before source scans, inverse +passes, constant preparation, head travel, or scalar cleanup are charged. +It cannot serve as a polynomial-in-B repair within this averaging class. + +The bound does not cover adaptive offsets, extra nonlinear oracles, or +arbitrary programs. It does cover arbitrary integer signed combinations +of a fixed finite collection of translated rounded evaluations. + +## 7. A finite exact-lift escape and its width bill + +Exact rational arithmetic of unbounded height is not an implementation. +The following bounded construction states what an exact lift would cost +for repeated scalar p/q leaves. It is an interface comparison, not a fast +cyclic inverse or a supplier. + +Fix a finite PR1057 word with N leaf records. Regard its linear state as +polynomials in noncommuting factor symbols, with each initial row a +separate symbol. Let D be the largest factor degree at any prefix. Each +record increases degree by at most one, so `D<=N`. D can exceed the +number n of factors at the root; do not assume `D=n` for borrowed ports. + +Represent each row by an integer numerator with common denominator +`Q=q^D`. Initialize a coarse-grid integer entry z as zQ. For a leaf, +perform + + target_numerator += sign * p * source_numerator / q. + +Every indicated division is exact. Before a multiplication by p/q, each +source monomial has degree at most D-1; its numerator contains a factor +q. This proves the assertion at every record. PR1057's exact additive +proof then restores every helper and gives the exact product. A literal +inverse executes the reversed records with opposite signs. + +This construction restricts every incoming array to the embedded coarse +lattice. It pays for extra precision in all `L(S+2)` data entries, where +S is the dirty-array count. If the original integer entries have norm at +most M and `K>=max(1,|p/q|)`, use PR1057's prefix bound H. Numerator data +need signed width + + 1 + bit_length(ceil(M H q^D)). + +The scalar product needs a further `ceil(log2(max(1,|p|)))` bits. Store +q and Q, and pay for preparation of Q. Initialization requires one source +read, one multiplication by Q, and one write per data entry. Each leaf +requires L source reads, L target reads, L writes, L products by p, L +exact divisions by q, and L additions. Add control, coefficient reads, +source routing, tape movement, and scalar initialization/restoration for +the chosen backend. These are not supplied as unit-cost pointer actions. + +The final output can be rounded once. Its initial coarse-grid target is +an integer, so nearest rounding commutes with adding it. Discarding the +output residue is a paid irreversible operation; a bit-reversible +implementation must retain or uncompute it. The helper extensions are +already restored to their initial embedded values. + +Even the endpoint gives a lower bound for this exact-lift class. With +source 1 and n repeated coprime p/q factors, the exact output is +`p^n/q^n`. A common-denominator representation must have Q divisible by +q^n. Its fractional resolution thus costs at least `n log2 q` bits. With +arbitrary integer target data, each numerator word must also hold the +target times Q. The finite prefix can require more. This is a width bound +for the specified representation, not for compressed symbolic values. It does not +prove the same bound for approximate arithmetic or for a special kernel +whose factors cancel denominators. + +The checker executes this finite-width integer construction and compares +it with a separate Fraction oracle. It records the actual D, widths, +leaf counts, division count, and accesses. This is exact-grid evidence +for the stated class, not a fixed-tape compiler or an unbounded rational +substitution for a rounded algorithm. + +## 8. Kappa and remaining work + +The selected source at the experiment base has conditional +`kappa=1661960547713947/10^18`. Its complex supplier binds. No selected +record or source changes here. The three-array saving of PR1057 changes +storage; it does not change that word's child multiplicities. Its inherited +direct all-role moment obstruction remains. + +During this work, main advanced to +`ba82555c64e1879e4b7decce28186f208fcb8262`. Its selected record names +PR1042 and `kappa=1672188119205421/10^18`. The package preserves both +selected records as immutable context. The experiment still starts at +`abdc6a7002abdbcd9e21bfc5e1a795784deacfdf`; it does not claim that the +older selected record remains current. + +The new result closes the generic same-grid exact-additive wrapper route +for nonintegral rounded factors. A residue repair has an explicit array +cost under the summary interface. Fixed-offset averaging has a sharp +denominator-dependent call cost. An exact lift has explicit growing +precision and initialization costs. None supplies a useful complete +supplier recurrence. PR1054's cubic precision proof applies to its retained +excluded-ancestor word, not automatically to one of these changed words. + +A future contribution can escape through a proved restricted translation +lattice, different input/output grids with paid initialization, or a new +nonadditive restoration invariant and complete work/accuracy recurrence. +The present proof does not exclude those routes. Finite checks below +support the uniform arguments; they are not a formal proof of the full +multiplication theorem. diff --git a/research/rounded-borrowing-contract/README.md b/research/rounded-borrowing-contract/README.md new file mode 100644 index 0000000000..dd5d9a671c --- /dev/null +++ b/research/rounded-borrowing-contract/README.md @@ -0,0 +1,69 @@ +# Rounded child restoration under port borrowing + +**Status: scoped obstruction and resource tradeoff. No new kappa.** + +A generic same-grid rounded wrapper cannot satisfy PR1057's exact additive +child contract with arbitrarily small uniform error. On a working grid +`delta Z`, additivity forces an integer slope. For the valid PR985 leaf +`x -> 4x/3`, the error is at least `1/3` on the physical interval `[-1,1]`, +independent of the number of guard bits. A coarser source grid, a different +output grid, or a new recursive contract can escape this result. + +The [proof](PROOF.md) identifies the precise borrowed boundary. It also +classifies all safe translations of componentwise nearest rounding of +`Pz/q`: they are exactly the integer vectors h with `Ph=0 mod q`. +This gives a sharp saved-residue state count when the old helper cannot +be reread. On a complete residue domain, a diagonal coprime p/q leaf +needs q^L states for length L. For a bounded physical grid, the allowed +source and displacement ranges must contain that complete domain. +The proof explicitly covers reaccess and replay as escapes from that +summary-only bound; it does not claim a general memory lower bound. + +A fixed-offset averaging repair needs at least q signed variable calls +to obtain a nonzero additive result. The q-call construction attains the +bound but returns the q-scaled integer map. A separate bounded integer +lift demonstrates the clean precision extension that can make exact +arithmetic safe; its denominator, data widths, initialization, inverse +calls, and accesses are paid. + +Run from the repository root with Python 3.9 or newer and the standard +library: + +```sh +python3 -I -B research/rounded-borrowing-contract/verify.py +python3 -I -B research/rounded-borrowing-contract/test_package.py +``` + +The second command runs the first from a read-only copy under optimized +Python and checks three command failures. It prints: + +```text +PASS_ROUNDED_BORROWING_CONTRACT ratios=716 responses=3495180 rounded_leaves=380 exact_lifts=22 controls=9 +PASS_ROUNDED_BORROWING_PACKAGE controls=3 relocation=1 +``` + +The receipt also covers all 700 normalized functions on the cyclic groups +of orders 2 through 5 at the actual borrowed child boundary, six matrix +quotients, three joint-denominator families, and physical input grids +through 8 fractional bits. These are finite checks of the written proof. +They are not a formal proof of the full multiplication theorem. + +The actual PR985 replay uses its nearest rule with ties upward. Its +four-factor rounded witness differs from PR1057's eight-factor arbitrary +nonlinear witness. The witness is supporting evidence; the contribution +is the uniform contract, lattice, and resource results. The complete +literal inverse restores the state even when the positive call changes +a helper, which separates whole-word reversibility from helper restoration. + +Experiment base: `abdc6a7002abdbcd9e21bfc5e1a795784deacfdf`. +Dependencies: PR1057 `78a062df1dcab2bffea5ff4d8243f3da6e465414`, PR985 +`da1cdf8ed4ac9b1b8378dfec73f77ff4e81a4f70`, and PR1054 +`6bc675be1554b3a3be771147f21f9dc2c6dae50a`. Only immutable vendored files +and context copies are hashed; a changing root selected record is not a +runtime input. During this work, main `ba82555c64e1879e4b7decce28186f208fcb8262` +selected PR1042 at conditional `kappa=1672188119205421/10^18`. + +See [COVERAGE.md](COVERAGE.md) for the finite domains, check ownership, +limits, and failed approaches. [NOTICE.md](NOTICE.md) preserves predecessor +credit and discloses substantial OpenAI Codex assistance. The selected +frontier and `upstream/` are unchanged. diff --git a/research/rounded-borrowing-contract/SOURCES.json b/research/rounded-borrowing-contract/SOURCES.json new file mode 100644 index 0000000000..f1d3e0ee13 --- /dev/null +++ b/research/rounded-borrowing-contract/SOURCES.json @@ -0,0 +1,75 @@ +{ + "base_commit": "abdc6a7002abdbcd9e21bfc5e1a795784deacfdf", + "files": [ + { + "path": "vendor/pr1057/borrow.py", + "commit": "78a062df1dcab2bffea5ff4d8243f3da6e465414", + "source_path": "research/linear-port-borrowing/borrow.py", + "git_blob": "b5014c9eb26adad166e4021a430eebfc2ca10d55", + "sha256": "14f267a3a6b85b08f0d23326cdb6de8c27f70ad8d156359c01fdf93bf19682d0" + }, + { + "path": "vendor/pr1057/PROOF.md", + "commit": "78a062df1dcab2bffea5ff4d8243f3da6e465414", + "source_path": "research/linear-port-borrowing/PROOF.md", + "git_blob": "96e13812019eaf39a86b265ca96c552300bfbe15", + "sha256": "790fb2c67d9e59c7e80e212cb025d643a5315636f977ab9269e96cc7eef5556e" + }, + { + "path": "vendor/pr1057/NOTICE.md", + "commit": "78a062df1dcab2bffea5ff4d8243f3da6e465414", + "source_path": "research/linear-port-borrowing/NOTICE.md", + "git_blob": "e718ab189a0eb51cb1bdadf0f898598f72815600", + "sha256": "1f8ce68b254b6c40fe6255bffd2975ef8cf7c0df1de7414cd59353eea80f1e37" + }, + { + "path": "vendor/pr985/dirty_stride.py", + "commit": "da1cdf8ed4ac9b1b8378dfec73f77ff4e81a4f70", + "source_path": "research/dirty-stride-source-reuse/dirty_stride.py", + "git_blob": "027108871df4564156b600ea20c37e66697ca4b6", + "sha256": "941b8499a290bd08199c1ac4a6f90ef0e031be0f6249a60db2b6604900f2255a" + }, + { + "path": "vendor/pr985/PROOF.md", + "commit": "da1cdf8ed4ac9b1b8378dfec73f77ff4e81a4f70", + "source_path": "research/dirty-stride-source-reuse/PROOF.md", + "git_blob": "01a3da73470dc773a33948ee5f8cfc8848798411", + "sha256": "af6560b048b20649aebd31d68815948a104d2c87efcdf556c85a10f48bbc0489" + }, + { + "path": "vendor/pr985/NOTICE.md", + "commit": "da1cdf8ed4ac9b1b8378dfec73f77ff4e81a4f70", + "source_path": "research/dirty-stride-source-reuse/NOTICE.md", + "git_blob": "66338a4d0fddae2710b12c80264fbad772e25d3a", + "sha256": "82f9d5b0610ee3f5d6dbc7e93c8e439556013d6e0effe2b7623dd63d5e21cf43" + }, + { + "path": "vendor/pr1054/PROOF.md", + "commit": "6bc675be1554b3a3be771147f21f9dc2c6dae50a", + "source_path": "research/dirty-stride-precision/PROOF.md", + "git_blob": "89cde9241919e479708146e07afe031fda100ea9", + "sha256": "11c23a39b91fe6acbda1d7f0e3aa640a983b106ac4733ae03530d79c952d6919" + }, + { + "path": "vendor/pr1054/NOTICE.md", + "commit": "6bc675be1554b3a3be771147f21f9dc2c6dae50a", + "source_path": "research/dirty-stride-precision/NOTICE.md", + "git_blob": "10dd84845b8b4ee59ee6eb315033028b04c6c239", + "sha256": "d8059542dc8b2cebe6747a1334f2e03b97311dc4210d32b8f177c2ceb6b5c485" + }, + { + "path": "context/base-selected-result.json", + "commit": "abdc6a7002abdbcd9e21bfc5e1a795784deacfdf", + "source_path": "certificates/selected-result.json", + "git_blob": "3d7529d77a5f22d8c6f64f98bd5a0e71b8eee892", + "sha256": "1d35283cb0ce3f8db1f285683933517f9e87475d295e2b6316399ad9928c81c3" + }, + { + "path": "context/refresh-selected-result.json", + "commit": "ba82555c64e1879e4b7decce28186f208fcb8262", + "source_path": "certificates/selected-result.json", + "git_blob": "f451ced6626a1f03aba6915ce23a136b01ebe51d", + "sha256": "207d1f49f113c585024b9d3c17eadbb8b1be17c1321e3d190aabe2f18ce1c5b7" + } + ] +} diff --git a/research/rounded-borrowing-contract/VALIDATION.json b/research/rounded-borrowing-contract/VALIDATION.json new file mode 100644 index 0000000000..8ba987ed41 --- /dev/null +++ b/research/rounded-borrowing-contract/VALIDATION.json @@ -0,0 +1,64 @@ +{ + "base_regressions": { + "checkout_commit": "abdc6a7002abdbcd9e21bfc5e1a795784deacfdf", + "commands": [ + "make selected-record-check", + "python3 -I -B -m unittest discover -s tests -p 'test_selected*.py'" + ], + "selected_record": "PASS", + "selected_unit_test_seconds": 1.078, + "selected_unit_tests": 25 + }, + "coordinator_replay": "The coordinator separately ran the real verify.py command and obtained the same PASS counts. The coordinator reviewed the written proof. These are AI checks, not independent human review.", + "experiment_base": "abdc6a7002abdbcd9e21bfc5e1a795784deacfdf", + "final_text_changes": "After the code checks, the summary and proof stated the finite-domain residue requirement in explicit form. The README command location was corrected. No tested Python file or expected result changed.", + "normal_command": { + "command": "python3 -I -B research/rounded-borrowing-contract/verify.py --output /tmp/kappa9-rounded-normal-receipt.json", + "output": "PASS_ROUNDED_BORROWING_CONTRACT ratios=716 responses=3495180 rounded_leaves=380 exact_lifts=22 controls=9", + "receipt_equals_expected": true + }, + "not_run": [ + "Full make verify", + "Selected cold replay", + "Remote CI", + "Physical fixed-tape compiler", + "Proof-assistant verification" + ], + "package_command": { + "command": "python3 -I -B research/rounded-borrowing-contract/test_package.py --output /tmp/kappa9-rounded-package-validation.json", + "output": "PASS_ROUNDED_BORROWING_PACKAGE controls=3 relocation=1", + "receipt": { + "command_controls": [ + "changed_pinned_source_rejected", + "discarded_residue_rejected_at_response_contract", + "occupied_output_rejected_without_change" + ], + "python": "3.14.7 (main, Aug 5 2026, 10:29:49) [Clang 21.0.0 (clang-2100.1.1.101)]", + "relocated_read_only_optimized_python": true, + "seconds": 19.665149, + "status": "PASS" + } + }, + "resolved_packaging_failure": "The first real command rejected an equal receipt because nested tuples were compared with JSON lists. The owner now compares canonical JSON, as required for proof-relevant payload equality. The normal and relocated optimized commands then passed.", + "runtime": { + "python": "3.14.7 (main, Aug 5 2026, 10:29:49) [Clang 21.0.0 (clang-2100.1.1.101)]", + "system": "macOS-26.6.1-arm64-arm-64bit-Mach-O", + "thread_limit_environment": { + "OMP_NUM_THREADS": "1", + "OPENBLAS_NUM_THREADS": "1", + "VECLIB_MAXIMUM_THREADS": "1" + } + }, + "scope": "The written proof and exact finite checks establish the stated restoration contract and resource tradeoffs. They do not establish a new rounded recursive supplier or a new kappa.", + "status": "PASS", + "tested_files_sha256": { + "EXPECTED.json": "7a7da31f29151a7d01920835905d4776c2251a55f445267def2b90ba1e9322b2", + "PROOF.md": "ec941e11023b79b0e4987869cbea64271f2938c4a686bfb62b65bd3b6c5a710d", + "README.md": "4c2d8e745b9036fc769ae75cbbf7cc1dfaef34e37de39729a147e78219460c67", + "SOURCES.json": "62a201160146b30911ebf83606cde131295454ba911647a7f41b2634a72f1c82", + "contracts.py": "bef12e6cd14fdf864f2df07152e1fef619359beca042dbe2fcac2458ef33c142", + "test_package.py": "1976b09fe671e07abab5649022f7692f6d3618c14a5f0979d9750d4c07a85297", + "verify.py": "37de1dbadcb67ca055838cf3b1253ae1a5f27ea144271d8d8e6cecccf1726eb4" + }, + "validation_date_utc": "2026-10-13" +} diff --git a/research/rounded-borrowing-contract/context/base-selected-result.json b/research/rounded-borrowing-contract/context/base-selected-result.json new file mode 100644 index 0000000000..3d7529d77a --- /dev/null +++ b/research/rounded-borrowing-contract/context/base-selected-result.json @@ -0,0 +1,177 @@ +{ + "status": "Maintainer-reviewed conditional finite construction; see the integration receipt for publication and PR resolution status", + "kappa": "1661960547713947/1000000000000000000", + "decimal": "0.001661960547713947", + "source_prs": [ + 942, + 890, + 870, + 869, + 858, + 799, + 741, + 699, + 685, + 676, + 664, + 660, + 659, + 656, + 655, + 653, + 658, + 649, + 645, + 635, + 589, + 555, + 545, + 626, + 623, + 622, + 620, + 617, + 615, + 604, + 601, + 596, + 592, + 591, + 593, + 599, + 588, + 543, + 584, + 586, + 583, + 582, + 579, + 576, + 575, + 574, + 571, + 569, + 568, + 567, + 564, + 562, + 561, + 559, + 558, + 552, + 550, + 548, + 541, + 535, + 510, + 503, + 531, + 523, + 493, + 514, + 507, + 484, + 496, + 505, + 522, + 520, + 472, + 458, + 445, + 442, + 425, + 433, + 370, + 361, + 315 + ], + "source_manifest": "research/community-frontier942-audit/SELECTED-SOURCE.json", + "certificate": "research/community-frontier942-audit/ASSEMBLY.json", + "certificate_sha256": "4b2894956e594e408e111d806c842f2ed2c32aefcadff93fad69ff0b46f1991a", + "proof": "docs/research/community-batch952-review.md", + "proof_supplements": { + "research/e8-bit-r420/README.md": "9807be57c6adf26b30e4f54e2f8160075bbc05091f1a6d157e43d2a4620c1c9f", + "research/complex-571-free4fc8/NOTICE.md": "a4c084abdc1c7a9ac683eeb11124335d51cff8a6deba6ee92ba5a12bceaa2c97", + "research/complex-multicold/proof/CONSTRUCTION.md": "27ece5e1c11b90d97a808b56eff897b998c10e61016db95867f84e6e6aef132f", + "research/complex-multicold/vendor/pr559/PROOF.md": "d5d498edc56fdef8c5798af7f5ec66948bd2f66c553b9efe366cdaab01bd3453", + "research/structural-gain/frontier-composition/README.md": "70f0f791cbe3b2603f85d85bb9055aa0ee1df6dc06ba82fc1921356948312887", + "research/complex-joint-prefix/proof/CONSTRUCTION.md": "a92e610e7a598d99c612d1b63d1a03a49c0cd1e15ddd29fa55c465ddd8c18105", + "research/kernel-frame-coalescing/PROOF.md": "fa8b2f36b9590ee80ff45d3f7724f8c7de8ad29a29f366d5133010c77e41fe1b", + "research/complex-571-hpeq5/README.md": "4000b37f6c07c09d971dc4010ceb137c13340f3a8809d3272046ccaf746c3e2b", + "research/hyperplane-end-lean/PROOF.md": "1cbce5cf0ff0152f71e8ae7bef25841d1ce13010af248ff7209182d2328c21c9", + "docs/research/community-hyperplane599-review.md": "3298cd0d451541508af232cac72efbd7c10580e6c6ad493a855ab0faa01ade8c", + "research/complex-571-cold14-b3/README.md": "1945785785c153c7d0e8d4c071adabe626c1091b71721ff85d2d67191b376b96", + "research/complex-571-cold14-b3/PROOF-NOTE.md": "1cf592cbc8ab8e21d2dd8c1e945a5c64c6d5cde1216fb06e05a36c1c6ec6613d", + "scripts/verify_cold617_interface.py": "95d7a9094c05ad975fb72f5ab7605593003245a503c8456764987e512028fa6a", + "docs/research/community-cold617-review.md": "b3f2bcbae1249f1f651032022ce1e6e2bfb3f563ce580bf53671f50a074d7046", + "research/complex-k492-owner-repair/README.md": "ee5a1ace4828f7a073be97e95c2d931988774dd3a29a877e65abdf429aeec902", + "research/complex-k492-owner-repair/PROOF-NOTE.md": "337d70fe7abd9afca1d90954c23bde87f4dc27888cc1a6b4bb80506fd6fbf8c5", + "research/complex-k492-owner-repair/PROOF-NOTE-R.md": "22312bb347bdf159e6a01a45c47675e6170d33b258e2fd9ed52aee88fb92c0ed", + "docs/research/community-k492-review.md": "3b731d30e80010b15408a289b0b32192700885474c8b36d48ee3320a7a8c5c47", + "scripts/verify_frontier626.py": "2207bd0ef04a19ef276869085afdedad80a0938fa75db5e1aa7ab73fd3429444", + "scripts/verify_frontier626_bindings.py": "cda63ff41c6d6e2e352c7bf75b84e690c0ce57e4ec6c0355573bb5d9b1f98280", + "scripts/verify_frontier588_bindings.py": "6d1932eea7b1936598118ea8e607b09c29b6e31b749ec41bbe0744ea4f0b606d", + "scripts/verify_hpe_lean_binding.py": "52aa1d23641e4c716b43c98f6b883ad042087dd03a9d01369e8e6a735b07aa03", + "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean": "eebf3a3982af7ab9be45777b272a6aaa523206fa7667ceb6df63ad6589fd8183", + "docs/research/community-frontier741-review.md": "4634694fa75ea9e749ecf19d3db3e4d82effe3b61a2efdf08ac5a97275fb676a", + "research/complex-sw4-frame8/PROVENANCE.md": "c7648719b01dd93af2c3a2c6e951a54711d13892dc4bd4339d16edb4c37c9bf0", + "research/e8-bit-p111-tuned/tune/README.md": "46c7917fb252949f38b7bcd88cf568efc282e3ea065b61d11e457e41673d0b2d", + "scripts/verify_frontier741.py": "215ee6a12de8dc2392e6811a1b8f2140035f6b2d2a0d2100ff4bd2fdcb8bb39b", + "scripts/verify_frontier741_bindings.py": "eff455167e2fd0bc9a67d35241d0e69d8edc58f3a23e776dcfe8f500ca8e8d67", + "docs/research/community-frontier799-review.md": "bd91c10c67f2a873fd456b95cbb43f715a43dac0e0a66938737d591c6b754052", + "scripts/verify_frontier799.py": "19fe1b32079095160dc00fe2f7df75e0fcbc82cff37f7159b755c8a63bd5ce99", + "scripts/verify_frontier799_bindings.py": "43897b3c99212d6134870898a1840f32898aa1b3679b299e654901568ad7e19b", + "research/gauge44-frames-x/PROOF-NOTE-FRAMES-X4.md": "39c50420ebb6e8813706a49b2cf759f277c4afac9f6780fc0a7ac6a5fb86e036", + "docs/research/community-frontier890-review.md": "cd03b7c2c6c09db2cfa89ae40133ae44e1deb6e32ec5ddd23aacecc9c50f2fea", + "scripts/verify_frontier890.py": "88ea38dbef62dd7c0dd46e212618520cc89213edddb2032800e5509993958175", + "scripts/verify_replay_coverage.py": "babe5941d7e6dac4248613ef01f950ee7bb6199e7355021aea4cf854fd1b91c5", + "scripts/verify_frontier741_bridge_coverage.py": "9a14f26762b6126eb54ed43db90371773374fe98733ada80ee871a74afa3b836", + "certificates/replay-coverage/pr741-sw4-v1.json": "7acd5033bc78e3f473718269edaa267c2785d84fbe95ccf6815a33dcf58c2756", + "research/complex-t21-owners/PROOF.md": "78721b32fceb34b21b8e77c95381c38c60276e72e6d9c2e9c6262cb347457def", + "research/complex-t21-owner-bound/PROOF.md": "2aa0aa6ec1d87402138564c38749b5ca0f058c16817efdf58a2685d2d90cb417", + "research/gauge44-barch/PROOF-NOTE-BARCH.md": "c24f211b09358b25d6cf47dd18e4bbd8bcf4ecf279e6f1c6c90613cfa230818d", + "research/complex-double-replica-owners/PROOF.md": "db99599e3966bec253c577c23915e2a2899c4c4e8568044efc11c7918b137bbc", + "docs/research/community-batch952-review.md": "04db59dfc2c31453229b6061bbf59547e71ce3abdc0ce0f6779144bb0dde127b", + "scripts/verify_frontier942.py": "27c6713532d9f53f55dfff4884d55a2d9ae74b68156e37a44596c0418fbed5b7", + "research/complex-t37-owners/PROOF.md": "09b39ad0d5f1f59f54dcff15c16640f7a7acf27e6597660acaf957b95c7e8510", + "research/complex-t37-owners/ALL-T-PROOF.md": "4c0c71ccd0afb850538af1b467e5208b7eb3edd0260fded84e02a8c01dfc868b", + ".github/workflows/t37-owners.yml": "c13acc2902c007237103072b7ec10caf5ca21c1b319d27934f194af2f7d87026" + }, + "review": "docs/research/community-batch952-review.md", + "validation": "docs/research/community-batch952-integration.json", + "reproduce": "make frontier942-verify", + "scope": "U8/T37 finite composition with 1024-bit complex prefix allowance and complete source-bound baseline coverage; explicit reused ancestry recorded. Inherited all-size/compiler, common-label/mutable-source, whole-call hosting, precision/tape, analytic and bit H1-H5 obligations remain. Not a full Lean multiplication theorem; Linux integration CI tracked separately.", + "previous_kappa": "1661957774647029/1000000000000000000", + "previous_record": "certificates/checkpoints/frontier890.json", + "audited_source_head": "1960cfa919a0945d0ca4cb14ea96237000037903", + "reviewed_dependency_heads": { + "588": "6d0e53b66c29abd17981881a09eaff41ac862d85", + "543": "2065fe4f72a914d907f1046603f5a36f17018535", + "568": "71c99ac935a33bb7b59a1b4a7af8725a939b0b90", + "569": "1424da81263a5305b35e4cf74ef686c275f03f3f", + "571": "b7bdc5a8de18fcf418cfb9c7d83a2b1097a5e4a3", + "575": "eac6f7e378ab622dac50a2fd4b7ef6eab014de44", + "583": "89be768f0157f5a3d8e4db69cf1748768605eac9", + "586": "4846fee5b06af770e9b3a10c36200f673d656725", + "591": "f622547244bf6d895a571a7b035142ba66279806", + "592": "1f471c445c06a45a32e2c47e8d74c8264b68356b", + "593": "fdb6dcc6d7bc29764c5b6b4d32b7fa050acf74a4", + "596": "7732dd5e46863ff294b5e443661cb9d99abf4e01", + "599": "bc13c8a3e000442606bd2dbe8583a17649ba6c32", + "601": "529ab7dcb59d5ea7a5798e9e06cf5b3aee8a1550", + "604": "1b795c5d7dea746ba310572585c0ef067574b4a6", + "615": "bf8a49a34350599763cced8592db81dc62c2c1c0", + "617": "904d62855723c00f8acef9a287a10768598fdeb2", + "622": "f69477f4f6d3c7eb1f740b166881bffed4ffa9f6", + "623": "e39a615ca601ce5d62abeb24f3fcdb8644ca1005", + "626": "660de893d27bb7abd1d5b01b1640207528a5c851", + "589": "a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46", + "741": "e516b1463606840a15f80aac1995d64ce0092e89", + "799": "80e6463157cfc80b85af09e7e2f14748fe2dac60", + "858": "ae2e25fee91540c83ceee5a60e3b07422ce21c7d", + "869": "73e86f69bf9a391e3c334999f7bbe3825dc42759", + "870": "b734850dc348800942f0ffd1f0723fdec7539b2b", + "890": "4b3bd8cbe8e3e81c44161017c9b72c905a8040a8", + "942": "1960cfa919a0945d0ca4cb14ea96237000037903" + } +} diff --git a/research/rounded-borrowing-contract/context/refresh-selected-result.json b/research/rounded-borrowing-contract/context/refresh-selected-result.json new file mode 100644 index 0000000000..f451ced662 --- /dev/null +++ b/research/rounded-borrowing-contract/context/refresh-selected-result.json @@ -0,0 +1,194 @@ +{ + "status": "Maintainer-reviewed conditional finite construction; see the integration receipt for publication and PR resolution status", + "kappa": "1672188119205421/1000000000000000000", + "decimal": "0.001672188119205421", + "source_prs": [ + 1042, + 1031, + 1028, + 1022, + 1018, + 1005, + 1004, + 987, + 942, + 890, + 870, + 869, + 858, + 799, + 741, + 699, + 685, + 676, + 664, + 660, + 659, + 656, + 655, + 653, + 658, + 649, + 645, + 635, + 589, + 555, + 545, + 626, + 623, + 622, + 620, + 617, + 615, + 604, + 601, + 596, + 592, + 591, + 593, + 599, + 588, + 543, + 584, + 586, + 583, + 582, + 579, + 576, + 575, + 574, + 571, + 569, + 568, + 567, + 564, + 562, + 561, + 559, + 558, + 552, + 550, + 548, + 541, + 535, + 510, + 503, + 531, + 523, + 493, + 514, + 507, + 484, + 496, + 505, + 522, + 520, + 472, + 458, + 445, + 442, + 425, + 433, + 370, + 361, + 315 + ], + "source_manifest": "research/community-frontier1042-audit/SELECTED-SOURCE.json", + "certificate": "research/community-frontier1042-audit/ASSEMBLY.json", + "certificate_sha256": "093f35445812ea96fe1bfe6a3af7d769cb7f274e08f4fb30f71a17ed1161e54e", + "proof": "docs/research/community-batch1047-review.md", + "proof_supplements": { + "research/e8-bit-r420/README.md": "9807be57c6adf26b30e4f54e2f8160075bbc05091f1a6d157e43d2a4620c1c9f", + "research/complex-571-free4fc8/NOTICE.md": "a4c084abdc1c7a9ac683eeb11124335d51cff8a6deba6ee92ba5a12bceaa2c97", + "research/complex-multicold/proof/CONSTRUCTION.md": "27ece5e1c11b90d97a808b56eff897b998c10e61016db95867f84e6e6aef132f", + "research/complex-multicold/vendor/pr559/PROOF.md": "d5d498edc56fdef8c5798af7f5ec66948bd2f66c553b9efe366cdaab01bd3453", + "research/structural-gain/frontier-composition/README.md": "70f0f791cbe3b2603f85d85bb9055aa0ee1df6dc06ba82fc1921356948312887", + "research/complex-joint-prefix/proof/CONSTRUCTION.md": "a92e610e7a598d99c612d1b63d1a03a49c0cd1e15ddd29fa55c465ddd8c18105", + "research/kernel-frame-coalescing/PROOF.md": "fa8b2f36b9590ee80ff45d3f7724f8c7de8ad29a29f366d5133010c77e41fe1b", + "research/complex-571-hpeq5/README.md": "4000b37f6c07c09d971dc4010ceb137c13340f3a8809d3272046ccaf746c3e2b", + "research/hyperplane-end-lean/PROOF.md": "1cbce5cf0ff0152f71e8ae7bef25841d1ce13010af248ff7209182d2328c21c9", + "docs/research/community-hyperplane599-review.md": "3298cd0d451541508af232cac72efbd7c10580e6c6ad493a855ab0faa01ade8c", + "research/complex-571-cold14-b3/README.md": "1945785785c153c7d0e8d4c071adabe626c1091b71721ff85d2d67191b376b96", + "research/complex-571-cold14-b3/PROOF-NOTE.md": "1cf592cbc8ab8e21d2dd8c1e945a5c64c6d5cde1216fb06e05a36c1c6ec6613d", + "scripts/verify_cold617_interface.py": "95d7a9094c05ad975fb72f5ab7605593003245a503c8456764987e512028fa6a", + "docs/research/community-cold617-review.md": "b3f2bcbae1249f1f651032022ce1e6e2bfb3f563ce580bf53671f50a074d7046", + "research/complex-k492-owner-repair/README.md": "ee5a1ace4828f7a073be97e95c2d931988774dd3a29a877e65abdf429aeec902", + "research/complex-k492-owner-repair/PROOF-NOTE.md": "337d70fe7abd9afca1d90954c23bde87f4dc27888cc1a6b4bb80506fd6fbf8c5", + "research/complex-k492-owner-repair/PROOF-NOTE-R.md": "22312bb347bdf159e6a01a45c47675e6170d33b258e2fd9ed52aee88fb92c0ed", + "docs/research/community-k492-review.md": "3b731d30e80010b15408a289b0b32192700885474c8b36d48ee3320a7a8c5c47", + "scripts/verify_frontier626.py": "2207bd0ef04a19ef276869085afdedad80a0938fa75db5e1aa7ab73fd3429444", + "scripts/verify_frontier626_bindings.py": "cda63ff41c6d6e2e352c7bf75b84e690c0ce57e4ec6c0355573bb5d9b1f98280", + "scripts/verify_frontier588_bindings.py": "6d1932eea7b1936598118ea8e607b09c29b6e31b749ec41bbe0744ea4f0b606d", + "scripts/verify_hpe_lean_binding.py": "52aa1d23641e4c716b43c98f6b883ad042087dd03a9d01369e8e6a735b07aa03", + "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean": "eebf3a3982af7ab9be45777b272a6aaa523206fa7667ceb6df63ad6589fd8183", + "docs/research/community-frontier741-review.md": "4634694fa75ea9e749ecf19d3db3e4d82effe3b61a2efdf08ac5a97275fb676a", + "research/complex-sw4-frame8/PROVENANCE.md": "c7648719b01dd93af2c3a2c6e951a54711d13892dc4bd4339d16edb4c37c9bf0", + "research/e8-bit-p111-tuned/tune/README.md": "46c7917fb252949f38b7bcd88cf568efc282e3ea065b61d11e457e41673d0b2d", + "scripts/verify_frontier741.py": "215ee6a12de8dc2392e6811a1b8f2140035f6b2d2a0d2100ff4bd2fdcb8bb39b", + "scripts/verify_frontier741_bindings.py": "eff455167e2fd0bc9a67d35241d0e69d8edc58f3a23e776dcfe8f500ca8e8d67", + "docs/research/community-frontier799-review.md": "bd91c10c67f2a873fd456b95cbb43f715a43dac0e0a66938737d591c6b754052", + "scripts/verify_frontier799.py": "19fe1b32079095160dc00fe2f7df75e0fcbc82cff37f7159b755c8a63bd5ce99", + "scripts/verify_frontier799_bindings.py": "43897b3c99212d6134870898a1840f32898aa1b3679b299e654901568ad7e19b", + "research/gauge44-frames-x/PROOF-NOTE-FRAMES-X4.md": "39c50420ebb6e8813706a49b2cf759f277c4afac9f6780fc0a7ac6a5fb86e036", + "docs/research/community-frontier890-review.md": "cd03b7c2c6c09db2cfa89ae40133ae44e1deb6e32ec5ddd23aacecc9c50f2fea", + "scripts/verify_frontier890.py": "88ea38dbef62dd7c0dd46e212618520cc89213edddb2032800e5509993958175", + "scripts/verify_replay_coverage.py": "babe5941d7e6dac4248613ef01f950ee7bb6199e7355021aea4cf854fd1b91c5", + "scripts/verify_frontier741_bridge_coverage.py": "9a14f26762b6126eb54ed43db90371773374fe98733ada80ee871a74afa3b836", + "certificates/replay-coverage/pr741-sw4-v1.json": "7acd5033bc78e3f473718269edaa267c2785d84fbe95ccf6815a33dcf58c2756", + "research/complex-t21-owners/PROOF.md": "78721b32fceb34b21b8e77c95381c38c60276e72e6d9c2e9c6262cb347457def", + "research/complex-t21-owner-bound/PROOF.md": "2aa0aa6ec1d87402138564c38749b5ca0f058c16817efdf58a2685d2d90cb417", + "research/gauge44-barch/PROOF-NOTE-BARCH.md": "c24f211b09358b25d6cf47dd18e4bbd8bcf4ecf279e6f1c6c90613cfa230818d", + "research/complex-double-replica-owners/PROOF.md": "db99599e3966bec253c577c23915e2a2899c4c4e8568044efc11c7918b137bbc", + "docs/research/community-batch952-review.md": "04db59dfc2c31453229b6061bbf59547e71ce3abdc0ce0f6779144bb0dde127b", + "scripts/verify_frontier942.py": "27c6713532d9f53f55dfff4884d55a2d9ae74b68156e37a44596c0418fbed5b7", + "research/complex-t37-owners/PROOF.md": "09b39ad0d5f1f59f54dcff15c16640f7a7acf27e6597660acaf957b95c7e8510", + "research/complex-t37-owners/ALL-T-PROOF.md": "4c0c71ccd0afb850538af1b467e5208b7eb3edd0260fded84e02a8c01dfc868b", + ".github/workflows/t37-owners.yml": "c13acc2902c007237103072b7ec10caf5ca21c1b319d27934f194af2f7d87026", + "docs/research/community-batch1047-review.md": "a6271faf5db0afe3ff7d24a34a3be7a959cdc33ee37784572fba014ee5358787", + "scripts/verify_frontier1042.py": "700fdcaeb6e8f57f6e63c71c2dd1652fc5b183e8d706cd092779bdc0d271e854" + }, + "review": "docs/research/community-batch1047-review.md", + "validation": "docs/research/community-batch1047-integration.json", + "reproduce": "make frontier1042-verify", + "scope": "Finite composition under inherited all-size/compiler, common-label/mutable-source, whole-call hosting, precision/tape, analytic and bit H1-H5 assumptions. Not a full Lean multiplication theorem.", + "previous_kappa": "1661960547713947/1000000000000000000", + "previous_record": "certificates/checkpoints/frontier942.json", + "audited_source_head": "7e8ef087c02a77038a28a337a7ee3a77039cac0d", + "reviewed_dependency_heads": { + "588": "6d0e53b66c29abd17981881a09eaff41ac862d85", + "543": "2065fe4f72a914d907f1046603f5a36f17018535", + "568": "71c99ac935a33bb7b59a1b4a7af8725a939b0b90", + "569": "1424da81263a5305b35e4cf74ef686c275f03f3f", + "571": "b7bdc5a8de18fcf418cfb9c7d83a2b1097a5e4a3", + "575": "eac6f7e378ab622dac50a2fd4b7ef6eab014de44", + "583": "89be768f0157f5a3d8e4db69cf1748768605eac9", + "586": "4846fee5b06af770e9b3a10c36200f673d656725", + "591": "f622547244bf6d895a571a7b035142ba66279806", + "592": "1f471c445c06a45a32e2c47e8d74c8264b68356b", + "593": "fdb6dcc6d7bc29764c5b6b4d32b7fa050acf74a4", + "596": "7732dd5e46863ff294b5e443661cb9d99abf4e01", + "599": "bc13c8a3e000442606bd2dbe8583a17649ba6c32", + "601": "529ab7dcb59d5ea7a5798e9e06cf5b3aee8a1550", + "604": "1b795c5d7dea746ba310572585c0ef067574b4a6", + "615": "bf8a49a34350599763cced8592db81dc62c2c1c0", + "617": "904d62855723c00f8acef9a287a10768598fdeb2", + "622": "f69477f4f6d3c7eb1f740b166881bffed4ffa9f6", + "623": "e39a615ca601ce5d62abeb24f3fcdb8644ca1005", + "626": "660de893d27bb7abd1d5b01b1640207528a5c851", + "589": "a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46", + "741": "e516b1463606840a15f80aac1995d64ce0092e89", + "799": "80e6463157cfc80b85af09e7e2f14748fe2dac60", + "858": "ae2e25fee91540c83ceee5a60e3b07422ce21c7d", + "869": "73e86f69bf9a391e3c334999f7bbe3825dc42759", + "870": "b734850dc348800942f0ffd1f0723fdec7539b2b", + "890": "4b3bd8cbe8e3e81c44161017c9b72c905a8040a8", + "942": "1960cfa919a0945d0ca4cb14ea96237000037903", + "1004": "1974578f82a30158dd5fcdcdf226b83df8e7196f", + "1005": "779e80aef469bc3a28b19f1adde199871a9a22e3", + "1018": "eac7547cb191f875d5f5ea5f9bbb1d2b8c51c4ef", + "1022": "58618bcbfe88a252467755fc283c04c3db5ca4fd", + "1028": "be4bd89cb4483dcee43257200cd27601f938f13d", + "1031": "e900534f0beda892c726723524203b97471fb9a3", + "1042": "7e8ef087c02a77038a28a337a7ee3a77039cac0d" + } +} diff --git a/research/rounded-borrowing-contract/contracts.py b/research/rounded-borrowing-contract/contracts.py new file mode 100644 index 0000000000..db8e4767ce --- /dev/null +++ b/research/rounded-borrowing-contract/contracts.py @@ -0,0 +1,92 @@ +"""Exact integer operations for the contracts in PROOF.md. + +Prepared for Ali Romman with substantial OpenAI Codex assistance. +Apache-2.0. See NOTICE.md for source credit. +""" + + +def nearest(numerator, denominator): + """Round a rational number to nearest, with ties toward positive infinity.""" + if denominator <= 0: + raise ValueError("positive denominator required") + return (2 * numerator + denominator) // (2 * denominator) + + +def residue_response(p, q, residue, shift): + """Use a saved numerator residue to recover the exact output difference.""" + if not 0 <= residue < q: + raise ValueError("canonical residue required") + return nearest(residue + p * shift, q) - nearest(residue, q) + + +def offset_sum(p, q, value): + """Use all q residue offsets and subtract their prepared constants.""" + return sum(nearest(p * (value + r), q) - nearest(p * r, q) + for r in range(q)) + + +def replay(word, state, leaf): + """Execute signed shears on a copied scalar state.""" + result = list(state) + for source, target, factor, sign in word: + result[target] += sign * leaf(factor, result[source]) + return result + + +def inverse(word): + return [(s, t, i, -sign) for s, t, i, sign in reversed(word)] + + +def prefix_degree(word, rows): + """Keep every initial-row symbol and every ordered factor word.""" + state = [{((), i): 1} for i in range(rows)] + degree = 0 + for source, target, factor, sign in word: + for (factors, origin), coefficient in state[source].items(): + monomial = ((factor,) + factors, origin) + value = state[target].get(monomial, 0) + sign * coefficient + if value: + state[target][monomial] = value + degree = max(degree, len(monomial[0])) + else: + state[target].pop(monomial, None) + return degree + + +def exact_lift(word, initial, p, q, degree): + """Execute the word on integer numerators with denominator q**degree. + + The returned counts exclude the verifier's copied state. A backend must + also pay for routing, coefficients, control, scalar work, and preparation. + """ + if q < 1 or degree < 0: + raise ValueError("positive denominator and nonnegative degree required") + denominator = q ** degree + state = [[value * denominator for value in row] for row in initial] + peak = max(abs(value) for row in state for value in row) + entries = sum(map(len, initial)) + count = { + "initial_reads": entries, + "initial_products": entries, + "initial_writes": entries, + "source_reads": 0, + "target_reads": 0, + "writes": 0, + "products": 0, + "exact_divisions": 0, + "additions": 0, + } + for source, target, factor, sign in word: + for j in range(len(state[source])): + product = p * state[source][j] + quotient, remainder = divmod(product, q) + if remainder: + raise ValueError("exact lift needs more denominator precision") + state[target][j] += sign * quotient + peak = max(peak, abs(product), abs(state[target][j])) + for key in ("source_reads", "target_reads", "writes", "products", + "exact_divisions", "additions"): + count[key] += 1 + count["peak_signed_bits"] = peak.bit_length() + 1 + count["denominator_bits"] = denominator.bit_length() + return state, denominator, count diff --git a/research/rounded-borrowing-contract/test_package.py b/research/rounded-borrowing-contract/test_package.py new file mode 100644 index 0000000000..6af9aa9df1 --- /dev/null +++ b/research/rounded-borrowing-contract/test_package.py @@ -0,0 +1,97 @@ +#!/usr/bin/env python3 +"""Run the checker from a read-only copy and check command failures.""" +import argparse +import json +import os +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import time + +ROOT = Path(__file__).resolve().parent + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def command(root, extra=()): + env = dict(os.environ) + env.update(OPENBLAS_NUM_THREADS="1", OMP_NUM_THREADS="1", VECLIB_MAXIMUM_THREADS="1") + return subprocess.run([sys.executable, "-I", "-O", "-B", str(root / "verify.py"), *extra], + cwd=root.parent, env=env, text=True, capture_output=True, + timeout=180) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, help="write validation metadata to a new path") + args = parser.parse_args() + if args.output and args.output.exists(): + raise FileExistsError("validation path already exists") + started = time.monotonic() + controls = [] + with tempfile.TemporaryDirectory(prefix="rounded borrowing checks ") as temporary: + folder = Path(temporary) + relocated = folder / "read only package" + shutil.copytree(ROOT, relocated, ignore=shutil.ignore_patterns("__pycache__")) + try: + for path in relocated.rglob("*"): + path.chmod(0o555 if path.is_dir() else 0o444) + relocated.chmod(0o555) + receipt = folder / "fresh receipt.json" + result = command(relocated, ("--output", str(receipt))) + need(result.returncode == 0, "relocated command failed: " + result.stderr) + need(json.loads(receipt.read_text()) == json.loads((ROOT / "EXPECTED.json").read_text()), + "relocated receipt differs") + print(result.stdout, end="") + finally: + relocated.chmod(0o755) + for path in relocated.rglob("*"): + path.chmod(0o755 if path.is_dir() else 0o644) + + bad_source = folder / "changed source" + shutil.copytree(ROOT, bad_source, ignore=shutil.ignore_patterns("__pycache__")) + source = bad_source / "vendor/pr1057/borrow.py" + source.write_bytes(source.read_bytes() + b"\n# Source fault for the command control.\n") + result = command(bad_source) + need(result.returncode != 0 and "source digest mismatch" in result.stderr, + "changed source was not rejected by its digest guard") + controls.append("changed_pinned_source_rejected") + + bad_residue = folder / "discarded residue" + shutil.copytree(ROOT, bad_residue, ignore=shutil.ignore_patterns("__pycache__")) + owner = bad_residue / "contracts.py" + text = owner.read_text() + original = "return nearest(residue + p * shift, q) - nearest(residue, q)" + need(text.count(original) == 1, "residue mutation target is not unique") + owner.write_text(text.replace(original, "return nearest(p * shift, q)")) + result = command(bad_residue) + need(result.returncode != 0 and "saved residue response failed" in result.stderr, + "discarded residue did not fail at the response contract") + controls.append("discarded_residue_rejected_at_response_contract") + + occupied = folder / "occupied receipt.json" + original_bytes = b"keep this existing receipt\n" + occupied.write_bytes(original_bytes) + result = command(ROOT, ("--output", str(occupied))) + need(result.returncode != 0 and "receipt path already exists" in result.stderr, + "occupied output was not rejected") + need(occupied.read_bytes() == original_bytes, "occupied output was changed") + controls.append("occupied_output_rejected_without_change") + + metadata = {"status": "PASS", "command_controls": controls, + "relocated_read_only_optimized_python": True, + "python": sys.version, "seconds": round(time.monotonic() - started, 6)} + if args.output: + with args.output.open("x") as stream: + json.dump(metadata, stream, indent=2, sort_keys=True) + stream.write("\n") + print(f"PASS_ROUNDED_BORROWING_PACKAGE controls={len(controls)} relocation=1") + + +if __name__ == "__main__": + main() diff --git a/research/rounded-borrowing-contract/vendor/pr1054/NOTICE.md b/research/rounded-borrowing-contract/vendor/pr1054/NOTICE.md new file mode 100644 index 0000000000..10dd84845b --- /dev/null +++ b/research/rounded-borrowing-contract/vendor/pr1054/NOTICE.md @@ -0,0 +1,46 @@ +# Source credit and scope + +Prepared for Ali Romman (@aliromman) with substantial OpenAI Codex +assistance. One assigned research agent prepared this package in the +eight-contribution sprint. The coordinator reviews it separately. No +independent human review or formal verification is claimed. + +The new work proves the effective-depth and zero-subtree transfer for +PR985's actual constant-coefficient dirty word. It also transfers the +common-operator prefix estimate to that target-dependent rounded word, +with explicit inverse-preimage magnitude guards, exact budgets, and +supporting checks. The code changes precision admission in the leaf and +caches two validation reads. The simultaneous phase lane found the +duplicate-read accounting mismatch with an independent array observer. +That finding is credited here; the rounded data word does not change. +The source and test files are under the repository's Apache-2.0 license. + +Credit the following predecessor contributions: + +- Ali Romman, PR985, for source-prefix closure reuse, reversible block + transport on two tapes, the target-dependent rounded leaf, and its + local accuracy and complete cost proof. Its complete package is + retained unchanged in `vendor/pr985/`. +- Chafik Boukhalfa (@chafreaky), PR905, for the free-algebra prefix lemma + and its use with the common-operator subset bound in a dirty word. +- Chafik Boukhalfa, PR862, for the complementary-factor/common-isometry + estimate and cubic analytic preparation budgets. +- Chafik Boukhalfa, PR977, for effective-depth analysis of PR846's + clean-scratch solver. Its source is retained for comparison. Its + clean-scratch identity is not used as a dirty-word theorem. +- Rohan Guliani, PR846, for the Euclidean chain and closure decomposition. +- Chafik Boukhalfa, PR628, for certified kernel factors and the balanced + dirty commutator. Gareth Davidson (@bitplane), PR877, for the nonlinear + prefix perturbation method. 0xkilgore, PR663, for the exact leaf count + and restoration audit. Charles Bethin, PR764, for the shared-suffix + estimate. Ali Romman, PR621, for the retained kernel proof lineage. + +All retained notices remain in place. `SOURCES.json` gives the exact +heads, source paths, Git blobs, and SHA256 values. The proof identifies +which claims are inherited and which implications this package adds. +No priority claim is made for the classical Mahler-measure, Neumann, +variation-of-constants, or approximate-factorization methods. + +The result does not change the selected bound. It does not implement +variable site phases, a new transport scheme, a Lean proof, a fast +arithmetic compiler, a complete transform, or a multiplication reduction. diff --git a/research/rounded-borrowing-contract/vendor/pr1054/PROOF.md b/research/rounded-borrowing-contract/vendor/pr1054/PROOF.md new file mode 100644 index 0000000000..89cde92419 --- /dev/null +++ b/research/rounded-borrowing-contract/vendor/pr1054/PROOF.md @@ -0,0 +1,338 @@ +# Cubic precision for the constant-coefficient dirty stride word + +## Result and fixed interface + +This result applies to PR985 at +`9df42a99dd8497b6e7d46cd2507bb89071372640`. The unchanged source is in +`vendor/pr985/`. The new `dirty_stride.py` changes the precision admission, +adds its effective-depth formula, and caches two validation reads. It retains every rounded +operation, recursive child, block swap, coefficient computation, and head +return. In particular, it does not add an early exit or a clean data array. + +The two validation loops now read each datum once, check that cached value, +and discard it. PR985's Python expression read the same entry twice while +charging one access. The simultaneous phase lane found that mismatch with +an independent array observer. The derived source corrects it without a +new data operation or a changed validation result. An observer separate +from the meter checks every literal indexed read and write in the new +leaf and kernel executions. The original source remains unchanged. + +Let `u=2^-W`, `0=4g+16` implies (1) at every length and stride. The +unscaled leaf error remains `64 (X+1) u / beta^5` for source norm at most +`X`. For a multiplier with modulus at most `R>=1`, it is at most + + [64 R (X+1)/beta^5 + 3] u. (2) + +For the inherited certified prime-power kernels, the complete balanced +dirty word has sufficient fractional precision + + W <= max(p,w_input) + m + 18r^3, + +where every initial array has norm at most `2^m`. A sufficient signed +integer reserve per component is at most `m+15r^3`. The bound applies to +both signs of the word. Exact source and scratch restoration, two data +tapes, the logarithmic borrowed-array count, and the full PR985 movement +bill remain. No new multiplication exponent follows. + +## 1. Extinction for the coefficients that PR985 computes + +At a normalized non-base level, `0M`, that level cannot +occur. Reversal changes orientation but does not change these counts. + +PR985 computes each coefficient afresh as `power(b,e,W)`. It does not +multiply a stored array of child coefficients. Its binary powering +truncates both components toward zero after each product. Truncation +cannot increase complex modulus. Induction over the multiplication tree +therefore gives + + |power(b,e,W)| <= |b|^e. + +For `e>=2`, the returned number is on the grid of spacing `u`; the final +operation includes truncation. At level `k>=D_eff`, + + beta e >= 2^-g 2^k >= W+1, + |b|^e <= (1-beta)^e <= exp(-beta e) + <= exp(-(W+1)) < 2^-W. + +The last inequality is strict, also when `W=0`. Since `g>=1`, these +levels have `e>=2`. Each component of the returned grid number thus has +absolute value below one grid unit and must be zero. This proof uses +complex modulus and the actual truncation rule. It does not assume a +positive real coefficient, a dyadic root descriptor, or monotonicity of +individual rounded powers. Every descendant meets the same bound. The +terminal cycle exponent is also at most `M` and meets the lower bound. + +## 2. The full dirty zero subtree + +Consider a subtree in which the two prepared coefficients at every level, +including every diagonal coefficient, are zero. A causal map with zero +coefficient is the identity on both arrays. Its physical implementation +still makes all the prescribed swaps, but only permutes values temporarily. +An expansion is a causal inverse, a zero injection, and a causal map. +It is the identity, including when its target contains arbitrary data. + +At a non-base node, the closure calls are consequently adjacent inverse +maps after the identity expansions are removed. The first call adds its +result to the source prefix; the inverse sees the exact state that the +first call left. Both calls restore their tail input. The pair cancels +exactly. The baseline addition is the only remaining operation. At a +diagonal node, division by one and grid rounding leave the source value +unchanged. Thus, with the internal multiplier one, the whole subtree is +exactly `y += sign*x`. Both signs satisfy the identity. This is an +induction on the actual dirty word, not a use of PR977's clean-scratch +identity and not an assumption of target-independent rounding elsewhere. + +The identity also has an internal magnitude bound. Let the incoming source +and target norms be at most `S` and `T`. Each recursive source is an +unchanged tail of its caller's source. Its target is a disjoint prefix of +that source. No recursive source includes an already changed connector. +Each temporary connector therefore contains at most the sum of two +source values, with norm at most `2S`. The outer target has norm at most +`T+S`. The inverse sign has the same bound. All other data movement is +swaps. The peak in the entire zero subtree is at most + + max(T+S, 2S), + +independently of its structural depth. Endpoint equality alone would not +have proved this internal bound. + +For the accuracy proof only, replace each subtree at depth `D_eff` by +its exact addition. This preserves the complete rounded output. There +are now at most `min(K,D_eff)` active non-base levels. PR985's power +error, shared-suffix, coefficient mismatch, and weighted source estimates +apply to those levels without any change. The new terminal has zero +error, which satisfies the former terminal allowance `u`. Beyond the +cutoff, the actual source causal maps are identities; their weighted +source bound does not accumulate more error. The preceding magnitude +lemma also controls all data in the untruncated zero tail. This proves +(1), (2), and the use of PR985's internal forward-leaf bound below. + +No runtime subtree is removed. The structural depth, recursive call +count, two-tape movement, metadata stack, and coefficient preparation +still have their original costs. + +## 3. A length-independent sufficient threshold + +For fixed `g`, `(D_eff+1)2^-W` decreases as integer `W` increases: the +ceiling logarithm increases by at most one at a step, while the power of +two doubles. It is enough to check `W0=4g+16`. For `g>=1`, + + 4g+17 <= 2^(g+5), + D_eff(W0)+1 <= 2g+6 <= 8*2^(g-1), + 48(D_eff(W0)+1) <= 192*2^g <= 2^(g+16). + +As `beta>=2^-g`, this proves `48(D_eff+1)2^-W<=beta^3`. The first two +elementary inequalities hold at `g=1` and persist after incrementing +`g`: each right side doubles and each left side grows by at most four. + +The executable admission uses (1), which can be weaker than this simple +threshold. For example, `beta=1/2`, `W=12`, `L=5741`, `w=2378` has +`K=10` and `D_eff=5`. The original admission fails and (1) holds. The +checker executes the full rounded word on this case, checks its residual +and exact inverse, and charges every data movement. A residual check is +numerical evidence for this one input; the preceding proof covers all +lengths. + +## 4. Transfer to the actual target-dependent kernel leaves + +Let `U=tau Z_L^w`, with one immutable unit scalar `tau` shared by all +factors. Let `Q(z)=r^-1 product_j(z-rho_j)`, of degree `n=r-1`. +The outer leaf has coefficient `tau/rho_j` and multiplier `-1/rho_j`. +The inner leaf has coefficient `rho_j conjugate(tau)`, stride `-w`, +multiplier `conjugate(tau)`, and output shift `-w`. Both ideal maps are +`(U-rho_j I)^-1`. Exactly one factor also has scale `r`. These are the +maps in PR985's unchanged dispatcher, and all use the same `U`. + +Let `||Q||_1<=M_Q` and `||Q(U)^-1||<=H_Q`. PR862's complementary-factor +argument gives a norm bound for every subset of the scaled factors: + + G = max(1, r 2^n M_Q H_Q). (3) + +Indeed `product max(1,|rho_j|)<=||rQ||_1<=r M_Q` by the elementary +Mahler-measure inequality. A complementary polynomial has coefficient +norm at most `2^n r M_Q`. Multiplication by `Q(U)^-1/r` bounds the +unscaled subset inverse, and the one factor `r` is then paid. The same +unit isometry must occur in all factors; this is not a bound for +arbitrary unrelated operators. + +Use PR905's free-algebra prefix lemma for the balanced four-call word. +With `h=ceil(log2 n)`, every ideal prefix and inverse prefix has +coefficient row sum at most `C=2*3^h`, and each monomial uses a strictly +decreasing subset of factor occurrences. Its proof includes both signs +of every child word. It depends on the ideal shear word, not on the +implementation of a rounded leaf. PR985's ideal dispatcher is exactly +that word. Equation (3) therefore gives + + B = C G + +for every ideal prefix and inverse prefix, and `B^2` for every interval +propagator. The retained PR905 proof gives the universal induction. The +new contribution here is the transfer to the PR985 leaf contract and its +physical word, not a new prefix lemma. + +For a positive PR985 leaf, (2) implies error at most + + a u (||source||+1), a=68(r+1) beta^-5. (4) + +For a negative leaf, write its input target as `y` and its output as +`z`. Exact inversion of the positive word gives + + y = z + A x + delta(x,z), + z = y - A x - delta(x,z). + +The source is unchanged. The positive bound (4) holds for every target +`z`, without a target magnitude hypothesis. Thus the negative leaf has +the same error bound with the same source norm. No bound on the unknown +preimage target is used for this accuracy step. Its magnitude is paid +separately in Section 5. + +Let all initial arrays have norm at most `D0`. The exact leaf count is +`N=3qn-2q^2<=2n^2`, with `q=2^floor(log2 n)`. Let `T` be the largest +actual joint norm at complete leaf boundaries. Every computed prefix is +finite because all closure denominators have modulus at least `beta`. +Insert the actual nonlinear errors into the ideal word by variation of +constants. For either sign, the prefix bounds and (4) give + + T <= B D0 + t(T+1), t=N B^2 a u. + +If `t<=1/2`, then `T<=2 B D0+1`, and the final execution error is at most + + 2 N B^2 a u (B D0+1). (5) + +This argument uses neither linearity nor target independence of a rounded +call. Each closure and each whole-word inverse is still the exact inverse +grid word. Distinct ancestor operands and the original scratch-depth +condition remain required by the implementation. + +## 5. Integer guards, including inverse preimages + +At a leaf boundary put `D*=2 B D0+1`. PR985's forward-leaf bound is + + 512 (r+1)(D*+1)/beta^7. + +Section 2 justifies the same bound in the full zero tails. To apply it +inside an inverse leaf, first bound that leaf's positive preimage. Its +source has norm at most `D*`, and its ideal operator has norm at most +`r/beta`. Since `a u<=1` follows from `t<=1/2`, the preimage target has +norm at most + + D_pre <= (2+r/beta)D*+1. + +The inverse traverses the positive word at this preimage in reverse. +Use `D_pre+1<=(r+2)(D*+1)/beta` in the forward bound. A bound for every +data value, in either sign of every leaf, is consequently + + V = 1024 (r+1)(r+2)(B D0+1)/beta^8. (6) + +Two extra bits above `ceil(log2 V)` suffice for a signed component +reserve. This extra preimage factor is necessary in this proof; the +incoming negative target was not assumed to obey the forward preimage +bound. Block transport only moves these values and adds no new magnitude. + +## 6. Explicit prime-power budgets + +Retain the PR621/628/862 analytic and supplied factor-preparation +hypotheses. Let `r>=3` be a prime power, `n=r-1`, `ell=ceil(log2 r)`, +`h=ceil(log2 n)`, `phi=EulerPhi(r)`, and `D0<=2^m`, `m>=0`. Define + + d0 = 1+2ell+r n phi, + a0 = 2d0+r+2, + g = d0+ell+2r+2, beta=2^-g, + e = max(d0+1,a0+1,p+2a0+m+4), + b_factor = max(n ell,e+r+3). + +The original inverse has norm at most `2^a0`. The supplied dyadic-root +polynomial `Q` has coefficient error at most `2^-e`, norm at most `2^r`, +and stable factor margin `beta`. The common-isometry Neumann argument +gives `||Q(U)^-1||<=2^(a0+1)`. On a source of norm at most `2^m`, the +original-versus-prepared inverse error is at most `2^(-p-3)`. These are +inherited hypotheses and algorithms; this package does not implement +an all-size root factorizer. + +Equations (3)--(6) are paid by the integer exponents + + J = a0+2r+ell+1+2h, + A = 5g+ceil(log2(68(r+1))), + W = max(w_input,4g+16,p+3+ceil(log2 N)+A+m+3J), + I = J+m+8g+2ell+16. + +Here `B<=2^J`, `a<=2^A`, and `B D0+1<=2^(J+m+1)`. Thus (5) is at +most `2^(-p-1)`, with `t<=1/2`. Admission follows from Section 3. The +bound (6), plus a sign reserve, is below `2^I`. No incoming grid is +coarsened. Preparation plus execution error is below `2^-p`. + +For completeness, use `phi,ell,h<=r`, +`ceil(log2 N)<=1+2h`, and `ceil(log2(68(r+1)))<=ell+8`. The fractional +overhead is at most + + 11r^3-11r^2+58r+42 <= 18r^3. + +The difference is `(r-3)(7r^2+32r+38)+72`. The term `4g+16` is smaller +than this same majorant. Likewise + + I-m <= 10r^3-10r^2+52r+45 <= 15r^3, + +with difference `(r-3)(5r^2+25r+23)+24`. The inherited factor width obeys +`b_factor<=p+m+7r^3`. These polynomial identities prove the all-size +bounds; the finite budget rows check their implementation. + +At `r=64`, `p=128`, `m=20`, and `w_input=0`, the fractional budget is +`1,420,902` bits. PR985's full-word bound with the same margin and initial +norm needs `517,236,859` bits before any larger structural-depth admission. +Both words have `4,000` leaf calls and six borrowed arrays. These are +sufficient bounds, not optimal widths or measured execution times. + +## 7. Complete cost and scope + +Every leaf still uses two data arrays, a constant number of clean complex +arithmetic registers, and `O(log^2 L)` integer metadata bits. PR985 proves +at most `1280L` scalar products and divisions and `4096L` record moves +per leaf, including the complete structural recursion and returns. The +kernel retains `h` arbitrary dirty arrays and routes all of them over +two physical tapes. Its unchanged bound is + + 8192 (N+1)(h+2)L + +data-record moves. The effective depth is only for error analysis. It +must not replace structural depth in these resource counts. + +Let `A_word=W+I` and let `B_desc` include the actual immutable root, +margin, multiplier, and unit-gauge descriptor lengths. Let `M(s)` pay +for rounded multiplication and division of words of width `s`. The bill +remains + + preparation + O(N L M(A_word+B_desc)) + + O(N(h+2)L(A_word+B_desc)) + O(NL). + +The last term pays the inherited integer-control bound. Reading a stride +descriptor longer than `O(log L)` is additional input work. The supplied +preparation bill is `soft-O(r^3(p+m+r^3))` under the retained algorithms. +An arbitrarily long exact gauge description remains an extra charge. +There is no new coefficient array, tape, or borrowed data allocation. + +This is a written accuracy proof with exact-rational supporting checks. +It is not a Lean proof, a fast arithmetic compiler, a measured runtime +gain, a variable-site-phase construction, a complete transform, or a +multiplication reduction. The selected certificate and `upstream/` do +not change. Source credit and substantial AI assistance are in `NOTICE.md`. diff --git a/research/rounded-borrowing-contract/vendor/pr1057/NOTICE.md b/research/rounded-borrowing-contract/vendor/pr1057/NOTICE.md new file mode 100644 index 0000000000..e718ab189a --- /dev/null +++ b/research/rounded-borrowing-contract/vendor/pr1057/NOTICE.md @@ -0,0 +1,42 @@ +# Attribution and license + +Prepared for **bitplane** with substantial **OpenAI Codex assistance** in +mathematical reasoning, implementation, verification and writing. No +independent human review or formal verification is claimed. No delegated +agent was used. New files are Apache-2.0 under the copied repository LICENSE. + +- **shhxera, PR822**: sibling-connector reuse, the strong nonlinear contract, + its ancestor-target counterexample, fixed-budget optimizer and exact + comparison implementation. Original `reuse.py`, `PROOF.md` and `NOTICE.md` + are retained byte-for-byte at commit + `8c5e1b557f59bca29139c4c2dcc65edfb808372b`; Git blobs and SHA-256 digests + appear in SOURCES.json. Their historical relative links refer to the + original package layout. The new emitter adapts that credited echo word + and changes its allocator and admissible contract. +- **androolloyd, PR673**: multiway dirty echo, nonlinear restoration analysis + and the direct all-role integration obstruction. **Sagar Thakrar + (@thakrarsagar), PR730**: ordered binary/ternary dynamic programming and + the reserved-connector comparison. **Chafik Boukhalfa (@chafreaky), PR628**: + rounded inverse leaves and the binary commutator. All predecessor credits + retained in the original PR822 notice continue to apply. +- **Michael Ben-Or and Richard Cleve**, *Computing Algebraic Formulas Using a + Constant Number of Registers*, SIAM J. Comput. 21(1), 54–58 (1992), + [doi:10.1137/0221006](https://epubs.siam.org/doi/abs/10.1137/0221006): + prior constant-register algebraic computation. No priority is claimed + for the general principle or the elementary transvection identity. +- **Alexander Schwartzman (@AlexS-scale), PR784**, and **bitplane, PR887**: + the reserved-tree scratch/call lower bound and its Lean formalization + concern a different allocator. **bitplane, PR896**: formalized nonlinear + restoration for the excluded-ancestor interface, also a different contract. +- **Jerry Chen (@CubeJerry), PR889**; **Ross Richardson, PR982**; and + **CinnaDavis1337isnot1337, PR997**, together with PR934/943/944, provide + concurrent common-factor, output-borrowing and signed source batching. + Those inspected interfaces are comparison context, not source inputs or + a claim that this package improves their query bounds. +- The selected PR942 result remains credited to **Jonathan Capalbo + (@jon314159)** and all supplier, owner and predecessor contributors in + its retained maintainer review. Its frontier and assumptions are unchanged. + +The new scope is exact additive ancestor-port borrowing with a globally +protected external source, independent noncommuting replay, an explicit +nonlinear failure boundary and a fully stated conditional backend bill. diff --git a/research/rounded-borrowing-contract/vendor/pr1057/PROOF.md b/research/rounded-borrowing-contract/vendor/pr1057/PROOF.md new file mode 100644 index 0000000000..96e1381201 --- /dev/null +++ b/research/rounded-borrowing-contract/vendor/pr1057/PROOF.md @@ -0,0 +1,238 @@ +# A fixed pool under an exact additive contract + +## Contract and allocator + +Let V be an abelian group and let A_0,...,A_(n-1) be exact additive +endomorphisms of V. A leaf on distinct rows s,t performs +`row[t] += q A_i(row[s])`, with q in {+1,-1}, restoring its source and its +separately supplied private workspace. There are no aliased row views, +mutable coefficient descriptors, hidden state, concurrent observers or +exceptions midway through a leaf. Coefficients and descriptors are read-only. +Represented arithmetic is exact, with sufficient headroom. This is stronger +than merely requiring a reversible shear with a deterministic nonlinear +increment. Factors need not commute. + +Global row zero is the external input. Row one is the output. For ternary +and binary nodes, retain the fixed mutable pool `{1,2,3,4}` and choose k-1 +connectors from it after excluding the current source and target. The fixed +priority `[2,3,1,4]` specifies the emitted addresses. Every child receives +this same global pool; ancestor ports may be selected when they are not that +child's immediate ports. Global row zero is never a connector or target. + +At most two pool rows are excluded, leaving at least two connectors. Thus +three dirty rows suffice for every finite ordered binary/ternary tree. +For binary-only trees the pool `{1,2,3}` leaves at least one connector, so +two dirty rows suffice. These are upper bounds, not necessity claims. +Small trees can use fewer. No row copy, row initialization or row clear +occurs when a physical row is lent to another invocation. + +The external input is read-only at every prefix. An internal invocation's +source is guaranteed restored **on return**; deeper descendants can modify +it temporarily. This weaker internal source interface is part of the change. +Leaf calls still have distinct immediate ports and preserve their immediate +source throughout that atomic leaf. + +## Induction and the echo word + +Induct on the supplied finite tree. A leaf satisfies the contract. At an +internal node, let B_i be the ordered product represented by child i. By +induction, every completed child changes exactly its target by `q B_i(source)` +and restores every other row, independently of the incoming dirty values. +Consequently the state at child boundaries is precisely the state of ideal +shears on the chain of ports `(x,z_1,...,z_(k-1),y)`. Borrowing other ancestor +ports inside a child does not change these boundary maps. + +Write U_i for the shear from chain port i to port i+1. With execution order +left to right, let `C = U_0 ... U_(k-2)` and `D = U_1 ... U_(k-2)`. +Use the credited PR673/PR822 word + +``` +C; U_(k-1); inverse(C); D; inverse(U_(k-1)); inverse(D). +``` + +For k=2 the word is `U; V; U^-1; V^-1`. After U, the connector is +`z + B_0 x`. The two V calls add +`B_1(z+B_0 x) - B_1 z = B_1 B_0 x` to y, and the connector restores. + +For k=3 the word is `U; V; W; V^-1; U^-1; V; W^-1; V^-1`. +The first W reads `z_2 + B_1 z_1 + B_1 B_0 x`; the second reads +`z_2 + B_1 z_1`. Their difference is `B_2 B_1 B_0 x`. The inverse +ladders restore both connectors. No commutation of B_i is used. All +non-chain rows restore by the induction hypothesis. This proves the +positive call; reversing all leaf records and negating each sign proves +the negative call. Deterministic address selection makes this inverse +literal, even when ancestor ports are reused. + +The result holds for arbitrary initial output and dirty rows. Its essential +step is that a completed child is an additive shear independent of its +incoming private pool. PR822's nonlinear contract permits that increment +to depend on private dirt. Lending an ancestor target can then change the +increment that a later inverse call must subtract. The eight-factor +certificate exhibits this failure, rather than extending the theorem to +rounded or arbitrary nonlinear leaves. + +The general constant-register algebraic phenomenon is classical; see +Michael Ben-Or and Richard Cleve, *Computing Algebraic Formulas Using a +Constant Number of Registers*, SIAM J. Comput. 21(1), 54–58 (1992), +[doi:10.1137/0221006](https://epubs.siam.org/doi/abs/10.1137/0221006). +The contribution here is the specific allocator/contract comparison, +literal noncommuting replay and explicit resource bill, not priority for +constant-register computation. + +## Calls, planning and the comparison class + +For per-factor prices c_i valid for both signs, every occurrence, the common +precision and all required private work, a leaf has bill c_i. Binary nodes +have bill `2 W_0 + 2 W_1`; ternary nodes have bill `2 W_0 + 4 W_1 + 2 W_2`. +These include both target updates and every inverse ladder. Address-dependent +leaf costs must instead be summed over the actual emitted `(s,t,i,q)` records; +they cannot be replaced by a uniform c_i without justification. + +For unit prices, let F(1)=1. For n>1 take the minimum of + +``` +2 F(a) + 2 F(n-a), 1 <= a < n, +2 F(a) + 4 F(b) + 2 F(n-a-b), a,b >= 1, a+b < n. +``` + +Every admitted root has one listed partition, and joining minimizers attains +each candidate. Induction proves optimality within these fixed echo templates +over binary/ternary ordered trees. It says nothing about other algebraic +identities, higher arities or arbitrary programs. Ties are resolved by +`(bill, arity, split sizes)`, and leaves are labeled consecutively. + +The planner through 64 examines exactly 43,680 candidates. Its DP has O(n) +entries and O(n^3) arithmetic/comparison steps on their actual integer bit +lengths. The public routine also materializes all plans through n, using +O(n^2) tree storage; a single selected tree has O(n) nodes. Planning, tree +construction, precision calculation, coefficient preparation and word +compilation are paid separately. No reuse of planning is assumed. + +For the 56-factor chosen tree: `N = 1,568`, depth five, 91 tree nodes. +The pinned PR822 sibling allocator has S=5, while the reserved allocator +has S=9 for this same tree. PR822's exact optimizer at cap five also costs +1,568; cap four is infeasible. Its proved capacity recurrence gives +`M_4 = 29 < 56 <= M_5 = 70`. This does not contradict that theorem because +its excluded-ancestor contract has changed. A balanced binary 56-factor +tree has 3,328 calls and six reserved dirty rows; our binary allocator can +emit that different word with two dirty rows. It is a separate space/time +choice, not a claim that three arrays are minimal. + +With a fixed pool the generator uses O(h) control frames for tree depth h, +besides the read-only tree. Its Python validation/list construction and +yield propagation have the conservative record-operation bound +`O((n+N)h)`. The verifier deliberately materializes words, polynomial states +and receipts; its memory usage is not the theorem's data-space bound. + +## Exact integer headroom + +For a normed linear realization choose an integer `K >= 1` bounding every factor's induced +infinity norm. Define + +``` +H(leaf) = 1 + K, +H(node) = (k+1) K^n max_i H(child_i), +``` + +where n counts leaves below that node. At a completed-child boundary of +either the positive or negative k=2 or k=3 ladder, each chain row is a sum +of at most k+1 signed products applied to entry rows. Each product has +degree at most n; cancellation is exact. All other rows retain their entry +values. Hence the joint maximum norm is at most `(k+1) K^n` times the +node's entry norm at every such boundary. During a child, its inductively +bounded prefix multiplies this estimate by at most H(child). This proves +the displayed majorant for all prefixes, including borrowed ancestor ports. + +For a dense integer leaf, each product and each partial row sum is bounded +by K times its incoming source norm, and the final target by 1+K times the +joint incoming norm. Thus the same majorant bounds scalar work as well as +data. If initial joint norm is at most a nonnegative integer D, sufficient signed payload width is + +``` +P = bit_length(max(K, D H(root))) + 1. +``` + +The maximum includes immutable coefficient values. This uses exact integer +arithmetic; no numerical error estimate or rounded restoration follows. +The independent free-module interpreter also computes weighted coefficient +l1 norms (`K^degree` per monomial) at every leaf boundary and checks the +majorant. In the main fixture the bound gives P=119 for D=7, K=2. +Observed dense maxima are evidence for those fixtures, not a replacement +for the majorant. Intermediate products can have degree greater than n +under port borrowing (69 at n=56), so a simple `K^n` global-prefix claim +would be unjustified. + +## A complete, conditional price + +For any actual backend, the complete execution price is + +``` +planning + coefficient/descriptor preparation + word compilation ++ sum over emitted leaves of C_i(s,t,q,L,P) ++ dispatch/control + any routing/frame work outside C_i ++ private-work initialization/final restoration. +``` + +`C_i` must include source/coefficient accesses, the chosen leaf's arithmetic, +its private work and both signs at the required precision. If a supplier +requires copies, physical frame changes or additional recursive children, +they belong in C_i or an explicit additional term. Port borrowing makes no +such adapter free and does not change those supplier requirements. + +To make the accounting concrete, the certificate executes dense integer +matrix-vector leaves with four **clean scalar** P-bit work registers: +accumulator, source/target value, coefficient and product. Each matrix row +zeros its accumulator, reads L source entries and L coefficients, multiplies +and sums them, reads and updates one target entry and writes it back. After +each leaf all four scalar registers are explicitly zeroed. These are paid +ordinary assignments; no reversible-gate implementation of clearing is claimed. +The external arrays are arbitrary dirty data, while this small private/control +workspace has its separately stated clean contract. The same workspace is +charged to every allocator in the comparison. + +Per leaf this executes `L^2` multiplies, `L^2+L` add/subtracts, `L+4` scalar +zero assignments, `2L^2+L` reads and L writes: `4L^2+4L+4` commands. +Initialize the four scalar registers once as four more paid zero assignments. +No length-L copy or clear is hidden here. Distinct leaf source and target +make the row-by-row target writes safe. + +Data has `(S+2)L` P-bit cells, and read-only coefficients follow in `nL^2` +P-bit cells. Addresses are `sL+j`, `tL+i`, and +`(S+2)L+(factor*L+i)L+j`. The specified itinerary alternates source and +coefficient reads, visits the target for its read/write, and returns the +data head to address zero after **every** leaf. Literal replay and a separate +invoice calculation agree on every intercell distance. At each access a +bit head can scan a full P-bit cell and return to its left edge, adding +`2(P-1)` within-cell moves. Thus the explicit head bill is +`P * intercell_steps + 2(P-1) * accesses`, in addition to `P * accesses` +read/write bit actions. Address calculation is also paid: the receipt gives +the number of address events E and the address width a. With a specified +address routine of cost R(a) per event, add `E R(a)`. + +The read-only unrolled program has N records of +`b = max(1,ceil(log2 n)) + 2 max(1,ceil(log2(S+2))) + 1` bits. +Charge Nb bits of storage and reads and 2Nb bits of forward-and-rewind +traversal. With a specified dispatcher of cost Q(b,a,log L) per record, +add `N Q(b,a,log L)` and its control workspace. Neither the dispatcher nor +the address routine is a proven fixed-tape compiler here. They remain +explicit backend parameters, not omitted constant-time pointer operations. + +Writing M(P), A(P), Z(P) for scalar multiply, add/subtract and zero-assignment +costs, the dense arithmetic term is exactly + +``` +N L^2 M(P) + N(L^2+L) A(P) + (N(L+4)+4) Z(P). +``` + +Add the stated bit accesses/head travel, program preparation/read/travel, +`E R(a)`, `N Q(b,a,log L)`, coefficients, scalar workspace and backend control +storage. This gives an instantiated, conditional bill with no silent free +source access, restoration, scalar clearing or metadata. It does not prove +that the array saving improves runtime on another machine model. + +PR673/730/822's call obstruction for the direct all-role adapter survives: +for n>=2 these echo trees have `N >= 4n-4`, so its optimistic moment +`3N / (2 n^(1-b))` is already at least three at b=0. Our fixed-tree call +multiplicities are unchanged. Selected supplier assumptions, exact recovery, +all-size realization, physical hosting, fixed-tape and analytic transfer +obligations remain inherited or open. No selected certificate is edited. diff --git a/research/rounded-borrowing-contract/vendor/pr1057/borrow.py b/research/rounded-borrowing-contract/vendor/pr1057/borrow.py new file mode 100644 index 0000000000..b5014c9eb2 --- /dev/null +++ b/research/rounded-borrowing-contract/vendor/pr1057/borrow.py @@ -0,0 +1,152 @@ +"""Exact additive echo with ancestor ports borrowed from a fixed dirty pool. + +Apache-2.0. Prepared for bitplane with substantial OpenAI Codex assistance. +The echo word and sibling allocator are credited to PR673/730/822; see NOTICE. +""" +from functools import lru_cache + + +def leaves(tree): + if type(tree) is int and tree >= 0: + return [tree] + if not isinstance(tree, (tuple, list)) or len(tree) not in (2, 3): + raise ValueError("an ordered binary/ternary tree is required") + return [i for child in tree for i in leaves(child)] + + +def validate(tree): + ids = leaves(tree) + if ids != list(range(len(ids))): + raise ValueError("ordered consecutive leaf indices required") + return len(ids) + + +def macro(arity): + chain = [(i, 1) for i in range(arity - 1)] + inv = lambda word: [(i, -q) for i, q in reversed(word)] + return (chain + [(arity - 1, 1)] + inv(chain) + chain[1:] + + [(arity - 1, -1)] + inv(chain[1:])) + + +def instructions(tree, dirty_rows=3, sign=1): + """Yield (source, target, factor, sign); row zero is globally read-only. + + Four mutable rows suffice for all binary/ternary trees. Three suffice for + binary trees. Smaller supplied pools can fail during iteration; callers + needing atomic validation must materialize the word before executing it. + """ + validate(tree) + if type(dirty_rows) is not int or dirty_rows < 0: + raise ValueError("nonnegative integer dirty row count required") + if type(sign) is not int or sign not in (-1, 1): + raise ValueError("integer sign +1 or -1 required") + # This fixed priority makes the nonlinear boundary witness reproducible. + pool = [r for r in [2, 3, 1, 4] if r < dirty_rows + 2] + pool += list(range(5, dirty_rows + 2)) + + def emit(node, src, dst, direction): + if type(node) is int: + yield src, dst, node, direction + return + connectors = [r for r in pool if r not in (src, dst)][:len(node)-1] + if len(connectors) != len(node)-1: + raise ValueError("insufficient mutable ports") + ports = [src] + connectors + [dst] + word = macro(len(node)) + if direction < 0: + word = [(i, -q) for i, q in reversed(word)] + for i, q in word: + yield from emit(node[i], ports[i], ports[i+1], q) + + yield from emit(tree, 0, 1, sign) + + +def unit_plan(limit): + """Minimize unit leaf calls over the stated binary/ternary echo class. + + Ties use (bill, arity, split sizes). Planning is separate from execution. + """ + if type(limit) is not int or limit < 1: + raise ValueError("positive integer limit required") + bills, splits = [0, 1], [None, None] + candidates = 0 + for n in range(2, limit+1): + best = None + for a in range(1, n): + candidate = (2*(bills[a]+bills[n-a]), 2, (a, n-a)) + candidates += 1 + if best is None or candidate < best: + best = candidate + for a in range(1, n-1): + for b in range(1, n-a): + c = n-a-b + candidate = (2*bills[a]+4*bills[b]+2*bills[c], 3, (a, b, c)) + candidates += 1 + if candidate < best: + best = candidate + bills.append(best[0]) + splits.append(best[2]) + + def build(n, start=0): + if n == 1: + return start + children = [] + for size in splits[n]: + children.append(build(size, start)) + start += size + return tuple(children) + + return bills, [build(n) for n in range(1, limit+1)], candidates + + +def resources(tree): + """(leaves, calls, reserved dirty rows, sibling dirty rows, depth).""" + if type(tree) is int: + return 1, 1, 0, 0, 0 + children = [resources(t) for t in tree] + k = len(tree) + weights = [2, 2] if k == 2 else [2, 4, 2] + return (sum(r[0] for r in children), + sum(w*r[1] for w, r in zip(weights, children)), + k-1+max(r[2] for r in children), + max([k-1]+[r[3]+(1 if i in (0, k-1) else 2) + for i, r in enumerate(children)]), + 1+max(r[4] for r in children)) + + +def norm_bound(tree, factor_norm): + """Bound every prefix on the joint maximum norm, including scalar work.""" + if type(factor_norm) is not int or factor_norm < 1: + raise ValueError("positive integer factor norm required") + if type(tree) is int: + return 1+factor_norm + return ((len(tree)+1)*factor_norm**len(leaves(tree)) + * max(norm_bound(child, factor_norm) for child in tree)) + + +def reserved_instructions(tree, sign=1): + """Old fully reserved allocator, used only as an address-cost comparator.""" + validate(tree) + + def emit(node, src, dst, pool, q): + if type(node) is int: + yield src, dst, node, q + return + connectors = pool[:len(node)-1] + ports = [src]+connectors+[dst] + word = macro(len(node)) + if q < 0: + word = [(i, -s) for i, s in reversed(word)] + for i, s in word: + yield from emit(node[i], ports[i], ports[i+1], + pool[len(node)-1:], s) + + yield from emit(tree, 0, 1, list(range(2, resources(tree)[2]+2)), sign) + + +@lru_cache(None) +def balanced_binary(n, offset=0): + if n == 1: + return offset + left = n//2 + return balanced_binary(left, offset), balanced_binary(n-left, offset+left) diff --git a/research/rounded-borrowing-contract/vendor/pr985/NOTICE.md b/research/rounded-borrowing-contract/vendor/pr985/NOTICE.md new file mode 100644 index 0000000000..66338a4d0f --- /dev/null +++ b/research/rounded-borrowing-contract/vendor/pr985/NOTICE.md @@ -0,0 +1,41 @@ +# Attribution and license + +New material is prepared for Ali Romman (@aliromman), with substantial +OpenAI Codex assistance in the derivation, implementation, tests, and text. +One AI agent produced the initial construction. The quadratic-phase agent +found the repeated validation reads; the coordinator reproduced and corrected +them. These AI checks and separate exact arithmetic paths are not independent +human review or a formal proof of the full theorem. + +The new files use Apache-2.0. The retained predecessor files keep their +original notices and source pins in `SOURCE.json`. + +- Rohan Guliani (@Rohansguliani), PR846, supplies the Euclidean chain and + closure decomposition and its linear-tape clean-storage solver. This + submission uses that decomposition and supplies a separate dirty transport + proof. It does not reuse the clean queue or its traffic constant. +- Chafik Boukhalfa (@chafreaky), PR628, supplies certified factor data, + paid coefficient and phase preparation, rounded integer lifts, and the + balanced dirty commutator. Its unchanged checker and dense solver check + the original kernels here. Its original dirty proof supplies the + conservative full-word perturbation argument. +- Charles Bethin (@cbethin), PR764, supplies the shared-suffix estimate used + in the weighted error argument, also used by PR846. No PR764 code is used. +- Ali Romman, PR621, supplies the uniform cyclic inverse bound and retained + kernel lineage. PR628's notice credits the pinned OpenAI exact-DFT + preprint, classical Newton and q-Pochhammer factorization, Alexey + Kuznetsov, and the cited preparation and filtering methods. Those credits + remain applicable. No priority claim is made for those methods. +- 0xkilgore's PR663 independently audits exact restoration and the binary + leaf count. PR673, PR689, PR730, PR744, and later echo work study other + tree and scratch contracts. The present source reuse acts inside a leaf. + +The overlap check also read Chafik Boukhalfa's PR862, PR905, PR929, and PR951, +Gareth Davidson's PR877, Wentao Li's PR805, and Chafik Boukhalfa's new +PR977. PR977 improves the precision of the clean solver. Ross Richardson's +PR982 borrows outputs for a different fanout interface. These results supply different +precision or storage results. They are not implemented, benchmarked, or +combined by this package. Their inspected heads are recorded in CLAIM.json. + +No literature-priority, new kappa, selected-supplier, production-speed, +bit-reversible compiler, or complete multiplication theorem claim is made. diff --git a/research/rounded-borrowing-contract/vendor/pr985/PROOF.md b/research/rounded-borrowing-contract/vendor/pr985/PROOF.md new file mode 100644 index 0000000000..01a3da7347 --- /dev/null +++ b/research/rounded-borrowing-contract/vendor/pr985/PROOF.md @@ -0,0 +1,428 @@ +# A dirty source for the arbitrary-stride closure + +## Contract and limits + +Let `Z_L^w x` have entry `x_((i-w) mod L)`. Let `0 < beta <= 1/2`, +`|b| <= 1-beta`, and `u=2^-W`. The source `x` and target `y` are distinct +length-`L` arrays on the complex dyadic grid of spacing `u`. They can contain +arbitrary data. The coefficient `b` is one immutable rational complex number. Reduce the +stride modulo `L`. The bounds below use a residue with `O(log L)` bits; +reading an oversized stride descriptor is additional input work. + +The function `lift` adds an approximation to + + m (I-b Z_L^w)^-1 x + +to a cyclic shift of `y`. It restores `x` exactly. It needs no other data +array, no reserved zero bits, and only a constant number of clean complex +arithmetic registers. The recursion keeps integer indices and array views. +It does not keep a clean array of coefficients or closure values. + +Reversible block swaps implement the data operations on two sequential +tapes. No blank data array or coefficient table is used. The source and +target occupy one tape each during a leaf. The complete kernel routes its +borrowed arrays over the same two tapes, with all movement charged below. +The optional output shift is zero or the leaf stride; these are the two +cases required by the kernel factors. The construction does not implement +the variable-coefficient case of PR846's Theorem 1. + +Let `K` be the number of non-base Euclidean levels. Assume + + 48 (K+1) u <= beta^3. + +If `|x_i| <= B`, the unscaled target increment differs from the inverse by +at most + + 64 (B+1) u / beta^5. + +A multiplier of modulus at most `M`, with `M>=1`, changes this bound to + + (64 M (B+1) / beta^5 + 3) u. + +The rounded increment can depend on the target's initial value within this +error bound. A negative call executes the exact inverse word. It restores +the completed positive call, including all source and target data. + +## Source reuse + +As in Rohan Guliani's PR846, normalize the stride and reverse the index views +when necessary. Then `0 < w <= L/2`. Split the source into chains with +indices `c, c+w, c+2w, ...`. Apply the causal integer lifts + + x_i += rnd(a_i x_(i-w)), i=w,...,L-1. + +Call the resulting source `z`. Each lift has an exact inverse on the grid: +subtract the same rounded product in reverse order. Add `z` to the target +before using any source entries as temporary storage. + +The last `w` source entries contain the closure right-hand side. The first +`w` source entries are disjoint from that tail. Use this prefix as a dirty +target for the recursive closure. It contains arbitrary values; it is not +cleared. Let `F` be the completed rounded closure call. Let `H` be the +linear chain expansion. A reversible rounded conjugation implements the +additive `H` call, as specified below. +Execute + + F(tail, prefix) + H_add(prefix, y) + F_inverse(tail, prefix) + H_add_inverse(prefix, y) + +Then undo the original causal lifts. There are two recursive calls. + +The recursive call restores its input tail. The expansion preserves the +whole source, including the changed prefix and the tail. Thus `F_inverse` +sees precisely the state left by `F` and restores the prefix exactly. +Target independence and rounded linearity are not required. The two +expansion errors are charged separately. At every depth the prefix and +tail are disjoint because `2w <= L`. This proves restoration by induction. + +The negative leaf reverses the complete middle word: first the positive +expansion, then `F`, then the inverse expansion, then `F_inverse`, then the +negative baseline addition. It is not the positive word with all signs +changed in place. + +In exact arithmetic the source lifts give the chain decomposition +`S x = z + H S_child z_tail`. The four instructions above add precisely the +second term. This is the usual dirty commutator, with its connector taken +from the source prefix. PR628 supplies the dirty commutator and exact grid +lift methods; PR846 supplies the chain/closure decomposition. + +## Reversible transport on two dirty tapes + +Write `C` for the causal map whose non-start coefficient is `a`. Split the +source and carrier views into consecutive blocks of at most `w` records. +The carrier has arbitrary contents. For each block in forward order: + +1. For each position after the first block, add the rounded product of `a` + and the preceding block's value on the carrier tape to the source. +2. Swap this whole source block with its corresponding carrier block. + +At this point the source tape holds the original carrier, and the carrier +tape holds `C_round(source)`. Swap the two complete views. The causal map +has been applied, and the carrier has been restored exactly. Each block +scan and each rewind costs its block length. There is no length-`w` clean +queue. The old carrier data remains in the other tape throughout. + +For the inverse, first swap the complete views. Visit the blocks in reverse +order. Swap the current block back, then subtract its rounded predecessor +products. The predecessor block is still on the carrier tape. Reverse the +order within each block as well. This is the exact inverse grid word. +Each map costs at most `64n` data-record moves on views of length `n`, +including read/write charges, block rewinds and full-view swaps. This loose +bound also covers a cyclic view that crosses the root tape boundary once. + +An expansion uses this causal map on the **target**, with the source as +its dirty carrier. Apply `C_round_inverse` to the target, add +`rnd(m*b_start*prefix_i)` to its first `w` entries, then apply `C_round`. +The source is restored by each transport pass and is unchanged at the +injection. The negative expansion changes only the injection sign. It is +the exact inverse of the positive expansion. + +The closure source and its dirty prefix initially lie on the same tape. +Swap the source prefix with the first `w` records of the other tape. Run +the child on the source tail and this moved prefix, then swap back. The +outer target's displaced data is never read by the child and is restored +exactly. Both child views are now on distinct tapes. Their physical spans +are contiguous. At the root an output shift of zero or the leaf stride +ensures that the moved prefix does not cross the tape boundary. All later +views are reversals or subintervals of these contiguous views. + +## Two coefficients per level + +No length-dependent clean coefficient table is required. Put + + g = gcd(L0,w0), M = L0/g, v = (w0/g)^-1 modulo M. + +For `M=1`, all cycles have length one and no modular inverse is required. +At a recursive level the remaining original indices form an interval, +with orientation `s` equal to `+1` or `-1`. Its length and stride are `n,d`. +The displacement to a predecessor is `s*d` when `i>=d`, and `s*(d-n)` +otherwise. The number of original edges is the unique integer in `[1,M]` +congruent to + + (displacement/g) v modulo M. + +The induced edge stops at the first remaining vertex. It cannot complete +an extra original cycle first. Thus these residues are the actual return +times, not only congruence classes. At a base level each vertex has returned +to itself, so its exponent is `M`. There are only two possible coefficients +per level, both powers of the original `b`. + +The checker independently forms each new exponent by summing the old chain +exponents. It compares all resulting entries with this modular formula. +That finite comparison supports the all-length argument above. + +The implementation recomputes these two powers before each pass. Scalar +temporaries are held only inside `causal`, `expand`, and `diagonal`; they +are discarded before a recursive call. The recursion retains only views, +integer metadata, and references to the immutable root descriptor. + +## Rounded coefficient preparation + +`power` uses binary powering from the most significant bit. After each +product it truncates both components toward zero. A truncation has complex +error at most `2u` and cannot increase the norm. Hence the value prepared +for exponent `e` has norm at most `q^e`, where `q=|b|`. + +Expand the repeated squaring into a binary multiplication tree with `e` +leaves. A local error propagates through sibling products whose combined +norm is at most `q^(e-t)`, where that node contains `t` leaves. At most two +nodes have more than `floor(e/2)` leaves. All other internal nodes have at +least `ceil(e/2)` leaves outside them. Therefore the error is at most + + 2u [2 + e q^ceil(e/2)] <= 2u [2 + 2/beta] <= 8u/beta. + +Here `k q^k <= sum_(j=0)^(k-1) q^j <= 1/beta`. Exponents one and two +satisfy the same bound directly. The tree counts repeated operands with +their multiplicity; reuse of a scalar result does not remove its error. + +Let a chain contain `t` prepared coefficients. Each coefficient and its +exact counterpart has norm at most `q`. A telescoping product comparison +gives error at most + + (8u/beta) t q^(t-1) <= 8u/beta^2. + +Compare this chain product `pi` with the freshly prepared child coefficient. +They approximate the same original power. Their difference is at most + + eta = 12u/beta^2, + +since `8u/beta^2 + 8u/beta <= 12u/beta^2`. Every prepared coefficient has +margin at least `beta`. These statements include complex coefficients. + +## Error recurrence + +Consider the exact solution of the system with the prepared coefficients +at each level. Suppose its right-hand side satisfies + + |x_i| <= A (1-|a_i|). + +The shared-suffix identity used by Charles Bethin in PR764 bounds the exact +zero-seed chain value by `A(1-|pi|)`. The rounded causal pass adds at most +`u/beta`. Because the child coefficient differs from `pi` by at most `eta`, +the next weighted bound is + + A_next <= (1 + 12u/beta^3) A + u/beta^2. + +Start with `A0=B/beta`. The admission condition gives +`K*12u/beta^3 <= 1/4`. Thus `(1+12u/beta^3)^K < 2`, and at every level + + A <= Astar = 2(B/beta+1). + +The inverse of a system with coefficients of modulus at most `1-beta` +has infinity norm at most `1/beta`. Its stronger weighted estimate is: +if `|v_i| <= C(1-|a_i|)`, its solution has norm at most `C`. Both follow +from the absolutely convergent Neumann series and telescoping weights. + +Compare the exact child solution with the exact Schur solution. Their +right-hand sides differ by at most `u/beta`, and their coefficients differ +by at most `eta`. The Schur solution is a restriction of the parent solution +and has norm at most `Astar`. Their solution difference is at most + + Dstar = u/beta^2 + 12 Astar u/beta^3. + +The rounded inverse causal map differs from `C^-1` by at most `u` per +entry: each non-start entry subtracts one rounded product. The forward map +differs from `C` by at most `u/beta`. The seed injection adds at most `u` +error. Since `||C||<=1/beta`, the conjugated expansion differs from its +linear additive map by at most `3u/beta`, independently of both dirty +arrays. There are two expansions. The source pass contributes another +`u/beta`. Each chain prefix contains at +least one coefficient, so it contracts a child error by at most `1-beta`. +For the unscaled leaf error, + + e_k <= (1-beta) e_(k+1) + Dstar + 7u/beta, + e_K <= u. + +Summing the geometric series gives + + e_0 <= u + u/beta^3 + 12 Astar u/beta^4 + 7u/beta^2 + <= 64(B+1)u/beta^5. + +The root multiplier scales the baseline and each seed injection. The +injection rounding was already charged above. The baseline adds at most +one further `u`; a diagonal root adds at most one. Taking `M>=1` gives the +stated conservative bound with an additional `3u` allowance. + +## Complete arithmetic and storage recurrence + +Let `n_k` be the level lengths after orientation changes. Then + + n_k >= 2 n_(k+1) + n_(k+2). + +Indeed the next length is the normalized remainder, which is at most the +ordinary Euclidean remainder. Let `S(n,d)` be the sum of lengths over the +full binary recursion tree. It satisfies + + S(n,0)=n, + S(n,d)=n+2 S(d,(-n) mod d) <= 5n+2d <= 6n. + +The potential `5n+2d` proves the inequality directly using +`n>=2d+d_next`. Each non-base visit pays for six complete causal maps, +two seed injections, the baseline output, four closure transport swaps, +and both complete children. Each base visit pays for all divisions and +target additions. Validation scans and final head returns are also paid. +Reversal and slicing create index views; their physical accesses still pay +for every movement. + +Each visit prepares at most sixteen powers, each with `O(log M)` products. +This cost is also `O(L)`, although the constant is not optimized. From +`n_k>=5n_(k+2)`, a tree of depth `K` has `O(2^K)` nodes and +`2^K=O(L^log_5(4))`. Since `log_5(4)<1`, +`2^K log L=O(L)`. The Euclidean and modular-inverse setup uses integer +arithmetic on `O(log L)` bits. The implementation retains `O(log L)` +integer metadata words, or `O(log^2 L)` bits, with no data-sized values +on the recursion stack. Index arithmetic can be charged conservatively +with sequential counter updates. A block counter costs `O(w)` bit changes +over a block, including its `O(log(w+1))` reset. Integer setup costs +`O(log^3 L)` per visit, using a conservative schoolbook division bound. +The bound on `2^K` also gives `2^K log^3 L=O(L)`, so the total control cost +is `O(L)` bit operations in +the stated tape implementation. The rational reference uses Python +indices; it is not a timing implementation of this control bound. + +An explicit loose count is at most `1280L` scalar products and divisions, +including power preparation and a root multiplier. To see this, let `J` +be the number of tree visits. The direct count is at most +`9S + 32J bit_length(M) + 3L`. Since `4^8 <= 5^7`, the depth bound gives +`J <= 4 L^(7/8)`. Also `log2 L <= 8 L^(1/8)` for `L>=1`. It follows that +`J bit_length(M) <= 36L`, which proves the stated count. Mutable data +accesses are at most `71S+2L < 512L`, including both validation scans. +These constants are arithmetic bounds, not measured runtime claims. + +Thus one leaf uses `O(L)` rounded scalar operations, two data arrays, and +`O(1)` clean arithmetic registers, apart from scalar arithmetic workspace. +If both incoming arrays have norm at most `D`, internal values have +magnitude bounded by a polynomial in `(D+1)/beta`, independent of `L`. +The weighted bound gives `H=3(D+1)/beta` for causal source values at every +level. Under `a*u<=1` below, a completed child changes a prefix of this +size by at most `H/beta+(H+1)/2`. Thus the changed seed has norm at most +`10(D+1)/beta^2`. Each expansion target adds at most `M` times that seed +norm plus `3u/beta`. Inside its causal conjugation, the inverse pass has +norm at most twice its input plus `u`; the injection adds its seed term; +the forward pass divides this combined bound by at most `beta` and adds +`u/beta`. Apply these inequalities to both expansion calls and the baseline. +The loose bound `512(M+1)(D+1)/beta^7` covers every intermediate value, +including the displaced carrier data. At each recursive call its initial +target is a source prefix or the completed change to that prefix; no +unbounded sequence of target magnifications is assumed. The implementation +is an exact-rational reference with explicit +rounding; it is not a fast fixed-precision arithmetic compiler. + +## Products and paid precision + +For a certified kernel `Q(U)=r^-1 product_j(U-rho_j)`, use the same factor +maps as PR628 and PR846, with `U=tau Z_L^w` and constant `|tau|=1`. +For an outer root use coefficient `tau/rho` and multiplier `-1/rho`. +For an inner root use coefficient `rho*conj(tau)`, stride `-w`, multiplier +`conj(tau)`, and output shift `-w`. Include `r` in one multiplier. + +The implementation uses PR628's balanced four-call dirty commutator. +It requires `h=ceil(log2(r-1))` distinct arbitrary dirty arrays. The new +leaf needs no additional array. For `n` factors, the complete leaf count is + + N(1)=1, N(n)=2N(floor(n/2))+2N(ceil(n/2)) <= 4n^2. + +A negative composition reverses the order and signs of the four child +calls. Ancestor inputs and targets cannot be used as deeper scratch. +All source and borrowed data restore exactly. The final rounded increment +of a composition can depend on the initial borrowed values, as in PR628. + +For a simple sufficient bound retain PR628's full-word perturbation proof. +Put `a=68(r+1)/beta^5`, `G=2+r/beta`, and let every initial array have norm +at most `D`. If `a*u<=1`, then the execution error is at most + + N a (D+1) u G^(N-1). + +Choose `W` at least the incoming grid precision, the admission budget, and + + p+1 + ceil(log2(N a (D+1))) + (N-1) ceil(log2 G). + +This pays the execution error to `2^(-p-1)`. The pinned factor certificate +pays the remaining error to `2^(-p-1)` after scaling by the source norm. +For general input norm `X`, coefficient preparation must use target +`p+ceil(log2(max(1,X)))`. The supplied fixtures have ample certified margin; +their scaled perturbation is checked exactly, not assumed. + +With PR628's inherited `log2(1/beta)=O(r^3)`, this conservative choice is +`O(p+incoming_bits+log(D+1)+r^5+log(log L+2))` fractional bits. Integer +magnitude bits have the same order. An explicit safe integer reserve is + + ceil(log2(D+1)) + N ceil(log2 G) + + ceil(log2(512(r+1)/beta^7)) + 3. + +This note does not claim a precision improvement. Gareth Davidson's PR877 +and Chafik Boukhalfa's PR905 give stronger prefix bounds for the predecessor +dispatcher. Their cubic or quartic conclusions are not imported without a +separate check of the new leaf contract. + +## Complete tape and preparation bill + +The meter maps every mutable array to one of **two** physical tapes and +an absolute tape offset. It charges the distance from the previous head +position plus one unit for each read or write. It counts transport swaps, +validation, source restoration, and explicit final head returns. It does +not give each borrowed array a free tape head. + +One non-base visit costs at most `640n` record moves, apart from its two +children. Six causal maps cost at most `384n`. Baseline and seed scans cost +at most `24n`. The closure swaps and travel into and out of the child spans +cost at most `32n`. These total less than `640n`. The loose allowance also +covers the root cyclic view and entry positioning. A base visit costs at +most `8n`. Since `S<=6L`, validation and head returns leave the complete +leaf below **`4096L` data-record moves**. This is a proof bound, not a claim +that its constant is sharp. + +For a full kernel with `h>=1`, place the last borrowed array on tape B. +Place the source, target, and other borrowed arrays consecutively on tape +A. If a leaf's two arrays are both on A, swap its target with the array on +B, execute the leaf, and swap back. The B array is distinct from both +operands in this case. Its contents never enter the leaf calculation and +are restored exactly. If a leaf already uses both tapes, no such routing +is needed. For `h=0`, put the two arrays on separate tapes directly. + +This routing adds `O((h+2)L)` moves per leaf, including the distance between +array slots and returns to the tape origins. The full bound used by the +checker is `8192(N+1)(h+2)L` moves. It includes the initial validation scan. +No extra data array is allocated for transport. + +Let `W_total` include the fractional bits, integer reserve, and the bit +lengths of the immutable coefficient, gauge, and margin descriptors. The generic +rational API does not bound descriptor length from coefficient magnitude. +Let `M(W_total)` include the chosen rounded scalar multiplication and +division cost. With this complete scalar word size, the resulting bill is + + preparation + O(N L) M(W_total) + O(N(h+2)L W_total). + +Locating a factor on a sequential read-only descriptor tape costs at most +`O(r W_total)` per leaf, hence `O(r^3 W_total)` over the word. The original +factor and phase preparation charges remain inherited from PR628; this +descriptor access is included, not treated as free. Temporary powers, +source reads, multipliers, divisions, copies, inverse calls, and children +are all charged. The two data tapes, scalar arithmetic tapes, and metadata +stack use a fixed number of tapes. Borrowed data storage remains `hL` +complex words. Scalar arithmetic workspace has the declared word size; +the leaf index stack has `O(log^2 L)` bits. The balanced composition and +array routing retain another `O(log r (log r + log L))` metadata bits. +Their control cost is absorbed by the routing and descriptor terms, since +`log L=O(L)` and `log^2 r=O(r)`. These are metadata bits, not arithmetic +registers or data arrays. + +This is a constant-coefficient kernel construction. Variable site phases, +complete-transform composition and normalization, common-label/Clifford +compilation, physical supplier hosting, and the multiplication reduction +remain open. There is no new kappa, complex b, or BIT c claim. Finite replay +is not a formal proof of the full theorem or independent human review. + +Chafik Boukhalfa's concurrent PR951 gives two grouped additive calls with +no dirty connector in a neighboring-cycle layout. It uses a larger clean +scalar workspace. This note instead uses constant clean arithmetic storage +per first-order leaf, the original logarithmic dirty array budget, and +arbitrary-stride transport. It makes no claim to improve PR951's arithmetic +count or cubic precision. + +Chafik Boukhalfa's PR977 removes the length admission and proves cubic +precision for PR846 in its original clean scratch model. This construction +retains its stated admission and conservative precision. Combining those +precision arguments with the new dirty leaf requires a separate proof. diff --git a/research/rounded-borrowing-contract/vendor/pr985/dirty_stride.py b/research/rounded-borrowing-contract/vendor/pr985/dirty_stride.py new file mode 100644 index 0000000000..027108871d --- /dev/null +++ b/research/rounded-borrowing-contract/vendor/pr985/dirty_stride.py @@ -0,0 +1,409 @@ +"""Add a cyclic inverse to a target and restore the source exactly. + +This is a fixed-grid arithmetic model with two data tapes. Every data access +pays its head movement. See PROOF.md for the complete bill. +""" +from dataclasses import dataclass, field +from fractions import Fraction as F +from math import gcd + +ZERO = (F(0), F(0)) +ONE = (F(1), F(0)) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def add(a, b): + return (a[0] + b[0], a[1] + b[1]) + + +def sub(a, b): + return (a[0] - b[0], a[1] - b[1]) + + +def mul(a, b): + return (a[0]*b[0] - a[1]*b[1], a[0]*b[1] + a[1]*b[0]) + + +def norm2(a): + return a[0]*a[0] + a[1]*a[1] + + +def div(a, b): + d = norm2(b) + need(d != 0, 'zero divisor') + v = mul(a, (b[0], -b[1])) + return (v[0]/d, v[1]/d) + + +def rnd(a, bits): + """Use nearest dyadic rounding, with ties toward positive infinity.""" + scale = 1 << bits + def component(v): + t = v*scale + F(1, 2) + return F(t.numerator // t.denominator, scale) + return (component(a[0]), component(a[1])) + + +def trunc(a, bits): + """Truncate each component toward zero. This cannot increase the norm.""" + scale = 1 << bits + return tuple(F(int(v*scale), scale) for v in a) + + +@dataclass +class Meter: + reads: int = 0 + writes: int = 0 + tape_moves: int = 0 + products: int = 0 + power_products: int = 0 + divisions: int = 0 + nodes: int = 0 + leaves: int = 0 + validation_reads: int = 0 + max_depth: int = 0 + heads: dict = field(default_factory=dict) + layout: dict = field(default_factory=dict) + + def access(self, data, index, write=False): + tape, start = self.layout[id(data)] + position = start+index + self.tape_moves += abs(position - self.heads.get(tape, 0)) + 1 + self.heads[tape] = position + if write: + self.writes += 1 + else: + self.reads += 1 + + def rewind(self): + for tape, position in self.heads.items(): + self.tape_moves += position + self.heads[tape] = 0 + + +@dataclass(frozen=True) +class View: + data: list + start: int + step: int + length: int + meter: Meter + + def index(self, i): + need(0 <= i < self.length, 'view index') + return (self.start + self.step*i) % len(self.data) + + def get(self, i): + j = self.index(i) + self.meter.access(self.data, j) + return self.data[j] + + def put(self, i, value): + j = self.index(i) + self.meter.access(self.data, j, True) + self.data[j] = value + + def part(self, first, length): + need(0 <= first and first + length <= self.length, 'view interval') + return View(self.data, self.start + self.step*first, self.step, length, self.meter) + + def reverse(self): + return View(self.data, self.start + self.step*(self.length-1), + -self.step, self.length, self.meter) + + +def depth(length, stride): + count = 0 + while True: + stride %= length + stride = min(stride, length-stride) + if stride == 0: + return count + length, stride = stride, (-length) % stride + count += 1 + + +def admitted(beta, bits, levels): + return (type(bits) is int and bits >= 0 and 0 < beta <= F(1, 2) + and 48*(levels+1)*F(1, 1 << bits) <= beta**3) + + +def power(b, exponent, bits, meter): + """Use a left-to-right binary product and scalar working storage.""" + need(exponent >= 1, 'positive exponent') + result = b + for k in range(exponent.bit_length()-2, -1, -1): + result = trunc(mul(result, result), bits) + meter.power_products += 1 + if (exponent >> k) & 1: + result = trunc(mul(result, b), bits) + meter.power_products += 1 + return result + + +@dataclass(frozen=True) +class Geometry: + root: tuple + divisor: int + cycle: int + inverse: int + bits: int + meter: Meter + + def exponents(self, length, stride, orientation): + if stride == 0: + return (self.cycle, self.cycle) + def exponent(displacement): + need(displacement % self.divisor == 0, 'cycle lattice') + return ((displacement // self.divisor)*self.inverse) % self.cycle or self.cycle + return (exponent(orientation*stride), exponent(orientation*(stride-length))) + + def coefficients(self, length, stride, orientation): + a, b = self.exponents(length, stride, orientation) + left = power(self.root, a, self.bits, self.meter) + right = left if a == b else power(self.root, b, self.bits, self.meter) + return (left, right) + + +def emit(target, i, value, multiplier, sign, bits): + if multiplier != ONE: + target.meter.products += 1 + value = rnd(mul(multiplier, value), bits) + old = target.get(i) + target.put(i, add(old, value) if sign == 1 else sub(old, value)) + + +def swap(source, target): + for i in range(source.length): + left, right = source.get(i), target.get(i) + source.put(i, right) + target.put(i, left) + + +def causal(source, carrier, stride, geometry, undo=False): + """Apply the causal lifts with block swaps; restore the dirty carrier.""" + a, _ = geometry.coefficients(source.length, stride, source.step) + n = source.length + if undo: + swap(source, carrier) + for first in range(((n-1)//stride)*stride, -1, -stride): + size = min(stride, n-first) + swap(source.part(first, size), carrier.part(first, size)) + if first: + for i in range(first+size-1, first-1, -1): + value = rnd(mul(a, carrier.get(i-stride)), geometry.bits) + geometry.meter.products += 1 + source.put(i, sub(source.get(i), value)) + else: + for first in range(0, n, stride): + size = min(stride, n-first) + if first: + for i in range(first, first+size): + value = rnd(mul(a, carrier.get(i-stride)), geometry.bits) + geometry.meter.products += 1 + source.put(i, add(source.get(i), value)) + swap(source.part(first, size), carrier.part(first, size)) + swap(source, carrier) + + +def expand(source, target, stride, geometry, multiplier, sign): + """Conjugate the seed injection by exact inverse causal grid maps.""" + causal(target, source, stride, geometry, undo=True) + _, b = geometry.coefficients(source.length, stride, source.step) + coefficient = mul(multiplier, b) + geometry.meter.products += 1 + for i in range(stride): + value = rnd(mul(coefficient, source.get(i)), geometry.bits) + geometry.meter.products += 1 + emit(target, i, value, ONE, sign, geometry.bits) + causal(target, source, stride, geometry) + + +def closure(source, target, stride, geometry, sign, level): + """Move the child target to the other tape and restore the carrier.""" + borrowed = source.part(0, stride) + carrier = target.part(0, stride) + ends = source.part(source.length-stride, stride) + swap(borrowed, carrier) + solve(ends, carrier, (-source.length) % stride, geometry, sign=sign, level=level+1) + swap(borrowed, carrier) + + +def diagonal(source, target, geometry, multiplier, sign): + coefficient = power(geometry.root, geometry.cycle, geometry.bits, geometry.meter) + denominator = sub(ONE, coefficient) + for i in range(source.length): + value = rnd(div(source.get(i), denominator), geometry.bits) + geometry.meter.divisions += 1 + emit(target, i, value, multiplier, sign, geometry.bits) + + +def solve(source, target, stride, geometry, multiplier=ONE, sign=1, level=0): + """Use integer metadata at each level; scalar temporaries stay in helpers.""" + length = source.length + stride %= length + if 2*stride > length: + source, target, stride = source.reverse(), target.reverse(), length-stride + geometry.meter.nodes += 1 + geometry.meter.max_depth = max(geometry.meter.max_depth, level) + if stride == 0: + diagonal(source, target, geometry, multiplier, sign) + return + causal(source, target, stride, geometry) + if sign == 1: + for i in range(length): + emit(target, i, source.get(i), multiplier, 1, geometry.bits) + closure(source, target, stride, geometry, 1, level) + expand(source, target, stride, geometry, multiplier, 1) + closure(source, target, stride, geometry, -1, level) + expand(source, target, stride, geometry, multiplier, -1) + else: + expand(source, target, stride, geometry, multiplier, 1) + closure(source, target, stride, geometry, 1, level) + expand(source, target, stride, geometry, multiplier, -1) + closure(source, target, stride, geometry, -1, level) + for i in range(length): + emit(target, i, source.get(i), multiplier, -1, geometry.bits) + causal(source, target, stride, geometry, undo=True) + + +def lift(x, y, b, beta, bits, stride, sign=1, multiplier=ONE, shift=0, meter=None): + """Add multiplier*(I-b Z^stride)^-1 x at output indices i+shift.""" + need(type(stride) is int and type(shift) is int and type(sign) is int + and sign in (-1, 1), 'integer stride and sign') + need(x is not y and len(x) == len(y) and len(x) > 0, 'distinct equal arrays') + need(shift % len(x) in (0, stride % len(x)), 'output shift must be zero or the leaf stride') + need(isinstance(b, tuple) and len(b) == 2 and norm2(b) <= (1-beta)**2, 'stable constant coefficient') + need(isinstance(multiplier, tuple) and len(multiplier) == 2, 'constant multiplier') + need(admitted(beta, bits, depth(len(x), stride)), 'precision admission') + meter = meter if meter is not None else Meter() + if not meter.layout: + meter.layout = {id(x): (0, 0), id(y): (1, 0)} + need(id(x) in meter.layout and id(y) in meter.layout + and {meter.layout[id(x)][0], meter.layout[id(y)][0]} == {0, 1}, 'two distinct data tapes') + for data in (x, y): + for i in range(len(data)): + meter.access(data, i) + meter.validation_reads += 1 + value = data[i] + need(rnd(value, bits) == value, 'fixed grid data') + divisor = gcd(len(x), stride) + cycle = len(x)//divisor + inverse = pow((stride//divisor) % cycle, -1, cycle) if cycle > 1 else 0 + geometry = Geometry(b, divisor, cycle, inverse, bits, meter) + solve(View(x, 0, 1, len(x), meter), View(y, shift, 1, len(y), meter), + stride, geometry, multiplier, sign) + meter.leaves += 1 + meter.rewind() + return meter + + +def leaf_bound(bound, beta, bits, multiplier_bound=1): + return (64*multiplier_bound*(bound+1)/beta**5 + 3)*F(1, 1 << bits) + + +def leaf_calls(count): + need(type(count) is int and count >= 1, 'positive factor count') + if count == 1: + return 1 + return 2*leaf_calls(count//2) + 2*leaf_calls(count-count//2) + + +def compose(x, y, factors, scratch, tau, beta, bits, stride, sign=1, meter=None): + """Use PR628's balanced dirty commutator with the new arbitrary-stride leaf.""" + need(factors and len(scratch) >= (len(factors)-1).bit_length(), 'dirty depth') + arrays = [x, y] + scratch + need(len({id(a) for a in arrays}) == len(arrays), 'all arrays distinct') + need(len(x) > 0 and all(len(a) == len(x) for a in arrays), 'array lengths') + need(isinstance(tau, tuple) and norm2(tau) == 1, 'immutable unit gauge') + need(type(sign) is int and sign in (-1, 1) and type(stride) is int, 'integer stride and sign') + need(admitted(beta, bits, depth(len(x), stride)), 'precision admission') + for factor in factors: + need(isinstance(factor, tuple) and len(factor) == 3, 'factor descriptor') + inside, b, scale = factor + need(type(inside) is bool and isinstance(b, tuple) and len(b) == 2 + and norm2(b) <= (1-beta)**2 and isinstance(scale, (int, F)), 'stable factor descriptor') + meter = meter if meter is not None else Meter() + if scratch: + layout = {id(a): (0, i*len(x)) for i, a in enumerate(arrays[:-1])} + layout[id(scratch[-1])] = (1, 0) + else: + layout = {id(x): (0, 0), id(y): (1, 0)} + need(not meter.layout or meter.layout == layout, 'kernel tape layout') + meter.layout = layout + for data in arrays: + for i in range(len(data)): + meter.access(data, i) + meter.validation_reads += 1 + value = data[i] + need(rnd(value, bits) == value, 'fixed grid data') + def run(src, dst, lo, hi, level, direction): + if hi-lo == 1: + inside, b, scale = factors[lo] + phase = (tau[0], -tau[1]) if inside else tau + coefficient = mul(b, phase) + m = phase if inside else (-b[0], -b[1]) + m = (m[0]*scale, m[1]*scale) + if meter.layout[id(src)][0] == meter.layout[id(dst)][0]: + spare = scratch[-1] + destination = View(dst, 0, 1, len(dst), meter) + carrier = View(spare, 0, 1, len(spare), meter) + swap(destination, carrier) + lift(src, spare, coefficient, beta, bits, -stride if inside else stride, + direction, m, -stride if inside else 0, meter) + swap(destination, carrier) + else: + lift(src, dst, coefficient, beta, bits, -stride if inside else stride, + direction, m, -stride if inside else 0, meter) + return + mid = (lo+hi)//2 + z = scratch[level] + if direction == 1: + run(src, z, lo, mid, level+1, 1) + run(z, dst, mid, hi, level+1, 1) + run(src, z, lo, mid, level+1, -1) + run(z, dst, mid, hi, level+1, -1) + else: + run(z, dst, mid, hi, level+1, 1) + run(src, z, lo, mid, level+1, 1) + run(z, dst, mid, hi, level+1, -1) + run(src, z, lo, mid, level+1, -1) + run(x, y, 0, len(factors), 0, sign) + meter.rewind() + return meter + + +def ceil_log2(value): + value = F(value) + need(value > 0, 'positive logarithm') + k = value.numerator.bit_length() - value.denominator.bit_length() + power_of_two = F(2)**k + return k if value <= power_of_two else k+1 + + +def execution_bound(count, r, beta, initial_bound, bits): + need(r >= 1 and initial_bound >= 0 and 0 < beta <= F(1, 2) + and type(bits) is int and bits >= 0, 'execution budget domain') + calls = leaf_calls(count) + a = 68*(r+1)/beta**5 + growth = 2+F(r)/beta + need(a*F(1, 1 << bits) <= 1, 'execution precision') + return calls*a*(initial_bound+1)*F(1, 1 << bits)*growth**(calls-1) + + +def working_bits(count, r, beta, initial_bound, target_bits, incoming_bits, length, stride): + need(r >= 1 and initial_bound >= 0 and 0 < beta <= F(1, 2) + and type(target_bits) is int and target_bits >= 0 + and type(incoming_bits) is int and incoming_bits >= 0 + and type(length) is int and length > 0 and type(stride) is int, 'working budget domain') + calls = leaf_calls(count) + a = 68*(r+1)/beta**5 + growth = 2+F(r)/beta + levels = depth(length, stride) + return max(incoming_bits, target_bits+1+ceil_log2(calls*a*(initial_bound+1)) + +(calls-1)*ceil_log2(growth), ceil_log2(a), + ceil_log2(48*(levels+1)/beta**3)) diff --git a/research/rounded-borrowing-contract/verify.py b/research/rounded-borrowing-contract/verify.py new file mode 100644 index 0000000000..1cca862052 --- /dev/null +++ b/research/rounded-borrowing-contract/verify.py @@ -0,0 +1,403 @@ +#!/usr/bin/env python3 +"""Check the exact finite domains specified in COVERAGE.md. + +The uniform claims use the written proof. This finite checker is not a proof +assistant or a multiplication implementation. See NOTICE.md for attribution. +""" +import argparse +from fractions import Fraction +from hashlib import sha256 +import importlib.util +from itertools import product +import json +from math import gcd +from pathlib import Path +import sys + +ROOT = Path(__file__).resolve().parent +sys.path.insert(0, str(ROOT)) +from contracts import (exact_lift, inverse, nearest, offset_sum, prefix_degree, + replay, residue_response) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def load_module(name, path): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def sources(): + manifest = json.loads((ROOT / "SOURCES.json").read_text()) + for item in manifest["files"]: + data = (ROOT / item["path"]).read_bytes() + need(sha256(data).hexdigest() == item["sha256"], "source digest mismatch") + blob = b"blob " + str(len(data)).encode() + b"\0" + data + import hashlib + need(hashlib.sha1(blob).hexdigest() == item["git_blob"], + "source Git blob mismatch") + return manifest["base_commit"], len(manifest["files"]) + + +def oracle(p, q, value): + result = Fraction(p * value, q) + Fraction(1, 2) + return result.numerator // result.denominator + + +def scalar_census(): + ratios = stable_tests = response_tests = average_tests = 0 + digest = sha256() + for q in range(2, 25): + for p in range(-2 * q, 2 * q + 1): + if gcd(p, q) != 1: + continue + ratios += 1 + values = range(q) + signatures = [] + for z in values: + signatures.append(tuple(oracle(p, q, z + h) - oracle(p, q, z) + for h in values)) + need(len(set(signatures)) == q, "residue classes not distinguished") + for h in range(-2 * q, 2 * q + 1): + differences = {oracle(p, q, z + h) - oracle(p, q, z) + for z in values} + need((len(differences) == 1) == (h % q == 0), + "safe translation classification failed") + stable_tests += 1 + for z in range(-2 * q, 2 * q + 1): + expected = oracle(p, q, z + h) - oracle(p, q, z) + observed = residue_response(p, q, p * z % q, h) + need(observed == expected, "saved residue response failed") + response_tests += 1 + for z in range(-q, q + 1): + need(offset_sum(p, q, z) == p * z, "offset identity failed") + average_tests += 1 + digest.update(canonical([p, q, signatures])) + return {"denominators": [2, 24], "numerator_rule": "-2q<=p<=2q; gcd(p,q)=1", + "ratios": ratios, "translation_tests": stable_tests, + "residue_response_tests": response_tests, + "offset_identity_tests": average_tests, + "signature_sha256": digest.hexdigest()} + + +def matrix_census(): + cases = [] + # These matrices include singular maps, nonprime moduli, and shared residues. + fixtures = [([[1, 0], [0, 1]], 2), ([[2, 0], [0, 2]], 4), + ([[1, 1], [2, 2]], 4), ([[2, 3], [4, 0]], 6), + ([[1, 2, 3], [0, 1, 1]], 4), ([[0, 0]], 5)] + for matrix, q in fixtures: + d = len(matrix[0]) + domain = list(product(range(q), repeat=d)) + + def image(z): + return tuple(sum(a * b for a, b in zip(row, z)) for row in matrix) + + def value(z): + return tuple(oracle(1, q, coordinate) for coordinate in image(z)) + + residues = {tuple(v % q for v in image(z)) for z in domain} + signatures = set() + stable_count = 0 + for h in domain: + differences = set() + for z in domain: + shifted = tuple(a + b for a, b in zip(z, h)) + differences.add(tuple(a - b for a, b in zip(value(shifted), value(z)))) + safe = all(v % q == 0 for v in image(h)) + need((len(differences) == 1) == safe, "matrix safe lattice failed") + stable_count += safe + for z in domain: + signature = [] + for h in domain: + shifted = tuple(a + b for a, b in zip(z, h)) + signature.append(tuple(a - b for a, b in zip(value(shifted), value(z)))) + signatures.add(tuple(signature)) + need(len(signatures) == len(residues), "matrix response state count failed") + need(len(residues) * stable_count == len(domain), "matrix quotient count failed") + cases.append({"matrix": matrix, "q": q, "domain": len(domain), + "safe_residues": stable_count, "response_classes": len(signatures)}) + return cases + + +def joint_census(): + cases = [] + for ratios in [((1, 2), (1, 3)), ((2, 3), (4, 9)), ((4, 3), (8, 7))]: + period = 1 + for _, q in ratios: + period = period * q // gcd(period, q) + signatures = { + tuple(oracle(p, q, z + h) - oracle(p, q, z) + for p, q in ratios for h in range(period)) + for z in range(period) + } + need(len(signatures) == period, "joint residual state count failed") + cases.append({"ratios": ratios, "classes_per_coordinate": len(signatures)}) + return cases + + +def borrowed_probe(borrow): + # F is any normalized function on Z/qZ. Enumerate every such function. + cases = [] + tree = (0, ((1, 2), 3)) + root_word = list(borrow.instructions(tree)) + child_calls = borrow.resources(tree[1])[1] + word = root_word[1:1 + child_calls] + need(child_calls == 10, "borrowed child boundary has changed") + for q in range(2, 6): + functions = additive_count = restored_count = boundaries = 0 + for tail in product(range(q), repeat=q - 1): + f = (0,) + tail + additive = all(f[(a + b) % q] == (f[a] + f[b]) % q + for a in range(q) for b in range(q)) + restored = True + for x, y, z in product(range(q), repeat=3): + # Execute the ten primitive calls with identity neighbors. + state = [0, y, x, z, 0] + for s, t, factor, sign in word: + increment = f[state[s]] if factor == 2 else state[s] + state[t] = (state[t] + sign * increment) % q + restored &= state[3] == z + boundaries += 1 + need(restored == additive, "borrowed boundary equivalence failed") + functions += 1 + additive_count += additive + restored_count += restored + need(additive_count == q, "cyclic endomorphism count failed") + cases.append({"group_order": q, "normalized_functions": functions, + "additive": additive_count, "restoring": restored_count, + "boundary_states": boundaries}) + return cases + + +def finite_accuracy(): + rows = [] + for width in range(0, 9): + scale = 1 << width + errors = [] + for slope in range(-2, 5): + error = max(abs(Fraction(slope * n, scale) - Fraction(4 * n, 3 * scale)) + for n in range(-scale, scale + 1)) + errors.append(error) + need(min(errors) == Fraction(1, 3), "physical unit-range gap failed") + rounded_error = max(abs(Fraction(oracle(4, 3, n), scale) + - Fraction(4 * n, 3 * scale)) + for n in range(-scale, scale + 1)) + need(rounded_error == Fraction(1, 3 * scale), "rounded error scale failed") + rows.append({"width": width, "source_points": 2 * scale + 1, + "best_additive_error": str(min(errors)), + "rounded_error": str(rounded_error)}) + return rows + + +def pinned_execution(borrow, dirty): + width = 12 + unit = Fraction(1, 1 << width) + beta = Fraction(1, 2) + factors = [] + executions = 0 + for numerator, expected in ((1, 1), (-1, 0), (3, 2), (-3, -1)): + need(dirty.rnd((Fraction(numerator, 2) * unit, Fraction(0)), width) + == (expected * unit, Fraction(0)), "PR985 data tie convention failed") + for bits in range(2, 9): + p, q = 1 << bits, (1 << bits) - 1 + b = (Fraction(1, p), Fraction(0)) + for z in (-q - 1, -q, -1, 0, 1, q - 1, q, q + 1): + for target in (-7, 0, 5): + x = [(z * unit, Fraction(0))] + y = [(target * unit, Fraction(0))] + original_x, original_y = list(x), list(y) + meter = dirty.lift(x, y, b, beta, width, 0) + need(x == original_x, "PR985 diagonal source changed") + need(y[0] == ((target + oracle(p, q, z)) * unit, Fraction(0)), + "PR985 diagonal differs from nearest rational map") + dirty.lift(x, y, b, beta, width, 0, sign=-1) + need(x == original_x and y == original_y, "PR985 inverse failed") + executions += 2 + factors.append({"coefficient_bits": bits, "p": p, "q": q, + "residue_states_per_coordinate": q}) + tree = (0, ((1, 2), 3)) + word = list(borrow.instructions(tree)) + initial = [-2, -2, -2, 1, -2] + arrays = [[(v * unit, Fraction(0))] for v in initial] + counters = {"reads": 0, "writes": 0, "tape_moves": 0, + "products": 0, "divisions": 0} + + def execute(records): + nonlocal executions + for s, t, factor, sign in records: + meter = dirty.lift(arrays[s], arrays[t], (Fraction(1, 4), Fraction(0)), + beta, width, 0, sign=sign) + for key in counters: + counters[key] += getattr(meter, key) + executions += 1 + + execute(word) + final = [int(row[0][0] / unit) for row in arrays] + need(final == [-2, -10, -2, 2, -2], "rounded borrowed boundary fixture changed") + need(final[2:] != initial[2:], "rounded helper failure was not observed") + execute(inverse(word)) + need([row[0][0] / unit for row in arrays] == initial, + "literal inverse did not restore the complete rounded state") + return {"width": width, "diagonal_families": factors, "leaf_executions": executions, + "borrowed_tree": tree, "borrowed_calls": len(word), "initial_units": initial, + "final_units": final, "literal_inverse_units": initial, + "borrowed_forward_and_inverse_meter": counters} + + +def lift_census(borrow): + rows = [] + _, plans, _ = borrow.unit_plan(16) + for n in (2, 3, 4, 5, 8, 16): + for tree in dict.fromkeys((plans[n - 1], borrow.balanced_binary(n))): + word = list(borrow.instructions(tree)) + degree = prefix_degree(word, 5) + for length in (1, 3): + initial = [[(r + 2) * (j + 1) - 5 for j in range(length)] for r in range(5)] + state, denominator, count = exact_lift(word, initial, 4, 3, degree) + expected = [[Fraction(value) for value in row] for row in initial] + for j in range(length): + expected[1][j] += Fraction(4, 3) ** n * initial[0][j] + need([[Fraction(v, denominator) for v in row] for row in state] == expected, + "finite exact lift or helper restoration failed") + need(count["exact_divisions"] == len(word) * length, + "finite lift division bill failed") + need(denominator % (3 ** n) == 0, "endpoint denominator was not paid") + need(count["source_reads"] == count["target_reads"] == count["writes"] + == len(word) * length, "finite lift access bill failed") + # The independent rational oracle checks every literal prefix. + rational = [[Fraction(v) for v in row] for row in initial] + integer = [[v * denominator for v in row] for row in initial] + peak = max(abs(v) for row in integer for v in row) + for s, t, factor, sign in word: + for j in range(length): + rational[t][j] += sign * Fraction(4, 3) * rational[s][j] + numerator = 4 * integer[s][j] + need(numerator % 3 == 0, "oracle found an inexact division") + integer[t][j] += sign * (numerator // 3) + need(Fraction(integer[t][j], denominator) == rational[t][j], + "exact lift prefix differs from rational oracle") + peak = max(peak, abs(numerator), abs(integer[t][j])) + need(count["peak_signed_bits"] == peak.bit_length() + 1, + "finite lift peak width failed") + magnitude = max(abs(v) for row in initial for v in row) + prefix_bound = borrow.norm_bound(tree, 2) + bit_bound = (4 * magnitude * prefix_bound * denominator).bit_length() + 1 + need(count["peak_signed_bits"] <= bit_bound, + "finite lift exceeds its stated signed width") + round_trip, _, round_trip_count = exact_lift( + word + inverse(word), initial, 4, 3, degree) + need(round_trip == [[v * denominator for v in row] for row in initial], + "integer inverse did not restore every extended array") + need(round_trip_count["exact_divisions"] == 2 * len(word) * length, + "integer inverse work was not paid") + for s, t, factor, sign in inverse(word): + for j in range(length): + rational[t][j] += sign * Fraction(4, 3) * rational[s][j] + need(rational == initial, "finite lift literal inverse failed") + rows.append({"factors": n, "tree": tree, "length": length, + "calls": len(word), "maximum_prefix_degree": degree, + "denominator": str(denominator), "signed_width_bound": bit_bound, + "round_trip_divisions": round_trip_count["exact_divisions"], + "invoice": count}) + return rows + + +def controls(borrow): + labels = [] + need(nearest(1, 2) == 1 and nearest(-1, 2) == 0, + "nearest tie convention failed") + need(round(Fraction(1, 2)) != nearest(1, 2), "nearest-even control is ineffective") + labels.append("nearest_even_is_not_the_data_rounder") + need(int(Fraction(2, 3)) != nearest(2, 3), "truncation control is ineffective") + labels.append("coefficient_truncation_is_not_data_rounding") + need(residue_response(4, 3, 0, 1) != residue_response(4, 3, 1, 1), + "discarded residue control is ineffective") + labels.append("discarded_residue_changes_a_required_response") + need(nearest(8, 3) != 2 * nearest(4, 3), "additive wrapper defect not detected") + labels.append("nearest_source_increment_is_not_additive") + need(nearest(4 * 3, 3) == 4 and nearest(4, 3) * 3 == 3, + "constant first difference control is ineffective") + labels.append("full_period_refutes_constant_first_differences") + need(offset_sum(4, 3, 1) != nearest(4, 3), "averaging scaling control is ineffective") + labels.append("offset_averaging_returns_the_scaled_integer_map") + # Reaccess defeats the summary restriction, with no saved residue. + for z in range(-12, 13): + for h in range(-12, 13): + current = z + h + recovered = current - h + need(nearest(4 * current, 3) - nearest(4 * recovered, 3) + == oracle(4, 3, z + h) - oracle(4, 3, z), + "zero-summary reaccess escape failed") + labels.append("readable_current_and_shift_allow_zero_summary") + word = list(borrow.instructions((0, ((1, 2), 3)))) + initial = [[1], [2], [3], [4], [5]] + try: + exact_lift(word, initial, 4, 3, 0) + except ValueError as error: + need(str(error) == "exact lift needs more denominator precision", + "wrong failure for omitted precision extension") + else: + raise ValueError("omitted precision extension was accepted") + labels.append("zero_precision_extension_rejects_inexact_division") + # A coarser source grid and a finer target grid admit the exact ratio. + for z in range(-20, 21): + physical_source = Fraction(z) + target_units = 4 * z + need(Fraction(target_units, 3) == Fraction(4, 3) * physical_source, + "different-grid escape failed") + labels.append("different_input_and_output_grids_escape_integer_slope") + return labels + + +def compute(): + base, pins = sources() + borrow = load_module("pinned_borrow", ROOT / "vendor/pr1057/borrow.py") + dirty = load_module("pinned_dirty", ROOT / "vendor/pr985/dirty_stride.py") + selected = {} + for label in ("base", "refresh"): + context = json.loads((ROOT / "context" / (label + "-selected-result.json")).read_text()) + selected[label] = {"kappa": context["kappa"], "primary_pr": context["source_prs"][0]} + return {"format": 1, "base_commit": base, "pinned_files": pins, + "selected_context": selected, + "scalar_census": scalar_census(), "matrix_census": matrix_census(), + "joint_census": joint_census(), "borrowed_probe": borrowed_probe(borrow), + "physical_accuracy": finite_accuracy(), + "pinned_execution": pinned_execution(borrow, dirty), + "finite_exact_lifts": lift_census(borrow), "controls": controls(borrow)} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, + help="write a fresh receipt to a path that does not exist") + args = parser.parse_args() + if args.output and args.output.exists(): + raise FileExistsError("receipt path already exists") + result = compute() + expected = json.loads((ROOT / "EXPECTED.json").read_text()) + need(canonical(result) == canonical(expected), "complete receipt differs from EXPECTED.json") + if args.output: + with args.output.open("x") as stream: + json.dump(result, stream, indent=2, sort_keys=True) + stream.write("\n") + print("PASS_ROUNDED_BORROWING_CONTRACT " + f"ratios={result['scalar_census']['ratios']} " + f"responses={result['scalar_census']['residue_response_tests']} " + f"rounded_leaves={result['pinned_execution']['leaf_executions']} " + f"exact_lifts={len(result['finite_exact_lifts'])} " + f"controls={len(result['controls'])}") + + +if __name__ == "__main__": + main()