Skip to content

Sharpen reversible phase squared error from 1 to 4/5 (no κ) #6304

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Mister-Meeseeks merged 1 commit into from
Oct 31, 2026
Merged

Sharpen reversible phase squared error from 1 to 4/5 (no κ) #6304

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
148 changes: 148 additions & 0 deletions research/reversible-phase-tie-optimum/PROOF.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.
102 changes: 102 additions & 0 deletions research/reversible-phase-tie-optimum/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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).
30 changes: 30 additions & 0 deletions research/reversible-phase-tie-optimum/SOURCES.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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"
}
]
}
106 changes: 106 additions & 0 deletions research/reversible-phase-tie-optimum/TASK.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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"
}
}
Loading