From 983c2cebd7946c26a1251c07ea7dabff601d5243 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 3 Nov 2026 09:16:25 +0000 Subject: [PATCH] feat(research): prove the rounded dyadic connector carry --- research/rounded-dyadic-conjugation/PROOF.md | 146 ++++++++++++ research/rounded-dyadic-conjugation/README.md | 116 ++++++++++ .../rounded-dyadic-conjugation/SOURCES.json | 24 ++ research/rounded-dyadic-conjugation/TASK.json | 80 +++++++ .../rounded-dyadic-conjugation/VERIFY.json | 36 +++ research/rounded-dyadic-conjugation/verify.py | 212 ++++++++++++++++++ 6 files changed, 614 insertions(+) create mode 100644 research/rounded-dyadic-conjugation/PROOF.md create mode 100644 research/rounded-dyadic-conjugation/README.md create mode 100644 research/rounded-dyadic-conjugation/SOURCES.json create mode 100644 research/rounded-dyadic-conjugation/TASK.json create mode 100644 research/rounded-dyadic-conjugation/VERIFY.json create mode 100644 research/rounded-dyadic-conjugation/verify.py diff --git a/research/rounded-dyadic-conjugation/PROOF.md b/research/rounded-dyadic-conjugation/PROOF.md new file mode 100644 index 0000000000..bb1d69f8f6 --- /dev/null +++ b/research/rounded-dyadic-conjugation/PROOF.md @@ -0,0 +1,146 @@ +# Rounded dyadic conjugation and a sharp root carry + +This scoped proof concerns the two local replacements and the displayed B0 +repair in Hanson Sun / bbMisk's PR1526. That work supplies the exact word and +its exact-arithmetic context. Its optimality theorem is a cited predecessor +result, not a claim re-established here. + +## Rounded child contract + +Fix a positive grid spacing h. All public real coordinates lie in hZ. +Complex arrays use this contract separately on their real and imaginary +coordinates. Coefficients and source products can be arbitrary real numbers. +Define the translation-equivariant nearest rounder + +``` +Q_h(t) = h floor(t/h + 1/2). +``` + +At a tie it chooses the larger grid point. A signed rounded query updates +its destination by `s Q_h(F(source))`, where s is +1 or -1. Its source and +other roles stay fixed. Rounding happens before applying the sign. The +literal inverse subtracts the identical rounded value. It does not evaluate +`Q_h(-F(source))`. The latter convention can fail at ties. + +Within a halved-root interval the root uses the common h/2 grid. The scale +operations H and D divide and multiply the root by two exactly. This is a +specified additive child contract. A child with target-dependent errors, +inexact scaling or input-dependent precision needs a separate argument. + +## The local theorem + +Let v=Bx and let z be an arbitrary dirty root in hZ. Application order is +left to right. The refined source interval is + +``` +H; z += s Q_(h/2)(v); D + z -> z + 2s Q_(h/2)(v) = z + s Q_h(2v). +``` + +The equality follows directly from the floor definition. Its error against +`z+2sv` has absolute value at most h/2 in every real coordinate. Two ordinary +rounded queries instead give `z+2s Q_h(v)`, with sharp error bound h. +Both bounds are attained: v=h/4 attains h/2 in the refined interval, and +v=h/2 attains h for the repeated interval. No hZ-valued endpoint can have +a uniform error below h/2, since the ideal increment can equal h/2. Thus the +refined endpoint is minimax optimal in that output lattice. + +For the output query, linearity gives + +``` +D; y += s Q_h(Az); H + (z,y) -> (z, y+s Q_h(2Az)). +``` + +It has the same sharp h/2 coordinate error without refining the output grid. +Both intervals have exact literal inverses under the stated sign rule. +They do not require zero dirty data. + +For H B D, one extra fractional bit for the root is sufficient, and necessary +in the fixed common-grid representation of its initial exact H: H sends z=h +to h/2, which is absent from hZ. An equivalent residue flag also has two +possible classes modulo h. This necessity concerns representing this H, +not every possible implementation of the doubled query. The final H of +D A H acts on 2hZ and needs no finer fractional grid. Doubling can also +need one more magnitude bit. Neither storage nor either scan is free here. + +## Local accuracy does not preserve the complete root boundary + +Take the literal B0 repair displayed in PR1526: + +``` +B0- A1- H B0+ D A2+ B1+ A0+ B0- A2- B2- A1+ B1- A0- B2+ +``` + +All ordinary B queries use Q_h; the B0 query between H and D uses Q_(h/2). +All A queries use Q_h and never change the root. Sources never change. +The first B0- is halved and then doubled, so its eventual root contribution +is -Q_h(v). The special B0+ contributes Q_h(2v). The later B0- contributes +-Q_h(v). B1 and B2 each cancel exactly. Therefore, for arbitrary linear +operators, source data and dirty root, + +``` +z_final = z_initial + rho_h(v), +rho_h(v) = Q_h(2v) - 2 Q_h(v), v = B0 x0. +``` + +This is an exact endpoint formula for this rounded word. It makes no claim +that the rounded output rows equal their ideal linear values. + +Set r=v-Q_h(v), so -h/2 <= r < h/2. Integer translation equivariance gives +rho_h(v)=Q_h(2r), hence + +``` +rho_h(v) = -h if -h/2 <= r < -h/4, + 0 if -h/4 <= r < h/4, + +h if h/4 <= r < h/2. +``` + +All three cases occur. For a tie-free counterexample choose h=1, B0=1/8, +x0=3 and z_initial=0. All public inputs are on the integer grid. Take the +other source values and all A maps to be zero. The refined word ends at +z=1, although its exact-arithmetic root boundary requires z=0. The signed +partner x0=-3 ends at z=-1. These examples also establish the sharp root +error h. They are errors of this newly specified rounded extension, not +errors in PR1526's exact-arithmetic theorem. + +The refined word restores its dirty root exactly if and only if every real +coordinate has rho_h(B0x0)=0. Merely adding the one fractional bit does not +establish this condition. + +## Two explicit ways to satisfy the root boundary + +First, retain Q_h for the special B query, while retaining the h/2 root +representation for exact H. Then H B D is exactly the same rounded map as +two coarse B queries. The complete root restores for all inputs, but the +local error bound remains h. This option gives no local accuracy gain. + +Second, use the refined query and append a root shear by -rho_h(B0x0) +after every output read. This restores the root and leaves the already +computed outputs fixed. Its inverse adds the same correction before the +literal inverse of the word. The correction has exactly three possible +values per real coordinate. Computing, delivering or retaining it requires +an explicit bill; no free correction or optimal implementation is claimed. +This is an algebraic repair of the root boundary only. + +A coarse whole-target rounding is a different operation. With v=0, the +map `z -> 2 Q_h(z/2)` identifies z=-h and z=0 under the stated tie rule. +It loses arbitrary dirty information. It cannot replace the refined +additive child as a reversible exact H-B-D interval. + +## Scope and evidence + +The proof applies in every finite array dimension coordinatewise. The +verifier checks exact rational local intervals, the carry partition and +the full 15-event word with noncommuting two-coordinate matrix maps and +arbitrary dirty fixtures. It also multiplies literal inverse words. +Finite fixtures corroborate the implementation; the universal claim rests +on the equations above. A complete rounded connector output-error budget, +native child realization, physical correction bill, compiler admission, +precision/tape hosting and a new multiplication theorem remain open. + +The new result was produced by Nick Petalas. Credit Hanson Sun / bbMisk +for PR1526, Ross Richardson for PR944, martinxxx9 for PR1088, and the +retained signed-connector lineage. Nearest-grid rounding and elementary +error transport are classical. Independent human and formal proof-kernel +review are unclaimed. Apache-2.0. diff --git a/research/rounded-dyadic-conjugation/README.md b/research/rounded-dyadic-conjugation/README.md new file mode 100644 index 0000000000..4f8035aac4 --- /dev/null +++ b/research/rounded-dyadic-conjugation/README.md @@ -0,0 +1,116 @@ +# A sharp rounding carry at the dyadic connector boundary + +**Scoped proof with exact finite corroboration. No new kappa.** This answers +one bounded part of the approximate-child question in Hanson Sun / bbMisk's +[PR1526](https://github.com/CrocSwap/integer-mult-bounds/pull/1526). + +For the deterministic nearest-grid additive child +`Q_h(t)=h floor(t/h+1/2)`, one additional fractional bit makes `H B D` compute +`z+s Q_h(2Bx)`. Its sharp coordinate error is h/2, versus h for two ordinary +rounded queries. `D A H` also has sharp error h/2 and restores its root. +Both intervals have exact literal inverses when the sign is applied after +rounding. The extra root bit and both scale passes remain paid obligations. + +The local accuracy improvement creates an exact dirty-root obstruction in +PR1526's displayed B0 repair: + +``` +z_final - z_initial = rho_h(B0 x0), +rho_h(v) = Q_h(2v) - 2 Q_h(v) in {-h, 0, h}. +``` + +Every value occurs. With h=1, B0=1/8 and x0=3, the word leaves root error 1 +even with zero output maps. Keeping coarse rounding in the special B query +restores cancellation, with the original error h. A final correction by +`-rho_h(B0 x0)` also restores the root, but needs its own implementation and +invoice. One extra fractional bit alone does not admit the refined word. + +[PROOF.md](PROOF.md) proves the local optimum, the exact three-interval carry +classification, the necessary and sufficient root-restoration condition, and +the two stated root repairs. This is a new rounded extension of the exact +predecessor circuit. It does not identify an error in that exact circuit or +re-establish its optimum. + +## Reproduce + +From the repository root, CPython 3.12 and the standard library suffice: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/rounded-dyadic-conjugation +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/rounded-dyadic-conjugation/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/rounded-dyadic-conjugation/verify.py +``` + +The direct verifier emits a generated JSON receipt bound to all six package +file hashes, followed by `PASS_ROUNDED_DYADIC_CONJUGATION`. It writes no files. +Both registered commands use warning-strict isolated normal and optimized +execution. The checks enumerate 3,402 source intervals, 1,050 output intervals, +102 complete rounded-word fixtures and eight controls. The full-word fixtures +use two-coordinate noncommuting matrices, immutable sources, dirty outputs +and dirty roots, and replay literal inverses. Coarse/refined root endpoints +and the correction agree with the proved formulas. + +The controls compute failures of coarse whole-target rounding, rounding the +negative as an inverse, omitted doubling, missing/wrong carry correction and +the false coarse h/2 error bound. They also check the root representation +requirement and reject a zero grid. No predecessor executable is imported or +replayed. The card's 945-pairing positive control and selected binding-only +orientation were run separately as required orientation, not as contributions. + +## Scope and provenance + +Canonical base `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8, +selected PR6030. [SOURCES.json](SOURCES.json) pins the predecessor README as +the sole live input. [TASK.json](TASK.json) retains the original +`connector-alphabet-change` card and records the changed scope to its open +rounded-interface question. The +[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19370233) +targets this local precision and admissibility decision. + +Live open PRs, recent account work, handoff claims and local reservations were +checked before claiming. Canonical-main README searches and merged searches +used PR1526, dyadic connector, rounded conjugation, root carry and related +terms. The overlap helper searched 506 open PRs and 6,502 discussion records +with complete remote pagination; its sparse local scan covered 118 of 8,917 +HEAD note records. Separate Git searches covered committed READMEs for the +target terms. These searches omit arbitrary diffs and unpublished work and +do not prove novelty. PR1556 concerns exact unit-phase query tariffs; +PR1770 concerns a different five-source binary connector. Neither supplies +this rounded carry formula. + +The claim requires exact dyadic scales and source-only deterministic rounded +increments with the specified tie and inverse rules. It does not cover +target-dependent defects or inexact H/D. The full connector output-error +budget, actual recursive/native child, physical correction tariff, compiler, +stock, tape and outer recovery remain unproved. All five selected framework +assumptions remain. No selected cold replay, Lean, Docker, independent human +review or proof-kernel acceptance is claimed. + +## Engineering constraints + +The verifier has no recursion or subprocesses. Its arithmetic loops have fixed +finite bounds, its word has 15 events and its state has seven two-coordinate +rows. Every function is below 60 lines. Contracts use explicit exceptions and +remain enabled under optimized execution. Python allocates managed arithmetic +objects during execution; fixed fixtures and fixed-size live state bound their +number. This is the managed-runtime deviation from static allocation. +Warning-strict normal and optimized executions supply the relevant diagnostics. + +## Open next questions + +1. Can an actual recursive B child supply the carry repair for less than the + removed child price after paying both scans? Begin with one literal native + source, its exact coefficient precision and a paid source-only correction. + Physical evaluation, routing and restoration costs are the blockers. +2. What is the complete output-error budget of the repaired rounded word? + Propagate its actual rounded errors through every A read, keeping the carry + until its final correction. The local radius and restored root do not bound + those outputs. This needs a specified native norm and caller allowance. + +## Credit + +This contribution was produced by Nick Petalas. Credit Hanson Sun / bbMisk +for PR1526's exact word and open precision question, Ross Richardson for +PR944, martinxxx9 for PR1088, and the retained signed-connector lineage. +Nearest-grid rounding is classical. Independent human and formal proof-kernel +review are unclaimed. Apache-2.0. diff --git a/research/rounded-dyadic-conjugation/SOURCES.json b/research/rounded-dyadic-conjugation/SOURCES.json new file mode 100644 index 0000000000..f111c5df85 --- /dev/null +++ b/research/rounded-dyadic-conjugation/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/complex-dyadic-connector-seed30/README.md", + "usage": "input", + "git_blob": "be139d563622ceb7948f8c8bff67155be18049b0", + "sha256": "88683e74286f7406fd4c9ec79c4e521706594221f7d7c00687dad007240e21c9" + } + ] +} diff --git a/research/rounded-dyadic-conjugation/TASK.json b/research/rounded-dyadic-conjugation/TASK.json new file mode 100644 index 0000000000..11e3672f8f --- /dev/null +++ b/research/rounded-dyadic-conjugation/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment.", + "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "scope_status": "changed", + "actual_scope": "Sharp nearest-grid error for H B D and D A H, and the exact ternary dirty-root carry of PR1526's displayed B0 repair.", + "scope_change_reason": "The card asks for a new connector operation. This answers the predecessor's explicit open precision question for its already extended alphabet, a scoped interface side result.", + "bottleneck_link": "An exact child-query saving cannot be admitted through this refined rounding rule without paying its root carry or retaining coarse rounding; no physical supplier or new kappa is claimed.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified local precision/admissibility result. Do not extend to other repairs, scales or output budgets.", + "outcome": "completed", + "evidence": "PROOF.md gives the universal coordinatewise argument. verify.py corroborates 3402 source intervals, 1050 output intervals, 102 complete rounded-word fixtures and eight controls; receipts hash all six package files.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can an actual recursive B child deliver the ternary carry repair within the removed child allowance?", + "why_it_matters": "The correction can repay the exact-arithmetic query saving.", + "first_step": "Specify one native B source and price coefficient evaluation, both root scans, correction delivery and restoration.", + "blocked_by": "No native correction circuit or complete physical invoice is supplied." + }, + { + "question": "What is the complete output-error budget of the repaired rounded word?", + "why_it_matters": "A restored root and local sharp radius do not bound downstream output errors.", + "first_step": "Propagate actual rounded query errors through all A reads under a specified native norm.", + "blocked_by": "A native norm, child precision and caller allowance have not been bound." + } + ], + "coordination": { + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19370233", + "source_pr": 1526, + "source_author": "bbMisk", + "selected_pr": 6030, + "source_head": "1fb85dc6813b88483f4f0a359ccd722376acd292" + }, + "environment": { + "python": "CPython 3.12.15", + "platform": "Darwin arm64", + "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12" + } +} diff --git a/research/rounded-dyadic-conjugation/VERIFY.json b/research/rounded-dyadic-conjugation/VERIFY.json new file mode 100644 index 0000000000..9f255b2956 --- /dev/null +++ b/research/rounded-dyadic-conjugation/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/complex-dyadic-connector-seed30/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Sharp local radii, carry partition, complete rounded root endpoint, literal inverse and eight controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Identical checks with optimized execution and explicit runtime contracts." + } + ] +} diff --git a/research/rounded-dyadic-conjugation/verify.py b/research/rounded-dyadic-conjugation/verify.py new file mode 100644 index 0000000000..fdc226eef2 --- /dev/null +++ b/research/rounded-dyadic-conjugation/verify.py @@ -0,0 +1,212 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the new rounded conjugation lemma.""" +from fractions import Fraction as F +from hashlib import sha256 +import json +from pathlib import Path +import sys + + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +WORD = "B0- A1- H B0+ D A2+ B1+ A0+ B0- A2- B2- A1+ B1- A0- B2+".split() + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def rounded(value, step): + require(step > 0, "positive grid required") + scaled = value / step + F(1, 2) + return step * (scaled.numerator // scaled.denominator) + + +def carry(value, step): + return rounded(2 * value, step) - 2 * rounded(value, step) + + +def source_interval(root, value, step, sign, refined): + child_grid = step / 2 if refined else step + return 2 * (root / 2 + sign * rounded(value, child_grid)) + + +def local_checks(): + source_cases = 0 + output_cases = 0 + carries = set() + for step in (F(1, 2), F(1), F(2)): + for numerator in range(-40, 41): + value = numerator * step / 16 + residue = value - rounded(value, step) + expected = -step if residue < -step / 4 else ( + step if residue >= step / 4 else F(0)) + require(carry(value, step) == expected, "carry partition") + carries.add(carry(value, step) / step) + for dirty in range(-3, 4): + root = dirty * step + for sign in (-1, 1): + new = source_interval(root, value, step, sign, True) + coarse = source_interval(root, value, step, sign, False) + require(new == root + sign * rounded(2 * value, step), + "refined source endpoint") + require(coarse == root + 2 * sign * rounded(value, step), + "coarse source endpoint") + require(abs(new - root - 2 * sign * value) <= step / 2, + "refined source error") + require(abs(coarse - root - 2 * sign * value) <= step, + "coarse source error") + require(source_interval(new, value, step, -sign, True) + == root, "source literal inverse") + source_cases += 1 + for dirty in range(-3, 4): + root = dirty * step + for coefficient in (F(-3), F(-1, 2), F(0), F(1, 4), F(2)): + for target in range(-2, 3): + for sign in (-1, 1): + y = target * step + doubled = 2 * root + result = y + sign * rounded(coefficient * doubled, step) + require(doubled / 2 == root, "output root restoration") + require(abs(result - y - 2 * sign * coefficient * root) + <= step / 2, "output error") + require(result - sign * rounded(coefficient * doubled, + step) == y, + "output literal inverse") + output_cases += 1 + require(abs(rounded(2 * step / 4, step) - step / 2) == step / 2, + "sharp refined radius") + require(abs(2 * rounded(step / 2, step) - step) == step, + "sharp repeated radius") + require(carries == {F(-1), F(0), F(1)}, "all carry values attained") + return source_cases, output_cases + + +def matvec(matrix, vector): + return tuple(sum(matrix[i][j] * vector[j] for j in range(2)) + for i in range(2)) + + +def run_word(initial, a_maps, b_maps, step, refined, inverse=False): + state = list(initial) + indices = range(14, -1, -1) if inverse else range(15) + for index in indices: + token = WORD[index] + if token in ("H", "D"): + factor = F(1, 2) if token == "H" else F(2) + if inverse: + factor = 1 / factor + state[6] = tuple(factor * x for x in state[6]) + continue + role = int(token[1]) + sign = 1 if token[2] == "+" else -1 + if inverse: + sign = -sign + if token[0] == "B": + destination = 6 + increment = matvec(b_maps[role], state[role]) + grid = step / 2 if refined and index == 3 else step + else: + destination = 3 + role + increment = matvec(a_maps[role], state[6]) + grid = step + state[destination] = tuple(state[destination][j] + + sign * rounded(increment[j], grid) + for j in range(2)) + return tuple(state) + + +def word_checks(): + a_maps = (((F(1), F(1, 2)), (F(0), F(1))), + ((F(0), F(1)), (F(-1), F(0))), + ((F(1), F(0)), (F(1), F(1)))) + b_maps = (((F(1, 8), F(0)), (F(0), F(3, 8))), + ((F(1), F(1)), (F(0), F(1))), + ((F(1), F(0)), (F(1), F(-1)))) + cases = 0 + observed = set() + for step in (F(1, 2), F(1), F(2)): + for seed in range(17): + initial = tuple(tuple(((seed * (i + 1) + 3 * j) % 7 - 3) * step + for j in range(2)) for i in range(7)) + value = matvec(b_maps[0], initial[0]) + rho = tuple(carry(x, step) for x in value) + for refined in (False, True): + final = run_word(initial, a_maps, b_maps, step, refined) + require(final[:3] == initial[:3], "immutable source rows") + expected = tuple(initial[6][j] + (rho[j] if refined else 0) + for j in range(2)) + require(final[6] == expected, "full rounded root endpoint") + require(run_word(final, a_maps, b_maps, step, refined, True) + == initial, "full literal inverse") + if refined: + corrected = tuple(final[6][j] - rho[j] for j in range(2)) + require(corrected == initial[6], "paid root correction") + observed.update(x / step for x in rho) + cases += 1 + require(observed == {F(-1), F(0), F(1)}, "full-word carry coverage") + return cases + + +def controls(): + # These compute wrong alternatives and require a concrete counterexample. + checks = { + "half_grid_is_needed": F(1, 2).denominator != 1, + "coarse_full_target_rounding_loses_dirty_root": + 2 * rounded(F(-1, 2), F(1)) == 2 * rounded(F(0), F(1)), + "rounding_the_negative_is_not_the_inverse": + rounded(F(1, 2), F(1)) + rounded(F(-1, 2), F(1)) != 0, + "omitting_final_double_changes_the_map": + F(1, 2) + rounded(F(3, 8), F(1, 2)) + != source_interval(F(1), F(3, 8), F(1), 1, True), + "omitting_carry_repair_leaves_a_root_error": + carry(F(3, 8), F(1)) == 1, + "wrong_sign_carry_repair_doubles_error": + carry(F(3, 8), F(1)) + carry(F(3, 8), F(1)) == 2, + "coarse_child_cannot_claim_half_grid_error": + abs(2 * rounded(F(1, 2), F(1)) - 1) > F(1, 2), + } + for name, condition in checks.items(): + require(condition, "missing counterexample: " + name) + try: + rounded(F(0), F(0)) + except ValueError: + return sorted(checks) + ["zero_grid_rejected"] + raise ValueError("zero grid was accepted") + + +def authenticate(): + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + require(len(manifest["files"]) == 3, "source inventory changed") + for row in manifest["files"]: + if row["usage"] == "input": + payload = (ROOT / row["path"]).read_bytes() + require(sha256(payload).hexdigest() == row["sha256"], "source drift") + require(" ".join(WORD) in payload.decode(), "source word mismatch") + + +def main(): + require(len(sys.argv) == 1, "no arguments supported") + authenticate() + source_cases, output_cases = local_checks() + report = { + "claim_type": "scoped proof with exact finite corroboration", + "source_interval_cases": source_cases, + "output_interval_cases": output_cases, + "complete_word_cases": word_checks(), + "controls": controls(), + "root_carry_over_h": [-1, 0, 1], + "new_source_error_over_h": "1/2", + "repeated_source_error_over_h": "1", + "package_sha256": { + name: sha256((PACKAGE / name).read_bytes()).hexdigest() + for name in ("PROOF.md", "README.md", "SOURCES.json", "TASK.json", + "VERIFY.json", "verify.py")}, + } + print(json.dumps(report, indent=2, sort_keys=True)) + print("PASS_ROUNDED_DYADIC_CONJUGATION") + + +if __name__ == "__main__": + main()