diff --git a/research/reversible-phase-tie-optimum/PROOF.md b/research/reversible-phase-tie-optimum/PROOF.md new file mode 100644 index 0000000000..068e921333 --- /dev/null +++ b/research/reversible-phase-tie-optimum/PROOF.md @@ -0,0 +1,148 @@ +# A sharp tie choice for a reversible rational phase + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Statement + +Let h>0 be the grid spacing, and let R be multiplication by (3+4i)/5. +Use integer numerators x,y for a point h(x+iy). Define + +```text +u = x - ceil(y/2) +v = y + nearest(4u/5) +w = u - floor(v/2) +F(x,y) = (w,v). +``` + +There are no half-integer ties in nearest(4u/5). Then F is a bijection of +Z² and + + ||h F(x,y) - R h(x,y)||² <= (4/5) h². (1) + +The constant is attained. The inverse has the same sharp error bound +relative to R inverse. Among the four programs obtained by choosing a fixed +upward or downward half-integer tie direction independently in the first +and last shear, the minimum squared error constant is exactly 4/5. +Both opposite-tie programs attain it. Each same-tie program has sharp +constant 1. This is optimality within four specified programs, not among +all reversible rounding algorithms or lattice bijections. + +The standard rounded-shear factorization is predecessor work. The new step +is the correlated residue calculation and the improved tie choice, together +with its sharp all-grid guarantee. PR2589 gives the same-tie lifting control +and the valid sufficient bound 153/80. That bound is cited, not disputed. + +## Exact inversion + +Each update changes one integer coordinate by a function of the unchanged +coordinate. Undo the updates in reverse order, with the same rounding rules: + +```text +u = w + floor(v/2) +y = v - nearest(4u/5) +x = u + ceil(y/2). +``` + +Thus both compositions with F are identity on the entire integer grid. +No input-dependent history, additional output or clean helper is needed +in this logical two-coordinate map. This statement does not price evaluation +or erasure of a physical quotient instruction's workspace. + +## Finite quotient proves the all-grid bound + +Write a,b in {0,1} for the first and last tie directions. Rounding n/2 is +floor((n+a)/2), and nearest(4u/5) is floor((8u+5)/10). Let F_ab be this +three-update program. For every integer input, direct substitution gives + + F_ab(x+5,y) = F_ab(x,y) + (3,4), + F_ab(x,y+10) = F_ab(x,y) + (-8,6). (2) + +For the first relation, u increases by 5, the middle rounded increment +increases by 4, and the last rounded half increases by 2. For the second, +u decreases by 5, v increases by 6, and the last half increases by 3. +These are exact integer shifts for either tie direction, including negative +inputs. The displayed output shifts are R(5,0) and R(0,10). Consequently + + E_ab(x,y) = 5 F_ab(x,y) - (3x-4y, 4x+3y) + +is periodic on the lattice 5Z × 10Z. Every integer input has one unique +representative in 0<=x<5, 0<=y<10. There are exactly 50 cases per tie pair. +This is a mathematical reduction to a finite quotient, rather than an +inference from a bounded input sweep. + +For the chosen pair a=1,b=0 the complete residual table is + +| Residual E | Number of representatives | Squared length | +| --- | ---: | ---: | +| (-2,-1) | 5 | 5 | +| (-1,-3) | 5 | 10 | +| (-1,2) | 5 | 5 | +| (0,0) | 10 | 0 | +| (1,-2) | 10 | 5 | +| (2,-4) | 5 | 20 | +| (2,1) | 5 | 5 | +| (3,-1) | 5 | 10 | + +Each row follows by substituting the 50 representatives into the displayed +integer formulas. The verifier emits all residuals and their multiplicities +and compares each evaluation with a separate rational nearest-rounding +implementation. The maximum residual squared length is 20, proving (1). +For example, F(0,3)=(-2,1), with E=(2,-4), proves equality. + +The analogous four-program calculation is + +| First tie | Last tie | Maximum squared residual | Equality input | Output | +| --- | --- | ---: | --- | --- | +| Down | Down | 25 | (0,5) | (-3,3) | +| Down | Up | 20 | (0,7) | (-6,5) | +| Up | Down | 20 | (0,3) | (-2,1) | +| Up | Up | 25 | (0,3) | (-3,1) | + +The error squared is h²||E||²/25. This proves sharpness and the stated +four-program minimum. For any output z=F(x), orthogonality of R gives + + ||F inverse(z) - R inverse(z)|| = ||F(x) - R(x)||. + +Surjectivity of F transfers both the upper bound and its attainment to the +inverse. A separately rounded conjugate recipe is not assumed to be this +inverse. + +## Outward slack and the disk boundary + +The triangle inequality gives, uniformly over all inputs, + + ||h F(x,y)|| <= ||h(x,y)|| + (2/sqrt(5)) h. (3) + +This additive radial constant is also sharp over the full integer grid. +Take x_n=(-5n,3-10n), n>=1. Formula (2) and the equality input give + + F(x_n) = (5n-2,1-10n), + ||x_n||² = 125n²-60n+9, + ||F(x_n)||² - ||x_n||² = 20n-4. + +Rationalizing the difference of norms shows that it tends to +20/(2 sqrt(125)) = 2/sqrt(5). This proves sharpness of (3) without a +numerical approximation. In particular x_1=(-5,-7) has squared norm 74 +and image (3,-9) of squared norm 90. Exact return requires permitting this +outward motion. No claim is made that the same constant is minimal on the +particular disks with radius exactly 2^p in numerator units. + +## Scope and credit + +ywz65's +[PR2589](https://github.com/CrocSwap/integer-mult-bounds/pull/2589) and +`research/reversible-phase-disk-obstruction/model.py` supply the standard +rounded-shear control, the complete-disk return boundary and the question +of which changed interfaces can support reversible phases. Retain ywz65's +PR2527/PR2549, Mason Hale's PR2313 quantizer, Jose Manuel's PR2298 phase +context and the classical shear-lifting lineage credited there. No source +code is imported or vendored here. SOURCES.json pins the cited definitions +as provenance at the package base commit. + +The written periodicity argument and exhaustive 200-case arithmetic are +the scoped proof. Wider signed-grid, large-integer and semantic mutation +checks corroborate its implementation. Independent human and formal +proof-kernel review are unclaimed. A rational phase is a valid generic +phase-kernel input; it is not identified with a selected supplier root. +This result does not resolve precision_tape at an actual selected caller, +discharge an inherited framework assumption or improve kappa. diff --git a/research/reversible-phase-tie-optimum/README.md b/research/reversible-phase-tie-optimum/README.md new file mode 100644 index 0000000000..1db935da3f --- /dev/null +++ b/research/reversible-phase-tie-optimum/README.md @@ -0,0 +1,102 @@ +# Sharper reversible phase lifting by changing one tie rule + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Claim type: scoped proof with exact finite corroboration.** For the rational +phase (3+4i)/5, changing the final half-integer tie direction in the standard +three-shear lifting program reduces its sharp all-grid squared error from +h² to **(4/5)h²**, where h is the grid spacing. The new map and its inverse +are exact bijections of the full grid. Both opposite-tie choices attain 4/5; +both same-tie choices attain 1. The optimum is over these four fixed tie pairs. + +```text +u = x - ceil(y/2) +v = y + nearest(4u/5) +w = u - floor(v/2) +return (w,v) +``` + +[PROOF.md](PROOF.md) proves periodicity of the residual on 5Z × 10Z, +reducing the all-grid statement to 50 representatives per program. It gives +the full residual table, equality at (0,3), exact inverse and sharp additive +radial allowance 2h/sqrt(5). The program can move outward and does not preserve +each closed disk. For example (-5,-7) maps to (3,-9), increasing squared +radius from 74 to 90. + +## Predecessor and new step + +ywz65's [PR2589](https://github.com/CrocSwap/integer-mult-bounds/pull/2589) +supplies the standard reversible lifting control, a sufficient squared-error +bound 153/80, and the complete-disk obstruction. Its valid bound is cited, +not disputed. Classical three-shear lifting is not claimed as new. This +contribution changes one rounding rule and proves the correlated exact error +and fixed-family optimum. No predecessor mathematical verifier is imported +or replayed. Retain ywz65's PR2527/PR2549, Mason Hale's PR2313 quantizer, +Jose Manuel's PR2298 phase context and the source's classical lifting credit. +[SOURCES.json](SOURCES.json) binds the cited README and model as provenance. + +The `uniform-transfer-audit` card is explicitly **changed** to this generic +precision interface side result. The original card asks for an actual selected +caller and is not discharged. Current main was +`2485805a6d47f36ea83ddde6327d453ac82d44dc`, priority revision 8; the baseline +binding check passed at selected conditional kappa .003125804. The +[advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19299721) +names the phase, four tie pairs and first-improvement stopping rule. + +## Reproduce + +From the repository root, with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/reversible-phase-tie-optimum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/reversible-phase-tie-optimum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/reversible-phase-tie-optimum +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/reversible-phase-tie-optimum --check-source-history +``` + +An equivalent CPython 3.12 interpreter works elsewhere. The direct verifier +is standalone and prints a generated JSON receipt with status +`PASS_REVERSIBLE_PHASE_TIE_OPTIMUM`, all residual tables and SHA256 hashes of +the six package files. `--output NEW_PATH` exclusively writes that receipt; +normal replay leaves files unchanged. No hand-written receipt is supplied. + +The replay covers all 200 fundamental cases, 26,244 signed-grid cases with +both inverse compositions and both error directions, 5,600 signed translations +with shifts through 4,096 bits, eight radial-family instances, eight semantic +controls and six invalid tie-rule rejections. A separate Fraction/divmod +nearest-rounding implementation checks all fundamental and large-translation +cases. The written periodicity proof establishes the unbounded quantifier; +the wider sweeps are implementation evidence. + +## Limits and implementation discipline + +Optimality is restricted to the four specified constant tie policies. It does +not cover input-dependent policies, other factorizations or all lattice +bijections. The phase is a generic rational kernel input, not an identified +selected root. No physical quotient workspace, overflow/word-width budget, +phase-generation tariff, repeated-word error accumulation, native realization, +complete signed invoice or new kappa is supplied. The five selected framework +assumptions remain. Independent human and formal proof-kernel review are unclaimed. + +The verifier has no recursion or unbounded search. Each function is under +60 lines. Loop bounds are the stated finite fixture sizes, at most 26,244 +grid cases and 5,600 large translations. Python integer and Fraction allocation +is a managed-runtime deviation from static allocation. The largest retained +set has at most 6,561 image pairs; large tests use integers of at most 4,120 bits +and stream each case. The eight semantic checks and six rejected calls are +fixed. The verifier-owned indirect targets are the two explicit forward/inverse +functions in the invalid-input checks. Warning-strict normal and optimized +checks supply the available diagnostics without changing shared tooling. + +## Open next questions + +1. Can a phase actually required by a rounded supplier use this exact residue + analysis to reduce its complete precision allocation? First bind one literal + phase and its allowed outward headroom. An actual selected caller, bounded + integer storage and the physical quotient/return tariff are missing here. +2. Can a reversible rounding program outside these four fixed tie pairs attain + a smaller all-grid error for the same phase? First formulate a finite residue + matching problem with an explicit inverse. No optimality beyond the stated + four-program family is proved. + +The structured relevance, first steps and blockers are in [TASK.json](TASK.json). diff --git a/research/reversible-phase-tie-optimum/SOURCES.json b/research/reversible-phase-tie-optimum/SOURCES.json new file mode 100644 index 0000000000..56f4d08279 --- /dev/null +++ b/research/reversible-phase-tie-optimum/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "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/reversible-phase-disk-obstruction/README.md", + "usage": "provenance", + "git_blob": "7bcebabca764db24c69f975b28e3e47b3842764a", + "sha256": "5ffba7f923a3b761b41a2319e4e7038c997f86f47c44734a3f63a59d1bf89581" + }, + { + "path": "research/reversible-phase-disk-obstruction/model.py", + "usage": "provenance", + "git_blob": "9d1625623b556123d25e97eeb56609f442fd8ffb", + "sha256": "44b94b841fd727f1570f337950557aadb089875f4aed0085abdbdc73467c599e" + } + ] +} diff --git a/research/reversible-phase-tie-optimum/TASK.json b/research/reversible-phase-tie-optimum/TASK.json new file mode 100644 index 0000000000..f6641dea54 --- /dev/null +++ b/research/reversible-phase-tie-optimum/TASK.json @@ -0,0 +1,106 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Sharp all-grid squared error and exact inverse for four fixed nearest-rounding tie pairs implementing the rational phase (3+4i)/5.", + "scope_change_reason": "The card asks for an actual selected caller. This is a generic precision_tape side result changing one tie rule in PR2589's reversible lifting control; no selected caller assumption is discharged.", + "bottleneck_link": "An exact reversible phase with a smaller local error constant may reduce a future caller precision budget, but physical costs and an actual selected phase remain unbound.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified error-constant improvement inside the four fixed tie pairs; package without pursuing other phases or algorithms.", + "outcome": "completed", + "evidence": "PROOF.md gives the all-grid periodicity reduction, complete residual table, inverse, sharp witnesses and radial corollary. verify.py checks all 200 residues, 26244 signed-grid cases, 5600 large translations and controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can an actual rounded supplier phase use the residue analysis to reduce its complete precision allocation?", + "why_it_matters": "A generic local error gain affects precision_tape only after binding a real phase and full caller budget.", + "first_step": "Bind one literal phase, arithmetic grid and permitted outward headroom in an emitted caller.", + "blocked_by": "No actual selected phase, integer-width bound or physical quotient/return tariff is supplied." + }, + { + "question": "Can a reversible program outside the four fixed tie pairs improve the same phase's all-grid error?", + "why_it_matters": "The 4/5 optimum is scoped to a small program family.", + "first_step": "Formulate a finite residue matching problem with an explicit exact inverse.", + "blocked_by": "Input-dependent policies and other factorizations are not covered by this proof." + } + ], + "claim_type": "scoped proof with exact finite corroboration", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19299721", + "source_question": { + "source": "original", + "author": "original", + "context_pr": 2589, + "context_author": "ywz65", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2589", + "question_origin": "The tie-optimization question is originally posed here; PR2589 supplies the concrete lifting example and changed-interface motivation." + }, + "playbook": "Autonomous local run", + "upstream_checkpoint": { + "commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "priority_revision": 8, + "checked_utc": "2026-10-30T18:21:04Z", + "selected_kappa": "781451/250000000" + } +} diff --git a/research/reversible-phase-tie-optimum/VERIFY.json b/research/reversible-phase-tie-optimum/VERIFY.json new file mode 100644 index 0000000000..c5187fd71b --- /dev/null +++ b/research/reversible-phase-tie-optimum/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All-grid residue certificate, exact two-sided inverse, large signed translations, sharp radial family and semantic rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Identical complete verification with assertions disabled." + } + ] +} diff --git a/research/reversible-phase-tie-optimum/verify.py b/research/reversible-phase-tie-optimum/verify.py new file mode 100644 index 0000000000..c1af7a99b4 --- /dev/null +++ b/research/reversible-phase-tie-optimum/verify.py @@ -0,0 +1,212 @@ +#!/usr/bin/env python3 +"""Exact residue certificate. Produced by Nick Petalas. Apache-2.0.""" +import argparse +from collections import Counter +from fractions import Fraction +import hashlib +from itertools import product +import json +from pathlib import Path +import platform +import sys + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def forward(point, first=1, last=0): + """0 means downward half ties, 1 upward half ties.""" + need(first in (0, 1) and last in (0, 1), "invalid tie rule") + x, y = point + u = x - (y + first) // 2 + v = y + (8 * u + 5) // 10 + return u - (v + last) // 2, v + + +def inverse(point, first=1, last=0): + need(first in (0, 1) and last in (0, 1), "invalid tie rule") + w, v = point + u = w + (v + last) // 2 + y = v - (8 * u + 5) // 10 + return u + (y + first) // 2, y + + +def residual(point, image, sign=1): + x, y = point + w, v = image + return 5 * w - 3 * x + 4 * sign * y, 5 * v - 4 * sign * x - 3 * y + + +def norm2(point): + x, y = point + return x * x + y * y + + +def reference_nearest(value, tie): + """Separate Fraction/divmod oracle, including negative half integers.""" + low, remainder = divmod(value.numerator, value.denominator) + twice = 2 * remainder + if twice < value.denominator: + return low + if twice > value.denominator: + return low + 1 + return low + tie + + +def reference(point, first, last): + x, y = point + x -= reference_nearest(Fraction(y, 2), first) + y += reference_nearest(Fraction(4 * x, 5), 0) + x -= reference_nearest(Fraction(y, 2), last) + return x, y + + +def residue_certificate(): + results = [] + for first, last in product(range(2), repeat=2): + counts = Counter() + witness = None + maximum = -1 + for point in product(range(5), range(10)): + image = forward(point, first, last) + need(image == reference(point, first, last), "rational oracle") + error = residual(point, image) + counts[error] += 1 + if norm2(error) > maximum: + maximum, witness = norm2(error), [list(point), list(image)] + for step, output_step in (((5, 0), (3, 4)), ((0, 10), (-8, 6))): + translated = tuple(a + b for a, b in zip(point, step)) + expected = tuple(a + b for a, b in zip(image, output_step)) + need(forward(translated, first, last) == expected, "period generator") + need(maximum == (25 if first == last else 20), "sharp fixed-tie maximum") + need(sum(counts.values()) == 50, "complete fundamental rectangle") + results.append({"ties": [first, last], "max_error_squared_times_25": maximum, + "witness": witness, + "residual_counts": [[list(k), v] for k, v in sorted(counts.items())]}) + return results + + +def check_grid(): + cases = 0 + for first, last in product(range(2), repeat=2): + images = set() + limit = 25 if first == last else 20 + for point in product(range(-40, 41), repeat=2): + image = forward(point, first, last) + preimage = inverse(point, first, last) + need(inverse(image, first, last) == point, "left inverse") + need(forward(preimage, first, last) == point, "right inverse") + need(norm2(residual(point, image)) <= limit, "forward error") + need(norm2(residual(point, preimage, -1)) <= limit, "inverse error") + images.add(image) + cases += 1 + need(len(images) == 81 * 81, "finite injection") + return cases + + +def check_translates(): + cases = 0 + for first, last in product(range(2), repeat=2): + for bits in (1, 4, 16, 64, 256, 1024, 4096): + for sx, sy in product((-1, 1), repeat=2): + a, b = sx * (1 << bits), sy * ((1 << bits) + 1) + shift = (5 * a, 10 * b) + out_shift = (3 * a - 8 * b, 4 * a + 6 * b) + for point in product(range(5), range(10)): + translated = tuple(x + y for x, y in zip(point, shift)) + image = forward(translated, first, last) + expected = tuple(x + y for x, y in + zip(forward(point, first, last), out_shift)) + need(image == expected, "large signed translation") + need(image == reference(translated, first, last), "large rational oracle") + need(inverse(image, first, last) == translated, "large exact return") + cases += 1 + return cases + + +def check_radial_family(): + cases = 0 + for n in (1, 2, 4, 8, 16, 256, 65536, 1 << 128): + point = (-5 * n, 3 - 10 * n) + image = forward(point) + need(image == (5 * n - 2, 1 - 10 * n), "radial equality family") + need(residual(point, image) == (2, -4), "constant sharp residual") + need(norm2(point) == 125 * n * n - 60 * n + 9, "input radius polynomial") + need(norm2(image) - norm2(point) == 20 * n - 4, "outward radius polynomial") + cases += 1 + return cases + + +def check_controls(): + point = (0, 3) + image = forward(point) + need(image == (-2, 1), "sharp mixed-tie witness") + controls = { + "smaller_squared_constant_19_over_25": norm2(residual(point, image)) > 19, + "equal_upward_ties_at_4_over_5": norm2(residual(point, forward(point, 1, 1))) > 20, + "equal_downward_ties_at_4_over_5": norm2(residual((0, 5), forward((0, 5), 0, 0))) > 20, + "closed_disk_return": norm2(forward((-5, -7))) > norm2((-5, -7)), + "clipping_keeps_inverse": inverse((0, 0)) != (-5, -7), + "rounding_ties_does_not_matter": forward(point, 1, 1) != image, + } + w, v = image + u = w + (v + 1) // 2 + y = v - (8 * u + 5) // 10 + wrong_inverse = (u + (y + 1) // 2, y) + controls["inverse_uses_other_last_tie"] = wrong_inverse != point + point = (-3, -3) + u = point[0] - int(Fraction(point[1], 2)) + v = point[1] + (8 * u + 5) // 10 + wrong_forward = (u - int(Fraction(v, 2)), v) + controls["truncate_negative_halves"] = wrong_forward != forward(point) + for name, detected in controls.items(): + need(detected, "undetected semantic mutant: " + name) + for first, last in ((-1, 0), (0, 2), (3, 3)): + for operation in (forward, inverse): + try: + operation((0, 0), first, last) + except ValueError: + continue + raise ValueError("invalid tie rule accepted") + return sorted(controls) + + +def run(): + table = residue_certificate() + grid_cases = check_grid() + translation_cases = check_translates() + radial_cases = check_radial_family() + controls = check_controls() + return {"status": "PASS_REVERSIBLE_PHASE_TIE_OPTIMUM", + "claim_type": "scoped proof with exact finite corroboration", + "phase": ["3/5", "4/5"], "sharp_squared_error_over_grid_squared": "4/5", + "optimal_fixed_tie_pairs": [[0, 1], [1, 0]], + "residue_cases": 200, "residue_table": table, + "grid_cases": grid_cases, "large_translation_cases": translation_cases, + "radial_family_cases": radial_cases, "semantic_controls": controls, + "invalid_tie_rejections": 6, + "limits": "Four fixed tie pairs only; outward slack permitted; no physical caller or kappa claim."} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, help="exclusively write a generated hash-bound receipt") + args = parser.parse_args() + result = run() + here = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + receipt = {"result": result, + "package_sha256": {name: hashlib.sha256((here / name).read_bytes()).hexdigest() + for name in names}, + "environment": {"python": sys.version, "platform": platform.platform()}} + serialized = json.dumps(receipt, indent=2, sort_keys=True) + "\n" + if args.output is not None: + with args.output.open("x", encoding="utf-8") as target: + need(target.write(serialized) == len(serialized), "partial receipt write") + print(serialized, end="") + + +if __name__ == "__main__": + main()