Prove the sharp rounded dyadic connector carry (no κ)

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.

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.

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"
+    }
+  ]
+}

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"
+  }
+}