Independent bound: deferred R439 scatter optimum is 94 over all undo ideals

research/r439-deferred-ideal-optimum/PROOF.md

@@ -0,0 +1,173 @@
+# Exact optimum over all dependency ideals
+
+## Statement and scope
+
+Take the PR1062 word pinned in SOURCES.json. Number its 111 target rows from 0 through 110.
+Number the 306 elementary gates in its literal target-basis undo from 0 through 305.
+These are local target indices; physical target register r is 111+r.
+
+Let E be the target-basis preparation and S the 111-by-9 binary scatter matrix.
+The undo is the literal reverse of E. Every undo gate has the form d ^= s.
+All target-basis gates use frame zero.
+
+For every subset I of the 306 undo gates, impose this condition:
+if i belongs to I and an earlier gate j does not commute with i, then j belongs to I.
+Such subsets are precisely the dependency ideals used in PR2115, section 5.
+There is no restriction on the size of I.
+Let G_I apply its selected gates in their original order.
+
+**Theorem.** The minimum of nnz(G_I E S), over all these ideals I, is exactly 94.
+The ideal {31,51,52} attains the minimum.
+
+Here nnz counts ones over F2. Each scatter entry costs one ADD.
+All 306 undo gates remain present, either before or after the scatter.
+This result does not optimize a different basis circuit, interleaving within the scatter, frame paths, or extra workspace.
+It does not assert supplier admission or a new exponent.
+
+## Constant increments from a complete circuit
+
+Write P=ES. Execute the complete undo on P once.
+For gate i=(d_i,s_i), let a_i be its source row immediately before that gate in this complete execution.
+For an ideal I, the resulting row d is
+
+```text
+P_d XOR XOR_{i in I, d_i=d} a_i.                       (1)
+```
+
+**Proof.** Proceed in the order of selected gates.
+Every earlier gate that writes s_i does not commute with gate i, so the ideal contains it.
+By induction, each such earlier selected gate adds the same source row as in the complete execution.
+Thus s_i has its complete-execution value when gate i runs.
+This proves the claim about its increment, and summing the increments gives (1).
+
+The empty prefix supplies the induction base.
+
+For completeness, two elementary transvections (d,s) and (e,t) commute exactly when d is not t and e is not s.
+The source binding contains 850 earlier noncommuting pairs.
+The independent checker reconstructs these pairs by multiplying their small coefficient matrices.
+
+Equation (1) is a consequence of the ideal condition.
+An arbitrary nonideal subset does not establish a valid circuit through this equation.
+In particular, {31,47,51,52} has relaxed cost 93 but omits necessary predecessors of gate 47.
+The verifier rejects that subset.
+
+## A certificate using row weights
+
+Represent each nine-bit row by its integer mask, with scatter column 0 as the least significant bit.
+Let w_d be the Hamming weight of row d after applying (1).
+For each row, temporarily allow every subset of the gates that write that row, ignoring dependencies.
+This only enlarges the feasible set, so a row lower bound remains valid for every ideal.
+
+There are 1,386 such row subsets in total.
+The most populated row has eight writer gates, so its table has 256 cases.
+CERTIFICATE.json lists each row's initial mask, writer indices, case count, and minimum.
+The initial total is 97.
+Every row except 24,28,47,68,93 has minimum equal to its initial weight.
+The five exceptional minima are respectively 4,0,1,1,1, with initial weights 5,2,2,2,2.
+
+The following seven exact row expressions contain every nonzero coefficient needed for the stronger bound.
+Here z_i is 1 when gate i belongs to I, and multiplication by z_i selects a mask or zero.
+All displayed additions are bitwise XOR, not integer addition.
+Zero increments do not appear.
+
+| Row d | Row mask after selected increments |
+|---:|---|
+| 6 | 3 z_36 XOR 25 z_288 |
+| 24 | 171 XOR 128 z_31 XOR 372 z_186 |
+| 28 | 3 XOR z_51 XOR 2 z_52 XOR 67 z_53 XOR 256 z_54 XOR 104 z_196 |
+| 47 | 96 XOR 32 z_47 XOR 124 z_266 XOR 425 z_298 |
+| 68 | 257 XOR 3 z_62 XOR 256 z_93 XOR 67 z_119 XOR 488 z_289 |
+| 93 | 3 XOR 257 z_37 XOR 2 z_39 XOR 96 z_159 |
+| 96 | 272 XOR 96 z_6 XOR 4 z_7 |
+
+Their complete truth tables give these implications:
+
+1. w_47 < 2 implies z_47=1; z_6=1 implies w_96 >= 4.
+2. w_68 < 2 implies z_93=1.
+3. w_93 < 2 implies z_39=1; z_36=1 implies w_6 >= 2.
+
+These are small explicit finite statements, not numerical approximations.
+Both checkers exhaust their truth tables, including choices that violate the ideal condition.
+The relevant ideal implications are
+
+```text
+z_47 <= z_6,
+z_93 <= z_37 <= z_36,
+z_39 <= z_36.                                          (2)
+```
+
+Each implication in (2) is a direct noncommuting dependency, not a guessed relation.
+
+First group rows 47 and 96. If w_47 >= 2, their sum is at least 2+2=4.
+Otherwise (2) forces z_6=1, and their sum is at least 1+4=5.
+Thus w_47+w_96 >= 4 in either case.
+
+Next group rows 68,93,6. If neither of the first two weights drops, their sum is at least 2+2+0=4.
+If either drops, (2) forces z_36=1, giving a sum of at least 1+1+2=4.
+Thus this second group always costs at least 4.
+
+The other 104 rows exclude these five grouped rows and rows 24,28.
+Their individual minima sum to 82.
+Rows 24 and 28 cost at least 4 and 0.
+Adding the disjoint groups proves
+
+```text
+nnz(G_I E S) >= 82 + 4 + 0 + 4 + 4 = 94.               (3)
+```
+
+No search over a bounded ideal size enters (3).
+The certificate covers every ideal, through the row relaxation and its four necessary dependencies.
+
+## Attainment and complete word boundary
+
+Gates 31,51,52 have no earlier noncommuting predecessor, so their set is an ideal.
+Their literal execution changes only row 24 from 171 to 43 and row 28 from 3 to 0.
+The total weight falls from 97 to 94.
+This is the same attaining split already reported by Sagar Thakrar in PR2115.
+The new contribution is its optimality over every ideal.
+
+To connect the optimization with the stated circuit class, write the complete undo as U.
+Any omitted gate that precedes a selected gate commutes with it, by the ideal condition.
+Repeatedly exchanging these pairs puts selected gates first without changing the product.
+Thus U equals the remaining undo after G_I, in execution order.
+
+Keep G_I in D, use listing G_I E S, and put the remaining undo before the original B.
+A never reads or writes a target, so the target basis commutes past A.
+The copied totals depend only on sources and helpers and remain unchanged.
+The modified scatter contributes G_I E S c to the targets for arbitrary copied values c.
+The remaining undo cancels G_I E and restores the original S c contribution.
+After this undo, the entire state agrees with the original word before B.
+
+The unchanged B and C therefore give the same boundary.
+
+This argument is a binary coefficient identity on arbitrary source, target, and helper inputs.
+It extends to any F2-module through the same coefficients.
+The verifier also executes the literal COPY/ERASE stream on all 661 input columns, in both directions.
+It obtains (x,y,h) -> (x,y+x,h), including restoration of every arbitrary helper.
+
+The 306 undo ADDs move but remain charged. The scatter decreases from 527 to 94.
+The complete local ADD count is therefore 11,500-527+94=11,067.
+Nine COPY/ERASE pairs, preparation, helpers, A, C, and the original B remain present.
+
+All moved gates use frame zero and preserve the target paths and recursive profile under the inherited realization.
+PR2115 supplies the chronological argument and its reported guards for this exact attaining split.
+This package does not repeat its native, hosting, precision, or supplier-admission obligations.
+
+## Independent validation and limits
+
+The primary checker follows forward row states to derive P and all 306 increments.
+It enumerates row subsets and checks (2), (3), and the complete attaining word.
+
+The separate checker imports no primary or predecessor implementation.
+It derives every coefficient through backward propagation of a row functional through the original circuit.
+It evaluates all row choices as Boolean truth-table bit planes.
+It reconstructs the dependency relation by literal multiplication of transvection matrices.
+It also checks the attaining reorder as a complete 111-by-111 coefficient map.
+These checks validate the crucial coefficients and lower-bound premises through different traversals and models.
+
+They do not constitute independent human review or proof-assistant verification.
+
+Z3 4.15.3 first found that the exact full-ideal model has no solution of cost at most 93.
+That exploratory answer is not a premise of the proof or a runtime dependency.
+The small certificate above replaces solver trust and large ideal enumeration.
+The finite source facts remain tied to the pinned word and the stated gate ordering.

research/r439-deferred-ideal-optimum/README.md

@@ -0,0 +1,71 @@
+# The deferred R439 scatter has exact ideal optimum 94
+
+**Independent verification / finite optimality result; no new supplier or kappa.**
+For the pinned PR1062 word, every dependency ideal of its 306-gate target-basis undo has scatter cost at least 94 ADDs.
+The known ideal {31,51,52} attains 94.
+This closes PR2115's larger-ideal question for this word, with no bound on ideal size.
+
+Sagar Thakrar's [PR2115](https://github.com/CrocSwap/integer-mult-bounds/pull/2115), head `b56dceffad83c88e8ad39ffd82a1bdd55c4130da`, supplies the construction and attaining split.
+Its search checks ideals of size at most four and explicitly leaves larger ideals open.
+The new result is a complete lower bound, not a new circuit or a repeated small census.
+
+[PROOF.md](PROOF.md) gives the exact claim, constant-increment lemma, row inequalities, dependency argument, and attainment.
+Only five rows can improve over the 97-ADD start.
+Necessary dependencies charge three possible improvements back to two other rows.
+The resulting disjoint row bounds sum to 94.
+All 1,386 unrestricted row subsets certify the premises; the proof avoids enumeration of all ideals.
+
+## Reproduce
+
+Standard library only, from the repository root:
+
+```sh
+python3 -I -O -B research/r439-deferred-ideal-optimum/verify.py && python3 -I -O -B research/r439-deferred-ideal-optimum/independent.py
+```
+
+Expected:
+
+```text
+PASS_R439_DEFERRED_IDEAL_OPTIMUM minimum=94 gates=306 row_subsets=1386 dirty_columns=661 controls=5 no_new_kappa
+PASS_INDEPENDENT_IDEAL_AUDIT backward_coefficients=417 row_subsets=1386 matrix_dependencies=850 minimum=94
+```
+
+The primary checker uses forward row states and complete arbitrary-dirty input columns.
+The separate checker uses backward coefficient cones, Boolean truth tables, and literal small-matrix commutators.
+It imports no primary or predecessor engine.
+Five controls reject a cheaper nonideal subset, a missing dependency, a missing compensating cost, an old scatter, and an omitted undo.
+Checks remain active under Python optimization.
+
+The frozen certificate records every row minimum and all consumed coefficients.
+An exact SMT model helped discover the bound; replay uses neither Z3 nor its answer.
+
+## Accounting and scope
+
+The complete attaining word costs 11,500-527+94=11,067 scalar ADDs, as already reported by PR2115.
+All 306 undo gates remain charged, with nine COPY/ERASE pairs and all helpers restored.
+The verifier independently checks all 661 dirty input columns in both directions through the literal stream.
+The construction preserves the inherited frame paths and paid profile; this package does not regenerate their invoice.
+
+The theorem concerns one fixed undo circuit, its nine-column scatter, and every commutation-closed split into D and B.
+It does not cover new basis circuits, different frame paths, scatter interleavings, or extra workspace.
+Native address action, stage hosting, precision/tape, all-size realization, and the multiplication theorem remain inherited or unverified here.
+We claim neither independent human review nor a full selected-frontier replay.
+
+## Open next questions
+
+A different target-basis circuit could improve the deferred objective.
+First price both basis directions and the resulting scatter, then verify the dirty boundary and full precision charge.
+The present optimum applies only to the frozen 306-gate circuit; it supplies no global lower bound for that changed problem.
+Structured scope and blockers appear in [TASK.json](TASK.json).
+
+## Credit
+
+Credit Sagar Thakrar for PR2115's deferred basis and PR1062's composed word.
+Credit Gareth Davidson for the PR915 target basis, with commdata2338, Scott Woolsey Biggart, and Sagar Thakrar in its lineage.
+The R439 word retains Sricharan Vagvala's helper stars, Aaron Wang's B circuits, Ross Richardson's frame circuit, and DreamingOfClouds' tuning.
+The interface and exporter lineage includes eumemic, Zhihao Chen, woklerx, Arham Tahir, and Dylan Crow.
+All predecessor source files remain unchanged.
+
+Prepared for Charles Bethin with substantial OpenAI Codex assistance in the proof, implementation, checks, and writing.
+The two implementations have the same AI author; their independence is algorithmic, not human.
+New material is Apache-2.0.

research/r439-deferred-ideal-optimum/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "e8870e5917057d59b730eb14721a778639eca050",
+      "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7"
+    },
+    {
+      "path": "research/r439-bsection-stars-seed01/candidate.json.gz",
+      "usage": "input",
+      "git_blob": "9a17b4920334878d6c949191f6931bd97126fe3c",
+      "sha256": "b452d2c2b0b2a546d1105b1da9769aa78e5c54d6f00e97b30c77e3f54ce445ee"
+    }
+  ]
+}

research/r439-deferred-ideal-optimum/TASK.json

@@ -0,0 +1,106 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-helper-contract",
+  "priority_revision": 4,
+  "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+  "original_card": {
+    "id": "bit-helper-contract",
+    "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?",
+    "starting_points": [
+      "research/r439-bsection-stars-seed01/README.md",
+      "research/r439-copy-path-sharing-barrier/README.md"
+    ],
+    "methods": [
+      "Derive a replacement interface lemma and price its implementation.",
+      "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement."
+    ],
+    "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "research/r439-bsection-stars-seed01/verify.py"
+      ],
+      "expected": "PASS_R439_BSECTION_STARS",
+      "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.",
+    "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.",
+    "allowed_variations": [
+      "Choose one helper-star or quartet instance; narrow to one boundary implication."
+    ],
+    "scope_change_triggers": [
+      "Changing only source count or scalar addition count without an interface argument."
+    ],
+    "overlap_terms": [
+      "H2_D_frame0_targets_from_helpers",
+      "K_equals_D",
+      "helper-star"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Prove the exact minimum scatter ADD count over all dependency ideals of the pinned PR1062 306-gate target-basis undo, answering the explicit PR2115 open question without an ideal-size bound.",
+  "scope_change_reason": "The user assigned bit-supplier seed 9. The retained semantic D lemma already covers restored helper mixing. This side result completes the finite optimization question in PR2115 rather than deriving that existing lemma again.",
+  "bottleneck_link": "This closes a specific local optimization route under a changed target-basis interface. It does not change paid recursive rank mass, the selected bit supplier, or kappa.",
+  "budget_minutes": 45,
+  "stop_rule": "Prove the full ideal bound or save the incomplete model locally. No further size-bounded census merits publication. Reserve the final quarter for verification and handoff.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and CERTIFICATE.json: exact lower bound 94, attained by {31,51,52}, 1386 unrestricted row subsets, four essential dependencies, separate backward coefficients and matrix commutators, 661 dirty columns in both directions, and five negative controls.",
+  "author": "Charles Bethin with substantial OpenAI Codex assistance",
+  "ai_assistance": "Substantial OpenAI Codex assistance in mathematics, implementation, verification and writing. Same AI author for both algorithms; no independent human review or proof-assistant verification.",
+  "open_questions": [
+    {
+      "question": "Can a different target-basis circuit beat the fully priced deferred objective?",
+      "why_it_matters": "The exact 94 bound covers only this fixed undo word. A new circuit changes the feasible problem.",
+      "first_step": "Price preparation, undo and scatter together, then verify the arbitrary-dirty boundary and precision charge.",
+      "blocked_by": "No such completed candidate or physical supplier invoice is supplied."
+    }
+  ],
+  "session_id": "01a1335e-7a24-73c3-a549-9bcb5496a363",
+  "start_time": "2026-10-15T02:56:33Z",
+  "experiment_seed": 9,
+  "seed_method": "secrets.randbelow(100), operating-system random",
+  "track": "bit supplier",
+  "coordination": "No pinned coordination issue at the 03:00 UTC query. Local claim saved in the originating research capture.",
+  "predecessors": [
+    {
+      "pr": 2115,
+      "head": "b56dceffad83c88e8ad39ffd82a1bdd55c4130da",
+      "author": "Sagar Thakrar",
+      "credit": "Deferred target-basis contract, ideal-split construction and known 94-ADD attaining split",
+      "proof_sha256": "3a921c0e7cb8670dc28980e08635e0c1361f88f5391b14254438b56a699e488b"
+    },
+    {
+      "pr": 1062,
+      "author": "Sagar Thakrar",
+      "credit": "Pinned 11500-ADD R439 B/star word, retained at the base commit"
+    }
+  ],
+  "overlap": {
+    "open_prs": 495,
+    "open_prs_complete_pagination": true,
+    "recent_discussions": 12,
+    "targeted_discussion_searches": [
+      "order ideal",
+      "deferred target"
+    ],
+    "limits": "Targeted search is not a complete comment or code-diff index. Local package READMEs and review ledger also checked. Final live refresh recorded before publication.",
+    "prepublication": {
+      "checked_at": "2026-10-15T03:14:32.459445Z",
+      "canonical_main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+      "open_prs": 501,
+      "open_prs_complete_pagination": true,
+      "matching_prs": [
+        2115
+      ],
+      "predecessor_head": "b56dceffad83c88e8ad39ffd82a1bdd55c4130da",
+      "predecessor_comments": 0,
+      "predecessor_reviews": 0,
+      "cached_discussions": 937,
+      "cached_discussions_fetched_at": "2026-10-15T01:39:09.767583Z",
+      "cached_discussions_complete_pagination": true,
+      "cached_warning": "Offline snapshot may miss later comments; 12 recent live discussions and targeted live searches supplement it."
+    }
+  }
+}