From dafa58003b20ad72b6300410a2656f7329679562 Mon Sep 17 00:00:00 2001 From: Aaron Wang Date: Wed, 14 Oct 2026 07:42:15 -0400 Subject: [PATCH 1/2] Add dirty-host gauge binding receipt for hosted pending-factor credit Aaron Wang, with help from opencode. Scoped interface receipt answering an664's handoff (discussions/1166#discussioncomment-18916098) and PR 1664's open next questions 1-2: exact entry/exit gauges for the idle-axis hosted residual move and a per-cut credit allocation showing credit <= H_end for restored hosts, verified on 156 complete toy regions with exact rational arithmetic and four failure controls. No kappa claim; scope changed from the drawn persistent-boundary object (covered by concurrent PR 1739). --- .../README.md | 139 +++++++ .../SOURCES.json | 24 ++ .../TASK.json | 72 ++++ .../VERIFY.json | 21 + .../verify.py | 362 ++++++++++++++++++ 5 files changed, 618 insertions(+) create mode 100644 research/dirty-host-gauge-binding-seedea2e/README.md create mode 100644 research/dirty-host-gauge-binding-seedea2e/SOURCES.json create mode 100644 research/dirty-host-gauge-binding-seedea2e/TASK.json create mode 100644 research/dirty-host-gauge-binding-seedea2e/VERIFY.json create mode 100644 research/dirty-host-gauge-binding-seedea2e/verify.py diff --git a/research/dirty-host-gauge-binding-seedea2e/README.md b/research/dirty-host-gauge-binding-seedea2e/README.md new file mode 100644 index 0000000000..75a37eefce --- /dev/null +++ b/research/dirty-host-gauge-binding-seedea2e/README.md @@ -0,0 +1,139 @@ +# Dirty-host gauge binding: what a hosted pending factor may claim credit for + +No new bound and no kappa claim. This package is an interface receipt answering +the open request in the [handoffs thread](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18916098) +and PR https://github.com/CrocSwap/integer-mult-bounds/pull/1664's open next +questions 1-2: bind a hosted residual's claimed credit to exact host +entry/exit gauges and to the history-span endpoint term `H_end`. + +## Scope and evidence + +Original card: `persistent-boundary`, **scope changed** (see +[TASK.json](TASK.json)). The drawn object (consecutive dirty-connector calls) is +covered by open concurrent PR +https://github.com/CrocSwap/integer-mult-bounds/pull/1739 and the adjacent-call +centre-fanout claim in +https://github.com/CrocSwap/integer-mult-bounds/discussions/1516 (posted +2026-10-14T11:11Z); this package instead keeps the card's method-2 shape — a +lower bound on the compulsory transitions of one proposed typed interface — and +applies it to the idle-axis hosted-residual interface +([research/idle-axis-hosting/PROOF.md](../idle-axis-hosting/PROOF.md)) in the +scalar common-frame transport model of PR 1664's PROOF.md sections 4-5. + +Concretely, `verify.py` implements PR 1664's cut lemma `(C-down)`/`(C-up)` and a +crossing feasibility check exactly (rational arithmetic; entry rows are an +identity basis, so row equality covers arbitrary dirty inputs by linearity), and +audits one hosted residual: one invocation residual factor of width `w` hosted +on a block `S'` of an idle family's pending set `S`, moved from the invocation +to the idle child's advance. + +**Finding 1 (operator gauges, exact).** The hosting move leaves the complete +operator unchanged exactly when the moved factor is the advance's own factor on +`S'`, no non-commuting touch of the host occurs strictly between the residual +application and the advance, and hosted blocks are disjoint (order preserved). +Each dropped gauge has a smallest counterexample as composed linear maps +(3x3 shears): an escaping block gives a different endpoint, an out-of-window +touch that does not commute with the moved factor breaks the composition, and +overlapping blocks are order-dependent. + +**Finding 2 (credit binding on the smallest complete instances).** With hosts +restored and the clean scatter `Y' = Y + S X` demanded at height 0 (PR 1664's +section 5.1 contract), the per-cut demand identity + +`sum_j need_j = q*rank(S) + sum_alpha |a_alpha - b_alpha| = q*rank(S) + H_end` + +holds exactly on **all 156 enumerated tiny regions** (every binary `t x m` +scatter matrix with `m,t <= 2`, `w <= 2`, and host motions `(a,b)` in +`{(1,0),(2,0),(2,1)}`). The smallest double-duty borrow — one host row `d` +descending `1 -> 0` carrying `d + x` while both `y' = y + x` and a restored `d` +are demanded — is refuted at cut 1 by exactly one direction, both by the count +(`D_j = 1 < 2`) and by span feasibility. So a hosted pending factor's +creditable mass is exactly its host's endpoint displacement `H_end`, and never +more: the scatter term `q*rank(S)` cannot be hosted away while hosts are +restored, and each useful pending factor is counted once. This instantiates PR +1664's "show that the claimed hosting credit is `H_end`" affirmatively for the +toy class, with the double-credit loop as the smallest refuted instance. + +**Finding 3 (the only free route, and it is a contract change).** At zero extra +mass a host crossing may deliver a hosted direction **only** if the host's own +prescribed endpoint absorbs that direction and no separate target or restoration +demand survives. Dropping PR 1664's clean-scatter and restoration obligations is +exactly such an endpoint-contract change; it must be charged against the data +endpoint (a coordinate cannot be counted unpaid while left unadvanced there). +This is the precise accounting interface between "hosting credit" and "unpaid +coordinate", the quantity the coverage-law line (discussion +https://github.com/CrocSwap/integer-mult-bounds/discussions/1587) manipulates. + +A pre-positioned copy of the host dirt below the cut earns no credit (the +restoration direction is already in `W_j^0`), instantiated as a machine check of +PR 1664's section 7 warning. + +## What this does not establish + +- No bank-tile physics: the replaced bank write/clear mass is not modeled; the + claim "one bank tile of width `w` eliminated" is compared only through the + credit shape `w*|a-b|` per host row. +- No wrappers, spectators or gauge charts: PR 1664's section 6 warning that + "useful width" is not generally endpoint displacement (non-nested frames such + as `span(e_1)` to `span(e_2)`) remains open here. +- No physical or production admission, no selected-word application, no + selected rank-8/64 calculation, no kappa claim, no supplier/profile change. + The whole-construction budget and the `a < D/E` diagnostic are not applicable + to this interface receipt. +- Finite checks on toy regions do not certify the universal written statements + of PR 1664 or idle-axis hosting. + +## Reproduce + +From the repository root (stdlib only): + +```sh +python3.12 -B research/dirty-host-gauge-binding-seedea2e/verify.py +python3.12 scripts/research_package.py --package research/dirty-host-gauge-binding-seedea2e --check-only +python3.12 scripts/research_package.py --package research/dirty-host-gauge-binding-seedea2e +``` + +Expected first and last lines: `PASS_DIRTY_HOST_GAUGE_BINDING_BEGIN` and +`PASS_DIRTY_HOST_GAUGE_BINDING`, with the smallest falsifying instances run +first. Source pins are in [SOURCES.json](SOURCES.json); replay commands are in +[VERIFY.json](VERIFY.json). + +## Open next questions + +Structured versions are in [TASK.json](TASK.json). + +1. **Bind the gauges on the pinned selected replay.** Check every hosted slot of + the selected 480-helper word for `S' subset S`, in-window and pairwise + disjoint blocks, then re-derive its credited residual count against + `H_end`. It matters because it turns this toy receipt into a statement about + the construction. First step: parse the hosted slots in + `research/community-frontier1094-audit/selected-replay.tar.gz`'s + `LOCAL-PROGRAMS.json.gz` and the per-stream pending sets. Blocked by: the + slot/pending-set data definitions and separately claimed centre-phase work in + https://github.com/CrocSwap/integer-mult-bounds/discussions/1516. +2. **Non-nested frame gauges.** Replace `|a-b|` by the supplied frame metric + `d(L_A,L_B) = dim A + dim B - 2 dim(A meet B)` and decide the useful-width + versus endpoint-displacement mismatch PR 1664 section 6 records. First step: + the smallest toy with `A = span(e_1)`, `B = span(e_2)` (transition rank 2, + equal heights). Blocked by: a concrete inherited wrapper/chart convention. +3. **Can a legal data endpoint actually absorb a hosted direction?** Finding 3 + says absorption is the only free route; whether any endpoint contract admits + it without leaving a coordinate unadvanced is the coverage question. First + step: test the plane-port endpoint's two unpaid coordinates (discussion + https://github.com/CrocSwap/integer-mult-bounds/discussions/1587) for exactly + this absorption. Blocked by: the open plane-port decoder contract. + +## Credit + +Prepared by **Aaron Wang**, with help from opencode. Substantial AI assistance is +disclosed in [TASK.json](TASK.json). New work is Apache-2.0. + +Predecessors (read, not modified): Andrey Mas / an664's PR +https://github.com/CrocSwap/integer-mult-bounds/pull/1664 +(`research/dirty-host-cutrank-audit/`, including its GPT-6 Pro review) and the +handoff https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18916098; +ctoh's dirty-host implication and branching-tree bound in +https://github.com/CrocSwap/integer-mult-bounds/discussions/1516; DaysSky's +`research/idle-axis-hosting`; and the lineage recorded in PR 1664's SOURCES.json +(icekylinx, DreamingOfClouds, jeremykothe2, rohanarun, Dennis / +@antunishdPursuit). diff --git a/research/dirty-host-gauge-binding-seedea2e/SOURCES.json b/research/dirty-host-gauge-binding-seedea2e/SOURCES.json new file mode 100644 index 0000000000..511e8629f2 --- /dev/null +++ b/research/dirty-host-gauge-binding-seedea2e/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/idle-axis-hosting/PROOF.md", + "usage": "input", + "git_blob": "4468a00349b4f68dce103e785a8392099435e1d6", + "sha256": "cfe34bf0b64259661312dae22c3a23adc5bf6f6326951eee5c1488ccfc347542" + } + ] +} diff --git a/research/dirty-host-gauge-binding-seedea2e/TASK.json b/research/dirty-host-gauge-binding-seedea2e/TASK.json new file mode 100644 index 0000000000..8a705b4fd5 --- /dev/null +++ b/research/dirty-host-gauge-binding-seedea2e/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "persistent-boundary", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "original_card": { + "id": "persistent-boundary", + "question": "Can a specified pair of consecutive calls eliminate a restoration that the next call reconstructs?", + "starting_points": [ + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Write typed entry/exit contracts and a contracting multitype recurrence.", + "Derive a lower bound for the compulsory transitions of one proposed typed interface." + ], + "acceptance_gate": "Show actual eliminated work and legal composition; changing a scalar recurrence into a matrix is insufficient.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Find a concrete consecutive-call boundary in the selected review and list its entry/exit obligations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Specify two call types and one operation actually removed by composition; derive the normalized recurrence.", + "bottleneck_link": "Eliminating compulsory boundary work can lower recursive cost beyond packing gains.", + "allowed_variations": [ + "A two-type pilot or one explicit deferred restoration." + ], + "scope_change_triggers": [ + "Rewriting the old scalar recurrence as a matrix without eliminating work." + ], + "overlap_terms": [ + "persistent boundary", + "deferred restoration", + "multitype" + ] + }, + "scope_status": "changed", + "actual_scope": "Credit binding for one idle-axis hosted residual: exact entry/exit gauges for the hosting move (S' inside the pending set S, no non-commuting intervening touch, disjoint hosted blocks, host endpoint prescribed by the advance) and a per-cut credit allocation for the claimed hosting credit against the history-span endpoint term H_end, audited on the smallest complete instances in the scalar common-frame transport model of PR 1664 (pull/1664) PROOF.md sections 4-5.", + "scope_change_reason": "The drawn persistent-boundary object (consecutive dirty-connector calls) is covered by open concurrent PR https://github.com/CrocSwap/integer-mult-bounds/pull/1739 (1337isnot1337) and the adjacent-call centre-fanout claim posted 2026-10-14T11:11Z in https://github.com/CrocSwap/integer-mult-bounds/discussions/1516. This task instead takes the explicit open request https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18916098 (an664) and PR 1664's open next questions 1-2, keeping the card's method-2 shape: a lower bound on the compulsory transitions of one proposed typed interface (the idle-axis hosting window contract).", + "bottleneck_link": "Hosting credit is the accounting that lets the coverage law count work as eliminated boundary work; without a gauge binding, a claimed hosting credit can exceed what the host's compulsory displacement pays. The receipt pins credit <= H_end for restored hosts and isolates the one endpoint-contract change (absorption) that could credit more, which is the quantity the coverage-law/unpaid-coordinate line changes.", + "budget_minutes": 60, + "stop_rule": "One bounded interface receipt: smallest falsifying instance first, one exhaustive toy family (156 regions), four gauge controls, then stop. No supplier replay, no kappa target.", + "outcome": "completed", + "evidence": "python3.12 -B research/dirty-host-gauge-binding-seedea2e/verify.py prints PASS_DIRTY_HOST_GAUGE_BINDING: the double-duty borrow and the absorbed-endpoint-with-separate-target are refuted at cut 1 by exactly one direction (count and span feasibility); full absorption alone passes and is flagged as a contract change; three dropped-gauge counterexamples for the operator identity; the PR1664 section 5.2 arithmetic reproduced with an M<=6 mutant refuted; pre-positioned dirt earns no credit; and all 156 enumerated restored-host regions satisfy (C-down) and the exact identity sum_j need_j = q*rank(S) + H_end.", + "author": "Aaron Wang (with help from opencode)", + "ai_assistance": "Substantial AI assistance: this session was run by an opencode coding agent (model not cited per donor instruction); the verifier, proof notes and package text were drafted with that assistance and checked by exact replay.", + "open_questions": [ + { + "question": "Bind the gauges on the pinned selected replay: check every hosted slot of the selected 480-helper word for S' subset S, in-window and pairwise disjoint blocks, and re-derive its credited residual count against H_end.", + "why_it_matters": "It turns this toy receipt into a statement about the construction's actual hosting credit.", + "first_step": "Parse the hosted slots in research/community-frontier1094-audit/selected-replay.tar.gz (LOCAL-PROGRAMS.json.gz) and the per-stream pending sets; recompute windows exactly as research/idle-axis-hosting/audit.py does.", + "blocked_by": "Slot/pending-set data definitions in the replay; the centre-phase scatter work is separately claimed in https://github.com/CrocSwap/integer-mult-bounds/discussions/1516." + }, + { + "question": "Non-nested frame gauges: replace |a-b| by the frame metric d(L_A,L_B) and decide the useful-width versus endpoint-displacement mismatch PR 1664 section 6 records.", + "why_it_matters": "H_end uses height displacement; the mismatch is the open accounting-interface warning for non-nested frames.", + "first_step": "Smallest toy with A = span(e_1), B = span(e_2) (transition rank 2, equal heights), computing both credit conventions.", + "blocked_by": "A concrete inherited wrapper/chart convention fixing the frame metric on the actual streams." + }, + { + "question": "Can a legal data endpoint absorb a hosted direction (Finding 3's only free route) without leaving a coordinate unadvanced in the data endpoint?", + "why_it_matters": "Absorption is the only way hosting credit exceeds H_end; whether any contract admits it is exactly the coverage-law question.", + "first_step": "Test the plane-port endpoint's two unpaid coordinates (https://github.com/CrocSwap/integer-mult-bounds/discussions/1587) for this absorption.", + "blocked_by": "The open plane-port decoder contract (PR https://github.com/CrocSwap/integer-mult-bounds/pull/1825 and its follow-ups)." + } + ] +} diff --git a/research/dirty-host-gauge-binding-seedea2e/VERIFY.json b/research/dirty-host-gauge-binding-seedea2e/VERIFY.json new file mode 100644 index 0000000000..62ddad400a --- /dev/null +++ b/research/dirty-host-gauge-binding-seedea2e/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/idle-axis-hosting/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "PASS_DIRTY_HOST_GAUGE_BINDING: smallest falsifying instances first (double-duty borrow and absorbed-endpoint-with-separate-target refuted at cut 1 by count and span feasibility; full absorption flagged as an endpoint-contract change), operator gauges with three dropped-gauge counterexamples, the PR1664 section 5.2 canonical arithmetic with an M<=6 mutant refuted, pre-positioned dirt earning no credit, and all 156 restored-host toy regions satisfying (C-down) and the exact identity sum_j need_j = q*rank(S) + H_end." + } + ] +} diff --git a/research/dirty-host-gauge-binding-seedea2e/verify.py b/research/dirty-host-gauge-binding-seedea2e/verify.py new file mode 100644 index 0000000000..230120842c --- /dev/null +++ b/research/dirty-host-gauge-binding-seedea2e/verify.py @@ -0,0 +1,362 @@ +#!/usr/bin/env python3 +"""Credit-binding checks for hosted dirty residuals in the scalar common-frame transport model. + +Model: PR 1664 (https://github.com/CrocSwap/integer-mult-bounds/pull/1664) +PROOF.md sections 4-5, "scalar common-frame transport": registers hold formal +coefficient rows over Q; a transport of one register frame A -> B is charged +|nu(A)-nu(B)|; add/scale/copy at one common frame are free. The cut lemma is + + D_j >= dim(W_j^0 + span Q_j) - dim W_j^0 (C-down) + +with the symmetric high-side statement, and M >= sum_j (D_j + U_j). The +conditional dirty-host corollary is M >= H_end + q*rank_K(S) (H) + +for restored hosts and clean scatter Y' = Y + S X at height 0. + +This script implements (C-down) and the crossing feasibility condition exactly, +and audits the *credit binding* of the idle-axis hosted-residual mechanism +(research/idle-axis-hosting/PROOF.md): which entry/exit gauges make a hosting +move operator-identical, and how much mass a hosted pending factor may claim +credit for. All checks are exact rational arithmetic; entry rows are +identity-basis rows (arbitrary dirty content), so row equality covers every +dirty input by linearity. + +Aaron Wang, with help from opencode. Apache-2.0. +""" + +from fractions import Fraction +import sys + +# ---------------------------------------------------------------- exact linear algebra + + +def rank(rows): + m = [[Fraction(x) for x in r] for r in rows] + if not m: + return 0 + n = len(m[0]) + row = 0 + for col in range(n): + piv = None + for i in range(row, len(m)): + if m[i][col] != 0: + piv = i + break + if piv is None: + continue + m[row], m[piv] = m[piv], m[row] + inv = Fraction(1) / m[row][col] + m[row] = [x * inv for x in m[row]] + for i in range(len(m)): + if i != row and m[i][col] != 0: + f = m[i][col] + m[i] = [a - f * b for a, b in zip(m[i], m[row])] + row += 1 + if row == len(m): + break + return row + + +def mod_rank(base, extra): + return rank(base + extra) - rank(base) + + +def contained(base, rows): + """True iff every row of `rows` lies in span(base).""" + return mod_rank(base, rows) == 0 + + +def vec(n, *ones): + v = [0] * n + for i in ones: + v[i] = 1 + return v + + +def matmul(a, b): + return [[sum(a[i][k] * b[k][j] for k in range(len(b))) for j in range(len(b[0]))] + for i in range(len(a))] + + +def eye(n): + return [[1 if i == j else 0 for j in range(n)] for i in range(n)] + + +def shear(n, dst, src): + m = eye(n) + m[dst][src] = 1 + return m + + +# ---------------------------------------------------------------- region + cut engine + + +class Region: + """A finite charged region. + + entry: list of (name, height, row) at the region entry (row = content as a + coefficient row over the formal inputs; arbitrary dirty inputs are + covered by taking entry rows as a basis). + moves: list of (name, from_height, to_height, row_at_move): one-register + transports; paid mass |delta| each; the row is what actually crosses. + exits: list of (name, height, row) demanded at the region exit. + """ + + def __init__(self, entry, moves, exits): + self.entry = entry + self.moves = moves + self.exits = exits + + def paid_mass(self): + return sum(abs(t - f) for _, f, t, _ in self.moves) + + def crossings(self, j): + """(D_j, U_j, rows_down, rows_up) at cut j.""" + d = u = 0 + down, up = [], [] + for _, f, t, r in self.moves: + if f >= j > t: + d += 1 + down.append(r) + elif t >= j > f: + u += 1 + up.append(r) + return d, u, down, up + + def cut_report(self): + """For every cut j: (need_low, D_j, rows_down, need_high, U_j, rows_up, + W_low, W_high).""" + heights = {h for _, h, _ in self.entry} | {t for _, _, t, _ in self.moves} \ + | {h for _, h, _ in self.exits} | {f for _, f, _, _ in self.moves} + lo, hi = min(heights), max(heights) + out = {} + for j in range(lo, hi + 2): + w_low = [r for _, h, r in self.entry if h < j] + w_high = [r for _, h, r in self.entry if h >= j] + q_low = [r for _, h, r in self.exits if h < j] + q_high = [r for _, h, r in self.exits if h >= j] + d, u, down, up = self.crossings(j) + out[j] = (mod_rank(w_low, q_low), d, down, + mod_rank(w_high, q_high), u, up, w_low, w_high) + return out + + def obstructions(self): + """Violations of (C-down)/(C-up) and of crossing feasibility.""" + bad = [] + for j, (nl, d, down, nh, u, up, w_low, w_high) in sorted(self.cut_report().items()): + if d < nl: + bad.append(f"cut {j}: D_j={d} < demanded quotient rank {nl}") + if u < nh: + bad.append(f"cut {j}: U_j={u} < demanded quotient rank {nh}") + q_low = [r for _, h, r in self.exits if h < j] + q_high = [r for _, h, r in self.exits if h >= j] + if not contained(w_low + down, q_low): + bad.append(f"cut {j}: low-side exits not in span(W_j^0 + crossed rows)") + if not contained(w_high + up, q_high): + bad.append(f"cut {j}: high-side exits not in span(W_j^0 + crossed rows)") + return bad + + +def report(name, ok, detail): + print(("PASS" if ok else "FAIL"), name, "-", detail) + if not ok: + raise SystemExit(f"CHECK FAILED: {name}: {detail}") + + +# ---------------------------------------------------------------- checks + + +def check_smallest_falsifier(): + """Smallest double-duty borrow: one host row asked to carry both the centre + direction and its own restoration. m=t=w=1, q=1, r=1, host 1->0. + Inputs x (centre total), d (host dirt), y (target old value). + """ + n = 3 # x, d, y + x, d, y = vec(3, 0), vec(3, 1), vec(3, 2) + entry = [("x", 1, x), ("d", 1, d), ("y", 0, y)] + # hosted schedule: d += x at height 1 (free add), one descent 1->0 + crossed = [1, 1, 0] # the row d+x crosses + exits = [("y", 0, [1, 0, 1]), ("d", 0, [0, 1, 0])] # y'=y+x; host restored + hosted = Region(entry, [("d", 1, 0, crossed)], exits) + bad = hosted.obstructions() + report("double-duty-borrow-refuted", bool(bad), + f"m=t=w=1: one crossing carries d+x and cannot also produce both " + f"y'=y+x and the restored d; {bad}") + + # Absorbed endpoint, separate target demand survives: the host exits at d+x + # (its prescribed advance), but the construction's data endpoint still + # demands y'=y+x. Refuted the same way: d+x alone cannot give y+x. + exits_abs = [("y", 0, [1, 0, 1]), ("d", 0, [1, 1, 0])] + hosted_abs = Region(entry, [("d", 1, 0, crossed)], exits_abs) + bad = hosted_abs.obstructions() + report("absorbed-endpoint-with-target-refuted", bool(bad), + f"even when the host endpoint absorbs the direction, the separate " + f"target row y'=y+x still owes its own crossing: {bad}") + + # Full absorption: no separate target demand at all (the family's advance IS + # the delivery). Feasible with M=1, and (H) no longer applies because the + # clean-scatter and restoration obligations are absent from the contract. + exits_free = [("d", 0, [1, 1, 0])] + hosted_free = Region(entry, [("d", 1, 0, crossed)], exits_free) + bad = hosted_free.obstructions() + report("full-absorption-is-the-only-free-route", not bad, + "with the host endpoint absorbing the direction and no separate target " + "demand, M=1 passes (C-down); this drops the (H) scatter/restoration " + "obligations and is exactly the endpoint-contract change that must be " + "charged (see README)") + + +def check_operator_gauges(): + """The factor-move gauges as exact composed linear maps on d=3 coordinates. + The hosted version applies I_mu' (the advance off the hosted block) followed + by the moved factor; the gauges make that equal the original advance I_mu. + Controls: escape, overlap order dependence, out-of-window touch. + """ + d = 3 + moved = shear(d, 0, 2) # hosted pending factor on S'={0} + ip = shear(d, 1, 2) # I_mu' : the advance on S \ S', S={0,1} + imu = matmul(moved, ip) # the original advance, factored on S' then S\S' + # Convention: total = later o earlier. Original: moved at I1, then I_mu' + # at I_mu. Hosted: both applied at I_mu in the factor order that equals I_mu. + total_orig = matmul(ip, moved) + total_hosted = imu + report("gauge-move-identity", total_orig == total_hosted, + "the moved factor at I1 followed by I_mu' reproduces the advance exactly") + # escape: the moved factor is not the advance's factor on S' (block outside S) + escape = shear(d, 2, 1) + report("gauge-escape-refuted", matmul(ip, escape) != imu, + "a moved factor whose block escapes the pending set does not compose " + "to the advance: the endpoint differs") + # overlap: two moved factors on overlapping blocks do not commute + m1, m2 = shear(d, 0, 1), shear(d, 1, 0) + report("gauge-overlap-order-refuted", matmul(m1, m2) != matmul(m2, m1), + "overlapping hosted blocks are order-dependent: disjointness (count " + "each pending factor once) is required for an order-free composition") + # out-of-window touch: an intervening touch T between the residual write at + # I1 and the advance at I_mu; hosting moves the factor past T + T = shear(d, 2, 0) + total_orig_w = matmul(ip, matmul(T, moved)) + total_hosted_w = matmul(imu, T) + report("gauge-window-refuted", total_orig_w != total_hosted_w, + "an intervening touch that does not commute with the moved factor " + "breaks the composition: the window condition is required") + + +def check_engine_canonical(): + """The PR1664 section 5.2 arithmetic: two carriers, two restored hosts, + q=r=2, host rows 2->0. Baseline M = 8 = H_end(4) + q*r(4); a schedule + claiming the same obligations in M=6 is refuted. + """ + n = 6 # x1, x2, d1, d2, y1, y2 + entry = [("x1", 2, vec(6, 0)), ("x2", 2, vec(6, 1)), + ("d1", 2, vec(6, 2)), ("d2", 2, vec(6, 3)), + ("y1", 0, vec(6, 4)), ("y2", 0, vec(6, 5))] + exits = [("y1", 0, [1, 0, 0, 0, 1, 0]), ("y2", 0, [0, 1, 0, 0, 0, 1]), + ("d1", 0, vec(6, 2)), ("d2", 0, vec(6, 3))] + base = Region(entry, [("x1", 2, 0, vec(6, 0)), ("x2", 2, 0, vec(6, 1)), + ("d1", 2, 0, vec(6, 2)), ("d2", 2, 0, vec(6, 3))], exits) + bad = base.obstructions() + report("canonical-bound-baseline", not bad and base.paid_mass() == 8, + f"M=8 = H_end(4)+q*r(4) passes; obstructions: {bad}") + mutant = Region(entry, [("x1", 2, 0, vec(6, 0)), ("x2", 2, 0, vec(6, 1)), + ("d1", 2, 0, vec(6, 2))], exits) + bad = mutant.obstructions() + report("canonical-bound-mutant-refuted", bool(bad), + f"M<=6 mutant refuted: {bad}") + + +def check_prepositioned_dirt(): + """Pre-positioned dirt: the host's row was already copied below the cut at + entry, so its descent earns no credit and the x direction stays unpaid. + """ + n = 3 # x, d, y + entry = [("x", 1, vec(3, 0)), ("d", 1, vec(3, 1)), + ("d_copy", 0, vec(3, 1)), # pre-positioned copy of d below the cut + ("y", 0, vec(3, 2))] + exits = [("y", 0, [1, 0, 1]), ("d", 0, [0, 1, 0])] # y'=y+x, host restored + region = Region(entry, [("d", 1, 0, vec(3, 1))], exits) + cr = region.cut_report() + need1 = cr[1][0] + bad = region.obstructions() + report("prepositioned-dirt-no-credit", need1 == 1 and bool(bad), + f"cut 1 demand quotient rank is {need1} (the restoration direction is " + f"already in W_1^0 and earns no credit) and the unpaid x direction is " + f"refuted: {bad}") + + +def check_restored_host_exhaustive(): + """All tiny restored-host regions: m,t in {1,2}, w in {1,2}, + (a,b) in {(1,0),(2,0),(2,1)}, every binary t x m scatter S (26 cases). + + Verified per case: + (i) the baseline schedule (carriers a->0, hosts a->b) passes (C-down); + (ii) the exact per-cut demand identity + sum_j need_j = q*rank(S) + w*|a-b| (q = a), + i.e. with restored hosts the scatter term q*rank(S) survives every + hosting claim and the creditable mass never exceeds the host + displacement w*|a-b|. + """ + cases = 0 + for m in (1, 2): + for t in (1, 2): + for w in (1, 2): + for a, b in ((1, 0), (2, 0), (2, 1)): + for bits in range(1 << (t * m)): + S = [[(bits >> (i * m + j)) & 1 for j in range(m)] + for i in range(t)] + r = rank(S) + n = m + w + t # carriers, hosts, target old values + entry = [] + for i in range(m): + entry.append((f"x{i}", a, vec(n, i))) + for k in range(w): + entry.append((f"d{k}", a, vec(n, m + k))) + for i in range(t): + entry.append((f"y{i}", 0, vec(n, m + w + i))) + exits = [] + for i in range(t): + row = [0] * n + for j in range(m): + row[j] = S[i][j] + row[m + w + i] = 1 + exits.append((f"y{i}", 0, row)) + for k in range(w): + exits.append((f"d{k}", b, vec(n, m + k))) + moves = [(f"d{k}", a, b, vec(n, m + k)) for k in range(w)] + \ + [(f"x{i}", a, 0, vec(n, i)) for i in range(m)] + region = Region(entry, moves, exits) + bad = region.obstructions() + if bad: + report(f"restored-host-case-{cases}", False, + f"m={m} t={t} w={w} (a,b)=({a},{b}) S={S}: {bad}") + cr = region.cut_report() + demand = sum(nl for (nl, _d, _dn, _nh, _u, _up, _wl, _wh) + in cr.values()) + rhs = a * r + w * abs(a - b) + if demand != rhs: + report(f"demand-identity-{cases}", False, + f"per-cut demand {demand} != H_end + q*r = {rhs} " + f"(m={m} t={t} w={w} ({a},{b}) S={S})") + cases += 1 + report("restored-host-exhaustive", cases == 156, + f"{cases} complete tiny regions (all binary S, m,t<=2, w<=2) satisfy " + f"(C-down) and the exact per-cut demand identity " + f"sum_j need_j = H_end + q*rank(S): the scatter term cannot be hosted " + f"away while hosts are restored, and credit <= host displacement") + + +def main(): + print("PASS_DIRTY_HOST_GAUGE_BINDING_BEGIN") + print("--- smallest falsifying instance first ---") + check_smallest_falsifier() + print("--- operator gauges ---") + check_operator_gauges() + print("--- credit accounting ---") + check_engine_canonical() + check_prepositioned_dirt() + check_restored_host_exhaustive() + print("PASS_DIRTY_HOST_GAUGE_BINDING") + + +if __name__ == "__main__": + main() From 313dca90398797c44ff40f83bac772a1b4ab8c14 Mon Sep 17 00:00:00 2001 From: Aaron Wang Date: Wed, 14 Oct 2026 13:02:09 -0400 Subject: [PATCH 2/2] Repair Finding 1 gauge wording: sufficient hypotheses, not "exactly when" Aaron Wang, with help from opencode. Reviewer follow-up on https://github.com/CrocSwap/integer-mult-bounds/pull/1837 (comment https://github.com/CrocSwap/integer-mult-bounds/pull/1837#issuecomment-6173237648): Finding 1's operator-level "exactly when" was not established by the examples. Reproduced the reviewer's exact 3x3 counterexample over Q (R = I + E01, T = I + E12, T^{-1} = I - E12: both touches fail to commute with R, yet T^{-1} T R = R T^{-1} T = R) and added it as the regression control cancellation-equality-not-rejected in verify.py, which the now sufficient-only condition must not reject. README.md, TASK.json and VERIFY.json state the inherited interface conditions (own factor on S', no intervening host touch, disjoint hosted blocks) as sufficient legality hypotheses for operator equality; no necessity claim is made, and cancellation-based routes stay open. The tiny cut examples and the selected no-touch hosting rule are unchanged and remain valid. All package checks pass: PASS_DIRTY_HOST_GAUGE_BINDING, PASS_REGISTERED_RESEARCH_PACKAGE research/dirty-host-gauge-binding-seedea2e outcome=completed, 42 tests OK. --- .../README.md | 32 +++++++--- .../TASK.json | 4 +- .../VERIFY.json | 2 +- .../verify.py | 60 +++++++++++++++++-- 4 files changed, 81 insertions(+), 17 deletions(-) diff --git a/research/dirty-host-gauge-binding-seedea2e/README.md b/research/dirty-host-gauge-binding-seedea2e/README.md index 75a37eefce..d82e9d1e75 100644 --- a/research/dirty-host-gauge-binding-seedea2e/README.md +++ b/research/dirty-host-gauge-binding-seedea2e/README.md @@ -27,14 +27,26 @@ audits one hosted residual: one invocation residual factor of width `w` hosted on a block `S'` of an idle family's pending set `S`, moved from the invocation to the idle child's advance. -**Finding 1 (operator gauges, exact).** The hosting move leaves the complete -operator unchanged exactly when the moved factor is the advance's own factor on -`S'`, no non-commuting touch of the host occurs strictly between the residual -application and the advance, and hosted blocks are disjoint (order preserved). -Each dropped gauge has a smallest counterexample as composed linear maps -(3x3 shears): an escaping block gives a different endpoint, an out-of-window -touch that does not commute with the moved factor breaks the composition, and -overlapping blocks are order-dependent. +**Finding 1 (operator gauges, exact; sufficient hypotheses).** The hosting move +leaves the complete operator unchanged whenever the moved factor is the +advance's own factor on `S'`, no touch of the host occurs strictly between the +residual application and the advance (more generally, every such touch commutes +with the moved factor), and hosted blocks are disjoint (order preserved). These +are the inherited hosting interface's sufficient legality hypotheses, not a +necessary condition for operator equality, and no necessity claim is proved +here for any class. Exact 3x3 counterexample over Q, kept as the regression +control `cancellation-equality-not-rejected` in `verify.py`: `R = I + E01`, +`T = I + E12`, `T^{-1} = I - E12`. Both `T` and `T^{-1}` fail to commute with +`R`, yet moving `R` across the consecutive touches `T, T^{-1}` preserves the +complete operator, `T^{-1} T R = R T^{-1} T = R`. Cancellation routes like this +one are not closed by this receipt. Each dropped hypothesis still has a +smallest counterexample as composed linear maps (3x3 shears): an escaping block +gives a different endpoint, a single out-of-window touch that does not commute +with the moved factor breaks the composition, and the exhibited overlapping +blocks are order-dependent. Those controls show the hypotheses cannot simply be +deleted; they do not establish necessity. The tiny cut examples below +(including the 156 restored-host regions) and the selected no-touch hosting +rule remain valid as they stand. **Finding 2 (credit binding on the smallest complete instances).** With hosts restored and the clean scatter `Y' = Y + S X` demanded at height 0 (PR 1664's @@ -70,6 +82,10 @@ PR 1664's section 7 warning. ## What this does not establish +- Finding 1's operator-level hypotheses are sufficient only. A necessity claim + would have to be restricted to a stated class and proved there; any such + class must provably exclude cancellation examples such as the `T, T^{-1}` + control above, which this receipt deliberately leaves open. - No bank-tile physics: the replaced bank write/clear mass is not modeled; the claim "one bank tile of width `w` eliminated" is compared only through the credit shape `w*|a-b|` per host row. diff --git a/research/dirty-host-gauge-binding-seedea2e/TASK.json b/research/dirty-host-gauge-binding-seedea2e/TASK.json index 8a705b4fd5..db826ddb16 100644 --- a/research/dirty-host-gauge-binding-seedea2e/TASK.json +++ b/research/dirty-host-gauge-binding-seedea2e/TASK.json @@ -40,13 +40,13 @@ ] }, "scope_status": "changed", - "actual_scope": "Credit binding for one idle-axis hosted residual: exact entry/exit gauges for the hosting move (S' inside the pending set S, no non-commuting intervening touch, disjoint hosted blocks, host endpoint prescribed by the advance) and a per-cut credit allocation for the claimed hosting credit against the history-span endpoint term H_end, audited on the smallest complete instances in the scalar common-frame transport model of PR 1664 (pull/1664) PROOF.md sections 4-5.", + "actual_scope": "Credit binding for one idle-axis hosted residual: sufficient entry/exit gauges for the hosting move (S' inside the pending set S, no intervening touch of the host between the residual application and the advance, pairwise disjoint hosted blocks, host endpoint prescribed by the advance), stated as sufficient legality hypotheses of the inherited hosting interface rather than a necessary condition for operator equality (cancellation routes such as the consecutive touches T, T^{-1} past a moved factor R = I + E01 remain open), and a per-cut credit allocation for the claimed hosting credit against the history-span endpoint term H_end, audited on the smallest complete instances in the scalar common-frame transport model of PR 1664 (pull/1664) PROOF.md sections 4-5.", "scope_change_reason": "The drawn persistent-boundary object (consecutive dirty-connector calls) is covered by open concurrent PR https://github.com/CrocSwap/integer-mult-bounds/pull/1739 (1337isnot1337) and the adjacent-call centre-fanout claim posted 2026-10-14T11:11Z in https://github.com/CrocSwap/integer-mult-bounds/discussions/1516. This task instead takes the explicit open request https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18916098 (an664) and PR 1664's open next questions 1-2, keeping the card's method-2 shape: a lower bound on the compulsory transitions of one proposed typed interface (the idle-axis hosting window contract).", "bottleneck_link": "Hosting credit is the accounting that lets the coverage law count work as eliminated boundary work; without a gauge binding, a claimed hosting credit can exceed what the host's compulsory displacement pays. The receipt pins credit <= H_end for restored hosts and isolates the one endpoint-contract change (absorption) that could credit more, which is the quantity the coverage-law/unpaid-coordinate line changes.", "budget_minutes": 60, "stop_rule": "One bounded interface receipt: smallest falsifying instance first, one exhaustive toy family (156 regions), four gauge controls, then stop. No supplier replay, no kappa target.", "outcome": "completed", - "evidence": "python3.12 -B research/dirty-host-gauge-binding-seedea2e/verify.py prints PASS_DIRTY_HOST_GAUGE_BINDING: the double-duty borrow and the absorbed-endpoint-with-separate-target are refuted at cut 1 by exactly one direction (count and span feasibility); full absorption alone passes and is flagged as a contract change; three dropped-gauge counterexamples for the operator identity; the PR1664 section 5.2 arithmetic reproduced with an M<=6 mutant refuted; pre-positioned dirt earns no credit; and all 156 enumerated restored-host regions satisfy (C-down) and the exact identity sum_j need_j = q*rank(S) + H_end.", + "evidence": "python3.12 -B research/dirty-host-gauge-binding-seedea2e/verify.py prints PASS_DIRTY_HOST_GAUGE_BINDING: the double-duty borrow and the absorbed-endpoint-with-separate-target are refuted at cut 1 by exactly one direction (count and span feasibility); full absorption alone passes and is flagged as a contract change; three dropped-gauge counterexamples for the sufficient operator hypotheses (each cannot simply be deleted, none proved necessary) plus the cancellation regression control R = I + E01, T = I + E12, T^{-1} = I - E12, where both touches fail to commute with R yet T^{-1} T R = R T^{-1} T = R and the sufficient-only condition accepts the equality; the PR1664 section 5.2 arithmetic reproduced with an M<=6 mutant refuted; pre-positioned dirt earns no credit; and all 156 enumerated restored-host regions satisfy (C-down) and the exact identity sum_j need_j = q*rank(S) + H_end.", "author": "Aaron Wang (with help from opencode)", "ai_assistance": "Substantial AI assistance: this session was run by an opencode coding agent (model not cited per donor instruction); the verifier, proof notes and package text were drafted with that assistance and checked by exact replay.", "open_questions": [ diff --git a/research/dirty-host-gauge-binding-seedea2e/VERIFY.json b/research/dirty-host-gauge-binding-seedea2e/VERIFY.json index 62ddad400a..7d402c24c6 100644 --- a/research/dirty-host-gauge-binding-seedea2e/VERIFY.json +++ b/research/dirty-host-gauge-binding-seedea2e/VERIFY.json @@ -15,7 +15,7 @@ "{package}/verify.py" ], "timeout_seconds": 120, - "checks": "PASS_DIRTY_HOST_GAUGE_BINDING: smallest falsifying instances first (double-duty borrow and absorbed-endpoint-with-separate-target refuted at cut 1 by count and span feasibility; full absorption flagged as an endpoint-contract change), operator gauges with three dropped-gauge counterexamples, the PR1664 section 5.2 canonical arithmetic with an M<=6 mutant refuted, pre-positioned dirt earning no credit, and all 156 restored-host toy regions satisfying (C-down) and the exact identity sum_j need_j = q*rank(S) + H_end." + "checks": "PASS_DIRTY_HOST_GAUGE_BINDING: smallest falsifying instances first (double-duty borrow and absorbed-endpoint-with-separate-target refuted at cut 1 by count and span feasibility; full absorption flagged as an endpoint-contract change), operator gauges stated as sufficient hypotheses with three dropped-gauge counterexamples and a cancellation regression control (R = I + E01, T = I + E12, T^{-1} = I - E12: both touches fail to commute with R yet T^{-1} T R = R T^{-1} T = R) that the sufficient-only condition must not reject, the PR1664 section 5.2 canonical arithmetic with an M<=6 mutant refuted, pre-positioned dirt earning no credit, and all 156 restored-host toy regions satisfying (C-down) and the exact identity sum_j need_j = q*rank(S) + H_end." } ] } diff --git a/research/dirty-host-gauge-binding-seedea2e/verify.py b/research/dirty-host-gauge-binding-seedea2e/verify.py index 230120842c..11b8157d08 100644 --- a/research/dirty-host-gauge-binding-seedea2e/verify.py +++ b/research/dirty-host-gauge-binding-seedea2e/verify.py @@ -15,8 +15,10 @@ This script implements (C-down) and the crossing feasibility condition exactly, and audits the *credit binding* of the idle-axis hosted-residual mechanism -(research/idle-axis-hosting/PROOF.md): which entry/exit gauges make a hosting -move operator-identical, and how much mass a hosted pending factor may claim +(research/idle-axis-hosting/PROOF.md): which entry/exit gauges *suffice* to make +a hosting move operator-identical (sufficient legality hypotheses of the +inherited interface; not claimed necessary -- see the cancellation control +below), and how much mass a hosted pending factor may claim credit for. All checks are exact rational arithmetic; entry rows are identity-basis rows (arbitrary dirty content), so row equality covers every dirty input by linearity. @@ -211,6 +213,9 @@ def check_operator_gauges(): The hosted version applies I_mu' (the advance off the hosted block) followed by the moved factor; the gauges make that equal the original advance I_mu. Controls: escape, overlap order dependence, out-of-window touch. + The gauges are sufficient legality hypotheses only: each control shows one + hypothesis cannot simply be deleted, not that any of them is necessary for + operator equality (see check_cancellation_control). """ d = 3 moved = shear(d, 0, 2) # hosted pending factor on S'={0} @@ -230,16 +235,58 @@ def check_operator_gauges(): # overlap: two moved factors on overlapping blocks do not commute m1, m2 = shear(d, 0, 1), shear(d, 1, 0) report("gauge-overlap-order-refuted", matmul(m1, m2) != matmul(m2, m1), - "overlapping hosted blocks are order-dependent: disjointness (count " - "each pending factor once) is required for an order-free composition") + "the exhibited overlapping hosted blocks are order-dependent; " + "disjointness (count each pending factor once) is the inherited " + "interface's sufficient premise for an order-free composition") # out-of-window touch: an intervening touch T between the residual write at # I1 and the advance at I_mu; hosting moves the factor past T T = shear(d, 2, 0) total_orig_w = matmul(ip, matmul(T, moved)) total_hosted_w = matmul(imu, T) report("gauge-window-refuted", total_orig_w != total_hosted_w, - "an intervening touch that does not commute with the moved factor " - "breaks the composition: the window condition is required") + "a single intervening touch that does not commute with the moved " + "factor breaks the composition: the no-touch window is a sufficient " + "premise, not a necessary one (see the cancellation control)") + + +def commute(a, b): + return matmul(a, b) == matmul(b, a) + + +def check_cancellation_control(): + """Regression control: the sufficient-only hypotheses must NOT reject a + genuine equality (reviewer's counterexample, PR 1837 comment 6173237648). + + Over Q take R = I + E01, T = I + E12, T^{-1} = I - E12. Both T and T^{-1} + fail to commute with R, so the sufficient window premise ("no intervening + touch of the host", or "every intervening touch commutes with the moved + factor") is not met in this instance; yet moving R across the consecutive + touches T, T^{-1} preserves the complete operator: + + T^{-1} T R = R T^{-1} T = R. + + This is a genuine equality (the touches cancel as a composite), checked + below with this package's composed-linear-map machinery (exact integer + arithmetic on these entries). The corrected condition is sufficient only, + so it must accept this instance rather than reject it: premise failure is + not an operator change, and cancellation-based routes stay open. + """ + d = 3 + r = shear(d, 0, 1) # R = I + E01 + t = shear(d, 1, 2) # T = I + E12 + tinv = eye(d) + tinv[1][2] = -1 # T^{-1} = I - E12 + premise_met = commute(r, t) and commute(r, tinv) + lhs = matmul(matmul(tinv, t), r) # T^{-1} T R + rhs = matmul(r, matmul(tinv, t)) # R T^{-1} T + report("cancellation-touches-noncommuting", not premise_met, + "T = I + E12 and T^{-1} = I - E12 each fail to commute with " + "R = I + E01, so the sufficient window premise is not met here") + report("cancellation-equality-not-rejected", (not premise_met) and lhs == rhs == r, + "T^{-1} T R = R T^{-1} T = R = [[1,1,0],[0,1,0],[0,0,1]] exactly, so the " + "sufficient-only condition must NOT reject this instance: absence of " + "individually noncommuting touches is sufficient, not necessary, and " + "cancellation-based routes remain open") def check_engine_canonical(): @@ -351,6 +398,7 @@ def main(): check_smallest_falsifier() print("--- operator gauges ---") check_operator_gauges() + check_cancellation_control() print("--- credit accounting ---") check_engine_canonical() check_prepositioned_dirt()